		Search-engine friendly clone of the ACL2 documentation.

Dynamic-struct-environments

Add-struct-dinfo

Add information for a struct type to a dynamic environment.

Signature
(add-struct-dinfo name info env) → new-env
Arguments: name — Guard (identifierp name).; info — Guard (struct-dinfop info).; env — Guard (struct-denvp env).
Returns: new-env — Type (struct-denv-optionp new-env).

We return `none' if there is already a struct type with the same nme in the environment.

Definitions and Theorems

Function: add-struct-dinfo

(defun add-struct-dinfo (name info env)
  (declare (xargs :guard (and (identifierp name)
                              (struct-dinfop info)
                              (struct-denvp env))))
  (let ((__function__ 'add-struct-dinfo))
    (declare (ignorable __function__))
    (b* ((name (identifier-fix name))
         (info (struct-dinfo-fix info))
         (env (struct-denv-fix env))
         ((when (consp (omap::assoc name env)))
          (struct-denv-option-none))
         (new-env (omap::update name info env)))
      (struct-denv-option-some new-env))))

Theorem: struct-denv-optionp-of-add-struct-dinfo

(defthm struct-denv-optionp-of-add-struct-dinfo
  (b* ((new-env (add-struct-dinfo name info env)))
    (struct-denv-optionp new-env))
  :rule-classes :rewrite)

Theorem: add-struct-dinfo-of-identifier-fix-name

(defthm add-struct-dinfo-of-identifier-fix-name
  (equal (add-struct-dinfo (identifier-fix name)
                           info env)
         (add-struct-dinfo name info env)))

Theorem: add-struct-dinfo-identifier-equiv-congruence-on-name

(defthm add-struct-dinfo-identifier-equiv-congruence-on-name
  (implies (identifier-equiv name name-equiv)
           (equal (add-struct-dinfo name info env)
                  (add-struct-dinfo name-equiv info env)))
  :rule-classes :congruence)

Theorem: add-struct-dinfo-of-struct-dinfo-fix-info

(defthm add-struct-dinfo-of-struct-dinfo-fix-info
  (equal (add-struct-dinfo name (struct-dinfo-fix info)
                           env)
         (add-struct-dinfo name info env)))

Theorem: add-struct-dinfo-struct-dinfo-equiv-congruence-on-info

(defthm add-struct-dinfo-struct-dinfo-equiv-congruence-on-info
  (implies (struct-dinfo-equiv info info-equiv)
           (equal (add-struct-dinfo name info env)
                  (add-struct-dinfo name info-equiv env)))
  :rule-classes :congruence)

Theorem: add-struct-dinfo-of-struct-denv-fix-env

(defthm add-struct-dinfo-of-struct-denv-fix-env
  (equal (add-struct-dinfo name info (struct-denv-fix env))
         (add-struct-dinfo name info env)))

Theorem: add-struct-dinfo-struct-denv-equiv-congruence-on-env

(defthm add-struct-dinfo-struct-denv-equiv-congruence-on-env
  (implies (struct-denv-equiv env env-equiv)
           (equal (add-struct-dinfo name info env)
                  (add-struct-dinfo name info env-equiv)))
  :rule-classes :congruence)