Parse expressions, declarations, and related entities.
In accordance with the mutual recursion in the C grammar, and with the mutual recursion exprs/decls in our abstract syntax, the functions to parse expressions, declarations, 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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-assignment-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-expression-rest expr span pstate))))
Function:
(defun parse-expression-rest (prev-expr prev-span pstate) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate)) ((when (not (equal token (token-punctuator ",")))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok (expr-fix prev-expr) (span-fix prev-span) pstate))) (psize (parsize pstate)) ((erp expr expr-span pstate) (parse-assignment-expression pstate)) ((unless (mbt (<= (parsize pstate) (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 pstate))))
Function:
(defun parse-assignment-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-assignment-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-conditional-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((when (not (expr-unary/postfix/primary-p expr))) (retok expr span pstate)) ((erp token & pstate) (read-token pstate)) ((when (not (token-assignment-operator-p token))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok expr span pstate))) (asgop (token-to-assignment-operator token)) ((erp expr2 span2 pstate) (parse-assignment-expression pstate))) (retok (make-expr-binary :op asgop :arg1 expr :arg2 expr2) (span-join span span2) pstate))))
Function:
(defun parse-conditional-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-conditional-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-logical-or-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp token & pstate) (read-token pstate)) ((when (not (equal token (token-punctuator "?")))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok expr span pstate))) (psize (parsize pstate)) ((erp expr2 & pstate) (parse-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp & pstate) (read-punctuator ":" pstate)) ((erp expr3 span3 pstate) (parse-conditional-expression pstate))) (retok (make-expr-cond :test expr :then expr2 :else expr3) (span-join span span3) pstate))))
Function:
(defun parse-logical-or-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-logical-or-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-logical-and-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-logical-or-expression-rest expr span pstate))))
Function:
(defun parse-logical-or-expression-rest (prev-expr prev-span pstate) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-logical-or-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate)) ((when (not (equal token (token-punctuator "||")))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok (expr-fix prev-expr) (span-fix prev-span) pstate))) (psize (parsize pstate)) ((erp expr expr-span pstate) (parse-logical-and-expression pstate)) ((unless (mbt (<= (parsize pstate) (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 pstate))))
Function:
(defun parse-logical-and-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-logical-and-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-inclusive-or-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-logical-and-expression-rest expr span pstate))))
Function:
(defun parse-logical-and-expression-rest (prev-expr prev-span pstate) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-logical-and-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate)) ((when (not (equal token (token-punctuator "&&")))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok (expr-fix prev-expr) (span-fix prev-span) pstate))) (psize (parsize pstate)) ((erp expr expr-span pstate) (parse-inclusive-or-expression pstate)) ((unless (mbt (<= (parsize pstate) (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 pstate))))
Function:
(defun parse-inclusive-or-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-inclusive-or-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-exclusive-or-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-inclusive-or-expression-rest expr span pstate))))
Function:
(defun parse-inclusive-or-expression-rest (prev-expr prev-span pstate) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-inclusive-or-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate)) ((when (not (equal token (token-punctuator "|")))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok (expr-fix prev-expr) (span-fix prev-span) pstate))) (psize (parsize pstate)) ((erp expr expr-span pstate) (parse-exclusive-or-expression pstate)) ((unless (mbt (<= (parsize pstate) (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 pstate))))
Function:
(defun parse-exclusive-or-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-exclusive-or-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-and-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-exclusive-or-expression-rest expr span pstate))))
Function:
(defun parse-exclusive-or-expression-rest (prev-expr prev-span pstate) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-exclusive-or-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate)) ((when (not (equal token (token-punctuator "^")))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok (expr-fix prev-expr) (span-fix prev-span) pstate))) (psize (parsize pstate)) ((erp expr expr-span pstate) (parse-and-expression pstate)) ((unless (mbt (<= (parsize pstate) (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 pstate))))
Function:
(defun parse-and-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-and-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-equality-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-and-expression-rest expr span pstate))))
Function:
(defun parse-and-expression-rest (prev-expr prev-span pstate) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-and-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate)) ((when (not (equal token (token-punctuator "&")))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok (expr-fix prev-expr) (span-fix prev-span) pstate))) (psize (parsize pstate)) ((erp expr expr-span pstate) (parse-equality-expression pstate)) ((unless (mbt (<= (parsize pstate) (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 pstate))))
Function:
(defun parse-equality-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-equality-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-relational-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-equality-expression-rest expr span pstate))))
Function:
(defun parse-equality-expression-rest (prev-expr prev-span pstate) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-equality-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate)) ((when (not (token-equality-operator-p token))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok (expr-fix prev-expr) (span-fix prev-span) pstate))) (psize (parsize pstate)) ((erp expr expr-span pstate) (parse-relational-expression pstate)) ((unless (mbt (<= (parsize pstate) (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 pstate))))
Function:
(defun parse-relational-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-relational-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-shift-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-relational-expression-rest expr span pstate))))
Function:
(defun parse-relational-expression-rest (prev-expr prev-span pstate) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-relational-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate)) ((when (not (token-relational-operator-p token))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok (expr-fix prev-expr) (span-fix prev-span) pstate))) (psize (parsize pstate)) ((erp expr expr-span pstate) (parse-shift-expression pstate)) ((unless (mbt (<= (parsize pstate) (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 pstate))))
Function:
(defun parse-shift-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-shift-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-additive-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-shift-expression-rest expr span pstate))))
Function:
(defun parse-shift-expression-rest (prev-expr prev-span pstate) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-shift-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate)) ((when (not (token-shift-operator-p token))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok (expr-fix prev-expr) (span-fix prev-span) pstate))) (psize (parsize pstate)) ((erp expr expr-span pstate) (parse-additive-expression pstate)) ((unless (mbt (<= (parsize pstate) (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 pstate))))
Function:
(defun parse-additive-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-additive-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-multiplicative-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-additive-expression-rest expr span pstate))))
Function:
(defun parse-additive-expression-rest (prev-expr prev-span pstate) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-additive-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate)) ((when (not (token-additive-operator-p token))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok (expr-fix prev-expr) (span-fix prev-span) pstate))) (psize (parsize pstate)) ((erp expr expr-span pstate) (parse-multiplicative-expression pstate)) ((unless (mbt (<= (parsize pstate) (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 pstate))))
Function:
(defun parse-multiplicative-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-multiplicative-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-cast-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-multiplicative-expression-rest expr span pstate))))
Function:
(defun parse-multiplicative-expression-rest (prev-expr prev-span pstate) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-multiplicative-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate)) ((when (not (token-multiplicative-operator-p token))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok (expr-fix prev-expr) (span-fix prev-span) pstate))) (psize (parsize pstate)) ((erp expr expr-span pstate) (parse-cast-expression pstate)) ((unless (mbt (<= (parsize pstate) (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 pstate))))
Function:
(defun parse-cast-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-cast-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((equal token (token-punctuator "(")) (b* ((pstate (record-checkpoint pstate)) (psize (parsize pstate)) ((erp expr/tyname & pstate) (parse-expression-or-type-name pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (amb?-expr/tyname-case expr/tyname :tyname (b* ((pstate (clear-checkpoint pstate)) ((erp & pstate) (read-punctuator ")" pstate)) ((erp token2 & pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator "{")) (b* ((pstate (unread-token pstate))) (parse-compound-literal expr/tyname.unwrap span pstate))) (t (b* ((pstate (if token2 (unread-token pstate) pstate)) ((erp expr last-span pstate) (parse-cast-expression pstate))) (retok (make-expr-cast :type expr/tyname.unwrap :arg expr) (span-join span last-span) pstate))))) :expr (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) (pstate (unread-token pstate))) (parse-postfix-expression pstate)) :ambig (b* (((erp & pstate) (read-punctuator ")" pstate)) ((erp incdecops pstate) (parse-*-increment/decrement pstate)) ((erp token2 & pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator "(")) (b* ((pstate (clear-checkpoint pstate)) (pstate (unread-token pstate)) ((erp expr last-span pstate) (parse-postfix-expression pstate))) (retok (make-expr-cast/call-ambig :type/fun expr/tyname.unwrap :inc/dec incdecops :arg/rest expr) (span-join span last-span) pstate))) ((equal token2 (token-punctuator "*")) (b* ((pstate (clear-checkpoint pstate)) ((erp expr last-span pstate) (parse-cast-expression pstate))) (retok (make-expr-cast/mul-ambig :type/arg1 expr/tyname.unwrap :inc/dec incdecops :arg/arg2 expr) (span-join span last-span) pstate))) ((or (equal token2 (token-punctuator "+")) (equal token2 (token-punctuator "-"))) (b* ((pstate (clear-checkpoint pstate)) ((erp expr last-span pstate) (parse-multiplicative-expression pstate))) (retok (make-expr-cast/add-or-cast/sub-ambig token2 expr/tyname.unwrap incdecops expr) (span-join span last-span) pstate))) ((equal token2 (token-punctuator "&")) (b* ((pstate (clear-checkpoint pstate)) ((erp expr last-span pstate) (parse-equality-expression pstate))) (retok (make-expr-cast/and-ambig :type/arg1 expr/tyname.unwrap :inc/dec incdecops :arg/arg2 expr) (span-join span last-span) pstate))) ((token-unary-expression-start-p token2) (b* ((pstate (clear-checkpoint pstate)) (pstate (unread-token pstate)) ((erp expr last-span pstate) (parse-unary-expression pstate)) (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) pstate))) (t (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) (pstate (unread-token pstate))) (parse-postfix-expression pstate)))))))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (parse-unary-expression pstate)))))))
Function:
(defun parse-unary-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-unary-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((token-primary-expression-start-p token) (b* ((pstate (unread-token pstate))) (parse-postfix-expression pstate))) ((token-preinc/predec-operator-p token) (b* (((erp expr last-span pstate) (parse-unary-expression pstate)) (unop (token-to-preinc/predec-operator token))) (retok (make-expr-unary :op unop :arg expr) (span-join span last-span) pstate))) ((token-unary-operator-p token) (b* (((erp expr last-span pstate) (parse-cast-expression pstate)) (unop (token-to-unary-operator token))) (retok (make-expr-unary :op unop :arg expr) (span-join span last-span) pstate))) ((equal token (token-keyword "sizeof")) (b* (((erp token2 & pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator "(")) (b* (((erp expr/tyname & pstate) (parse-expression-or-type-name pstate)) ((erp last-span pstate) (read-punctuator ")" pstate)) (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) pstate))) (t (b* ((pstate (if token2 (unread-token pstate) pstate)) ((erp expr last-span pstate) (parse-unary-expression pstate))) (retok (make-expr-unary :op (unop-sizeof) :arg expr) (span-join span last-span) pstate)))))) ((or (equal token (token-keyword "_Alignof")) (equal token (token-keyword "__alignof__"))) (b* (((erp & pstate) (read-punctuator "(" pstate)) ((erp tyname & pstate) (parse-type-name pstate)) ((erp last-span pstate) (read-punctuator ")" pstate))) (retok (make-expr-alignof :type tyname :uscores (equal token (token-keyword "__alignof__"))) (span-join span last-span) pstate))) (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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-postfix-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((equal token (token-punctuator "(")) (b* ((psize (parsize pstate)) ((erp expr/tyname & pstate) (parse-expression-or-type-name pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp close-paren-span pstate) (read-punctuator ")" pstate))) (amb?-expr/tyname-case expr/tyname :tyname (parse-compound-literal expr/tyname.unwrap (span-join span close-paren-span) pstate) :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 pstate)) :ambig (b* (((erp token2 & pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator "{")) (b* ((pstate (unread-token pstate)) (tyname (amb-expr/tyname->tyname expr/tyname.unwrap))) (parse-compound-literal tyname (span-join span close-paren-span) pstate))) (t (b* ((pstate (if token2 (unread-token pstate) pstate)) (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 pstate)))))))) (t (b* ((pstate (if token (unread-token pstate) pstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-primary-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-postfix-expression-rest expr span pstate)))))))
Function:
(defun parse-postfix-expression-rest (prev-expr prev-span pstate) (declare (xargs :guard (and (exprp prev-expr) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-postfix-expression-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((equal token (token-punctuator "[")) (b* ((psize (parsize pstate)) ((erp expr & pstate) (parse-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp last-span pstate) (read-punctuator "]" pstate)) (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 pstate))) ((equal token (token-punctuator "(")) (b* ((psize (parsize pstate)) ((erp exprs & pstate) (parse-argument-expressions pstate)) ((unless (mbt (<= (parsize pstate) psize))) (reterr :impossible)) ((erp last-span pstate) (read-punctuator ")" pstate)) (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 pstate))) ((equal token (token-punctuator ".")) (b* (((erp ident ident-span pstate) (read-identifier pstate)) (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 pstate))) ((equal token (token-punctuator "->")) (b* (((erp ident ident-span pstate) (read-identifier pstate)) (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 pstate))) ((equal token (token-punctuator "++")) (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 pstate))) ((equal token (token-punctuator "--")) (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 pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (expr-fix prev-expr) (span-fix prev-span) pstate)))))))
Function:
(defun parse-argument-expressions (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-argument-expressions)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate))) (cond ((token-expression-start-p token) (b* ((pstate (unread-token pstate)) (psize (parsize pstate)) ((erp expr span pstate) (parse-assignment-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) (curr-exprs (list expr)) (curr-span span)) (parse-argument-expressions-rest curr-exprs curr-span pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok nil (irr-span) pstate)))))))
Function:
(defun parse-argument-expressions-rest (prev-exprs prev-span pstate) (declare (xargs :guard (and (expr-listp prev-exprs) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-argument-expressions-rest)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate)) ((when (not (equal token (token-punctuator ",")))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok (expr-list-fix prev-exprs) (span-fix prev-span) pstate))) (psize (parsize pstate)) ((erp expr span pstate) (parse-assignment-expression pstate)) ((unless (mbt (<= (parsize pstate) (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 pstate))))
Function:
(defun parse-primary-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-primary-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((and token (token-case token :ident)) (retok (expr-ident (token-ident->unwrap token)) span pstate)) ((and token (token-case token :const)) (retok (expr-const (token-const->unwrap token)) span pstate)) ((and token (token-case token :string)) (retok (expr-string (token-string->unwrap token)) span pstate)) ((equal token (token-punctuator "(")) (b* (((erp expr & pstate) (parse-expression pstate)) ((erp last-span pstate) (read-punctuator ")" pstate))) (retok (expr-paren expr) (span-join span last-span) pstate))) ((equal token (token-keyword "_Generic")) (b* (((erp & pstate) (read-punctuator "(" pstate)) (psize (parsize pstate)) ((erp expr & pstate) (parse-assignment-expression pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp & pstate) (read-punctuator "," pstate)) (psize (parsize pstate)) ((erp genassoc genassoc-span pstate) (parse-generic-association pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp genassocs & pstate) (parse-generic-associations-rest (list genassoc) genassoc-span pstate)) ((erp last-span pstate) (read-punctuator ")" pstate))) (retok (make-expr-gensel :control expr :assoc genassocs) (span-join span last-span) pstate))) (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-generic-associations-rest (prev-genassocs prev-span pstate) (declare (xargs :guard (and (genassoc-listp prev-genassocs) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-generic-associations-rest)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate)) ((when (not (equal token (token-punctuator ",")))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok (genassoc-list-fix prev-genassocs) (span-fix prev-span) pstate))) (psize (parsize pstate)) ((erp genassoc span pstate) (parse-generic-association pstate)) ((unless (mbt (<= (parsize pstate) (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 pstate))))
Function:
(defun parse-generic-association (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-generic-association)) (declare (ignorable __function__)) (b* (((reterr) (irr-genassoc) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((token-type-name-start-p token) (b* ((pstate (unread-token pstate)) (psize (parsize pstate)) ((erp tyname & pstate) (parse-type-name pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp & pstate) (read-punctuator ":" pstate)) ((erp expr last-span pstate) (parse-assignment-expression pstate))) (retok (make-genassoc-type :type tyname :expr expr) (span-join span last-span) pstate))) ((equal token (token-keyword "default")) (b* (((erp & pstate) (read-punctuator ":" pstate)) ((erp expr last-span pstate) (parse-assignment-expression pstate))) (retok (genassoc-default expr) (span-join span last-span) pstate))) (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-compound-literal (tyname first-span pstate) (declare (xargs :guard (and (tynamep tyname) (spanp first-span) (parstatep pstate)))) (let ((__function__ 'parse-compound-literal)) (declare (ignorable __function__)) (b* (((reterr) (irr-expr) (irr-span) (irr-parstate)) ((erp & pstate) (read-punctuator "{" pstate)) ((erp desiniters final-comma & pstate) (parse-initializer-list pstate)) ((erp last-span pstate) (read-punctuator "}" pstate))) (retok (make-expr-complit :type tyname :elems desiniters :final-comma final-comma) (span-join first-span last-span) pstate))))
Function:
(defun parse-constant-expression (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-constant-expression)) (declare (ignorable __function__)) (b* (((reterr) (irr-const-expr) (irr-span) (irr-parstate)) ((erp expr span pstate) (parse-conditional-expression pstate))) (retok (const-expr expr) span pstate))))
Function:
(defun parse-static-assert-declaration (first-span pstate) (declare (xargs :guard (and (spanp first-span) (parstatep pstate)))) (let ((__function__ 'parse-static-assert-declaration)) (declare (ignorable __function__)) (b* (((reterr) (irr-statassert) (irr-span) (irr-parstate)) ((erp & pstate) (read-punctuator "(" pstate)) ((erp cexpr & pstate) (parse-constant-expression pstate)) ((erp & pstate) (read-punctuator "," pstate)) ((erp stringlit & pstate) (read-stringlit pstate)) ((erp & pstate) (read-punctuator ")" pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (make-statassert :test cexpr :message stringlit) (span-join first-span last-span) pstate))))
Function:
(defun parse-designator (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-designator)) (declare (ignorable __function__)) (b* (((reterr) (irr-designor) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((equal token (token-punctuator "[")) (b* (((erp cexpr & pstate) (parse-constant-expression pstate)) ((erp last-span pstate) (read-punctuator "]" pstate))) (retok (designor-sub cexpr) (span-join span last-span) pstate))) ((equal token (token-punctuator ".")) (b* (((erp ident last-span pstate) (read-identifier pstate))) (retok (designor-dot ident) (span-join span last-span) pstate))) (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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-designator-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp designor span pstate) (parse-designator pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp token & pstate) (read-token pstate)) ((when (not (token-designator-start-p token))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok (list designor) span pstate))) (pstate (unread-token pstate)) ((erp designors more-span pstate) (parse-designator-list pstate))) (retok (cons designor designors) (span-join span more-span) pstate))))
Function:
(defun parse-initializer (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-initializer)) (declare (ignorable __function__)) (b* (((reterr) (irr-initer) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((token-expression-start-p token) (b* ((pstate (unread-token pstate)) ((erp expr span pstate) (parse-assignment-expression pstate))) (retok (initer-single expr) span pstate))) ((equal token (token-punctuator "{")) (b* (((erp desiniters final-comma & pstate) (parse-initializer-list pstate)) ((erp last-span pstate) (read-punctuator "}" pstate))) (retok (make-initer-list :elems desiniters :final-comma final-comma) (span-join span last-span) pstate))) (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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-designation?-initializer)) (declare (ignorable __function__)) (b* (((reterr) (irr-desiniter) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((token-designation-start-p token) (b* ((pstate (unread-token pstate)) (psize (parsize pstate)) ((erp designors span pstate) (parse-designator-list pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp & pstate) (read-punctuator "=" pstate)) ((erp initer last-span pstate) (parse-initializer pstate))) (retok (make-desiniter :design designors :init initer) (span-join span last-span) pstate))) ((token-initializer-start-p token) (b* ((pstate (unread-token pstate)) ((erp initer span pstate) (parse-initializer pstate))) (retok (make-desiniter :design nil :init initer) span pstate))) (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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-initializer-list)) (declare (ignorable __function__)) (b* (((reterr) nil nil (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp desiniter span pstate) (parse-designation?-initializer pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp token & pstate) (read-token pstate))) (cond ((equal token (token-punctuator ",")) (b* (((erp token2 span2 pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator "}")) (b* ((pstate (unread-token pstate))) (retok (list desiniter) t (span-join span span2) pstate))) ((token-designation?-initializer-start-p token2) (b* ((pstate (unread-token pstate)) ((erp desiniters final-comma last-span pstate) (parse-initializer-list pstate))) (retok (cons desiniter desiniters) final-comma (span-join span last-span) pstate))) (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)))))) ((equal token (token-punctuator "}")) (b* ((pstate (unread-token pstate))) (retok (list desiniter) nil span pstate))) (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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-enumerator)) (declare (ignorable __function__)) (b* (((reterr) (irr-enumer) (irr-span) (irr-parstate)) ((erp ident span pstate) (read-identifier pstate)) ((erp token & pstate) (read-token pstate))) (cond ((equal token (token-punctuator "=")) (b* (((erp cexpr last-span pstate) (parse-constant-expression pstate))) (retok (make-enumer :name ident :value cexpr) (span-join span last-span) pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (make-enumer :name ident :value nil) span pstate)))))))
Function:
(defun parse-enumerator-list (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-enumerator-list)) (declare (ignorable __function__)) (b* (((reterr) nil nil (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp enumer enumer-span pstate) (parse-enumerator pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp token span pstate) (read-token pstate))) (cond ((equal token (token-punctuator ",")) (b* (((erp token2 span2 pstate) (read-token pstate))) (cond ((and token2 (token-case token2 :ident)) (b* ((pstate (unread-token pstate)) ((erp enumers final-comma enumers-span pstate) (parse-enumerator-list pstate))) (retok (cons enumer enumers) final-comma (span-join enumer-span enumers-span) pstate))) ((equal token2 (token-punctuator "}")) (b* ((pstate (unread-token pstate))) (retok (list enumer) t (span-join enumer-span span) pstate))) (t (reterr-msg :where (position-to-msg (span->start span2)) :expected "an identifier ~ or a closed curly brace" :found (token-to-msg token2)))))) ((equal token (token-punctuator "}")) (b* ((pstate (unread-token pstate))) (retok (list enumer) nil enumer-span pstate))) (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 pstate) (declare (xargs :guard (and (booleanp tyspec-seenp) (parstatep pstate)))) (let ((__function__ 'parse-specifier/qualifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-spec/qual) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((token-type-specifier-keyword-p token) (retok (spec/qual-tyspec (token-to-type-specifier-keyword token)) span pstate)) ((equal token (token-keyword "_Atomic")) (b* (((erp token2 & pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator "(")) (if tyspec-seenp (b* ((pstate (unread-token pstate))) (retok (spec/qual-tyqual (type-qual-atomic)) span pstate)) (b* (((erp tyname & pstate) (parse-type-name pstate)) ((erp last-span pstate) (read-punctuator ")" pstate))) (retok (spec/qual-tyspec (type-spec-atomic tyname)) (span-join span last-span) pstate)))) (t (b* ((pstate (if token2 (unread-token pstate) pstate))) (retok (spec/qual-tyqual (type-qual-atomic)) span pstate)))))) ((equal token (token-keyword "struct")) (b* (((erp strunispec last-span pstate) (parse-struct-or-union-specifier pstate))) (retok (spec/qual-tyspec (type-spec-struct strunispec)) (span-join span last-span) pstate))) ((equal token (token-keyword "union")) (b* (((erp strunispec last-span pstate) (parse-struct-or-union-specifier pstate))) (retok (spec/qual-tyspec (type-spec-union strunispec)) (span-join span last-span) pstate))) ((equal token (token-keyword "enum")) (b* (((erp enumspec last-span pstate) (parse-enum-specifier span pstate))) (retok (spec/qual-tyspec (type-spec-enum enumspec)) (span-join span last-span) pstate))) ((and token (token-case token :ident)) (retok (spec/qual-tyspec (type-spec-tydef (token-ident->unwrap token))) span pstate)) ((token-type-qualifier-p token) (retok (spec/qual-tyqual (token-to-type-qualifier token)) span pstate)) ((equal token (token-keyword "_Alignas")) (b* (((erp alignspec last-span pstate) (parse-alignment-specifier span pstate))) (retok (spec/qual-alignspec alignspec) (span-join span last-span) pstate))) (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 pstate) (declare (xargs :guard (and (booleanp tyspec-seenp) (parstatep pstate)))) (let ((__function__ 'parse-specifier-qualifier-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp specqual first-span pstate) (parse-specifier/qualifier tyspec-seenp pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) (tyspec-seenp (or tyspec-seenp (spec/qual-case specqual :tyspec))) ((erp token & pstate) (read-token pstate))) (cond ((and token (token-case token :ident)) (if tyspec-seenp (b* ((pstate (unread-token pstate))) (retok (list specqual) first-span pstate)) (b* ((pstate (unread-token pstate)) ((erp specquals last-span pstate) (parse-specifier-qualifier-list tyspec-seenp pstate))) (retok (cons specqual specquals) (span-join first-span last-span) pstate)))) ((token-specifier/qualifier-start-p token) (b* ((pstate (unread-token pstate)) ((erp specquals last-span pstate) (parse-specifier-qualifier-list tyspec-seenp pstate))) (retok (cons specqual specquals) (span-join first-span last-span) pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (list specqual) first-span pstate)))))))
Function:
(defun parse-declaration-specifier (tyspec-seenp pstate) (declare (xargs :guard (and (booleanp tyspec-seenp) (parstatep pstate)))) (let ((__function__ 'parse-declaration-specifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-declspec) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((token-storage-class-specifier-p token) (retok (declspec-stocla (token-to-storage-class-specifier token)) span pstate)) ((token-type-specifier-keyword-p token) (retok (declspec-tyspec (token-to-type-specifier-keyword token)) span pstate)) ((equal token (token-keyword "_Atomic")) (b* (((erp token2 & pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator "(")) (if tyspec-seenp (b* ((pstate (unread-token pstate))) (retok (declspec-tyqual (type-qual-atomic)) span pstate)) (b* (((erp tyname & pstate) (parse-type-name pstate)) ((erp last-span pstate) (read-punctuator ")" pstate))) (retok (declspec-tyspec (type-spec-atomic tyname)) (span-join span last-span) pstate)))) (t (b* ((pstate (if token2 (unread-token pstate) pstate))) (retok (declspec-tyqual (type-qual-atomic)) span pstate)))))) ((equal token (token-keyword "struct")) (b* (((erp strunispec last-span pstate) (parse-struct-or-union-specifier pstate))) (retok (declspec-tyspec (type-spec-struct strunispec)) (span-join span last-span) pstate))) ((equal token (token-keyword "union")) (b* (((erp strunispec last-span pstate) (parse-struct-or-union-specifier pstate))) (retok (declspec-tyspec (type-spec-union strunispec)) (span-join span last-span) pstate))) ((equal token (token-keyword "enum")) (b* (((erp enumspec last-span pstate) (parse-enum-specifier span pstate))) (retok (declspec-tyspec (type-spec-enum enumspec)) (span-join span last-span) pstate))) ((and token (token-case token :ident)) (retok (declspec-tyspec (type-spec-tydef (token-ident->unwrap token))) span pstate)) ((token-type-qualifier-p token) (retok (declspec-tyqual (token-to-type-qualifier token)) span pstate)) ((token-function-specifier-p token) (retok (declspec-funspec (token-to-function-specifier token)) span pstate)) ((equal token (token-keyword "_Alignas")) (b* (((erp alignspec last-span pstate) (parse-alignment-specifier span pstate))) (retok (declspec-alignspec alignspec) (span-join span last-span) pstate))) (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 pstate) (declare (xargs :guard (and (booleanp tyspec-seenp) (parstatep pstate)))) (let ((__function__ 'parse-declaration-specifiers)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp declspec first-span pstate) (parse-declaration-specifier tyspec-seenp pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) (tyspec-seenp (or tyspec-seenp (declspec-case declspec :tyspec))) ((erp token & pstate) (read-token pstate))) (cond ((and token (token-case token :ident)) (if tyspec-seenp (b* ((pstate (unread-token pstate))) (retok (list declspec) first-span pstate)) (b* ((pstate (unread-token pstate)) ((erp declspecs last-span pstate) (parse-declaration-specifiers tyspec-seenp pstate))) (retok (cons declspec declspecs) (span-join first-span last-span) pstate)))) ((token-declaration-specifier-start-p token) (b* ((pstate (unread-token pstate)) ((erp declspecs last-span pstate) (parse-declaration-specifiers tyspec-seenp pstate))) (retok (cons declspec declspecs) (span-join first-span last-span) pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (list declspec) first-span pstate)))))))
Function:
(defun parse-struct-or-union-specifier (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-struct-or-union-specifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-strunispec) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((and token (token-case token :ident)) (b* ((ident (token-ident->unwrap token)) ((erp token2 & pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator "{")) (b* (((erp structdecls & pstate) (parse-struct-declaration-list pstate)) ((erp last-span pstate) (read-punctuator "}" pstate))) (retok (make-strunispec :name ident :members structdecls) (span-join span last-span) pstate))) (t (b* ((pstate (if token2 (unread-token pstate) pstate))) (retok (make-strunispec :name ident :members nil) span pstate)))))) ((equal token (token-punctuator "{")) (b* (((erp structdecls & pstate) (parse-struct-declaration-list pstate)) ((erp last-span pstate) (read-punctuator "}" pstate))) (retok (make-strunispec :name nil :members structdecls) (span-join span last-span) pstate))) (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 pstate) (declare (xargs :guard (and (spanp first-span) (parstatep pstate)))) (let ((__function__ 'parse-enum-specifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-enumspec) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((and token (token-case token :ident)) (b* ((ident (token-ident->unwrap token)) ((erp token2 & pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator "{")) (b* (((erp enumers final-comma & pstate) (parse-enumerator-list pstate)) ((erp last-span pstate) (read-punctuator "}" pstate))) (retok (make-enumspec :name ident :list enumers :final-comma final-comma) (span-join first-span last-span) pstate))) (t (b* ((pstate (if token2 (unread-token pstate) pstate))) (retok (make-enumspec :name ident :list nil :final-comma nil) (span-join first-span span) pstate)))))) ((equal token (token-punctuator "{")) (b* (((erp enumers final-comma & pstate) (parse-enumerator-list pstate)) ((erp last-span pstate) (read-punctuator "}" pstate))) (retok (make-enumspec :name nil :list enumers :final-comma final-comma) (span-join first-span last-span) pstate))) (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 pstate) (declare (xargs :guard (and (spanp first-span) (parstatep pstate)))) (let ((__function__ 'parse-alignment-specifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-alignspec) (irr-span) (irr-parstate)) ((erp & pstate) (read-punctuator "(" pstate)) ((erp expr/tyname & pstate) (parse-expression-or-type-name pstate)) ((erp last-span pstate) (read-punctuator ")" pstate))) (amb?-expr/tyname-case expr/tyname :expr (retok (alignspec-alignas-expr (const-expr expr/tyname.unwrap)) (span-join first-span last-span) pstate) :tyname (retok (alignspec-alignas-type expr/tyname.unwrap) (span-join first-span last-span) pstate) :ambig (retok (alignspec-alignas-ambig expr/tyname.unwrap) (span-join first-span last-span) pstate)))))
Function:
(defun parse-array/function-abstract-declarator (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-array/function-abstract-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-dirabsdeclor) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((equal token (token-punctuator "[")) (b* (((erp token2 span2 pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator "]")) (retok (make-dirabsdeclor-array :decl? nil :tyquals nil :expr? nil) (span-join span span2) pstate)) ((equal token2 (token-punctuator "*")) (b* (((erp token3 span3 pstate) (read-token pstate))) (cond ((equal token3 (token-punctuator "]")) (retok (make-dirabsdeclor-array-star :decl? nil) (span-join span span3) pstate)) (t (b* ((pstate (if token3 (unread-token pstate) pstate)) (pstate (unread-token pstate)) ((erp expr & pstate) (parse-assignment-expression pstate)) ((erp last-span pstate) (read-punctuator "]" pstate))) (retok (make-dirabsdeclor-array :decl? nil :tyquals nil :expr? expr) (span-join span last-span) pstate)))))) ((equal token2 (token-keyword "static")) (b* (((erp token3 & pstate) (read-token pstate))) (cond ((token-type-qualifier-p token3) (b* ((pstate (unread-token pstate)) ((erp tyquals & pstate) (parse-type-qualifier-list pstate)) ((erp expr & pstate) (parse-assignment-expression pstate)) ((erp last-span pstate) (read-punctuator "]" pstate))) (retok (make-dirabsdeclor-array-static1 :decl? nil :tyquals tyquals :expr expr) (span-join span last-span) pstate))) (t (b* ((pstate (if token3 (unread-token pstate) pstate)) ((erp expr & pstate) (parse-assignment-expression pstate)) ((erp last-span pstate) (read-punctuator "]" pstate))) (retok (make-dirabsdeclor-array-static1 :decl? nil :tyquals nil :expr expr) (span-join span last-span) pstate)))))) ((token-type-qualifier-p token2) (b* ((pstate (unread-token pstate)) ((erp tyquals & pstate) (parse-type-qualifier-list pstate)) ((erp token3 span3 pstate) (read-token pstate))) (cond ((equal token3 (token-keyword "static")) (b* (((erp expr & pstate) (parse-assignment-expression pstate)) ((erp last-span pstate) (read-punctuator "]" pstate))) (retok (make-dirabsdeclor-array-static2 :decl? nil :tyquals tyquals :expr expr) (span-join span last-span) pstate))) ((equal token3 (token-punctuator "]")) (retok (make-dirabsdeclor-array :decl? nil :tyquals tyquals :expr? nil) (span-join span span3) pstate)) (t (b* ((pstate (if token3 (unread-token pstate) pstate)) ((erp expr & pstate) (parse-assignment-expression pstate)) ((erp last-span pstate) (read-punctuator "]" pstate))) (retok (make-dirabsdeclor-array :decl? nil :tyquals tyquals :expr? expr) (span-join span last-span) pstate)))))) (t (b* ((pstate (if token2 (unread-token pstate) pstate)) ((erp expr & pstate) (parse-assignment-expression pstate)) ((erp last-span pstate) (read-punctuator "]" pstate))) (retok (make-dirabsdeclor-array :decl? nil :tyquals nil :expr? expr) (span-join span last-span) pstate)))))) ((equal token (token-punctuator "(")) (b* (((erp token2 span2 pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator ")")) (retok (make-dirabsdeclor-function :decl? nil :params nil :ellipsis nil) (span-join span span2) pstate)) (t (b* ((pstate (if token2 (unread-token pstate) pstate)) ((erp paramdecls ellipsis & pstate) (parse-parameter-declaration-list pstate)) ((erp last-span pstate) (read-punctuator ")" pstate))) (retok (make-dirabsdeclor-function :decl? nil :params paramdecls :ellipsis ellipsis) (span-join span last-span) pstate)))))) (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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-direct-abstract-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-dirabsdeclor) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((equal token (token-punctuator "(")) (b* (((erp token2 & pstate) (read-token pstate))) (cond ((token-abstract-declarator-start-p token2) (b* ((pstate (unread-token pstate)) (psize (parsize pstate)) ((erp absdeclor & pstate) (parse-abstract-declarator pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp last-span pstate) (read-punctuator ")" pstate))) (parse-direct-abstract-declarator-rest (dirabsdeclor-paren absdeclor) (span-join span last-span) pstate))) (t (b* ((pstate (if token2 (unread-token pstate) pstate)) (pstate (unread-token pstate)) (psize (parsize pstate)) ((erp dirabsdeclor span pstate) (parse-array/function-abstract-declarator pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-direct-abstract-declarator-rest dirabsdeclor span pstate)))))) ((equal token (token-punctuator "[")) (b* ((pstate (unread-token pstate)) (psize (parsize pstate)) ((erp dirabsdeclor span pstate) (parse-array/function-abstract-declarator pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-direct-abstract-declarator-rest dirabsdeclor span pstate))) (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 pstate) (declare (xargs :guard (and (dirabsdeclorp prev-dirabsdeclor) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-direct-abstract-declarator-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-dirabsdeclor) (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate))) (cond ((or (equal token (token-punctuator "(")) (equal token (token-punctuator "["))) (b* ((pstate (unread-token pstate)) (psize (parsize pstate)) ((erp next-dirabsdeclor next-span pstate) (parse-array/function-abstract-declarator pstate)) ((unless (mbt (<= (parsize pstate) (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 pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (dirabsdeclor-fix prev-dirabsdeclor) (span-fix prev-span) pstate)))))))
Function:
(defun parse-abstract-declarator (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-abstract-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-absdeclor) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((equal token (token-punctuator "*")) (b* ((pstate (unread-token pstate)) (psize (parsize pstate)) ((erp tyqualss tyqualss-span pstate) (parse-pointer pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp token2 & pstate) (read-token pstate))) (cond ((token-direct-abstract-declarator-start-p token2) (b* ((pstate (unread-token pstate)) ((erp dirabsdeclor dirabsdeclor-span pstate) (parse-direct-abstract-declarator pstate))) (retok (make-absdeclor :pointers tyqualss :decl? dirabsdeclor) (span-join tyqualss-span dirabsdeclor-span) pstate))) (t (b* ((pstate (if token2 (unread-token pstate) pstate))) (retok (make-absdeclor :pointers tyqualss :decl? nil) tyqualss-span pstate)))))) ((token-direct-abstract-declarator-start-p token) (b* ((pstate (unread-token pstate)) ((erp dirabsdeclor span pstate) (parse-direct-abstract-declarator pstate))) (retok (make-absdeclor :pointers nil :decl? dirabsdeclor) span pstate))) (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 pstate) (declare (xargs :guard (and (dirdeclorp prev-dirdeclor) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-array/function-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-dirdeclor) (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate))) (cond ((equal token (token-punctuator "[")) (b* (((erp token2 span2 pstate) (read-token pstate))) (cond ((token-type-qualifier-p token2) (b* ((pstate (unread-token pstate)) ((erp tyquals & pstate) (parse-type-qualifier-list pstate)) ((erp token3 span3 pstate) (read-token pstate))) (cond ((equal token3 (token-punctuator "*")) (b* (((erp token4 span4 pstate) (read-token pstate))) (cond ((equal token4 (token-punctuator "]")) (retok (make-dirdeclor-array-star :decl prev-dirdeclor :tyquals tyquals) (span-join prev-span span4) pstate)) (t (b* ((pstate (if token4 (unread-token pstate) pstate)) (pstate (unread-token pstate)) ((erp expr & pstate) (parse-assignment-expression pstate)) ((erp last-span pstate) (read-punctuator "]" pstate))) (retok (make-dirdeclor-array :decl prev-dirdeclor :tyquals tyquals :expr? expr) (span-join prev-span last-span) pstate)))))) ((token-expression-start-p token3) (b* ((pstate (unread-token pstate)) ((erp expr & pstate) (parse-assignment-expression pstate)) ((erp last-span pstate) (read-punctuator "]" pstate))) (retok (make-dirdeclor-array :decl prev-dirdeclor :tyquals tyquals :expr? expr) (span-join prev-span last-span) pstate))) ((equal token3 (token-punctuator "]")) (retok (make-dirdeclor-array :decl prev-dirdeclor :tyquals tyquals :expr? nil) (span-join prev-span span3) pstate)) ((equal token3 (token-keyword "static")) (b* (((erp expr & pstate) (parse-assignment-expression pstate)) ((erp last-span pstate) (read-punctuator "]" pstate))) (retok (make-dirdeclor-array-static2 :decl prev-dirdeclor :tyquals tyquals :expr expr) (span-join prev-span last-span) pstate))) (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)))))) ((equal token2 (token-punctuator "*")) (b* (((erp token3 span3 pstate) (read-token pstate))) (cond ((equal token3 (token-punctuator "]")) (retok (make-dirdeclor-array-star :decl prev-dirdeclor :tyquals nil) (span-join prev-span span3) pstate)) (t (b* ((pstate (if token3 (unread-token pstate) pstate)) (pstate (unread-token pstate)) ((erp expr & pstate) (parse-assignment-expression pstate)) ((erp last-span pstate) (read-punctuator "]" pstate))) (retok (make-dirdeclor-array :decl prev-dirdeclor :tyquals nil :expr? expr) (span-join prev-span last-span) pstate)))))) ((token-expression-start-p token2) (b* ((pstate (unread-token pstate)) ((erp expr & pstate) (parse-assignment-expression pstate)) ((erp last-span pstate) (read-punctuator "]" pstate))) (retok (make-dirdeclor-array :decl prev-dirdeclor :tyquals nil :expr? expr) (span-join prev-span last-span) pstate))) ((equal token2 (token-keyword "static")) (b* (((erp token3 & pstate) (read-token pstate))) (cond ((token-type-qualifier-p token3) (b* ((pstate (unread-token pstate)) ((erp tyquals & pstate) (parse-type-qualifier-list pstate)) ((erp expr & pstate) (parse-assignment-expression pstate)) ((erp last-span pstate) (read-punctuator "]" pstate))) (retok (make-dirdeclor-array-static1 :decl prev-dirdeclor :tyquals tyquals :expr expr) (span-join prev-span last-span) pstate))) (t (b* ((pstate (unread-token pstate)) ((erp expr & pstate) (parse-assignment-expression pstate)) ((erp last-span pstate) (read-punctuator "]" pstate))) (retok (make-dirdeclor-array-static1 :decl prev-dirdeclor :tyquals nil :expr expr) (span-join prev-span last-span) pstate)))))) ((equal token2 (token-punctuator "]")) (retok (make-dirdeclor-array :decl prev-dirdeclor :tyquals nil :expr? nil) (span-join prev-span span2) pstate)) (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)))))) ((equal token (token-punctuator "(")) (b* (((erp token2 span2 pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator ")")) (retok (make-dirdeclor-function-params :decl prev-dirdeclor :params nil :ellipsis nil) (span-join prev-span span2) pstate)) (t (b* ((pstate (if token2 (unread-token pstate) pstate)) ((erp paramdecls ellipsis & pstate) (parse-parameter-declaration-list pstate)) ((erp last-span pstate) (read-punctuator ")" pstate))) (retok (make-dirdeclor-function-params :decl prev-dirdeclor :params paramdecls :ellipsis ellipsis) (span-join prev-span last-span) pstate)))))) (t (prog2$ (raise "Internal error: unexpected token ~x0." token) (reterr t)))))))
Function:
(defun parse-direct-declarator (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-direct-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-dirdeclor) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((and token (token-case token :ident)) (parse-direct-declarator-rest (dirdeclor-ident (token-ident->unwrap token)) span pstate)) ((equal token (token-punctuator "(")) (b* ((psize (parsize pstate)) ((erp declor & pstate) (parse-declarator pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp last-span pstate) (read-punctuator ")" pstate))) (parse-direct-declarator-rest (dirdeclor-paren declor) (span-join span last-span) pstate))) (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 pstate) (declare (xargs :guard (and (dirdeclorp prev-dirdeclor) (spanp prev-span) (parstatep pstate)))) (let ((__function__ 'parse-direct-declarator-rest)) (declare (ignorable __function__)) (b* (((reterr) (irr-dirdeclor) (irr-span) (irr-parstate)) ((erp token & pstate) (read-token pstate))) (cond ((or (equal token (token-punctuator "(")) (equal token (token-punctuator "["))) (b* ((pstate (unread-token pstate)) (psize (parsize pstate)) ((erp curr-dirdeclor curr-span pstate) (parse-array/function-declarator prev-dirdeclor prev-span pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible))) (parse-direct-declarator-rest curr-dirdeclor curr-span pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (dirdeclor-fix prev-dirdeclor) (span-fix prev-span) pstate)))))))
Function:
(defun parse-declarator (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-declor) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((equal token (token-punctuator "*")) (b* ((pstate (unread-token pstate)) ((erp tyqualss & pstate) (parse-pointer pstate)) ((erp dirdeclor last-span pstate) (parse-direct-declarator pstate))) (retok (make-declor :pointers tyqualss :decl dirdeclor) (span-join span last-span) pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate)) ((erp dirdeclor span pstate) (parse-direct-declarator pstate))) (retok (make-declor :pointers nil :decl dirdeclor) span pstate)))))))
Function:
(defun parse-struct-declarator (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-struct-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-structdeclor) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((token-declarator-start-p token) (b* ((pstate (unread-token pstate)) (psize (parsize pstate)) ((erp declor span pstate) (parse-declarator pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp token2 & pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator ":")) (b* (((erp cexpr last-span pstate) (parse-constant-expression pstate))) (retok (make-structdeclor :declor? declor :expr? cexpr) (span-join span last-span) pstate))) (t (b* ((pstate (if token2 (unread-token pstate) pstate))) (retok (make-structdeclor :declor? declor :expr? nil) span pstate)))))) ((equal token (token-punctuator ":")) (b* (((erp cexpr last-span pstate) (parse-constant-expression pstate))) (retok (make-structdeclor :declor? nil :expr? cexpr) (span-join span last-span) pstate))) (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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-struct-declarator-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp structdeclor span pstate) (parse-struct-declarator pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp token & pstate) (read-token pstate))) (cond ((equal token (token-punctuator ",")) (b* (((erp structdeclors last-span pstate) (parse-struct-declarator-list pstate))) (retok (cons structdeclor structdeclors) (span-join span last-span) pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (list structdeclor) span pstate)))))))
Function:
(defun parse-struct-declaration (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-struct-declaration)) (declare (ignorable __function__)) (b* (((reterr) (irr-structdecl) (irr-span) (irr-parstate)) ((erp token span pstate) (read-token pstate))) (cond ((equal token (token-keyword "_Static_assert")) (b* (((erp statassert span pstate) (parse-static-assert-declaration span pstate))) (retok (structdecl-statassert statassert) span pstate))) (t (b* (((mv extension pstate) (if (and (equal token (token-keyword "__extension__")) (parstate->gcc pstate)) (mv t pstate) (mv nil (if token (unread-token pstate) pstate)))) (psize (parsize pstate)) ((erp specquals span pstate) (parse-specifier-qualifier-list nil pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp token2 span2 pstate) (read-token pstate))) (cond ((token-struct-declarator-start-p token2) (b* ((pstate (unread-token pstate)) (psize (parsize pstate)) ((erp structdeclors & pstate) (parse-struct-declarator-list pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (make-structdecl-member :extension extension :specqual specquals :declor structdeclors :attrib attrspecs) (span-join span last-span) pstate))) ((equal token2 (token-keyword "__attribute__")) (b* ((pstate (unread-token pstate)) ((erp attrspecs & pstate) (parse-*-attribute-specifier pstate)) ((erp last-span pstate) (read-punctuator ";" pstate))) (retok (make-structdecl-member :extension extension :specqual specquals :declor nil :attrib attrspecs) (span-join span last-span) pstate))) ((equal token2 (token-punctuator ";")) (retok (make-structdecl-member :extension extension :specqual specquals :declor nil :attrib nil) (span-join span span2) pstate)) (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 (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-struct-declaration-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp structdecl span pstate) (parse-struct-declaration pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp token & pstate) (read-token pstate))) (cond ((token-struct-declaration-start-p token) (b* ((pstate (unread-token pstate)) ((erp structdecls last-span pstate) (parse-struct-declaration-list pstate))) (retok (cons structdecl structdecls) (span-join span last-span) pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (list structdecl) span pstate)))))))
Function:
(defun parse-parameter-declaration (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-parameter-declaration)) (declare (ignorable __function__)) (b* (((reterr) (irr-paramdecl) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp declspecs span pstate) (parse-declaration-specifiers nil pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp token & pstate) (read-token pstate))) (cond ((or (equal token (token-punctuator ")")) (equal token (token-punctuator ","))) (b* ((pstate (unread-token pstate))) (retok (make-paramdecl :spec declspecs :decl (paramdeclor-none)) span pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate)) ((erp declor/absdeclor last-span pstate) (parse-declarator-or-abstract-declarator pstate))) (amb?-declor/absdeclor-case declor/absdeclor :declor (retok (make-paramdecl :spec declspecs :decl (paramdeclor-declor declor/absdeclor.unwrap)) (span-join span last-span) pstate) :absdeclor (retok (make-paramdecl :spec declspecs :decl (paramdeclor-absdeclor declor/absdeclor.unwrap)) (span-join span last-span) pstate) :ambig (retok (make-paramdecl :spec declspecs :decl (paramdeclor-ambig declor/absdeclor.unwrap)) (span-join span last-span) pstate))))))))
Function:
(defun parse-parameter-declaration-list (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-parameter-declaration-list)) (declare (ignorable __function__)) (b* (((reterr) nil nil (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp paramdecl span pstate) (parse-parameter-declaration pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp token & pstate) (read-token pstate))) (cond ((equal token (token-punctuator ",")) (b* (((erp token2 span2 pstate) (read-token pstate))) (cond ((equal token2 (token-punctuator "...")) (retok (list paramdecl) t (span-join span span2) pstate)) (t (b* ((pstate (if token2 (unread-token pstate) pstate)) ((erp paramdecls ellipsis last-span pstate) (parse-parameter-declaration-list pstate))) (retok (cons paramdecl paramdecls) ellipsis (span-join span last-span) pstate)))))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (list paramdecl) nil span pstate)))))))
Function:
(defun parse-type-name (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-type-name)) (declare (ignorable __function__)) (b* (((reterr) (irr-tyname) (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp specquals span pstate) (parse-specifier-qualifier-list nil pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp token & pstate) (read-token pstate))) (cond ((token-abstract-declarator-start-p token) (b* ((pstate (unread-token pstate)) ((erp absdeclor last-span pstate) (parse-abstract-declarator pstate))) (retok (make-tyname :specqual specquals :decl? absdeclor) (span-join span last-span) pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (make-tyname :specqual specquals :decl? nil) span pstate)))))))
Function:
(defun parse-expression-or-type-name (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-expression-or-type-name)) (declare (ignorable __function__)) (b* (((reterr) (irr-amb?-expr/tyname) (irr-span) (irr-parstate)) (pstate (record-checkpoint pstate)) (psize (parsize pstate)) ((mv erp-expr expr span-expr pstate) (parse-expression pstate))) (if erp-expr (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) ((erp tyname span pstate) (parse-type-name pstate)) ((erp & pstate) (read-punctuator ")" pstate)) (pstate (unread-token pstate))) (retok (amb?-expr/tyname-tyname tyname) span pstate)) (b* (((erp token & pstate) (read-token pstate))) (if (equal token (token-punctuator ")")) (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) (pstate (record-checkpoint pstate)) ((mv erp tyname span-tyname pstate) (parse-type-name pstate))) (if erp (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) ((mv erp expr1 span-expr1 pstate) (parse-expression pstate)) ((when erp) (raise "Internal error: ~ parsing the same expression ~x0 twice ~ gives the error ~x1." expr erp) (reterr t)) ((unless (equal expr1 expr)) (raise "Internal error: ~ parsing the same expression ~x0 twice ~ gives a different expression ~x1." expr expr1) (reterr t)) ((unless (equal span-expr1 span-expr)) (raise "Internal error: ~ parsing the same expression ~x0 twice ~ gives a different span ~x1 from ~x2." expr span-expr1 span-expr) (reterr t))) (retok (amb?-expr/tyname-expr expr) span-expr pstate)) (b* (((erp token & pstate) (read-token pstate))) (if (equal token (token-punctuator ")")) (b* ((pstate (clear-checkpoint pstate)) ((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)) (pstate (unread-token pstate))) (retok (amb?-expr/tyname-ambig (make-amb-expr/tyname :expr expr :tyname tyname)) span-expr pstate)) (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) ((mv erp expr1 span-expr1 pstate) (parse-expression pstate)) ((when erp) (raise "Internal error: ~ parsing the same expression ~x0 twice ~ gives the error ~x1." expr erp) (reterr t)) ((unless (equal expr1 expr)) (raise "Internal error: ~ parsing the same expression ~x0 twice ~ gives a different expression ~x1." expr expr1) (reterr t)) ((unless (equal span-expr1 span-expr)) (raise "Internal error: ~ parsing the same expression ~x0 twice ~ gives a different span ~x1 from ~x2." expr span-expr1 span-expr) (reterr t))) (retok (amb?-expr/tyname-expr expr) span-expr pstate)))))) (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) ((erp tyname span pstate) (parse-type-name pstate)) ((erp & pstate) (read-punctuator ")" pstate)) (pstate (unread-token pstate))) (retok (amb?-expr/tyname-tyname tyname) span pstate))))))))
Function:
(defun parse-declarator-or-abstract-declarator (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-declarator-or-abstract-declarator)) (declare (ignorable __function__)) (b* (((reterr) (irr-amb?-declor/absdeclor) (irr-span) (irr-parstate)) (pstate (record-checkpoint pstate)) (psize (parsize pstate)) ((mv erp-declor declor span-declor pstate) (parse-declarator pstate))) (if erp-declor (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) ((erp absdeclor span pstate) (parse-abstract-declarator pstate))) (retok (amb?-declor/absdeclor-absdeclor absdeclor) span pstate)) (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) (pstate (record-checkpoint pstate)) ((mv erp absdeclor span-absdeclor pstate) (parse-abstract-declarator pstate))) (if erp (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) ((mv erp declor1 span-declor1 pstate) (parse-declarator pstate)) ((when erp) (raise "Internal error: ~ parsing the same declarator ~x0 twice ~ gives the error ~x1." declor erp) (reterr t)) ((unless (equal declor1 declor)) (raise "Internal error: ~ parsing the same declarator ~x0 twice ~ gives a different declarator ~x1." declor declor1) (reterr t)) ((unless (equal span-declor1 span-declor)) (raise "Internal error: ~ parsing the same declarator ~x0 twice ~ gives a different span ~x1 from ~x2." declor span-declor1 span-declor) (reterr t))) (retok (amb?-declor/absdeclor-declor declor) span-declor pstate)) (b* (((erp token & pstate) (read-token pstate))) (if (or (equal token (token-punctuator ",")) (equal token (token-punctuator ")"))) (b* ((pstate (clear-checkpoint pstate)) ((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)) (pstate (unread-token pstate))) (retok (amb?-declor/absdeclor-ambig (make-amb-declor/absdeclor :declor declor :absdeclor absdeclor)) span-declor pstate)) (b* ((pstate (backtrack-checkpoint pstate)) ((unless (<= (parsize pstate) psize)) (raise "Internal error: ~ size ~x0 after backtracking exceeds ~ size ~x1 before backtracking." (parsize pstate) psize) (b* ((pstate (init-parstate nil nil))) (reterr t))) ((mv erp declor1 span-declor1 pstate) (parse-declarator pstate)) ((when erp) (raise "Internal error: ~ parsing the same declarator ~x0 twice ~ gives the error ~x1." declor erp) (reterr t)) ((unless (equal declor1 declor)) (raise "Internal error: ~ parsing the same declarator ~x0 twice ~ gives a different declarator ~x1." declor declor1) (reterr t)) ((unless (equal span-declor1 span-declor)) (raise "Internal error: ~ parsing the same declarator ~x0 twice ~ gives a different span ~x1 from ~x2." declor span-declor1 span-declor) (reterr t))) (retok (amb?-declor/absdeclor-declor declor) span-declor pstate))))))))))
Function:
(defun parse-attribute-parameters (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-attribute-parameters)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) ((erp open-span pstate) (read-punctuator "(" pstate)) ((erp exprs & pstate) (parse-argument-expressions pstate)) ((erp close-span pstate) (read-punctuator ")" pstate))) (retok exprs (span-join open-span close-span) pstate))))
Function:
(defun parse-attribute (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-attribute)) (declare (ignorable __function__)) (b* (((reterr) (irr-attrib) (irr-span) (irr-parstate)) ((erp ident ident-span pstate) (read-identifier pstate)) ((erp token & pstate) (read-token pstate))) (cond ((equal token (token-punctuator "(")) (b* ((pstate (unread-token pstate)) ((erp exprs span pstate) (parse-attribute-parameters pstate))) (retok (make-attrib-name-param :name ident :param exprs) (span-join ident-span span) pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (attrib-name ident) ident-span pstate)))))))
Function:
(defun parse-attribute-list (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-attribute-list)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) (psize (parsize pstate)) ((erp attr span pstate) (parse-attribute pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp token & pstate) (read-token pstate))) (cond ((equal token (token-punctuator ",")) (b* (((erp attrs last-span pstate) (parse-attribute-list pstate))) (retok (cons attr attrs) (span-join span last-span) pstate))) (t (b* ((pstate (if token (unread-token pstate) pstate))) (retok (list attr) span pstate)))))))
Function:
(defun parse-attribute-specifier (first-span pstate) (declare (xargs :guard (and (spanp first-span) (parstatep pstate)))) (let ((__function__ 'parse-attribute-specifier)) (declare (ignorable __function__)) (b* (((reterr) (irr-attrib-spec) (irr-span) (irr-parstate)) ((erp & pstate) (read-punctuator "(" pstate)) ((erp & pstate) (read-punctuator "(" pstate)) ((erp attrs & pstate) (parse-attribute-list pstate)) ((erp & pstate) (read-punctuator ")" pstate)) ((erp last-span pstate) (read-punctuator ")" pstate))) (retok (attrib-spec attrs) (span-join first-span last-span) pstate))))
Function:
(defun parse-*-attribute-specifier (pstate) (declare (xargs :guard (parstatep pstate))) (let ((__function__ 'parse-*-attribute-specifier)) (declare (ignorable __function__)) (b* (((reterr) nil (irr-span) (irr-parstate)) ((erp token first-span pstate) (read-token pstate)) ((unless (equal token (token-keyword "__attribute__"))) (b* ((pstate (if token (unread-token pstate) pstate))) (retok nil (irr-span) pstate))) (psize (parsize pstate)) ((erp attrspec span pstate) (parse-attribute-specifier first-span pstate)) ((unless (mbt (<= (parsize pstate) (1- psize)))) (reterr :impossible)) ((erp attrspecs last-span pstate) (parse-*-attribute-specifier pstate))) (retok (cons attrspec attrspecs) (if attrspecs (span-join span last-span) span) pstate))))
Theorem:
(defthm return-type-of-parse-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-expression-rest prev-expr prev-span pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-expression-rest prev-expr prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression-rest.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-expression-rest prev-expr prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-assignment-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-assignment-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-assignment-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-assignment-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-assignment-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-assignment-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-conditional-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-conditional-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-conditional-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-conditional-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-conditional-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-conditional-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-or-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-or-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-or-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-or-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-or-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-or-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-or-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-or-expression-rest prev-expr prev-span pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-or-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-or-expression-rest prev-expr prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-or-expression-rest.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-or-expression-rest prev-expr prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-and-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-and-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-and-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-and-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-and-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-and-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-and-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-and-expression-rest prev-expr prev-span pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-and-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-and-expression-rest prev-expr prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-logical-and-expression-rest.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-and-expression-rest prev-expr prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-inclusive-or-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-inclusive-or-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-inclusive-or-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-inclusive-or-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-inclusive-or-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-inclusive-or-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-inclusive-or-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-inclusive-or-expression-rest prev-expr prev-span pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-inclusive-or-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-inclusive-or-expression-rest prev-expr prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-inclusive-or-expression-rest.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-inclusive-or-expression-rest prev-expr prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-exclusive-or-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-exclusive-or-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-exclusive-or-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-exclusive-or-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-exclusive-or-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-exclusive-or-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-exclusive-or-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-exclusive-or-expression-rest prev-expr prev-span pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-exclusive-or-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-exclusive-or-expression-rest prev-expr prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-exclusive-or-expression-rest.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-exclusive-or-expression-rest prev-expr prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-and-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-and-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-and-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-and-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-and-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-and-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-and-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-and-expression-rest prev-expr prev-span pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-and-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-and-expression-rest prev-expr prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-and-expression-rest.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-and-expression-rest prev-expr prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-equality-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-equality-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-equality-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-equality-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-equality-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-equality-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-equality-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-equality-expression-rest prev-expr prev-span pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-equality-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-equality-expression-rest prev-expr prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-equality-expression-rest.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-equality-expression-rest prev-expr prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-relational-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-relational-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-relational-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-relational-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-relational-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-relational-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-relational-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-relational-expression-rest prev-expr prev-span pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-relational-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-relational-expression-rest prev-expr prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-relational-expression-rest.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-relational-expression-rest prev-expr prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-shift-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-shift-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-shift-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-shift-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-shift-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-shift-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-shift-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-shift-expression-rest prev-expr prev-span pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-shift-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-shift-expression-rest prev-expr prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-shift-expression-rest.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-shift-expression-rest prev-expr prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-additive-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-additive-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-additive-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-additive-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-additive-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-additive-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-additive-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-additive-expression-rest prev-expr prev-span pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-additive-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-additive-expression-rest prev-expr prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-additive-expression-rest.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-additive-expression-rest prev-expr prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-multiplicative-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-multiplicative-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-multiplicative-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-multiplicative-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-multiplicative-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-multiplicative-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-multiplicative-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-multiplicative-expression-rest prev-expr prev-span pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-multiplicative-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-multiplicative-expression-rest prev-expr prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-multiplicative-expression-rest.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-multiplicative-expression-rest prev-expr prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-cast-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-cast-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-cast-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-cast-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-cast-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-cast-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-unary-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-unary-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-unary-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-unary-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-unary-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-unary-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-postfix-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-postfix-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-postfix-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-postfix-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-postfix-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-postfix-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-postfix-expression-rest.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-postfix-expression-rest prev-expr prev-span pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-postfix-expression-rest.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-postfix-expression-rest prev-expr prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-postfix-expression-rest.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-postfix-expression-rest prev-expr prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-argument-expressions.exprs (b* (((mv acl2::?erp ?exprs ?span ?new-pstate) (parse-argument-expressions pstate))) (expr-listp exprs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-argument-expressions.span (b* (((mv acl2::?erp ?exprs ?span ?new-pstate) (parse-argument-expressions pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-argument-expressions.new-pstate (b* (((mv acl2::?erp ?exprs ?span ?new-pstate) (parse-argument-expressions pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-argument-expressions-rest.exprs (b* (((mv acl2::?erp ?exprs ?span ?new-pstate) (parse-argument-expressions-rest prev-exprs prev-span pstate))) (expr-listp exprs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-argument-expressions-rest.span (b* (((mv acl2::?erp ?exprs ?span ?new-pstate) (parse-argument-expressions-rest prev-exprs prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-argument-expressions-rest.new-pstate (b* (((mv acl2::?erp ?exprs ?span ?new-pstate) (parse-argument-expressions-rest prev-exprs prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-primary-expression.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-primary-expression pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-primary-expression.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-primary-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-primary-expression.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-primary-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-generic-associations-rest.genassocs (b* (((mv acl2::?erp ?genassocs ?span ?new-pstate) (parse-generic-associations-rest prev-genassocs prev-span pstate))) (genassoc-listp genassocs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-generic-associations-rest.span (b* (((mv acl2::?erp ?genassocs ?span ?new-pstate) (parse-generic-associations-rest prev-genassocs prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-generic-associations-rest.new-pstate (b* (((mv acl2::?erp ?genassocs ?span ?new-pstate) (parse-generic-associations-rest prev-genassocs prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-generic-association.genassoc (b* (((mv acl2::?erp ?genassoc ?span ?new-pstate) (parse-generic-association pstate))) (genassocp genassoc)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-generic-association.span (b* (((mv acl2::?erp ?genassoc ?span ?new-pstate) (parse-generic-association pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-generic-association.new-pstate (b* (((mv acl2::?erp ?genassoc ?span ?new-pstate) (parse-generic-association pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-compound-literal.expr (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-compound-literal tyname first-span pstate))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-compound-literal.span (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-compound-literal tyname first-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-compound-literal.new-pstate (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-compound-literal tyname first-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-constant-expression.cexpr (b* (((mv acl2::?erp ?cexpr ?span ?new-pstate) (parse-constant-expression pstate))) (const-exprp cexpr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-constant-expression.span (b* (((mv acl2::?erp ?cexpr ?span ?new-pstate) (parse-constant-expression pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-constant-expression.new-pstate (b* (((mv acl2::?erp ?cexpr ?span ?new-pstate) (parse-constant-expression pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-static-assert-declaration.statassert (b* (((mv acl2::?erp ?statassert ?span ?new-pstate) (parse-static-assert-declaration first-span pstate))) (statassertp statassert)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-static-assert-declaration.span (b* (((mv acl2::?erp ?statassert ?span ?new-pstate) (parse-static-assert-declaration first-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-static-assert-declaration.new-pstate (b* (((mv acl2::?erp ?statassert ?span ?new-pstate) (parse-static-assert-declaration first-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designator.designor (b* (((mv acl2::?erp ?designor ?span ?new-pstate) (parse-designator pstate))) (designorp designor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designator.span (b* (((mv acl2::?erp ?designor ?span ?new-pstate) (parse-designator pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designator.new-pstate (b* (((mv acl2::?erp ?designor ?span ?new-pstate) (parse-designator pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designator-list.designors (b* (((mv acl2::?erp ?designors ?span ?new-pstate) (parse-designator-list pstate))) (designor-listp designors)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designator-list.span (b* (((mv acl2::?erp ?designors ?span ?new-pstate) (parse-designator-list pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designator-list.new-pstate (b* (((mv acl2::?erp ?designors ?span ?new-pstate) (parse-designator-list pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-initializer.initer (b* (((mv acl2::?erp ?initer ?span ?new-pstate) (parse-initializer pstate))) (initerp initer)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-initializer.span (b* (((mv acl2::?erp ?initer ?span ?new-pstate) (parse-initializer pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-initializer.new-pstate (b* (((mv acl2::?erp ?initer ?span ?new-pstate) (parse-initializer pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designation?-initializer.desiniter (b* (((mv acl2::?erp ?desiniter ?span ?new-pstate) (parse-designation?-initializer pstate))) (desiniterp desiniter)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designation?-initializer.span (b* (((mv acl2::?erp ?desiniter ?span ?new-pstate) (parse-designation?-initializer pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-designation?-initializer.new-pstate (b* (((mv acl2::?erp ?desiniter ?span ?new-pstate) (parse-designation?-initializer pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-initializer-list.desiniters (b* (((mv acl2::?erp ?desiniters ?final-comma ?span ?new-pstate) (parse-initializer-list pstate))) (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-pstate) (parse-initializer-list pstate))) (booleanp final-comma)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-initializer-list.span (b* (((mv acl2::?erp ?desiniters ?final-comma ?span ?new-pstate) (parse-initializer-list pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-initializer-list.new-pstate (b* (((mv acl2::?erp ?desiniters ?final-comma ?span ?new-pstate) (parse-initializer-list pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enumerator.enumer (b* (((mv acl2::?erp ?enumer ?span ?new-pstate) (parse-enumerator pstate))) (enumerp enumer)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enumerator.span (b* (((mv acl2::?erp ?enumer ?span ?new-pstate) (parse-enumerator pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enumerator.new-pstate (b* (((mv acl2::?erp ?enumer ?span ?new-pstate) (parse-enumerator pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enumerator-list.enumers (b* (((mv acl2::?erp ?enumers ?final-comma ?span ?new-pstate) (parse-enumerator-list pstate))) (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-pstate) (parse-enumerator-list pstate))) (booleanp final-comma)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enumerator-list.span (b* (((mv acl2::?erp ?enumers ?final-comma ?span ?new-pstate) (parse-enumerator-list pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enumerator-list.new-pstate (b* (((mv acl2::?erp ?enumers ?final-comma ?span ?new-pstate) (parse-enumerator-list pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-specifier/qualifier.specqual (b* (((mv acl2::?erp ?specqual ?span ?new-pstate) (parse-specifier/qualifier tyspec-seenp pstate))) (spec/qual-p specqual)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-specifier/qualifier.span (b* (((mv acl2::?erp ?specqual ?span ?new-pstate) (parse-specifier/qualifier tyspec-seenp pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-specifier/qualifier.new-pstate (b* (((mv acl2::?erp ?specqual ?span ?new-pstate) (parse-specifier/qualifier tyspec-seenp pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-specifier-qualifier-list.specquals (b* (((mv acl2::?erp ?specquals ?span ?new-pstate) (parse-specifier-qualifier-list tyspec-seenp pstate))) (spec/qual-listp specquals)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-specifier-qualifier-list.span (b* (((mv acl2::?erp ?specquals ?span ?new-pstate) (parse-specifier-qualifier-list tyspec-seenp pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-specifier-qualifier-list.new-pstate (b* (((mv acl2::?erp ?specquals ?span ?new-pstate) (parse-specifier-qualifier-list tyspec-seenp pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-specifier.declspec (b* (((mv acl2::?erp ?declspec ?span ?new-pstate) (parse-declaration-specifier tyspec-seenp pstate))) (declspecp declspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-specifier.span (b* (((mv acl2::?erp ?declspec ?span ?new-pstate) (parse-declaration-specifier tyspec-seenp pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-specifier.new-pstate (b* (((mv acl2::?erp ?declspec ?span ?new-pstate) (parse-declaration-specifier tyspec-seenp pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-specifiers.declspecs (b* (((mv acl2::?erp ?declspecs ?span ?new-pstate) (parse-declaration-specifiers tyspec-seenp pstate))) (declspec-listp declspecs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-specifiers.span (b* (((mv acl2::?erp ?declspecs ?span ?new-pstate) (parse-declaration-specifiers tyspec-seenp pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declaration-specifiers.new-pstate (b* (((mv acl2::?erp ?declspecs ?span ?new-pstate) (parse-declaration-specifiers tyspec-seenp pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-or-union-specifier.strunispec (b* (((mv acl2::?erp ?strunispec ?span ?new-pstate) (parse-struct-or-union-specifier pstate))) (strunispecp strunispec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-or-union-specifier.span (b* (((mv acl2::?erp ?strunispec ?span ?new-pstate) (parse-struct-or-union-specifier pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-or-union-specifier.new-pstate (b* (((mv acl2::?erp ?strunispec ?span ?new-pstate) (parse-struct-or-union-specifier pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enum-specifier.enumspec (b* (((mv acl2::?erp ?enumspec ?span ?new-pstate) (parse-enum-specifier first-span pstate))) (enumspecp enumspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enum-specifier.span (b* (((mv acl2::?erp ?enumspec ?span ?new-pstate) (parse-enum-specifier first-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-enum-specifier.new-pstate (b* (((mv acl2::?erp ?enumspec ?span ?new-pstate) (parse-enum-specifier first-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-alignment-specifier.alignspec (b* (((mv acl2::?erp ?alignspec ?span ?new-pstate) (parse-alignment-specifier first-span pstate))) (alignspecp alignspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-alignment-specifier.span (b* (((mv acl2::?erp ?alignspec ?span ?new-pstate) (parse-alignment-specifier first-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-alignment-specifier.new-pstate (b* (((mv acl2::?erp ?alignspec ?span ?new-pstate) (parse-alignment-specifier first-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-array/function-abstract-declarator.dirabsdeclor (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-array/function-abstract-declarator pstate))) (dirabsdeclorp dirabsdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-array/function-abstract-declarator.span (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-array/function-abstract-declarator pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-array/function-abstract-declarator.new-pstate (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-array/function-abstract-declarator pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-abstract-declarator.dirabsdeclor (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-direct-abstract-declarator pstate))) (dirabsdeclorp dirabsdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-abstract-declarator.span (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-direct-abstract-declarator pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-abstract-declarator.new-pstate (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-direct-abstract-declarator pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-abstract-declarator-rest.dirabsdeclor (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-direct-abstract-declarator-rest prev-dirabsdeclor prev-span pstate))) (dirabsdeclorp dirabsdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-abstract-declarator-rest.span (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-direct-abstract-declarator-rest prev-dirabsdeclor prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-abstract-declarator-rest.new-pstate (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-direct-abstract-declarator-rest prev-dirabsdeclor prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-abstract-declarator.absdeclor (b* (((mv acl2::?erp ?absdeclor ?span ?new-pstate) (parse-abstract-declarator pstate))) (absdeclorp absdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-abstract-declarator.span (b* (((mv acl2::?erp ?absdeclor ?span ?new-pstate) (parse-abstract-declarator pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-abstract-declarator.new-pstate (b* (((mv acl2::?erp ?absdeclor ?span ?new-pstate) (parse-abstract-declarator pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-array/function-declarator.dirdeclor (b* (((mv acl2::?erp ?dirdeclor ?span ?new-pstate) (parse-array/function-declarator prev-dirdeclor prev-span pstate))) (dirdeclorp dirdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-array/function-declarator.span (b* (((mv acl2::?erp ?dirdeclor ?span ?new-pstate) (parse-array/function-declarator prev-dirdeclor prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-array/function-declarator.new-pstate (b* (((mv acl2::?erp ?dirdeclor ?span ?new-pstate) (parse-array/function-declarator prev-dirdeclor prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-declarator.dirdeclor (b* (((mv acl2::?erp ?dirdeclor ?span ?new-pstate) (parse-direct-declarator pstate))) (dirdeclorp dirdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-declarator.span (b* (((mv acl2::?erp ?dirdeclor ?span ?new-pstate) (parse-direct-declarator pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-declarator.new-pstate (b* (((mv acl2::?erp ?dirdeclor ?span ?new-pstate) (parse-direct-declarator pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-declarator-rest.dirdeclor (b* (((mv acl2::?erp ?dirdeclor ?span ?new-pstate) (parse-direct-declarator-rest prev-dirdeclor prev-span pstate))) (dirdeclorp dirdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-declarator-rest.span (b* (((mv acl2::?erp ?dirdeclor ?span ?new-pstate) (parse-direct-declarator-rest prev-dirdeclor prev-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-direct-declarator-rest.new-pstate (b* (((mv acl2::?erp ?dirdeclor ?span ?new-pstate) (parse-direct-declarator-rest prev-dirdeclor prev-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declarator.declor (b* (((mv acl2::?erp ?declor ?span ?new-pstate) (parse-declarator pstate))) (declorp declor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declarator.span (b* (((mv acl2::?erp ?declor ?span ?new-pstate) (parse-declarator pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declarator.new-pstate (b* (((mv acl2::?erp ?declor ?span ?new-pstate) (parse-declarator pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declarator.structdeclor (b* (((mv acl2::?erp ?structdeclor ?span ?new-pstate) (parse-struct-declarator pstate))) (structdeclorp structdeclor)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declarator.span (b* (((mv acl2::?erp ?structdeclor ?span ?new-pstate) (parse-struct-declarator pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declarator.new-pstate (b* (((mv acl2::?erp ?structdeclor ?span ?new-pstate) (parse-struct-declarator pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declarator-list.structdeclors (b* (((mv acl2::?erp ?structdeclors ?span ?new-pstate) (parse-struct-declarator-list pstate))) (structdeclor-listp structdeclors)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declarator-list.span (b* (((mv acl2::?erp ?structdeclors ?span ?new-pstate) (parse-struct-declarator-list pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declarator-list.new-pstate (b* (((mv acl2::?erp ?structdeclors ?span ?new-pstate) (parse-struct-declarator-list pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declaration.structdecl (b* (((mv acl2::?erp ?structdecl ?span ?new-pstate) (parse-struct-declaration pstate))) (structdeclp structdecl)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declaration.span (b* (((mv acl2::?erp ?structdecl ?span ?new-pstate) (parse-struct-declaration pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declaration.new-pstate (b* (((mv acl2::?erp ?structdecl ?span ?new-pstate) (parse-struct-declaration pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declaration-list.structdecls (b* (((mv acl2::?erp ?structdecls ?span ?new-pstate) (parse-struct-declaration-list pstate))) (structdecl-listp structdecls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declaration-list.span (b* (((mv acl2::?erp ?structdecls ?span ?new-pstate) (parse-struct-declaration-list pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-struct-declaration-list.new-pstate (b* (((mv acl2::?erp ?structdecls ?span ?new-pstate) (parse-struct-declaration-list pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-parameter-declaration.paramdecl (b* (((mv acl2::?erp ?paramdecl ?span ?new-pstate) (parse-parameter-declaration pstate))) (paramdeclp paramdecl)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-parameter-declaration.span (b* (((mv acl2::?erp ?paramdecl ?span ?new-pstate) (parse-parameter-declaration pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-parameter-declaration.new-pstate (b* (((mv acl2::?erp ?paramdecl ?span ?new-pstate) (parse-parameter-declaration pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-parameter-declaration-list.paramdecls (b* (((mv acl2::?erp ?paramdecls ?ellipsis ?span ?new-pstate) (parse-parameter-declaration-list pstate))) (paramdecl-listp paramdecls)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-parameter-declaration-list.ellipsis (b* (((mv acl2::?erp ?paramdecls ?ellipsis ?span ?new-pstate) (parse-parameter-declaration-list pstate))) (booleanp ellipsis)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-parameter-declaration-list.span (b* (((mv acl2::?erp ?paramdecls ?ellipsis ?span ?new-pstate) (parse-parameter-declaration-list pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-parameter-declaration-list.new-pstate (b* (((mv acl2::?erp ?paramdecls ?ellipsis ?span ?new-pstate) (parse-parameter-declaration-list pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-type-name.tyname (b* (((mv acl2::?erp ?tyname ?span ?new-pstate) (parse-type-name pstate))) (tynamep tyname)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-type-name.span (b* (((mv acl2::?erp ?tyname ?span ?new-pstate) (parse-type-name pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-type-name.new-pstate (b* (((mv acl2::?erp ?tyname ?span ?new-pstate) (parse-type-name pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression-or-type-name.expr/tyname (b* (((mv acl2::?erp ?expr/tyname ?span ?new-pstate) (parse-expression-or-type-name pstate))) (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-pstate) (parse-expression-or-type-name pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-expression-or-type-name.new-pstate (b* (((mv acl2::?erp ?expr/tyname ?span ?new-pstate) (parse-expression-or-type-name pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declarator-or-abstract-declarator.declor/absdeclor (b* (((mv acl2::?erp ?declor/absdeclor ?span ?new-pstate) (parse-declarator-or-abstract-declarator pstate))) (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-pstate) (parse-declarator-or-abstract-declarator pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-declarator-or-abstract-declarator.new-pstate (b* (((mv acl2::?erp ?declor/absdeclor ?span ?new-pstate) (parse-declarator-or-abstract-declarator pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-parameters.attrparams (b* (((mv acl2::?erp ?attrparams ?span ?new-pstate) (parse-attribute-parameters pstate))) (expr-listp attrparams)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-parameters.span (b* (((mv acl2::?erp ?attrparams ?span ?new-pstate) (parse-attribute-parameters pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-parameters.new-pstate (b* (((mv acl2::?erp ?attrparams ?span ?new-pstate) (parse-attribute-parameters pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute.attr (b* (((mv acl2::?erp ?attr ?span ?new-pstate) (parse-attribute pstate))) (attribp attr)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute.span (b* (((mv acl2::?erp ?attr ?span ?new-pstate) (parse-attribute pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute.new-pstate (b* (((mv acl2::?erp ?attr ?span ?new-pstate) (parse-attribute pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-list.attrs (b* (((mv acl2::?erp ?attrs ?span ?new-pstate) (parse-attribute-list pstate))) (attrib-listp attrs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-list.span (b* (((mv acl2::?erp ?attrs ?span ?new-pstate) (parse-attribute-list pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-list.new-pstate (b* (((mv acl2::?erp ?attrs ?span ?new-pstate) (parse-attribute-list pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-specifier.attrspec (b* (((mv acl2::?erp ?attrspec ?span ?new-pstate) (parse-attribute-specifier first-span pstate))) (attrib-specp attrspec)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-specifier.span (b* (((mv acl2::?erp ?attrspec ?span ?new-pstate) (parse-attribute-specifier first-span pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-attribute-specifier.new-pstate (b* (((mv acl2::?erp ?attrspec ?span ?new-pstate) (parse-attribute-specifier first-span pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-*-attribute-specifier.attrspecs (b* (((mv acl2::?erp ?attrspecs ?span ?new-pstate) (parse-*-attribute-specifier pstate))) (attrib-spec-listp attrspecs)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-*-attribute-specifier.span (b* (((mv acl2::?erp ?attrspecs ?span ?new-pstate) (parse-*-attribute-specifier pstate))) (spanp span)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-parse-*-attribute-specifier.new-pstate (b* (((mv acl2::?erp ?attrspecs ?span ?new-pstate) (parse-*-attribute-specifier pstate))) (parstatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm parsize-of-parse-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-expression-rest prev-expr prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-assignment-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-assignment-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-conditional-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-conditional-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-logical-or-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-or-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-logical-or-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-or-expression-rest prev-expr prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-logical-and-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-and-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-logical-and-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-and-expression-rest prev-expr prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-inclusive-or-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-inclusive-or-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-inclusive-or-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-inclusive-or-expression-rest prev-expr prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-exclusive-or-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-exclusive-or-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-exclusive-or-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-exclusive-or-expression-rest prev-expr prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-and-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-and-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-and-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-and-expression-rest prev-expr prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-equality-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-equality-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-equality-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-equality-expression-rest prev-expr prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-relational-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-relational-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-relational-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-relational-expression-rest prev-expr prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-shift-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-shift-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-shift-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-shift-expression-rest prev-expr prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-additive-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-additive-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-additive-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-additive-expression-rest prev-expr prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-multiplicative-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-multiplicative-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-multiplicative-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-multiplicative-expression-rest prev-expr prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-cast-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-cast-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-unary-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-unary-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-postfix-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-postfix-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-postfix-expression-rest-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-postfix-expression-rest prev-expr prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-argument-expressions-uncond (b* (((mv acl2::?erp ?exprs ?span ?new-pstate) (parse-argument-expressions pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-argument-expressions-rest-uncond (b* (((mv acl2::?erp ?exprs ?span ?new-pstate) (parse-argument-expressions-rest prev-exprs prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-primary-expression-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-primary-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-generic-associations-rest-uncond (b* (((mv acl2::?erp ?genassocs ?span ?new-pstate) (parse-generic-associations-rest prev-genassocs prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-generic-association-uncond (b* (((mv acl2::?erp ?genassoc ?span ?new-pstate) (parse-generic-association pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-compound-literal-uncond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-compound-literal tyname first-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-constant-expression-uncond (b* (((mv acl2::?erp ?cexpr ?span ?new-pstate) (parse-constant-expression pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-static-assert-declaration-uncond (b* (((mv acl2::?erp ?statassert ?span ?new-pstate) (parse-static-assert-declaration first-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-designator-uncond (b* (((mv acl2::?erp ?designor ?span ?new-pstate) (parse-designator pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-designator-list-uncond (b* (((mv acl2::?erp ?designors ?span ?new-pstate) (parse-designator-list pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse--initializer-uncond (b* (((mv acl2::?erp ?initer ?span ?new-pstate) (parse-initializer pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-designation?-initializer-uncond (b* (((mv acl2::?erp ?desiniter ?span ?new-pstate) (parse-designation?-initializer pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-initializer-list-uncond (b* (((mv acl2::?erp ?desiniters ?final-comma ?span ?new-pstate) (parse-initializer-list pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-enumerator-uncond (b* (((mv acl2::?erp ?enumer ?span ?new-pstate) (parse-enumerator pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-enumerator-list-uncond (b* (((mv acl2::?erp ?enumers ?final-comma ?span ?new-pstate) (parse-enumerator-list pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-specifier/qualifier-uncond (b* (((mv acl2::?erp ?specqual ?span ?new-pstate) (parse-specifier/qualifier tyspec-seenp pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-specifier-qualifier-list-uncond (b* (((mv acl2::?erp ?specquals ?span ?new-pstate) (parse-specifier-qualifier-list tyspec-seenp pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-specifier-uncond (b* (((mv acl2::?erp ?declspec ?span ?new-pstate) (parse-declaration-specifier tyspec-seenp pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-specifiers-uncond (b* (((mv acl2::?erp ?declspecs ?span ?new-pstate) (parse-declaration-specifiers tyspec-seenp pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-or-union-specifier-uncond (b* (((mv acl2::?erp ?strunispec ?span ?new-pstate) (parse-struct-or-union-specifier pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-enum-specifier-uncond (b* (((mv acl2::?erp ?enumspec ?span ?new-pstate) (parse-enum-specifier first-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-alignment-specifier-uncond (b* (((mv acl2::?erp ?alignspec ?span ?new-pstate) (parse-alignment-specifier first-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-array/function-abstract-declarator-uncond (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-array/function-abstract-declarator pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-direct-abstract-declarator-uncond (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-direct-abstract-declarator pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-direct-abstract-declarator-rest-uncond (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-direct-abstract-declarator-rest prev-dirabsdeclor prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-abstract-declarator-uncond (b* (((mv acl2::?erp ?absdeclor ?span ?new-pstate) (parse-abstract-declarator pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-array/function-declarator-uncond (b* (((mv acl2::?erp ?dirdeclor ?span ?new-pstate) (parse-array/function-declarator prev-dirdeclor prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-direct-declarator-uncond (b* (((mv acl2::?erp ?dirdeclor ?span ?new-pstate) (parse-direct-declarator pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-direct-declarator-rest-uncond (b* (((mv acl2::?erp ?dirdeclor ?span ?new-pstate) (parse-direct-declarator-rest prev-dirdeclor prev-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declarator-uncond (b* (((mv acl2::?erp ?declor ?span ?new-pstate) (parse-declarator pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declarator-uncond (b* (((mv acl2::?erp ?structdeclor ?span ?new-pstate) (parse-struct-declarator pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declarator-list-uncond (b* (((mv acl2::?erp ?structdeclors ?span ?new-pstate) (parse-struct-declarator-list pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declaration-uncond (b* (((mv acl2::?erp ?structdecl ?span ?new-pstate) (parse-struct-declaration pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declaration-list-uncond (b* (((mv acl2::?erp ?structdecls ?span ?new-pstate) (parse-struct-declaration-list pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-parameter-declaration-uncond (b* (((mv acl2::?erp ?paramdecl ?span ?new-pstate) (parse-parameter-declaration pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-parameter-declaration-list-uncond (b* (((mv acl2::?erp ?paramdecls ?ellipsis ?span ?new-pstate) (parse-parameter-declaration-list pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-type-name-uncond (b* (((mv acl2::?erp ?tyname ?span ?new-pstate) (parse-type-name pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-expression-or-type-name-uncond (b* (((mv acl2::?erp ?expr/tyname ?span ?new-pstate) (parse-expression-or-type-name pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declarator-or-abstract-declarator-uncond (b* (((mv acl2::?erp ?declor/absdeclor ?span ?new-pstate) (parse-declarator-or-abstract-declarator pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-parameters-uncond (b* (((mv acl2::?erp ?attrparams ?span ?new-pstate) (parse-attribute-parameters pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-uncond (b* (((mv acl2::?erp ?attr ?span ?new-pstate) (parse-attribute pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-list-uncond (b* (((mv acl2::?erp ?attrs ?span ?new-pstate) (parse-attribute-list pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-specifier-uncond (b* (((mv acl2::?erp ?attrspec ?span ?new-pstate) (parse-attribute-specifier first-span pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-*-attribute-specifier-uncond (b* (((mv acl2::?erp ?attrspecs ?span ?new-pstate) (parse-*-attribute-specifier pstate))) (<= (parsize new-pstate) (parsize pstate))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-assignment-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-conditional-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-conditional-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-logical-or-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-logical-or-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-logical-and-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-inclusive-or-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-exclusive-or-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-and-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-equality-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-relational-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-shift-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-additive-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-multiplicative-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-cast-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-unary-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-unary-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-postfix-expression-cond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-postfix-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-primary-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-generic-association pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-compound-literal-cond (b* (((mv acl2::?erp ?expr ?span ?new-pstate) (parse-compound-literal tyname first-span pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-constant-expression-cond (b* (((mv acl2::?erp ?cexpr ?span ?new-pstate) (parse-constant-expression pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-static-assert-declaration-cond (b* (((mv acl2::?erp ?statassert ?span ?new-pstate) (parse-static-assert-declaration first-span pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-designator-cond (b* (((mv acl2::?erp ?designor ?span ?new-pstate) (parse-designator pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-designator-list-cond (b* (((mv acl2::?erp ?designors ?span ?new-pstate) (parse-designator-list pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-initializer-cond (b* (((mv acl2::?erp ?initer ?span ?new-pstate) (parse-initializer pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-designation?-initializer-cond (b* (((mv acl2::?erp ?desiniter ?span ?new-pstate) (parse-designation?-initializer pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-initializer-list-cond (b* (((mv acl2::?erp ?desiniters ?final-comma ?span ?new-pstate) (parse-initializer-list pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-enumerator-cond (b* (((mv acl2::?erp ?enumer ?span ?new-pstate) (parse-enumerator pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-enumerator-list-cond (b* (((mv acl2::?erp ?enumers ?final-comma ?span ?new-pstate) (parse-enumerator-list pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-specifier/qualifier-cond (b* (((mv acl2::?erp ?specqual ?span ?new-pstate) (parse-specifier/qualifier tyspec-seenp pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-specifier-qualifier-list-cond (b* (((mv acl2::?erp ?specquals ?span ?new-pstate) (parse-specifier-qualifier-list tyspec-seenp pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-specifier-cond (b* (((mv acl2::?erp ?declspec ?span ?new-pstate) (parse-declaration-specifier tyspec-seenp pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declaration-specifiers-cond (b* (((mv acl2::?erp ?declspecs ?span ?new-pstate) (parse-declaration-specifiers tyspec-seenp pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-or-union-specifier-cond (b* (((mv acl2::?erp ?strunispec ?span ?new-pstate) (parse-struct-or-union-specifier pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-enum-specifier-cond (b* (((mv acl2::?erp ?enumspec ?span ?new-pstate) (parse-enum-specifier first-span pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-alignment-specifier-cond (b* (((mv acl2::?erp ?alignspec ?span ?new-pstate) (parse-alignment-specifier first-span pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-array/function-abstract-declarator-cond (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-array/function-abstract-declarator pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-direct-abstract-declarator-cond (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-direct-abstract-declarator pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-abstract-declarator pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-array/function-declarator-cond (b* (((mv acl2::?erp ?dirdeclor ?span ?new-pstate) (parse-array/function-declarator prev-dirdeclor prev-span pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-direct-declarator-cond (b* (((mv acl2::?erp ?dirdeclor ?span ?new-pstate) (parse-direct-declarator pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :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-pstate) (parse-declarator pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declarator-cond (b* (((mv acl2::?erp ?structdeclor ?span ?new-pstate) (parse-struct-declarator pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declarator-list-cond (b* (((mv acl2::?erp ?structdeclors ?span ?new-pstate) (parse-struct-declarator-list pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declaration-cond (b* (((mv acl2::?erp ?structdecl ?span ?new-pstate) (parse-struct-declaration pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-struct-declaration-list-cond (b* (((mv acl2::?erp ?structdecls ?span ?new-pstate) (parse-struct-declaration-list pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-parameter-declaration-cond (b* (((mv acl2::?erp ?paramdecl ?span ?new-pstate) (parse-parameter-declaration pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-parameter-declaration-list-cond (b* (((mv acl2::?erp ?paramdecls ?ellipsis ?span ?new-pstate) (parse-parameter-declaration-list pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-type-name-cond (b* (((mv acl2::?erp ?tyname ?span ?new-pstate) (parse-type-name pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-expression-or-type-name-cond (b* (((mv acl2::?erp ?expr/tyname ?span ?new-pstate) (parse-expression-or-type-name pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-declarator-or-abstract-declarator-cond (b* (((mv acl2::?erp ?declor/absdeclor ?span ?new-pstate) (parse-declarator-or-abstract-declarator pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-parameters-cond (b* (((mv acl2::?erp ?attrparams ?span ?new-pstate) (parse-attribute-parameters pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-cond (b* (((mv acl2::?erp ?attr ?span ?new-pstate) (parse-attribute pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-list-cond (b* (((mv acl2::?erp ?attrs ?span ?new-pstate) (parse-attribute-list pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-attribute-specifier-cond (b* (((mv acl2::?erp ?attrspec ?span ?new-pstate) (parse-attribute-specifier first-span pstate))) (implies (not erp) (<= (parsize new-pstate) (1- (parsize pstate))))) :rule-classes :linear)
Theorem:
(defthm parsize-of-parse-*-attribute-specifier-cond (b* nil t) :rule-classes nil)
Theorem:
(defthm dirabsdeclor-decl?-nil-p-of-parse-array/function-abstract-declarator (b* (((mv acl2::?erp ?dirabsdeclor ?span ?new-pstate) (parse-array/function-abstract-declarator pstate))) (implies (not erp) (dirabsdeclor-decl?-nil-p dirabsdeclor))))