		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Pread-token/newline

Read a token or newline during preprocessing.

Signature
(pread-token/newline headerp ppstate) → (mv erp nontokens-nonnewlines token/newline? token/newline-span new-ppstate)
Arguments: headerp — Guard (booleanp headerp).; ppstate — Guard (ppstatep ppstate).
Returns: nontokens-nonnewlines — Type (plexeme-listp nontokens-nonnewlines).; token/newline? — Type (plexeme-optionp token/newline?).; token/newline-span — Type (spanp token/newline-span).; new-ppstate — Type (ppstatep new-ppstate), given (ppstatep ppstate).

As explained in plexeme-token/newline-p, we also include line comments as newlines.

Definitions and Theorems

Function: pread-token/newline

(defun pread-token/newline (headerp ppstate)
  (declare (xargs :stobjs (ppstate)))
  (declare (xargs :guard (and (booleanp headerp)
                              (ppstatep ppstate))))
  (b* (((reterr) nil nil (irr-span) ppstate)
       ((erp lexeme span ppstate)
        (plex-lexeme headerp ppstate))
       ((when (not lexeme))
        (retok nil nil span ppstate))
       ((when (plexeme-token/newline-p lexeme))
        (retok nil lexeme span ppstate))
       ((erp nontokens-nonnewlines token/newline
             token/newline-span ppstate)
        (pread-token/newline headerp ppstate)))
    (retok (cons lexeme nontokens-nonnewlines)
           token/newline
           token/newline-span ppstate)))

Theorem: plexeme-listp-of-pread-token/newline.nontokens-nonnewlines

(defthm plexeme-listp-of-pread-token/newline.nontokens-nonnewlines
  (b* (((mv acl2::?erp
            ?nontokens-nonnewlines ?token/newline?
            ?token/newline-span ?new-ppstate)
        (pread-token/newline headerp ppstate)))
    (plexeme-listp nontokens-nonnewlines))
  :rule-classes :rewrite)

Theorem: plexeme-optionp-of-pread-token/newline.token/newline?

(defthm plexeme-optionp-of-pread-token/newline.token/newline?
  (b* (((mv acl2::?erp
            ?nontokens-nonnewlines ?token/newline?
            ?token/newline-span ?new-ppstate)
        (pread-token/newline headerp ppstate)))
    (plexeme-optionp token/newline?))
  :rule-classes :rewrite)

Theorem: spanp-of-pread-token/newline.token/newline-span

(defthm spanp-of-pread-token/newline.token/newline-span
  (b* (((mv acl2::?erp
            ?nontokens-nonnewlines ?token/newline?
            ?token/newline-span ?new-ppstate)
        (pread-token/newline headerp ppstate)))
    (spanp token/newline-span))
  :rule-classes :rewrite)

Theorem: ppstatep-of-pread-token/newline.new-ppstate

(defthm ppstatep-of-pread-token/newline.new-ppstate
  (implies (ppstatep ppstate)
           (b* (((mv acl2::?erp
                     ?nontokens-nonnewlines ?token/newline?
                     ?token/newline-span ?new-ppstate)
                 (pread-token/newline headerp ppstate)))
             (ppstatep new-ppstate)))
  :rule-classes :rewrite)

Theorem: plexeme-list-not-token/newline-p-of-pread-token/newline

(defthm plexeme-list-not-token/newline-p-of-pread-token/newline
  (b* (((mv acl2::?erp
            ?nontokens-nonnewlines ?token/newline?
            ?token/newline-span ?new-ppstate)
        (pread-token/newline headerp ppstate)))
    (plexeme-list-not-token/newline-p nontokens-nonnewlines)))

Theorem: plexeme-token/newline-p-of-pread-token/newline

(defthm plexeme-token/newline-p-of-pread-token/newline
  (b* (((mv acl2::?erp
            ?nontokens-nonnewlines ?token/newline?
            ?token/newline-span ?new-ppstate)
        (pread-token/newline headerp ppstate)))
    (implies token?
             (plexeme-token/newline-p token/newline?))))

Theorem: ppstate->size-of-pread-token/newline-uncond

(defthm ppstate->size-of-pread-token/newline-uncond
  (b* (((mv acl2::?erp
            ?nontokens-nonnewlines ?token/newline?
            ?token/newline-span ?new-ppstate)
        (pread-token/newline headerp ppstate)))
    (<= (ppstate->size new-ppstate)
        (ppstate->size ppstate)))
  :rule-classes :linear)

Theorem: ppstate->size-of-pread-token/newline-cond

(defthm ppstate->size-of-pread-token/newline-cond
  (b* (((mv acl2::?erp
            ?nontokens-nonnewlines ?token/newline?
            ?token/newline-span ?new-ppstate)
        (pread-token/newline headerp ppstate)))
    (implies (and (not erp) token/newline?)
             (<= (ppstate->size new-ppstate)
                 (1- (ppstate->size ppstate)))))
  :rule-classes :linear)