Find a function in the function environment by name.
We search through the scopes, from innermost to outermost. It is an expected invariant that the scopes in a function environment have disjoint function names (we may formalize and prove this invariant at some point): thus, the search order would not matter if we only needed the function information; however, as explained below, we also return a function environment, and therefore the innermost-to-outermost search order is important.
If we find
It is an error if
(defun find-fun (fun funenv) (declare (xargs :guard (and (identifierp fun) (funenvp funenv)))) (let ((__function__ 'find-fun)) (declare (ignorable __function__)) (b* (((when (endp funenv)) (reserrf (list :function-not-found (identifier-fix fun)))) (funscope (funscope-fix (car funenv))) (fun+info (omap::in (identifier-fix fun) funscope)) ((when (consp fun+info)) (make-funinfo+funenv :info (cdr fun+info) :env funenv))) (find-fun fun (cdr funenv)))))
(defthm funinfo+funenv-resultp-of-find-fun (b* ((info (find-fun fun funenv))) (funinfo+funenv-resultp info)) :rule-classes :rewrite)
(defthm error-info-wfp-of-find-fun (b* ((fty::?info (find-fun fun funenv))) (implies (reserrp info) (error-info-wfp info))))
(defthm find-fun-of-identifier-fix-fun (equal (find-fun (identifier-fix fun) funenv) (find-fun fun funenv)))
(defthm find-fun-identifier-equiv-congruence-on-fun (implies (identifier-equiv fun fun-equiv) (equal (find-fun fun funenv) (find-fun fun-equiv funenv))) :rule-classes :congruence)
(defthm find-fun-of-funenv-fix-funenv (equal (find-fun fun (funenv-fix funenv)) (find-fun fun funenv)))