Parse zero or more assembler goto labels.
(parse-asm-goto-labels parstate) → (mv erp labels span new-parstate)
Function:
(defun parse-asm-goto-labels-loop (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-asm-goto-labels-loop)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp label span parstate) (read-identifier parstate)) ((erp token & parstate) (read-token parstate)) ((unless (token-punctuatorp token ",")) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list label) span parstate))) ((erp labels last-span parstate) (parse-asm-goto-labels-loop parstate))) (retok (cons label labels) (span-join span last-span) parstate))))
Theorem:
(defthm ident-listp-of-parse-asm-goto-labels-loop.labels (b* (((mv acl2::?erp common-lisp::?labels ?span ?new-parstate) (parse-asm-goto-labels-loop parstate))) (ident-listp labels)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-asm-goto-labels-loop.span (b* (((mv acl2::?erp common-lisp::?labels ?span ?new-parstate) (parse-asm-goto-labels-loop parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-asm-goto-labels-loop.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp common-lisp::?labels ?span ?new-parstate) (parse-asm-goto-labels-loop parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-asm-goto-labels-loop (b* (((mv acl2::?erp common-lisp::?labels ?span ?new-parstate) (parse-asm-goto-labels-loop parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Function:
(defun parse-asm-goto-labels (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-asm-goto-labels)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((unless (and token (token-case token :ident))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok nil (irr-span) parstate))) (parstate (unread-token parstate))) (parse-asm-goto-labels-loop parstate))))
Theorem:
(defthm ident-listp-of-parse-asm-goto-labels.labels (b* (((mv acl2::?erp common-lisp::?labels ?span ?new-parstate) (parse-asm-goto-labels parstate))) (ident-listp labels)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-asm-goto-labels.span (b* (((mv acl2::?erp common-lisp::?labels ?span ?new-parstate) (parse-asm-goto-labels parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-asm-goto-labels.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp common-lisp::?labels ?span ?new-parstate) (parse-asm-goto-labels parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-asm-goto-labels (b* (((mv acl2::?erp common-lisp::?labels ?span ?new-parstate) (parse-asm-goto-labels parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)