		Search-engine friendly clone of the ACL2 documentation.

Static-environments

Get-function-sinfo

Retrieve information about a function from a static environment.

Signature
(get-function-sinfo fun env) → info
Arguments: fun — Guard (identifierp fun).; env — Guard (senvp env).
Returns: info — Type (function-sinfo-optionp info).

We return nil if the function is not found. This includes the case that the identifier is in the environment but it does not refer to a function.

Definitions and Theorems

Function: get-function-sinfo

(defun get-function-sinfo (fun env)
  (declare (xargs :guard (and (identifierp fun) (senvp env))))
  (let ((__function__ 'get-function-sinfo))
    (declare (ignorable __function__))
    (b* ((info (get-ident-sinfo fun env))
         ((unless info) nil))
      (ident-sinfo-case info
                        :var/const nil
                        :function info.get
                        :struct nil))))

Theorem: function-sinfo-optionp-of-get-function-sinfo

(defthm function-sinfo-optionp-of-get-function-sinfo
  (b* ((info (get-function-sinfo fun env)))
    (function-sinfo-optionp info))
  :rule-classes :rewrite)

Theorem: get-function-sinfo-of-identifier-fix-fun

(defthm get-function-sinfo-of-identifier-fix-fun
  (equal (get-function-sinfo (identifier-fix fun)
                             env)
         (get-function-sinfo fun env)))

Theorem: get-function-sinfo-identifier-equiv-congruence-on-fun

(defthm get-function-sinfo-identifier-equiv-congruence-on-fun
  (implies (identifier-equiv fun fun-equiv)
           (equal (get-function-sinfo fun env)
                  (get-function-sinfo fun-equiv env)))
  :rule-classes :congruence)

Theorem: get-function-sinfo-of-senv-fix-env

(defthm get-function-sinfo-of-senv-fix-env
  (equal (get-function-sinfo fun (senv-fix env))
         (get-function-sinfo fun env)))

Theorem: get-function-sinfo-senv-equiv-congruence-on-env

(defthm get-function-sinfo-senv-equiv-congruence-on-env
  (implies (senv-equiv env env-equiv)
           (equal (get-function-sinfo fun env)
                  (get-function-sinfo fun env-equiv)))
  :rule-classes :congruence)