[acl2/acl2] 28a9bc: [Remora] Add type substitution with auto-alpha-ren...
0 views
Skip to first unread message
Alessandro Coglio
Jun 25, 2026, 1:38:32 AM (yesterday) Jun 25
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 28a9bcc5c19d10cc727e0e4461311b3875bf4062
https://github.com/acl2/acl2/commit/28a9bcc5c19d10cc727e0e4461311b3875bf4062
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add type substitution with auto-alpha-rename.
This is an initial version. It has an avoid set (which could be set to nil at
the top level), which is not ideal.
We also add a helper, and a couple of supporting theorems.
Commit: 4ff0cee3410036af4b6deb2e7364654298d5d22d
https://github.com/acl2/acl2/commit/4ff0cee3410036af4b6deb2e7364654298d5d22d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add some important doc.
Commit: a50d1472c7434dfe8708dba7e2cced19dfd20c86
https://github.com/acl2/acl2/commit/a50d1472c7434dfe8708dba7e2cced19dfd20c86
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Tweak some doc.
Commit: d283f4ab550c93c51f5e352feaee32459303f003
https://github.com/acl2/acl2/commit/d283f4ab550c93c51f5e352feaee32459303f003
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add wrappers for type auto-alpha substitutions.
The `deffold-map` functions are now auxiliary ones, because of the extra avoid
set input. We provide wrappers that only take the AST and the substitution,
initializing the avoid set to empty.
Commit: fff5dd352ad7372e195defc59ee6d0022c5ed803
https://github.com/acl2/acl2/commit/fff5dd352ad7372e195defc59ee6d0022c5ed803
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add auto-alpha-renaming ispace substitution ops.
Commit: e6ec4b8a1887fc8671b2c67aa535ddedbdb48ba3
https://github.com/acl2/acl2/commit/e6ec4b8a1887fc8671b2c67aa535ddedbdb48ba3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/bound-and-free-variable-operations.lisp
Log Message:
-----------
[Remora] Add an operation about bound variables.
Commit: 491437fe2af91b421ec7455c933b768ed5c63cb6
https://github.com/acl2/acl2/commit/491437fe2af91b421ec7455c933b768ed5c63cb6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add more auto-alpha-rename operations.
These are for substitutions of expression variables.
Commit: cb0c09ae2d2deb753f64c46a3703bc5fa4cbf76d
https://github.com/acl2/acl2/commit/cb0c09ae2d2deb753f64c46a3703bc5fa4cbf76d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Update some doc.
Commit: 9c677a3b87b81c91e40d39bcf95259f771316cf4
https://github.com/acl2/acl2/commit/9c677a3b87b81c91e40d39bcf95259f771316cf4
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-doc.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
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/type-checking.lisp
M books/kestrel/remora/values.lisp
Log Message:
-----------
Merge.
Commit: dbd7fbae7ad6fb8a1388db045dfb1895ac3bb66c
https://github.com/acl2/acl2/commit/dbd7fbae7ad6fb8a1388db045dfb1895ac3bb66c
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] Improve type checker.
Auto-alpha-rename variables, instead of returning an error when there may be a
variable capture.
Commit: afda80b07f8fe1caddffe29067220b8fe779c425
https://github.com/acl2/acl2/commit/afda80b07f8fe1caddffe29067220b8fe779c425
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Expand some doc.
Commit: 51c08081642ef77ce52c413c145e84481a90430e
https://github.com/acl2/acl2/commit/51c08081642ef77ce52c413c145e84481a90430e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Move op to more general place.
Commit: ece1f0a84f57e18401c945b8e0ecc39754f5c00c
https://github.com/acl2/acl2/commit/ece1f0a84f57e18401c945b8e0ecc39754f5c00c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/fty/string-string-map.lisp
Log Message:
-----------
[FTY] Add a theorem.
Commit: 6db009170e13de276d82dda047443df03dc4d61d
https://github.com/acl2/acl2/commit/6db009170e13de276d82dda047443df03dc4d61d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
Log Message:
-----------
[Remora] Add some AST ops.
Commit: 93f41349a8ea71d745bcc0b3c1b73ae47c44fac4
https://github.com/acl2/acl2/commit/93f41349a8ea71d745bcc0b3c1b73ae47c44fac4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Shorten some doc.
Commit: ce3bccf25a911b4d6b328fb6c400dcda59f0541a
https://github.com/acl2/acl2/commit/ce3bccf25a911b4d6b328fb6c400dcda59f0541a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Improve two function names.
Commit: 18df5f29aaa9391325663eccf4104d8a97806e06
https://github.com/acl2/acl2/commit/18df5f29aaa9391325663eccf4104d8a97806e06
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Improve file layout.
Commit: 986f8db1cc08a69770f1439cd60692da0206ede9
https://github.com/acl2/acl2/commit/986f8db1cc08a69770f1439cd60692da0206ede9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/variable-renaming-alpha-operations.lisp
Log Message:
-----------
[Remora] Add capture-avoiding renaming ops.
Commit: 6ee3a7889b6d8c3d2b993d8bd76d34e54ed35fd7
https://github.com/acl2/acl2/commit/6ee3a7889b6d8c3d2b993d8bd76d34e54ed35fd7
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] Improve type checker.
Use capture-avoiding renaming.
Commit: 07a1e9e4cc50afa3eff67ebb0ba905e0f405bc06
https://github.com/acl2/acl2/commit/07a1e9e4cc50afa3eff67ebb0ba905e0f405bc06
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
Log Message:
-----------
[Remora] Update two XDOC links.
Compare: https://github.com/acl2/acl2/compare/5d3fdd60a65c...07a1e9e4cc50
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 28a9bcc5c19d10cc727e0e4461311b3875bf4062
https://github.com/acl2/acl2/commit/28a9bcc5c19d10cc727e0e4461311b3875bf4062
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add type substitution with auto-alpha-rename.
This is an initial version. It has an avoid set (which could be set to nil at
the top level), which is not ideal.
We also add a helper, and a couple of supporting theorems.
Commit: 4ff0cee3410036af4b6deb2e7364654298d5d22d
https://github.com/acl2/acl2/commit/4ff0cee3410036af4b6deb2e7364654298d5d22d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add some important doc.
Commit: a50d1472c7434dfe8708dba7e2cced19dfd20c86
https://github.com/acl2/acl2/commit/a50d1472c7434dfe8708dba7e2cced19dfd20c86
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Tweak some doc.
Commit: d283f4ab550c93c51f5e352feaee32459303f003
https://github.com/acl2/acl2/commit/d283f4ab550c93c51f5e352feaee32459303f003
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add wrappers for type auto-alpha substitutions.
The `deffold-map` functions are now auxiliary ones, because of the extra avoid
set input. We provide wrappers that only take the AST and the substitution,
initializing the avoid set to empty.
Commit: fff5dd352ad7372e195defc59ee6d0022c5ed803
https://github.com/acl2/acl2/commit/fff5dd352ad7372e195defc59ee6d0022c5ed803
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add auto-alpha-renaming ispace substitution ops.
Commit: e6ec4b8a1887fc8671b2c67aa535ddedbdb48ba3
https://github.com/acl2/acl2/commit/e6ec4b8a1887fc8671b2c67aa535ddedbdb48ba3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/bound-and-free-variable-operations.lisp
Log Message:
-----------
[Remora] Add an operation about bound variables.
Commit: 491437fe2af91b421ec7455c933b768ed5c63cb6
https://github.com/acl2/acl2/commit/491437fe2af91b421ec7455c933b768ed5c63cb6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add more auto-alpha-rename operations.
These are for substitutions of expression variables.
Commit: cb0c09ae2d2deb753f64c46a3703bc5fa4cbf76d
https://github.com/acl2/acl2/commit/cb0c09ae2d2deb753f64c46a3703bc5fa4cbf76d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Update some doc.
Commit: 9c677a3b87b81c91e40d39bcf95259f771316cf4
https://github.com/acl2/acl2/commit/9c677a3b87b81c91e40d39bcf95259f771316cf4
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-doc.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
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/type-checking.lisp
M books/kestrel/remora/values.lisp
Log Message:
-----------
Merge.
Commit: dbd7fbae7ad6fb8a1388db045dfb1895ac3bb66c
https://github.com/acl2/acl2/commit/dbd7fbae7ad6fb8a1388db045dfb1895ac3bb66c
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] Improve type checker.
Auto-alpha-rename variables, instead of returning an error when there may be a
variable capture.
Commit: afda80b07f8fe1caddffe29067220b8fe779c425
https://github.com/acl2/acl2/commit/afda80b07f8fe1caddffe29067220b8fe779c425
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Expand some doc.
Commit: 51c08081642ef77ce52c413c145e84481a90430e
https://github.com/acl2/acl2/commit/51c08081642ef77ce52c413c145e84481a90430e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Move op to more general place.
Commit: ece1f0a84f57e18401c945b8e0ecc39754f5c00c
https://github.com/acl2/acl2/commit/ece1f0a84f57e18401c945b8e0ecc39754f5c00c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/fty/string-string-map.lisp
Log Message:
-----------
[FTY] Add a theorem.
Commit: 6db009170e13de276d82dda047443df03dc4d61d
https://github.com/acl2/acl2/commit/6db009170e13de276d82dda047443df03dc4d61d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
Log Message:
-----------
[Remora] Add some AST ops.
Commit: 93f41349a8ea71d745bcc0b3c1b73ae47c44fac4
https://github.com/acl2/acl2/commit/93f41349a8ea71d745bcc0b3c1b73ae47c44fac4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Shorten some doc.
Commit: ce3bccf25a911b4d6b328fb6c400dcda59f0541a
https://github.com/acl2/acl2/commit/ce3bccf25a911b4d6b328fb6c400dcda59f0541a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Improve two function names.
Commit: 18df5f29aaa9391325663eccf4104d8a97806e06
https://github.com/acl2/acl2/commit/18df5f29aaa9391325663eccf4104d8a97806e06
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Improve file layout.
Commit: 986f8db1cc08a69770f1439cd60692da0206ede9
https://github.com/acl2/acl2/commit/986f8db1cc08a69770f1439cd60692da0206ede9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/variable-renaming-alpha-operations.lisp
Log Message:
-----------
[Remora] Add capture-avoiding renaming ops.
Commit: 6ee3a7889b6d8c3d2b993d8bd76d34e54ed35fd7
https://github.com/acl2/acl2/commit/6ee3a7889b6d8c3d2b993d8bd76d34e54ed35fd7
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] Improve type checker.
Use capture-avoiding renaming.
Commit: 07a1e9e4cc50afa3eff67ebb0ba905e0f405bc06
https://github.com/acl2/acl2/commit/07a1e9e4cc50afa3eff67ebb0ba905e0f405bc06
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
Log Message:
-----------
[Remora] Update two XDOC links.
Compare: https://github.com/acl2/acl2/compare/5d3fdd60a65c...07a1e9e4cc50
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Jun 25, 2026, 2:57:18 AM (yesterday) Jun 25
to acl2-...@googlegroups.com
Branch: refs/heads/master
Alessandro Coglio
Jun 25, 2026, 2:57:34 AM (yesterday) Jun 25
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Reply all
Reply to author
Forward
0 new messages