[acl2/acl2] 1a8188: [Remora] Fix free variable ops.

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 1a81882e5692e96b4c4d908dbf9db83a0a3291f9
https://github.com/acl2/acl2/commit/1a81882e5692e96b4c4d908dbf9db83a0a3291f9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

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

Log Message:
-----------
[Remora] Fix free variable ops.

The fix concerns the treatment of `let`-bound functions. This was known likely
to need revision, and a close examination revealed that.


Commit: 2579e1cad500e4cceee2bb5772525480a80fcf0b
https://github.com/acl2/acl2/commit/2579e1cad500e4cceee2bb5772525480a80fcf0b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-structural-operations.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/frame-flattening.lisp
M books/kestrel/remora/ispace-equivalence.lisp

Log Message:
-----------
[Remora] Improve topic and ruleset names for some folds.


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

Changed paths:
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/deffold-reduce.lisp

Log Message:
-----------
[Remora] Improve `deffold-reduce` and `deffold-map`.

Generate return variables in the same package as the other symbols, not in the
FTY package.


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

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

Log Message:
-----------
[Remora] Use unqualified variable names.

Takes advantage of the improvement to `deffold-...` in the previous commit.


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

Changed paths:
M books/kestrel/remora/package.lsp

Log Message:
-----------
[Remora] Import symbol.


Commit: 048aef4777ed35e7d64ea3cbe388570ecd6461c1
https://github.com/acl2/acl2/commit/048aef4777ed35e7d64ea3cbe388570ecd6461c1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

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

Log Message:
-----------
[Remora] Factor some code for clarity.


Commit: 54eb2bd4b2a48801c478d890278acdc7693980e9
https://github.com/acl2/acl2/commit/54eb2bd4b2a48801c478d890278acdc7693980e9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

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

Log Message:
-----------
[Remora] Add doc about variable name spaces.

Based on the recent clarifications with the team on Element.


Commit: 76abf7af4249a61d8f91acd8c9d58c585802873e
https://github.com/acl2/acl2/commit/76abf7af4249a61d8f91acd8c9d58c585802873e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
A books/kestrel/apt/remove-nesting-tests.lisp
A books/kestrel/apt/remove-nesting.lisp
M books/kestrel/apt/top.lisp

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


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

Changed paths:
A books/kestrel/remora/cert.acl2
A books/kestrel/remora/concrete-syntax-trees.lisp
A books/kestrel/remora/concrete-syntax.lisp
M books/kestrel/remora/grammar.lisp
M books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/parse-directory-files.lisp
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
A books/kestrel/remora/parsing-and-printing.acl2
A books/kestrel/remora/parsing-and-printing.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/top.lisp

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


Commit: 230fbb8a16495b5062ac664dc7cc3873557283f3
https://github.com/acl2/acl2/commit/230fbb8a16495b5062ac664dc7cc3873557283f3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

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

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


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

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

Log Message:
-----------
[Remora] Simplify model of values.

Fold atom values into (array) values.


Commit: 668c9596429db1514def3deee9a9d8e1eb67a255
https://github.com/acl2/acl2/commit/668c9596429db1514def3deee9a9d8e1eb67a255
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
A books/kestrel/fty/nat-list-list.lisp
M books/kestrel/fty/top.lisp

Log Message:
-----------
[FTY] Add fixtype for lists of lists of naturals.

This includes `[books]/kestrel/typed-lists-light/nat-list-listp.lisp` to avoid
conflicts.


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

Changed paths:
A books/kestrel/fty/nat-list-list-result.lisp
M books/kestrel/fty/top.lisp

Log Message:
-----------
[FTY] Add result fixtype of lists of lists of naturals.


Commit: 7c513a116fcdf1b3469548e8c165c0c7645c8787
https://github.com/acl2/acl2/commit/7c513a116fcdf1b3469548e8c165c0c7645c8787
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-structural-operations.lisp
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Move a function to more general place.


Commit: 0f2ed8b98e3876baa85278a8b196fbd397c42476
https://github.com/acl2/acl2/commit/0f2ed8b98e3876baa85278a8b196fbd397c42476
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

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

Log Message:
-----------
[Remora] Fix field name and improve some doc.


Commit: 139b9430e1a8f5c81cb732703d34311450444dbc
https://github.com/acl2/acl2/commit/139b9430e1a8f5c81cb732703d34311450444dbc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/kestrel/remora/package.lsp

Log Message:
-----------
[Remora] Import two symbols.


Commit: 1dad158476fe560067a8187aaafa9b0b3e722f72
https://github.com/acl2/acl2/commit/1dad158476fe560067a8187aaafa9b0b3e722f72
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

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

Log Message:
-----------
[Remora] Add checkers of dimension constraints on values.


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

Changed paths:
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp

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


Compare: https://github.com/acl2/acl2/compare/1adfe8a04d89...e5038e8ab07b

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