[acl2/acl2] ef9c1e: [Remora] Factor some code.

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: ef9c1ec3776e57ff59f31af8ddd1640054533856
https://github.com/acl2/acl2/commit/ef9c1ec3776e57ff59f31af8ddd1640054533856
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] Factor some code.


Commit: 41ee22b3ea62cb18d250c127b9420c2a6a04919f
https://github.com/acl2/acl2/commit/41ee22b3ea62cb18d250c127b9420c2a6a04919f
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] Start expanding tyeps and ispaces.


Commit: 858b874ae0321bc9ece93d3d96394d2d6d6fec3d
https://github.com/acl2/acl2/commit/858b874ae0321bc9ece93d3d96394d2d6d6fec3d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)

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

Log Message:
-----------
[Remora] Add another type expansion.


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

Changed paths:
M books/kestrel/arithmetic-light/times.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/leftrotate.lisp
M books/kestrel/bv/leftrotate32.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/sbvlt.lisp
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/crypto/sha-3/sha-3.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/extra-grammatical-restrictions.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/values.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.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/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
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.


Commit: 08f4d1ac084e572fc83b51e95f644596fbc2a9a5
https://github.com/acl2/acl2/commit/08f4d1ac084e572fc83b51e95f644596fbc2a9a5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)

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

Log Message:
-----------
[Remora] Expand types in another place.


Commit: 6919ff5ff5a1862499ef92a531aabf6871d6c900
https://github.com/acl2/acl2/commit/6919ff5ff5a1862499ef92a531aabf6871d6c900
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)

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

Log Message:
-----------
[Remora] Add remaining type expansions.


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

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

Log Message:
-----------
[Remora] Document a critical type-checking invariant.


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

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

Log Message:
-----------
[Remora] Add some ops on static environments.


Commit: 897f1c1eecedc3c03e61c1929fe686be07d04ecd
https://github.com/acl2/acl2/commit/897f1c1eecedc3c03e61c1929fe686be07d04ecd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)

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

Log Message:
-----------
[Remora] Complete type checking for `let`.


Commit: 180972a0e64f9042e09a4e384ebdfb687b16c04c
https://github.com/acl2/acl2/commit/180972a0e64f9042e09a4e384ebdfb687b16c04c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/values.lisp

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


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
A books/kestrel/c/syntax/tests/types-to-tynames.lisp
M books/kestrel/c/syntax/top.lisp
A books/kestrel/c/syntax/types-to-tynames.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/utilities/context-msg.lisp
M books/kestrel/c/transformation/utilities/print-to-str.lisp

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


Compare: https://github.com/acl2/acl2/compare/e97adafdbf17...5d3fdd60a65c

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

[Alessandro Coglio]

Branch: refs/heads/master

[Alessandro Coglio]

Branch: refs/heads/testing