[acl2/acl2] 21351d: [C$] Add check to reader.

[Alessandro Coglio]

Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 21351df0b8efda36ca0b58447683326e9237e80e
https://github.com/acl2/acl2/commit/21351df0b8efda36ca0b58447683326e9237e80e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-26 (Tue, 26 May 2026)

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

Log Message:
-----------
[C$] Add check to reader.

Excludes surrogate Unicode code points.


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

Changed paths:
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/reader.lisp
M books/kestrel/c/syntax/unicode-characters.lisp

Log Message:
-----------
[C$] Tighten some types.

This replaces natural numbers with unicode characters in the character-position
pairs in the parser stobj and in the return of the reader.


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/syntax/unicode-characters.lisp
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Tighten a fixtype.

Use the type of Unicode character codes for the code field of a `c-char` AST.


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

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

Log Message:
-----------
[C$] Refine our model of array types.

Add an optional positive integer as size. Extend notions of type compatibility
and composite types accordingtly.

Since this matches the notion of array types in the language formalization, the
formalp predicates and the mapping to the language formalization have been
extended to include array types.

There are intentional TODOs in the validator to try and set the size if
possible. It is currently always set to `nil` (i.e. unknown size), so the
behavior is essentially like before this change. But this change paves the way
for further changes.


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/syntax/unicode-characters.lisp
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Use a tighter fixtype.

Restrict the code field of a `s-char` AST to be a Unicode character code.


Commit: ebed9b5f79a1c59aa57cc9a17429b45dada74701
https://github.com/acl2/acl2/commit/ebed9b5f79a1c59aa57cc9a17429b45dada74701
Author: Alessandro Coglio <2409151...@users.noreply.github.com>
Date: 2026-05-27 (Wed, 27 May 2026)

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

Log Message:
-----------
Merge pull request #1942 from acoglio/mac1

[C$] Refine our model of array types.


Commit: 65b21d706a3b1798b25469885fefa628b24ff97b
https://github.com/acl2/acl2/commit/65b21d706a3b1798b25469885fefa628b24ff97b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-27 (Wed, 27 May 2026)

Changed paths:
M books/kestrel/axe/arm/rule-lists.lisp

Log Message:
-----------
[axe/arm] Add more definition rules to rule-list.


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

Changed paths:
M books/kestrel/c/language/implementation-environments/dialects.lisp

Log Message:
-----------
[C] Remove needless line break.


Commit: 14aa3d42f3d527eaa9a25a882d0f53179155a38c
https://github.com/acl2/acl2/commit/14aa3d42f3d527eaa9a25a882d0f53179155a38c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-27 (Wed, 27 May 2026)

Changed paths:
M books/kestrel/x86/flags.lisp

Log Message:
-----------
[x86] Add constant for standard flags.


Commit: 6ef7e5c716ad13b802829aff8d1ae081bb01012b
https://github.com/acl2/acl2/commit/6ef7e5c716ad13b802829aff8d1ae081bb01012b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-27 (Wed, 27 May 2026)

Changed paths:
M books/kestrel/axe/x86/tests/kestrel/assembly/add.lisp

Log Message:
-----------
[axe/x86] Add another proof to test.

Inspired by something NDSU did.


Commit: ff70cc797e77466a516b00a05c58fe8ec3347eee
https://github.com/acl2/acl2/commit/ff70cc797e77466a516b00a05c58fe8ec3347eee
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-27 (Wed, 27 May 2026)

Changed paths:
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/evaluation.lisp
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
A books/kestrel/c/syntax/grammar/lexemes.abnf
A books/kestrel/c/syntax/grammar/tokens.abnf
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-options.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validator.lisp

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


Commit: 0ac1e8618650cc0792e22dcf7b74b45600ac2f28
https://github.com/acl2/acl2/commit/0ac1e8618650cc0792e22dcf7b74b45600ac2f28
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-27 (Wed, 27 May 2026)

Changed paths:
M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp

Log Message:
-----------
[arm] Add decoding and stub model for supervisor call.


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

Changed paths:
M books/kestrel/c/syntax/grammar.lisp
A books/kestrel/c/syntax/grammar/expressions-ext.abnf
A books/kestrel/c/syntax/grammar/expressions-std.abnf
A books/kestrel/c/syntax/grammar/expressions.abnf
M books/kestrel/c/syntax/grammar/grammar-rest.abnf

Log Message:
-----------
[C$] Start modularizing grammar of expressions.


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/unicode-characters.lisp

Log Message:
-----------
[C$] Tighten a fixtype in ASTs.

Use Unicode character codes instead of natural numbers in `u-char`.


Commit: 27740ff20c1ac5771727c335b9a32df131fa25d6
https://github.com/acl2/acl2/commit/27740ff20c1ac5771727c335b9a32df131fa25d6
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-27 (Wed, 27 May 2026)

Changed paths:
M books/kestrel/axe/arm/package.lsp

Log Message:
-----------
[axe/arm] Add symbols to package.


Commit: f347790b179c71051f4f1cddb42e2a01aa3ff235
https://github.com/acl2/acl2/commit/f347790b179c71051f4f1cddb42e2a01aa3ff235
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-27 (Wed, 27 May 2026)

Changed paths:
M books/kestrel/axe/arm/axe-rules.lisp
M books/kestrel/axe/arm/rule-lists.lisp
A books/kestrel/axe/arm/run-until-return-with-tracing.lisp
M books/kestrel/axe/arm/run-until-return.lisp
M books/kestrel/axe/arm/unroller.lisp

Log Message:
-----------
[axe/arm] Add tracing option to lifter.


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Tighten a fixtype in ASTs.

In `q-char` ASTs, use Unicode character codes instead of just natural numbers.


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

Changed paths:
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp

Log Message:
-----------
[C$] Tighten an AST fixtype.

Use Unicode character codes for the content of block comments, instead of just
natural numbers.


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

Changed paths:
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Tighten a fixtype in ASTs.

Use Unicode character codes in line comments of preprocessor lexemes.


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

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

Log Message:
-----------
[C$] Tighten an AST fixtype.


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

Changed paths:
M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/axe/arm/axe-rules.lisp
M books/kestrel/axe/arm/package.lsp
M books/kestrel/axe/arm/rule-lists.lisp
A books/kestrel/axe/arm/run-until-return-with-tracing.lisp
M books/kestrel/axe/arm/run-until-return.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/x86/tests/kestrel/assembly/add.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/evaluation.lisp
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
A books/kestrel/c/syntax/grammar/lexemes.abnf
A books/kestrel/c/syntax/grammar/tokens.abnf
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-options.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/x86/flags.lisp

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


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

Changed paths:
M books/kestrel/c/language/implementation-environments/dialects.lisp
M books/kestrel/c/syntax/grammar.lisp
A books/kestrel/c/syntax/grammar/expressions-ext.abnf
A books/kestrel/c/syntax/grammar/expressions-std.abnf
A books/kestrel/c/syntax/grammar/expressions.abnf
M books/kestrel/c/syntax/grammar/grammar-rest.abnf

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


Compare: https://github.com/acl2/acl2/compare/0f56681c7554...37bb516ee484

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

[Alessandro Coglio]

Branch: refs/heads/master

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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/syntax/unicode-characters.lisp
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Use a tighter fixtype.

Restrict the code field of a `s-char` AST to be a Unicode character code.

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

Changed paths:
M books/kestrel/c/language/implementation-environments/dialects.lisp

Log Message:
-----------
[C] Remove needless line break.

Compare: https://github.com/acl2/acl2/compare/f347790b179c...37bb516ee484

[Alessandro Coglio]

Branch: refs/heads/testing