		Search-engine friendly clone of the ACL2 documentation.

Dynamic-environments

Add-var/const-dinfo-to-scope

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

Signature
(add-var/const-dinfo-to-scope name info scope) → new-scope
Arguments: name — Guard (identifierp name).; info — Guard (var/const-dinfop info).; scope — Guard (vcscope-dinfop scope).
Returns: new-scope — Type (vcscope-dinfop new-scope).

This is used after checking that the variable or constant is indeed new. We should probably add a guard to that effect here.

Definitions and Theorems

Function: add-var/const-dinfo-to-scope

(defun add-var/const-dinfo-to-scope (name info scope)
  (declare (xargs :guard (and (identifierp name)
                              (var/const-dinfop info)
                              (vcscope-dinfop scope))))
  (let ((__function__ 'add-var/const-dinfo-to-scope))
    (declare (ignorable __function__))
    (omap::update (identifier-fix name)
                  (var/const-dinfo-fix info)
                  (vcscope-dinfo-fix scope))))

Theorem: vcscope-dinfop-of-add-var/const-dinfo-to-scope

(defthm vcscope-dinfop-of-add-var/const-dinfo-to-scope
  (b* ((new-scope (add-var/const-dinfo-to-scope name info scope)))
    (vcscope-dinfop new-scope))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

Theorem: add-var/const-dinfo-to-scope-of-vcscope-dinfo-fix-scope

(defthm add-var/const-dinfo-to-scope-of-vcscope-dinfo-fix-scope
 (equal
  (add-var/const-dinfo-to-scope name info (vcscope-dinfo-fix scope))
  (add-var/const-dinfo-to-scope name info scope)))

Theorem: add-var/const-dinfo-to-scope-vcscope-dinfo-equiv-congruence-on-scope

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