Parse a declaration or a statement.
(parse-declaration-or-statement parstate) → (mv erp decl/stmt span new-parstate)
This is called when a block item may be a declaration or an expression statement, which have a complex syntactic overlap, as explained in amb-decl/stmt. Thus, this parsing function returns a possibly ambiguous declaration or statement.
We try to parse both a declaration and an expression followed by a semicolon (note that a declaration always ends in semicolon). If only one succeeds, there is no ambiguity, and we return either a declaration or a statement (wrapped); since the statement is always an expression statement, we actually return an expression in this case. If both succeed, there is an ambiguity, which we return as such. If none succeeds, it is an error.
Function:
(defun parse-declaration-or-statement (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-declaration-or-statement)) (declare (ignorable __function__)) (b* (((reterr) (irr-amb?-decl/stmt) (irr-span) parstate) (parstate (record-checkpoint parstate)) (psize (parsize parstate)) ((mv erp expr span-expr parstate) (parse-expression parstate))) (if erp (b* ((parstate (backtrack-checkpoint parstate)) ((unless (<= (parsize parstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize parstate) psize) (b* ((parstate (init-parstate nil nil parstate))) (reterr t))) ((erp decl span parstate) (parse-declaration parstate))) (retok (amb?-decl/stmt-decl decl) span parstate)) (b* (((erp token span-semicolon parstate) (read-token parstate)) (span-stmt (span-join span-expr span-semicolon))) (if (token-punctuatorp token ";") (b* ((parstate (backtrack-checkpoint parstate)) ((unless (<= (parsize parstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize parstate) psize) (b* ((parstate (init-parstate nil nil parstate))) (reterr t))) (parstate (record-checkpoint parstate)) ((mv erp decl span-decl parstate) (parse-declaration parstate))) (if erp (b* ((parstate (backtrack-checkpoint parstate)) ((unless (<= (parsize parstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize parstate) psize) (b* ((parstate (init-parstate nil nil parstate))) (reterr t))) ((mv erp expr1 span-expr1 parstate) (parse-expression parstate)) ((when erp) (raise "Internal error: ~ parsing the same expression ~x0 twice ~ gives the error ~x1." expr erp) (reterr t)) ((unless (equal expr1 expr)) (raise "Internal error: ~ parsing the same expression ~x0 twice ~ gives a different expression ~x1." expr expr1) (reterr t)) ((unless (equal span-expr1 span-expr)) (raise "Internal error: ~ parsing the same expression ~x0 twice ~ gives a different span ~x1 from ~x2." expr span-expr1 span-expr) (reterr t)) ((mv erp span-semicolon1 parstate) (read-punctuator ";" parstate)) ((when erp) (raise "Internal error: ~ parsing the semicolon twice ~ after the same expression ~x0 ~ gives the error ~x1." expr erp) (reterr t)) ((unless (equal span-semicolon1 span-semicolon)) (raise "Internal error: ~ parsing the same semicolon twice ~ after the same expression ~x0 ~ gives a span ~x1 different from ~ the span ~x2 from the previous time." expr span-semicolon1 span-semicolon) (reterr t))) (retok (amb?-decl/stmt-stmt expr) (span-join span-expr span-semicolon) parstate)) (b* ((parstate (clear-checkpoint parstate)) ((unless (equal span-stmt span-decl)) (raise "Internal error: span ~x0 of expression statement ~x1 ~ differs from ~ span ~x2 of declaration ~x3." span-stmt expr span-decl decl) (reterr t))) (retok (amb?-decl/stmt-ambig (make-amb-decl/stmt :stmt expr :decl decl)) span-stmt parstate)))) (b* ((parstate (backtrack-checkpoint parstate)) ((unless (<= (parsize parstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize parstate) psize) (b* ((parstate (init-parstate nil nil parstate))) (reterr t))) ((erp decl span parstate) (parse-declaration parstate))) (retok (amb?-decl/stmt-decl decl) span parstate))))))))
Theorem:
(defthm amb?-decl/stmt-p-of-parse-declaration-or-statement.decl/stmt (b* (((mv acl2::?erp ?decl/stmt ?span ?new-parstate) (parse-declaration-or-statement parstate))) (amb?-decl/stmt-p decl/stmt)) :rule-classes :rewrite)
Theorem:
(defthm spanp-of-parse-declaration-or-statement.span (b* (((mv acl2::?erp ?decl/stmt ?span ?new-parstate) (parse-declaration-or-statement parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-declaration-or-statement.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?decl/stmt ?span ?new-parstate) (parse-declaration-or-statement parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-declaration-or-statement-uncond (b* (((mv acl2::?erp ?decl/stmt ?span ?new-parstate) (parse-declaration-or-statement parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-or-statement-cond (b* (((mv acl2::?erp ?decl/stmt ?span ?new-parstate) (parse-declaration-or-statement parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)