[acl2/acl2] 9cc58d: Improve RESTRICT transformation.

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: 9cc58d71fd07cc9efba4f1be442efd90a8985eb6
https://github.com/acl2/acl2/commit/9cc58d71fd07cc9efba4f1be442efd90a8985eb6
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-06 (Sun, 06 Aug 2017)

Changed paths:
M books/kestrel/apt/restrict-reference.lisp
M books/kestrel/apt/restrict-tests.lisp
M books/kestrel/apt/restrict.lisp

Log Message:
-----------
Improve RESTRICT transformation.

Ensure that the target function does not occur in the term that defines the
domain restriction. This seems reasonable, given that the purpose of the
transformation is generally to "replace" the target function with the new one;
but this decision may be revisited, if there is a good example.


Commit: 6372418cfaaccefa07e91c8f26e4deeb491cda42
https://github.com/acl2/acl2/commit/6372418cfaaccefa07e91c8f26e4deeb491cda42
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-06 (Sun, 06 Aug 2017)

Changed paths:
M books/kestrel/apt/restrict-reference.lisp
M books/kestrel/apt/restrict-tests.lisp
M books/kestrel/apt/restrict.lisp

Log Message:
-----------
Extend the RESTRICT transformation.

It is now possible to customize the value to return outside the domain
restriction. The default is :UNDEFINED.


Commit: 3e08d4737128aae4cf318f2b607c3fd4178859a7
https://github.com/acl2/acl2/commit/3e08d4737128aae4cf318f2b607c3fd4178859a7
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-06 (Sun, 06 Aug 2017)

Changed paths:
M books/kestrel/utilities/error-checking.lisp

Log Message:
-----------
Improve message in error-checking utilities.

Clarify that non-guard-verified functions may occur in EC-CALL besides in the
:LOGIC subterms of MBEs.


Commit: ea96c6cb3ad17e730d27ebf7e6f7f01009c21dcd
https://github.com/acl2/acl2/commit/ea96c6cb3ad17e730d27ebf7e6f7f01009c21dcd
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-06 (Sun, 06 Aug 2017)

Changed paths:
M books/kestrel/apt/restrict-reference.lisp
M books/kestrel/apt/tailrec-reference.lisp

Log Message:
-----------
Improve documentation of APT transformations.

Clarify that, for certain purposes, non-guard-verified functions may occur not
only in :LOGIC subterms of MBEs, but also in EC-CALLs.


Commit: 551154c51f055a03705bbb954d543b3a7ee2ed7f
https://github.com/acl2/acl2/commit/551154c51f055a03705bbb954d543b3a7ee2ed7f
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-08-06 (Sun, 06 Aug 2017)

Changed paths:
M books/kestrel/apt/package.lsp
M books/kestrel/apt/tailrec-reference.lisp
M books/kestrel/apt/tailrec-tests.lisp
M books/kestrel/apt/tailrec.lisp

Log Message:
-----------
Improve TAILREC transformation.

Ensure that the target function is not the domain (if the domain is a function)
and is not called by the domain (if the domain is a lambda expression). This
seems reasonable since the purpose of the transformation is generally to replace
the old function with the new one, but this decision could be revisited if there
is a good example.


Compare: https://github.com/acl2/acl2/compare/24b69e4884a6...551154c51f05

[GitHub]

Branch: refs/heads/master