Parse an optional assembler name specifier.
(parse-?-asm-name-specifier pstate) → (mv erp asmspec? span new-pstate)
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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-?-asm-name-specifier)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((equal token (token-keyword "asm")) (parse-asm-name-specifier nil span pstate)) ((equal token (token-keyword "__asm__")) (parse-asm-name-specifier t span pstate)) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok nil (irr-span) pstate)))))))
Theorem:
(defthm asm-name-spec-optionp-of-parse-?-asm-name-specifier.asmspec? (b* (((mv acl2::?erp ?asmspec? ?span ?new-pstate) (parse-?-asm-name-specifier pstate))) (asm-name-spec-optionp asmspec?)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-?-asm-name-specifier.span (b* (((mv acl2::?erp ?asmspec? ?span ?new-pstate) (parse-?-asm-name-specifier pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-?-asm-name-specifier.new-pstate (b* (((mv acl2::?erp ?asmspec? ?span ?new-pstate) (parse-?-asm-name-specifier pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-?-asm-name-specifier (b* (((mv acl2::?erp ?asmspec? ?span ?new-pstate) (parse-?-asm-name-specifier pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)