		Search-engine friendly clone of the ACL2 documentation.

Frame-and-scope-peeling

Peel-frames

Peel frames from the computation state.

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

We pop n frames, but we stop earlier if we run out of frames.

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

Definitions and Theorems

Function: peel-frames

(defun peel-frames (n compst)
  (declare (xargs :guard (and (natp n) (compustatep compst))))
  (cond ((zp n) (compustate-fix compst))
        ((= (compustate-frames-number compst) 0)
         (compustate-fix compst))
        (t (peel-frames (1- n)
                        (pop-frame compst)))))

Theorem: compustatep-of-peel-frames

(defthm compustatep-of-peel-frames
  (b* ((new-compst (peel-frames n compst)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: peel-frames-of-create-var

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

Theorem: peel-frames-of-exit-scope

(defthm peel-frames-of-exit-scope
  (implies (and (not (zp n))
                (> (compustate-frames-number compst) 0))
           (equal (peel-frames n (exit-scope compst))
                  (peel-frames n compst))))

Theorem: peel-frames-of-pop-frame-fold

(defthm peel-frames-of-pop-frame-fold
  (implies (> (compustate-frames-number compst) 0)
           (equal (peel-frames n (pop-frame compst))
                  (peel-frames (1+ (nfix n)) compst))))

Theorem: peel-frames-of-write-object

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

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

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

Theorem: peel-frames-of-nfix-n

(defthm peel-frames-of-nfix-n
  (equal (peel-frames (nfix n) compst)
         (peel-frames n compst)))

Theorem: peel-frames-nat-equiv-congruence-on-n

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

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

(defthm peel-frames-of-compustate-fix-compst
  (equal (peel-frames n (compustate-fix compst))
         (peel-frames n compst)))

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

(defthm peel-frames-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (peel-frames n compst)
                  (peel-frames n compst-equiv)))
  :rule-classes :congruence)