[acl2/acl2] b5e393: [Remora] Add theorems.

[Alessandro Coglio]

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

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

Log Message:
-----------
[Remora] Add theorems.


Commit: 26b8e55d16a6d716e27a878309fcb975f34e3040
https://github.com/acl2/acl2/commit/26b8e55d16a6d716e27a878309fcb975f34e3040
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser.lisp

Log Message:
-----------
[cpp-syntax] Speed up a file.


Commit: d17801e14737b52c6488947551977425d5903995
https://github.com/acl2/acl2/commit/d17801e14737b52c6488947551977425d5903995
Author: Mihir Mehta <mi...@cs.utexas.edu>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser.lisp

Log Message:
-----------
Merge pull request #1955 from acl2/cpp-speedups

[cpp-syntax] Speed up a file.


Commit: 8c2a205f1091b758ad1764e488a4b54902673462
https://github.com/acl2/acl2/commit/8c2a205f1091b758ad1764e488a4b54902673462
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validation-tables.lisp
M books/kestrel/c/syntax/validator.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/tests/struct-type-split/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/typedef-chain.c
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
Merge commit '568df750b73e6ad6c9e802e684ab79753e1389a0' into HEAD


Commit: 2fb6a50f835e33f0116718b5680f958e19de7e3f
https://github.com/acl2/acl2/commit/2fb6a50f835e33f0116718b5680f958e19de7e3f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

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

Log Message:
-----------
[Remora] Add a list operation.


Commit: 56bd9fe74b1835781ae91631e31d57f8636cf59e
https://github.com/acl2/acl2/commit/56bd9fe74b1835781ae91631e31d57f8636cf59e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

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

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


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

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

Log Message:
-----------
[Remora] add a structural op and theorem.


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

Changed paths:
M books/kestrel/remora/ispace-equivalence.lisp

Log Message:
-----------
[Remora] Slightly change ispace normalization.

Instead of normalizing to the `:dim` summand of `shape`, normalize to singleton
lists in the `:dims` summand of `shape`, because `:dim` will be removed.


Commit: 0c36eb5d7288cd261e17abb785c2624896858135
https://github.com/acl2/acl2/commit/0c36eb5d7288cd261e17abb785c2624896858135
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 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] Slightly change core and desugaring.

Avoid the `:dim` summand of `shape` in favor of `:dims` with singleton lists.
The `:dim` summand will be eliminated.


Commit: 494204ea609e352a9d8d66dbb162f7f143f298a7
https://github.com/acl2/acl2/commit/494204ea609e352a9d8d66dbb162f7f143f298a7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp

Log Message:
-----------
[Remora] Join shape and ispaces into AST clique.

This does not change the definitions, but puts shape and ispace ASTs under the
same `fty::deftypes` clique, as a preliminary step towards making them actually
mutually recursive.

We adapt what's needed, particularly calls of `deffold-...`.


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

Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp

Log Message:
-----------
[Remora] Improve type splice ASTs.

Use ispaces instead of shapes, in preparation for the elimination of dimensions
auto-lifted to shapes.

A number of things had to be adapted to this change.


Commit: 5012d0bdb316eaa6dd4f02dc37fa0b3e2eaffa53
https://github.com/acl2/acl2/commit/5012d0bdb316eaa6dd4f02dc37fa0b3e2eaffa53
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

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

Log Message:
-----------
[Remora] Improve some naming and nomenclature.

Use 'expression value' for the values that expressions evaluate to, which is
symmetric with 'type value' and 'ispace value'.


Commit: 9125a39f1856542bdae867e808ce8c30ae4285ca
https://github.com/acl2/acl2/commit/9125a39f1856542bdae867e808ce8c30ae4285ca
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validation-tables.lisp
M books/kestrel/c/syntax/validator.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/tests/struct-type-split/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/typedef-chain.c
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser.lisp

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


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

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

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


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

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

Log Message:
-----------
[Remora] Reorder some code.


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

Changed paths:
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/dynamic-semantics.lisp
R books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/type-value-equivalence.lisp
A books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Rename a file and topic.


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

Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/type-value-equivalence.lisp
M books/kestrel/remora/values.lisp

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


Commit: 052c23397d89243ebeda08a11638775541f24ae4
https://github.com/acl2/acl2/commit/052c23397d89243ebeda08a11638775541f24ae4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

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

Log Message:
-----------
[Remora] Add an op on ispace values.


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

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

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


Commit: 729ab0623a19dfea3b4ba789020c56bf611218b6
https://github.com/acl2/acl2/commit/729ab0623a19dfea3b4ba789020c56bf611218b6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/ispace-equivalence.lisp

Log Message:
-----------
[Remora] Improve ispace equivalence.

Add operations for actual ispace, vs. just shape, equivalence.

Add some theorems.


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

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
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/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.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/type-equivalence.lisp

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

Use ispaces in array types.


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

Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/ispace-equivalence.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/type-equivalence.lisp
M books/kestrel/remora/values.lisp

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

Use ispaces instead of shapes in bracket types.


Commit: 1786593535ed1044e808ef24bf5e45b0955f82e4
https://github.com/acl2/acl2/commit/1786593535ed1044e808ef24bf5e45b0955f82e4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

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

Log Message:
-----------
[Remora] Remove function no longer needed.


Compare: https://github.com/acl2/acl2/compare/568df750b73e...1786593535ed

To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[Alessandro Coglio]

Branch: refs/heads/master

Home: https://github.com/acl2/acl2
Commit: b5e393a24c9d6e3e91c1c21fced9c42767887458
https://github.com/acl2/acl2/commit/b5e393a24c9d6e3e91c1c21fced9c42767887458
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

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

Log Message:
-----------
[Remora] Add theorems.

Compare: https://github.com/acl2/acl2/compare/8c2a205f1091...1786593535ed

[Alessandro Coglio]

Branch: refs/heads/testing