Add an identifier and its kind to the disambiguation table.
(dimb-add-ident ident kind table) → new-table
It is an internal error if the table is empty; it should never be empty. We should replace this with guards and proofs.
We add the identifier to the innermost (i.e. top) scope. If the identifier is already in the innermost scope, we override its mapping with the new one. This is necessary to handle re-declarations of the same identifier, which are allowed under suitable conditions; in particular, the kind of the identifier should not change. But we override the mapping unconditionally, even if the new kind differs from the old kind: this situation should only happen with invalid code, in which case it does not matter how we disambiguate it exactly.
Function:
(defun dimb-add-ident (ident kind table) (declare (xargs :guard (and (identp ident) (dimb-kindp kind) (dimb-tablep table)))) (let ((__function__ 'dimb-add-ident)) (declare (ignorable __function__)) (b* (((when (endp table)) (raise "Internal error: empty disambiguation table.")) (scope (dimb-scope-fix (car table))) (new-scope (acons (ident-fix ident) (dimb-kind-fix kind) scope)) (new-table (cons new-scope (cdr table)))) (dimb-table-fix new-table))))
Theorem:
(defthm dimb-tablep-of-dimb-add-ident (b* ((new-table (dimb-add-ident ident kind table))) (dimb-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm dimb-add-ident-of-ident-fix-ident (equal (dimb-add-ident (ident-fix ident) kind table) (dimb-add-ident ident kind table)))
Theorem:
(defthm dimb-add-ident-ident-equiv-congruence-on-ident (implies (ident-equiv ident ident-equiv) (equal (dimb-add-ident ident kind table) (dimb-add-ident ident-equiv kind table))) :rule-classes :congruence)
Theorem:
(defthm dimb-add-ident-of-dimb-kind-fix-kind (equal (dimb-add-ident ident (dimb-kind-fix kind) table) (dimb-add-ident ident kind table)))
Theorem:
(defthm dimb-add-ident-dimb-kind-equiv-congruence-on-kind (implies (dimb-kind-equiv kind kind-equiv) (equal (dimb-add-ident ident kind table) (dimb-add-ident ident kind-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-add-ident-of-dimb-table-fix-table (equal (dimb-add-ident ident kind (dimb-table-fix table)) (dimb-add-ident ident kind table)))
Theorem:
(defthm dimb-add-ident-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-add-ident ident kind table) (dimb-add-ident ident kind table-equiv))) :rule-classes :congruence)