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.

books/kestrel/utilities/term-applicand-recognizers.lisp

@@ -0,0 +1,101 @@
+; Term Applicand Recognizers
+;
+; Copyright (C) 2016-2017 Kestrel Institute (http://www.kestrel.edu)
+;
+; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
+;
+; Author: Alessandro Coglio (coglio@kestrel.edu)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(in-package "ACL2")
+
+(include-book "std/util/define" :dir :system)
+
+(local (include-book "all-vars-theorems"))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(defxdoc term-applicand-recognizers
+  :parents (term-utilities system-utilities)
+  :short "Recognizers of term applicands."
+  :long
+  "<p>
+   In translated @(see term)s,
+   applicands are lambda expressions and function names.
+   They are applied to argument terms.
+   </p>
+   <p>
+   The built-in predicates @(tsee pseudo-termp) and @(tsee termp)
+   recognize pseudo-terms and terms.
+   The following predicates recognize lambda expressions and applicands
+   in pseudo-terms and terms.
+   </p>")
+
+(define pseudo-lambdap (x)
+  :returns (yes/no booleanp)
+  :parents (term-utilities term-applicand-recognizers)
+  :short "Recognize pseudo-lambda-expressions,
+          i.e. lambda expressions of
+          <see topic='@(url pseudo-termp)'>pseudo-terms</see>."
+  :long
+  "<p>
+   Check whether @('x') is
+   a @('nil')-terminated list of exactly three elements,
+   whose first element is the symbol @('lambda'),
+   whose second element is a list of symbols, and
+   whose third element is a pseudo-term.
+   </p>"
+  (and (true-listp x)
+       (= (len x) 3)
+       (eq (first x) 'lambda)
+       (symbol-listp (second x))
+       (pseudo-termp (third x))))
+
+(define pseudo-fn/lambda-p (x)
+  :returns (yes/no booleanp)
+  :parents (term-utilities term-applicand-recognizers)
+  :short "Recognize pseudo-applicands,
+          i.e. symbols and pseudo-lambda-expressions."
+  :long
+  "<p>
+   Check whether @('x') is a symbol or a
+   <see topic='@(url pseudo-lambdap)'>pseudo-lambda-expression</see>.
+   These are the possible values of the first element of
+   a <see topic='@(url pseudo-termp)'>pseudo-term</see>
+   that is not a variable or a quoted constant
+   (i.e. a pseudo-term that is a function application).
+   </p>"
+  (or (symbolp x)
+      (pseudo-lambdap x)))
+
+(define lambdap (x (wrld plist-worldp-with-formals))
+  :returns (yes/no booleanp)
+  :parents (term-utilities term-applicand-recognizers)
+  :short "Recognize valid
+          <see topic='@(url term)'>translated</see> lambda expression."
+  :long
+  "<p>
+   Check whether @('x') is a @('nil')-terminated list of exactly three elements,
+   whose first element is the symbol @('lambda'),
+   whose second element is a list of legal variable symbols without duplicates,
+   and whose third element is a valid translated term
+   whose free variables are all among the ones in the second element.
+   </p>"
+  (and (true-listp x)
+       (= (len x) 3)
+       (eq (first x) 'lambda)
+       (arglistp (second x))
+       (termp (third x) wrld)
+       (subsetp-eq (all-vars (third x))
+                   (second x))))
+
+(define fn/lambda-p (x (wrld plist-worldp-with-formals))
+  :returns (yes/no booleanp)
+  :parents (term-utilities term-applicand-recognizers)
+  :short "Recognize valid applicands,
+          i.e. function symbols and
+          <see topic='@(url term)'>translated</see> lambda expression."
+  (or (and (symbolp x)
+           (function-symbolp x wrld))
+      (lambdap x wrld)))

books/kestrel/utilities/terms.lisp

@@ -15,6 +15,7 @@
 (in-package "ACL2")
 
 (include-book "std/util/defines" :dir :system)
+(include-book "term-applicand-recognizers")
 (include-book "world-queries")
 
 (local (include-book "all-vars-theorems"))
@@ -26,71 +27,6 @@
   :parents (kestrel-utilities system-utilities)
   :short "Utilities for @(see term)s.")
 
-(define pseudo-lambdap (x)
-  :returns (yes/no booleanp)
-  :parents (term-utilities)
-  :short "Recognize lambda expressions of
-          <see topic='@(url pseudo-termp)'>pseudo-terms</see>."
-  :long
-  "<p>
-   Check whether @('x') is
-   a @('nil')-terminated list of exactly three elements,
-   whose first element is the symbol @('lambda'),
-   whose second element is a list of symbols, and
-   whose third element is a pseudo-term.
-   </p>"
-  (and (true-listp x)
-       (= (len x) 3)
-       (eq (first x) 'lambda)
-       (symbol-listp (second x))
-       (pseudo-termp (third x))))
-
-(define pseudo-fn/lambda-p (x)
-  :returns (yes/no booleanp)
-  :parents (term-utilities)
-  :short "Recognize symbols and
-          lambda expressions of
-          <see topic='@(url pseudo-termp)'>pseudo-terms</see>."
-  :long
-  "<p>
-   Check whether @('x') is a symbol or a
-   <see topic='@(url pseudo-lambdap)'>pseudo-lambda-expression</see>.
-   These are the possible values of the first element of
-   a pseudo-term that is not a variable or a quoted constant
-   (i.e. a pseudo-term that is a function application).
-   </p>"
-  (or (symbolp x)
-      (pseudo-lambdap x)))
-
-(define lambdap (x (wrld plist-worldp-with-formals))
-  :returns (yes/no booleanp)
-  :parents (term-utilities)
-  :short "Recognize valid
-          <see topic='@(url term)'>translated</see> lambda expression."
-  :long
-  "<p>
-   Check whether @('x') is a @('nil')-terminated list of exactly three elements,
-   whose first element is the symbol @('lambda'),
-   whose second element is a list of legal variable symbols without duplicates,
-   and whose third element is a valid translated term
-   whose free variables are all among the ones in the second element.
-   </p>"
-  (and (true-listp x)
-       (= (len x) 3)
-       (eq (first x) 'lambda)
-       (arglistp (second x))
-       (termp (third x) wrld)
-       (subsetp-eq (all-vars (third x))
-                   (second x))))
-
-(define fn/lambda-p (x (wrld plist-worldp-with-formals))
-  :returns (yes/no booleanp)
-  :parents (term-utilities)
-  :short "Recognize valid function symbols and
-          <see topic='@(url term)'>translated</see> lambda expression."
-  (or (function-namep x wrld)
-      (lambdap x wrld)))
-
 (define lambda-closedp ((lambd pseudo-lambdap))
   :returns (yes/no booleanp)
   :parents (term-utilities)