[acl2/acl2] c530d7: Slightly refactor term utilities.

[GitHub]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: c530d756c75343e3fe82a97807fbcf14b9a13124
https://github.com/acl2/acl2/commit/c530d756c75343e3fe82a97807fbcf14b9a13124
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-10-16 (Mon, 16 Oct 2017)

Changed paths:
A books/kestrel/utilities/term-applicand-recognizers.lisp
M books/kestrel/utilities/terms.lisp

Log Message:
-----------
Slightly refactor term utilities.

Put the term applicand recognizers (PSEUDO-LAMBDAP, LAMBDAP, PSEUDO-FN/LAMBDA-P,
and FN/LAMBDA-P) into a separate file, so they can be included into
worldp-queries.lisp (which is already included into terms.lisp) without causing
inclusion circularities.

Also create an XDOC topic for these term applicand recognizers.


Commit: 08279ebde1fbda68dee041798423e3b189b4e00e
https://github.com/acl2/acl2/commit/08279ebde1fbda68dee041798423e3b189b4e00e
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-10-16 (Mon, 16 Oct 2017)

Changed paths:
M books/kestrel/utilities/world-queries.lisp

Log Message:
-----------
Strengthen guard of IRECURSIVEP+ system utility.

Require the argument function to be in logic mode, otherwise the RECURSIVEP
property may not be reliable.


Commit: 5f1b1ad0285cf00da4bf8e3dde78a1eeae95ec4c
https://github.com/acl2/acl2/commit/5f1b1ad0285cf00da4bf8e3dde78a1eeae95ec4c
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-10-16 (Mon, 16 Oct 2017)

Changed paths:
A books/kestrel/utilities/term-applicand-recognizers-tests.lisp
M books/kestrel/utilities/terms-tests.lisp

Log Message:
-----------
Split term tests into two files.

This mirrors the factoring of the term applicand recognizers out of the term
utilities file.


Commit: 3cfeaa6669891b865459309b90ba6329172c913f
https://github.com/acl2/acl2/commit/3cfeaa6669891b865459309b90ba6329172c913f
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-10-16 (Mon, 16 Oct 2017)

Changed paths:
A books/kestrel/utilities/arglistp-theorems.lisp
M books/kestrel/utilities/top.lisp

Log Message:
-----------
Add a theorem about ARGLISTP.


Commit: 5a236bf178c5204c4da1207353dbc5847d410b18
https://github.com/acl2/acl2/commit/5a236bf178c5204c4da1207353dbc5847d410b18
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-10-16 (Mon, 16 Oct 2017)

Changed paths:
M books/kestrel/utilities/world-queries.lisp

Log Message:
-----------
Add two world query utilities.

FORMALS+ and ARITY+ are "logic-friendly" variants of the built-in FORMALS and
ARITY system utilities, with stronger guards and return type theorems. They also
operate on lambda expressions.


Commit: ef8ef1e716a643896fc7602f6596814a2a454b3b
https://github.com/acl2/acl2/commit/ef8ef1e716a643896fc7602f6596814a2a454b3b
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2017-10-16 (Mon, 16 Oct 2017)

Changed paths:
M books/kestrel/utilities/world-queries-tests.lisp

Log Message:
-----------
Add some tests for the newly added FORMALS+ and ARITY+.


Compare: https://github.com/acl2/acl2/compare/bf204464f77d...ef8ef1e716a6

[GitHub]

Branch: refs/heads/master