		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Punread-token

Unread a token.

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

We move the token from the sequence of read lexemes to the sequence of unread lexemes.

It is an internal error if lexemes-read is 0. It means that the calling code is wrong. In this case, after raising the hard error, logically we still increment lexemes-read so that the theorem about ppstate->size holds unconditionally.

Definitions and Theorems

Function: punread-token

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

Theorem: ppstatep-of-punread-token

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

Theorem: ppstate->size-of-unread-token

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