		Search-engine friendly clone of the ACL2 documentation.

Execution

Extend-denv-with-structdecl

Extend a dynamic environment with a struct declaration.

Signature
(extend-denv-with-structdecl decl env) → new-env
Arguments: decl — Guard (structdeclp decl).; env — Guard (denvp env).
Returns: new-env — Type (denv-resultp new-env).

Information about the struct type is added to the dynamic struct environment, unless a struct type with that name is already present.

Definitions and Theorems

Function: extend-denv-with-structdecl

(defun extend-denv-with-structdecl (decl env)
  (declare (xargs :guard (and (structdeclp decl) (denvp env))))
  (let ((__function__ 'extend-denv-with-structdecl))
    (declare (ignorable __function__))
    (b* (((structdecl decl) decl)
         ((okf comps)
          (extend-type-map-with-compdecl-list decl.components nil))
         (info (make-struct-dinfo :components comps))
         (cenv (denv->structs env))
         (new-cenv (add-struct-dinfo decl.name info cenv))
         ((when (struct-denv-option-case new-cenv :none))
          (reserrf (list :duplicate-struct decl.name)))
         (new-cenv (struct-denv-option-some->get new-cenv))
         (new-env (change-denv env :structs new-cenv)))
      new-env)))

Theorem: denv-resultp-of-extend-denv-with-structdecl

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

Theorem: extend-denv-with-structdecl-of-structdecl-fix-decl

(defthm extend-denv-with-structdecl-of-structdecl-fix-decl
  (equal (extend-denv-with-structdecl (structdecl-fix decl)
                                      env)
         (extend-denv-with-structdecl decl env)))

Theorem: extend-denv-with-structdecl-structdecl-equiv-congruence-on-decl

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

Theorem: extend-denv-with-structdecl-of-denv-fix-env

(defthm extend-denv-with-structdecl-of-denv-fix-env
  (equal (extend-denv-with-structdecl decl (denv-fix env))
         (extend-denv-with-structdecl decl env)))

Theorem: extend-denv-with-structdecl-denv-equiv-congruence-on-env

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