		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-transformations

Remove-unused-vars

Remove all the lambda-bound variables that are not used.

Signature
(remove-unused-vars term) → new-term
Arguments: term — Guard (pseudo-termp term).
Returns: new-term — Type (pseudo-termp new-term), given the guard.

We go through the term and, for each lambda expression we encounter, we remove all the formal parameters, and corresponding actual parameters, that are not free in the body of the lambda expression, i.e. that are not used. If all the formal parameters are unused, we replace the lambda expression with its body.

The new term is logically equivalent to the old term. If the actual parameters that have been removed have no side effects, executing the new term gives the same outcomes as executing the old term (except for perhaps doing so a little faster).

In order to prove termination, we add an mbt that establishes the hypothesis of the theorem about remove-unused-vars-aux asserting that the new actual parameters are not more than the old ones.

Function: remove-unused-vars

(defun remove-unused-vars (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'remove-unused-vars))
    (declare (ignorable __function__))
    (b* (((when (variablep term)) term)
         ((when (fquotep term)) term)
         (fn (ffn-symb term))
         ((when (symbolp fn))
          (fcons-term fn
                      (remove-unused-vars-lst (fargs term))))
         (formals (lambda-formals fn))
         (body (lambda-body fn))
         (actuals (fargs term))
         (body-vars (all-vars body))
         ((unless (mbt (equal (len formals) (len actuals))))
          nil)
         ((mv formals actuals)
          (remove-unused-vars-aux formals actuals body-vars))
         ((when (eq formals nil))
          (remove-unused-vars body))
         (actuals (remove-unused-vars-lst actuals))
         (body (remove-unused-vars body)))
      (fcons-term (make-lambda formals body)
                  actuals))))

Function: remove-unused-vars-lst

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

Function: remove-unused-vars-aux

(defun remove-unused-vars-aux (formals actuals body-vars)
  (declare (xargs :guard (and (symbol-listp formals)
                              (pseudo-term-listp actuals)
                              (symbol-listp body-vars))))
  (declare (xargs :guard (= (len formals) (len actuals))))
  (let ((__function__ 'remove-unused-vars-aux))
    (declare (ignorable __function__))
    (b* (((when (endp formals)) (mv nil nil))
         (formal (car formals))
         (actual (car actuals))
         ((unless (member-eq formal body-vars))
          (remove-unused-vars-aux (cdr formals)
                                  (cdr actuals)
                                  body-vars))
         ((mv formals actuals)
          (remove-unused-vars-aux (cdr formals)
                                  (cdr actuals)
                                  body-vars)))
      (mv (cons formal formals)
          (cons actual actuals)))))

Theorem: return-type-of-remove-unused-vars.new-term

(defthm return-type-of-remove-unused-vars.new-term
  (implies (and (pseudo-termp term))
           (b* ((?new-term (remove-unused-vars term)))
             (pseudo-termp new-term)))
  :rule-classes :rewrite)

Theorem: return-type-of-remove-unused-vars-lst.new-terms

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

Subtopics

Remove-unused-vars-aux
Remove-unused-vars-lst