		Search-engine friendly clone of the ACL2 documentation.

Dead-code-eliminator-execution

Funinfo-dead

Eliminate dead code in function information.

Signature
(funinfo-dead info) → new-info
Arguments: info — Guard (funinfop info).
Returns: new-info — Type (funinfop new-info).

We apply the transformation to the body of the function.

Definitions and Theorems

Function: funinfo-dead

(defun funinfo-dead (info)
  (declare (xargs :guard (funinfop info)))
  (let ((__function__ 'funinfo-dead))
    (declare (ignorable __function__))
    (change-funinfo info
                    :body (block-dead (funinfo->body info)))))

Theorem: funinfop-of-funinfo-dead

(defthm funinfop-of-funinfo-dead
  (b* ((new-info (funinfo-dead info)))
    (funinfop new-info))
  :rule-classes :rewrite)

Theorem: funinfo-dead-of-funinfo

(defthm funinfo-dead-of-funinfo
  (equal (funinfo-dead (funinfo inputs outputs body))
         (funinfo inputs outputs (block-dead body))))

Theorem: funinfo->inputs-of-funinfo-dead

(defthm funinfo->inputs-of-funinfo-dead
  (equal (funinfo->inputs (funinfo-dead info))
         (funinfo->inputs info)))

Theorem: funinfo->outputs-of-funinfo-dead

(defthm funinfo->outputs-of-funinfo-dead
  (equal (funinfo->outputs (funinfo-dead info))
         (funinfo->outputs info)))

Theorem: funinfo->body-of-funinfo-dead

(defthm funinfo->body-of-funinfo-dead
  (equal (funinfo->body (funinfo-dead info))
         (block-dead (funinfo->body info))))

Theorem: funinfo-dead-of-funinfo-fix-info

(defthm funinfo-dead-of-funinfo-fix-info
  (equal (funinfo-dead (funinfo-fix info))
         (funinfo-dead info)))

Theorem: funinfo-dead-funinfo-equiv-congruence-on-info

(defthm funinfo-dead-funinfo-equiv-congruence-on-info
  (implies (funinfo-equiv info info-equiv)
           (equal (funinfo-dead info)
                  (funinfo-dead info-equiv)))
  :rule-classes :congruence)