Read an identifier token.
This is called when we expect an identifier token. We read the next token, ensuring it exists and is an identifier. We return the identifier if successful.
Function:
(defun read-identifier (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'read-identifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-ident) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate)) ((unless (and token (token-case token :ident))) (reterr-msg :where (position-to-msg (span->start span)) :expected "an identifier" :found (token-to-msg token))) (ident (token-ident->unwrap token))) (retok ident span pstate))))
Theorem:
(defthm identp-of-read-identifier.ident (b* (((mv acl2::?erp ?ident ?span ?new-pstate) (read-identifier pstate))) (identp ident)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-read-identifier.span (b* (((mv acl2::?erp ?ident ?span ?new-pstate) (read-identifier pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-read-identifier.new-pstate (b* (((mv acl2::?erp ?ident ?span ?new-pstate) (read-identifier pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-read-ident-uncond (b* (((mv acl2::?erp ?ident ?span ?new-pstate) (read-identifier pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-read-ident-cond (b* (((mv acl2::?erp ?ident ?span ?new-pstate) (read-identifier pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)