[acl2/acl2] e9fff0: [C$] Promote function to top-level.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: e9fff0e868e02c98ef748b85c255b1fc558b1b47
https://github.com/acl2/acl2/commit/e9fff0e868e02c98ef748b85c255b1fc558b1b47
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Promote function to top-level.


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

Changed paths:
M books/kestrel/c/syntax/grammar/encoding-prefixes.abnf

Log Message:
-----------
[C$] Improve some doc.


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

Changed paths:
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
A books/kestrel/c/syntax/grammar/identifier-lists.abnf

Log Message:
-----------
[C$] Factor a grammar rule.


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

Changed paths:
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Improve some variable names.


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

Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp

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


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

Changed paths:
M books/kestrel/c/syntax/unambiguity.lisp

Log Message:
-----------
[C$] Add a theorem.


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

Changed paths:
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Change recursion structure.

This is in preparation for extensions for modular validation.


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

Changed paths:
M books/kestrel/fty/deffold-reduce-doc.lisp
M books/kestrel/fty/deffold-reduce.lisp

Log Message:
-----------
[FTY] Improve `deffold-reduce`.

Have it generate an additional theorem.


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

Changed paths:
M books/kestrel/c/syntax/unambiguity.lisp

Log Message:
-----------
[C$] Remove theorem now auto-generated.


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

Changed paths:
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives-c17.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives-c23.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives.abnf

Log Message:
-----------
[C$] Modularize and extend some grammar rules.

These are the rules for preprocessing directives.


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

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp

Log Message:
-----------
[C$] Avoid some run-time checks via guards.


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

Changed paths:
M books/kestrel/fty/deffold-reduce-doc.lisp
M books/kestrel/fty/deffold-reduce.lisp

Log Message:
-----------
[FTY] Extend `deffold-redudce`.

Have it generate another theorem.


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

Changed paths:
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Avoid some run-time checks via guards.


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

Changed paths:
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Improve some variable names.


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

Changed paths:
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/encoding-prefixes.abnf
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
A books/kestrel/c/syntax/grammar/identifier-lists.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives-c17.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives-c23.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives.abnf

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


Compare: https://github.com/acl2/acl2/compare/49bba68fde9a...c656640af155

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

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel