Mutually recursive functions to eliminate dead code in statements, blocks, cases, and function definitions.
Function:
(defun statement-dead (stmt) (declare (xargs :guard (statementp stmt))) (let ((__function__ 'statement-dead)) (declare (ignorable __function__)) (statement-case stmt :block (statement-block (block-dead stmt.get)) :variable-single (statement-fix stmt) :variable-multi (statement-fix stmt) :assign-single (statement-fix stmt) :assign-multi (statement-fix stmt) :funcall (statement-fix stmt) :if (make-statement-if :test stmt.test :body (block-dead stmt.body)) :for (make-statement-for :init (block-dead stmt.init) :test stmt.test :update (block-dead stmt.update) :body (block-dead stmt.body)) :switch (make-statement-switch :target stmt.target :cases (swcase-list-dead stmt.cases) :default (block-option-dead stmt.default)) :leave (statement-leave) :break (statement-break) :continue (statement-continue) :fundef (statement-fundef (fundef-dead stmt.get)))))
Function:
(defun statement-list-dead (stmts) (declare (xargs :guard (statement-listp stmts))) (let ((__function__ 'statement-list-dead)) (declare (ignorable __function__)) (b* (((when (endp stmts)) nil) (stmt (car stmts)) (new-stmt (statement-dead stmt)) ((when (or (statement-case stmt :leave) (statement-case stmt :break) (statement-case stmt :continue))) (list new-stmt))) (cons new-stmt (statement-list-dead (cdr stmts))))))
Function:
(defun block-dead (block) (declare (xargs :guard (blockp block))) (let ((__function__ 'block-dead)) (declare (ignorable __function__)) (block (statement-list-dead (block->statements block)))))
Function:
(defun block-option-dead (block?) (declare (xargs :guard (block-optionp block?))) (let ((__function__ 'block-option-dead)) (declare (ignorable __function__)) (block-option-case block? :some (block-dead block?.val) :none nil)))
Function:
(defun swcase-dead (case) (declare (xargs :guard (swcasep case))) (let ((__function__ 'swcase-dead)) (declare (ignorable __function__)) (make-swcase :value (swcase->value case) :body (block-dead (swcase->body case)))))
Function:
(defun swcase-list-dead (cases) (declare (xargs :guard (swcase-listp cases))) (let ((__function__ 'swcase-list-dead)) (declare (ignorable __function__)) (cond ((endp cases) nil) (t (cons (swcase-dead (car cases)) (swcase-list-dead (cdr cases)))))))
Function:
(defun fundef-dead (fundef) (declare (xargs :guard (fundefp fundef))) (let ((__function__ 'fundef-dead)) (declare (ignorable __function__)) (make-fundef :name (fundef->name fundef) :inputs (fundef->inputs fundef) :outputs (fundef->outputs fundef) :body (block-dead (fundef->body fundef)))))
Theorem:
(defthm return-type-of-statement-dead.new-stmt (b* ((?new-stmt (statement-dead stmt))) (statementp new-stmt)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-statement-list-dead.new-stmt (b* ((?new-stmt (statement-list-dead stmts))) (statement-listp new-stmt)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-block-dead.new-block (b* ((?new-block (block-dead block))) (blockp new-block)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-block-option-dead.new-block? (b* ((?new-block? (block-option-dead block?))) (block-optionp new-block?)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-swcase-dead.new-case (b* ((?new-case (swcase-dead case))) (swcasep new-case)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-swcase-list-dead.new-cases (b* ((?new-cases (swcase-list-dead cases))) (swcase-listp new-cases)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-fundef-dead.new-fdef (b* ((?new-fdef (fundef-dead fundef))) (fundefp new-fdef)) :rule-classes :rewrite)
Theorem:
(defthm statement-dead-of-statement-fix-stmt (equal (statement-dead (statement-fix stmt)) (statement-dead stmt)))
Theorem:
(defthm statement-list-dead-of-statement-list-fix-stmts (equal (statement-list-dead (statement-list-fix stmts)) (statement-list-dead stmts)))
Theorem:
(defthm block-dead-of-block-fix-block (equal (block-dead (block-fix block)) (block-dead block)))
Theorem:
(defthm block-option-dead-of-block-option-fix-block? (equal (block-option-dead (block-option-fix block?)) (block-option-dead block?)))
Theorem:
(defthm swcase-dead-of-swcase-fix-case (equal (swcase-dead (swcase-fix case)) (swcase-dead case)))
Theorem:
(defthm swcase-list-dead-of-swcase-list-fix-cases (equal (swcase-list-dead (swcase-list-fix cases)) (swcase-list-dead cases)))
Theorem:
(defthm fundef-dead-of-fundef-fix-fundef (equal (fundef-dead (fundef-fix fundef)) (fundef-dead fundef)))
Theorem:
(defthm statement-dead-statement-equiv-congruence-on-stmt (implies (statement-equiv stmt stmt-equiv) (equal (statement-dead stmt) (statement-dead stmt-equiv))) :rule-classes :congruence)
Theorem:
(defthm statement-list-dead-statement-list-equiv-congruence-on-stmts (implies (statement-list-equiv stmts stmts-equiv) (equal (statement-list-dead stmts) (statement-list-dead stmts-equiv))) :rule-classes :congruence)
Theorem:
(defthm block-dead-block-equiv-congruence-on-block (implies (block-equiv block block-equiv) (equal (block-dead block) (block-dead block-equiv))) :rule-classes :congruence)
Theorem:
(defthm block-option-dead-block-option-equiv-congruence-on-block? (implies (block-option-equiv block? block?-equiv) (equal (block-option-dead block?) (block-option-dead block?-equiv))) :rule-classes :congruence)
Theorem:
(defthm swcase-dead-swcase-equiv-congruence-on-case (implies (swcase-equiv case case-equiv) (equal (swcase-dead case) (swcase-dead case-equiv))) :rule-classes :congruence)
Theorem:
(defthm swcase-list-dead-swcase-list-equiv-congruence-on-cases (implies (swcase-list-equiv cases cases-equiv) (equal (swcase-list-dead cases) (swcase-list-dead cases-equiv))) :rule-classes :congruence)
Theorem:
(defthm fundef-dead-fundef-equiv-congruence-on-fundef (implies (fundef-equiv fundef fundef-equiv) (equal (fundef-dead fundef) (fundef-dead fundef-equiv))) :rule-classes :congruence)
Theorem:
(defthm statement-kind-of-statement-dead (equal (statement-kind (statement-dead stmt)) (statement-kind stmt)))
Theorem:
(defthm block->statements-of-block-dead (equal (block->statements (block-dead block)) (statement-list-dead (block->statements block))))
Theorem:
(defthm block-option-dead-iff (iff (block-option-dead block?) block?))
Theorem:
(defthm swcase->value-of-swcase-dead (equal (swcase->value (swcase-dead case)) (swcase->value case)))
Theorem:
(defthm consp-of-swcase-list-dead (equal (consp (swcase-list-dead cases)) (consp cases)))
Theorem:
(defthm fundef->name-of-fundef-dead (equal (fundef->name (fundef-dead fdef)) (fundef->name fdef)))