		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-transformations

Close-lambdas

Make all the lambda expressions in a term closed.

Signature
(close-lambdas term) → new-term
Arguments: term — Guard (pseudo-termp term).
Returns: new-term — Type (pseudo-termp new-term), given (pseudo-termp term).

ACL2 lambda expressions in translated terms are always closed, which means that they often include formal parameters that are replaced by themselves (i.e. by the same symbols) when the lambda expression is applied. For instance, the untranslated term (let ((x 0)) (+ x y)) is ((lambda (x y) (binary-+ x y)) '3 y) in translated form: the lambda expression includes the extra formal parameter y which is not bound by the let, applied to y itself, making the lambda expression closed.

Terms with non-closed lambda expressions, e.g. produced by remove-trivial-vars, still satisfy pseudo-termp, but not termp. The close-lambdas utility closes any non-closed lambda expression in a term, so that it also satisfies lambdap. It is essentially the inverse of remove-trivial-vars.

Function: close-lambdas

(defun close-lambdas (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'close-lambdas))
    (declare (ignorable __function__))
    (b* (((when (variablep term)) term)
         ((when (fquotep term)) term)
         (fn (ffn-symb term))
         ((when (symbolp fn))
          (fcons-term fn (close-lambdas-lst (fargs term))))
         (formals (lambda-formals fn))
         (body (lambda-body fn))
         (actuals (fargs term))
         (new-body (close-lambdas body))
         (extra-params (set-difference-eq (all-vars new-body)
                                          formals))
         (new-formals (append formals extra-params))
         (new-actuals (append (close-lambdas-lst actuals)
                              extra-params)))
      (fcons-term (make-lambda new-formals new-body)
                  new-actuals))))

Function: close-lambdas-lst

(defun close-lambdas-lst (terms)
  (declare (xargs :guard (pseudo-term-listp terms)))
  (let ((__function__ 'close-lambdas-lst))
    (declare (ignorable __function__))
    (cond ((endp terms) nil)
          (t (cons (close-lambdas (car terms))
                   (close-lambdas-lst (cdr terms)))))))

Theorem: return-type-of-close-lambdas.new-term

(defthm return-type-of-close-lambdas.new-term
  (implies (pseudo-termp term)
           (b* ((?new-term (close-lambdas term)))
             (pseudo-termp new-term)))
  :rule-classes :rewrite)

Theorem: return-type-of-close-lambdas-lst.new-terms

(defthm return-type-of-close-lambdas-lst.new-terms
  (implies (pseudo-term-listp terms)
           (b* ((?new-terms (close-lambdas-lst terms)))
             (and (pseudo-term-listp new-terms)
                  (equal (len new-terms) (len terms)))))
  :rule-classes :rewrite)

Subtopics

Close-lambdas-lst