		Search-engine friendly clone of the ACL2 documentation.

Parser

Unread-chars

Unread a specified number of characters.

Signature
(unread-chars n parstate) → new-parstate
Arguments: n — Guard (natp n).; parstate — Guard (parstatep parstate).
Returns: new-parstate — Type (parstatep new-parstate), given (parstatep parstate).

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, besides raising the error, we increment chars-unread so that the theorem on the parser state size holds unconditionally.

Definitions and Theorems

Function: unread-chars

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

Theorem: parstatep-of-unread-chars

(defthm parstatep-of-unread-chars
  (implies (parstatep parstate)
           (b* ((new-parstate (unread-chars n parstate)))
             (parstatep new-parstate)))
  :rule-classes :rewrite)

Theorem: parsize-of-unread-chars

(defthm parsize-of-unread-chars
  (b* ((?new-parstate (unread-chars n parstate)))
    (equal (parsize new-parstate)
           (+ (parsize parstate) (nfix n)))))