Parse a list of one or more external declarations.
(parse-external-declaration-list pstate) → (mv erp extdecls span eof-pos new-pstate)
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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-external-declaration-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-position) (irr-parstate)) ((erp extdecl first-span pstate) (parse-external-declaration pstate)) ((erp token span pstate) (read-token pstate)) ((when (not token)) (retok (list extdecl) first-span (span->start span) pstate)) (pstate (unread-token pstate)) ((erp extdecls last-span eof-pos pstate) (parse-external-declaration-list pstate))) (retok (cons extdecl extdecls) (span-join first-span last-span) eof-pos pstate))))
Theorem:
(defthm extdecl-listp-of-parse-external-declaration-list.extdecls (b* (((mv acl2::?erp ?extdecls ?span ?eof-pos ?new-pstate) (parse-external-declaration-list pstate))) (extdecl-listp extdecls)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-external-declaration-list.span (b* (((mv acl2::?erp ?extdecls ?span ?eof-pos ?new-pstate) (parse-external-declaration-list pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm positionp-of-parse-external-declaration-list.eof-pos (b* (((mv acl2::?erp ?extdecls ?span ?eof-pos ?new-pstate) (parse-external-declaration-list pstate))) (positionp eof-pos)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-external-declaration-list.new-pstate (b* (((mv acl2::?erp ?extdecls ?span ?eof-pos ?new-pstate) (parse-external-declaration-list pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-external-declaration-list-uncond (b* (((mv acl2::?erp ?extdecls ?span ?eof-pos ?new-pstate) (parse-external-declaration-list pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-external-declaration-list-cond (b* (((mv acl2::?erp ?extdecls ?span ?eof-pos ?new-pstate) (parse-external-declaration-list pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)