Disambiguate a declaration.
(dimb-decl decl table) → (mv erp new-decl new-table)
First we process the declaration specifiers,
which, as explained in dimb-declspec,
determine whether the (one or more) identifiers
introduced by the declarators
denote
Function:
(defun dimb-decl (decl table) (declare (xargs :guard (and (declp decl) (dimb-tablep table)))) (let ((__function__ 'dimb-decl)) (declare (ignorable __function__)) (b* (((reterr) (irr-decl) (irr-dimb-table))) (decl-case decl :decl (b* (((erp new-specs kind table) (dimb-declspec-list decl.specs (dimb-kind-objfun) table)) ((erp new-init table) (dimb-initdeclor-list decl.init kind table))) (retok (make-decl-decl :extension decl.extension :specs new-specs :init new-init :asm? decl.asm? :attrib decl.attrib) table)) :statassert (b* (((erp new-statassert table) (dimb-statassert decl.unwrap table))) (retok (decl-statassert new-statassert) table))))))
Theorem:
(defthm declp-of-dimb-decl.new-decl (b* (((mv acl2::?erp ?new-decl ?new-table) (dimb-decl decl table))) (declp new-decl)) :rule-classes :rewrite)
Theorem:
(defthm dimb-tablep-of-dimb-decl.new-table (b* (((mv acl2::?erp ?new-decl ?new-table) (dimb-decl decl table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm decl-unambp-of-dimb-decl (b* (((mv acl2::?erp ?new-decl ?new-table) (dimb-decl decl table))) (implies (not erp) (decl-unambp new-decl))))
Theorem:
(defthm dimb-decl-of-decl-fix-decl (equal (dimb-decl (decl-fix decl) table) (dimb-decl decl table)))
Theorem:
(defthm dimb-decl-decl-equiv-congruence-on-decl (implies (decl-equiv decl decl-equiv) (equal (dimb-decl decl table) (dimb-decl decl-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-decl-of-dimb-table-fix-table (equal (dimb-decl decl (dimb-table-fix table)) (dimb-decl decl table)))
Theorem:
(defthm dimb-decl-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-decl decl table) (dimb-decl decl table-equiv))) :rule-classes :congruence)