all-free-bound-vars

(in-package "ACL2")

(defines all-free/bound-vars
  :parents (std/system/term-queries)
  :short "Return all the free and bound variables that occur in a term."
  :long (topstring (p "The returned list of variables is in no particular order,
     but it has no duplicates,
     because we use @(tsee union-eq) to join variable lists.")
    (p "This utility is in contrast with the built-in @(tsee all-vars),
     which returns only the free variables.")
    (@def "all-free/bound-vars")
    (@def "all-free/bound-vars-lst"))
  (define all-free/bound-vars
    ((term pseudo-termp))
    :returns (vars symbol-listp :hyp :guard)
    (cond ((variablep term) (list term))
      ((fquotep term) nil)
      (t (b* ((fn/lambda (ffn-symb term)) (fn/lambda-vars (and (flambdap fn/lambda)
                (union-eq (lambda-formals fn/lambda)
                  (all-free/bound-vars (lambda-body fn/lambda)))))
            (args-vars (all-free/bound-vars-lst (fargs term))))
          (union-eq fn/lambda-vars args-vars)))))
  (define all-free/bound-vars-lst
    ((terms pseudo-term-listp))
    :returns (vars symbol-listp :hyp :guard)
    (cond ((endp terms) nil)
      (t (union-eq (all-free/bound-vars (car terms))
          (all-free/bound-vars-lst (cdr terms))))))
  :verify-guards nil
  ///
  (verify-guards all-free/bound-vars))