[acl2/acl2] 51f75b: [Remora] Add some derived AST fixtypes.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 51f75b96ed7b2067d41b8eebe49e88eaffd83ef4
https://github.com/acl2/acl2/commit/51f75b96ed7b2067d41b8eebe49e88eaffd83ef4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

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


Commit: 3ea1f7b96252f0752af4295f9197c4e0e5c617e4
https://github.com/acl2/acl2/commit/3ea1f7b96252f0752af4295f9197c4e0e5c617e4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Advance type checking.

Add code to match argument type indices to input type indices.


Commit: c660caa9e6ff7d5a34b9be2c1371242e0ba5c2f7
https://github.com/acl2/acl2/commit/c660caa9e6ff7d5a34b9be2c1371242e0ba5c2f7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Finish type checking of term application.

Define the join operation on indices and complete the type checking of term
application.


Commit: 8849b39065a551b12e22cdac59d5877a7627ae59
https://github.com/acl2/acl2/commit/8849b39065a551b12e22cdac59d5877a7627ae59
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

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


Commit: 3d01a6d5c6b633ec9cf1498afcc1a30e6ecc3d77
https://github.com/acl2/acl2/commit/3d01a6d5c6b633ec9cf1498afcc1a30e6ecc3d77
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Add an AST matching operation.


Commit: 2363428a517126f342b2aaa57557d7ec98a97792
https://github.com/acl2/acl2/commit/2363428a517126f342b2aaa57557d7ec98a97792
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Add an AST structural operation.


Commit: 5e925aad90f4d3f0a70b52e67019d337629ac118
https://github.com/acl2/acl2/commit/5e925aad90f4d3f0a70b52e67019d337629ac118
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Start type checking of type applications.


Commit: 290e66666a548f5433df42fedd4e036fc0dd695b
https://github.com/acl2/acl2/commit/290e66666a548f5433df42fedd4e036fc0dd695b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Rename some fixtypes and functions.

Make the fixtype more general, as it is going to be used more generally.


Commit: 1f391e9f7fd59e1c18113fd0de8f968970b92f8b
https://github.com/acl2/acl2/commit/1f391e9f7fd59e1c18113fd0de8f968970b92f8b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Improve some variable names.


Commit: 847acf5cf6703ea44c3d690725fdfe11d70ae6e2
https://github.com/acl2/acl2/commit/847acf5cf6703ea44c3d690725fdfe11d70ae6e2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Move some fixtype definitions.


Commit: f1f39cc3f5462a2050f9963c54d73e7d9b3267a7
https://github.com/acl2/acl2/commit/f1f39cc3f5462a2050f9963c54d73e7d9b3267a7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

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


Commit: 497b6defb75ea141b73f691eb4a3a021f0f434c2
https://github.com/acl2/acl2/commit/497b6defb75ea141b73f691eb4a3a021f0f434c2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Add some AST substitution operations.


Commit: 754750b3480ed8b16c12599a7035d9e7586b2990
https://github.com/acl2/acl2/commit/754750b3480ed8b16c12599a7035d9e7586b2990
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

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


Commit: c523c91e61b9744fa078b541f24ced6ca59e9630
https://github.com/acl2/acl2/commit/c523c91e61b9744fa078b541f24ced6ca59e9630
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Finish type checking of type application.


Commit: 453d01487cea13d34392505850b8d82d11089e93
https://github.com/acl2/acl2/commit/453d01487cea13d34392505850b8d82d11089e93
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Add more derived AST fixtypes and theorems.


Commit: a22162242a7d72c2421a36e6c3fdb8c587c10f7e
https://github.com/acl2/acl2/commit/a22162242a7d72c2421a36e6c3fdb8c587c10f7e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Add two AST matching operations.


Commit: 290d52939ff21a4e6d34e3013274ec3e8e6ff79e
https://github.com/acl2/acl2/commit/290d52939ff21a4e6d34e3013274ec3e8e6ff79e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Add two AST structural operations.


Commit: 8a890fc60ac3be28542192a51fd4f4abff4cf9f4
https://github.com/acl2/acl2/commit/8a890fc60ac3be28542192a51fd4f4abff4cf9f4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

Log Message:
-----------
[Remora] Add type checking of index applications.


Commit: 99388bd01e7aa5e1f93c9087688c540a7b28eae7
https://github.com/acl2/acl2/commit/99388bd01e7aa5e1f93c9087688c540a7b28eae7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-16 (Thu, 16 Apr 2026)

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

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


Compare: https://github.com/acl2/acl2/compare/42e11f6a0e3d...99388bd01e7a

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

[Alessandro Coglio]

Branch: refs/heads/testing