[acl2/acl2] 527c51: [C$] Refine our model of array types.

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
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: 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.


Compare: https://github.com/acl2/acl2/compare/0f56681c7554...ebed9b5f79a1

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