[acl2/acl2] 217a83: [Remora] Add closures to type values.

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 217a83b941acbae06721363e56e3590243427925
https://github.com/acl2/acl2/commit/217a83b941acbae06721363e56e3590243427925
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/type-values-and-environments.lisp

Log Message:
-----------
[Remora] Add closures to type values.

These are unused for now, but this commit makes type values and type dynamic
environments mutually recursive, and adds the environment slots in the type
values that include unevaluated type ASTs.


Commit: 4e8e29b43210db8d9c578eff3359089fd4755c7c
https://github.com/acl2/acl2/commit/4e8e29b43210db8d9c578eff3359089fd4755c7c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

Changed paths:
M books/kestrel/remora/ispace-values-and-environments.lisp
M books/kestrel/remora/type-values-and-environments.lisp

Log Message:
-----------
[Remora] Add environment restriction ops.


Commit: 7ac1132cdf06dcaa7e3de840c12141deaecabd6c
https://github.com/acl2/acl2/commit/7ac1132cdf06dcaa7e3de840c12141deaecabd6c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

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

Log Message:
-----------
[Remora] Store proper environments in type values.


Commit: cb804f813c07f92a44d7a3c81b40ee15a19a5832
https://github.com/acl2/acl2/commit/cb804f813c07f92a44d7a3c81b40ee15a19a5832
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

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

Log Message:
-----------
[Remora] Use the type closures in evaluation.


Commit: 0e7affdba509f8d94d961f7dd323c80606e5c180
https://github.com/acl2/acl2/commit/0e7affdba509f8d94d961f7dd323c80606e5c180
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

Changed paths:
A books/kestrel/remora/evaluation-tests.lisp

Log Message:
-----------
[Remora] Add some evaluation tests.


Commit: 9519df2747b39c58bbd759c71fc00694c688e2bf
https://github.com/acl2/acl2/commit/9519df2747b39c58bbd759c71fc00694c688e2bf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

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

Log Message:
-----------
[Remora] Add two evaluation tests.

These demonstrate the type closures.


Commit: 93cfd10b079ae309fd9d2f445104018dc8084f42
https://github.com/acl2/acl2/commit/93cfd10b079ae309fd9d2f445104018dc8084f42
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

Changed paths:
A books/kestrel/remora/base-values.lisp
M books/kestrel/remora/expression-values-and-environments.lisp

Log Message:
-----------
[Remora] Factor base values in new file/topic.


Commit: 7b729b799552236f479da24d5cd178564d30005a
https://github.com/acl2/acl2/commit/7b729b799552236f479da24d5cd178564d30005a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

Changed paths:
M books/kestrel/remora/expression-values-and-environments.lisp
A books/kestrel/remora/primitive-operation-values.lisp

Log Message:
-----------
[Remora] Factor primop values into new file/topic.


Commit: 003eb9ea48775bc3c061afa2ea5c525f5baa07f5
https://github.com/acl2/acl2/commit/003eb9ea48775bc3c061afa2ea5c525f5baa07f5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

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

Log Message:
-----------
[Remora] Reduce book inclusions.


Commit: 7c313763dd8472afa2fac5d5ac5d0eab04199087
https://github.com/acl2/acl2/commit/7c313763dd8472afa2fac5d5ac5d0eab04199087
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

Changed paths:
M books/kestrel/axe/trim-intro-rules-axe.lisp
M books/kestrel/bv/bv-syntax.lisp
M books/kestrel/bv/leftrotate-rules.lisp
M books/kestrel/bv/leftrotate32.lisp
M books/kestrel/bv/trim-elim-rules-bv.lisp
M books/kestrel/bv/trim-intro-rules.lisp
M books/kestrel/c/transformation/json-rpc/README.md
M books/kestrel/c/transformation/json-rpc/struct-type-split.lisp
M books/kestrel/c/transformation/json-rpc/tests/struct-type-split.lsp
M books/kestrel/remora/value-printing.lisp

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


Compare: https://github.com/acl2/acl2/compare/5451e607479a...7c313763dd84

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