Look up an identifier in the disambiguation table.
(dimb-lookup-ident ident table) → kind?
According the visibility and hiding rules [C:6.2.1/2],
we look up the identifier starting from the innermost scope.
We stop as soon as we find a match.
We return
Function:
(defun dimb-lookup-ident (ident table) (declare (xargs :guard (and (identp ident) (dimb-tablep table)))) (let ((__function__ 'dimb-lookup-ident)) (declare (ignorable __function__)) (b* (((when (endp table)) nil) (scope (dimb-scope-fix (car table))) (ident+kind (assoc-equal (ident-fix ident) scope)) ((when ident+kind) (dimb-kind-fix (cdr ident+kind)))) (dimb-lookup-ident ident (cdr table)))))
Theorem:
(defthm dimb-kind-optionp-of-dimb-lookup-ident (b* ((kind? (dimb-lookup-ident ident table))) (dimb-kind-optionp kind?)) :rule-classes :rewrite)
Theorem:
(defthm dimb-lookup-ident-of-ident-fix-ident (equal (dimb-lookup-ident (ident-fix ident) table) (dimb-lookup-ident ident table)))
Theorem:
(defthm dimb-lookup-ident-ident-equiv-congruence-on-ident (implies (ident-equiv ident ident-equiv) (equal (dimb-lookup-ident ident table) (dimb-lookup-ident ident-equiv table))) :rule-classes :congruence)
Theorem:
(defthm dimb-lookup-ident-of-dimb-table-fix-table (equal (dimb-lookup-ident ident (dimb-table-fix table)) (dimb-lookup-ident ident table)))
Theorem:
(defthm dimb-lookup-ident-dimb-table-equiv-congruence-on-table (implies (dimb-table-equiv table table-equiv) (equal (dimb-lookup-ident ident table) (dimb-lookup-ident ident table-equiv))) :rule-classes :congruence)