		Search-engine friendly clone of the ACL2 documentation.

Type-checking

Extend-senv-with-vardecl

Extend a static environment with a variable declaration.

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

We add an entry for the variable, if possible. We ignore the initializing expression.

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

Definitions and Theorems

Function: extend-senv-with-vardecl

(defun extend-senv-with-vardecl (decl env)
  (declare (xargs :guard (and (vardeclp decl) (senvp env))))
  (let ((__function__ 'extend-senv-with-vardecl))
    (declare (ignorable __function__))
    (b* (((vardecl decl) decl)
         (info (make-var/const-sinfo :type decl.type
                                     :constp nil))
         (new-env (add-var/const-sinfo decl.name info env))
         ((unless new-env)
          (reserrf (list :cannot-add-variable
                         decl.name (senv-fix env)))))
      new-env)))

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

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

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

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

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

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

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

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

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

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