Create an ambiguous cast expression based on a token that is an additive operator.
(make-expr-cast/add-or-cast/sub-ambig plus/minus expr/tyname incdec expr) → new-expr
This is introduced just to avoid case splits in the large clique of mutually recursive parsing functions defined below. At some point in those functions, based on a parsed additive operator, we need to construct two different kinds of syntactically ambiguous cast expressions in our abstract syntax.
Function:
(defun make-expr-cast/add-or-cast/sub-ambig (plus/minus expr/tyname incdec expr) (declare (xargs :guard (and (tokenp plus/minus) (amb-expr/tyname-p expr/tyname) (inc/dec-op-listp incdec) (exprp expr)))) (declare (xargs :guard (token-additive-operator-p plus/minus))) (let ((__function__ 'make-expr-cast/add-or-cast/sub-ambig)) (declare (ignorable __function__)) (cond ((token-punctuatorp plus/minus "+") (make-expr-cast/add-ambig :type/arg1 expr/tyname :inc/dec incdec :arg/arg2 expr)) ((token-punctuatorp plus/minus "-") (make-expr-cast/sub-ambig :type/arg1 expr/tyname :inc/dec incdec :arg/arg2 expr)) (t (prog2$ (impossible) (irr-expr))))))
Theorem:
(defthm exprp-of-make-expr-cast/add-or-cast/sub-ambig (b* ((new-expr (make-expr-cast/add-or-cast/sub-ambig plus/minus expr/tyname incdec expr))) (exprp new-expr)) :rule-classes :rewrite)