		Search-engine friendly clone of the ACL2 documentation.

Computation-states

Enter-scope

Enter a scope.

Signature
(enter-scope compst) → new-compst
Arguments: compst — Guard (compustatep compst).
Returns: new-compst — Type (compustatep new-compst).

We push an empty scope onto the scope stack of the top frame.

Definitions and Theorems

Function: enter-scope

(defun enter-scope (compst)
  (declare (xargs :guard (compustatep compst)))
  (declare (xargs :guard (> (compustate-frames-number compst)
                            0)))
  (let ((__function__ 'enter-scope))
    (declare (ignorable __function__))
    (b* ((frame (top-frame compst))
         (scopes (frame->scopes frame))
         (new-scopes (cons nil scopes))
         (new-frame (change-frame frame :scopes new-scopes))
         (new-compst (push-frame new-frame (pop-frame compst))))
      new-compst)))

Theorem: compustatep-of-enter-scope

(defthm compustatep-of-enter-scope
  (b* ((new-compst (enter-scope compst)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: compustate-frames-number-of-enter-scope

(defthm compustate-frames-number-of-enter-scope
  (implies (> (compustate-frames-number compst) 0)
           (b* ((?new-compst (enter-scope compst)))
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-scopes-numbers-of-enter-scope

(defthm compustate-scopes-numbers-of-enter-scope
  (implies
       (> (compustate-frames-number compst) 0)
       (b* ((?new-compst (enter-scope compst)))
         (equal (compustate-scopes-numbers new-compst)
                (cons (1+ (car (compustate-scopes-numbers compst)))
                      (cdr (compustate-scopes-numbers compst)))))))

Theorem: enter-scope-of-compustate-fix-compst

(defthm enter-scope-of-compustate-fix-compst
  (equal (enter-scope (compustate-fix compst))
         (enter-scope compst)))

Theorem: enter-scope-compustate-equiv-congruence-on-compst

(defthm enter-scope-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (enter-scope compst)
                  (enter-scope compst-equiv)))
  :rule-classes :congruence)