Parse a declaration.
A declaration is either an assert declaration,
recognized by the starting
Function:
(defun parse-declaration (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-declaration)) (declare (ignorable __function__)) (b* (((reterr) (irr-decl) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((token-declaration-specifier-start-p token) (b* ((pstate (unread-token pstate)) ((erp declspecs span pstate) (parse-declaration-specifiers nil pstate)) ((erp token2 span2 pstate) (read-token pstate))) (cond ((token-declarator-start-p token2) (b* ((pstate (unread-token pstate)) ((erp initdeclors & pstate) (parse-init-declarator-list pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (make-decl-decl :specs declspecs :init initdeclors) (span-join span last-span) pstate))) ((equal token2 (token-punctuator ";")) (retok (make-decl-decl :specs declspecs :init nil) (span-join span span2) pstate)) (t (reterr-msg :where (position-to-msg (span->start span2)) :expected "a declarator or a semicolon" :found (token-to-msg token2)))))) ((equal token (token-keyword "_Static_assert")) (b* (((erp statassert last-span pstate) (parse-static-assert-declaration span pstate))) (retok (decl-statassert statassert) (span-join span last-span) pstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "a declaration specifier ~ or the _Static_assert keyword" :found (token-to-msg token)))))))
Theorem:
(defthm declp-of-parse-declaration.decl (b* (((mv acl2::?erp ?decl ?span ?new-pstate) (parse-declaration pstate))) (declp decl)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-declaration.span (b* (((mv acl2::?erp ?decl ?span ?new-pstate) (parse-declaration pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-declaration.new-pstate (b* (((mv acl2::?erp ?decl ?span ?new-pstate) (parse-declaration pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-declaration-uncond (b* (((mv acl2::?erp ?decl ?span ?new-pstate) (parse-declaration pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-cond (b* (((mv acl2::?erp ?decl ?span ?new-pstate) (parse-declaration pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)