		Search-engine friendly clone of the ACL2 documentation.

Type-checking

Extend-senv-with-fundecl

Extend a static environment with a function declaration.

Signature
(extend-senv-with-fundecl decl env) → new-env
Arguments: decl — Guard (fundeclp decl).; env — Guard (senvp env).
Returns: new-env — Type (senv-resultp new-env).

We add an entry for the function, if possible. We ignore the body of the function

This does not type-check the function declaration. It just incorporates it into the environment.

Definitions and Theorems

Function: extend-senv-with-fundecl

(defun extend-senv-with-fundecl (decl env)
 (declare (xargs :guard (and (fundeclp decl) (senvp env))))
 (let ((__function__ 'extend-senv-with-fundecl))
   (declare (ignorable __function__))
   (b* (((fundecl decl) decl)
        (inputs (funparam-list-to-var/const-sinfo-list decl.inputs))
        (output decl.output)
        (info (make-function-sinfo :inputs inputs
                                   :output output))
        (new-env (add-function-sinfo decl.name info env))
        ((unless new-env)
         (reserrf (list :cannot-add-function
                        decl.name (senv-fix env)))))
     new-env)))

Theorem: senv-resultp-of-extend-senv-with-fundecl

(defthm senv-resultp-of-extend-senv-with-fundecl
  (b* ((new-env (extend-senv-with-fundecl decl env)))
    (senv-resultp new-env))
  :rule-classes :rewrite)

Theorem: extend-senv-with-fundecl-of-fundecl-fix-decl

(defthm extend-senv-with-fundecl-of-fundecl-fix-decl
  (equal (extend-senv-with-fundecl (fundecl-fix decl)
                                   env)
         (extend-senv-with-fundecl decl env)))

Theorem: extend-senv-with-fundecl-fundecl-equiv-congruence-on-decl

(defthm extend-senv-with-fundecl-fundecl-equiv-congruence-on-decl
  (implies (fundecl-equiv decl decl-equiv)
           (equal (extend-senv-with-fundecl decl env)
                  (extend-senv-with-fundecl decl-equiv env)))
  :rule-classes :congruence)

Theorem: extend-senv-with-fundecl-of-senv-fix-env

(defthm extend-senv-with-fundecl-of-senv-fix-env
  (equal (extend-senv-with-fundecl decl (senv-fix env))
         (extend-senv-with-fundecl decl env)))

Theorem: extend-senv-with-fundecl-senv-equiv-congruence-on-env

(defthm extend-senv-with-fundecl-senv-equiv-congruence-on-env
  (implies (senv-equiv env env-equiv)
           (equal (extend-senv-with-fundecl decl env)
                  (extend-senv-with-fundecl decl env-equiv)))
  :rule-classes :congruence)