		Search-engine friendly clone of the ACL2 documentation.

Frame-and-scope-peeling

Peel-scopes

Peel scopes from the computation state.

Signature
(peel-scopes m compst) → new-compst
Arguments: m — Guard (natp m).; compst — Guard (compustatep compst).
Returns: new-compst — Type (compustatep new-compst).

We exit m scopes, but we stop earlier if we run out of scopes; note that a frame must always contain at least one scope, so we stop when one scope is left. The scopes are in the top frame; if there are no frames, this function does nothing.

We prove theorems about how this function interacts with creating variables and with writing objects. Some of these theorems generalize similar ones for exit-scope.

Definitions and Theorems

Function: peel-scopes

(defun peel-scopes (m compst)
  (declare (xargs :guard (and (natp m) (compustatep compst))))
  (cond ((zp m) (compustate-fix compst))
        ((= (compustate-frames-number compst) 0)
         (compustate-fix compst))
        ((= (compustate-top-frame-scopes-number compst)
            1)
         (compustate-fix compst))
        (t (peel-scopes (1- m)
                        (exit-scope compst)))))

Theorem: compustatep-of-peel-scopes

(defthm compustatep-of-peel-scopes
  (b* ((new-compst (peel-scopes m compst)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: peel-scopes-of-not-zp-unfold

(defthm peel-scopes-of-not-zp-unfold
  (implies (and (> (compustate-frames-number compst) 0)
                (> (compustate-top-frame-scopes-number compst)
                   1)
                (not (zp m)))
           (equal (peel-scopes m compst)
                  (peel-scopes (1- m)
                               (exit-scope compst)))))

Theorem: peel-scopes-of-create-var

(defthm peel-scopes-of-create-var
  (b* ((compst1 (create-var var val compst)))
    (implies (and (> (compustate-frames-number compst) 0)
                  (> (compustate-top-frame-scopes-number compst)
                     1)
                  (not (errorp compst1))
                  (not (zp m)))
             (equal (peel-scopes m compst1)
                    (peel-scopes m compst)))))

Theorem: peel-scopes-one-scope-unfold

(defthm peel-scopes-one-scope-unfold
  (implies (and (not (zp m))
                (equal (compustate-top-frame-scopes-number compst)
                       1))
           (equal (peel-scopes m compst)
                  (compustate-fix compst))))

Theorem: peel-scopes-of-exit-scope-fold

(defthm peel-scopes-of-exit-scope-fold
  (implies (and (> (compustate-frames-number compst) 0)
                (> (compustate-top-frame-scopes-number compst)
                   1))
           (equal (peel-scopes m (exit-scope compst))
                  (peel-scopes (1+ (nfix m)) compst))))

Theorem: peel-scopes-of-write-object

(defthm peel-scopes-of-write-object
 (implies
  (not (errorp (write-object objdes val compst)))
  (equal
    (peel-scopes m (write-object objdes val compst))
    (if (and (objdesign-case (objdesign-top objdes)
                             :auto)
             (equal (objdesign-auto->frame (objdesign-top objdes))
                    (1- (compustate-frames-number compst)))
             (>= (objdesign-auto->scope (objdesign-top objdes))
                 (if (< (nfix m)
                        (compustate-top-frame-scopes-number compst))
                     (- (compustate-top-frame-scopes-number compst)
                        (nfix m))
                   1)))
        (peel-scopes m compst)
      (write-object objdes val (peel-scopes m compst))))))

Theorem: not-errorp-of-write-object-of-peel-scopes

(defthm not-errorp-of-write-object-of-peel-scopes
 (implies
  (and
      (or (member-equal (objdesign-kind (objdesign-top objdes))
                        '(:static :alloc))
          (not (equal (objdesign-auto->frame (objdesign-top objdes))
                      (1- (compustate-frames-number compst))))
          (< (objdesign-auto->scope (objdesign-top objdes))
             (if (< (nfix m)
                    (compustate-top-frame-scopes-number compst))
                 (- (compustate-top-frame-scopes-number compst)
                    (nfix m))
               1)))
      (not (errorp (write-object objdes val compst))))
  (not (errorp (write-object objdes val (peel-scopes m compst))))))

Theorem: peel-scopes-of-nfix-m

(defthm peel-scopes-of-nfix-m
  (equal (peel-scopes (nfix m) compst)
         (peel-scopes m compst)))

Theorem: peel-scopes-nat-equiv-congruence-on-m

(defthm peel-scopes-nat-equiv-congruence-on-m
  (implies (acl2::nat-equiv m m-equiv)
           (equal (peel-scopes m compst)
                  (peel-scopes m-equiv compst)))
  :rule-classes :congruence)

Theorem: peel-scopes-of-compustate-fix-compst

(defthm peel-scopes-of-compustate-fix-compst
  (equal (peel-scopes m (compustate-fix compst))
         (peel-scopes m compst)))

Theorem: peel-scopes-compustate-equiv-congruence-on-compst

(defthm peel-scopes-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (peel-scopes m compst)
                  (peel-scopes m compst-equiv)))
  :rule-classes :congruence)