Disambiguate statements, blocks, and related entities.
Function:
(defun dimb-stmt (stmt table) (declare (xargs :guard (and (stmtp stmt) (dimb-tablep table)))) (let ((__function__ 'dimb-stmt)) (declare (ignorable __function__)) (b* (((reterr) (irr-stmt) (irr-dimb-table))) (stmt-case stmt :labeled (b* (((erp new-label table) (dimb-label stmt.label table)) ((erp new-stmt table) (dimb-stmt stmt.stmt table))) (retok (make-stmt-labeled :label new-label :stmt new-stmt) table)) :compound (b* ((table (dimb-push-scope table)) ((erp new-items table) (dimb-block-item-list stmt.items table)) (table (dimb-pop-scope table))) (retok (stmt-compound new-items) table)) :expr (b* (((erp new-expr? table) (dimb-expr-option stmt.expr? table))) (retok (stmt-expr new-expr?) table)) :if (b* ((table (dimb-push-scope table)) ((erp new-test table) (dimb-expr stmt.test table)) (table (dimb-push-scope table)) ((erp new-then table) (dimb-stmt stmt.then table)) (table (dimb-pop-scope table)) (table (dimb-pop-scope table))) (retok (make-stmt-if :test new-test :then new-then) table)) :ifelse (b* ((table (dimb-push-scope table)) ((erp new-test table) (dimb-expr stmt.test table)) (table (dimb-push-scope table)) ((erp new-then table) (dimb-stmt stmt.then table)) (table (dimb-pop-scope table)) (table (dimb-push-scope table)) ((erp new-else table) (dimb-stmt stmt.else table)) (table (dimb-pop-scope table)) (table (dimb-pop-scope table))) (retok (make-stmt-ifelse :test new-test :then new-then :else new-else) table)) :switch (b* ((table (dimb-push-scope table)) ((erp new-target table) (dimb-expr stmt.target table)) (table (dimb-push-scope table)) ((erp new-body table) (dimb-stmt stmt.body table)) (table (dimb-pop-scope table)) (table (dimb-pop-scope table))) (retok (make-stmt-switch :target new-target :body new-body) table)) :while (b* ((table (dimb-push-scope table)) ((erp new-test table) (dimb-expr stmt.test table)) (table (dimb-push-scope table)) ((erp new-body table) (dimb-stmt stmt.body table)) (table (dimb-pop-scope table)) (table (dimb-pop-scope table))) (retok (make-stmt-while :test new-test :body new-body) table)) :dowhile (b* ((table (dimb-push-scope table)) (table (dimb-push-scope table)) ((erp new-body table) (dimb-stmt stmt.body table)) (table (dimb-pop-scope table)) ((erp new-test table) (dimb-expr stmt.test table)) (table (dimb-pop-scope table))) (retok (make-stmt-dowhile :body new-body :test new-test) table)) :for-expr (b* ((table (dimb-push-scope table)) ((erp new-init table) (dimb-expr-option stmt.init table)) ((erp new-test table) (dimb-expr-option stmt.test table)) ((erp new-next table) (dimb-expr-option stmt.next table)) (table (dimb-push-scope table)) ((erp new-body table) (dimb-stmt stmt.body table)) (table (dimb-pop-scope table))) (retok (make-stmt-for-expr :init new-init :test new-test :next new-next :body new-body) table)) :for-decl (b* ((table (dimb-push-scope table)) ((erp new-init table) (dimb-decl stmt.init table)) ((erp new-test table) (dimb-expr-option stmt.test table)) ((erp new-next table) (dimb-expr-option stmt.next table)) (table (dimb-push-scope table)) ((erp new-body table) (dimb-stmt stmt.body table)) (table (dimb-pop-scope table))) (retok (make-stmt-for-decl :init new-init :test new-test :next new-next :body new-body) table)) :for-ambig (b* ((table (dimb-push-scope table)) ((erp decl/expr table) (dimb-amb-decl/stmt stmt.init table)) ((erp new-test table) (dimb-expr-option stmt.test table)) ((erp new-next table) (dimb-expr-option stmt.next table)) (table (dimb-push-scope table)) ((erp new-body table) (dimb-stmt stmt.body table)) (table (dimb-pop-scope table))) (decl/stmt-case decl/expr :decl (retok (make-stmt-for-decl :init decl/expr.unwrap :test new-test :next new-next :body new-body) table) :stmt (retok (make-stmt-for-expr :init decl/expr.unwrap :test new-test :next new-next :body new-body) table))) :goto (retok (stmt-fix stmt) (dimb-table-fix table)) :continue (retok (stmt-fix stmt) (dimb-table-fix table)) :break (retok (stmt-fix stmt) (dimb-table-fix table)) :return (b* (((erp new-expr? table) (dimb-expr-option stmt.expr? table))) (retok (stmt-return new-expr?) table))))))
Function:
(defun dimb-block-item (item table) (declare (xargs :guard (and (block-itemp item) (dimb-tablep table)))) (let ((__function__ 'dimb-block-item)) (declare (ignorable __function__)) (b* (((reterr) (irr-block-item) (irr-dimb-table))) (block-item-case item :decl (b* (((erp new-decl table) (dimb-decl item.unwrap table))) (retok (block-item-decl new-decl) table)) :stmt (b* (((erp new-stmt table) (dimb-stmt item.unwrap table))) (retok (block-item-stmt new-stmt) table)) :ambig (b* (((erp decl/stmt table) (dimb-amb-decl/stmt item.unwrap table))) (decl/stmt-case decl/stmt :decl (retok (block-item-decl decl/stmt.unwrap) table) :stmt (retok (block-item-stmt (stmt-expr decl/stmt.unwrap)) table)))))))
Function:
(defun dimb-block-item-list (items table) (declare (xargs :guard (and (block-item-listp items) (dimb-tablep table)))) (let ((__function__ 'dimb-block-item-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-dimb-table)) ((when (endp items)) (retok nil (dimb-table-fix table))) ((erp new-item table) (dimb-block-item (car items) table)) ((erp new-items table) (dimb-block-item-list (cdr items) table))) (retok (cons new-item new-items) table))))
Theorem:
(defthm return-type-of-dimb-stmt.new-stmt (b* (((mv acl2::?erp ?new-stmt ?new-table) (dimb-stmt stmt table))) (stmtp new-stmt)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-stmt.new-table (b* (((mv acl2::?erp ?new-stmt ?new-table) (dimb-stmt stmt table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-block-item.new-item (b* (((mv acl2::?erp ?new-item ?new-table) (dimb-block-item item table))) (block-itemp new-item)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-block-item.new-table (b* (((mv acl2::?erp ?new-item ?new-table) (dimb-block-item item table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-block-item-list.new-items (b* (((mv acl2::?erp ?new-items ?new-table) (dimb-block-item-list items table))) (block-item-listp new-items)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dimb-block-item-list.new-table (b* (((mv acl2::?erp ?new-items ?new-table) (dimb-block-item-list items table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm dimb-stmt-of-stmt-fix-stmt (equal (dimb-stmt (stmt-fix stmt) table) (dimb-stmt stmt table)))
Theorem:
(defthm dimb-stmt-of-dimb-table-fix-table (equal (dimb-stmt stmt (dimb-table-fix table)) (dimb-stmt stmt table)))
Theorem:
(defthm dimb-block-item-of-block-item-fix-item (equal (dimb-block-item (block-item-fix item) table) (dimb-block-item item table)))
Theorem:
(defthm dimb-block-item-of-dimb-table-fix-table (equal (dimb-block-item item (dimb-table-fix table)) (dimb-block-item item table)))
Theorem:
(defthm dimb-block-item-list-of-block-item-list-fix-items (equal (dimb-block-item-list (block-item-list-fix items) table) (dimb-block-item-list items table)))
Theorem:
(defthm dimb-block-item-list-of-dimb-table-fix-table (equal (dimb-block-item-list items (dimb-table-fix table)) (dimb-block-item-list items table)))
Theorem:
(defthm dimb-stmt-stmt-equiv-congruence-on-stmt (implies (stmt-equiv stmt stmt-equiv) (equal (dimb-stmt stmt table) (dimb-stmt stmt-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-stmt-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-stmt stmt table) (dimb-stmt stmt table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-block-item-block-item-equiv-congruence-on-item (implies (block-item-equiv item item-equiv) (equal (dimb-block-item item table) (dimb-block-item item-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-block-item-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-block-item item table) (dimb-block-item item table-equiv))) :rule-classes :congruence)
Theorem:
(defthm dimb-block-item-list-block-item-list-equiv-congruence-on-items (implies (block-item-list-equiv items items-equiv) (equal (dimb-block-item-list items table) (dimb-block-item-list items-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-block-item-list-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-block-item-list items table) (dimb-block-item-list items table-equiv))) :rule-classes :congruence)
Theorem:
(defthm stmt-unambp-of-dimb-stmt (b* (((mv acl2::?erp ?new-stmt ?new-table) (dimb-stmt stmt table))) (implies (not erp) (stmt-unambp new-stmt))))
Theorem:
(defthm block-item-unambp-of-dimb-block-item (b* (((mv acl2::?erp ?new-item ?new-table) (dimb-block-item item table))) (implies (not erp) (block-item-unambp new-item))))
Theorem:
(defthm block-item-list-unambp-of-dimb-block-item-list (b* (((mv acl2::?erp ?new-items ?new-table) (dimb-block-item-list items table))) (implies (not erp) (block-item-list-unambp new-items))))