		Search-engine friendly clone of the ACL2 documentation.

Dynamic-environments

Add-var/const-dinfo

Add dynamic information about a new variable or constant to a dynamic environment.

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

We return nil when the call stack is empty or when the scope stack of the top call is empty.

Definitions and Theorems

Function: add-var/const-dinfo

(defun add-var/const-dinfo (name info env)
  (declare (xargs :guard (and (identifierp name)
                              (var/const-dinfop info)
                              (denvp env))))
  (let ((__function__ 'add-var/const-dinfo))
    (declare (ignorable __function__))
    (b* ((calls (denv->call-stack env))
         ((when (endp calls)) nil)
         (top-call (car calls))
         (scopes (call-dinfo->scopes top-call))
         ((when (endp scopes)) nil)
         (top-scope (car scopes))
         (new-top-scope
              (add-var/const-dinfo-to-scope name info top-scope))
         (new-scopes (cons new-top-scope (cdr scopes)))
         (new-top-call (change-call-dinfo top-call
                                          :scopes new-scopes))
         (new-calls (cons new-top-call (cdr calls)))
         (new-env (change-denv env
                               :call-stack new-calls)))
      new-env)))

Theorem: denv-optionp-of-add-var/const-dinfo

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

Theorem: add-var/const-dinfo-of-identifier-fix-name

(defthm add-var/const-dinfo-of-identifier-fix-name
  (equal (add-var/const-dinfo (identifier-fix name)
                              info env)
         (add-var/const-dinfo name info env)))

Theorem: add-var/const-dinfo-identifier-equiv-congruence-on-name

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

Theorem: add-var/const-dinfo-of-var/const-dinfo-fix-info

(defthm add-var/const-dinfo-of-var/const-dinfo-fix-info
  (equal (add-var/const-dinfo name (var/const-dinfo-fix info)
                              env)
         (add-var/const-dinfo name info env)))

Theorem: add-var/const-dinfo-var/const-dinfo-equiv-congruence-on-info

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

Theorem: add-var/const-dinfo-of-denv-fix-env

(defthm add-var/const-dinfo-of-denv-fix-env
  (equal (add-var/const-dinfo name info (denv-fix env))
         (add-var/const-dinfo name info env)))

Theorem: add-var/const-dinfo-denv-equiv-congruence-on-env

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