[acl2/acl2] d6080e: [Remora] Improve some doc.

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: d6080e02ee0adf38e5a531f8d9f249fdda4a987c
https://github.com/acl2/acl2/commit/d6080e02ee0adf38e5a531f8d9f249fdda4a987c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

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


Commit: 1fbcd97d91c466e7ab9c91df84074d94c369125a
https://github.com/acl2/acl2/commit/1fbcd97d91c466e7ab9c91df84074d94c369125a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

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

For consistency with upcoming extensions.


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

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

Log Message:
-----------
[Remora] Add model of primitive ops as values.


Commit: 8a0422e67eb04a351c485fab189ee35e1b5f0e8e
https://github.com/acl2/acl2/commit/8a0422e67eb04a351c485fab189ee35e1b5f0e8e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

Changed paths:
M books/projects/abnf/top.lisp

Log Message:
-----------
[ABNF] Improve top-level doc.


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

Changed paths:
M books/projects/abnf/grammar-definer/top.lisp
M books/projects/abnf/grammar-parser/top.lisp
M books/projects/abnf/grammar-printer/top.lisp
M books/projects/abnf/notation/top.lisp

Log Message:
-----------
[ABNF] XDOC hierarchy tweaks.


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

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

Log Message:
-----------
[Remora] Fix handling of `let` in ispace variable renaming.


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

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

Log Message:
-----------
[Remora] Fix handling of `let` in type variable renaming.


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

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

Log Message:
-----------
[Remora] Fix handling of `let` in expression variable renaming.


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

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

Log Message:
-----------
[Remora] Fix handling of `let` in ispace variable substitution.


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

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

Log Message:
-----------
[Remora] Improve initial static environment.

Now it consists of the selection of primitive operations whose dynamic semantics
is in `primitives-evaluation.lisp`. The exact names are taken by the
`RemoraPrelude.hs` file in the Haskell implementation of Remora.


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

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

Log Message:
-----------
[Remora] Align the model of primitive operation values.

This is now consistent with the ones in `primitives-evaluation.lisp` and the
ones in the initial static environment (see `primop-types`).


Commit: 01d4b00572aa4a7add29d52b2a1f422f80374ca2
https://github.com/acl2/acl2/commit/01d4b00572aa4a7add29d52b2a1f422f80374ca2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

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


Commit: 1214e99af8ab2941c92cd8c173f610e7ea35fe02
https://github.com/acl2/acl2/commit/1214e99af8ab2941c92cd8c173f610e7ea35fe02
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

Log Message:
-----------
[Remora] Fix handling of `let` in type variable substitution.


Commit: 178bae66cbbc6156409d38bff89128e2fbba29dc
https://github.com/acl2/acl2/commit/178bae66cbbc6156409d38bff89128e2fbba29dc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

Log Message:
-----------
[Remora] Fix handling of `let` in expression variable substitution.


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

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

Log Message:
-----------
[Remora] Extend primitive operation types and values.

Align to latest `primitives-evaluation.lisp`.


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

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

Log Message:
-----------
[Remora] Extend model of expression values.

Add a summand for primitive operations. Minimally extend evaluation machinery to
certify, but proper handling of primitive operations will be added in upcoming
commits.


Commit: 4649f0e23b13dadd0d1a8af34ee3c1996ae7055f
https://github.com/acl2/acl2/commit/4649f0e23b13dadd0d1a8af34ee3c1996ae7055f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

Log Message:
-----------
[Remora] Add type checking of bracket expressions.


Commit: 441fac232f86b97f0806a9a411fad99b059e53dd
https://github.com/acl2/acl2/commit/441fac232f86b97f0806a9a411fad99b059e53dd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

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


Commit: 33855b26ecbbeb3e1e519c1641e6960a9bf58da6
https://github.com/acl2/acl2/commit/33855b26ecbbeb3e1e519c1641e6960a9bf58da6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

Log Message:
-----------
[Remora] Improve a variable name.


Commit: 10bcffad7257cb9fc63c218807b0be60da2404a3
https://github.com/acl2/acl2/commit/10bcffad7257cb9fc63c218807b0be60da2404a3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

Log Message:
-----------
[Remora] Define the initial dynamic environment.

This contains the (current) primitive operations.


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

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

Log Message:
-----------
[Remora] Add mapping of primitive ops to their arities.


Commit: 33136a011d37097886e548e5110d1c768d5a6fbe
https://github.com/acl2/acl2/commit/33136a011d37097886e548e5110d1c768d5a6fbe
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

Log Message:
-----------
[Remora] Factor some type-checking code.

This is in preparation for an extension, but it has the added benefit of
obviating the need for a specific lemma with slightly large hints.


Commit: 052609bd649b9ceb0adbffffbf6cfe62a34f35f2
https://github.com/acl2/acl2/commit/052609bd649b9ceb0adbffffbf6cfe62a34f35f2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

Log Message:
-----------
[Remora] Add top-level primitive op evaluator.


Commit: 798cf70870b63896175fa7dfa4a572011e9a747a
https://github.com/acl2/acl2/commit/798cf70870b63896175fa7dfa4a572011e9a747a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

Log Message:
-----------
[Remora] Factor some type-checking code.

This is for an upcoming extension.


Commit: 85feba13a8cd5c81a2ef8014bed92dff50340cb4
https://github.com/acl2/acl2/commit/85feba13a8cd5c81a2ef8014bed92dff50340cb4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

Log Message:
-----------
[Remora] Factor some type-checking code.

To support an upcoming extension.


Commit: 3c6846ef5d967e8a27ce02948046f2e51b03ae3e
https://github.com/acl2/acl2/commit/3c6846ef5d967e8a27ce02948046f2e51b03ae3e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

Log Message:
-----------
[Remora] Avoid deferring some guard proofs.


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

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

Log Message:
-----------
[Remora] Add type checking of combine applications.


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

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

Log Message:
-----------
[Remora] Remove some now-unneeded doc.


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

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

Log Message:
-----------
[Remora] Generalize some dynamic semantics code.

Instead of just looking for a representative lambda abstraction in a function
array, we also look for a primitive operation. We add code to treat them
uniformly.


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

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

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


Commit: 1ecaefed3fdb1cb3c21602b6009f3d3a657551e8
https://github.com/acl2/acl2/commit/1ecaefed3fdb1cb3c21602b6009f3d3a657551e8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

Log Message:
-----------
[Remora] Add type checking of most let bindings.


Commit: 597fbd286612ecefc04f0a8c8705a099c98908bc
https://github.com/acl2/acl2/commit/597fbd286612ecefc04f0a8c8705a099c98908bc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

Log Message:
-----------
[Remora] Complete evaluation of primitive ops.

Connect the machinery to the main evaluation functions.


Commit: 84466e477888b5de82291ad1f6ee7aafbf4f55e3
https://github.com/acl2/acl2/commit/84466e477888b5de82291ad1f6ee7aafbf4f55e3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

Log Message:
-----------
[Remora] Some cleanup.


Commit: 6798217219c807c9538ec2e31630cc4059b10021
https://github.com/acl2/acl2/commit/6798217219c807c9538ec2e31630cc4059b10021
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

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

Log Message:
-----------
[Remora] Avoid a theorem by enabling an existing rule.


Commit: 9c3fa975f72b765e697c0bb4524ea0cf041c1fa1
https://github.com/acl2/acl2/commit/9c3fa975f72b765e697c0bb4524ea0cf041c1fa1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)

Changed paths:
M books/kestrel/remora/nat-lists.lisp
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Factor library theorem.


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

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

Log Message:
-----------
[Remora] Shorten a function name.


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

Changed paths:
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp

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


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

Changed paths:
M books/projects/abnf/grammar-definer/top.lisp
M books/projects/abnf/grammar-parser/top.lisp
M books/projects/abnf/grammar-printer/top.lisp
M books/projects/abnf/notation/top.lisp
M books/projects/abnf/top.lisp

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


Compare: https://github.com/acl2/acl2/compare/056fdb2cd8ae...d32054e3ebbf

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