		Search-engine friendly clone of the ACL2 documentation.

Parser

Read-token

Read a token.

Signature
(read-token parstate) → (mv erp token? span new-parstate)
Arguments: parstate — Guard (parstatep parstate).
Returns: token? — Type (token-optionp token?).; span — Type (spanp span).; new-parstate — Type (parstatep new-parstate), given (parstatep parstate).

If we find a token, we return it, along with its span. If we reach the end of file, we return nil for no token, along with a span that covers just the position just past the end of file, although this span is not that relevant (this span comes from lex-lexeme).

If there are unread tokens, we move a token from the sequence of unread tokens to the sequence of read tokens. We need to check that the index is in range, which we may be able to avoid in the future by adding invariants via an abstract stobj.

Otherwise, we call the lexer to get the next lexeme, until we find a token lexeme or the end of file. That is, we discard white space and comments. (Future extensions of this parser may instead return certain white space and comments under some conditions.)

Definitions and Theorems

Function: read-token-loop

(defun read-token-loop (parstate)
 (declare (xargs :stobjs (parstate)))
 (declare (xargs :guard (parstatep parstate)))
 (let ((__function__ 'read-token-loop))
   (declare (ignorable __function__))
   (b*
    (((reterr) nil (irr-span) parstate)
     (parstate.tokens-read (parstate->tokens-read parstate))
     ((erp lexeme? span parstate)
      (lex-lexeme parstate))
     ((when (not lexeme?))
      (retok nil span parstate))
     ((when (lexeme-case lexeme? :token))
      (b*
       ((token (lexeme-token->unwrap lexeme?))
        ((unless (< parstate.tokens-read
                    (parstate->tokens-length parstate)))
         (raise "Internal error: index ~x0 out of bound ~x1."
                parstate.tokens-read
                (parstate->tokens-length parstate))
         (reterr t))
        (parstate
             (update-parstate->token parstate.tokens-read
                                     (make-token+span :token token
                                                      :span span)
                                     parstate))
        (parstate
             (update-parstate->tokens-read (1+ parstate.tokens-read)
                                           parstate)))
       (retok token span parstate))))
    (read-token-loop parstate))))

Theorem: token-optionp-of-read-token-loop.token?

(defthm token-optionp-of-read-token-loop.token?
  (b* (((mv acl2::?erp ?token? ?span ?new-parstate)
        (read-token-loop parstate)))
    (token-optionp token?))
  :rule-classes :rewrite)

Theorem: spanp-of-read-token-loop.span

(defthm spanp-of-read-token-loop.span
  (b* (((mv acl2::?erp ?token? ?span ?new-parstate)
        (read-token-loop parstate)))
    (spanp span))
  :rule-classes :rewrite)

Theorem: parstatep-of-read-token-loop.new-parstate

(defthm parstatep-of-read-token-loop.new-parstate
  (implies (parstatep parstate)
           (b* (((mv acl2::?erp ?token? ?span ?new-parstate)
                 (read-token-loop parstate)))
             (parstatep new-parstate)))
  :rule-classes :rewrite)

Theorem: parsize-of-read-token-loop-uncond

(defthm parsize-of-read-token-loop-uncond
  (b* (((mv acl2::?erp ?token? ?span ?new-parstate)
        (read-token-loop parstate)))
    (<= (parsize new-parstate)
        (parsize parstate)))
  :rule-classes :linear)

Theorem: parsize-of-read-token-loop-cond

(defthm parsize-of-read-token-loop-cond
  (b* (((mv acl2::?erp ?token? ?span ?new-parstate)
        (read-token-loop parstate)))
    (implies (and (not erp) token?)
             (<= (parsize new-parstate)
                 (1- (parsize parstate)))))
  :rule-classes :linear)

Function: read-token

(defun read-token (parstate)
 (declare (xargs :stobjs (parstate)))
 (declare (xargs :guard (parstatep parstate)))
 (let ((__function__ 'read-token))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil (irr-span) parstate)
    (parstate.tokens-read (parstate->tokens-read parstate))
    (parstate.tokens-unread (parstate->tokens-unread parstate))
    (parstate.size (parstate->size parstate))
    ((when (and (> parstate.tokens-unread 0)
                (> parstate.size 0)))
     (b*
      (((unless (< parstate.tokens-read
                   (parstate->tokens-length parstate)))
        (raise "Internal error: index ~x0 out of bound ~x1."
               parstate.tokens-read
               (parstate->tokens-length parstate))
        (reterr t))
       (token+span (parstate->token parstate.tokens-read parstate))
       (parstate
         (update-parstate->tokens-unread (1- parstate.tokens-unread)
                                         parstate))
       (parstate
            (update-parstate->tokens-read (1+ parstate.tokens-read)
                                          parstate))
       (parstate (update-parstate->size (1- parstate.size)
                                        parstate)))
      (retok (token+span->token token+span)
             (token+span->span token+span)
             parstate))))
   (read-token-loop parstate))))

Theorem: token-optionp-of-read-token.token?

(defthm token-optionp-of-read-token.token?
  (b* (((mv acl2::?erp ?token? ?span ?new-parstate)
        (read-token parstate)))
    (token-optionp token?))
  :rule-classes :rewrite)

Theorem: spanp-of-read-token.span

(defthm spanp-of-read-token.span
  (b* (((mv acl2::?erp ?token? ?span ?new-parstate)
        (read-token parstate)))
    (spanp span))
  :rule-classes :rewrite)

Theorem: parstatep-of-read-token.new-parstate

(defthm parstatep-of-read-token.new-parstate
  (implies (parstatep parstate)
           (b* (((mv acl2::?erp ?token? ?span ?new-parstate)
                 (read-token parstate)))
             (parstatep new-parstate)))
  :rule-classes :rewrite)

Theorem: parsize-of-read-token-uncond

(defthm parsize-of-read-token-uncond
  (b* (((mv acl2::?erp ?token? ?span ?new-parstate)
        (read-token parstate)))
    (<= (parsize new-parstate)
        (parsize parstate)))
  :rule-classes :linear)

Theorem: parsize-of-read-token-cond

(defthm parsize-of-read-token-cond
  (b* (((mv acl2::?erp ?token? ?span ?new-parstate)
        (read-token parstate)))
    (implies (and (not erp) token?)
             (<= (parsize new-parstate)
                 (1- (parsize parstate)))))
  :rule-classes :linear)