Parse a list of one or more type qualifiers.
(parse-type-qualifier-list parstate) → (mv erp tyquals span new-parstate)
We parse the first one, which must exist. Then we check the next token to see if there is be another one, in which case we put it back and recursively parse a type qualifier list, otherwise we put back it back and return.
Function:
(defun parse-type-qualifier-list (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-type-qualifier-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-type-qualifier-p token) (b* ((tyqual (token-to-type-qualifier token)) ((erp token & parstate) (read-token parstate))) (cond ((token-type-qualifier-p token) (b* ((parstate (unread-token parstate)) ((erp tyquals last-span parstate) (parse-type-qualifier-list parstate))) (retok (cons tyqual tyquals) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list tyqual) span parstate)))))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "a keyword in {~ const, ~ restrict, ~ volatile, ~ _Atomic~ }" :found (token-to-msg token)))))))
Theorem:
(defthm type-qual-listp-of-parse-type-qualifier-list.tyquals (b* (((mv acl2::?erp ?tyquals ?span ?new-parstate) (parse-type-qualifier-list parstate))) (type-qual-listp tyquals)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-type-qualifier-list.span (b* (((mv acl2::?erp ?tyquals ?span ?new-parstate) (parse-type-qualifier-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-type-qualifier-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?tyquals ?span ?new-parstate) (parse-type-qualifier-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-type-qualifier-list-uncond (b* (((mv acl2::?erp ?tyquals ?span ?new-parstate) (parse-type-qualifier-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-type-qualifier-list-cond (b* (((mv acl2::?erp ?tyquals ?span ?new-parstate) (parse-type-qualifier-list parstate))) (implies (and (not erp) token?) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)