Parse a list of one or more declarations.
(parse-declaration-list pstate) → (mv erp decls span new-pstate)
We parse the first one, which must be present. Then we stop if the next token is an open curly brace, because the only place where we parse declaration lists is in function definitions, between declarator and body. Otherwise we recursively call this function to parse more.
Function:
(defun parse-declaration-list (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-declaration-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) ((erp decl span pstate) (parse-declaration pstate)) ((erp token & pstate) (read-token pstate))) (cond ((equal token (token-punctuator "{")) (retok (list decl) span pstate)) (t (b* ((pstate (if token (unread-token pstate) pstate)) ((erp decls last-span pstate) (parse-declaration-list pstate))) (retok (cons decl decls) (span-join span last-span) pstate)))))))
Theorem:
(defthm decl-listp-of-parse-declaration-list.decls (b* (((mv acl2::?erp ?decls ?span ?new-pstate) (parse-declaration-list pstate))) (decl-listp decls)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-declaration-list.span (b* (((mv acl2::?erp ?decls ?span ?new-pstate) (parse-declaration-list pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-declaration-list.new-pstate (b* (((mv acl2::?erp ?decls ?span ?new-pstate) (parse-declaration-list pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-declaration-list-uncond (b* (((mv acl2::?erp ?decls ?span ?new-pstate) (parse-declaration-list pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-list-cond (b* (((mv acl2::?erp ?decls ?span ?new-pstate) (parse-declaration-list pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)