		Search-engine friendly clone of the ACL2 documentation.

Parser

Init-parstate

Initialize the parser state.

Signature
(init-parstate data gcc parstate) → parstate
Arguments: data — Guard (byte-listp data).; gcc — Guard (booleanp gcc).
Returns: parstate — Type (parstatep parstate).

This is the state when we start parsing a file. Given (the data of) a file to parse, and a flag saying whether GCC extensions should be accepted or not, the initial parsing state consists of the data to parse, no read characters or tokens, no unread characters or tokens, and the initial file position. We also resize the arrays of characters and tokens to the number of data bytes, which is overkill but certainly sufficient (because we will never lex more characters or tokens than bytes); if this turns out to be too large, we will pick a different size, but then we may need to resize the array as needed while lexing and parsing.

Definitions and Theorems

Function: init-parstate

(defun init-parstate (data gcc parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (and (byte-listp data) (booleanp gcc))))
  (let ((__function__ 'init-parstate))
    (declare (ignorable __function__))
    (b* ((parstate (update-parstate->bytes data parstate))
         (parstate (update-parstate->position (position-init)
                                              parstate))
         (parstate (update-parstate->chars-length (len data)
                                                  parstate))
         (parstate (update-parstate->chars-read 0 parstate))
         (parstate (update-parstate->chars-unread 0 parstate))
         (parstate (update-parstate->tokens-length (len data)
                                                   parstate))
         (parstate (update-parstate->tokens-read 0 parstate))
         (parstate (update-parstate->tokens-unread 0 parstate))
         (parstate (update-parstate->gcc gcc parstate))
         (parstate (update-parstate->size (len data)
                                          parstate)))
      parstate)))

Theorem: parstatep-of-init-parstate

(defthm parstatep-of-init-parstate
  (b* ((parstate (init-parstate data gcc parstate)))
    (parstatep parstate))
  :rule-classes :rewrite)

Theorem: init-parstate-of-byte-list-fix-data

(defthm init-parstate-of-byte-list-fix-data
  (equal (init-parstate (byte-list-fix data)
                        gcc parstate)
         (init-parstate data gcc parstate)))

Theorem: init-parstate-byte-list-equiv-congruence-on-data

(defthm init-parstate-byte-list-equiv-congruence-on-data
  (implies (acl2::byte-list-equiv data data-equiv)
           (equal (init-parstate data gcc parstate)
                  (init-parstate data-equiv gcc parstate)))
  :rule-classes :congruence)

Theorem: init-parstate-of-bool-fix-gcc

(defthm init-parstate-of-bool-fix-gcc
  (equal (init-parstate data (bool-fix gcc)
                        parstate)
         (init-parstate data gcc parstate)))

Theorem: init-parstate-iff-congruence-on-gcc

(defthm init-parstate-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (init-parstate data gcc parstate)
                  (init-parstate data gcc-equiv parstate)))
  :rule-classes :congruence)

Theorem: init-parstate-of-parstate-fix-parstate

(defthm init-parstate-of-parstate-fix-parstate
  (equal (init-parstate data gcc (parstate-fix parstate))
         (init-parstate data gcc parstate)))

Theorem: init-parstate-parstate-equiv-congruence-on-parstate

(defthm init-parstate-parstate-equiv-congruence-on-parstate
  (implies (parstate-equiv parstate parstate-equiv)
           (equal (init-parstate data gcc parstate)
                  (init-parstate data gcc parstate-equiv)))
  :rule-classes :congruence)