[acl2/acl2] 4d3b0b: [Remora] Add some AST fixtypes.

[Alessandro Coglio]

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

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

Log Message:
-----------
[Remora] Add some AST fixtypes.


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

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

Log Message:
-----------
[Remora] Add some structural AST ops.


Commit: 9931067c0d66e9a9e44196d4710df5868a2ca95f
https://github.com/acl2/acl2/commit/9931067c0d66e9a9e44196d4710df5868a2ca95f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

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

Log Message:
-----------
[Remora] Add desugaring of string literals.


Commit: be2632595f27915dfcbfd290c3fe0abfb06630df
https://github.com/acl2/acl2/commit/be2632595f27915dfcbfd290c3fe0abfb06630df
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 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/desugaring.lisp

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


Commit: 527887248738ee9a18a5038be2a1e4e84fa69fd2
https://github.com/acl2/acl2/commit/527887248738ee9a18a5038be2a1e4e84fa69fd2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/java/aij/top.lisp
M books/kestrel/java/atj/aij-notions.lisp
M books/kestrel/java/atj/array-write-method-names.lisp
M books/kestrel/java/atj/atj.lisp
M books/kestrel/java/atj/code-generation.lisp
M books/kestrel/java/atj/common-code-generation.lisp
M books/kestrel/java/atj/deep-code-generation.lisp
M books/kestrel/java/atj/doc.lisp
M books/kestrel/java/atj/input-processing.lisp
M books/kestrel/java/atj/java-abstract-syntax.lisp
M books/kestrel/java/atj/java-input-types.lisp
M books/kestrel/java/atj/java-pretty-printer.lisp
M books/kestrel/java/atj/java-primitive-array-model.lisp
M books/kestrel/java/atj/java-primitive-arrays.lisp
M books/kestrel/java/atj/java-primitives.lisp
M books/kestrel/java/atj/java-syntax-operations.lisp
M books/kestrel/java/atj/name-translation.lisp
M books/kestrel/java/atj/post-translation/cache-const-methods.lisp
M books/kestrel/java/atj/post-translation/fold-returns.lisp
M books/kestrel/java/atj/post-translation/lift-loop-tests.lisp
M books/kestrel/java/atj/post-translation/remove-array-write-calls.lisp
M books/kestrel/java/atj/post-translation/remove-continue.lisp
M books/kestrel/java/atj/post-translation/simplify-conds.lisp
M books/kestrel/java/atj/post-translation/tailrec-elimination.lisp
M books/kestrel/java/atj/post-translation/top.lisp
M books/kestrel/java/atj/pre-translation/array-analysis.lisp
M books/kestrel/java/atj/pre-translation/conjunctions.lisp
M books/kestrel/java/atj/pre-translation/disjunctions.lisp
M books/kestrel/java/atj/pre-translation/multiple-values.lisp
M books/kestrel/java/atj/pre-translation/no-aij-types-analysis.lisp
M books/kestrel/java/atj/pre-translation/remove-dead-if-branches.lisp
M books/kestrel/java/atj/pre-translation/remove-return-last.lisp
M books/kestrel/java/atj/pre-translation/top.lisp
M books/kestrel/java/atj/pre-translation/trivial-vars.lisp
M books/kestrel/java/atj/pre-translation/type-annotation.lisp
M books/kestrel/java/atj/pre-translation/unused-vars.lisp
M books/kestrel/java/atj/pre-translation/var-renaming.lisp
M books/kestrel/java/atj/pre-translation/var-reuse.lisp
M books/kestrel/java/atj/shallow-code-generation.lisp
M books/kestrel/java/atj/shallow-quoted-constant-generation.lisp
M books/kestrel/java/atj/test-structures.lisp
M books/kestrel/java/atj/tests/abnf.lisp
M books/kestrel/java/atj/tests/acl2-times.lisp
M books/kestrel/java/atj/tests/booleans.lisp
M books/kestrel/java/atj/tests/cache-const-methods.lisp
M books/kestrel/java/atj/tests/factorial.lisp
M books/kestrel/java/atj/tests/fibonacci.lisp
M books/kestrel/java/atj/tests/hard-error.lisp
M books/kestrel/java/atj/tests/multivalue.lisp
M books/kestrel/java/atj/tests/natives.lisp
M books/kestrel/java/atj/tests/no-aij-types.lisp
M books/kestrel/java/atj/tests/packages.lisp
M books/kestrel/java/atj/tests/primarrays.lisp
M books/kestrel/java/atj/tests/primitives.lisp
M books/kestrel/java/atj/top.lisp
M books/kestrel/java/atj/tutorial.lisp
M books/kestrel/java/atj/type-macros.lisp
M books/kestrel/java/atj/types-for-built-ins.lisp
M books/kestrel/java/atj/types-for-bv-fns.lisp
M books/kestrel/java/atj/types-for-ihs-fns.lisp
M books/kestrel/java/atj/types-for-list-fns.lisp
M books/kestrel/java/atj/types-for-natives.lisp
M books/kestrel/java/atj/types-for-std-fns.lisp
M books/kestrel/java/atj/types.lisp
M books/kestrel/java/language/binary-digits-validation.lisp
M books/kestrel/java/language/binary-integer-literals.lisp
M books/kestrel/java/language/boolean-literals-validation.lisp
M books/kestrel/java/language/boolean-literals.lisp
M books/kestrel/java/language/decimal-digits-validation.lisp
M books/kestrel/java/language/decimal-integer-literals.lisp
M books/kestrel/java/language/escape-sequences.lisp
M books/kestrel/java/language/floating-point-placeholders.lisp
M books/kestrel/java/language/floating-point-value-set-parameters.lisp
M books/kestrel/java/language/grammar.lisp
M books/kestrel/java/language/hexadecimal-digits-validation.lisp
M books/kestrel/java/language/hexadecimal-integer-literals.lisp
M books/kestrel/java/language/integer-literals.lisp
M books/kestrel/java/language/keywords-validation.lisp
M books/kestrel/java/language/literals.lisp
M books/kestrel/java/language/null-literal-validation.lisp
M books/kestrel/java/language/null-literal.lisp
M books/kestrel/java/language/octal-digits-validation.lisp
M books/kestrel/java/language/octal-integer-literals.lisp
M books/kestrel/java/language/optional-integer-type-suffix.lisp
M books/kestrel/java/language/package-names.lisp
M books/kestrel/java/language/pointers.lisp
M books/kestrel/java/language/primitive-conversions.lisp
M books/kestrel/java/language/primitive-function-macros.lisp
M books/kestrel/java/language/primitive-operations.lisp
M books/kestrel/java/language/primitive-types.lisp
M books/kestrel/java/language/primitive-values.lisp
M books/kestrel/java/language/reference-types.lisp
M books/kestrel/java/language/reference-values.lisp
M books/kestrel/java/language/semantics.lisp
M books/kestrel/java/language/syntax.lisp
M books/kestrel/java/language/top.lisp
M books/kestrel/java/language/types.lisp
M books/kestrel/java/language/unicode-characters.lisp
M books/kestrel/java/language/unicode-escapes.lisp
M books/kestrel/java/language/unicode-input-characters.lisp
M books/kestrel/java/language/values.lisp
M books/kestrel/java/portcullis.lisp

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


Commit: 49b581c97b3df9f80af74135b5943abf72f3f2fe
https://github.com/acl2/acl2/commit/49b581c97b3df9f80af74135b5943abf72f3f2fe
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

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

Log Message:
-----------
[Remora] Add desugaring of combined application.


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

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

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


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

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

Log Message:
-----------
[Remora] Add two nested list fixtypes.


Commit: 10d24fa210c3f696665266d49511a8c3406e49ae
https://github.com/acl2/acl2/commit/10d24fa210c3f696665266d49511a8c3406e49ae
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

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

Log Message:
-----------
[Remora] Add some structural AST ops.


Commit: 6f477b3dbd497f7d2f3e692237b7f8ffb291237c
https://github.com/acl2/acl2/commit/6f477b3dbd497f7d2f3e692237b7f8ffb291237c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

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

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


Commit: 09ca324b656a1a33751116e7a5e4a57a70ff84c3
https://github.com/acl2/acl2/commit/09ca324b656a1a33751116e7a5e4a57a70ff84c3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Consistently use tt font for `let`.


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

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

Log Message:
-----------
[Remora] Extend desugaring.

Add desugaring of bracket expressions.

Expand doc to compare with Haskell implementation.


Commit: 58baad5154a396642346622815af637cdc817aea
https://github.com/acl2/acl2/commit/58baad5154a396642346622815af637cdc817aea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Remove stray annotaation.


Commit: 9428d940aacd3eab3132cd623c575ad0c726983f
https://github.com/acl2/acl2/commit/9428d940aacd3eab3132cd623c575ad0c726983f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Finish desugaring.

Include `let` in the core for now, for the (slightly tricky) reasons described
in the added documentation.


Commit: 39e9a79fcad231c8069c0a2ba297b98ea072ab91
https://github.com/acl2/acl2/commit/39e9a79fcad231c8069c0a2ba297b98ea072ab91
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

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


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

Changed paths:
M books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/frame-flattening.lisp

Log Message:
-----------
[Remora] Add frame flattening transformation.


Commit: 5506801f00b70b77d1e98bb023b524ed890964a7
https://github.com/acl2/acl2/commit/5506801f00b70b77d1e98bb023b524ed890964a7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
A books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parse-directory-files.lisp
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/syntax-abstraction.lisp

Log Message:
-----------
Merge and resolve conflicts.


Commit: 8be8fc0ff3fd78c166fff320b0d72a0e47b0c146
https://github.com/acl2/acl2/commit/8be8fc0ff3fd78c166fff320b0d72a0e47b0c146
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Prove more properties of desugaring.


Commit: 90180c157d21a6e2a169695f456e1b9c728741de
https://github.com/acl2/acl2/commit/90180c157d21a6e2a169695f456e1b9c728741de
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

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


Commit: 15e46589b6b5db314d9358b596bb35b188f2d094
https://github.com/acl2/acl2/commit/15e46589b6b5db314d9358b596bb35b188f2d094
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Add more properties of desugaring.


Commit: 9dba0c50cbb8d0b911df554c9eb8151dbf998cf4
https://github.com/acl2/acl2/commit/9dba0c50cbb8d0b911df554c9eb8151dbf998cf4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:

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


Commit: 4037bc2a7439e9597486bf79dbcb27501d9d429b
https://github.com/acl2/acl2/commit/4037bc2a7439e9597486bf79dbcb27501d9d429b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Generate more core-AST-checking predicates.


Commit: 6eb939ea6d0a847ea7141fc6a5fd77992636877c
https://github.com/acl2/acl2/commit/6eb939ea6d0a847ea7141fc6a5fd77992636877c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Add theorems about structural ops.


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

Changed paths:
M books/kestrel/remora/frame-flattening.lisp

Log Message:
-----------
[Remora] Prove core preservation of frame flattening.


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

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

Log Message:
-----------
[Remora] Fix XDOC link.


Commit: 91a4d57bf07a1b3c8139d053e309ffd8aa4ccf37
https://github.com/acl2/acl2/commit/91a4d57bf07a1b3c8139d053e309ffd8aa4ccf37
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:

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


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

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

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


Commit: 8f7559950fa2c2a0d7469059ed2f1eb837b14946
https://github.com/acl2/acl2/commit/8f7559950fa2c2a0d7469059ed2f1eb837b14946
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-gso.lisp
A books/kestrel/c/transformation/tests/split-gso/implicit-initer.c
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
A books/kestrel/c/transformation/tests/split-gso/unnamed-members.c
M books/kestrel/c/transformation/utilities/subst-free.lisp

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


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

Changed paths:
M books/kestrel/remora/parse-directory-files.lisp
A books/kestrel/remora/printer.lisp
M books/kestrel/remora/top.lisp

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


Compare: https://github.com/acl2/acl2/compare/12bf5dc307e9...ec50a736224e

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