Disambiguate an ambiguous declaration or statement.
(dimb-amb-decl/stmt decl/stmt table) → (mv erp decl-or-stmt new-table)
An ambiguous declaration or statement is represented as a pair of a declaration and an expression (with the same concrete syntax appearance); the latter is an expression and not a statement because the statement in question is always an expression statement, and so it suffices to represent the expression. We attempt to disambiguate both the declaration and the expression, independently from each other. In valid code, one of them must succeed and the other one must fail: then we disambiguate in favor of the one that succeeded. If none or both succeed, the code must be invalid.
Function:
(defun dimb-amb-decl/stmt (decl/stmt table) (declare (xargs :guard (and (amb-decl/stmt-p decl/stmt) (dimb-tablep table)))) (let ((__function__ 'dimb-amb-decl/stmt)) (declare (ignorable __function__)) (b* (((reterr) (irr-decl/stmt) (irr-dimb-table)) ((amb-decl/stmt decl/stmt) decl/stmt) ((mv erp-decl new-decl table-decl) (dimb-decl decl/stmt.decl table)) ((mv erp-expr new-expr table-expr) (dimb-expr decl/stmt.stmt table))) (if erp-decl (if erp-expr (reterr (msg "In the ambiguous declaration or statement ~x0, ~ neither the declaration nor the expression ~ can be successfully disambiguated ~ given the current table ~x1. ~ The code must be invalid, ~ because at least one must succeed.~%~%~ These are the failures for each:~%~%~ ~@2~%~%~@3" (amb-decl/stmt-fix decl/stmt) (dimb-table-fix table) erp-decl erp-expr)) (retok (decl/stmt-stmt new-expr) table-expr)) (if erp-expr (retok (decl/stmt-decl new-decl) table-decl) (reterr (msg "In the ambiguous declaration or statement ~x0, ~ both the declaration and the statement ~ are successfully disambiguated ~ given the current table ~x1. ~ The code must be invalid, ~ because at most one must succeed." (amb-decl/stmt-fix decl/stmt) (dimb-table-fix table))))))))
Theorem:
(defthm decl/stmt-p-of-dimb-amb-decl/stmt.decl-or-stmt (b* (((mv acl2::?erp ?decl-or-stmt ?new-table) (dimb-amb-decl/stmt decl/stmt table))) (decl/stmt-p decl-or-stmt)) :rule-classes :rewrite)
Theorem:
(defthm dimb-tablep-of-dimb-amb-decl/stmt.new-table (b* (((mv acl2::?erp ?decl-or-stmt ?new-table) (dimb-amb-decl/stmt decl/stmt table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm decl/stmt-unambp-of-dimb-amb-decl/stmt (b* (((mv acl2::?erp ?decl-or-stmt ?new-table) (dimb-amb-decl/stmt decl/stmt table))) (implies (not erp) (decl/stmt-unambp decl-or-stmt))))
Theorem:
(defthm dimb-amb-decl/stmt-of-amb-decl/stmt-fix-decl/stmt (equal (dimb-amb-decl/stmt (amb-decl/stmt-fix decl/stmt) table) (dimb-amb-decl/stmt decl/stmt table)))
Theorem:
(defthm dimb-amb-decl/stmt-amb-decl/stmt-equiv-congruence-on-decl/stmt (implies (amb-decl/stmt-equiv decl/stmt decl/stmt-equiv) (equal (dimb-amb-decl/stmt decl/stmt table) (dimb-amb-decl/stmt decl/stmt-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-amb-decl/stmt-of-dimb-table-fix-table (equal (dimb-amb-decl/stmt decl/stmt (dimb-table-fix table)) (dimb-amb-decl/stmt decl/stmt table)))
Theorem:
(defthm dimb-amb-decl/stmt-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-amb-decl/stmt decl/stmt table) (dimb-amb-decl/stmt decl/stmt table-equiv))) :rule-classes :congruence)