remove-dead-if-branches

(in-package "ACL2")

(defines remove-dead-if-branches
  :parents (std/system/term-transformations)
  :short "Remove all the dead @(tsee if) bramches in a term."
  :long (topstring (p "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.")
    (@def "remove-dead-if-branches")
    (@def "remove-dead-if-branches-lst"))
  (define remove-dead-if-branches
    ((term pseudo-termp))
    :returns (new-term pseudo-termp :hyp :guard)
    (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 `(if ,(REMOVE-DEAD-IF-BRANCHES (FARGN TERM 1))
                ,(REMOVE-DEAD-IF-BRANCHES (FARGN TERM 2))
                ,(REMOVE-DEAD-IF-BRANCHES (FARGN TERM 3))))))
        (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)))
  (define remove-dead-if-branches-lst
    ((terms pseudo-term-listp))
    :returns (new-terms (and (pseudo-term-listp new-terms)
        (equal (len new-terms) (len terms)))
      :hyp :guard)
    (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))))