[acl2/acl2] 81ca70: [C$] Add support for basic constant evaluation.

[Grant Jurgensen]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 81ca700810aa9ca6b70a80abfa6e33ca6ca1abcf
https://github.com/acl2/acl2/commit/81ca700810aa9ca6b70a80abfa6e33ca6ca1abcf
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-04-14 (Tue, 14 Apr 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/compilation-db.lisp
A books/kestrel/c/syntax/evaluation.lisp
M books/kestrel/c/syntax/infer-ienv.lisp
M books/kestrel/c/syntax/output-files.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/tests/compilation-db.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
M books/kestrel/c/syntax/tests/parser-states.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/tests/preprocess-file.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/reader.lisp
M books/kestrel/c/syntax/top.lisp

Log Message:
-----------
[C$] Add support for basic constant evaluation.

The symbol 'value is no longer exported from the ACL2 package. This
commit therefore features a number of incidental changes, where the
acl2::value function had to be explicitly prefixed by the acl2 package.


Commit: 006bea42cf7c1f777a5d187961219d113bda89b1
https://github.com/acl2/acl2/commit/006bea42cf7c1f777a5d187961219d113bda89b1
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-04-14 (Tue, 14 Apr 2026)

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

Log Message:
-----------
[C$] Make valid-dec/oct/hex-const delegate to dec/oct/hex-const->value.

Move the canonical implementation to abstract-syntax-operations,
with documentation. The validator's valid-dec/oct/hex-const now
simply calls dec/oct/hex-const->value.

Co-Authored-By: Claude Sonnet 4.6 <nor...@anthropic.com>


Commit: 4ab7e1957144fd9ad8cfcd13e0ba92f743bfff22
https://github.com/acl2/acl2/commit/4ab7e1957144fd9ad8cfcd13e0ba92f743bfff22
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-04-14 (Tue, 14 Apr 2026)

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

Log Message:
-----------
[C$] Incorporate Alessandro Coglio's suggestions

On PR 1931.


Commit: 31e0c0e5edbd98545950481921e190dc98fb45c7
https://github.com/acl2/acl2/commit/31e0c0e5edbd98545950481921e190dc98fb45c7
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-04-14 (Tue, 14 Apr 2026)

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

Log Message:
-----------
[C$] Fix XDOC links.


Compare: https://github.com/acl2/acl2/compare/7f286f3f337d...31e0c0e5edbd

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