Parse a list of one or more declarations.
(parse-declaration-list parstate) → (mv erp decls span new-parstate)
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 (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-declaration-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp decl span parstate) (parse-declaration parstate)) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token "{") (retok (list decl) span parstate)) (t (b* ((parstate (if token (unread-token parstate) parstate)) ((erp decls last-span parstate) (parse-declaration-list parstate))) (retok (cons decl decls) (span-join span last-span) parstate)))))))
Theorem:
(defthm decl-listp-of-parse-declaration-list.decls (b* (((mv acl2::?erp ?decls ?span ?new-parstate) (parse-declaration-list parstate))) (decl-listp decls)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-declaration-list.span (b* (((mv acl2::?erp ?decls ?span ?new-parstate) (parse-declaration-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-declaration-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?decls ?span ?new-parstate) (parse-declaration-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-declaration-list-uncond (b* (((mv acl2::?erp ?decls ?span ?new-parstate) (parse-declaration-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-list-cond (b* (((mv acl2::?erp ?decls ?span ?new-parstate) (parse-declaration-list parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)