[acl2/acl2] 79ca5f: [C$] Assign unique identifiers to typedefs

[Grant Jurgensen]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 79ca5f613de76dd135c1cc2f946a21789fccf264
https://github.com/acl2/acl2/commit/79ca5f613de76dd135c1cc2f946a21789fccf264
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validation-tables.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
[C$] Assign unique identifiers to typedefs

Extend the typedef validation info and the typedef name type specifier annotation with a UID. Assign a fresh UID at each typedef declaration, reusing the existing one when a typedef is redefined in the same scope with a compatible type. Record the declaration's UID at each typedef name use site.

Since every initializer declarator now declares an object, function, or typedef name, all of which receive UIDs, make the init-declor-info UID required rather than optional, updating the transformation utilities that read it. Add validator tests covering typedef UID assignment, redefinition, use sites, and inner-scope shadowing.


Commit: 350c3cc80f89f6eb7fc686180d38f4b80f5dfde5
https://github.com/acl2/acl2/commit/350c3cc80f89f6eb7fc686180d38f4b80f5dfde5
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validation-tables.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
Merge branch 'gj-validator-typedef' into testing-kestrel


Commit: 7dd2e5c9db06edde49860f5ea6e1cf27101005c2
https://github.com/acl2/acl2/commit/7dd2e5c9db06edde49860f5ea6e1cf27101005c2
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp

Log Message:
-----------
[C2C] Fix struct-type-split for non-optional typedef uid field

The [C$] validator now assigns a non-optional `uid` field to the info
defprods (init-declor-info, param-declor-nonabstract-info), replacing the
old optional `uid?`. init-declor-sts-split still referenced the removed
info.uid?, breaking certification. Mirror the already-migrated
param-declor-sts-split: drop the now-dead "(not info.uid?)" internal-error
guard (a uid defprod is never nil) and use info.uid.


Compare: https://github.com/acl2/acl2/compare/6e383038423b...7dd2e5c9db06

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

[acl2buildserver]

Branch: refs/heads/testing

Commit: 568df750b73e6ad6c9e802e684ab79753e1389a0
https://github.com/acl2/acl2/commit/568df750b73e6ad6c9e802e684ab79753e1389a0

Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:

M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/typedef-chain.c

Log Message:
-----------
[C2C] Support typedefs of the split struct type.

Now that the validator assigns unique identifiers to typedefs, a typedef
of a splittable type is split into a parallel right typedef, and uses of
the typedef name are substituted via the identifier map. Typedef
declarations reuse the existing uid-keyed declarator renaming, so the
core change is the type-spec typedef use case; the four rejection sites
and two detectors are removed. Add tests for direct, pointer, and chained
typedefs.


Commit: 8c2a205f1091b758ad1764e488a4b54902673462
https://github.com/acl2/acl2/commit/8c2a205f1091b758ad1764e488a4b54902673462
Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-06-16 (Tue, 16 Jun 2026)

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

M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/typedef-chain.c

M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------

Merge commit '568df750b73e6ad6c9e802e684ab79753e1389a0' into HEAD


Compare: https://github.com/acl2/acl2/compare/d17801e14737...8c2a205f1091

[acl2buildserver]

Branch: refs/heads/master