		Search-engine friendly clone of the ACL2 documentation.

Execution

Push-vcscope-dinfo

Push information about a variable and constant scope onto the scope stack of the top call of a dynamic environment.

Signature
(push-vcscope-dinfo scope env) → new-env
Arguments: scope — Guard (vcscope-dinfop scope).; env — Guard (denvp env).
Returns: new-env — Type (denv-resultp new-env).

Definitions and Theorems

Function: push-vcscope-dinfo

(defun push-vcscope-dinfo (scope env)
  (declare (xargs :guard (and (vcscope-dinfop scope)
                              (denvp env))))
  (let ((__function__ 'push-vcscope-dinfo))
    (declare (ignorable __function__))
    (b* ((calls (denv->call-stack env))
         ((when (endp calls))
          (reserrf :empty-call-stack))
         (top-call (car calls))
         (scopes (call-dinfo->scopes top-call))
         (new-scopes (cons scope 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-resultp-of-push-vcscope-dinfo

(defthm denv-resultp-of-push-vcscope-dinfo
  (b* ((new-env (push-vcscope-dinfo scope env)))
    (denv-resultp new-env))
  :rule-classes :rewrite)

Theorem: push-vcscope-dinfo-of-vcscope-dinfo-fix-scope

(defthm push-vcscope-dinfo-of-vcscope-dinfo-fix-scope
  (equal (push-vcscope-dinfo (vcscope-dinfo-fix scope)
                             env)
         (push-vcscope-dinfo scope env)))

Theorem: push-vcscope-dinfo-vcscope-dinfo-equiv-congruence-on-scope

(defthm push-vcscope-dinfo-vcscope-dinfo-equiv-congruence-on-scope
  (implies (vcscope-dinfo-equiv scope scope-equiv)
           (equal (push-vcscope-dinfo scope env)
                  (push-vcscope-dinfo scope-equiv env)))
  :rule-classes :congruence)

Theorem: push-vcscope-dinfo-of-denv-fix-env

(defthm push-vcscope-dinfo-of-denv-fix-env
  (equal (push-vcscope-dinfo scope (denv-fix env))
         (push-vcscope-dinfo scope env)))

Theorem: push-vcscope-dinfo-denv-equiv-congruence-on-env

(defthm push-vcscope-dinfo-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (push-vcscope-dinfo scope env)
                  (push-vcscope-dinfo scope env-equiv)))
  :rule-classes :congruence)