		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-reader

Update-ppstate-for-char

Update the preprocessor state for a character.

Signature
(update-ppstate-for-char char new-bytes new-position size-decrement ppstate) → new-ppstate
Arguments: char — Guard (natp char).; new-bytes — Guard (byte-listp new-bytes).; new-position — Guard (positionp new-position).; size-decrement — Guard (posp size-decrement).; ppstate — Guard (ppstatep ppstate).
Returns: new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).

This is used when pread-char reads a character from the data bytes (not from the unread characters). The new-bytes input consists of the remaining data bytes, i.e. after the one ore more bytes that form the character have already been removed (and decoded). The new-position input consists of the next position, which is normally one column more than the current one, except when dealing with new-line characters.

Definitions and Theorems

Function: update-ppstate-for-char

(defun update-ppstate-for-char
       (char new-bytes
             new-position size-decrement ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (and (natp char)
                              (byte-listp new-bytes)
                              (positionp new-position)
                              (posp size-decrement)
                              (ppstatep ppstate))))
  (declare (xargs :guard (and (< (ppstate->chars-read ppstate)
                                 (ppstate->chars-length ppstate))
                              (>= (ppstate->size ppstate)
                                  size-decrement))))
  (b* ((position (ppstate->position ppstate))
       (chars-read (ppstate->chars-read ppstate))
       (size (ppstate->size ppstate))
       (new-size (- size (pos-fix size-decrement)))
       (char+pos (make-char+position :char char
                                     :position position))
       (ppstate (update-ppstate->bytes new-bytes ppstate))
       (ppstate (update-ppstate->char chars-read char+pos ppstate))
       (ppstate (update-ppstate->chars-read (1+ chars-read)
                                            ppstate))
       (ppstate (update-ppstate->position new-position ppstate))
       (ppstate (update-ppstate->size new-size ppstate)))
    ppstate))

Theorem: ppstatep-of-update-ppstate-for-char

(defthm ppstatep-of-update-ppstate-for-char
 (implies
  (ppstatep ppstate)
  (b*
   ((new-ppstate
     (update-ppstate-for-char char new-bytes
                              new-position size-decrement ppstate)))
   (ppstatep new-ppstate)))
 :rule-classes :rewrite)

Theorem: ppstate->size-of-update-ppstate-for-char

(defthm ppstate->size-of-update-ppstate-for-char
 (implies
  (>= (ppstate->size ppstate)
      (pos-fix size-decrement))
  (b*
   ((?new-ppstate
     (update-ppstate-for-char char new-bytes
                              new-position size-decrement ppstate)))
   (equal (ppstate->size new-ppstate)
          (- (ppstate->size ppstate)
             (pos-fix size-decrement))))))