Parse an attribute name.
(parse-attribute-name parstate) → (mv erp attrname span new-parstate)
Function:
(defun parse-attribute-name (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-attribute-name)) (declare (ignorable __function__)) (b* (((reterr) (irr-attrib-name) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((and token (token-case token :ident)) (retok (attrib-name-ident (token-ident->unwrap token)) span parstate)) ((and token (token-case token :keyword)) (retok (attrib-name-keyword (token-keyword->unwrap token)) span parstate)) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an identifier or keyword" :found (token-to-msg token)))))))
Theorem:
(defthm attrib-namep-of-parse-attribute-name.attrname (b* (((mv acl2::?erp ?attrname ?span ?new-parstate) (parse-attribute-name parstate))) (attrib-namep attrname)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-attribute-name.span (b* (((mv acl2::?erp ?attrname ?span ?new-parstate) (parse-attribute-name parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-attribute-name.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?attrname ?span ?new-parstate) (parse-attribute-name parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-attribute-name-uncond (b* (((mv acl2::?erp ?attrname ?span ?new-parstate) (parse-attribute-name parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-name-cond (b* (((mv acl2::?erp ?attrname ?span ?new-parstate) (parse-attribute-name parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)