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