[acl2/acl2] e579b5: [C2C] Report the file path in struct-type-split er...

[Grant Jurgensen]

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

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

Log Message:
-----------
[C2C] Report the file path in struct-type-split errors

When a translation unit cannot be transformed, the error now names the
translation unit it came from. Add a filepath field to sts-split-state,
set per translation unit in sts-split-trans-units, and wrap the errors
surfacing from sts-check-completions and trans-unit-sts-split with the
file path via a new sts-error-in-translation-unit helper. Ensemble-level
errors (struct lookup, C17 check, input processing, re-validation) are
left unchanged.


Commit: d669e35fe2f3adb273bc8b73bc5f2e7579d8cb35
https://github.com/acl2/acl2/commit/d669e35fe2f3adb273bc8b73bc5f2e7579d8cb35
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-06-24 (Wed, 24 Jun 2026)

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

Log Message:
-----------
[C$] Fix argument order in nat-to-iconst

The calls to signed-byte-p and unsigned-byte-p passed the numeric value
as the bit width and the byte count as the value, so the representability
checks were backwards: small values such as 1 through 3 were reported as
unrepresentable, and the length suffix did not depend on the value's
magnitude. Compare the value against the implementation environment's
INT_MAX, LONG_MAX, LLONG_MAX, and ULLONG_MAX instead.


Commit: 8825e437ae97ddcbf66238e27c8b207d1c982ef3
https://github.com/acl2/acl2/commit/8825e437ae97ddcbf66238e27c8b207d1c982ef3
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-06-24 (Wed, 24 Jun 2026)

Changed paths:
A books/kestrel/c/syntax/tests/types-to-tynames.lisp
M books/kestrel/c/syntax/top.lisp
A books/kestrel/c/syntax/types-to-tynames.lisp

Log Message:
-----------
[C$] Add type-to-tyname conversion utility

Add types-to-tynames.lisp, which converts a validator type into an
abstract syntax type name (tyname) for pretty-printing. It handles
scalar, pointer, array, function, and tagged and untagged structure and
union types, reconstructing the members for the untagged case, and
returns an error for types with no source-level representation
(enumeration and unknown types). Array sizes are built with
nat-to-iconst, so the conversion takes an implementation environment.
Also add a test book and include the new book in top.lisp.


Commit: e7d7f834c670c363ee46f4807da611ff97c8ead0
https://github.com/acl2/acl2/commit/e7d7f834c670c363ee46f4807da611ff97c8ead0
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-06-24 (Wed, 24 Jun 2026)

Changed paths:
M books/kestrel/c/transformation/utilities/context-msg.lisp
M books/kestrel/c/transformation/utilities/print-to-str.lisp

Log Message:
-----------
[C2C] Add type printing and context-message utilities

Add print-type-to-str and context-msg-type, which render a validator
type as a type name by converting it with type-to-tyname and printing
the result. Both fall back gracefully (an error flag, or the raw type in
the message) when the type has no source-level representation.


Commit: e97adafdbf17dc6287ad57b22dd6e6b4a7a0a007
https://github.com/acl2/acl2/commit/e97adafdbf17dc6287ad57b22dd6e6b4a7a0a007
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-06-24 (Wed, 24 Jun 2026)

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

Log Message:
-----------
[C2C] Render types as type names in struct-type-split messages

Use context-msg-type to print the offending type as a type name in the
error messages of sts-check-type, instead of dumping the raw type with
~x. Store the implementation environment in sts-split-state so it is
available for the conversion.


Compare: https://github.com/acl2/acl2/compare/74be596754bd...e97adafdbf17

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

[Grant Jurgensen]

Branch: refs/heads/master

[Grant Jurgensen]

Branch: refs/heads/testing