Look up a function in a function table.
(get-funtype name funtab) → funty?
The lookup is by name. If a function is found, we return its type. Otherwise we return an error.
Function:
(defun get-funtype (name funtab) (declare (xargs :guard (and (identifierp name) (funtablep funtab)))) (let ((__function__ 'get-funtype)) (declare (ignorable __function__)) (b* ((pair (omap::assoc (identifier-fix name) (funtable-fix funtab)))) (if (consp pair) (cdr pair) (reserrf (list :function-not-found (identifier-fix name)))))))
Theorem:
(defthm funtype-resultp-of-get-funtype (b* ((funty? (get-funtype name funtab))) (funtype-resultp funty?)) :rule-classes :rewrite)
Theorem:
(defthm get-funtype-of-identifier-fix-name (equal (get-funtype (identifier-fix name) funtab) (get-funtype name funtab)))
Theorem:
(defthm get-funtype-identifier-equiv-congruence-on-name (implies (identifier-equiv name name-equiv) (equal (get-funtype name funtab) (get-funtype name-equiv funtab))) :rule-classes :congruence)
Theorem:
(defthm get-funtype-of-funtable-fix-funtab (equal (get-funtype name (funtable-fix funtab)) (get-funtype name funtab)))
Theorem:
(defthm get-funtype-funtable-equiv-congruence-on-funtab (implies (funtable-equiv funtab funtab-equiv) (equal (get-funtype name funtab) (get-funtype name funtab-equiv))) :rule-classes :congruence)