Disambiguate an initializer declarator.
(dimb-initdeclor ideclor kind table) → (mv erp new-ideclor new-table)
An initializer declarator is part of a declaration. At the end of the initializer declarator, the declared identifier is added to the disambiguation table, with the appropriate kind, which comes from the preceding declaration specifiers, and is passed to this function.
We pass
Function:
(defun dimb-initdeclor (ideclor kind table) (declare (xargs :guard (and (initdeclorp ideclor) (dimb-kindp kind) (dimb-tablep table)))) (let ((__function__ 'dimb-initdeclor)) (declare (ignorable __function__)) (b* (((reterr) (irr-initdeclor) (irr-dimb-table)) ((initdeclor ideclor) ideclor) ((erp new-declor ident table) (dimb-declor ideclor.declor nil table)) ((erp new-init? table) (dimb-initer-option ideclor.init? table)) (table (dimb-add-ident ident kind table) )) (retok (make-initdeclor :declor new-declor :init? new-init?) table))))
Theorem:
(defthm initdeclorp-of-dimb-initdeclor.new-ideclor (b* (((mv acl2::?erp ?new-ideclor ?new-table) (dimb-initdeclor ideclor kind table))) (initdeclorp new-ideclor)) :rule-classes :rewrite)
Theorem:
(defthm dimb-tablep-of-dimb-initdeclor.new-table (b* (((mv acl2::?erp ?new-ideclor ?new-table) (dimb-initdeclor ideclor kind table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm initdeclor-unambp-of-dimb-initdeclor (b* (((mv acl2::?erp ?new-ideclor ?new-table) (dimb-initdeclor ideclor kind table))) (implies (not erp) (initdeclor-unambp new-ideclor))))
Theorem:
(defthm dimb-initdeclor-of-initdeclor-fix-ideclor (equal (dimb-initdeclor (initdeclor-fix ideclor) kind table) (dimb-initdeclor ideclor kind table)))
Theorem:
(defthm dimb-initdeclor-initdeclor-equiv-congruence-on-ideclor (implies (initdeclor-equiv ideclor ideclor-equiv) (equal (dimb-initdeclor ideclor kind table) (dimb-initdeclor ideclor-equiv kind table))) :rule-classes :congruence)
Theorem:
(defthm dimb-initdeclor-of-dimb-kind-fix-kind (equal (dimb-initdeclor ideclor (dimb-kind-fix kind) table) (dimb-initdeclor ideclor kind table)))
Theorem:
(defthm dimb-initdeclor-dimb-kind-equiv-congruence-on-kind (implies (dimb-kind-equiv kind kind-equiv) (equal (dimb-initdeclor ideclor kind table) (dimb-initdeclor ideclor kind-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-initdeclor-of-dimb-table-fix-table (equal (dimb-initdeclor ideclor kind (dimb-table-fix table)) (dimb-initdeclor ideclor kind table)))
Theorem:
(defthm dimb-initdeclor-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-initdeclor ideclor kind table) (dimb-initdeclor ideclor kind table-equiv))) :rule-classes :congruence)