Parse an external declaration.
An external declaration is
either a function definition,
which starts with a non-empty sequence of declaration specifiers,
or a declaration,
which also starts with a non-empty sequence of declaration specifiers,
unless it is a static assert declaration,
which starts with the keyword
No declaration specifier starts with the keyword
Otherwise, we read one or more declaration specifiers, since those are present both in declarations and in function definitions. Then we must have a declarator in either case, but based on what follows it, we can decide whether we have a declarator or a function definition.
If GCC extensions are supported, we must also taken into account
the possible presence of attributes and assembler name specifiers,
as well as of an
Function:
(defun parse-external-declaration (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-external-declaration)) (declare (ignorable __function__)) (b* (((reterr) (irr-extdecl) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((equal token (token-keyword "_Static_assert")) (b* (((erp statassert span pstate) (parse-static-assert-declaration span pstate))) (retok (extdecl-decl (decl-statassert statassert)) span pstate))) (t (b* (((mv extension pstate) (if (and (equal token (token-keyword "__extension__")) (parstate->gcc pstate)) (mv t pstate) (mv nil (if token (unread-token pstate) pstate)))) ((erp declspecs span pstate) (parse-declaration-specifiers nil pstate)) ((erp token2 span2 pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator ";")) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init nil :asm? nil :attrib nil)) (span-join span span2) pstate)) ((and (or (equal token2 (token-keyword "asm")) (equal token2 (token-keyword "__asm__"))) (parstate->gcc pstate)) (b* ((uscores (equal token2 (token-keyword "__asm__"))) ((erp asmspec & pstate) (parse-asm-name-specifier uscores span2 pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init nil :asm? asmspec :attrib attrspecs)) (span-join span last-span) pstate))) ((and (equal token2 (token-keyword "__attribute__")) (parstate->gcc pstate)) (b* ((pstate (unread-token pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init nil :asm? nil :attrib attrspecs)) (span-join span last-span) pstate))) (t (b* ((pstate (if token2 (unread-token pstate) pstate)) ((erp declor & pstate) (parse-declarator pstate)) ((erp token3 span3 pstate) (read-token pstate))) (cond ((equal token3 (token-punctuator "=")) (b* (((erp initer & pstate) (parse-initializer pstate)) ((erp token4 span4 pstate) (read-token pstate))) (cond ((equal token4 (token-punctuator ";")) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (list (make-initdeclor :declor declor :init? initer)) :asm? nil :attrib nil)) (span-join span span4) pstate)) ((equal token4 (token-punctuator ",")) (b* (((erp initdeclors & pstate) (parse-init-declarator-list pstate)) ((erp asmspec? & pstate) (if (parstate->gcc pstate) (parse-?-asm-name-specifier pstate) (retok nil (irr-span) pstate))) ((erp attrspecs & pstate) (if (parstate->gcc pstate) (parse-*-attribute-specifier pstate) (retok nil (irr-span) pstate))) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (cons (make-initdeclor :declor declor :init? initer) initdeclors) :asm? asmspec? :attrib attrspecs)) (span-join span last-span) pstate))) ((and (or (equal token4 (token-keyword "asm")) (equal token4 (token-keyword "__asm__"))) (parstate->gcc pstate)) (b* ((uscore (equal token4 (token-keyword "__asm__"))) ((erp asmspec & pstate) (parse-asm-name-specifier uscore span4 pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (list (make-initdeclor :declor declor :init? initer)) :asm? asmspec :attrib attrspecs)) (span-join span last-span) pstate))) ((and (equal token4 (token-keyword "__attribute__")) (parstate->gcc pstate)) (b* ((pstate (unread-token pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (list (make-initdeclor :declor declor :init? initer)) :asm? nil :attrib attrspecs)) (span-join span last-span) pstate))) (t (reterr-msg :where (position-to-msg (span->start span4)) :expected "a semicolon or a comma" :found (token-to-msg token4)))))) ((equal token3 (token-punctuator ";")) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (list (make-initdeclor :declor declor :init? nil)) :asm? nil :attrib nil)) (span-join span span3) pstate)) ((equal token3 (token-punctuator ",")) (b* (((erp initdeclors & pstate) (parse-init-declarator-list pstate)) ((erp asmspec? & pstate) (parse-?-asm-name-specifier pstate)) ((erp attrspecs & pstate) (if (parstate->gcc pstate) (parse-*-attribute-specifier pstate) (retok nil (irr-span) pstate))) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (cons (make-initdeclor :declor declor :init? nil) initdeclors) :asm? asmspec? :attrib attrspecs)) (span-join span last-span) pstate))) ((and (or (equal token3 (token-keyword "asm")) (equal token3 (token-keyword "__asm__"))) (parstate->gcc pstate)) (b* ((uscores (equal token3 (token-keyword "__asm__"))) ((erp asmspec & pstate) (parse-asm-name-specifier uscores span3 pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (list (make-initdeclor :declor declor :init? nil)) :asm? asmspec :attrib attrspecs)) (span-join span last-span) pstate))) ((and (equal token3 (token-keyword "__attribute__")) (parstate->gcc pstate)) (b* ((pstate (unread-token pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (extdecl-decl (make-decl-decl :extension extension :specs declspecs :init (list (make-initdeclor :declor declor :init? nil)) :asm? nil :attrib attrspecs)) (span-join span last-span) pstate))) ((equal token3 (token-punctuator "{")) (b* ((pstate (unread-token pstate)) ((erp stmt last-span pstate) (parse-statement pstate))) (retok (extdecl-fundef (make-fundef :extension extension :spec declspecs :declor declor :decls nil :body stmt)) (span-join span last-span) pstate))) (t (b* ((pstate (if token3 (unread-token pstate) pstate)) ((erp decls & pstate) (parse-declaration-list pstate)) ((erp token4 span4 pstate) (read-token pstate)) ((unless (equal token4 (token-punctuator "{"))) (reterr-msg :where (position-to-msg (span->start span4)) :expected "an open curly brace" :found (token-to-msg token4))) (pstate (unread-token pstate)) ((erp stmt last-span pstate) (parse-statement pstate))) (retok (extdecl-fundef (make-fundef :extension extension :spec declspecs :declor declor :decls decls :body stmt)) (span-join span last-span) pstate)))))))))))))
Theorem:
(defthm extdeclp-of-parse-external-declaration.extdecl (b* (((mv acl2::?erp ?extdecl ?span ?new-pstate) (parse-external-declaration pstate))) (extdeclp extdecl)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-external-declaration.span (b* (((mv acl2::?erp ?extdecl ?span ?new-pstate) (parse-external-declaration pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-external-declaration.new-pstate (b* (((mv acl2::?erp ?extdecl ?span ?new-pstate) (parse-external-declaration pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-external-declaration-uncond (b* (((mv acl2::?erp ?extdecl ?span ?new-pstate) (parse-external-declaration pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-external-declaration-cond (b* (((mv acl2::?erp ?extdecl ?span ?new-pstate) (parse-external-declaration pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)