Parse a list of zero or more string literals.
(parse-*-stringlit pstate) → (mv erp strings span new-pstate)
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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-*-stringlit)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate)) ((unless (and token (token-case token :string))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok nil (irr-span) pstate))) (string (token-string->unwrap token)) ((erp strings last-span pstate) (parse-*-stringlit pstate))) (retok (cons string strings) (if strings (span-join span last-span) span) pstate))))
Theorem:
(defthm stringlit-listp-of-parse-*-stringlit.strings (b* (((mv acl2::?erp ?strings ?span ?new-pstate) (parse-*-stringlit pstate))) (stringlit-listp strings)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-*-stringlit.span (b* (((mv acl2::?erp ?strings ?span ?new-pstate) (parse-*-stringlit pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-*-stringlit.new-pstate (b* (((mv acl2::?erp ?strings ?span ?new-pstate) (parse-*-stringlit pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-*-stringlit-uncond (b* (((mv acl2::?erp ?strings ?span ?new-pstate) (parse-*-stringlit pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)