[acl2/acl2] b4a99e: [Remora] Make unary box types optionals in ASTs.

[Alessandro Coglio]

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

Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp

Log Message:
-----------
[Remora] Make unary box types optionals in ASTs.

This mirrors a recent change to the Haskell implementation, related to the
proper handling of the desugaring of n-ary boxes to unary ones.


Commit: 9826583245b7bad3933b5d39933daf92924bd0e2
https://github.com/acl2/acl2/commit/9826583245b7bad3933b5d39933daf92924bd0e2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/desugaring.lisp

Log Message:
-----------
[Remora] Add desugaring of n-ary boxes.


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

Changed paths:
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Adapt type checking to desugared boxes.


Commit: 5fa695ad1ea92fc691392889af51165a6cb0f3a8
https://github.com/acl2/acl2/commit/5fa695ad1ea92fc691392889af51165a6cb0f3a8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)

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

Log Message:
-----------
[Remora] Slightly simplify some code.


Commit: 12160a9624bf90cd057bce1488c4d5dc5fc0d6ff
https://github.com/acl2/acl2/commit/12160a9624bf90cd057bce1488c4d5dc5fc0d6ff
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/arithmetic-light/mod.lisp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/logext.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp

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


Compare: https://github.com/acl2/acl2/compare/0ac898a0a60a...12160a9624bf

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