Parse a list of one or more type qualifiers.
(parse-type-qualifier-list pstate) → (mv erp tyquals span new-pstate)
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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-type-qualifier-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((token-type-qualifier-p token) (b* ((tyqual (token-to-type-qualifier token)) ((erp token & pstate) (read-token pstate))) (cond ((token-type-qualifier-p token) (b* ((pstate (unread-token pstate)) ((erp tyquals last-span pstate) (parse-type-qualifier-list pstate))) (retok (cons tyqual tyquals) (span-join span last-span) pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (list tyqual) span pstate)))))) (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-pstate) (parse-type-qualifier-list pstate))) (type-qual-listp tyquals)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-type-qualifier-list.span (b* (((mv acl2::?erp ?tyquals ?span ?new-pstate) (parse-type-qualifier-list pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-type-qualifier-list.new-pstate (b* (((mv acl2::?erp ?tyquals ?span ?new-pstate) (parse-type-qualifier-list pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-type-qualifier-list-uncond (b* (((mv acl2::?erp ?tyquals ?span ?new-pstate) (parse-type-qualifier-list pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-type-qualifier-list-cond (b* (((mv acl2::?erp ?tyquals ?span ?new-pstate) (parse-type-qualifier-list pstate))) (implies (and (not erp) token?) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)