		Search-engine friendly clone of the ACL2 documentation.

Dead-code-eliminator-execution

Funscope-dead

Eliminate dead code in function scopes.

Signature
(funscope-dead funscope) → new-funscope
Arguments: funscope — Guard (funscopep funscope).
Returns: new-funscope — Type (funscopep new-funscope).

We transform all the function information values of the map.

Definitions and Theorems

Function: funscope-dead

(defun funscope-dead (funscope)
  (declare (xargs :guard (funscopep funscope)))
  (let ((__function__ 'funscope-dead))
    (declare (ignorable __function__))
    (b* ((funscope (funscope-fix funscope))
         ((when (omap::emptyp funscope)) nil)
         ((mv name info) (omap::head funscope)))
      (omap::update name (funinfo-dead info)
                    (funscope-dead (omap::tail funscope))))))

Theorem: funscopep-of-funscope-dead

(defthm funscopep-of-funscope-dead
  (b* ((new-funscope (funscope-dead funscope)))
    (funscopep new-funscope))
  :rule-classes :rewrite)

Theorem: keys-of-funscope-dead

(defthm keys-of-funscope-dead
  (implies (funscopep funscope)
           (equal (omap::keys (funscope-dead funscope))
                  (omap::keys funscope))))

Theorem: consp-of-in-of-funscope-dead

(defthm consp-of-in-of-funscope-dead
  (implies (funscopep funscope)
           (equal (consp (omap::assoc fun (funscope-dead funscope)))
                  (consp (omap::assoc fun funscope)))))

Theorem: cdr-of-in-of-funscope-dead

(defthm cdr-of-in-of-funscope-dead
  (implies (and (funscopep funscope)
                (omap::assoc fun funscope))
           (equal (cdr (omap::assoc fun (funscope-dead funscope)))
                  (funinfo-dead (cdr (omap::assoc fun funscope))))))

Theorem: funscope-dead-of-update

(defthm funscope-dead-of-update
  (implies (and (identifierp name)
                (funinfop info)
                (funscopep funscope))
           (equal (funscope-dead (omap::update name info funscope))
                  (omap::update name (funinfo-dead info)
                                (funscope-dead funscope)))))

Theorem: funscope-dead-of-funscope-fix-funscope

(defthm funscope-dead-of-funscope-fix-funscope
  (equal (funscope-dead (funscope-fix funscope))
         (funscope-dead funscope)))

Theorem: funscope-dead-funscope-equiv-congruence-on-funscope

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