		Search-engine friendly clone of the ACL2 documentation.

Execution

Pop-vcscope-dinfo

Pop information about a variable and constant scope off the scope stack of the top call of a dynamic environment.

Signature
(pop-vcscope-dinfo env) → new-env
Arguments: env — Guard (denvp env).
Returns: new-env — Type (denv-resultp new-env).

Definitions and Theorems

Function: pop-vcscope-dinfo

(defun pop-vcscope-dinfo (env)
  (declare (xargs :guard (denvp env)))
  (let ((__function__ 'pop-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))
         ((when (endp scopes))
          (reserrf :empty-scope-stack))
         (new-scopes (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-resultp-of-pop-vcscope-dinfo

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

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

(defthm pop-vcscope-dinfo-of-denv-fix-env
  (equal (pop-vcscope-dinfo (denv-fix env))
         (pop-vcscope-dinfo env)))

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

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