		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-transformations

Remove-dead-if-branches

Remove all the dead if bramches in a term.

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

Each (if t a b) or (if (not nil) a b) is turned into a, and each (if nil a b) or (if (not t) a b) is turned into b. This is done to a and b, recursively.

Function: remove-dead-if-branches

(defun remove-dead-if-branches (term)
 (declare (xargs :guard (pseudo-termp term)))
 (let ((__function__ 'remove-dead-if-branches))
  (declare (ignorable __function__))
  (b*
   (((when (variablep term)) term)
    ((when (fquotep term)) term)
    (fn (ffn-symb term))
    ((when (and (eq fn 'if)
                (= (len (fargs term)) 3)))
     (cond
      ((member-equal (fargn term 1)
                     (list *t* (fcons-term 'not (list *nil*))))
       (remove-dead-if-branches (fargn term 2)))
      ((member-equal (fargn term 1)
                     (list *nil* (fcons-term 'not (list *t*))))
       (remove-dead-if-branches (fargn term 3)))
      (t
       (cons
          'if
          (cons (remove-dead-if-branches (fargn term 1))
                (cons (remove-dead-if-branches (fargn term 2))
                      (cons (remove-dead-if-branches (fargn term 3))
                            'nil)))))))
    (new-args (remove-dead-if-branches-lst (fargs term)))
    ((when (symbolp fn))
     (fcons-term fn new-args)))
   (fcons-term
        (make-lambda (lambda-formals fn)
                     (remove-dead-if-branches (lambda-body fn)))
        new-args))))

Function: remove-dead-if-branches-lst

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

Theorem: return-type-of-remove-dead-if-branches.new-term

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

Theorem: return-type-of-remove-dead-if-branches-lst.new-terms

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

Subtopics

Remove-dead-if-branches-lst