Parse a list of one or more external declarations.
(parse-external-declaration-list parstate) → (mv erp extdecls span eof-pos new-parstate)
This is called by parse-translation-unit to parse all the external declarations in a file. If successful, we return the list of external declarations.
We also return the position just past the end of the file. The latter is used for a check performed by the caller.
We parse the first external declaration, which must be present. Then, unless we have reached the end of the file, we recursively parse more external declarations.
Function:
(defun parse-external-declaration-list (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-external-declaration-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-position) parstate) ((erp extdecl first-span parstate) (parse-external-declaration parstate)) ((erp token span parstate) (read-token parstate)) ((when (not token)) (retok (list extdecl) first-span (span->start span) parstate)) (parstate (unread-token parstate)) ((erp extdecls last-span eof-pos parstate) (parse-external-declaration-list parstate))) (retok (cons extdecl extdecls) (span-join first-span last-span) eof-pos parstate))))
Theorem:
(defthm extdecl-listp-of-parse-external-declaration-list.extdecls (b* (((mv acl2::?erp ?extdecls ?span ?eof-pos ?new-parstate) (parse-external-declaration-list parstate))) (extdecl-listp extdecls)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-external-declaration-list.span (b* (((mv acl2::?erp ?extdecls ?span ?eof-pos ?new-parstate) (parse-external-declaration-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-parse-external-declaration-list.eof-pos (b* (((mv acl2::?erp ?extdecls ?span ?eof-pos ?new-parstate) (parse-external-declaration-list parstate))) (positionp eof-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-external-declaration-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?extdecls ?span ?eof-pos ?new-parstate) (parse-external-declaration-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-external-declaration-list-uncond (b* (((mv acl2::?erp ?extdecls ?span ?eof-pos ?new-parstate) (parse-external-declaration-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-external-declaration-list-cond (b* (((mv acl2::?erp ?extdecls ?span ?eof-pos ?new-parstate) (parse-external-declaration-list parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)