		Search-engine friendly clone of the ACL2 documentation.

Preprocessor

Pread-token

Read a token during preprocessing.

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

We lex zero or more non-tokens, until we find a token. We return the list of non-tokens, and the token with its span. If we reach the end of file, we return nil as the token, and an span consisting of just the current position.

The headerp flag has the same meaning as in plex-lexeme: see that function's documentation.

Definitions and Theorems

Function: pread-token

(defun pread-token (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-tokenp lexeme))
        (retok nil lexeme span ppstate))
       ((erp nontokens token token-span ppstate)
        (pread-token headerp ppstate)))
    (retok (cons lexeme nontokens)
           token token-span ppstate)))

Theorem: plexeme-listp-of-pread-token.nontokens

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

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

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

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

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

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

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

Theorem: plexeme-list-not-tokenp-of-pread-token

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

Theorem: plexeme-tokenp-of-pread-token

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

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

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

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

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