Read a token.
(read-token pstate) → (mv erp token? span new-pstate)
If we find a token, we return it, along with its span.
If we reach the end of file, we return
First we check whether some token was unread, in which case we pop the stack of unread tokens. See the discussion in parstate.
The token read is pushed onto the
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.)
Function:
(defun read-token-loop (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'read-token-loop)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) ((erp lexeme? span pstate) (lex-lexeme pstate)) ((when (not lexeme?)) (retok nil span pstate)) ((when (lexeme-case lexeme? :token)) (b* ((token (lexeme-token->unwrap lexeme?)) (pstate (change-parstate pstate :tokens-read (cons (make-token+span :token token :span span) (parstate->tokens-read pstate)) :tokens-read-len (1+ (parstate->tokens-read-len pstate))))) (retok token span pstate)))) (read-token-loop pstate))))
Theorem:
(defthm token-optionp-of-read-token-loop.token? (b* (((mv acl2::?erp ?token? ?span ?new-pstate) (read-token-loop pstate))) (token-optionp token?)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-read-token-loop.span (b* (((mv acl2::?erp ?token? ?span ?new-pstate) (read-token-loop pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-read-token-loop.new-pstate (b* (((mv acl2::?erp ?token? ?span ?new-pstate) (read-token-loop pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-read-token-loop-uncond (b* (((mv acl2::?erp ?token? ?span ?new-pstate) (read-token-loop pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-read-token-loop-cond (b* (((mv acl2::?erp ?token? ?span ?new-pstate) (read-token-loop pstate))) (implies (and (not erp) token?) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Function:
(defun read-token (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'read-token)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) ((parstate pstate) pstate) ((when (consp pstate.tokens-unread)) (b* ((token+span (car pstate.tokens-unread))) (retok (token+span->token token+span) (token+span->span token+span) (change-parstate pstate :tokens-unread (cdr pstate.tokens-unread) :tokens-read (cons token+span pstate.tokens-read) :tokens-read-len (1+ pstate.tokens-read-len) :chars-read nil :size (1- pstate.size)))))) (read-token-loop pstate))))
Theorem:
(defthm token-optionp-of-read-token.token? (b* (((mv acl2::?erp ?token? ?span ?new-pstate) (read-token pstate))) (token-optionp token?)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-read-token.span (b* (((mv acl2::?erp ?token? ?span ?new-pstate) (read-token pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-read-token.new-pstate (b* (((mv acl2::?erp ?token? ?span ?new-pstate) (read-token pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-read-token-uncond (b* (((mv acl2::?erp ?token? ?span ?new-pstate) (read-token pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-read-token-cond (b* (((mv acl2::?erp ?token? ?span ?new-pstate) (read-token pstate))) (implies (and (not erp) token?) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)