[acl2/acl2] 8313de: [FTY] Improve `deffold-reduce`.
0 views
Skip to first unread message
Alessandro Coglio
Jun 19, 2026, 3:07:08 PM (4 days ago) Jun 19
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 8313de4e1db7f0297047b100cfba41c4ec76a3d0
https://github.com/acl2/acl2/commit/8313de4e1db7f0297047b100cfba41c4ec76a3d0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp
Log Message:
-----------
[FTY] Improve `deffold-reduce`.
In the generated functions, also make the `:extra-args`, if any,
ignorable. Otherwise certain `:overrides` might cause failure.
Add some demonstrative tests.
Commit: 310c578b8026c616c7826621a089bea6ffde4d24
https://github.com/acl2/acl2/commit/310c578b8026c616c7826621a089bea6ffde4d24
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp
Log Message:
-----------
[FTY] Improve `deffold-map`.
Ensure that the `:extra-args`, if present, are declared ignorable in the
generated functions. This was already the case for most types, but not for list
types, which can be overridden. This commit adds that. It also updates the doc
of the other cases, which only mentioned the formal and not the extra args.
Add some demonstrative tests.
Commit: a116d0739e541315355c6a52eb49af699139107a
https://github.com/acl2/acl2/commit/a116d0739e541315355c6a52eb49af699139107a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
Log Message:
-----------
[C$] Export more symbols.
Commit: 44bbbb4a9dbb87cdcd1541127a6291bb448aebee
https://github.com/acl2/acl2/commit/44bbbb4a9dbb87cdcd1541127a6291bb448aebee
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
A books/kestrel/c/transformation/struct-safety-checks.lisp
M books/kestrel/c/transformation/top.lisp
Log Message:
-----------
[C2C] Start struct safety checks.
These are extremely strict, to the point of not being useful, but they are a
starting point.
Commit: 47a208421c91097d61628e9a875cd5d59efc8a52
https://github.com/acl2/acl2/commit/47a208421c91097d61628e9a875cd5d59efc8a52
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/fty/database.lisp
Log Message:
-----------
[FTY] Add a database query utility.
Commit: 0a8984478608089f2bad12ed8f05825f022c0752
https://github.com/acl2/acl2/commit/0a8984478608089f2bad12ed8f05825f022c0752
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp
Log Message:
-----------
[safestruct] Accept binary expressions.
Commit: 17347c8ae4c5aad39b475046424a4fbf8a94cb70
https://github.com/acl2/acl2/commit/17347c8ae4c5aad39b475046424a4fbf8a94cb70
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/fty/deffold-reduce.lisp
Log Message:
-----------
[FTY] Improve `deffold-reduce`.
Handle finding recognizers of base types, which do not have entries in the FTY
table.
Commit: d800102f900c52cbb64d917c15a137d0d0b1e91b
https://github.com/acl2/acl2/commit/d800102f900c52cbb64d917c15a137d0d0b1e91b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/fty/deffold-map.lisp
Log Message:
-----------
[FTY] Improve `deffold-map`.
Handle finding recognizers of base types, which do not have entries in the FTY
table.
Commit: 105caf57508af2b45afd8568b0ae642404b83199
https://github.com/acl2/acl2/commit/105caf57508af2b45afd8568b0ae642404b83199
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/fty/deffold-map-tests.lisp
Log Message:
-----------
[FTY] Simplify a test.
Commit: 29737382d848f1f208c38ab90c99603857c3739a
https://github.com/acl2/acl2/commit/29737382d848f1f208c38ab90c99603857c3739a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/fty/database.lisp
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp
Log Message:
-----------
Merge.
Commit: ed0517ca35065252382673cb11c8494a8e1a3801
https://github.com/acl2/acl2/commit/ed0517ca35065252382673cb11c8494a8e1a3801
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
Log Message:
-----------
[C$] Export more symbols.
Commit: 7c26e2b778606026c8cf017a4e7ab7291f0cbad5
https://github.com/acl2/acl2/commit/7c26e2b778606026c8cf017a4e7ab7291f0cbad5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp
Log Message:
-----------
[safestruct] Exclude atomic type qualifiers.
Commit: 506f8fb471da90efa5c096bb76b3bb0c0ed82b51
https://github.com/acl2/acl2/commit/506f8fb471da90efa5c096bb76b3bb0c0ed82b51
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp
Log Message:
-----------
[safestruct] Add some doc.
Commit: 64a53774f31d821c7296275a0865765b2f8d959d
https://github.com/acl2/acl2/commit/64a53774f31d821c7296275a0865765b2f8d959d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
Log Message:
-----------
[C$] Export more symbols.
Commit: 1b0409aa5e093440352961d230cc2fa601e6ee28
https://github.com/acl2/acl2/commit/1b0409aa5e093440352961d230cc2fa601e6ee28
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp
Log Message:
-----------
[safestruct] Elaborate checks.
Commit: 978708391d271438ad21a85619518d33c265bbe0
https://github.com/acl2/acl2/commit/978708391d271438ad21a85619518d33c265bbe0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
A books/kestrel/jsonrpc/.gitignore
A books/kestrel/jsonrpc/acl2-customization.lsp
A books/kestrel/jsonrpc/cert.acl2
A books/kestrel/jsonrpc/example-request.json
A books/kestrel/jsonrpc/json-to-string.lisp
A books/kestrel/jsonrpc/package.lsp
A books/kestrel/jsonrpc/parse-rpc.lisp
A books/kestrel/jsonrpc/portcullis.acl2
A books/kestrel/jsonrpc/portcullis.lisp
A books/kestrel/jsonrpc/process-rpc.lisp
A books/kestrel/jsonrpc/response.lisp
A books/kestrel/jsonrpc/socket-raw.lsp
A books/kestrel/jsonrpc/socket.lisp
A books/kestrel/jsonrpc/subtract-example.lisp
A books/kestrel/jsonrpc/top.lisp
A books/kestrel/jsonrpc/types.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/top.lisp
Log Message:
-----------
Merge.
Commit: 3e6aef89a2a684a4b948f881918813edf2a283b6
https://github.com/acl2/acl2/commit/3e6aef89a2a684a4b948f881918813edf2a283b6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp
Log Message:
-----------
[safestruct] Add mising type.
Commit: fef54874785bd77bc628ddc3652291ea36be4905
https://github.com/acl2/acl2/commit/fef54874785bd77bc628ddc3652291ea36be4905
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
Log Message:
-----------
[C$] Export more symbols.
Commit: c47f381a7d85190702b4f3215af3b0d659285bb2
https://github.com/acl2/acl2/commit/c47f381a7d85190702b4f3215af3b0d659285bb2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp
Log Message:
-----------
[safestruct] Fix XDOC links.
Compare: https://github.com/acl2/acl2/compare/e087174069d8...c47f381a7d85
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 8313de4e1db7f0297047b100cfba41c4ec76a3d0
https://github.com/acl2/acl2/commit/8313de4e1db7f0297047b100cfba41c4ec76a3d0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp
Log Message:
-----------
[FTY] Improve `deffold-reduce`.
In the generated functions, also make the `:extra-args`, if any,
ignorable. Otherwise certain `:overrides` might cause failure.
Add some demonstrative tests.
Commit: 310c578b8026c616c7826621a089bea6ffde4d24
https://github.com/acl2/acl2/commit/310c578b8026c616c7826621a089bea6ffde4d24
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp
Log Message:
-----------
[FTY] Improve `deffold-map`.
Ensure that the `:extra-args`, if present, are declared ignorable in the
generated functions. This was already the case for most types, but not for list
types, which can be overridden. This commit adds that. It also updates the doc
of the other cases, which only mentioned the formal and not the extra args.
Add some demonstrative tests.
Commit: a116d0739e541315355c6a52eb49af699139107a
https://github.com/acl2/acl2/commit/a116d0739e541315355c6a52eb49af699139107a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
Log Message:
-----------
[C$] Export more symbols.
Commit: 44bbbb4a9dbb87cdcd1541127a6291bb448aebee
https://github.com/acl2/acl2/commit/44bbbb4a9dbb87cdcd1541127a6291bb448aebee
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
A books/kestrel/c/transformation/struct-safety-checks.lisp
M books/kestrel/c/transformation/top.lisp
Log Message:
-----------
[C2C] Start struct safety checks.
These are extremely strict, to the point of not being useful, but they are a
starting point.
Commit: 47a208421c91097d61628e9a875cd5d59efc8a52
https://github.com/acl2/acl2/commit/47a208421c91097d61628e9a875cd5d59efc8a52
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/fty/database.lisp
Log Message:
-----------
[FTY] Add a database query utility.
Commit: 0a8984478608089f2bad12ed8f05825f022c0752
https://github.com/acl2/acl2/commit/0a8984478608089f2bad12ed8f05825f022c0752
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp
Log Message:
-----------
[safestruct] Accept binary expressions.
Commit: 17347c8ae4c5aad39b475046424a4fbf8a94cb70
https://github.com/acl2/acl2/commit/17347c8ae4c5aad39b475046424a4fbf8a94cb70
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/fty/deffold-reduce.lisp
Log Message:
-----------
[FTY] Improve `deffold-reduce`.
Handle finding recognizers of base types, which do not have entries in the FTY
table.
Commit: d800102f900c52cbb64d917c15a137d0d0b1e91b
https://github.com/acl2/acl2/commit/d800102f900c52cbb64d917c15a137d0d0b1e91b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/fty/deffold-map.lisp
Log Message:
-----------
[FTY] Improve `deffold-map`.
Handle finding recognizers of base types, which do not have entries in the FTY
table.
Commit: 105caf57508af2b45afd8568b0ae642404b83199
https://github.com/acl2/acl2/commit/105caf57508af2b45afd8568b0ae642404b83199
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/fty/deffold-map-tests.lisp
Log Message:
-----------
[FTY] Simplify a test.
Commit: 29737382d848f1f208c38ab90c99603857c3739a
https://github.com/acl2/acl2/commit/29737382d848f1f208c38ab90c99603857c3739a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/fty/database.lisp
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp
Log Message:
-----------
Merge.
Commit: ed0517ca35065252382673cb11c8494a8e1a3801
https://github.com/acl2/acl2/commit/ed0517ca35065252382673cb11c8494a8e1a3801
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
Log Message:
-----------
[C$] Export more symbols.
Commit: 7c26e2b778606026c8cf017a4e7ab7291f0cbad5
https://github.com/acl2/acl2/commit/7c26e2b778606026c8cf017a4e7ab7291f0cbad5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp
Log Message:
-----------
[safestruct] Exclude atomic type qualifiers.
Commit: 506f8fb471da90efa5c096bb76b3bb0c0ed82b51
https://github.com/acl2/acl2/commit/506f8fb471da90efa5c096bb76b3bb0c0ed82b51
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp
Log Message:
-----------
[safestruct] Add some doc.
Commit: 64a53774f31d821c7296275a0865765b2f8d959d
https://github.com/acl2/acl2/commit/64a53774f31d821c7296275a0865765b2f8d959d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
Log Message:
-----------
[C$] Export more symbols.
Commit: 1b0409aa5e093440352961d230cc2fa601e6ee28
https://github.com/acl2/acl2/commit/1b0409aa5e093440352961d230cc2fa601e6ee28
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp
Log Message:
-----------
[safestruct] Elaborate checks.
Commit: 978708391d271438ad21a85619518d33c265bbe0
https://github.com/acl2/acl2/commit/978708391d271438ad21a85619518d33c265bbe0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
A books/kestrel/jsonrpc/.gitignore
A books/kestrel/jsonrpc/acl2-customization.lsp
A books/kestrel/jsonrpc/cert.acl2
A books/kestrel/jsonrpc/example-request.json
A books/kestrel/jsonrpc/json-to-string.lisp
A books/kestrel/jsonrpc/package.lsp
A books/kestrel/jsonrpc/parse-rpc.lisp
A books/kestrel/jsonrpc/portcullis.acl2
A books/kestrel/jsonrpc/portcullis.lisp
A books/kestrel/jsonrpc/process-rpc.lisp
A books/kestrel/jsonrpc/response.lisp
A books/kestrel/jsonrpc/socket-raw.lsp
A books/kestrel/jsonrpc/socket.lisp
A books/kestrel/jsonrpc/subtract-example.lisp
A books/kestrel/jsonrpc/top.lisp
A books/kestrel/jsonrpc/types.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/top.lisp
Log Message:
-----------
Merge.
Commit: 3e6aef89a2a684a4b948f881918813edf2a283b6
https://github.com/acl2/acl2/commit/3e6aef89a2a684a4b948f881918813edf2a283b6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp
Log Message:
-----------
[safestruct] Add mising type.
Commit: fef54874785bd77bc628ddc3652291ea36be4905
https://github.com/acl2/acl2/commit/fef54874785bd77bc628ddc3652291ea36be4905
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
Log Message:
-----------
[C$] Export more symbols.
Commit: c47f381a7d85190702b4f3215af3b0d659285bb2
https://github.com/acl2/acl2/commit/c47f381a7d85190702b4f3215af3b0d659285bb2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp
Log Message:
-----------
[safestruct] Fix XDOC links.
Compare: https://github.com/acl2/acl2/compare/e087174069d8...c47f381a7d85
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Jun 19, 2026, 3:07:37 PM (4 days ago) Jun 19
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
Jun 19, 2026, 4:20:36 PM (4 days ago) Jun 19
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Reply all
Reply to author
Forward
0 new messages