[acl2/acl2] ddfeeb: [Remora] Add an operation on types.

[Alessandro Coglio]

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

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

Log Message:
-----------
[Remora] Add an operation on types.

This will be used to fix some issues in the type checker.


Commit: 411e552f98234468174c45ed4a33c90e9d09e93a
https://github.com/acl2/acl2/commit/411e552f98234468174c45ed4a33c90e9d09e93a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

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

Log Message:
-----------
[Remora] Relax `let` type annotation checks.

While the expression type is always an array type, the annotating type may be an
atom type, which we must thus auto-lift to an array type before we compare the
two types for equivalence.

Thanks to Quan Luu for running the type checker on an example that exposed this
bug.


Commit: f7bcb8e01dfe69bb457654f60af5a6b62fea1fb7
https://github.com/acl2/acl2/commit/f7bcb8e01dfe69bb457654f60af5a6b62fea1fb7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

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

Log Message:
-----------
[Remora] Enforce a static invariant.

Ensure that all the types associated to variables in the static environment have
array types.

Thanks to Quan Luu for running the type checker on an example that exposed the
need for this enforcement.


Commit: 6daae0d51648499365d02b2b55d85d3554a25ece
https://github.com/acl2/acl2/commit/6daae0d51648499365d02b2b55d85d3554a25ece
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

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

Log Message:
-----------
[Remora] Move two functions to better place.


Commit: fafbbb8699d1330b9f3504b73bf482542c500480
https://github.com/acl2/acl2/commit/fafbbb8699d1330b9f3504b73bf482542c500480
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-02 (Thu, 02 Jul 2026)

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

Log Message:
-----------
[Remora] Relax array type matching.

The relaxation is twofold: we regard atom types as scalar array types, and we
handle bracket array types. The first is motivated by the fact that the ASTs
allow atom types where array types are expected; without this relaxation, some
checks were unjustly failing. The second relaxation is just a forgotten case:
bracket syntax is just an alternative to explicit array type syntax.

Thanks to Quan Luu for running type checker on some examples that exposed both
bugs.


Compare: https://github.com/acl2/acl2/compare/f46ff5520c09...fafbbb8699d1

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