		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Funvars-of-term/terms

Function variables that terms depend on.

A term may depend on a function variable directly (when the function variable occurs in the term) or indirectly (when a the second-order function that occurs in the term depends on the function variable).

Note that, in the following code, if (sofunp fn wrld) is nil, then fn is a first-order function, which depends on no function variables.

The returned list may contain duplicates.

Function: funvars-of-term

(defun funvars-of-term (term wrld)
  (declare (xargs :guard (and (pseudo-termp term)
                              (plist-worldp wrld))))
  (let ((__function__ 'funvars-of-term))
    (declare (ignorable __function__))
    (if (or (variablep term) (quotep term))
        nil
      (let* ((fn (fn-symb term))
             (fn-vars (if (flambdap fn)
                          (funvars-of-term (lambda-body fn) wrld)
                        (if (funvarp fn wrld)
                            (list fn)
                          (if (sofunp fn wrld)
                              (sofun-funvars fn wrld)
                            nil)))))
        (append fn-vars
                (funvars-of-terms (fargs term)
                                  wrld))))))

Function: funvars-of-terms

(defun funvars-of-terms (terms wrld)
  (declare (xargs :guard (and (pseudo-term-listp terms)
                              (plist-worldp wrld))))
  (let ((__function__ 'funvars-of-terms))
    (declare (ignorable __function__))
    (if (endp terms)
        nil
      (append (funvars-of-term (car terms) wrld)
              (funvars-of-terms (cdr terms) wrld)))))

Definitions and Theorems

Function: funvars-of-term

(defun funvars-of-term (term wrld)
  (declare (xargs :guard (and (pseudo-termp term)
                              (plist-worldp wrld))))
  (let ((__function__ 'funvars-of-term))
    (declare (ignorable __function__))
    (if (or (variablep term) (quotep term))
        nil
      (let* ((fn (fn-symb term))
             (fn-vars (if (flambdap fn)
                          (funvars-of-term (lambda-body fn) wrld)
                        (if (funvarp fn wrld)
                            (list fn)
                          (if (sofunp fn wrld)
                              (sofun-funvars fn wrld)
                            nil)))))
        (append fn-vars
                (funvars-of-terms (fargs term)
                                  wrld))))))

Function: funvars-of-terms

(defun funvars-of-terms (terms wrld)
  (declare (xargs :guard (and (pseudo-term-listp terms)
                              (plist-worldp wrld))))
  (let ((__function__ 'funvars-of-terms))
    (declare (ignorable __function__))
    (if (endp terms)
        nil
      (append (funvars-of-term (car terms) wrld)
              (funvars-of-terms (cdr terms) wrld)))))

Subtopics

Funvars-of-term
Funvars-of-terms