Parse expressions, declarations, statements, and related entities.
In accordance with the mutual recursion in the C grammar, and with the mutual recursion exprs/decls/stmts in our abstract syntax, the functions to parse expressions, declarations, statements, and related entities are mutually recursive.
Some functions in this mutually recursive clique call other functions in the same clique on the same input, which therefore does not immediately decrease. Thus, we use a lexicographic measure consisting of the size of the parser state followed by a constant that ``orders'' the functions, based on how the parser makes progress by calling ``smaller'' functions even though the input stays the same. For example, parse-expression calls parse-assignment-expression on the same input; so we assign a smaller constant to the latter, so that it is considered ``smaller'' than the former.
The fact that each function in this clique reduces, or at least does not increase, the size of the input is proved after the functions are admitted in the ACL2 logic. But that fact is needed to prove the termination of some of these functions. For example, parse-conditional-expression calls parse-expression, and then parse-conditional-expression again, under certain conditions. For termination, we need to show that the latter call is performed on a smaller input, which is true for the former call, but at termination time that is not known yet. Thus, we need to add mbt tests about certain inputs decreasing in size, which we verify when we verify the guards, after proving the input size inequalities for all the functions in the clique.
Function:
(defun parse-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) (psize (parsize parstate)) ((erp expr span parstate) (parse-assignment-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-expression-rest expr span parstate))))
Function:
(defun parse-expression-rest (prev-expr prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (not (token-punctuatorp token ","))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (expr-fix prev-expr) (span-fix prev-span) parstate))) (psize (parsize parstate)) ((erp expr expr-span parstate) (parse-assignment-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (curr-expr (make-expr-comma :first prev-expr :next expr)) (curr-span (span-join prev-span expr-span))) (parse-expression-rest curr-expr curr-span parstate))))
Function:
(defun parse-assignment-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-assignment-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) (psize (parsize parstate)) ((erp expr span parstate) (parse-conditional-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((when (not (expr-unary/postfix/primary-p expr))) (retok expr span parstate)) ((erp token & parstate) (read-token parstate)) ((when (not (token-assignment-operator-p token))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok expr span parstate))) (asgop (token-to-assignment-operator token)) ((erp expr2 span2 parstate) (parse-assignment-expression parstate))) (retok (make-expr-binary :op asgop :arg1 expr :arg2 expr2) (span-join span span2) parstate))))
Function:
(defun parse-conditional-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-conditional-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) (psize (parsize parstate)) ((erp expr span parstate) (parse-logical-or-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate)) ((when (not (token-punctuatorp token "?"))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok expr span parstate))) (psize (parsize parstate)) ((erp expr2 & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp & parstate) (read-punctuator ":" parstate)) ((erp expr3 span3 parstate) (parse-conditional-expression parstate))) (retok (make-expr-cond :test expr :then expr2 :else expr3) (span-join span span3) parstate))))
Function:
(defun parse-logical-or-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-logical-or-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) (psize (parsize parstate)) ((erp expr span parstate) (parse-logical-and-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-logical-or-expression-rest expr span parstate))))
Function:
(defun parse-logical-or-expression-rest (prev-expr prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-logical-or-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (not (token-punctuatorp token "||"))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (expr-fix prev-expr) (span-fix prev-span) parstate))) (psize (parsize parstate)) ((erp expr expr-span parstate) (parse-logical-and-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (curr-expr (make-expr-binary :op (binop-logor) :arg1 prev-expr :arg2 expr)) (curr-span (span-join prev-span expr-span))) (parse-logical-or-expression-rest curr-expr curr-span parstate))))
Function:
(defun parse-logical-and-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-logical-and-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) (psize (parsize parstate)) ((erp expr span parstate) (parse-inclusive-or-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-logical-and-expression-rest expr span parstate))))
Function:
(defun parse-logical-and-expression-rest (prev-expr prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-logical-and-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (not (token-punctuatorp token "&&"))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (expr-fix prev-expr) (span-fix prev-span) parstate))) (psize (parsize parstate)) ((erp expr expr-span parstate) (parse-inclusive-or-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (curr-expr (make-expr-binary :op (binop-logand) :arg1 prev-expr :arg2 expr)) (curr-span (span-join prev-span expr-span))) (parse-logical-and-expression-rest curr-expr curr-span parstate))))
Function:
(defun parse-inclusive-or-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-inclusive-or-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) (psize (parsize parstate)) ((erp expr span parstate) (parse-exclusive-or-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-inclusive-or-expression-rest expr span parstate))))
Function:
(defun parse-inclusive-or-expression-rest (prev-expr prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-inclusive-or-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (not (token-punctuatorp token "|"))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (expr-fix prev-expr) (span-fix prev-span) parstate))) (psize (parsize parstate)) ((erp expr expr-span parstate) (parse-exclusive-or-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (curr-expr (make-expr-binary :op (binop-bitior) :arg1 prev-expr :arg2 expr)) (curr-span (span-join prev-span expr-span))) (parse-inclusive-or-expression-rest curr-expr curr-span parstate))))
Function:
(defun parse-exclusive-or-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-exclusive-or-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) (psize (parsize parstate)) ((erp expr span parstate) (parse-and-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-exclusive-or-expression-rest expr span parstate))))
Function:
(defun parse-exclusive-or-expression-rest (prev-expr prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-exclusive-or-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (not (token-punctuatorp token "^"))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (expr-fix prev-expr) (span-fix prev-span) parstate))) (psize (parsize parstate)) ((erp expr expr-span parstate) (parse-and-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (curr-expr (make-expr-binary :op (binop-bitxor) :arg1 prev-expr :arg2 expr)) (curr-span (span-join prev-span expr-span))) (parse-exclusive-or-expression-rest curr-expr curr-span parstate))))
Function:
(defun parse-and-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-and-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) (psize (parsize parstate)) ((erp expr span parstate) (parse-equality-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-and-expression-rest expr span parstate))))
Function:
(defun parse-and-expression-rest (prev-expr prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-and-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (not (token-punctuatorp token "&"))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (expr-fix prev-expr) (span-fix prev-span) parstate))) (psize (parsize parstate)) ((erp expr expr-span parstate) (parse-equality-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (curr-expr (make-expr-binary :op (binop-bitand) :arg1 prev-expr :arg2 expr)) (curr-span (span-join prev-span expr-span))) (parse-and-expression-rest curr-expr curr-span parstate))))
Function:
(defun parse-equality-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-equality-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) (psize (parsize parstate)) ((erp expr span parstate) (parse-relational-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-equality-expression-rest expr span parstate))))
Function:
(defun parse-equality-expression-rest (prev-expr prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-equality-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (not (token-equality-operator-p token))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (expr-fix prev-expr) (span-fix prev-span) parstate))) (psize (parsize parstate)) ((erp expr expr-span parstate) (parse-relational-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (op (token-to-equality-operator token)) (curr-expr (make-expr-binary :op op :arg1 prev-expr :arg2 expr)) (curr-span (span-join prev-span expr-span))) (parse-equality-expression-rest curr-expr curr-span parstate))))
Function:
(defun parse-relational-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-relational-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) (psize (parsize parstate)) ((erp expr span parstate) (parse-shift-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-relational-expression-rest expr span parstate))))
Function:
(defun parse-relational-expression-rest (prev-expr prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-relational-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (not (token-relational-operator-p token))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (expr-fix prev-expr) (span-fix prev-span) parstate))) (psize (parsize parstate)) ((erp expr expr-span parstate) (parse-shift-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (op (token-to-relational-operator token)) (curr-expr (make-expr-binary :op op :arg1 prev-expr :arg2 expr)) (curr-span (span-join prev-span expr-span))) (parse-relational-expression-rest curr-expr curr-span parstate))))
Function:
(defun parse-shift-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-shift-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) (psize (parsize parstate)) ((erp expr span parstate) (parse-additive-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-shift-expression-rest expr span parstate))))
Function:
(defun parse-shift-expression-rest (prev-expr prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-shift-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (not (token-shift-operator-p token))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (expr-fix prev-expr) (span-fix prev-span) parstate))) (psize (parsize parstate)) ((erp expr expr-span parstate) (parse-additive-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (op (token-to-shift-operator token)) (curr-expr (make-expr-binary :op op :arg1 prev-expr :arg2 expr)) (curr-span (span-join prev-span expr-span))) (parse-shift-expression-rest curr-expr curr-span parstate))))
Function:
(defun parse-additive-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-additive-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) (psize (parsize parstate)) ((erp expr span parstate) (parse-multiplicative-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-additive-expression-rest expr span parstate))))
Function:
(defun parse-additive-expression-rest (prev-expr prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-additive-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (not (token-additive-operator-p token))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (expr-fix prev-expr) (span-fix prev-span) parstate))) (psize (parsize parstate)) ((erp expr expr-span parstate) (parse-multiplicative-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (op (token-to-additive-operator token)) (curr-expr (make-expr-binary :op op :arg1 prev-expr :arg2 expr)) (curr-span (span-join prev-span expr-span))) (parse-additive-expression-rest curr-expr curr-span parstate))))
Function:
(defun parse-multiplicative-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-multiplicative-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) (psize (parsize parstate)) ((erp expr span parstate) (parse-cast-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-multiplicative-expression-rest expr span parstate))))
Function:
(defun parse-multiplicative-expression-rest (prev-expr prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-multiplicative-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (not (token-multiplicative-operator-p token))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (expr-fix prev-expr) (span-fix prev-span) parstate))) (psize (parsize parstate)) ((erp expr expr-span parstate) (parse-cast-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (op (token-to-multiplicative-operator token)) (curr-expr (make-expr-binary :op op :arg1 prev-expr :arg2 expr)) (curr-span (span-join prev-span expr-span))) (parse-multiplicative-expression-rest curr-expr curr-span parstate))))
Function:
(defun parse-cast-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-cast-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-punctuatorp token "(") (b* (((erp token2 & parstate) (read-token parstate)) ((when (and (token-punctuatorp token2 "{") (parstate->gcc parstate))) (b* (((erp token3 & parstate) (read-token parstate))) (cond ((token-punctuatorp token3 "}") (b* (((erp last-span parstate) (read-punctuator ")" parstate))) (retok (expr-stmt nil) (span-join span last-span) parstate))) (t (b* ((parstate (if token3 (unread-token parstate) parstate)) ((erp items & parstate) (parse-block-item-list parstate)) ((erp & parstate) (read-punctuator "}" parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (expr-stmt items) (span-join span last-span) parstate)))))) (parstate (if token2 (unread-token parstate) parstate)) (checkpoint (parstate->tokens-read parstate)) (psize (parsize parstate)) ((erp expr/tyname & parstate) (parse-expression-or-type-name parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (amb?-expr/tyname-case expr/tyname :tyname (b* (((erp & parstate) (read-punctuator ")" parstate)) ((erp token2 & parstate) (read-token parstate))) (cond ((token-punctuatorp token2 "{") (b* ((parstate (unread-token parstate))) (parse-compound-literal expr/tyname.unwrap span parstate))) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) ((erp expr last-span parstate) (parse-cast-expression parstate))) (retok (make-expr-cast :type expr/tyname.unwrap :arg expr) (span-join span last-span) parstate))))) :expr (b* ((parstate (unread-to-token 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 (unread-token parstate))) (parse-postfix-expression parstate)) :ambig (b* (((erp & parstate) (read-punctuator ")" parstate)) ((erp incdecops parstate) (parse-*-increment/decrement parstate)) ((erp token2 & parstate) (read-token parstate))) (cond ((token-punctuatorp token2 "(") (b* ((parstate (unread-token parstate))) (cond ((consp incdecops) (b* (((erp expr last-span parstate) (parse-postfix-expression parstate))) (retok (make-expr-cast/call-ambig :type/fun expr/tyname.unwrap :inc/dec incdecops :arg/rest expr) (span-join span last-span) parstate))) (t (b* (((erp expr last-span parstate) (parse-cast-expression parstate))) (cond ((expr-postfix/primary-p expr) (retok (make-expr-cast/call-ambig :type/fun expr/tyname.unwrap :inc/dec incdecops :arg/rest expr) (span-join span last-span) parstate)) (t (retok (make-expr-cast :type (amb-expr/tyname->tyname expr/tyname.unwrap) :arg expr) (span-join span last-span) parstate)))))))) ((token-punctuatorp token2 "*") (b* (((erp expr last-span parstate) (parse-cast-expression parstate))) (retok (make-expr-cast/mul-ambig :type/arg1 expr/tyname.unwrap :inc/dec incdecops :arg/arg2 expr) (span-join span last-span) parstate))) ((or (token-punctuatorp token2 "+") (token-punctuatorp token2 "-")) (b* (((erp expr last-span parstate) (parse-multiplicative-expression parstate))) (retok (make-expr-cast/add-or-cast/sub-ambig token2 expr/tyname.unwrap incdecops expr) (span-join span last-span) parstate))) ((token-punctuatorp token2 "&") (b* (((erp expr last-span parstate) (parse-equality-expression parstate))) (retok (make-expr-cast/and-ambig :type/arg1 expr/tyname.unwrap :inc/dec incdecops :arg/arg2 expr) (span-join span last-span) parstate))) ((token-unary-expression-start-p token2) (b* ((parstate (unread-token parstate)) ((erp expr last-span parstate) (parse-unary-expression parstate)) (expr (make-expr-unary-with-preinc/predec-ops incdecops expr)) (tyname (amb-expr/tyname->tyname expr/tyname.unwrap))) (retok (make-expr-cast :type tyname :arg expr) (span-join span last-span) parstate))) (t (b* ((parstate (unread-to-token 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 (unread-token parstate))) (parse-postfix-expression parstate)))))))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (parse-unary-expression parstate)))))))
Function:
(defun parse-unary-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-unary-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-primary-expression-start-p token) (b* ((parstate (unread-token parstate))) (parse-postfix-expression parstate))) ((token-preinc/predec-operator-p token) (b* (((erp expr last-span parstate) (parse-unary-expression parstate)) (unop (token-to-preinc/predec-operator token))) (retok (make-expr-unary :op unop :arg expr) (span-join span last-span) parstate))) ((token-unary-operator-p token) (b* (((erp expr last-span parstate) (parse-cast-expression parstate)) (unop (token-to-unary-operator token))) (retok (make-expr-unary :op unop :arg expr) (span-join span last-span) parstate))) ((token-keywordp token "sizeof") (b* (((erp token2 & parstate) (read-token parstate))) (cond ((token-punctuatorp token2 "(") (b* (((erp token2 & parstate) (read-token parstate)) ((when (and (token-punctuatorp token2 "{") (parstate->gcc parstate))) (b* (((erp token3 & parstate) (read-token parstate))) (cond ((token-punctuatorp token3 "}") (b* (((erp last-span parstate) (read-punctuator ")" parstate))) (retok (expr-stmt nil) (span-join span last-span) parstate))) (t (b* ((parstate (if token3 (unread-token parstate) parstate)) ((erp items & parstate) (parse-block-item-list parstate)) ((erp & parstate) (read-punctuator "}" parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (expr-stmt items) (span-join span last-span) parstate)))))) (parstate (if token2 (unread-token parstate) parstate)) ((erp expr/tyname & parstate) (parse-expression-or-type-name parstate)) ((erp last-span parstate) (read-punctuator ")" parstate)) (expr (amb?-expr/tyname-case expr/tyname :expr (make-expr-unary :op (unop-sizeof) :arg expr/tyname.unwrap) :tyname (expr-sizeof expr/tyname.unwrap) :ambig (expr-sizeof-ambig expr/tyname.unwrap)))) (retok expr (span-join span last-span) parstate))) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) ((erp expr last-span parstate) (parse-unary-expression parstate))) (retok (make-expr-unary :op (unop-sizeof) :arg expr) (span-join span last-span) parstate)))))) ((or (token-keywordp token "_Alignof") (token-keywordp token "__alignof") (token-keywordp token "__alignof__")) (b* (((erp & parstate) (read-punctuator "(" parstate)) ((erp tyname & parstate) (parse-type-name parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (make-expr-alignof :type tyname :uscores (cond ((token-keywordp token "_Alignof") (keyword-uscores-none)) ((token-keywordp token "__alignof") (keyword-uscores-start)) ((token-keywordp token "__alignof__") (keyword-uscores-both)))) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an identifier ~ or a constant ~ or a string literal ~ or a keyword in {~ _Alignof, ~ _Generic, ~ sizeof~ } ~ or a punctuator in {~ \"++\", ~ \"--\", ~ \"+\", ~ \"-\", ~ \"~~\", ~ \"!\", ~ \"*\", ~ \"&\", ~ \"(\"~ }" :found (token-to-msg token)))))))
Function:
(defun parse-postfix-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-postfix-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-punctuatorp token "(") (b* ((psize (parsize parstate)) ((erp expr/tyname & parstate) (parse-expression-or-type-name parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp close-paren-span parstate) (read-punctuator ")" parstate))) (amb?-expr/tyname-case expr/tyname :tyname (parse-compound-literal expr/tyname.unwrap (span-join span close-paren-span) parstate) :expr (b* ((prev-expr (expr-paren expr/tyname.unwrap)) (prev-span (span-join span close-paren-span))) (parse-postfix-expression-rest prev-expr prev-span parstate)) :ambig (b* (((erp token2 & parstate) (read-token parstate))) (cond ((token-punctuatorp token2 "{") (b* ((parstate (unread-token parstate)) (tyname (amb-expr/tyname->tyname expr/tyname.unwrap))) (parse-compound-literal tyname (span-join span close-paren-span) parstate))) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) (expr (amb-expr/tyname->expr expr/tyname.unwrap)) (prev-expr (expr-paren expr)) (prev-span (span-join span close-paren-span))) (parse-postfix-expression-rest prev-expr prev-span parstate)))))))) (t (b* ((parstate (if token (unread-token parstate) parstate)) (psize (parsize parstate)) ((erp expr span parstate) (parse-primary-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-postfix-expression-rest expr span parstate)))))))
Function:
(defun parse-postfix-expression-rest (prev-expr prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-postfix-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-punctuatorp token "[") (b* ((psize (parsize parstate)) ((erp expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp last-span parstate) (read-punctuator "]" parstate)) (curr-expr (make-expr-arrsub :arg1 prev-expr :arg2 expr)) (curr-span (span-join prev-span last-span))) (parse-postfix-expression-rest curr-expr curr-span parstate))) ((token-punctuatorp token "(") (b* ((psize (parsize parstate)) ((erp exprs & parstate) (parse-argument-expressions parstate)) ((unless (mbt (<= (parsize parstate) psize))) (reterr :impossible)) ((erp last-span parstate) (read-punctuator ")" parstate)) (curr-expr (make-expr-funcall :fun prev-expr :args exprs)) (curr-span (span-join prev-span last-span))) (parse-postfix-expression-rest curr-expr curr-span parstate))) ((token-punctuatorp token ".") (b* (((erp ident ident-span parstate) (read-identifier parstate)) (curr-expr (make-expr-member :arg prev-expr :name ident)) (curr-span (span-join prev-span ident-span))) (parse-postfix-expression-rest curr-expr curr-span parstate))) ((token-punctuatorp token "->") (b* (((erp ident ident-span parstate) (read-identifier parstate)) (curr-expr (make-expr-memberp :arg prev-expr :name ident)) (curr-span (span-join prev-span ident-span))) (parse-postfix-expression-rest curr-expr curr-span parstate))) ((token-punctuatorp token "++") (b* ((curr-expr (make-expr-unary :op (unop-postinc) :arg prev-expr)) (curr-span (span-join prev-span span))) (parse-postfix-expression-rest curr-expr curr-span parstate))) ((token-punctuatorp token "--") (b* ((curr-expr (make-expr-unary :op (unop-postdec) :arg prev-expr)) (curr-span (span-join prev-span span))) (parse-postfix-expression-rest curr-expr curr-span parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (expr-fix prev-expr) (span-fix prev-span) parstate)))))))
Function:
(defun parse-argument-expressions (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-argument-expressions)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp token & parstate) (read-token parstate))) (cond ((token-expression-start-p token) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp expr span parstate) (parse-assignment-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (curr-exprs (list expr)) (curr-span span)) (parse-argument-expressions-rest curr-exprs curr-span parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok nil (irr-span) parstate)))))))
Function:
(defun parse-argument-expressions-rest (prev-exprs prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (expr-listp prev-exprs) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-argument-expressions-rest)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (not (token-punctuatorp token ","))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (expr-list-fix prev-exprs) (span-fix prev-span) parstate))) (psize (parsize parstate)) ((erp expr span parstate) (parse-assignment-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (curr-exprs (append prev-exprs (list expr))) (curr-span (span-join prev-span span))) (parse-argument-expressions-rest curr-exprs curr-span parstate))))
Function:
(defun parse-primary-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-primary-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((and token (token-case token :ident)) (retok (expr-ident (token-ident->unwrap token)) span parstate)) ((and token (token-case token :const)) (retok (expr-const (token-const->unwrap token)) span parstate)) ((and token (token-case token :string)) (b* (((erp strings last-span parstate) (parse-*-stringlit parstate))) (retok (expr-string (cons (token-string->unwrap token) strings)) (if strings (span-join span last-span) span) parstate))) ((token-punctuatorp token "(") (b* (((erp token2 & parstate) (read-token parstate))) (cond ((and (token-punctuatorp token2 "{") (parstate->gcc parstate)) (b* (((erp token3 & parstate) (read-token parstate))) (cond ((token-punctuatorp token3 "}") (b* (((erp last-span parstate) (read-punctuator ")" parstate))) (retok (expr-stmt nil) (span-join span last-span) parstate))) (t (b* ((parstate (if token3 (unread-token parstate) parstate)) ((erp items & parstate) (parse-block-item-list parstate)) ((erp & parstate) (read-punctuator "}" parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (expr-stmt items) (span-join span last-span) parstate)))))) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) ((erp expr & parstate) (parse-expression parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (expr-paren expr) (span-join span last-span) parstate)))))) ((token-keywordp token "_Generic") (b* (((erp & parstate) (read-punctuator "(" parstate)) (psize (parsize parstate)) ((erp expr & parstate) (parse-assignment-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp & parstate) (read-punctuator "," parstate)) (psize (parsize parstate)) ((erp genassoc genassoc-span parstate) (parse-generic-association parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp genassocs & parstate) (parse-generic-associations-rest (list genassoc) genassoc-span parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (make-expr-gensel :control expr :assocs genassocs) (span-join span last-span) parstate))) ((token-keywordp token "__builtin_types_compatible_p") (b* (((erp & parstate) (read-punctuator "(" parstate)) (psize (parsize parstate)) ((erp type1 & parstate) (parse-type-name parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp & parstate) (read-punctuator "," parstate)) ((erp type2 & parstate) (parse-type-name parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (make-expr-tycompat :type1 type1 :type2 type2) (span-join span last-span) parstate))) ((token-keywordp token "__builtin_offsetof") (b* (((erp & parstate) (read-punctuator "(" parstate)) (psize (parsize parstate)) ((erp tyname & parstate) (parse-type-name parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp & parstate) (read-punctuator "," parstate)) ((erp memdes & parstate) (parse-member-designor parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (make-expr-offsetof :type tyname :member memdes) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an identifier ~ or a constant ~ or a string literal ~ or an open parenthesis ~ or the keyword _Generic" :found (token-to-msg token)))))))
Function:
(defun parse-compound-literal (tyname first-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (tynamep tyname) (spanp first-span) (parstatep parstate)))) (let ((__function__ 'parse-compound-literal)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) parstate) ((erp & parstate) (read-punctuator "{" parstate)) ((erp desiniters final-comma & parstate) (parse-initializer-list parstate)) ((erp last-span parstate) (read-punctuator "}" parstate))) (retok (make-expr-complit :type tyname :elems desiniters :final-comma final-comma) (span-join first-span last-span) parstate))))
Function:
(defun parse-generic-association (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-generic-association)) (declare (ignorable __function__)) (b* (((reterr) (irr-genassoc) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-type-name-start-p token) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp tyname & parstate) (parse-type-name parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp & parstate) (read-punctuator ":" parstate)) ((erp expr last-span parstate) (parse-assignment-expression parstate))) (retok (make-genassoc-type :type tyname :expr expr) (span-join span last-span) parstate))) ((token-keywordp token "default") (b* (((erp & parstate) (read-punctuator ":" parstate)) ((erp expr last-span parstate) (parse-assignment-expression parstate))) (retok (genassoc-default expr) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an identifier ~ or a keyword in {~ _Alignas, ~ _Atomic, ~ _Bool, ~ _Complex, ~ char, ~ const, ~ double, ~ enum, ~ float, ~ int, ~ long, ~ restrict, ~ short, ~ signed, ~ struct, ~ union, ~ unsigned, ~ void, ~ volatile~ }" :found (token-to-msg token)))))))
Function:
(defun parse-generic-associations-rest (prev-genassocs prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (genassoc-listp prev-genassocs) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-generic-associations-rest)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (not (token-punctuatorp token ","))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (genassoc-list-fix prev-genassocs) (span-fix prev-span) parstate))) (psize (parsize parstate)) ((erp genassoc span parstate) (parse-generic-association parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (curr-genassocs (append prev-genassocs (list genassoc))) (curr-span (span-join prev-span span))) (parse-generic-associations-rest curr-genassocs curr-span parstate))))
Function:
(defun parse-member-designor (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-member-designor)) (declare (ignorable __function__)) (b* (((reterr) (irr-member-designor) (irr-span) parstate) ((erp ident span parstate) (read-identifier parstate)) (curr-memdes (member-designor-ident ident)) (curr-span span)) (parse-member-designor-rest curr-memdes curr-span parstate))))
Function:
(defun parse-member-designor-rest (prev-memdes prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (member-designorp prev-memdes) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-member-designor-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-member-designor) (irr-span) parstate) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token ".") (b* (((erp ident span parstate) (read-identifier parstate)) (curr-memdes (make-member-designor-dot :member prev-memdes :name ident)) (curr-span (span-join prev-span span))) (parse-member-designor-rest curr-memdes curr-span parstate))) ((token-punctuatorp token "[") (b* ((psize (parsize parstate)) ((erp index & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp span parstate) (read-punctuator "]" parstate)) (curr-memdes (make-member-designor-sub :member prev-memdes :index index)) (curr-span (span-join prev-span span))) (parse-member-designor-rest curr-memdes curr-span parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (member-designor-fix prev-memdes) (span-fix prev-span) parstate)))))))
Function:
(defun parse-constant-expression (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-constant-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-const-expr) (irr-span) parstate) ((erp expr span parstate) (parse-conditional-expression parstate))) (retok (const-expr expr) span parstate))))
Function:
(defun parse-static-assert-declaration (first-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (spanp first-span) (parstatep parstate)))) (let ((__function__ 'parse-static-assert-declaration)) (declare (ignorable __function__)) (b* (((reterr) (irr-statassert) (irr-span) parstate) ((erp & parstate) (read-punctuator "(" parstate)) ((erp cexpr & parstate) (parse-constant-expression parstate)) ((erp & parstate) (read-punctuator "," parstate)) ((erp stringlit & parstate) (read-stringlit parstate)) ((erp stringlits & parstate) (parse-*-stringlit parstate)) ((erp & parstate) (read-punctuator ")" parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (make-statassert :test cexpr :message (cons stringlit stringlits)) (span-join first-span last-span) parstate))))
Function:
(defun parse-designator (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-designator)) (declare (ignorable __function__)) (b* (((reterr) (irr-designor) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-punctuatorp token "[") (b* (((erp cexpr & parstate) (parse-constant-expression parstate)) ((erp last-span parstate) (read-punctuator "]" parstate))) (retok (designor-sub cexpr) (span-join span last-span) parstate))) ((token-punctuatorp token ".") (b* (((erp ident last-span parstate) (read-identifier parstate))) (retok (designor-dot ident) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an open square bracket ~ or a dot" :found (token-to-msg token)))))))
Function:
(defun parse-designator-list (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-designator-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) (psize (parsize parstate)) ((erp designor span parstate) (parse-designator parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate)) ((when (not (token-designator-start-p token))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list designor) span parstate))) (parstate (unread-token parstate)) ((erp designors more-span parstate) (parse-designator-list parstate))) (retok (cons designor designors) (span-join span more-span) parstate))))
Function:
(defun parse-initializer (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-initializer)) (declare (ignorable __function__)) (b* (((reterr) (irr-initer) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-expression-start-p token) (b* ((parstate (unread-token parstate)) ((erp expr span parstate) (parse-assignment-expression parstate))) (retok (initer-single expr) span parstate))) ((token-punctuatorp token "{") (b* (((erp desiniters final-comma & parstate) (parse-initializer-list parstate)) ((erp last-span parstate) (read-punctuator "}" parstate))) (retok (make-initer-list :elems desiniters :final-comma final-comma) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an identifier ~ or a constant ~ or a string literal ~ or a keyword in {~ _Alignof, ~ _Generic, ~ sizeof~ } ~ or a punctuator in {~ \"++\", ~ \"--\", ~ \"+\", ~ \"-\", ~ \"~~\", ~ \"!\", ~ \"*\", ~ \"&\", ~ \"(\", ~ \"{\"~ }" :found (token-to-msg token)))))))
Function:
(defun parse-designation?-initializer (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-designation?-initializer)) (declare (ignorable __function__)) (b* (((reterr) (irr-desiniter) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-designation-start-p token) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp designors span parstate) (parse-designator-list parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp & parstate) (read-punctuator "=" parstate)) ((erp initer last-span parstate) (parse-initializer parstate))) (retok (make-desiniter :design designors :init initer) (span-join span last-span) parstate))) ((token-initializer-start-p token) (b* ((parstate (unread-token parstate)) ((erp initer span parstate) (parse-initializer parstate))) (retok (make-desiniter :design nil :init initer) span parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an identifier ~ or a constant ~ or a string literal ~ or a keyword in {~ _Alignof, ~ _Generic, ~ sizeof~ } ~ or a punctuator in {~ \"++\", ~ \"--\", ~ \"+\", ~ \"-\", ~ \"~~\", ~ \"!\", ~ \"*\", ~ \"&\", ~ \"(\", ~ \"{\"~ }" :found (token-to-msg token)))))))
Function:
(defun parse-initializer-list (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-initializer-list)) (declare (ignorable __function__)) (b* (((reterr) nil nil (irr-span) parstate) (psize (parsize parstate)) ((erp desiniter span parstate) (parse-designation?-initializer parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token ",") (b* (((erp token2 span2 parstate) (read-token parstate))) (cond ((token-punctuatorp token2 "}") (b* ((parstate (unread-token parstate))) (retok (list desiniter) t (span-join span span2) parstate))) ((token-designation?-initializer-start-p token2) (b* ((parstate (unread-token parstate)) ((erp desiniters final-comma last-span parstate) (parse-initializer-list parstate))) (retok (cons desiniter desiniters) final-comma (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span2)) :expected "an identifier ~ or a constant ~ or a string literal ~ or a keyword in {~ _Alignof, ~ _Generic, ~ sizeof~ } ~ or a punctuator in {~ \"++\", ~ \"--\", ~ \"+\", ~ \"-\", ~ \"~~\", ~ \"!\", ~ \"*\", ~ \"&\", ~ \"(\", ~ \"{\"~ }" :found (token-to-msg token2)))))) ((token-punctuatorp token "}") (b* ((parstate (unread-token parstate))) (retok (list desiniter) nil span parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an identifier ~ or a constant ~ or a string literal ~ or a keyword in {~ _Alignof, ~ _Generic, ~ sizeof~ } ~ or a punctuator in {~ \"++\", ~ \"--\", ~ \"+\", ~ \"-\", ~ \"~~\", ~ \"!\", ~ \"*\", ~ \"&\", ~ \"(\", ~ \"{\", ~ \"}\", ~ \",\"~ }" :found (token-to-msg token)))))))
Function:
(defun parse-enumerator (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-enumerator)) (declare (ignorable __function__)) (b* (((reterr) (irr-enumer) (irr-span) parstate) ((erp ident span parstate) (read-identifier parstate)) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token "=") (b* (((erp cexpr last-span parstate) (parse-constant-expression parstate))) (retok (make-enumer :name ident :value cexpr) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (make-enumer :name ident :value nil) span parstate)))))))
Function:
(defun parse-enumerator-list (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-enumerator-list)) (declare (ignorable __function__)) (b* (((reterr) nil nil (irr-span) parstate) (psize (parsize parstate)) ((erp enumer enumer-span parstate) (parse-enumerator parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token span parstate) (read-token parstate))) (cond ((token-punctuatorp token ",") (b* (((erp token2 span2 parstate) (read-token parstate))) (cond ((and token2 (token-case token2 :ident)) (b* ((parstate (unread-token parstate)) ((erp enumers final-comma enumers-span parstate) (parse-enumerator-list parstate))) (retok (cons enumer enumers) final-comma (span-join enumer-span enumers-span) parstate))) ((token-punctuatorp token2 "}") (b* ((parstate (unread-token parstate))) (retok (list enumer) t (span-join enumer-span span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span2)) :expected "an identifier ~ or a closed curly brace" :found (token-to-msg token2)))))) ((token-punctuatorp token "}") (b* ((parstate (unread-token parstate))) (retok (list enumer) nil enumer-span parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "a comma ~ or a closed curly brace" :found (token-to-msg token)))))))
Function:
(defun parse-specifier/qualifier (tyspec-seenp parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (booleanp tyspec-seenp) (parstatep parstate)))) (let ((__function__ 'parse-specifier/qualifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-spec/qual) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-type-specifier-keyword-p token) (retok (spec/qual-tyspec (token-to-type-specifier-keyword token)) span parstate)) ((token-keywordp token "_Atomic") (b* (((erp token2 & parstate) (read-token parstate))) (cond ((token-punctuatorp token2 "(") (if tyspec-seenp (b* ((parstate (unread-token parstate))) (retok (spec/qual-tyqual (type-qual-atomic)) span parstate)) (b* (((erp tyname & parstate) (parse-type-name parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (spec/qual-tyspec (type-spec-atomic tyname)) (span-join span last-span) parstate)))) (t (b* ((parstate (if token2 (unread-token parstate) parstate))) (retok (spec/qual-tyqual (type-qual-atomic)) span parstate)))))) ((token-keywordp token "struct") (b* (((erp strunispec last-span parstate) (parse-struct-or-union-specifier parstate))) (retok (spec/qual-tyspec (type-spec-struct strunispec)) (span-join span last-span) parstate))) ((token-keywordp token "union") (b* (((erp strunispec last-span parstate) (parse-struct-or-union-specifier parstate))) (retok (spec/qual-tyspec (type-spec-union strunispec)) (span-join span last-span) parstate))) ((token-keywordp token "enum") (b* (((erp enumspec last-span parstate) (parse-enum-specifier span parstate))) (retok (spec/qual-tyspec (type-spec-enum enumspec)) (span-join span last-span) parstate))) ((and token (token-case token :ident)) (retok (spec/qual-tyspec (type-spec-typedef (token-ident->unwrap token))) span parstate)) ((or (token-keywordp token "typeof") (token-keywordp token "__typeof") (token-keywordp token "__typeof__")) (b* ((uscores (cond ((token-keywordp token "typeof") (keyword-uscores-none)) ((token-keywordp token "__typeof") (keyword-uscores-start)) ((token-keywordp token "__typeof__") (keyword-uscores-both)))) ((erp & parstate) (read-punctuator "(" parstate)) ((erp expr/tyname & parstate) (parse-expression-or-type-name parstate)) ((erp last-span parstate) (read-punctuator ")" parstate)) (tyspec (amb?-expr/tyname-case expr/tyname :expr (make-type-spec-typeof-expr :expr expr/tyname.unwrap :uscores uscores) :tyname (make-type-spec-typeof-type :type expr/tyname.unwrap :uscores uscores) :ambig (make-type-spec-typeof-ambig :expr/type expr/tyname.unwrap :uscores uscores)))) (retok (spec/qual-tyspec tyspec) (span-join span last-span) parstate))) ((token-type-qualifier-p token) (retok (spec/qual-tyqual (token-to-type-qualifier token)) span parstate)) ((token-keywordp token "_Alignas") (b* (((erp alignspec last-span parstate) (parse-alignment-specifier span parstate))) (retok (spec/qual-align alignspec) (span-join span last-span) parstate))) ((or (token-keywordp token "__attribute") (token-keywordp token "__attribute__")) (b* ((uscores (token-keywordp token "__attribute__")) ((erp attrspec last-span parstate) (parse-attribute-specifier uscores span parstate))) (retok (spec/qual-attrib attrspec) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an identifier ~ or a keyword in {~ _Alignas, ~ _Atomic, ~ _Bool, ~ _Complex, ~ char, ~ const, ~ double, ~ enum, ~ float, ~ int, ~ long, ~ restrict, ~ short, ~ signed, ~ struct, ~ union, ~ unsigned, ~ void, ~ volatile~ }" :found (token-to-msg token)))))))
Function:
(defun parse-specifier-qualifier-list (tyspec-seenp parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (booleanp tyspec-seenp) (parstatep parstate)))) (let ((__function__ 'parse-specifier-qualifier-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) (psize (parsize parstate)) ((erp specqual first-span parstate) (parse-specifier/qualifier tyspec-seenp parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (tyspec-seenp (or tyspec-seenp (spec/qual-case specqual :tyspec))) ((erp token & parstate) (read-token parstate))) (cond ((and token (token-case token :ident)) (if tyspec-seenp (b* ((parstate (unread-token parstate))) (retok (list specqual) first-span parstate)) (b* ((parstate (unread-token parstate)) ((erp specquals last-span parstate) (parse-specifier-qualifier-list tyspec-seenp parstate))) (retok (cons specqual specquals) (span-join first-span last-span) parstate)))) ((token-specifier/qualifier-start-p token) (b* ((parstate (unread-token parstate)) ((erp specquals last-span parstate) (parse-specifier-qualifier-list tyspec-seenp parstate))) (retok (cons specqual specquals) (span-join first-span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list specqual) first-span parstate)))))))
Function:
(defun parse-declaration-specifier (tyspec-seenp parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (booleanp tyspec-seenp) (parstatep parstate)))) (let ((__function__ 'parse-declaration-specifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-declspec) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-storage-class-specifier-p token) (retok (declspec-stocla (token-to-storage-class-specifier token)) span parstate)) ((token-type-specifier-keyword-p token) (retok (declspec-tyspec (token-to-type-specifier-keyword token)) span parstate)) ((token-keywordp token "_Atomic") (b* (((erp token2 & parstate) (read-token parstate))) (cond ((token-punctuatorp token2 "(") (if tyspec-seenp (b* ((parstate (unread-token parstate))) (retok (declspec-tyqual (type-qual-atomic)) span parstate)) (b* (((erp tyname & parstate) (parse-type-name parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (declspec-tyspec (type-spec-atomic tyname)) (span-join span last-span) parstate)))) (t (b* ((parstate (if token2 (unread-token parstate) parstate))) (retok (declspec-tyqual (type-qual-atomic)) span parstate)))))) ((token-keywordp token "struct") (b* (((erp strunispec last-span parstate) (parse-struct-or-union-specifier parstate))) (retok (declspec-tyspec (type-spec-struct strunispec)) (span-join span last-span) parstate))) ((token-keywordp token "union") (b* (((erp strunispec last-span parstate) (parse-struct-or-union-specifier parstate))) (retok (declspec-tyspec (type-spec-union strunispec)) (span-join span last-span) parstate))) ((token-keywordp token "enum") (b* (((erp enumspec last-span parstate) (parse-enum-specifier span parstate))) (retok (declspec-tyspec (type-spec-enum enumspec)) (span-join span last-span) parstate))) ((and token (token-case token :ident)) (retok (declspec-tyspec (type-spec-typedef (token-ident->unwrap token))) span parstate)) ((or (token-keywordp token "typeof") (token-keywordp token "__typeof") (token-keywordp token "__typeof__")) (b* ((uscores (cond ((token-keywordp token "typeof") (keyword-uscores-none)) ((token-keywordp token "__typeof") (keyword-uscores-start)) ((token-keywordp token "__typeof__") (keyword-uscores-both)))) ((erp & parstate) (read-punctuator "(" parstate)) ((erp expr/tyname & parstate) (parse-expression-or-type-name parstate)) ((erp last-span parstate) (read-punctuator ")" parstate)) (tyspec (amb?-expr/tyname-case expr/tyname :expr (make-type-spec-typeof-expr :expr expr/tyname.unwrap :uscores uscores) :tyname (make-type-spec-typeof-type :type expr/tyname.unwrap :uscores uscores) :ambig (make-type-spec-typeof-ambig :expr/type expr/tyname.unwrap :uscores uscores)))) (retok (declspec-tyspec tyspec) (span-join span last-span) parstate))) ((token-type-qualifier-p token) (retok (declspec-tyqual (token-to-type-qualifier token)) span parstate)) ((token-function-specifier-p token) (retok (declspec-funspec (token-to-function-specifier token)) span parstate)) ((token-keywordp token "_Alignas") (b* (((erp alignspec last-span parstate) (parse-alignment-specifier span parstate))) (retok (declspec-align alignspec) (span-join span last-span) parstate))) ((or (token-keywordp token "__attribute") (token-keywordp token "__attribute__")) (b* ((uscores (token-keywordp token "__attribute__")) ((erp attrspec last-span parstate) (parse-attribute-specifier uscores span parstate))) (retok (declspec-attrib attrspec) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an identifier ~ or a keyword in {~ _Alignas, ~ _Atomic, ~ _Bool, ~ _Complex, ~ _Noreturn, ~ _Thread_local, ~ auto, ~ char, ~ const, ~ double, ~ enum, ~ extern, ~ float, ~ inline, ~ int, ~ long, ~ register, ~ restrict, ~ short, ~ signed, ~ static, ~ struct, ~ typedef, ~ union, ~ unsigned, ~ void, ~ volatile~ }" :found (token-to-msg token)))))))
Function:
(defun parse-declaration-specifiers (tyspec-seenp parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (booleanp tyspec-seenp) (parstatep parstate)))) (let ((__function__ 'parse-declaration-specifiers)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) (psize (parsize parstate)) ((erp declspec first-span parstate) (parse-declaration-specifier tyspec-seenp parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) (tyspec-seenp (or tyspec-seenp (declspec-case declspec :tyspec))) ((erp token & parstate) (read-token parstate))) (cond ((and token (token-case token :ident)) (if tyspec-seenp (b* ((parstate (unread-token parstate))) (retok (list declspec) first-span parstate)) (b* ((parstate (unread-token parstate)) ((erp declspecs last-span parstate) (parse-declaration-specifiers tyspec-seenp parstate))) (retok (cons declspec declspecs) (span-join first-span last-span) parstate)))) ((token-declaration-specifier-start-p token) (b* ((parstate (unread-token parstate)) ((erp declspecs last-span parstate) (parse-declaration-specifiers tyspec-seenp parstate))) (retok (cons declspec declspecs) (span-join first-span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list declspec) first-span parstate)))))))
Function:
(defun parse-type-qualifier-or-attribute-specifier (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-type-qualifier-or-attribute-specifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-typequal/attribspec) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-type-qualifier-p token) (retok (typequal/attribspec-tyqual (token-to-type-qualifier token)) span parstate)) ((or (token-keywordp token "__attribute") (token-keywordp token "__attribute__")) (b* ((uscores (token-keywordp token "__attribute__")) ((erp attrspec last-span parstate) (parse-attribute-specifier uscores span parstate))) (retok (typequal/attribspec-attrib attrspec) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "a keyword in {~ _Atomic, ~ const, ~ restrict, ~ volatile~ }" :found (token-to-msg token)))))))
Function:
(defun parse-type-qualifier-and-attribute-specifier-list (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-type-qualifier-and-attribute-specifier-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) (psize (parsize parstate)) ((erp tyqualattrib span parstate) (parse-type-qualifier-or-attribute-specifier parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate))) (cond ((token-type-qualifier-or-attribute-specifier-start-p token) (b* ((parstate (unread-token parstate)) ((erp tyqualattribs last-span parstate) (parse-type-qualifier-and-attribute-specifier-list parstate))) (retok (cons tyqualattrib tyqualattribs) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list tyqualattrib) span parstate)))))))
Function:
(defun parse-pointer (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-pointer)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp span parstate) (read-punctuator "*" parstate)) ((erp token & parstate) (read-token parstate))) (cond ((token-type-qualifier-or-attribute-specifier-start-p token) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp tyqualattribs span2 parstate) (parse-type-qualifier-and-attribute-specifier-list parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token "*") (b* ((parstate (unread-token parstate)) ((erp tyqualattribss last-span parstate) (parse-pointer parstate))) (retok (cons tyqualattribs tyqualattribss) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list tyqualattribs) (span-join span span2) parstate)))))) ((token-punctuatorp token "*") (b* ((parstate (unread-token parstate)) ((erp tyqualattribss last-span parstate) (parse-pointer parstate))) (retok (cons nil tyqualattribss) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list nil) span parstate)))))))
Function:
(defun parse-struct-or-union-specifier (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-struct-or-union-specifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-strunispec) (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 structdecls & parstate) (parse-struct-declaration-list parstate)) ((erp last-span parstate) (read-punctuator "}" parstate))) (retok (make-strunispec :name ident :members structdecls) (span-join span last-span) parstate))) (t (b* ((parstate (if token2 (unread-token parstate) parstate))) (retok (make-strunispec :name ident :members nil) span parstate)))))) ((token-punctuatorp token "{") (b* (((erp structdecls & parstate) (parse-struct-declaration-list parstate)) ((erp last-span parstate) (read-punctuator "}" parstate))) (retok (make-strunispec :name nil :members structdecls) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an identifier ~ or an open curly brace" :found (token-to-msg token)))))))
Function:
(defun parse-enum-specifier (first-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (spanp first-span) (parstatep parstate)))) (let ((__function__ 'parse-enum-specifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-enumspec) (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 enumers final-comma & parstate) (parse-enumerator-list parstate)) ((erp last-span parstate) (read-punctuator "}" parstate))) (retok (make-enumspec :name ident :list enumers :final-comma final-comma) (span-join first-span last-span) parstate))) (t (b* ((parstate (if token2 (unread-token parstate) parstate))) (retok (make-enumspec :name ident :list nil :final-comma nil) (span-join first-span span) parstate)))))) ((token-punctuatorp token "{") (b* (((erp enumers final-comma & parstate) (parse-enumerator-list parstate)) ((erp last-span parstate) (read-punctuator "}" parstate))) (retok (make-enumspec :name nil :list enumers :final-comma final-comma) (span-join first-span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an identifier ~ or a closed curly brace" :found (token-to-msg token)))))))
Function:
(defun parse-alignment-specifier (first-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (spanp first-span) (parstatep parstate)))) (let ((__function__ 'parse-alignment-specifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-align-spec) (irr-span) parstate) ((erp & parstate) (read-punctuator "(" parstate)) ((erp expr/tyname & parstate) (parse-expression-or-type-name parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (amb?-expr/tyname-case expr/tyname :expr (retok (align-spec-alignas-expr (const-expr expr/tyname.unwrap)) (span-join first-span last-span) parstate) :tyname (retok (align-spec-alignas-type expr/tyname.unwrap) (span-join first-span last-span) parstate) :ambig (retok (align-spec-alignas-ambig expr/tyname.unwrap) (span-join first-span last-span) parstate)))))
Function:
(defun parse-array/function-abstract-declarator (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-array/function-abstract-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-dirabsdeclor) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-punctuatorp token "[") (b* (((erp token2 span2 parstate) (read-token parstate))) (cond ((token-punctuatorp token2 "]") (retok (make-dirabsdeclor-array :decl? nil :tyquals nil :expr? nil) (span-join span span2) parstate)) ((token-punctuatorp token2 "*") (b* (((erp token3 span3 parstate) (read-token parstate))) (cond ((token-punctuatorp token3 "]") (retok (make-dirabsdeclor-array-star :decl? nil) (span-join span span3) parstate)) (t (b* ((parstate (if token3 (unread-token parstate) parstate)) (parstate (unread-token parstate)) ((erp expr & parstate) (parse-assignment-expression parstate)) ((erp last-span parstate) (read-punctuator "]" parstate))) (retok (make-dirabsdeclor-array :decl? nil :tyquals nil :expr? expr) (span-join span last-span) parstate)))))) ((token-keywordp token2 "static") (b* (((erp token3 & parstate) (read-token parstate))) (cond ((token-type-qualifier-p token3) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp tyquals & parstate) (parse-type-qualifier-and-attribute-specifier-list parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp expr & parstate) (parse-assignment-expression parstate)) ((erp last-span parstate) (read-punctuator "]" parstate))) (retok (make-dirabsdeclor-array-static1 :decl? nil :tyquals tyquals :expr expr) (span-join span last-span) parstate))) (t (b* ((parstate (if token3 (unread-token parstate) parstate)) ((erp expr & parstate) (parse-assignment-expression parstate)) ((erp last-span parstate) (read-punctuator "]" parstate))) (retok (make-dirabsdeclor-array-static1 :decl? nil :tyquals nil :expr expr) (span-join span last-span) parstate)))))) ((token-type-qualifier-p token2) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp tyquals & parstate) (parse-type-qualifier-and-attribute-specifier-list parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token3 span3 parstate) (read-token parstate))) (cond ((token-keywordp token3 "static") (b* (((erp expr & parstate) (parse-assignment-expression parstate)) ((erp last-span parstate) (read-punctuator "]" parstate))) (retok (make-dirabsdeclor-array-static2 :decl? nil :tyquals tyquals :expr expr) (span-join span last-span) parstate))) ((token-punctuatorp token3 "]") (retok (make-dirabsdeclor-array :decl? nil :tyquals tyquals :expr? nil) (span-join span span3) parstate)) (t (b* ((parstate (if token3 (unread-token parstate) parstate)) ((erp expr & parstate) (parse-assignment-expression parstate)) ((erp last-span parstate) (read-punctuator "]" parstate))) (retok (make-dirabsdeclor-array :decl? nil :tyquals tyquals :expr? expr) (span-join span last-span) parstate)))))) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) ((erp expr & parstate) (parse-assignment-expression parstate)) ((erp last-span parstate) (read-punctuator "]" parstate))) (retok (make-dirabsdeclor-array :decl? nil :tyquals nil :expr? expr) (span-join span last-span) parstate)))))) ((token-punctuatorp token "(") (b* (((erp token2 span2 parstate) (read-token parstate))) (cond ((token-punctuatorp token2 ")") (retok (make-dirabsdeclor-function :decl? nil :params nil :ellipsis nil) (span-join span span2) parstate)) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) ((erp paramdecls ellipsis & parstate) (parse-parameter-declaration-list parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (make-dirabsdeclor-function :decl? nil :params paramdecls :ellipsis ellipsis) (span-join span last-span) parstate)))))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an open parenthesis ~ or an open square bracket" :found (token-to-msg token)))))))
Function:
(defun parse-direct-abstract-declarator (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-direct-abstract-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-dirabsdeclor) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-punctuatorp token "(") (b* (((erp token2 & parstate) (read-token parstate))) (cond ((token-abstract-declarator-start-p token2) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp absdeclor & parstate) (parse-abstract-declarator parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp last-span parstate) (read-punctuator ")" parstate))) (parse-direct-abstract-declarator-rest (dirabsdeclor-paren absdeclor) (span-join span last-span) parstate))) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) (parstate (unread-token parstate)) (psize (parsize parstate)) ((erp dirabsdeclor span parstate) (parse-array/function-abstract-declarator parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-direct-abstract-declarator-rest dirabsdeclor span parstate)))))) ((token-punctuatorp token "[") (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp dirabsdeclor span parstate) (parse-array/function-abstract-declarator parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-direct-abstract-declarator-rest dirabsdeclor span parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an open parenthesis ~ or an open square bracket" :found (token-to-msg token)))))))
Function:
(defun parse-direct-abstract-declarator-rest (prev-dirabsdeclor prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (dirabsdeclorp prev-dirabsdeclor) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-direct-abstract-declarator-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-dirabsdeclor) (irr-span) parstate) ((erp token & parstate) (read-token parstate))) (cond ((or (token-punctuatorp token "(") (token-punctuatorp token "[")) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp next-dirabsdeclor next-span parstate) (parse-array/function-abstract-declarator parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((unless (mbt (dirabsdeclor-decl?-nil-p next-dirabsdeclor))) (reterr :impossible)) (curr-dirabsdeclor (combine-dirabsdeclor-into-dirabsdeclor prev-dirabsdeclor next-dirabsdeclor)) (curr-span (span-join prev-span next-span))) (parse-direct-abstract-declarator-rest curr-dirabsdeclor curr-span parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (dirabsdeclor-fix prev-dirabsdeclor) (span-fix prev-span) parstate)))))))
Function:
(defun parse-abstract-declarator (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-abstract-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-absdeclor) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-punctuatorp token "*") (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp tyqualss tyqualss-span parstate) (parse-pointer parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token2 & parstate) (read-token parstate))) (cond ((token-direct-abstract-declarator-start-p token2) (b* ((parstate (unread-token parstate)) ((erp dirabsdeclor dirabsdeclor-span parstate) (parse-direct-abstract-declarator parstate))) (retok (make-absdeclor :pointers tyqualss :decl? dirabsdeclor) (span-join tyqualss-span dirabsdeclor-span) parstate))) (t (b* ((parstate (if token2 (unread-token parstate) parstate))) (retok (make-absdeclor :pointers tyqualss :decl? nil) tyqualss-span parstate)))))) ((token-direct-abstract-declarator-start-p token) (b* ((parstate (unread-token parstate)) ((erp dirabsdeclor span parstate) (parse-direct-abstract-declarator parstate))) (retok (make-absdeclor :pointers nil :decl? dirabsdeclor) span parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "a star ~ or an open parenthesis ~ or an open square bracket" :found (token-to-msg token)))))))
Function:
(defun parse-array/function-declarator (prev-dirdeclor prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (dirdeclorp prev-dirdeclor) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-array/function-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-dirdeclor) (irr-span) parstate) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token "[") (b* (((erp token2 span2 parstate) (read-token parstate))) (cond ((token-type-qualifier-p token2) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp tyquals & parstate) (parse-type-qualifier-and-attribute-specifier-list parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token3 span3 parstate) (read-token parstate))) (cond ((token-punctuatorp token3 "*") (b* (((erp token4 span4 parstate) (read-token parstate))) (cond ((token-punctuatorp token4 "]") (retok (make-dirdeclor-array-star :decl prev-dirdeclor :tyquals tyquals) (span-join prev-span span4) parstate)) (t (b* ((parstate (if token4 (unread-token parstate) parstate)) (parstate (unread-token parstate)) ((erp expr & parstate) (parse-assignment-expression parstate)) ((erp last-span parstate) (read-punctuator "]" parstate))) (retok (make-dirdeclor-array :decl prev-dirdeclor :tyquals tyquals :expr? expr) (span-join prev-span last-span) parstate)))))) ((token-expression-start-p token3) (b* ((parstate (unread-token parstate)) ((erp expr & parstate) (parse-assignment-expression parstate)) ((erp last-span parstate) (read-punctuator "]" parstate))) (retok (make-dirdeclor-array :decl prev-dirdeclor :tyquals tyquals :expr? expr) (span-join prev-span last-span) parstate))) ((token-punctuatorp token3 "]") (retok (make-dirdeclor-array :decl prev-dirdeclor :tyquals tyquals :expr? nil) (span-join prev-span span3) parstate)) ((token-keywordp token3 "static") (b* (((erp expr & parstate) (parse-assignment-expression parstate)) ((erp last-span parstate) (read-punctuator "]" parstate))) (retok (make-dirdeclor-array-static2 :decl prev-dirdeclor :tyquals tyquals :expr expr) (span-join prev-span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span3)) :expected "an expression ~ or the 'static' keyword ~ or a closed square bracket" :found (token-to-msg token3)))))) ((token-punctuatorp token2 "*") (b* (((erp token3 span3 parstate) (read-token parstate))) (cond ((token-punctuatorp token3 "]") (retok (make-dirdeclor-array-star :decl prev-dirdeclor :tyquals nil) (span-join prev-span span3) parstate)) (t (b* ((parstate (if token3 (unread-token parstate) parstate)) (parstate (unread-token parstate)) ((erp expr & parstate) (parse-assignment-expression parstate)) ((erp last-span parstate) (read-punctuator "]" parstate))) (retok (make-dirdeclor-array :decl prev-dirdeclor :tyquals nil :expr? expr) (span-join prev-span last-span) parstate)))))) ((token-expression-start-p token2) (b* ((parstate (unread-token parstate)) ((erp expr & parstate) (parse-assignment-expression parstate)) ((erp last-span parstate) (read-punctuator "]" parstate))) (retok (make-dirdeclor-array :decl prev-dirdeclor :tyquals nil :expr? expr) (span-join prev-span last-span) parstate))) ((token-keywordp token2 "static") (b* (((erp token3 & parstate) (read-token parstate))) (cond ((token-type-qualifier-p token3) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp tyquals & parstate) (parse-type-qualifier-and-attribute-specifier-list parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp expr & parstate) (parse-assignment-expression parstate)) ((erp last-span parstate) (read-punctuator "]" parstate))) (retok (make-dirdeclor-array-static1 :decl prev-dirdeclor :tyquals tyquals :expr expr) (span-join prev-span last-span) parstate))) (t (b* ((parstate (unread-token parstate)) ((erp expr & parstate) (parse-assignment-expression parstate)) ((erp last-span parstate) (read-punctuator "]" parstate))) (retok (make-dirdeclor-array-static1 :decl prev-dirdeclor :tyquals nil :expr expr) (span-join prev-span last-span) parstate)))))) ((token-punctuatorp token2 "]") (retok (make-dirdeclor-array :decl prev-dirdeclor :tyquals nil :expr? nil) (span-join prev-span span2) parstate)) (t (reterr-msg :where (position-to-msg (span->start span2)) :expected "a type qualifier ~ or an expression ~ or the 'static' keyword ~ or a closed square bracket" :found (token-to-msg token2)))))) ((token-punctuatorp token "(") (b* (((erp token2 span2 parstate) (read-token parstate))) (cond ((token-punctuatorp token2 ")") (retok (make-dirdeclor-function-params :decl prev-dirdeclor :params nil :ellipsis nil) (span-join prev-span span2) parstate)) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) ((erp paramdecls ellipsis & parstate) (parse-parameter-declaration-list parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (make-dirdeclor-function-params :decl prev-dirdeclor :params paramdecls :ellipsis ellipsis) (span-join prev-span last-span) parstate)))))) (t (prog2$ (raise "Internal error: unexpected token ~x0." token) (reterr t)))))))
Function:
(defun parse-direct-declarator (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-direct-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-dirdeclor) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((and token (token-case token :ident)) (parse-direct-declarator-rest (dirdeclor-ident (token-ident->unwrap token)) span parstate)) ((token-punctuatorp token "(") (b* ((psize (parsize parstate)) ((erp declor & parstate) (parse-declarator parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp last-span parstate) (read-punctuator ")" parstate))) (parse-direct-declarator-rest (dirdeclor-paren declor) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "an identifier ~ or an open parenthesis" :found (token-to-msg token)))))))
Function:
(defun parse-direct-declarator-rest (prev-dirdeclor prev-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (dirdeclorp prev-dirdeclor) (spanp prev-span) (parstatep parstate)))) (let ((__function__ 'parse-direct-declarator-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-dirdeclor) (irr-span) parstate) ((erp token & parstate) (read-token parstate))) (cond ((or (token-punctuatorp token "(") (token-punctuatorp token "[")) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp curr-dirdeclor curr-span parstate) (parse-array/function-declarator prev-dirdeclor prev-span parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (parse-direct-declarator-rest curr-dirdeclor curr-span parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (dirdeclor-fix prev-dirdeclor) (span-fix prev-span) parstate)))))))
Function:
(defun parse-declarator (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-declor) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-punctuatorp token "*") (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp tyqualss & parstate) (parse-pointer parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp dirdeclor last-span parstate) (parse-direct-declarator parstate))) (retok (make-declor :pointers tyqualss :decl dirdeclor) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate)) ((erp dirdeclor span parstate) (parse-direct-declarator parstate))) (retok (make-declor :pointers nil :decl dirdeclor) span parstate)))))))
Function:
(defun parse-struct-declarator (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-struct-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-structdeclor) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-declarator-start-p token) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp declor span parstate) (parse-declarator parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token2 & parstate) (read-token parstate))) (cond ((token-punctuatorp token2 ":") (b* (((erp cexpr last-span parstate) (parse-constant-expression parstate))) (retok (make-structdeclor :declor? declor :expr? cexpr) (span-join span last-span) parstate))) (t (b* ((parstate (if token2 (unread-token parstate) parstate))) (retok (make-structdeclor :declor? declor :expr? nil) span parstate)))))) ((token-punctuatorp token ":") (b* (((erp cexpr last-span parstate) (parse-constant-expression parstate))) (retok (make-structdeclor :declor? nil :expr? cexpr) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "a declarator or a colon" :found (token-to-msg token)))))))
Function:
(defun parse-struct-declarator-list (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-struct-declarator-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) (psize (parsize parstate)) ((erp structdeclor span parstate) (parse-struct-declarator parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token ",") (b* (((erp structdeclors last-span parstate) (parse-struct-declarator-list parstate))) (retok (cons structdeclor structdeclors) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list structdeclor) span parstate)))))))
Function:
(defun parse-struct-declaration (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-struct-declaration)) (declare (ignorable __function__)) (b* (((reterr) (irr-structdecl) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-keywordp token "_Static_assert") (b* (((erp statassert span parstate) (parse-static-assert-declaration span parstate))) (retok (structdecl-statassert statassert) span parstate))) (t (b* (((mv extension parstate) (if (and (token-keywordp token "__extension__") (parstate->gcc parstate)) (mv t parstate) (b* ((parstate (if token (unread-token parstate) parstate))) (mv nil parstate)))) (psize (parsize parstate)) ((erp specquals span parstate) (parse-specifier-qualifier-list nil parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token2 span2 parstate) (read-token parstate))) (cond ((token-struct-declarator-start-p token2) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp structdeclors & parstate) (parse-struct-declarator-list parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp attrspecs & parstate) (parse-*-attribute-specifier parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (make-structdecl-member :extension extension :specqual specquals :declor structdeclors :attrib attrspecs) (span-join span last-span) parstate))) ((token-keywordp token2 "__attribute__") (b* ((parstate (unread-token parstate)) ((erp attrspecs & parstate) (parse-*-attribute-specifier parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (make-structdecl-member :extension extension :specqual specquals :declor nil :attrib attrspecs) (span-join span last-span) parstate))) ((token-punctuatorp token2 ";") (retok (make-structdecl-member :extension extension :specqual specquals :declor nil :attrib nil) (span-join span span2) parstate)) (t (reterr-msg :where (position-to-msg (span->start span2)) :expected "a structure declarator or a semicolon" :found (token-to-msg token2))))))))))
Function:
(defun parse-struct-declaration-list (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-struct-declaration-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) (psize (parsize parstate)) ((erp structdecl span parstate) (parse-struct-declaration parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate))) (cond ((token-struct-declaration-start-p token) (b* ((parstate (unread-token parstate)) ((erp structdecls last-span parstate) (parse-struct-declaration-list parstate))) (retok (cons structdecl structdecls) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list structdecl) span parstate)))))))
Function:
(defun parse-parameter-declaration (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-parameter-declaration)) (declare (ignorable __function__)) (b* (((reterr) (irr-paramdecl) (irr-span) parstate) (psize (parsize parstate)) ((erp declspecs span parstate) (parse-declaration-specifiers nil parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate))) (cond ((or (token-punctuatorp token ")") (token-punctuatorp token ",")) (b* ((parstate (unread-token parstate))) (retok (make-paramdecl :spec declspecs :decl (paramdeclor-none)) span parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate)) ((erp declor/absdeclor last-span parstate) (parse-declarator-or-abstract-declarator parstate))) (amb?-declor/absdeclor-case declor/absdeclor :declor (retok (make-paramdecl :spec declspecs :decl (paramdeclor-declor declor/absdeclor.unwrap)) (span-join span last-span) parstate) :absdeclor (retok (make-paramdecl :spec declspecs :decl (paramdeclor-absdeclor declor/absdeclor.unwrap)) (span-join span last-span) parstate) :ambig (retok (make-paramdecl :spec declspecs :decl (paramdeclor-ambig declor/absdeclor.unwrap)) (span-join span last-span) parstate))))))))
Function:
(defun parse-parameter-declaration-list (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-parameter-declaration-list)) (declare (ignorable __function__)) (b* (((reterr) nil nil (irr-span) parstate) (psize (parsize parstate)) ((erp paramdecl span parstate) (parse-parameter-declaration parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token ",") (b* (((erp token2 span2 parstate) (read-token parstate))) (cond ((token-punctuatorp token2 "...") (retok (list paramdecl) t (span-join span span2) parstate)) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) ((erp paramdecls ellipsis last-span parstate) (parse-parameter-declaration-list parstate))) (retok (cons paramdecl paramdecls) ellipsis (span-join span last-span) parstate)))))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list paramdecl) nil span parstate)))))))
Function:
(defun parse-type-name (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-type-name)) (declare (ignorable __function__)) (b* (((reterr) (irr-tyname) (irr-span) parstate) (psize (parsize parstate)) ((erp specquals span parstate) (parse-specifier-qualifier-list nil parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate))) (cond ((token-abstract-declarator-start-p token) (b* ((parstate (unread-token parstate)) ((erp absdeclor last-span parstate) (parse-abstract-declarator parstate))) (retok (make-tyname :specqual specquals :decl? absdeclor) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (make-tyname :specqual specquals :decl? nil) span parstate)))))))
Function:
(defun parse-expression-or-type-name (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-expression-or-type-name)) (declare (ignorable __function__)) (b* (((reterr) (irr-amb?-expr/tyname) (irr-span) parstate) (checkpoint (parstate->tokens-read parstate)) (psize (parsize parstate)) ((mv erp-expr expr span-expr parstate) (parse-expression parstate))) (if erp-expr (b* ((parstate (unread-to-token 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 tyname span parstate) (parse-type-name parstate)) ((erp & parstate) (read-punctuator ")" parstate)) (parstate (unread-token parstate))) (retok (amb?-expr/tyname-tyname tyname) span parstate)) (b* (((erp token & parstate) (read-token parstate))) (if (token-punctuatorp token ")") (b* ((checkpoint-after-expr (parstate->tokens-read parstate)) (parstate (unread-to-token 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 tyname span-tyname parstate) (parse-type-name parstate))) (if erp (b* ((parstate (unread-to-token checkpoint parstate)) (parstate (reread-to-token checkpoint-after-expr parstate)) ((unless (<= (parsize parstate) (- psize 2))) (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 (unread-token parstate))) (retok (amb?-expr/tyname-expr expr) span-expr parstate)) (b* (((erp token & parstate) (read-token parstate))) (if (token-punctuatorp token ")") (b* (((unless (equal span-expr span-tyname)) (raise "Internal error: span ~x0 of expression ~x1 differs from ~ span ~x2 of type name ~x3." span-expr expr span-tyname tyname) (reterr t)) (parstate (unread-token parstate))) (retok (amb?-expr/tyname-ambig (make-amb-expr/tyname :expr expr :tyname tyname)) span-expr parstate)) (b* ((parstate (unread-to-token checkpoint parstate)) (parstate (reread-to-token checkpoint-after-expr parstate)) ((unless (<= (parsize parstate) (- psize 2))) (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 (unread-token parstate))) (retok (amb?-expr/tyname-expr expr) span-expr parstate)))))) (b* ((parstate (unread-to-token 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 tyname span parstate) (parse-type-name parstate)) ((erp & parstate) (read-punctuator ")" parstate)) (parstate (unread-token parstate))) (retok (amb?-expr/tyname-tyname tyname) span parstate))))))))
Function:
(defun parse-declarator-or-abstract-declarator (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-declarator-or-abstract-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-amb?-declor/absdeclor) (irr-span) parstate) (checkpoint (parstate->tokens-read parstate)) (psize (parsize parstate)) ((mv erp-declor declor span-declor parstate) (parse-declarator parstate))) (if erp-declor (b* ((parstate (unread-to-token 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 absdeclor span parstate) (parse-abstract-declarator parstate))) (retok (amb?-declor/absdeclor-absdeclor absdeclor) span parstate)) (b* ((checkpoint-after-declor (parstate->tokens-read parstate)) (parstate (unread-to-token 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 absdeclor span-absdeclor parstate) (parse-abstract-declarator parstate))) (if erp (b* ((parstate (unread-to-token checkpoint parstate)) (parstate (reread-to-token checkpoint-after-declor parstate)) ((unless (<= (parsize parstate) (1- 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)))) (retok (amb?-declor/absdeclor-declor declor) span-declor parstate)) (b* (((erp token & parstate) (read-token parstate))) (if (or (token-punctuatorp token ",") (token-punctuatorp token ")")) (b* (((unless (equal span-absdeclor span-declor)) (raise "Internal error: ~ span ~x0 of declarator ~x1 differs from ~ span ~x2 of abstract declarator ~x3." span-declor declor span-absdeclor absdeclor) (reterr t)) (parstate (unread-token parstate))) (retok (amb?-declor/absdeclor-ambig (make-amb-declor/absdeclor :declor declor :absdeclor absdeclor)) span-declor parstate)) (b* ((parstate (unread-to-token checkpoint parstate)) (parstate (reread-to-token checkpoint-after-declor parstate)) ((unless (<= (parsize parstate) (1- 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)))) (retok (amb?-declor/absdeclor-declor declor) span-declor parstate))))))))))
Function:
(defun parse-attribute-parameters (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-attribute-parameters)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp open-span parstate) (read-punctuator "(" parstate)) ((erp exprs & parstate) (parse-argument-expressions parstate)) ((erp close-span parstate) (read-punctuator ")" parstate))) (retok exprs (span-join open-span close-span) parstate))))
Function:
(defun parse-attribute (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-attribute)) (declare (ignorable __function__)) (b* (((reterr) (irr-attrib) (irr-span) parstate) ((erp name name-span parstate) (parse-attribute-name parstate)) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token "(") (b* ((parstate (unread-token parstate)) ((erp exprs span parstate) (parse-attribute-parameters parstate))) (retok (make-attrib-name-param :name name :param exprs) (span-join name-span span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (attrib-name name) name-span parstate)))))))
Function:
(defun parse-attribute-list (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-attribute-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) (psize (parsize parstate)) ((erp attr span parstate) (parse-attribute parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token ",") (b* (((erp attrs last-span parstate) (parse-attribute-list parstate))) (retok (cons attr attrs) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list attr) span parstate)))))))
Function:
(defun parse-attribute-specifier (uscores first-span parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (and (booleanp uscores) (spanp first-span) (parstatep parstate)))) (let ((__function__ 'parse-attribute-specifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-attrib-spec) (irr-span) parstate) ((erp & parstate) (read-punctuator "(" parstate)) ((erp & parstate) (read-punctuator "(" parstate)) ((erp attrs & parstate) (parse-attribute-list parstate)) ((erp & parstate) (read-punctuator ")" parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (make-attrib-spec :uscores uscores :attribs attrs) (span-join first-span last-span) parstate))))
Function:
(defun parse-*-attribute-specifier (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-*-attribute-specifier)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp token first-span parstate) (read-token parstate)) ((unless (or (token-keywordp token "__attribute") (token-keywordp token "__attribute__"))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok nil (irr-span) parstate))) (uscores (token-keywordp token "__attribute__")) (psize (parsize parstate)) ((erp attrspec span parstate) (parse-attribute-specifier uscores first-span parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp attrspecs last-span parstate) (parse-*-attribute-specifier parstate))) (retok (cons attrspec attrspecs) (if attrspecs (span-join span last-span) span) parstate))))
Function:
(defun parse-init-declarator (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-init-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-initdeclor) (irr-span) parstate) (psize (parsize parstate)) ((erp declor span parstate) (parse-declarator parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp asmspec? asmspec?-span parstate) (parse-?-asm-name-specifier parstate)) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token "=") (b* (((erp initer last-span parstate) (parse-initializer parstate))) (retok (make-initdeclor :declor declor :asm? asmspec? :init? initer) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (make-initdeclor :declor declor :asm? asmspec? :init? nil) (if asmspec? (span-join span asmspec?-span) span) parstate)))))))
Function:
(defun parse-init-declarator-list (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-init-declarator-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) (psize (parsize parstate)) ((erp initdeclor span parstate) (parse-init-declarator parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token ",") (b* (((erp initdeclors last-span parstate) (parse-init-declarator-list parstate))) (retok (cons initdeclor initdeclors) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list initdeclor) span parstate)))))))
Function:
(defun parse-declaration (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-declaration)) (declare (ignorable __function__)) (b* (((reterr) (irr-decl) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((or (token-declaration-specifier-start-p token) (and (token-keywordp token "__extension__") (parstate->gcc parstate))) (b* (((mv extension parstate) (if (and (token-keywordp token "__extension__") (parstate->gcc parstate)) (mv t parstate) (b* ((parstate (unread-token parstate))) (mv nil parstate)))) (psize (parsize parstate)) ((erp declspecs span parstate) (parse-declaration-specifiers nil parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token2 span2 parstate) (read-token parstate))) (cond ((and (token-keywordp token2 "__attribute__") (parstate->gcc parstate)) (b* ((parstate (unread-token parstate)) ((erp attrspecs & parstate) (parse-*-attribute-specifier parstate)) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (make-decl-decl :extension extension :specs declspecs :init nil :attrib attrspecs) (span-join span last-span) parstate))) ((token-declarator-start-p token2) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp initdeclors & parstate) (parse-init-declarator-list parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp attrspecs & parstate) (if (parstate->gcc parstate) (parse-*-attribute-specifier parstate) (retok nil (irr-span) parstate))) ((erp last-span parstate) (read-punctuator ";" parstate))) (retok (make-decl-decl :extension extension :specs declspecs :init initdeclors :attrib attrspecs) (span-join span last-span) parstate))) ((token-punctuatorp token2 ";") (retok (make-decl-decl :extension extension :specs declspecs :init nil :attrib nil) (span-join span span2) parstate)) (t (reterr-msg :where (position-to-msg (span->start span2)) :expected "a declarator or a semicolon" :found (token-to-msg token2)))))) ((token-keywordp token "_Static_assert") (b* (((erp statassert last-span parstate) (parse-static-assert-declaration span parstate))) (retok (decl-statassert statassert) (span-join span last-span) parstate))) (t (reterr-msg :where (position-to-msg (span->start span)) :expected "a declaration specifier ~ or the _Static_assert keyword" :found (token-to-msg token)))))))
Function:
(defun parse-declaration-list (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-declaration-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) (psize (parsize parstate)) ((erp decl span parstate) (parse-declaration parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate))) (cond ((token-punctuatorp token "{") (retok (list decl) span parstate)) (t (b* ((parstate (if token (unread-token parstate) parstate)) ((erp decls last-span parstate) (parse-declaration-list parstate))) (retok (cons decl decls) (span-join span last-span) parstate)))))))
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) (checkpoint (parstate->tokens-read parstate)) (psize (parsize parstate)) ((mv erp expr span-expr parstate) (parse-expression parstate))) (if erp (b* ((parstate (unread-to-token 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* ((checkpoint-after-expr (parstate->tokens-read parstate)) (parstate (unread-to-token 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 decl span-decl parstate) (parse-declaration parstate))) (if erp (b* ((parstate (unread-to-token checkpoint parstate)) (parstate (reread-to-token checkpoint-after-expr parstate)) ((unless (<= (parsize parstate) (- psize 2))) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize parstate) psize) (b* ((parstate (init-parstate nil nil parstate))) (reterr t)))) (retok (amb?-decl/stmt-stmt expr) (span-join span-expr span-semicolon) parstate)) (b* (((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 (unread-to-token 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))))))))
Function:
(defun parse-asm-output-operand (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-asm-output-operand)) (declare (ignorable __function__)) (b* (((reterr) (irr-asm-output) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-punctuatorp token "[") (b* (((erp name & parstate) (read-identifier parstate)) ((erp & parstate) (read-punctuator "]" parstate)) ((erp token2 span2 parstate) (read-token parstate)) ((unless (and token2 (token-case token2 :string))) (reterr-msg :where (position-to-msg (span->start span2)) :expected "a string literal" :found (token-to-msg token2))) (string (token-string->unwrap token2)) ((erp strings & parstate) (parse-*-stringlit parstate)) (constraint (cons string strings)) ((erp & parstate) (read-punctuator "(" parstate)) ((erp lvalue & parstate) (parse-expression parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (make-asm-output :name name :constraint constraint :lvalue lvalue) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate)) ((erp token2 span2 parstate) (read-token parstate)) ((unless (and token2 (token-case token2 :string))) (reterr-msg :where (position-to-msg (span->start span2)) :expected "a string literal" :found (token-to-msg token2))) (string (token-string->unwrap token2)) ((erp strings & parstate) (parse-*-stringlit parstate)) (constraint (cons string strings)) ((erp & parstate) (read-punctuator "(" parstate)) ((erp lvalue & parstate) (parse-expression parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (make-asm-output :name nil :constraint constraint :lvalue lvalue) (span-join span last-span) parstate)))))))
Function:
(defun parse-asm-output-operands (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-asm-output-operands)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) (psize (parsize parstate)) ((erp output span parstate) (parse-asm-output-operand parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate)) ((unless (token-punctuatorp token ",")) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list output) span parstate))) ((erp outputs last-span parstate) (parse-asm-output-operands parstate))) (retok (cons output outputs) (span-join span last-span) parstate))))
Function:
(defun parse-?-asm-output-operands (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-?-asm-output-operands)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (and (not (token-punctuatorp token "[")) (not (and token (token-case token :string))))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok nil (irr-span) parstate))) (parstate (unread-token parstate))) (parse-asm-output-operands parstate))))
Function:
(defun parse-asm-input-operand (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-asm-input-operand)) (declare (ignorable __function__)) (b* (((reterr) (irr-asm-input) (irr-span) parstate) ((erp token span parstate) (read-token parstate))) (cond ((token-punctuatorp token "[") (b* (((erp name & parstate) (read-identifier parstate)) ((erp & parstate) (read-punctuator "]" parstate)) ((erp token2 span2 parstate) (read-token parstate)) ((unless (and token2 (token-case token2 :string))) (reterr-msg :where (position-to-msg (span->start span2)) :expected "a string literal" :found (token-to-msg token2))) (string (token-string->unwrap token2)) ((erp strings & parstate) (parse-*-stringlit parstate)) (constraint (cons string strings)) ((erp & parstate) (read-punctuator "(" parstate)) ((erp rvalue & parstate) (parse-expression parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (make-asm-input :name name :constraint constraint :rvalue rvalue) (span-join span last-span) parstate))) (t (b* ((parstate (if token (unread-token parstate) parstate)) ((erp token2 span2 parstate) (read-token parstate)) ((unless (and token2 (token-case token2 :string))) (reterr-msg :where (position-to-msg (span->start span2)) :expected "a string literal" :found (token-to-msg token2))) (string (token-string->unwrap token2)) ((erp strings & parstate) (parse-*-stringlit parstate)) (constraint (cons string strings)) ((erp & parstate) (read-punctuator "(" parstate)) ((erp rvalue & parstate) (parse-expression parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (make-asm-input :name nil :constraint constraint :rvalue rvalue) (span-join span last-span) parstate)))))))
Function:
(defun parse-asm-input-operands (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-asm-input-operands)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) (psize (parsize parstate)) ((erp input span parstate) (parse-asm-input-operand parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token & parstate) (read-token parstate)) ((unless (token-punctuatorp token ",")) (b* ((parstate (if token (unread-token parstate) parstate))) (retok (list input) span parstate))) ((erp inputs last-span parstate) (parse-asm-input-operands parstate))) (retok (cons input inputs) (span-join span last-span) parstate))))
Function:
(defun parse-?-asm-input-operands (parstate) (declare (xargs :stobjs (parstate))) (declare (xargs :guard (parstatep parstate))) (let ((__function__ 'parse-?-asm-input-operands)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) parstate) ((erp token & parstate) (read-token parstate)) ((when (and (not (token-punctuatorp token "[")) (not (and token (token-case token :string))))) (b* ((parstate (if token (unread-token parstate) parstate))) (retok nil (irr-span) parstate))) (parstate (unread-token parstate))) (parse-asm-input-operands parstate))))
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* ((psize (parsize parstate)) ((erp cexpr & parstate) (parse-constant-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp token2 & parstate) (read-token parstate))) (cond ((and (token-punctuatorp token2 "...") (parstate->gcc parstate)) (b* ((psize (parsize parstate)) ((erp cexpr2 & parstate) (parse-constant-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp & parstate) (read-punctuator ":" parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-labeled :label (make-label-casexpr :expr cexpr :range? cexpr2) :stmt stmt) (span-join span last-span) parstate))) (t (b* ((parstate (if token2 (unread-token parstate) parstate)) ((erp & parstate) (read-punctuator ":" parstate)) ((erp stmt last-span parstate) (parse-statement parstate))) (retok (make-stmt-labeled :label (make-label-casexpr :expr cexpr :range? nil) :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)) (psize (parsize parstate)) ((erp expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((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)) (psize (parsize parstate)) ((erp expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((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)) (psize (parsize parstate)) ((erp expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((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* ((psize (parsize parstate)) ((erp stmt & parstate) (parse-statement parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((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)) (psize (parsize parstate)) ((erp test-expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp & parstate) (read-punctuator ";" parstate)) ((erp token4 span4 parstate) (read-token parstate))) (cond ((token-expression-start-p token4) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((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)) (psize (parsize parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((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)) (psize (parsize parstate)) ((erp decl/stmt & parstate) (parse-declaration-or-statement parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible))) (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)) (psize (parsize parstate)) ((erp test-expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp & parstate) (read-punctuator ";" parstate)) ((erp token4 span4 parstate) (read-token parstate))) (cond ((token-expression-start-p token4) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((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)) (psize (parsize parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((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)) (psize (parsize parstate)) ((erp test-expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp & parstate) (read-punctuator ";" parstate)) ((erp token4 span4 parstate) (read-token parstate))) (cond ((token-expression-start-p token4) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((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)) (psize (parsize parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((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)) (psize (parsize parstate)) ((erp test-expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((erp & parstate) (read-punctuator ";" parstate)) ((erp token4 span4 parstate) (read-token parstate))) (cond ((token-expression-start-p token4) (b* ((parstate (unread-token parstate)) (psize (parsize parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((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)) (psize (parsize parstate)) ((erp next-expr & parstate) (parse-expression parstate)) ((unless (mbt (<= (parsize parstate) (1- psize)))) (reterr :impossible)) ((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))) ((or (token-keywordp token "asm") (token-keywordp token "__asm") (token-keywordp token "__asm__")) (b* ((uscores (cond ((token-keywordp token "asm") (keyword-uscores-none)) ((token-keywordp token "__asm") (keyword-uscores-start)) ((token-keywordp token "__asm__") (keyword-uscores-both)))) ((erp quals & parstate) (parse-*-asm-qualifier parstate)) ((erp & parstate) (read-punctuator "(" parstate)) ((erp template & parstate) (parse-*-stringlit parstate)) ((erp token2 span2 parstate) (read-token parstate))) (cond ((token-punctuatorp token2 ")") (b* (((erp last-span parstate) (read-punctuator ";" parstate))) (retok (make-stmt-asm :uscores uscores :quals quals :template template :num-colons 0 :outputs nil :inputs nil :clobbers nil :labels nil) (span-join span last-span) parstate))) (t (b* (((unless (token-punctuatorp token2 ":")) (reterr-msg :where (position-to-msg (span->start span2)) :expected "a colon or a closed parenthesis" :found (token-to-msg token2))) (psize (parsize parstate)) ((erp outputs & parstate) (parse-?-asm-output-operands parstate)) ((unless (mbt (<= (parsize parstate) psize))) (reterr :impossible)) ((erp token3 span3 parstate) (read-token parstate))) (cond ((token-punctuatorp token3 ")") (retok (make-stmt-asm :uscores uscores :quals quals :template template :num-colons 1 :outputs outputs :inputs nil :clobbers nil :labels nil) (span-join span span3) parstate)) (t (b* (((unless (token-punctuatorp token3 ":")) (reterr-msg :where (position-to-msg (span->start span3)) :expected "a colon or a closed parenthesis" :found (token-to-msg token3))) ((erp inputs & parstate) (parse-?-asm-input-operands parstate)) ((erp token4 span4 parstate) (read-token parstate))) (cond ((token-punctuatorp token4 ")") (retok (make-stmt-asm :uscores uscores :quals quals :template template :num-colons 2 :outputs outputs :inputs inputs :clobbers nil :labels nil) (span-join span span4) parstate)) (t (b* (((unless (token-punctuatorp token4 ":")) (reterr-msg :where (position-to-msg (span->start span4)) :expected "a colon or a closed parenthesis" :found (token-to-msg token4))) ((erp clobbers & parstate) (parse-asm-clobbers parstate)) ((erp token5 span5 parstate) (read-token parstate))) (cond ((token-punctuatorp token5 ")") (retok (make-stmt-asm :uscores uscores :quals quals :template template :num-colons 3 :outputs outputs :inputs inputs :clobbers clobbers :labels nil) (span-join span span5) parstate)) (t (b* (((unless (token-punctuatorp token5 ":")) (reterr-msg :where (position-to-msg (span->start span5)) :expected "a colon or a closed parenthesis" :found (token-to-msg token5))) ((erp labels & parstate) (parse-asm-goto-labels parstate)) ((erp last-span parstate) (read-punctuator ")" parstate))) (retok (make-stmt-asm :uscores uscores :quals quals :template template :num-colons 4 :outputs outputs :inputs inputs :clobbers clobbers :labels labels) (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-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-expression-rest prev-expr prev-span parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-expression-rest prev-expr prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-expression-rest prev-expr prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-assignment-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-assignment-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-assignment-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-assignment-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-assignment-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-assignment-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-conditional-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-conditional-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-conditional-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-conditional-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-conditional-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-conditional-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-or-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-or-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-or-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-or-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-or-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-or-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-or-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-or-expression-rest prev-expr prev-span parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-or-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-or-expression-rest prev-expr prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-or-expression-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-or-expression-rest prev-expr prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-and-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-and-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-and-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-and-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-and-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-and-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-and-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-and-expression-rest prev-expr prev-span parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-and-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-and-expression-rest prev-expr prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-and-expression-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-and-expression-rest prev-expr prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-inclusive-or-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-inclusive-or-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-inclusive-or-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-inclusive-or-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-inclusive-or-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-inclusive-or-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-inclusive-or-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-inclusive-or-expression-rest prev-expr prev-span parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-inclusive-or-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-inclusive-or-expression-rest prev-expr prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-inclusive-or-expression-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-inclusive-or-expression-rest prev-expr prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-exclusive-or-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-exclusive-or-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-exclusive-or-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-exclusive-or-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-exclusive-or-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-exclusive-or-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-exclusive-or-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-exclusive-or-expression-rest prev-expr prev-span parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-exclusive-or-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-exclusive-or-expression-rest prev-expr prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-exclusive-or-expression-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-exclusive-or-expression-rest prev-expr prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-and-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-and-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-and-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-and-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-and-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-and-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-and-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-and-expression-rest prev-expr prev-span parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-and-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-and-expression-rest prev-expr prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-and-expression-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-and-expression-rest prev-expr prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-equality-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-equality-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-equality-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-equality-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-equality-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-equality-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-equality-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-equality-expression-rest prev-expr prev-span parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-equality-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-equality-expression-rest prev-expr prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-equality-expression-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-equality-expression-rest prev-expr prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-relational-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-relational-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-relational-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-relational-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-relational-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-relational-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-relational-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-relational-expression-rest prev-expr prev-span parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-relational-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-relational-expression-rest prev-expr prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-relational-expression-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-relational-expression-rest prev-expr prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-shift-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-shift-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-shift-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-shift-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-shift-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-shift-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-shift-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-shift-expression-rest prev-expr prev-span parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-shift-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-shift-expression-rest prev-expr prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-shift-expression-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-shift-expression-rest prev-expr prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-additive-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-additive-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-additive-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-additive-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-additive-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-additive-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-additive-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-additive-expression-rest prev-expr prev-span parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-additive-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-additive-expression-rest prev-expr prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-additive-expression-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-additive-expression-rest prev-expr prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-multiplicative-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-multiplicative-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-multiplicative-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-multiplicative-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-multiplicative-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-multiplicative-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-multiplicative-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-multiplicative-expression-rest prev-expr prev-span parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-multiplicative-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-multiplicative-expression-rest prev-expr prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-multiplicative-expression-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-multiplicative-expression-rest prev-expr prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-cast-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-cast-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-cast-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-cast-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-cast-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-cast-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-unary-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-unary-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-unary-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-unary-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-unary-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-unary-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-postfix-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-postfix-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-postfix-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-postfix-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-postfix-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-postfix-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-postfix-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-postfix-expression-rest prev-expr prev-span parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-postfix-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-postfix-expression-rest prev-expr prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-postfix-expression-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-postfix-expression-rest prev-expr prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-argument-expressions.exprs (b* (((mv acl2::?erp ?exprs ?span ?new-parstate) (parse-argument-expressions parstate))) (expr-listp exprs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-argument-expressions.span (b* (((mv acl2::?erp ?exprs ?span ?new-parstate) (parse-argument-expressions parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-argument-expressions.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?exprs ?span ?new-parstate) (parse-argument-expressions parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-argument-expressions-rest.exprs (b* (((mv acl2::?erp ?exprs ?span ?new-parstate) (parse-argument-expressions-rest prev-exprs prev-span parstate))) (expr-listp exprs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-argument-expressions-rest.span (b* (((mv acl2::?erp ?exprs ?span ?new-parstate) (parse-argument-expressions-rest prev-exprs prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-argument-expressions-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?exprs ?span ?new-parstate) (parse-argument-expressions-rest prev-exprs prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-primary-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-primary-expression parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-primary-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-primary-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-primary-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-primary-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-compound-literal.expr (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-compound-literal tyname first-span parstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-compound-literal.span (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-compound-literal tyname first-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-compound-literal.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-compound-literal tyname first-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-generic-association.genassoc (b* (((mv acl2::?erp ?genassoc ?span ?new-parstate) (parse-generic-association parstate))) (genassocp genassoc)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-generic-association.span (b* (((mv acl2::?erp ?genassoc ?span ?new-parstate) (parse-generic-association parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-generic-association.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?genassoc ?span ?new-parstate) (parse-generic-association parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-generic-associations-rest.genassocs (b* (((mv acl2::?erp ?genassocs ?span ?new-parstate) (parse-generic-associations-rest prev-genassocs prev-span parstate))) (genassoc-listp genassocs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-generic-associations-rest.span (b* (((mv acl2::?erp ?genassocs ?span ?new-parstate) (parse-generic-associations-rest prev-genassocs prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-generic-associations-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?genassocs ?span ?new-parstate) (parse-generic-associations-rest prev-genassocs prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-member-designor.memdes (b* (((mv acl2::?erp ?memdes ?span ?new-parstate) (parse-member-designor parstate))) (member-designorp memdes)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-member-designor.span (b* (((mv acl2::?erp ?memdes ?span ?new-parstate) (parse-member-designor parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-member-designor.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?memdes ?span ?new-parstate) (parse-member-designor parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-member-designor-rest.memdes (b* (((mv acl2::?erp ?memdes ?span ?new-parstate) (parse-member-designor-rest prev-memdes prev-span parstate))) (member-designorp memdes)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-member-designor-rest.span (b* (((mv acl2::?erp ?memdes ?span ?new-parstate) (parse-member-designor-rest prev-memdes prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-member-designor-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?memdes ?span ?new-parstate) (parse-member-designor-rest prev-memdes prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-constant-expression.cexpr (b* (((mv acl2::?erp ?cexpr ?span ?new-parstate) (parse-constant-expression parstate))) (const-exprp cexpr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-constant-expression.span (b* (((mv acl2::?erp ?cexpr ?span ?new-parstate) (parse-constant-expression parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-constant-expression.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?cexpr ?span ?new-parstate) (parse-constant-expression parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-static-assert-declaration.statassert (b* (((mv acl2::?erp ?statassert ?span ?new-parstate) (parse-static-assert-declaration first-span parstate))) (statassertp statassert)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-static-assert-declaration.span (b* (((mv acl2::?erp ?statassert ?span ?new-parstate) (parse-static-assert-declaration first-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-static-assert-declaration.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?statassert ?span ?new-parstate) (parse-static-assert-declaration first-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designator.designor (b* (((mv acl2::?erp ?designor ?span ?new-parstate) (parse-designator parstate))) (designorp designor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designator.span (b* (((mv acl2::?erp ?designor ?span ?new-parstate) (parse-designator parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designator.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?designor ?span ?new-parstate) (parse-designator parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designator-list.designors (b* (((mv acl2::?erp ?designors ?span ?new-parstate) (parse-designator-list parstate))) (designor-listp designors)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designator-list.span (b* (((mv acl2::?erp ?designors ?span ?new-parstate) (parse-designator-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designator-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?designors ?span ?new-parstate) (parse-designator-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-initializer.initer (b* (((mv acl2::?erp ?initer ?span ?new-parstate) (parse-initializer parstate))) (initerp initer)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-initializer.span (b* (((mv acl2::?erp ?initer ?span ?new-parstate) (parse-initializer parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-initializer.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?initer ?span ?new-parstate) (parse-initializer parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designation?-initializer.desiniter (b* (((mv acl2::?erp ?desiniter ?span ?new-parstate) (parse-designation?-initializer parstate))) (desiniterp desiniter)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designation?-initializer.span (b* (((mv acl2::?erp ?desiniter ?span ?new-parstate) (parse-designation?-initializer parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designation?-initializer.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?desiniter ?span ?new-parstate) (parse-designation?-initializer parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-initializer-list.desiniters (b* (((mv acl2::?erp ?desiniters ?final-comma ?span ?new-parstate) (parse-initializer-list parstate))) (desiniter-listp desiniters)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-initializer-list.final-comma (b* (((mv acl2::?erp ?desiniters ?final-comma ?span ?new-parstate) (parse-initializer-list parstate))) (booleanp final-comma)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-initializer-list.span (b* (((mv acl2::?erp ?desiniters ?final-comma ?span ?new-parstate) (parse-initializer-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-initializer-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?desiniters ?final-comma ?span ?new-parstate) (parse-initializer-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enumerator.enumer (b* (((mv acl2::?erp ?enumer ?span ?new-parstate) (parse-enumerator parstate))) (enumerp enumer)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enumerator.span (b* (((mv acl2::?erp ?enumer ?span ?new-parstate) (parse-enumerator parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enumerator.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?enumer ?span ?new-parstate) (parse-enumerator parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enumerator-list.enumers (b* (((mv acl2::?erp ?enumers ?final-comma ?span ?new-parstate) (parse-enumerator-list parstate))) (enumer-listp enumers)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enumerator-list.final-comma (b* (((mv acl2::?erp ?enumers ?final-comma ?span ?new-parstate) (parse-enumerator-list parstate))) (booleanp final-comma)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enumerator-list.span (b* (((mv acl2::?erp ?enumers ?final-comma ?span ?new-parstate) (parse-enumerator-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enumerator-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?enumers ?final-comma ?span ?new-parstate) (parse-enumerator-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-specifier/qualifier.specqual (b* (((mv acl2::?erp ?specqual ?span ?new-parstate) (parse-specifier/qualifier tyspec-seenp parstate))) (spec/qual-p specqual)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-specifier/qualifier.span (b* (((mv acl2::?erp ?specqual ?span ?new-parstate) (parse-specifier/qualifier tyspec-seenp parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-specifier/qualifier.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?specqual ?span ?new-parstate) (parse-specifier/qualifier tyspec-seenp parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-specifier-qualifier-list.specquals (b* (((mv acl2::?erp ?specquals ?span ?new-parstate) (parse-specifier-qualifier-list tyspec-seenp parstate))) (spec/qual-listp specquals)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-specifier-qualifier-list.span (b* (((mv acl2::?erp ?specquals ?span ?new-parstate) (parse-specifier-qualifier-list tyspec-seenp parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-specifier-qualifier-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?specquals ?span ?new-parstate) (parse-specifier-qualifier-list tyspec-seenp parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-specifier.declspec (b* (((mv acl2::?erp ?declspec ?span ?new-parstate) (parse-declaration-specifier tyspec-seenp parstate))) (declspecp declspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-specifier.span (b* (((mv acl2::?erp ?declspec ?span ?new-parstate) (parse-declaration-specifier tyspec-seenp parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-specifier.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?declspec ?span ?new-parstate) (parse-declaration-specifier tyspec-seenp parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-specifiers.declspecs (b* (((mv acl2::?erp ?declspecs ?span ?new-parstate) (parse-declaration-specifiers tyspec-seenp parstate))) (declspec-listp declspecs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-specifiers.span (b* (((mv acl2::?erp ?declspecs ?span ?new-parstate) (parse-declaration-specifiers tyspec-seenp parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-specifiers.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?declspecs ?span ?new-parstate) (parse-declaration-specifiers tyspec-seenp parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-type-qualifier-or-attribute-specifier.tyqual/attrib (b* (((mv acl2::?erp ?tyqual/attrib ?span ?new-parstate) (parse-type-qualifier-or-attribute-specifier parstate))) (typequal/attribspec-p tyqual/attrib)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-type-qualifier-or-attribute-specifier.span (b* (((mv acl2::?erp ?tyqual/attrib ?span ?new-parstate) (parse-type-qualifier-or-attribute-specifier parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-type-qualifier-or-attribute-specifier.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?tyqual/attrib ?span ?new-parstate) (parse-type-qualifier-or-attribute-specifier parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-type-qualifier-and-attribute-specifier-list.tyqualattribs (b* (((mv acl2::?erp ?tyqualattribs ?span ?new-parstate) (parse-type-qualifier-and-attribute-specifier-list parstate))) (typequal/attribspec-listp tyqualattribs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-type-qualifier-and-attribute-specifier-list.span (b* (((mv acl2::?erp ?tyqualattribs ?span ?new-parstate) (parse-type-qualifier-and-attribute-specifier-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-type-qualifier-and-attribute-specifier-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?tyqualattribs ?span ?new-parstate) (parse-type-qualifier-and-attribute-specifier-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-pointer.tyqualattribss (b* (((mv acl2::?erp ?tyqualattribss ?span ?new-parstate) (parse-pointer parstate))) (typequal/attribspec-list-listp tyqualattribss)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-pointer.span (b* (((mv acl2::?erp ?tyqualattribss ?span ?new-parstate) (parse-pointer parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-pointer.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?tyqualattribss ?span ?new-parstate) (parse-pointer parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-or-union-specifier.strunispec (b* (((mv acl2::?erp ?strunispec ?span ?new-parstate) (parse-struct-or-union-specifier parstate))) (strunispecp strunispec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-or-union-specifier.span (b* (((mv acl2::?erp ?strunispec ?span ?new-parstate) (parse-struct-or-union-specifier parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-or-union-specifier.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?strunispec ?span ?new-parstate) (parse-struct-or-union-specifier parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enum-specifier.enumspec (b* (((mv acl2::?erp ?enumspec ?span ?new-parstate) (parse-enum-specifier first-span parstate))) (enumspecp enumspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enum-specifier.span (b* (((mv acl2::?erp ?enumspec ?span ?new-parstate) (parse-enum-specifier first-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enum-specifier.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?enumspec ?span ?new-parstate) (parse-enum-specifier first-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-alignment-specifier.alignspec (b* (((mv acl2::?erp ?alignspec ?span ?new-parstate) (parse-alignment-specifier first-span parstate))) (align-specp alignspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-alignment-specifier.span (b* (((mv acl2::?erp ?alignspec ?span ?new-parstate) (parse-alignment-specifier first-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-alignment-specifier.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?alignspec ?span ?new-parstate) (parse-alignment-specifier first-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-array/function-abstract-declarator.dirabsdeclor (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-array/function-abstract-declarator parstate))) (dirabsdeclorp dirabsdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-array/function-abstract-declarator.span (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-array/function-abstract-declarator parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-array/function-abstract-declarator.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-array/function-abstract-declarator parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-abstract-declarator.dirabsdeclor (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-direct-abstract-declarator parstate))) (dirabsdeclorp dirabsdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-abstract-declarator.span (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-direct-abstract-declarator parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-abstract-declarator.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-direct-abstract-declarator parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-abstract-declarator-rest.dirabsdeclor (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-direct-abstract-declarator-rest prev-dirabsdeclor prev-span parstate))) (dirabsdeclorp dirabsdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-abstract-declarator-rest.span (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-direct-abstract-declarator-rest prev-dirabsdeclor prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-abstract-declarator-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-direct-abstract-declarator-rest prev-dirabsdeclor prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-abstract-declarator.absdeclor (b* (((mv acl2::?erp ?absdeclor ?span ?new-parstate) (parse-abstract-declarator parstate))) (absdeclorp absdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-abstract-declarator.span (b* (((mv acl2::?erp ?absdeclor ?span ?new-parstate) (parse-abstract-declarator parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-abstract-declarator.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?absdeclor ?span ?new-parstate) (parse-abstract-declarator parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-array/function-declarator.dirdeclor (b* (((mv acl2::?erp ?dirdeclor ?span ?new-parstate) (parse-array/function-declarator prev-dirdeclor prev-span parstate))) (dirdeclorp dirdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-array/function-declarator.span (b* (((mv acl2::?erp ?dirdeclor ?span ?new-parstate) (parse-array/function-declarator prev-dirdeclor prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-array/function-declarator.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?dirdeclor ?span ?new-parstate) (parse-array/function-declarator prev-dirdeclor prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-declarator.dirdeclor (b* (((mv acl2::?erp ?dirdeclor ?span ?new-parstate) (parse-direct-declarator parstate))) (dirdeclorp dirdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-declarator.span (b* (((mv acl2::?erp ?dirdeclor ?span ?new-parstate) (parse-direct-declarator parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-declarator.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?dirdeclor ?span ?new-parstate) (parse-direct-declarator parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-declarator-rest.dirdeclor (b* (((mv acl2::?erp ?dirdeclor ?span ?new-parstate) (parse-direct-declarator-rest prev-dirdeclor prev-span parstate))) (dirdeclorp dirdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-declarator-rest.span (b* (((mv acl2::?erp ?dirdeclor ?span ?new-parstate) (parse-direct-declarator-rest prev-dirdeclor prev-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-declarator-rest.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?dirdeclor ?span ?new-parstate) (parse-direct-declarator-rest prev-dirdeclor prev-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declarator.declor (b* (((mv acl2::?erp ?declor ?span ?new-parstate) (parse-declarator parstate))) (declorp declor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declarator.span (b* (((mv acl2::?erp ?declor ?span ?new-parstate) (parse-declarator parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declarator.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?declor ?span ?new-parstate) (parse-declarator parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declarator.structdeclor (b* (((mv acl2::?erp ?structdeclor ?span ?new-parstate) (parse-struct-declarator parstate))) (structdeclorp structdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declarator.span (b* (((mv acl2::?erp ?structdeclor ?span ?new-parstate) (parse-struct-declarator parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declarator.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?structdeclor ?span ?new-parstate) (parse-struct-declarator parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declarator-list.structdeclors (b* (((mv acl2::?erp ?structdeclors ?span ?new-parstate) (parse-struct-declarator-list parstate))) (structdeclor-listp structdeclors)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declarator-list.span (b* (((mv acl2::?erp ?structdeclors ?span ?new-parstate) (parse-struct-declarator-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declarator-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?structdeclors ?span ?new-parstate) (parse-struct-declarator-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declaration.structdecl (b* (((mv acl2::?erp ?structdecl ?span ?new-parstate) (parse-struct-declaration parstate))) (structdeclp structdecl)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declaration.span (b* (((mv acl2::?erp ?structdecl ?span ?new-parstate) (parse-struct-declaration parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declaration.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?structdecl ?span ?new-parstate) (parse-struct-declaration parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declaration-list.structdecls (b* (((mv acl2::?erp ?structdecls ?span ?new-parstate) (parse-struct-declaration-list parstate))) (structdecl-listp structdecls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declaration-list.span (b* (((mv acl2::?erp ?structdecls ?span ?new-parstate) (parse-struct-declaration-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declaration-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?structdecls ?span ?new-parstate) (parse-struct-declaration-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-parameter-declaration.paramdecl (b* (((mv acl2::?erp ?paramdecl ?span ?new-parstate) (parse-parameter-declaration parstate))) (paramdeclp paramdecl)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-parameter-declaration.span (b* (((mv acl2::?erp ?paramdecl ?span ?new-parstate) (parse-parameter-declaration parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-parameter-declaration.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?paramdecl ?span ?new-parstate) (parse-parameter-declaration parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-parameter-declaration-list.paramdecls (b* (((mv acl2::?erp ?paramdecls ?ellipsis ?span ?new-parstate) (parse-parameter-declaration-list parstate))) (paramdecl-listp paramdecls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-parameter-declaration-list.ellipsis (b* (((mv acl2::?erp ?paramdecls ?ellipsis ?span ?new-parstate) (parse-parameter-declaration-list parstate))) (booleanp ellipsis)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-parameter-declaration-list.span (b* (((mv acl2::?erp ?paramdecls ?ellipsis ?span ?new-parstate) (parse-parameter-declaration-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-parameter-declaration-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?paramdecls ?ellipsis ?span ?new-parstate) (parse-parameter-declaration-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-type-name.tyname (b* (((mv acl2::?erp ?tyname ?span ?new-parstate) (parse-type-name parstate))) (tynamep tyname)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-type-name.span (b* (((mv acl2::?erp ?tyname ?span ?new-parstate) (parse-type-name parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-type-name.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?tyname ?span ?new-parstate) (parse-type-name parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression-or-type-name.expr/tyname (b* (((mv acl2::?erp ?expr/tyname ?span ?new-parstate) (parse-expression-or-type-name parstate))) (amb?-expr/tyname-p expr/tyname)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression-or-type-name.span (b* (((mv acl2::?erp ?expr/tyname ?span ?new-parstate) (parse-expression-or-type-name parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression-or-type-name.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?expr/tyname ?span ?new-parstate) (parse-expression-or-type-name parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declarator-or-abstract-declarator.declor/absdeclor (b* (((mv acl2::?erp ?declor/absdeclor ?span ?new-parstate) (parse-declarator-or-abstract-declarator parstate))) (amb?-declor/absdeclor-p declor/absdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declarator-or-abstract-declarator.span (b* (((mv acl2::?erp ?declor/absdeclor ?span ?new-parstate) (parse-declarator-or-abstract-declarator parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declarator-or-abstract-declarator.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?declor/absdeclor ?span ?new-parstate) (parse-declarator-or-abstract-declarator parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-parameters.attrparams (b* (((mv acl2::?erp ?attrparams ?span ?new-parstate) (parse-attribute-parameters parstate))) (expr-listp attrparams)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-parameters.span (b* (((mv acl2::?erp ?attrparams ?span ?new-parstate) (parse-attribute-parameters parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-parameters.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?attrparams ?span ?new-parstate) (parse-attribute-parameters parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute.attr (b* (((mv acl2::?erp ?attr ?span ?new-parstate) (parse-attribute parstate))) (attribp attr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute.span (b* (((mv acl2::?erp ?attr ?span ?new-parstate) (parse-attribute parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?attr ?span ?new-parstate) (parse-attribute parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-list.attrs (b* (((mv acl2::?erp ?attrs ?span ?new-parstate) (parse-attribute-list parstate))) (attrib-listp attrs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-list.span (b* (((mv acl2::?erp ?attrs ?span ?new-parstate) (parse-attribute-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?attrs ?span ?new-parstate) (parse-attribute-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-specifier.attrspec (b* (((mv acl2::?erp ?attrspec ?span ?new-parstate) (parse-attribute-specifier uscores first-span parstate))) (attrib-specp attrspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-specifier.span (b* (((mv acl2::?erp ?attrspec ?span ?new-parstate) (parse-attribute-specifier uscores first-span parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-specifier.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?attrspec ?span ?new-parstate) (parse-attribute-specifier uscores first-span parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-*-attribute-specifier.attrspecs (b* (((mv acl2::?erp ?attrspecs ?span ?new-parstate) (parse-*-attribute-specifier parstate))) (attrib-spec-listp attrspecs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-*-attribute-specifier.span (b* (((mv acl2::?erp ?attrspecs ?span ?new-parstate) (parse-*-attribute-specifier parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-*-attribute-specifier.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?attrspecs ?span ?new-parstate) (parse-*-attribute-specifier parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-init-declarator.initdeclor (b* (((mv acl2::?erp ?initdeclor ?span ?new-parstate) (parse-init-declarator parstate))) (initdeclorp initdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-init-declarator.span (b* (((mv acl2::?erp ?initdeclor ?span ?new-parstate) (parse-init-declarator parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-init-declarator.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?initdeclor ?span ?new-parstate) (parse-init-declarator parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-init-declarator-list.initdeclors (b* (((mv acl2::?erp ?initdeclors ?span ?new-parstate) (parse-init-declarator-list parstate))) (initdeclor-listp initdeclors)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-init-declarator-list.span (b* (((mv acl2::?erp ?initdeclors ?span ?new-parstate) (parse-init-declarator-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-init-declarator-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?initdeclors ?span ?new-parstate) (parse-init-declarator-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration.decl (b* (((mv acl2::?erp ?decl ?span ?new-parstate) (parse-declaration parstate))) (declp decl)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration.span (b* (((mv acl2::?erp ?decl ?span ?new-parstate) (parse-declaration parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?decl ?span ?new-parstate) (parse-declaration parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-list.decls (b* (((mv acl2::?erp ?decls ?span ?new-parstate) (parse-declaration-list parstate))) (decl-listp decls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-list.span (b* (((mv acl2::?erp ?decls ?span ?new-parstate) (parse-declaration-list parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-list.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?decls ?span ?new-parstate) (parse-declaration-list parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-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 return-type-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 return-type-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 return-type-of-parse-asm-output-operand.output (b* (((mv acl2::?erp ?output ?span ?new-parstate) (parse-asm-output-operand parstate))) (asm-outputp output)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-asm-output-operand.span (b* (((mv acl2::?erp ?output ?span ?new-parstate) (parse-asm-output-operand parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-asm-output-operand.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?output ?span ?new-parstate) (parse-asm-output-operand parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-asm-output-operands.outputs (b* (((mv acl2::?erp ?outputs ?span ?new-parstate) (parse-asm-output-operands parstate))) (asm-output-listp outputs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-asm-output-operands.span (b* (((mv acl2::?erp ?outputs ?span ?new-parstate) (parse-asm-output-operands parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-asm-output-operands.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?outputs ?span ?new-parstate) (parse-asm-output-operands parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-?-asm-output-operands.outputs (b* (((mv acl2::?erp ?outputs ?span ?new-parstate) (parse-?-asm-output-operands parstate))) (asm-output-listp outputs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-?-asm-output-operands.span (b* (((mv acl2::?erp ?outputs ?span ?new-parstate) (parse-?-asm-output-operands parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-?-asm-output-operands.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?outputs ?span ?new-parstate) (parse-?-asm-output-operands parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-asm-input-operand.input (b* (((mv acl2::?erp ?input ?span ?new-parstate) (parse-asm-input-operand parstate))) (asm-inputp input)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-asm-input-operand.span (b* (((mv acl2::?erp ?input ?span ?new-parstate) (parse-asm-input-operand parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-asm-input-operand.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?input ?span ?new-parstate) (parse-asm-input-operand parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-asm-input-operands.inputs (b* (((mv acl2::?erp ?inputs ?span ?new-parstate) (parse-asm-input-operands parstate))) (asm-input-listp inputs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-asm-input-operands.span (b* (((mv acl2::?erp ?inputs ?span ?new-parstate) (parse-asm-input-operands parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-asm-input-operands.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?inputs ?span ?new-parstate) (parse-asm-input-operands parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-?-asm-input-operands.inputs (b* (((mv acl2::?erp ?inputs ?span ?new-parstate) (parse-?-asm-input-operands parstate))) (asm-input-listp inputs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-?-asm-input-operands.span (b* (((mv acl2::?erp ?inputs ?span ?new-parstate) (parse-?-asm-input-operands parstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-?-asm-input-operands.new-parstate (implies (parstatep parstate) (b* (((mv acl2::?erp ?inputs ?span ?new-parstate) (parse-?-asm-input-operands parstate))) (parstatep new-parstate))) :rule-classes :rewrite)
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-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-expression-rest prev-expr prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-assignment-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-assignment-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-conditional-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-conditional-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-logical-or-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-or-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-logical-or-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-or-expression-rest prev-expr prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-logical-and-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-and-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-logical-and-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-and-expression-rest prev-expr prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-inclusive-or-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-inclusive-or-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-inclusive-or-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-inclusive-or-expression-rest prev-expr prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-exclusive-or-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-exclusive-or-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-exclusive-or-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-exclusive-or-expression-rest prev-expr prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-and-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-and-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-and-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-and-expression-rest prev-expr prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-equality-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-equality-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-equality-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-equality-expression-rest prev-expr prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-relational-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-relational-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-relational-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-relational-expression-rest prev-expr prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-shift-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-shift-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-shift-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-shift-expression-rest prev-expr prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-additive-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-additive-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-additive-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-additive-expression-rest prev-expr prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-multiplicative-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-multiplicative-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-multiplicative-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-multiplicative-expression-rest prev-expr prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-cast-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-cast-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-unary-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-unary-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-postfix-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-postfix-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-postfix-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-postfix-expression-rest prev-expr prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-argument-expressions-uncond (b* (((mv acl2::?erp ?exprs ?span ?new-parstate) (parse-argument-expressions parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-argument-expressions-rest-uncond (b* (((mv acl2::?erp ?exprs ?span ?new-parstate) (parse-argument-expressions-rest prev-exprs prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-primary-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-primary-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-generic-associations-rest-uncond (b* (((mv acl2::?erp ?genassocs ?span ?new-parstate) (parse-generic-associations-rest prev-genassocs prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-generic-association-uncond (b* (((mv acl2::?erp ?genassoc ?span ?new-parstate) (parse-generic-association parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-compound-literal-uncond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-compound-literal tyname first-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-member-designor-uncond (b* (((mv acl2::?erp ?memdes ?span ?new-parstate) (parse-member-designor parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-member-designor-rest-uncond (b* (((mv acl2::?erp ?memdes ?span ?new-parstate) (parse-member-designor-rest prev-memdes prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-constant-expression-uncond (b* (((mv acl2::?erp ?cexpr ?span ?new-parstate) (parse-constant-expression parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-static-assert-declaration-uncond (b* (((mv acl2::?erp ?statassert ?span ?new-parstate) (parse-static-assert-declaration first-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-designator-uncond (b* (((mv acl2::?erp ?designor ?span ?new-parstate) (parse-designator parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-designator-list-uncond (b* (((mv acl2::?erp ?designors ?span ?new-parstate) (parse-designator-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse--initializer-uncond (b* (((mv acl2::?erp ?initer ?span ?new-parstate) (parse-initializer parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-designation?-initializer-uncond (b* (((mv acl2::?erp ?desiniter ?span ?new-parstate) (parse-designation?-initializer parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-initializer-list-uncond (b* (((mv acl2::?erp ?desiniters ?final-comma ?span ?new-parstate) (parse-initializer-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-enumerator-uncond (b* (((mv acl2::?erp ?enumer ?span ?new-parstate) (parse-enumerator parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-enumerator-list-uncond (b* (((mv acl2::?erp ?enumers ?final-comma ?span ?new-parstate) (parse-enumerator-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-specifier/qualifier-uncond (b* (((mv acl2::?erp ?specqual ?span ?new-parstate) (parse-specifier/qualifier tyspec-seenp parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-specifier-qualifier-list-uncond (b* (((mv acl2::?erp ?specquals ?span ?new-parstate) (parse-specifier-qualifier-list tyspec-seenp parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-specifier-uncond (b* (((mv acl2::?erp ?declspec ?span ?new-parstate) (parse-declaration-specifier tyspec-seenp parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-specifiers-uncond (b* (((mv acl2::?erp ?declspecs ?span ?new-parstate) (parse-declaration-specifiers tyspec-seenp parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-type-qualifier-or-attribute-specifier-uncond (b* (((mv acl2::?erp ?tyqual/attrib ?span ?new-parstate) (parse-type-qualifier-or-attribute-specifier parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-type-qualifier-and-attribute-specifier-list-uncond (b* (((mv acl2::?erp ?tyqualattribs ?span ?new-parstate) (parse-type-qualifier-and-attribute-specifier-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-pointer-uncond (b* (((mv acl2::?erp ?tyqualattribss ?span ?new-parstate) (parse-pointer parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-or-union-specifier-uncond (b* (((mv acl2::?erp ?strunispec ?span ?new-parstate) (parse-struct-or-union-specifier parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-enum-specifier-uncond (b* (((mv acl2::?erp ?enumspec ?span ?new-parstate) (parse-enum-specifier first-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-alignment-specifier-uncond (b* (((mv acl2::?erp ?alignspec ?span ?new-parstate) (parse-alignment-specifier first-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-array/function-abstract-declarator-uncond (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-array/function-abstract-declarator parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-direct-abstract-declarator-uncond (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-direct-abstract-declarator parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-direct-abstract-declarator-rest-uncond (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-direct-abstract-declarator-rest prev-dirabsdeclor prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-abstract-declarator-uncond (b* (((mv acl2::?erp ?absdeclor ?span ?new-parstate) (parse-abstract-declarator parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-array/function-declarator-uncond (b* (((mv acl2::?erp ?dirdeclor ?span ?new-parstate) (parse-array/function-declarator prev-dirdeclor prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-direct-declarator-uncond (b* (((mv acl2::?erp ?dirdeclor ?span ?new-parstate) (parse-direct-declarator parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-direct-declarator-rest-uncond (b* (((mv acl2::?erp ?dirdeclor ?span ?new-parstate) (parse-direct-declarator-rest prev-dirdeclor prev-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declarator-uncond (b* (((mv acl2::?erp ?declor ?span ?new-parstate) (parse-declarator parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declarator-uncond (b* (((mv acl2::?erp ?structdeclor ?span ?new-parstate) (parse-struct-declarator parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declarator-list-uncond (b* (((mv acl2::?erp ?structdeclors ?span ?new-parstate) (parse-struct-declarator-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declaration-uncond (b* (((mv acl2::?erp ?structdecl ?span ?new-parstate) (parse-struct-declaration parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declaration-list-uncond (b* (((mv acl2::?erp ?structdecls ?span ?new-parstate) (parse-struct-declaration-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-parameter-declaration-uncond (b* (((mv acl2::?erp ?paramdecl ?span ?new-parstate) (parse-parameter-declaration parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-parameter-declaration-list-uncond (b* (((mv acl2::?erp ?paramdecls ?ellipsis ?span ?new-parstate) (parse-parameter-declaration-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-type-name-uncond (b* (((mv acl2::?erp ?tyname ?span ?new-parstate) (parse-type-name parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-expression-or-type-name-uncond (b* (((mv acl2::?erp ?expr/tyname ?span ?new-parstate) (parse-expression-or-type-name parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declarator-or-abstract-declarator-uncond (b* (((mv acl2::?erp ?declor/absdeclor ?span ?new-parstate) (parse-declarator-or-abstract-declarator parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-parameters-uncond (b* (((mv acl2::?erp ?attrparams ?span ?new-parstate) (parse-attribute-parameters parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-uncond (b* (((mv acl2::?erp ?attr ?span ?new-parstate) (parse-attribute parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-list-uncond (b* (((mv acl2::?erp ?attrs ?span ?new-parstate) (parse-attribute-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-specifier-uncond (b* (((mv acl2::?erp ?attrspec ?span ?new-parstate) (parse-attribute-specifier uscores first-span parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-*-attribute-specifier-uncond (b* (((mv acl2::?erp ?attrspecs ?span ?new-parstate) (parse-*-attribute-specifier parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-init-declarator-uncond (b* (((mv acl2::?erp ?initdeclor ?span ?new-parstate) (parse-init-declarator parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-init-declarator-list-uncond (b* (((mv acl2::?erp ?initdeclors ?span ?new-parstate) (parse-init-declarator-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-uncond (b* (((mv acl2::?erp ?decl ?span ?new-parstate) (parse-declaration parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-list-uncond (b* (((mv acl2::?erp ?decls ?span ?new-parstate) (parse-declaration-list parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
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-asm-output-operand-uncond (b* (((mv acl2::?erp ?output ?span ?new-parstate) (parse-asm-output-operand parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-asm-output-operands (b* (((mv acl2::?erp ?outputs ?span ?new-parstate) (parse-asm-output-operands parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-?-asm-output-operands-uncond (b* (((mv acl2::?erp ?outputs ?span ?new-parstate) (parse-?-asm-output-operands parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-asm-input-operand-uncond (b* (((mv acl2::?erp ?input ?span ?new-parstate) (parse-asm-input-operand parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-asm-input-operands (b* (((mv acl2::?erp ?inputs ?span ?new-parstate) (parse-asm-input-operands parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-?-asm-input-operands-uncond (b* (((mv acl2::?erp ?inputs ?span ?new-parstate) (parse-?-asm-input-operands parstate))) (<= (parsize new-parstate) (parsize parstate))) :rule-classes :linear)
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-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-expression-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-assignment-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-assignment-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-conditional-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-conditional-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-logical-or-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-or-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-logical-or-expression-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-logical-and-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-logical-and-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-logical-and-expression-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-inclusive-or-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-inclusive-or-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-inclusive-or-expression-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-exclusive-or-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-exclusive-or-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-exclusive-or-expression-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-and-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-and-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-and-expression-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-equality-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-equality-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-equality-expression-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-relational-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-relational-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-relational-expression-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-shift-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-shift-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-shift-expression-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-additive-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-additive-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-additive-expression-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-multiplicative-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-multiplicative-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-multiplicative-expression-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-cast-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-cast-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-unary-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-unary-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-postfix-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-postfix-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-postfix-expression-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-argument-expressions-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-argument-expressions-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-primary-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-primary-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-generic-associations-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-generic-association-cond (b* (((mv acl2::?erp ?genassoc ?span ?new-parstate) (parse-generic-association parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-member-designor-cond (b* (((mv acl2::?erp ?memdes ?span ?new-parstate) (parse-member-designor parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-member-designor-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-compound-literal-cond (b* (((mv acl2::?erp ?expr ?span ?new-parstate) (parse-compound-literal tyname first-span parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-constant-expression-cond (b* (((mv acl2::?erp ?cexpr ?span ?new-parstate) (parse-constant-expression parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-static-assert-declaration-cond (b* (((mv acl2::?erp ?statassert ?span ?new-parstate) (parse-static-assert-declaration first-span parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-designator-cond (b* (((mv acl2::?erp ?designor ?span ?new-parstate) (parse-designator parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-designator-list-cond (b* (((mv acl2::?erp ?designors ?span ?new-parstate) (parse-designator-list parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-initializer-cond (b* (((mv acl2::?erp ?initer ?span ?new-parstate) (parse-initializer parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-designation?-initializer-cond (b* (((mv acl2::?erp ?desiniter ?span ?new-parstate) (parse-designation?-initializer parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-initializer-list-cond (b* (((mv acl2::?erp ?desiniters ?final-comma ?span ?new-parstate) (parse-initializer-list parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-enumerator-cond (b* (((mv acl2::?erp ?enumer ?span ?new-parstate) (parse-enumerator parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-enumerator-list-cond (b* (((mv acl2::?erp ?enumers ?final-comma ?span ?new-parstate) (parse-enumerator-list parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-specifier/qualifier-cond (b* (((mv acl2::?erp ?specqual ?span ?new-parstate) (parse-specifier/qualifier tyspec-seenp parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-specifier-qualifier-list-cond (b* (((mv acl2::?erp ?specquals ?span ?new-parstate) (parse-specifier-qualifier-list tyspec-seenp parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-specifier-cond (b* (((mv acl2::?erp ?declspec ?span ?new-parstate) (parse-declaration-specifier tyspec-seenp parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-specifiers-cond (b* (((mv acl2::?erp ?declspecs ?span ?new-parstate) (parse-declaration-specifiers tyspec-seenp parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-type-qualifier-or-attribute-specifier-cond (b* (((mv acl2::?erp ?tyqual/attrib ?span ?new-parstate) (parse-type-qualifier-or-attribute-specifier parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-type-qualifier-and-attribute-specifier-list-cond (b* (((mv acl2::?erp ?tyqualattribs ?span ?new-parstate) (parse-type-qualifier-and-attribute-specifier-list parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-pointer-cond (b* (((mv acl2::?erp ?tyqualattribss ?span ?new-parstate) (parse-pointer parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-or-union-specifier-cond (b* (((mv acl2::?erp ?strunispec ?span ?new-parstate) (parse-struct-or-union-specifier parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-enum-specifier-cond (b* (((mv acl2::?erp ?enumspec ?span ?new-parstate) (parse-enum-specifier first-span parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-alignment-specifier-cond (b* (((mv acl2::?erp ?alignspec ?span ?new-parstate) (parse-alignment-specifier first-span parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-array/function-abstract-declarator-cond (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-array/function-abstract-declarator parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-direct-abstract-declarator-cond (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-direct-abstract-declarator parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-direct-abstract-declarator-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-abstract-declarator-cond (b* (((mv acl2::?erp ?absdeclor ?span ?new-parstate) (parse-abstract-declarator parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-array/function-declarator-cond (b* (((mv acl2::?erp ?dirdeclor ?span ?new-parstate) (parse-array/function-declarator prev-dirdeclor prev-span parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-direct-declarator-cond (b* (((mv acl2::?erp ?dirdeclor ?span ?new-parstate) (parse-direct-declarator parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-direct-declarator-rest-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-declarator-cond (b* (((mv acl2::?erp ?declor ?span ?new-parstate) (parse-declarator parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declarator-cond (b* (((mv acl2::?erp ?structdeclor ?span ?new-parstate) (parse-struct-declarator parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declarator-list-cond (b* (((mv acl2::?erp ?structdeclors ?span ?new-parstate) (parse-struct-declarator-list parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declaration-cond (b* (((mv acl2::?erp ?structdecl ?span ?new-parstate) (parse-struct-declaration parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declaration-list-cond (b* (((mv acl2::?erp ?structdecls ?span ?new-parstate) (parse-struct-declaration-list parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-parameter-declaration-cond (b* (((mv acl2::?erp ?paramdecl ?span ?new-parstate) (parse-parameter-declaration parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-parameter-declaration-list-cond (b* (((mv acl2::?erp ?paramdecls ?ellipsis ?span ?new-parstate) (parse-parameter-declaration-list parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-type-name-cond (b* (((mv acl2::?erp ?tyname ?span ?new-parstate) (parse-type-name parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-expression-or-type-name-cond (b* (((mv acl2::?erp ?expr/tyname ?span ?new-parstate) (parse-expression-or-type-name parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declarator-or-abstract-declarator-cond (b* (((mv acl2::?erp ?declor/absdeclor ?span ?new-parstate) (parse-declarator-or-abstract-declarator parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-parameters-cond (b* (((mv acl2::?erp ?attrparams ?span ?new-parstate) (parse-attribute-parameters parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-cond (b* (((mv acl2::?erp ?attr ?span ?new-parstate) (parse-attribute parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-list-cond (b* (((mv acl2::?erp ?attrs ?span ?new-parstate) (parse-attribute-list parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-specifier-cond (b* (((mv acl2::?erp ?attrspec ?span ?new-parstate) (parse-attribute-specifier uscores first-span parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-*-attribute-specifier-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-init-declarator-cond (b* (((mv acl2::?erp ?initdeclor ?span ?new-parstate) (parse-init-declarator parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-init-declarator-list-cond (b* (((mv acl2::?erp ?initdeclors ?span ?new-parstate) (parse-init-declarator-list parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-cond (b* (((mv acl2::?erp ?decl ?span ?new-parstate) (parse-declaration parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-list-cond (b* (((mv acl2::?erp ?decls ?span ?new-parstate) (parse-declaration-list parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (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)
Theorem:
(defthm parsize-of-parse-asm-output-operand-cond (b* (((mv acl2::?erp ?output ?span ?new-parstate) (parse-asm-output-operand parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-asm-output-operands-cond (b* (((mv acl2::?erp ?outputs ?span ?new-parstate) (parse-asm-output-operands parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-?-asm-output-operands-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm parsize-of-parse-asm-input-operand-cond (b* (((mv acl2::?erp ?input ?span ?new-parstate) (parse-asm-input-operand parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-asm-input-operands-cond (b* (((mv acl2::?erp ?inputs ?span ?new-parstate) (parse-asm-input-operands parstate))) (implies (not erp) (<= (parsize new-parstate) (1- (parsize parstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-?-asm-input-operands-cond (b* nil t) :rule-classes nil)
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)
Theorem:
(defthm dirabsdeclor-decl?-nil-p-of-parse-array/function-abstract-declarator (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-parstate) (parse-array/function-abstract-declarator parstate))) (implies (not erp) (dirabsdeclor-decl?-nil-p dirabsdeclor))))