Parse statements, blocks, and related entities.
This clique of mutually recursive functions shares some characteristics with the clique to parse expressions, declarations, and related entities. See parse-exprs/decls for a discussion of technicalities that also apply to this clique.
Function:
(defun parse-statement (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-statement)) (declare (ignorable __function__)) (b* (((reterr) (irr-stmt) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((and token (token-case token :ident)) (b* ((ident (token-ident->unwrap token)) ((erp token2 & parstate) (read-token parstate))) (cond ((token-punctuatorp token2 ":") (b* (((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-labeled :label (label-name ident) :stmt stmt) (span-join span last-span) parstate))) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) (parstate (unread-token parstate)) ((erp expr span parstate) (parse-expression parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (stmt-expr expr) (span-join span last-span) parstate)))))) ((token-punctuatorp token "{") (b* (((erp token2 span2 parstate) (read-token parstate))) (cond ((token-punctuatorp token2 "}") (retok (stmt-compound nil) (span-join span span2) parstate)) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) ((erp items & parstate) (parse-block-item-list parstate)) ((erp last-span parstate) (read-punctuator "}" parstate))) (retok (stmt-compound items) (span-join span last-span) parstate)))))) ((token-punctuatorp token ";") (retok (stmt-expr nil) span parstate)) ((token-keywordp token "case") (b* (((erp cexpr & parstate) (parse-constant-expression parstate)) ((erp & parstate) (read-punctuator ":" parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-labeled :label (label-const cexpr) :stmt stmt) (span-join span last-span) parstate))) ((token-keywordp token "default") (b* (((erp & parstate) (read-punctuator ":" parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-labeled :label (label-default) :stmt stmt) (span-join span last-span) parstate))) ((token-keywordp token "goto") (b* (((erp ident & parstate) (read-identifier parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (stmt-goto ident) (span-join span last-span) parstate))) ((token-keywordp token "continue") (b* (((erp last-span parstate) (read-punctuator ";" parstate))) (retok (stmt-continue) (span-join span last-span) parstate))) ((token-keywordp token "break") (b* (((erp last-span parstate) (read-punctuator ";" parstate))) (retok (stmt-break) (span-join span last-span) parstate))) ((token-keywordp token "return") (b* (((erp token2 span2 parstate) (read-token parstate))) (cond ((token-expression-start-p token2) (b* ((parstate (unread-token parstate)) ((erp expr & parstate) (parse-expression parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (stmt-return expr) (span-join span last-span) parstate))) ((token-punctuatorp token2 ";") (retok (stmt-return nil) (span-join span span2) parstate)) (t (reterr-msg :where (position-to-msg (span->start span2)) :expected "an expression or a semicolon" :found (token-to-msg token2)))))) ((token-keywordp token "if") (b* (((erp & parstate) (read-punctuator "(" parstate)) ((erp expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ")" parstate)) (psize (parsize parstate)) ((erp stmt stmt-span parstate) (parse-statement parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token2 & parstate) (read-token parstate))) (cond ((token-keywordp token2 "else") (b* (((erp stmt-else last-span parstate) (parse-statement parstate))) (retok (make-stmt-ifelse :test expr :then stmt :else stmt-else) (span-join span last-span) parstate))) (t (b* ((parstate (if token2 (unread-token parstate) parstate))) (retok (make-stmt-if :test expr :then stmt) (span-join span stmt-span) parstate)))))) ((token-keywordp token "switch") (b* (((erp & parstate) (read-punctuator "(" parstate)) ((erp expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ")" parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-switch :target expr :body stmt) (span-join span last-span) parstate))) ((token-keywordp token "while") (b* (((erp & parstate) (read-punctuator "(" parstate)) ((erp expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ")" parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-while :test expr :body stmt) (span-join span last-span) parstate))) ((token-keywordp token "do") (b* (((erp stmt & parstate) (parse-statement parstate)) ((erp & parstate) (read-keyword "while" parstate)) ((erp & parstate) (read-punctuator "(" parstate)) ((erp expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ")" parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (make-stmt-dowhile :body stmt :test expr) (span-join span last-span) parstate))) ((token-keywordp token "for") (b* (((erp & parstate) (read-punctuator "(" parstate)) ((erp token2 & parstate) (read-token parstate))) (cond ((token-punctuatorp token2 ";") (b* (((erp token3 span3 parstate) (read-token parstate))) (cond ((token-expression-start-p token3) (b* ((parstate (unread-token parstate)) ((erp test-expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ";" parstate)) ((erp token4 span4 parstate) (read-token parstate))) (cond ((token-expression-start-p token4) (b* ((parstate (unread-token parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ")" parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-expr :init nil :test test-expr :next next-expr :body stmt) (span-join span last-span) parstate))) ((token-punctuatorp token4 ")") (b* (((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-expr :init nil :test test-expr :next nil :body stmt) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span4)) :expected "an expression ~ or a closed parenthesis" :found (token-to-msg token4)))))) ((token-punctuatorp token3 ";") (b* (((erp token4 span4 parstate) (read-token parstate))) (cond ((token-expression-start-p token4) (b* ((parstate (unread-token parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ")" parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-expr :init nil :test nil :next next-expr :body stmt) (span-join span last-span) parstate))) ((token-punctuatorp token4 ")") (b* (((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-expr :init nil :test nil :next nil :body stmt) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span4)) :expected "an expression ~ or a closed parenthesis" :found (token-to-msg token4)))))) (t (reterr-msg :where (position-to-msg (span->start span3)) :expected "an expression ~ or a semicolon" :found (token-to-msg token3)))))) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) ((erp decl/stmt & parstate) (parse-declaration-or-statement parstate))) (amb?-decl/stmt-case decl/stmt :decl (b* ((decl (amb?-decl/stmt-decl->unwrap decl/stmt)) ((erp token3 span3 parstate) (read-token parstate))) (cond ((token-expression-start-p token3) (b* ((parstate (unread-token parstate)) ((erp test-expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ";" parstate)) ((erp token4 span4 parstate) (read-token parstate))) (cond ((token-expression-start-p token4) (b* ((parstate (unread-token parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ")" parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-decl :init decl :test test-expr :next next-expr :body stmt) (span-join span last-span) parstate))) ((token-punctuatorp token4 ")") (b* (((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-decl :init decl :test test-expr :next nil :body stmt) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span4)) :expected "an expression ~ or a closed parenthesis" :found (token-to-msg token4)))))) ((token-punctuatorp token3 ";") (b* (((erp token4 span4 parstate) (read-token parstate))) (cond ((token-expression-start-p token4) (b* ((parstate (unread-token parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ")" parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-decl :init decl :test nil :next next-expr :body stmt) (span-join span last-span) parstate))) ((token-punctuatorp token4 ")") (b* (((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-decl :init decl :test nil :next nil :body stmt) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span4)) :expected "an expression ~ or a closed parenthesis" :found (token-to-msg token4)))))) (t (reterr-msg :where (position-to-msg (span->start span3)) :expected "an expression ~ or a semicolon" :found (token-to-msg token3))))) :stmt (b* ((expr (amb?-decl/stmt-stmt->unwrap decl/stmt)) ((erp token3 span3 parstate) (read-token parstate))) (cond ((token-expression-start-p token3) (b* ((parstate (unread-token parstate)) ((erp test-expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ";" parstate)) ((erp token4 span4 parstate) (read-token parstate))) (cond ((token-expression-start-p token4) (b* ((parstate (unread-token parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ")" parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-expr :init expr :test test-expr :next next-expr :body stmt) (span-join span last-span) parstate))) ((token-punctuatorp token4 ")") (b* (((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-expr :init expr :test test-expr :next nil :body stmt) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span4)) :expected "an expression ~ or a closed parenthesis" :found (token-to-msg token4)))))) ((token-punctuatorp token3 ";") (b* (((erp token4 span4 parstate) (read-token parstate))) (cond ((token-expression-start-p token4) (b* ((parstate (unread-token parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ")" parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-expr :init expr :test nil :next next-expr :body stmt) (span-join span last-span) parstate))) ((token-punctuatorp token4 ")") (b* (((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-expr :init expr :test nil :next nil :body stmt) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span4)) :expected "an expression ~ or a closed parenthesis" :found (token-to-msg token4)))))) (t (reterr-msg :where (position-to-msg (span->start span3)) :expected "an expression ~ or a semicolon" :found (token-to-msg token3))))) :ambig (b* ((decl/expr (amb?-decl/stmt-ambig->unwrap decl/stmt)) ((erp token3 span3 parstate) (read-token parstate))) (cond ((token-expression-start-p token3) (b* ((parstate (unread-token parstate)) ((erp test-expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ";" parstate)) ((erp token4 span4 parstate) (read-token parstate))) (cond ((token-expression-start-p token4) (b* ((parstate (unread-token parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ")" parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-ambig :init decl/expr :test test-expr :next next-expr :body stmt) (span-join span last-span) parstate))) ((token-punctuatorp token4 ")") (b* (((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-ambig :init decl/expr :test test-expr :next nil :body stmt) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span4)) :expected "an expression ~ or a closed parenthesis" :found (token-to-msg token4)))))) ((token-punctuatorp token3 ";") (b* (((erp token4 span4 parstate) (read-token parstate))) (cond ((token-expression-start-p token4) (b* ((parstate (unread-token parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((erp & parstate) (read-punctuator ")" parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-ambig :init decl/expr :test nil :next next-expr :body stmt) (span-join span last-span) parstate))) ((token-punctuatorp token4 ")") (b* (((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-for-ambig :init decl/expr :test nil :next nil :body stmt) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span4)) :expected "an expression ~ or a closed parenthesis" :found (token-to-msg token4)))))) (t (reterr-msg :where (position-to-msg (span->start span3)) :expected "an expression ~ or a semicolon" :found (token-to-msg token3))))))))))) ((token-expression-start-p token) (b* ((parstate (unread-token parstate)) ((erp expr span parstate) (parse-expression parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (stmt-expr expr) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an identifier ~ or a keyword in {~ break, ~ case, ~ continue, ~ default, ~ do, ~ for, ~ goto, ~ if, ~ return, ~ switch, ~ while~ } ~ or a punctuator in {~ \"++\", ~ \"--\", ~ \"+\", ~ \"-\", ~ \"~~\", ~ \"!\", ~ \"*\", ~ \"&\", ~ \"(\", ~ \"{\", ~ \";\"~ }" :found (token-to-msg token)))))))
Function:
(defun parse-block-item (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-block-item)) (declare (ignorable __function__)) (b* (((reterr) (irr-block-item) (irr-span) parstate) ((erp token & parstate) (read-token parstate))) (cond ((and token (token-case token :ident)) (b* (((erp token2 & parstate) (read-token parstate))) (cond ((token-punctuatorp token2 ":") (b* ((parstate (unread-token parstate)) (parstate (unread-token parstate)) ((erp stmt span parstate) (parse-statement parstate))) (retok (block-item-stmt stmt) span parstate))) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) (parstate (unread-token parstate)) ((erp decl/stmt span parstate) (parse-declaration-or-statement parstate))) (amb?-decl/stmt-case decl/stmt :decl (retok (block-item-decl decl/stmt.unwrap) span parstate) :stmt (retok (block-item-stmt (stmt-expr decl/stmt.unwrap)) span parstate) :ambig (retok (block-item-ambig decl/stmt.unwrap) span parstate))))))) ((token-declaration-specifier-start-p token) (b* ((parstate (unread-token parstate)) ((erp decl span parstate) (parse-declaration parstate))) (retok (block-item-decl decl) span parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate)) ((erp stmt span parstate) (parse-statement parstate))) (retok (block-item-stmt stmt) span parstate)))))))
Function:
(defun parse-block-item-list (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-block-item-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) (psize (parsize parstate)) ((erp item span parstate) (parse-block-item parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token "}") (b* ((parstate (unread-token parstate))) (retok (list item) span parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate)) ((erp items last-span parstate) (parse-block-item-list parstate))) (retok (cons item items) (span-join span last-span) parstate)))))))
Theorem:
(defthm return-type-of-parse-statement.stmt (b* (((mv acl2::?erp ?stmt ?span ?new-parstate) (parse-statement parstate))) (stmtp stmt)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-statement.span (b* (((mv acl2::?erp ?stmt ?span ?new-parstate) (parse-statement parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-statement.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?stmt ?span ?new-parstate) (parse-statement parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-block-item.item (b* (((mv acl2::?erp ?item ?span ?new-parstate) (parse-block-item parstate))) (block-itemp item)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-block-item.span (b* (((mv acl2::?erp ?item ?span ?new-parstate) (parse-block-item parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-block-item.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?item ?span ?new-parstate) (parse-block-item parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-block-item-list.items (b* (((mv acl2::?erp ?items ?span ?new-parstate) (parse-block-item-list parstate))) (block-item-listp items)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-block-item-list.span (b* (((mv acl2::?erp ?items ?span ?new-parstate) (parse-block-item-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-block-item-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?items ?span ?new-parstate) (parse-block-item-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-statement-uncond (b* (((mv acl2::?erp ?stmt ?span ?new-parstate) (parse-statement parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-block-item-uncond (b* (((mv acl2::?erp ?item ?span ?new-parstate) (parse-block-item parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-block-item-list-uncond (b* (((mv acl2::?erp ?items ?span ?new-parstate) (parse-block-item-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-statement-cond (b* (((mv acl2::?erp ?stmt ?span ?new-parstate) (parse-statement parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-block-item-cond (b* (((mv acl2::?erp ?item ?span ?new-parstate) (parse-block-item parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-block-item-list-cond (b* (((mv acl2::?erp ?items ?span ?new-parstate) (parse-block-item-list parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)