Read a token.
(read-token parstate) → (mv erp token? span new-parstate)
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 (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'read-token-loop)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) 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?)) (parstate (update-parstate->tokens-read (cons (make-token+span :token token :span span) (parstate->tokens-read parstate)) parstate)) (parstate (update-parstate->tokens-read-len (1+ (parstate->tokens-read-len parstate)) parstate))) (retok token span parstate)))) (read-token-loop parstate))))
Theorem:
(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:
(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:
(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:
(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:
(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:
(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-read-len (parstate->tokens-read-len parstate)) (parstate.tokens-unread (parstate->tokens-unread parstate)) (parstate.size (parstate->size parstate)) ((when (and (consp parstate.tokens-unread) (> parstate.size 0))) (b* ((token+span (car parstate.tokens-unread)) (parstate (update-parstate->tokens-unread (cdr parstate.tokens-unread) parstate)) (parstate (update-parstate->tokens-read (cons token+span parstate.tokens-read) parstate)) (parstate (update-parstate->tokens-read-len (1+ parstate.tokens-read-len) parstate)) (parstate (update-parstate->chars-read nil 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:
(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:
(defthm spanp-of-read-token.span (b* (((mv acl2::?erp ?token? ?span ?new-parstate) (read-token parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(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:
(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:
(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)