		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Find-fun

Find a function in the function environment by name.

Signature
(find-fun fun funenv) → info
Arguments: fun — Guard (identifierp fun).; funenv — Guard (funenvp funenv).
Returns: info — Type (funinfo+funenv-resultp info).

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 fun, we return not only its information, but also the current function environment, which is the initial function environment with zero or more scopes popped; the scope where fun is found is not popped, i.e. it is returned as the top scope. This resulting function environment represents the functions in scope for fun. In exec-function, which takes a fun as argument, we call find-fun to retrieve the information about fun so that we can execute its body: thus, it is convenient for find-fun to return the function environment for fun, which must be indeed passed to exec-block on the fun's body.

It is an error if fun is not found in the environment.

Definitions and Theorems

Function: find-fun

(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::assoc (identifier-fix fun)
                                funscope))
         ((when (consp fun+info))
          (make-funinfo+funenv :info (cdr fun+info)
                               :env funenv)))
      (find-fun fun (cdr funenv)))))

Theorem: funinfo+funenv-resultp-of-find-fun

(defthm funinfo+funenv-resultp-of-find-fun
  (b* ((info (find-fun fun funenv)))
    (funinfo+funenv-resultp info))
  :rule-classes :rewrite)

Theorem: error-info-wfp-of-find-fun

(defthm error-info-wfp-of-find-fun
  (b* ((fty::?info (find-fun fun funenv)))
    (implies (reserrp info)
             (error-info-wfp info))))

Theorem: find-fun-of-identifier-fix-fun

(defthm find-fun-of-identifier-fix-fun
  (equal (find-fun (identifier-fix fun) funenv)
         (find-fun fun funenv)))

Theorem: find-fun-identifier-equiv-congruence-on-fun

(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)

Theorem: find-fun-of-funenv-fix-funenv

(defthm find-fun-of-funenv-fix-funenv
  (equal (find-fun fun (funenv-fix funenv))
         (find-fun fun funenv)))

Theorem: find-fun-funenv-equiv-congruence-on-funenv

(defthm find-fun-funenv-equiv-congruence-on-funenv
  (implies (funenv-equiv funenv funenv-equiv)
           (equal (find-fun fun funenv)
                  (find-fun fun funenv-equiv)))
  :rule-classes :congruence)