Exit a scope.
(exit-scope compst) → new-compst
We pop the scope stack of the top frame.
Function:
(defun exit-scope (compst) (declare (xargs :guard (compustatep compst))) (declare (xargs :guard (and (> (compustate-frames-number compst) 0) (> (compustate-top-frame-scopes-number compst) 1)))) (let ((__function__ 'exit-scope)) (declare (ignorable __function__)) (b* ((frame (top-frame compst)) (scopes (frame->scopes frame)) (new-scopes (cdr scopes)) (new-frame (change-frame frame :scopes new-scopes)) (new-compst (push-frame new-frame (pop-frame compst)))) new-compst)))
Theorem:
(defthm compustatep-of-exit-scope (b* ((new-compst (exit-scope compst))) (compustatep new-compst)) :rule-classes :rewrite)
Theorem:
(defthm compustate-frames-number-of-exit-scope (implies (> (compustate-frames-number compst) 0) (b* nil (equal (compustate-frames-number (exit-scope compst)) (compustate-frames-number compst)))))
Theorem:
(defthm compustate-scopes-numbers-of-exit-scope (implies (and (> (compustate-frames-number compst) 0) (> (compustate-top-frame-scopes-number compst) 1)) (b* ((?new-compst (exit-scope compst))) (equal (compustate-scopes-numbers new-compst) (cons (1- (car (compustate-scopes-numbers compst))) (cdr (compustate-scopes-numbers compst)))))))
Theorem:
(defthm exit-scope-of-compustate-fix-compst (equal (exit-scope (compustate-fix compst)) (exit-scope compst)))
Theorem:
(defthm exit-scope-compustate-equiv-congruence-on-compst (implies (compustate-equiv compst compst-equiv) (equal (exit-scope compst) (exit-scope compst-equiv))) :rule-classes :congruence)