Parse a list of zero or more string literals.
(parse-*-stringlit parstate) → (mv erp strings span new-parstate)
That is, we parse a
If there are no string literals, we return an irrelevant span. When combining the span of the first string literal (if present) with the span of the remaining zero or more string literals, we join spans only if the remaining ones are one or more; if there are zero, the span of the first string literal is also the span of the whole sequence.
Function:
(defun parse-*-stringlit (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-*-stringlit)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp token span parstate) (read-token parstate)) ((unless (and token (token-case token :string))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok nil (irr-span) parstate))) (string (token-string->unwrap token)) ((erp strings last-span parstate) (parse-*-stringlit parstate))) (retok (cons string strings) (if strings (span-join span last-span) span) parstate))))
Theorem:
(defthm stringlit-listp-of-parse-*-stringlit.strings (b* (((mv acl2::?erp ?strings ?span ?new-parstate) (parse-*-stringlit parstate))) (stringlit-listp strings)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-*-stringlit.span (b* (((mv acl2::?erp ?strings ?span ?new-parstate) (parse-*-stringlit parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-*-stringlit.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?strings ?span ?new-parstate) (parse-*-stringlit parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-*-stringlit-uncond (b* (((mv acl2::?erp ?strings ?span ?new-parstate) (parse-*-stringlit parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)