		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

All-vars-open

Free variables in a term that may contain non-closed (i.e. open) lambda expressions.

Signature
(all-vars-open term) → vars
Arguments: term — Guard (pseudo-termp term).
Returns: vars — Type (symbol-listp vars), given the guard.

When trivial lambda-bound variables are removed from a term via remove-trivial-vars, some lambda expressions may not be closed. For collecting the free variables of this kind of terms, the system utility all-vars is inadequate, because it skips over lambda expressions, assuming they are closed, as is the case in ACL2's internal translated form.

Thus, we define a utility similar to all-vars that does not skip over lambda expressions. Instead, it collects the free variables of the body of a lambda expression, removes the formal parameters of the lambda expressions, and regards the remaining variables as the free ones of the lambda expression. This is the standard treatment of lambda expressions in languages where lambda expressions are not necessarily closed.

The returned list of variables has no duplicates. The list is in no particular order.

Function: all-vars-open

(defun all-vars-open (term)
 (declare (xargs :guard (pseudo-termp term)))
 (let ((__function__ 'all-vars-open))
   (declare (ignorable __function__))
   (b*
     (((when (variablep term)) (list term))
      ((when (fquotep term)) nil)
      (fn (ffn-symb term))
      (fn-vars (if (symbolp fn)
                   nil
                 (set-difference-eq (all-vars-open (lambda-body fn))
                                    (lambda-formals fn))))
      (args-vars (all-vars-open-lst (fargs term))))
     (union-eq fn-vars args-vars))))

Function: all-vars-open-lst

(defun all-vars-open-lst (terms)
  (declare (xargs :guard (pseudo-term-listp terms)))
  (let ((__function__ 'all-vars-open-lst))
    (declare (ignorable __function__))
    (cond ((endp terms) nil)
          (t (union-eq (all-vars-open (car terms))
                       (all-vars-open-lst (cdr terms)))))))

Theorem: return-type-of-all-vars-open.vars

(defthm return-type-of-all-vars-open.vars
  (implies (and (pseudo-termp term))
           (b* ((?vars (all-vars-open term)))
             (symbol-listp vars)))
  :rule-classes :rewrite)

Theorem: return-type-of-all-vars-open-lst.vars

(defthm return-type-of-all-vars-open-lst.vars
  (implies (and (pseudo-term-listp terms))
           (b* ((?vars (all-vars-open-lst terms)))
             (symbol-listp vars)))
  :rule-classes :rewrite)

Theorem: true-listp-of-all-vars-open

(defthm true-listp-of-all-vars-open
  (b* ((?vars (all-vars-open term)))
    (true-listp vars))
  :rule-classes :type-prescription)

Theorem: true-listp-of-all-vars-open-lst

(defthm true-listp-of-all-vars-open-lst
  (b* ((?vars (all-vars-open-lst terms)))
    (true-listp vars))
  :rule-classes :type-prescription)

Subtopics

All-vars-open-lst