Parse a list of one or more initializer declarators.
(parse-init-declarator-list parstate) → (mv erp initdeclors span new-parstate)
We parse the first one, which must be present. If there is a comma after that, we recursively parse one or more after the comma.
Function:
(defun parse-init-declarator-list (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-init-declarator-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp initdeclor span parstate) (parse-init-declarator parstate)) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token ",") (b* (((erp initdeclors last-span parstate) (parse-init-declarator-list parstate))) (retok (cons initdeclor initdeclors) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list initdeclor) span parstate)))))))
Theorem:
(defthm initdeclor-listp-of-parse-init-declarator-list.initdeclors (b* (((mv acl2::?erp ?initdeclors ?span ?new-parstate) (parse-init-declarator-list parstate))) (initdeclor-listp initdeclors)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-init-declarator-list.span (b* (((mv acl2::?erp ?initdeclors ?span ?new-parstate) (parse-init-declarator-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-init-declarator-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?initdeclors ?span ?new-parstate) (parse-init-declarator-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-init-declarator-list-uncond (b* (((mv acl2::?erp ?initdeclors ?span ?new-parstate) (parse-init-declarator-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-init-declarator-list-cond (b* (((mv acl2::?erp ?initdeclors ?span ?new-parstate) (parse-init-declarator-list parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)