		Search-engine friendly clone of the ACL2 documentation.

Type-checking

Extend-senv-with-structdecl

Extend a static environment with a struct declaration.

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

First we build a finite map from identifiers to types from the struct component declarations, which we use to build the information about the struct type. Then we add an entry to the static environment for the struct type, unless its name is already in use.

Definitions and Theorems

Function: extend-senv-with-structdecl

(defun extend-senv-with-structdecl (decl env)
  (declare (xargs :guard (and (structdeclp decl) (senvp env))))
  (let ((__function__ 'extend-senv-with-structdecl))
    (declare (ignorable __function__))
    (b* (((structdecl decl) decl)
         ((okf comps)
          (extend-type-map-with-compdecl-list decl.components nil))
         (info (make-struct-sinfo :components comps))
         (new-env (add-struct-sinfo decl.name info env))
         ((unless new-env)
          (reserrf (list :cannot-add-struct
                         decl.name (senv-fix env)))))
      new-env)))

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

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

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

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

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

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

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

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

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

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