		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-transformations

Remove-progn

Turn every call of prog2$ and progn$ in a term into just its last argument.

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

In translated terms, prog2$ and progn$ have the form (return-last 'progn a b). We turn that form into just b.

Function: remove-progn

(defun remove-progn (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'remove-progn))
    (declare (ignorable __function__))
    (b* (((when (variablep term)) term)
         ((when (fquotep term)) term)
         (fn (ffn-symb term))
         (args (fargs term))
         ((when (and (eq fn 'return-last)
                     (equal (first args) ''progn)))
          (remove-progn (third args)))
         (new-fn (if (symbolp fn)
                     fn
                   (make-lambda (lambda-formals fn)
                                (remove-progn (lambda-body fn)))))
         (new-args (remove-progn-lst args)))
      (fcons-term new-fn new-args))))

Function: remove-progn-lst

(defun remove-progn-lst (terms)
  (declare (xargs :guard (pseudo-term-listp terms)))
  (let ((__function__ 'remove-progn-lst))
    (declare (ignorable __function__))
    (b* (((when (endp terms)) nil)
         ((cons term terms) terms)
         (new-term (remove-progn term))
         (new-terms (remove-progn-lst terms)))
      (cons new-term new-terms))))

Theorem: return-type-of-remove-progn.new-term

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

Theorem: return-type-of-remove-progn-lst.new-terms

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

Subtopics

Remove-progn-lst