		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-reader

Punread-chars

Unread a specified number of characters during preprocessing.

Signature
(punread-chars n ppstate) → new-ppstate
Arguments: n — Guard (natp n).; ppstate — Guard (ppstatep ppstate).
Returns: new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).

We move characters from the sequence of read characters to the sequence of unread characters by incrementing the number of unread characters by n and decrementing the number of read characters by n.

It is an internal error if n exceeds the number of character read so far. In this case, after raising the hard error, logically we return a preprocessing state where we still increment chars-unread so that the theorem about ppstate->size holds unconditionally.

Definitions and Theorems

Function: punread-chars

(defun punread-chars (n ppstate)
 (declare (xargs :stobjs (ppstate)))
 (declare (xargs :guard (and (natp n) (ppstatep ppstate))))
 (let ((__function__ 'punread-chars))
  (declare (ignorable __function__))
  (b*
   ((n (nfix n))
    (chars-read (ppstate->chars-read ppstate))
    (chars-unread (ppstate->chars-unread ppstate))
    (size (ppstate->size ppstate))
    ((unless (<= n chars-read))
     (raise
      "Internal error: ~
                attempting to unread ~x0 characters ~
                from ~x1 read characters."
      n chars-read)
     (b* ((ppstate (update-ppstate->chars-unread (+ chars-unread n)
                                                 ppstate))
          (ppstate (update-ppstate->size (+ size n)
                                         ppstate)))
       ppstate))
    (new-chars-read (- chars-read n))
    (new-chars-unread (+ chars-unread n))
    (new-size (+ size n))
    (ppstate (update-ppstate->chars-read new-chars-read ppstate))
    (ppstate
         (update-ppstate->chars-unread new-chars-unread ppstate))
    (ppstate (update-ppstate->size new-size ppstate)))
   ppstate)))

Theorem: ppstatep-of-punread-chars

(defthm ppstatep-of-punread-chars
  (implies (ppstatep ppstate)
           (b* ((new-ppstate (punread-chars n ppstate)))
             (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: ppstate->size-of-punread-chars

(defthm ppstate->size-of-punread-chars
  (b* ((?new-ppstate (punread-chars n ppstate)))
    (equal (ppstate->size new-ppstate)
           (+ (ppstate->size ppstate) (nfix n)))))

Theorem: punread-chars-of-nfix-n

(defthm punread-chars-of-nfix-n
  (equal (punread-chars (nfix n) ppstate)
         (punread-chars n ppstate)))

Theorem: punread-chars-nat-equiv-congruence-on-n

(defthm punread-chars-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (punread-chars n ppstate)
                  (punread-chars n-equiv ppstate)))
  :rule-classes :congruence)

Theorem: punread-chars-of-ppstate-fix-ppstate

(defthm punread-chars-of-ppstate-fix-ppstate
  (equal (punread-chars n (ppstate-fix ppstate))
         (punread-chars n ppstate)))

Theorem: punread-chars-ppstate-equiv-congruence-on-ppstate

(defthm punread-chars-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (punread-chars n ppstate)
                  (punread-chars n ppstate-equiv)))
  :rule-classes :congruence)