		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-reader

Punread-char

Unread a character during preprocessing.

Signature
(punread-char ppstate) → new-ppstate
Arguments: ppstate — Guard (ppstatep ppstate).
Returns: new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).

We move the character from the sequence of read characters to the sequence of unread characters, by incrementing chars-unread and decrementing chars-read.

It is an internal error if chars-read is 0. It means that the calling code is wrong. 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-char

(defun punread-char (ppstate)
 (declare (xargs :stobjs (ppstate)))
 (declare (xargs :guard (ppstatep ppstate)))
 (let ((__function__ 'punread-char))
  (declare (ignorable __function__))
  (b*
   ((ppstate.chars-read (ppstate->chars-read ppstate))
    (ppstate.chars-unread (ppstate->chars-unread ppstate))
    (ppstate.size (ppstate->size ppstate))
    ((unless (> ppstate.chars-read 0))
     (raise "Internal error: no character to unread.")
     (b*
      ((ppstate
            (update-ppstate->chars-unread (1+ ppstate.chars-unread)
                                          ppstate))
       (ppstate (update-ppstate->size (1+ ppstate.size)
                                      ppstate)))
      ppstate))
    (ppstate (update-ppstate->chars-read (1- ppstate.chars-read)
                                         ppstate))
    (ppstate (update-ppstate->chars-unread (1+ ppstate.chars-unread)
                                           ppstate))
    (ppstate (update-ppstate->size (1+ ppstate.size)
                                   ppstate)))
   ppstate)))

Theorem: ppstatep-of-punread-char

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

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

(defthm ppstate->size-of-punread-char
  (b* ((?new-ppstate (punread-char ppstate)))
    (equal (ppstate->size new-ppstate)
           (1+ (ppstate->size ppstate)))))

Theorem: punread-char-of-ppstate-fix-ppstate

(defthm punread-char-of-ppstate-fix-ppstate
  (equal (punread-char (ppstate-fix ppstate))
         (punread-char ppstate)))

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

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