[acl2/acl2] fe21ea: [ABNF] Add customization file to subdir.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: fe21eab8621ef72e3b2aa505a3c0c564d3bca634
https://github.com/acl2/acl2/commit/fe21eab8621ef72e3b2aa505a3c0c564d3bca634
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
A books/projects/abnf/tree-operations/acl2-customization.lsp

Log Message:
-----------
[ABNF] Add customization file to subdir.


Commit: d6b95d911ea5f22b0c1458d2042066777470af96
https://github.com/acl2/acl2/commit/d6b95d911ea5f22b0c1458d2042066777470af96
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/projects/abnf/notation/semantics.lisp
A books/projects/abnf/tree-operations/subtree-operations.lisp
M books/projects/abnf/tree-operations/top.lisp

Log Message:
-----------
[ABNF] Move some tree ops to a new file/topic.


Commit: eaa850a338ba1894363c56c350ffbd99d7f96e0e
https://github.com/acl2/acl2/commit/eaa850a338ba1894363c56c350ffbd99d7f96e0e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/extra-grammatical-restrictions.lisp

Log Message:
-----------
[Remora] Adapt to ABNF library changes.


Commit: 78ea53e2a60ab2d74fbfbe89340d729810a10970
https://github.com/acl2/acl2/commit/78ea53e2a60ab2d74fbfbe89340d729810a10970
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp

Log Message:
-----------
[Remora] Add a fixtype.


Commit: a121585bcf6b74948310e50200260d11c36e10d6
https://github.com/acl2/acl2/commit/a121585bcf6b74948310e50200260d11c36e10d6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp

Log Message:
-----------
[Remora] Add some derived fixtypes.


Commit: 6d688a1eacdba2741980565fece052ecab6bd2da
https://github.com/acl2/acl2/commit/6d688a1eacdba2741980565fece052ecab6bd2da
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Generalize static environments.

Instead of just sets of ispace and type variables, use maps from ispace and type
variables to optional ispaces and optional types. These are equivalent to sets
when the optional ispaces and types are absent, but they will be present in an
upcoming extension to handle `let`s of ispaces and types.


Commit: 5ed3d52fd91433329c6a314f7d12147a60c640b2
https://github.com/acl2/acl2/commit/5ed3d52fd91433329c6a314f7d12147a60c640b2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp

Log Message:
-----------
[Remora] Add a type annotation to the ASTs.

This is the type of the body of a lambda. The type is optional, because there is
no concrete syntax for it. It will be calculated by type checking.


Commit: 7cd3d071f8bdfb36a068235b9ba4da15f40d81bf
https://github.com/acl2/acl2/commit/7cd3d071f8bdfb36a068235b9ba4da15f40d81bf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Improve model of lambda values.

Add a slot for an optional type value for the body, mirroring the AST.


Commit: 66220cb5906744f11043a657000cacb280e6858e
https://github.com/acl2/acl2/commit/66220cb5906744f11043a657000cacb280e6858e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Extend evaluation of lambdas.

Have it populate the optional type value slot.


Commit: 4e9b0c0e2b8faebf1652350fcdb94005171b9bc8
https://github.com/acl2/acl2/commit/4e9b0c0e2b8faebf1652350fcdb94005171b9bc8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Add some code to handle ispace/type bindings.

These are functions to expand ispaces and types according to the maps in the
static environment.


Commit: 56f7e21d0308daf2dab567b580c721aa597aff6d
https://github.com/acl2/acl2/commit/56f7e21d0308daf2dab567b580c721aa597aff6d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Improve a definition.


Commit: e7f6bf072ac5f92e567bc28aba4db3242211e3f6
https://github.com/acl2/acl2/commit/e7f6bf072ac5f92e567bc28aba4db3242211e3f6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Add mapping from primitive ops to their type values.

This is more general, and will subsume some of the other mappings.


Commit: 41a9c9bf91c91ed2e82643f35eacfb4e931124b5
https://github.com/acl2/acl2/commit/41a9c9bf91c91ed2e82643f35eacfb4e931124b5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Add two more helper functions.


Commit: 634e0ce9b69c991bf82875d615f67deaf9b5b0b7
https://github.com/acl2/acl2/commit/634e0ce9b69c991bf82875d615f67deaf9b5b0b7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp

Log Message:
-----------
[Remora] Expand some doc.


Commit: a0c4a7cd6d9c593800ccb331aa51e453587c5bad
https://github.com/acl2/acl2/commit/a0c4a7cd6d9c593800ccb331aa51e453587c5bad
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Add two theorems and simplify a definition.

Now the arity of a primitive operation can be derived from its type.


Commit: 4870815b671d15f8334e2f717f798d149803573e
https://github.com/acl2/acl2/commit/4870815b671d15f8334e2f717f798d149803573e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Expand some doc.


Commit: 4f01bf61798c21ff69ec385b8ff83e8d0b1cf8e8
https://github.com/acl2/acl2/commit/4f01bf61798c21ff69ec385b8ff83e8d0b1cf8e8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
Merge.


Commit: 0ca04219037c0f73cc25b029fc7b392ed1e704ac
https://github.com/acl2/acl2/commit/0ca04219037c0f73cc25b029fc7b392ed1e704ac
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/remora/extra-grammatical-restrictions.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/projects/abnf/notation/semantics.lisp
A books/projects/abnf/tree-operations/acl2-customization.lsp
A books/projects/abnf/tree-operations/subtree-operations.lisp
M books/projects/abnf/tree-operations/top.lisp

Log Message:
-----------
Merge.


Commit: f6f7eed604b68ee8bd70192aee5081c191d7988a
https://github.com/acl2/acl2/commit/f6f7eed604b68ee8bd70192aee5081c191d7988a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/types-formal-subset-and-mapping.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
A books/kestrel/terms-light/doc.acl2
A books/kestrel/terms-light/doc.lisp
A books/kestrel/terms-light/reconstruct-and-untranslate-term-tests.lisp
A books/kestrel/terms-light/reconstruct-and-untranslate-term.lisp
A books/kestrel/terms-light/simple-untranslate-in-term-proofs.lisp
A books/kestrel/terms-light/simple-untranslate-in-term-tests.lisp
A books/kestrel/terms-light/simple-untranslate-in-term.lisp
M books/kestrel/terms-light/top.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/x86/alt-defs.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp

Log Message:
-----------
Merge.


Compare: https://github.com/acl2/acl2/compare/243dfab47d8a...f6f7eed604b6

To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[Alessandro Coglio]

Branch: refs/heads/testing