[acl2/acl2] b440ab: [C2C] Improve interface of `simpadd0`.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: b440ab366b8fb7ddd4b138c05cf494eeec63cdb2
https://github.com/acl2/acl2/commit/b440ab366b8fb7ddd4b138c05cf494eeec63cdb2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/tests/simpadd0/asg-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/bin.lisp
M books/kestrel/c/transformation/tests/simpadd0/blocks.lisp
M books/kestrel/c/transformation/tests/simpadd0/cast-int-to-long.lisp
M books/kestrel/c/transformation/tests/simpadd0/cast-long-to-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/constant.lisp
M books/kestrel/c/transformation/tests/simpadd0/decl.lisp
M books/kestrel/c/transformation/tests/simpadd0/file-scope.lisp
M books/kestrel/c/transformation/tests/simpadd0/gg.lisp
M books/kestrel/c/transformation/tests/simpadd0/global.lisp
M books/kestrel/c/transformation/tests/simpadd0/if.lisp
M books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
M books/kestrel/c/transformation/tests/simpadd0/logand.lisp
M books/kestrel/c/transformation/tests/simpadd0/logor.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-const.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-param.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-return.lisp
M books/kestrel/c/transformation/tests/simpadd0/noninteger.lisp
M books/kestrel/c/transformation/tests/simpadd0/nosimp-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/nosimp-short.lisp
M books/kestrel/c/transformation/tests/simpadd0/nosimp-ulong.lisp
M books/kestrel/c/transformation/tests/simpadd0/paren.lisp
M books/kestrel/c/transformation/tests/simpadd0/return-void.lisp
M books/kestrel/c/transformation/tests/simpadd0/stmt-null.lisp
M books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/var.lisp
M books/kestrel/c/transformation/tests/simpadd0/while.lisp

Log Message:
-----------
[C2C] Improve interface of `simpadd0`.

Have it take keyword inputs `:const-old` and `:const-new`.


Commit: a363e56ae660dade937ea1fc80f3bef908b1904b
https://github.com/acl2/acl2/commit/a363e56ae660dade937ea1fc80f3bef908b1904b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/object-type-preservation.lisp
M books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/language/variable-visibility-preservation.lisp

Log Message:
-----------
[C] Improve formalization of dynamic semantics.

Make `exec-expr-call-or-asg` also return a result, besides the new computation
state, for more uniformity.


Commit: 23858b1641d9eb3f488d4c9f7ac9783022349757
https://github.com/acl2/acl2/commit/23858b1641d9eb3f488d4c9f7ac9783022349757
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-call-or-asg.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp

Log Message:
-----------
[ATC] Adapt to changes to dynamic semantics formulation.


Commit: 06f4921340ab65ad55c3103d0779ac0f23f540ef
https://github.com/acl2/acl2/commit/06f4921340ab65ad55c3103d0779ac0f23f540ef
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/printer.lisp
A books/kestrel/c/syntax/printing.lisp
M books/kestrel/c/syntax/top.lisp

Log Message:
-----------
[C$] Add a file and topic for printing.

Put the printer under there.


Commit: 1e34c90c2f0ef1d1316b21cf7095d03978999d6c
https://github.com/acl2/acl2/commit/1e34c90c2f0ef1d1316b21cf7095d03978999d6c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/projects/hol-in-acl2/acl2/lemmas.lisp
M books/projects/hol-in-acl2/acl2/package.lsp
M books/projects/hol-in-acl2/acl2/theories.lisp
A books/projects/hol-in-acl2/acl2/typ.lisp
M books/projects/hol-in-acl2/examples/README
A books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
A books/projects/hol-in-acl2/examples/eval-poly-thy-alt.lisp
A books/projects/hol-in-acl2/to-do.txt

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


Commit: e1ea1caaca32b8ffd5399f1654b679c497b9a02c
https://github.com/acl2/acl2/commit/e1ea1caaca32b8ffd5399f1654b679c497b9a02c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 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/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.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/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

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


Commit: 2d302a8cb5955cc2719e6a112ff693c860f4bab5
https://github.com/acl2/acl2/commit/2d302a8cb5955cc2719e6a112ff693c860f4bab5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 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/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.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-all-gso.lisp
M books/kestrel/c/transformation/splitgso.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: b6f35a0eb53aec662ecf000d67ced6da93fef2dc
https://github.com/acl2/acl2/commit/b6f35a0eb53aec662ecf000d67ced6da93fef2dc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
A books/kestrel/fty/character-set.lisp
M books/kestrel/fty/top.lisp

Log Message:
-----------
[FTY] Add fixtype of osets of characters.


Commit: 4cc080371e8f624cf285a550fb6f0adfffe47739
https://github.com/acl2/acl2/commit/4cc080371e8f624cf285a550fb6f0adfffe47739
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
A books/kestrel/fty/any-nat-map.lisp
M books/kestrel/fty/top.lisp

Log Message:
-----------
[FTY] Add fixtype of omaps from anything to naturals.


Commit: bf80b4dd82ac3b98c4767eaf3be8e9f8262e4ebf
https://github.com/acl2/acl2/commit/bf80b4dd82ac3b98c4767eaf3be8e9f8262e4ebf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 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/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.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/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

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


Commit: 7583eede2b6ac7ead0912cc9c210f7387b28bc45
https://github.com/acl2/acl2/commit/7583eede2b6ac7ead0912cc9c210f7387b28bc45
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
A books/kestrel/fty/character-any-map.lisp
M books/kestrel/fty/top.lisp

Log Message:
-----------
[FTY] Add fixtype of omaps from characters to anything.


Commit: aea17e245251dd990631c306537b4e956b787ac3
https://github.com/acl2/acl2/commit/aea17e245251dd990631c306537b4e956b787ac3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 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/parser.lisp
M books/kestrel/c/syntax/printer.lisp
A books/kestrel/c/syntax/printing.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/top.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-all-gso.lisp
M books/kestrel/c/transformation/splitgso.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

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


Commit: 85d14dd4076f2813b722641f23104c37fbb965e5
https://github.com/acl2/acl2/commit/85d14dd4076f2813b722641f23104c37fbb965e5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
A books/kestrel/fty/any-nat-map.lisp
A books/kestrel/fty/character-any-map.lisp
A books/kestrel/fty/character-set.lisp
M books/kestrel/fty/top.lisp

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


Compare: https://github.com/acl2/acl2/compare/271ae997abda...85d14dd4076f

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

[acl2buildserver]

Branch: refs/heads/testing

Commit: 2f56a758c818c219981c1f1d7d7f573ba3de6e4e
https://github.com/acl2/acl2/commit/2f56a758c818c219981c1f1d7d7f573ba3de6e4e
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-09-23 (Tue, 23 Sep 2025)

Changed paths:
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-call-or-asg.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/object-type-preservation.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-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
A books/kestrel/c/syntax/printing.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp

M books/kestrel/c/transformation/simpadd0-doc.lisp

M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/splitgso.lisp

M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

A books/kestrel/fty/any-nat-map.lisp
A books/kestrel/fty/character-any-map.lisp
A books/kestrel/fty/character-set.lisp
M books/kestrel/fty/top.lisp

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

Merge commit '85d14dd4076f2813b722641f23104c37fbb965e5' into HEAD


Compare: https://github.com/acl2/acl2/compare/54d516353d96...2f56a758c818