		Search-engine friendly clone of the ACL2 documentation.

Preprocessor-states

Init-ppstate

Initialize the preprocessor state.

Signature
(init-ppstate data version ppstate) → ppstate
Arguments: data — Guard (byte-listp data).; version — Guard (c::versionp version).
Returns: ppstate — Type (ppstatep ppstate).

This is the state when we start preprocessing a file. Given (the data of) a file to preprocess, and a C version, the initial preprocessing state consists of the data to preprocess, no read characters or lexemes, no unread characters or lexemes, and the initial file position. We also resize the arrays of characters and lexemes to the number of data bytes, which is overkill but certainly sufficient (because we will never lex more characters or lexemes 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 preprocessing.

Definitions and Theorems

Function: init-ppstate

(defun init-ppstate (data version ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (and (byte-listp data)
                              (c::versionp version))))
  (b* ((ppstate (update-ppstate->bytes data ppstate))
       (ppstate (update-ppstate->position (position-init)
                                          ppstate))
       (ppstate (update-ppstate->chars-length (len data)
                                              ppstate))
       (ppstate (update-ppstate->chars-read 0 ppstate))
       (ppstate (update-ppstate->chars-unread 0 ppstate))
       (ppstate (update-ppstate->lexemes-length (len data)
                                                ppstate))
       (ppstate (update-ppstate->lexemes-read 0 ppstate))
       (ppstate (update-ppstate->lexemes-unread 0 ppstate))
       (ppstate (update-ppstate->version version ppstate))
       (ppstate (update-ppstate->size (len data)
                                      ppstate))
       (ppstate (update-ppstate->macros (macro-table-init)
                                        ppstate)))
    ppstate))

Theorem: ppstatep-of-init-ppstate

(defthm ppstatep-of-init-ppstate
  (b* ((ppstate (init-ppstate data version ppstate)))
    (ppstatep ppstate))
  :rule-classes :rewrite)

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

(defthm init-ppstate-of-byte-list-fix-data
  (equal (init-ppstate (byte-list-fix data)
                       version ppstate)
         (init-ppstate data version ppstate)))

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

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

Theorem: init-ppstate-of-version-fix-version

(defthm init-ppstate-of-version-fix-version
  (equal (init-ppstate data (c::version-fix version)
                       ppstate)
         (init-ppstate data version ppstate)))

Theorem: init-ppstate-version-equiv-congruence-on-version

(defthm init-ppstate-version-equiv-congruence-on-version
  (implies (c::version-equiv version version-equiv)
           (equal (init-ppstate data version ppstate)
                  (init-ppstate data version-equiv ppstate)))
  :rule-classes :congruence)

Theorem: init-ppstate-of-ppstate-fix-ppstate

(defthm init-ppstate-of-ppstate-fix-ppstate
  (equal (init-ppstate data version (ppstate-fix ppstate))
         (init-ppstate data version ppstate)))

Theorem: init-ppstate-ppstate-equiv-congruence-on-ppstate

(defthm init-ppstate-ppstate-equiv-congruence-on-ppstate
  (implies (ppstate-equiv ppstate ppstate-equiv)
           (equal (init-ppstate data version ppstate)
                  (init-ppstate data version ppstate-equiv)))
  :rule-classes :congruence)