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