[acl2/acl2] 8a7878: [axe] Improve printing of add-known-boolean.

0 views
Skip to first unread message

Eric W. Smith

unread,
Dec 4, 2025, 4:58:08 PM (3 days ago) Dec 4
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 8a787887c57a6d6b90c0685a11b273e47bb8c5ae
https://github.com/acl2/acl2/commit/8a787887c57a6d6b90c0685a11b273e47bb8c5ae
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/known-booleans.lisp

Log Message:
-----------
[axe] Improve printing of add-known-boolean.


Commit: 90c0859b5a067b33dde38fbc54a7fd4e6fb2e065
https://github.com/acl2/acl2/commit/90c0859b5a067b33dde38fbc54a7fd4e6fb2e065
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/x86/canonical-unsigned.lisp

Log Message:
-----------
[axe/x86] Improve rule lists.

Add unsigned-canonical-address-p-smt. Also fix a rule name and a priority.


Commit: b4803e54daf68dc7aeb326535a0627f38b9dfe2d
https://github.com/acl2/acl2/commit/b4803e54daf68dc7aeb326535a0627f38b9dfe2d
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/x86-rules.lisp

Log Message:
-----------
[axe/x86] Add comment.


Commit: ed2e0173a724b8fb50bdbfa19546cd8aae2dd528
https://github.com/acl2/acl2/commit/ed2e0173a724b8fb50bdbfa19546cd8aae2dd528
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp

Log Message:
-----------
[axe/x86] Improve examples.

Remove rule now built in.


Commit: 404c9900e128ecaf37d9de71672429fbf20d831a
https://github.com/acl2/acl2/commit/404c9900e128ecaf37d9de71672429fbf20d831a
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/bv/bvsx.lisp

Log Message:
-----------
[bv] Generalize 2 rules.


Commit: 94267115fdf9d32317090c78741c7eb1a2ebee2d
https://github.com/acl2/acl2/commit/94267115fdf9d32317090c78741c7eb1a2ebee2d
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/bv/trim-intro-rules.lisp

Log Message:
-----------
[bv] Add bvsx-trim-all.


Commit: a088dcc485b63953530d89a5211428d5431cc3aa
https://github.com/acl2/acl2/commit/a088dcc485b63953530d89a5211428d5431cc3aa
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/bv/convert-to-bv-rules.lisp

Log Message:
-----------
[bv] Add bvsx-convert-arg3-to-bv.


Commit: 3de3eae48de82c41a90b192c21e19b2df00258ae
https://github.com/acl2/acl2/commit/3de3eae48de82c41a90b192c21e19b2df00258ae
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/convert-to-bv-rules-axe.lisp

Log Message:
-----------
[axe] Improve rule.


Commit: d39d46cc5dc465031da5493bf8c230fc8126eaba
https://github.com/acl2/acl2/commit/d39d46cc5dc465031da5493bf8c230fc8126eaba
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/trim-intro-rules-axe.lisp

Log Message:
-----------
[axe] Add bvsx-trim-axe-all.


Commit: 98ec0eabbc7a3bac9e58f0944c956948b352790d
https://github.com/acl2/acl2/commit/98ec0eabbc7a3bac9e58f0944c956948b352790d
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

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

Log Message:
-----------
[axe] Improve rule-lists.


Commit: ce181e38c7bd98d68e9f34be8635b3982ecc2751
https://github.com/acl2/acl2/commit/ce181e38c7bd98d68e9f34be8635b3982ecc2751
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp

Log Message:
-----------
[axe/x86] Improve examples.

Remove rules that are now built-in.


Commit: dffba2abc9de8153d3186c749a01d7e6c77e1d42
https://github.com/acl2/acl2/commit/dffba2abc9de8153d3186c749a01d7e6c77e1d42
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
A books/kestrel/c/atc/pure-expression-execution.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-asg.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-call.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
M books/kestrel/c/atc/tutorial.lisp
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
M books/kestrel/c/language/execution-without-function-calls.lisp
M books/kestrel/c/language/object-type-preservation.lisp
R books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/language/variable-visibility-preservation.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

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


Commit: 9c539f1c2861123a8cb12cfda8e102abd7cd0b0d
https://github.com/acl2/acl2/commit/9c539f1c2861123a8cb12cfda8e102abd7cd0b0d
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/rule-lists.lisp

Log Message:
-----------
[axe/x86] Build in another rule.


Commit: 3619b348d5dbf819f80c97853ce5ec309791631c
https://github.com/acl2/acl2/commit/3619b348d5dbf819f80c97853ce5ec309791631c
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/x86/read-and-write.lisp

Log Message:
-----------
[x86] Generalize rules.


Commit: f66585ed684cf543064ed9d2a647efb4a894ff80
https://github.com/acl2/acl2/commit/f66585ed684cf543064ed9d2a647efb4a894ff80
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

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

Log Message:
-----------
[axe/x86] Add comments.


Commit: 02fadb48544e2d94363ef1aab28dc25e83a56fcb
https://github.com/acl2/acl2/commit/02fadb48544e2d94363ef1aab28dc25e83a56fcb
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/rule-lists.lisp

Log Message:
-----------
[axe/x86] Build in more rules.


Compare: https://github.com/acl2/acl2/compare/86bf84bbcd8e...02fadb48544e

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

Eric W. Smith

unread,
Dec 4, 2025, 6:28:07 PM (3 days ago) Dec 4
to acl2-...@googlegroups.com
Branch: refs/heads/master

Eric W. Smith

unread,
Dec 4, 2025, 6:28:36 PM (3 days ago) Dec 4
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
Dec 5, 2025, 3:07:30 PM (2 days ago) Dec 5
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: cfefb5d8e6800f9636c1a570f0f20b97e89d8012
https://github.com/acl2/acl2/commit/cfefb5d8e6800f9636c1a570f0f20b97e89d8012
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

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

Log Message:
-----------
[C$] Advance preprocessor.

Add tokenizer.


Commit: 83ef3861a986d6fb9c6e7781e70b3dc891ac5357
https://github.com/acl2/acl2/commit/83ef3861a986d6fb9c6e7781e70b3dc891ac5357
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
Commit: bfdafd9a87e5abbabafb55db09e788b5bbf7dec6
https://github.com/acl2/acl2/commit/bfdafd9a87e5abbabafb55db09e788b5bbf7dec6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

Log Message:
-----------
[C$] Improve some AST names.
Commit: 48ecf0eb37040cb1d6ede627b81da05ebbb963a0
https://github.com/acl2/acl2/commit/48ecf0eb37040cb1d6ede627b81da05ebbb963a0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)

Changed paths:
M books/kestrel/axe/convert-to-bv-rules-axe.lisp
M books/kestrel/axe/known-booleans.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/trim-intro-rules-axe.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/bv/trim-intro-rules.lisp
M books/kestrel/x86/canonical-unsigned.lisp
M books/kestrel/x86/read-and-write.lisp

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


Commit: 859c1e92d06f958d5c8dc19f614086c423902406
https://github.com/acl2/acl2/commit/859c1e92d06f958d5c8dc19f614086c423902406
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

Log Message:
-----------
[C$] Improve some AST names.


Commit: bd20b8aa1f7023b2a805985b28e53f3f3abb7879
https://github.com/acl2/acl2/commit/bd20b8aa1f7023b2a805985b28e53f3f3abb7879
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

Log Message:
-----------
[C$] Improve some AST names.


Commit: 9202202dfd1cfc2b8a6c8a221b6ee65f5a0164a3
https://github.com/acl2/acl2/commit/9202202dfd1cfc2b8a6c8a221b6ee65f5a0164a3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)

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

Log Message:
-----------
[C$] Improve some AST names.


Commit: 17ae2fa4f05fb0cbde5fead656a985019cc41a47
https://github.com/acl2/acl2/commit/17ae2fa4f05fb0cbde5fead656a985019cc41a47
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)

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

Log Message:
-----------
[C$] Improve some AST names.


Commit: 720091317e22591de4b7048351ef3ee77ce54d2e
https://github.com/acl2/acl2/commit/720091317e22591de4b7048351ef3ee77ce54d2e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)

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

Log Message:
-----------
[C$] Improve some AST names.


Commit: b7e96d5a9282e96b55cfa0b9653354743083588e
https://github.com/acl2/acl2/commit/b7e96d5a9282e96b55cfa0b9653354743083588e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)

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

Log Message:
-----------
[C$] Improve some AST names.


Commit: 1fbe2440f197c0564b25901cb8388b365e22efce
https://github.com/acl2/acl2/commit/1fbe2440f197c0564b25901cb8388b365e22efce
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/tests/disambiguator.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/free-vars/free-vars.lisp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
[C$] Improve some AST names.


Commit: 4847349e15720c4927192b59e9fced66a7f7ede4
https://github.com/acl2/acl2/commit/4847349e15720c4927192b59e9fced66a7f7ede4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)

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

Log Message:
-----------
[C$] Fix a doc reference.


Commit: 10504252ce9658efe6cca734ad60fc041ff2c8e6
https://github.com/acl2/acl2/commit/10504252ce9658efe6cca734ad60fc041ff2c8e6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)

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

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


Commit: 563cd83bbca5c8871223811a31c10005772f571d
https://github.com/acl2/acl2/commit/563cd83bbca5c8871223811a31c10005772f571d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)

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

Log Message:
-----------
[C$] Add an irrelevant.


Commit: 135396cccbfd1d527713ef6887fde20693915ffb
https://github.com/acl2/acl2/commit/135396cccbfd1d527713ef6887fde20693915ffb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
[C$] Improve some AST names.


Commit: 3d4d935d14d7e4fb6a99436d285f435f099b14d9
https://github.com/acl2/acl2/commit/3d4d935d14d7e4fb6a99436d285f435f099b14d9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)

Changed paths:
M books/kestrel/axe/convert-to-bv-rules-axe.lisp
M books/kestrel/axe/known-booleans.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/trim-intro-rules-axe.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/bv/trim-intro-rules.lisp
M books/kestrel/c/syntax/file-paths.lisp
M books/kestrel/c/syntax/files.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/x86/canonical-unsigned.lisp
M books/kestrel/x86/read-and-write.lisp

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


Compare: https://github.com/acl2/acl2/compare/86bf84bbcd8e...3d4d935d14d7

Eric W. Smith

unread,
Dec 5, 2025, 4:05:57 PM (2 days ago) Dec 5
to acl2-...@googlegroups.com
Branch: refs/heads/testing-acl2s
Commit: 6afd2c084328a612337776a5140067a6354cb97b
https://github.com/acl2/acl2/commit/6afd2c084328a612337776a5140067a6354cb97b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/proof-generation.lisp

Log Message:
-----------
[C$] Improve some AST names.

Generally trying to avoid non-descript `unwrap` field names in fixtypes.


Commit: cb40186a2b4f06c6a24bf04aac8b70e756f03cb2
https://github.com/acl2/acl2/commit/cb40186a2b4f06c6a24bf04aac8b70e756f03cb2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

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

Log Message:
-----------
[C$] Improve some AST names.


Commit: f7be5985d04a2c8634602088935d29f186c1642b
https://github.com/acl2/acl2/commit/f7be5985d04a2c8634602088935d29f186c1642b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

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

Log Message:
-----------
[C$] Improve AST names.


Commit: 665d5048f2361db1408a3cec90c8284e7cd91c16
https://github.com/acl2/acl2/commit/665d5048f2361db1408a3cec90c8284e7cd91c16
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

Log Message:
-----------
[C$] Improve some AST names.


Commit: e159f1e445970a26d24583902dfa8421c1802ed0
https://github.com/acl2/acl2/commit/e159f1e445970a26d24583902dfa8421c1802ed0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

Log Message:
-----------
[C$] Improve some AST names.


Commit: 86bf84bbcd8e4bdb9d8e14380d5ed6171ebb6f04
https://github.com/acl2/acl2/commit/86bf84bbcd8e4bdb9d8e14380d5ed6171ebb6f04
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
A books/kestrel/c/atc/pure-expression-execution.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-asg.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-call.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
M books/kestrel/c/language/execution-without-function-calls.lisp
M books/kestrel/c/language/object-type-preservation.lisp
R books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/language/variable-visibility-preservation.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Compare: https://github.com/acl2/acl2/compare/fd800b5c9308...02fadb48544e
Reply all
Reply to author
Forward
0 new messages