Parse an optional assembler name specifier.
(parse-?-asm-name-specifier parstate) → (mv erp asmspec? span new-parstate)
The optionality is conveyed by
the question mark in the name of this function.
If the next token is the
Function:
(defun parse-?-asm-name-specifier (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-?-asm-name-specifier)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-keywordp token "asm") (parse-asm-name-specifier nil span parstate)) ((token-keywordp token "__asm__") (parse-asm-name-specifier t span parstate)) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok nil (irr-span) parstate)))))))
Theorem:
(defthm asm-name-spec-optionp-of-parse-?-asm-name-specifier.asmspec? (b* (((mv acl2::?erp ?asmspec? ?span ?new-parstate) (parse-?-asm-name-specifier parstate))) (asm-name-spec-optionp asmspec?)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-?-asm-name-specifier.span (b* (((mv acl2::?erp ?asmspec? ?span ?new-parstate) (parse-?-asm-name-specifier parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-?-asm-name-specifier.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?asmspec? ?span ?new-parstate) (parse-?-asm-name-specifier parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-?-asm-name-specifier (b* (((mv acl2::?erp ?asmspec? ?span ?new-parstate) (parse-?-asm-name-specifier parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)