Parse a declaration or a statement.
(parse-declaration-or-statement pstate) → (mv erp decl/stmt span new-pstate)
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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-declaration-or-statement)) (declare (ignorable __function__)) (b* (((reterr) (irr-amb?-decl/stmt) (irr-span) (irr-parstate)) (pstate (record-checkpoint pstate)) (psize (parsize pstate)) ((mv erp expr span-expr pstate) (parse-expression pstate))) (if erp (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) ((erp decl span pstate) (parse-declaration pstate))) (retok (amb?-decl/stmt-decl decl) span pstate)) (b* (((erp token span-semicolon pstate) (read-token pstate)) (span-stmt (span-join span-expr span-semicolon))) (if (equal token (token-punctuator ";")) (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) (pstate (record-checkpoint pstate)) ((mv erp decl span-decl pstate) (parse-declaration pstate))) (if erp (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) ((mv erp expr1 span-expr1 pstate) (parse-expression pstate)) ((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 pstate) (read-punctuator ";" pstate)) ((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) pstate)) (b* ((pstate (clear-checkpoint pstate)) ((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 pstate)))) (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) ((erp decl span pstate) (parse-declaration pstate))) (retok (amb?-decl/stmt-decl decl) span pstate))))))))
Theorem:
(defthm amb?-decl/stmt-p-of-parse-declaration-or-statement.decl/stmt (b* (((mv acl2::?erp ?decl/stmt ?span ?new-pstate) (parse-declaration-or-statement pstate))) (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-pstate) (parse-declaration-or-statement pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm parstatep-of-parse-declaration-or-statement.new-pstate (b* (((mv acl2::?erp ?decl/stmt ?span ?new-pstate) (parse-declaration-or-statement pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-declaration-or-statement-uncond (b* (((mv acl2::?erp ?decl/stmt ?span ?new-pstate) (parse-declaration-or-statement pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-or-statement-cond (b* (((mv acl2::?erp ?decl/stmt ?span ?new-pstate) (parse-declaration-or-statement pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)