Disambiguate an ambiguous cast or addition/subtraction expression to be a cast expression.
(dimb-cast/addsub-to-cast tyname inc/dec arg plus/minus) → expr
This is analogous in purpose to dimb-cast/call-to-cast,
but for a different kind of ambiguous expression,
actually two kinds, which are very similar and thus handled together;
the two kinds are selected by the unary operator passed as input.
Note that the
There is also an extra complexity here.
In the
(X) + Y * Z
which first the pattern
Function:
(defun dimb-cast/addsub-to-cast (tyname inc/dec arg plus/minus) (declare (xargs :guard (and (tynamep tyname) (inc/dec-op-listp inc/dec) (exprp arg) (unopp plus/minus)))) (declare (xargs :guard (or (unop-case plus/minus :plus) (unop-case plus/minus :minus)))) (let ((__function__ 'dimb-cast/addsub-to-cast)) (declare (ignorable __function__)) (b* (((mv mul? arg1 arg2) (check-expr-mul arg)) ((when (not mul?)) (make-expr-cast :type tyname :arg (make-expr-unary :op plus/minus :arg (apply-pre-inc/dec-ops inc/dec arg)))) (expr (dimb-cast/addsub-to-cast tyname inc/dec arg1 plus/minus))) (make-expr-binary :op (binop-mul) :arg1 expr :arg2 arg2))))
Theorem:
(defthm exprp-of-dimb-cast/addsub-to-cast (b* ((expr (dimb-cast/addsub-to-cast tyname inc/dec arg plus/minus))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm expr-unambp-of-dimb-cast/addsub-to-cast (implies (and (tyname-unambp tyname) (expr-unambp arg)) (b* ((?expr (dimb-cast/addsub-to-cast tyname inc/dec arg plus/minus))) (expr-unambp expr))))
Theorem:
(defthm dimb-cast/addsub-to-cast-of-tyname-fix-tyname (equal (dimb-cast/addsub-to-cast (tyname-fix tyname) inc/dec arg plus/minus) (dimb-cast/addsub-to-cast tyname inc/dec arg plus/minus)))
Theorem:
(defthm dimb-cast/addsub-to-cast-tyname-equiv-congruence-on-tyname (implies (tyname-equiv tyname tyname-equiv) (equal (dimb-cast/addsub-to-cast tyname inc/dec arg plus/minus) (dimb-cast/addsub-to-cast tyname-equiv inc/dec arg plus/minus))) :rule-classes :congruence)
Theorem:
(defthm dimb-cast/addsub-to-cast-of-inc/dec-op-list-fix-inc/dec (equal (dimb-cast/addsub-to-cast tyname (inc/dec-op-list-fix inc/dec) arg plus/minus) (dimb-cast/addsub-to-cast tyname inc/dec arg plus/minus)))
Theorem:
(defthm dimb-cast/addsub-to-cast-inc/dec-op-list-equiv-congruence-on-inc/dec (implies (inc/dec-op-list-equiv inc/dec inc/dec-equiv) (equal (dimb-cast/addsub-to-cast tyname inc/dec arg plus/minus) (dimb-cast/addsub-to-cast tyname inc/dec-equiv arg plus/minus))) :rule-classes :congruence)
Theorem:
(defthm dimb-cast/addsub-to-cast-of-expr-fix-arg (equal (dimb-cast/addsub-to-cast tyname inc/dec (expr-fix arg) plus/minus) (dimb-cast/addsub-to-cast tyname inc/dec arg plus/minus)))
Theorem:
(defthm dimb-cast/addsub-to-cast-expr-equiv-congruence-on-arg (implies (expr-equiv arg arg-equiv) (equal (dimb-cast/addsub-to-cast tyname inc/dec arg plus/minus) (dimb-cast/addsub-to-cast tyname inc/dec arg-equiv plus/minus))) :rule-classes :congruence)
Theorem:
(defthm dimb-cast/addsub-to-cast-of-unop-fix-plus/minus (equal (dimb-cast/addsub-to-cast tyname inc/dec arg (unop-fix plus/minus)) (dimb-cast/addsub-to-cast tyname inc/dec arg plus/minus)))
Theorem:
(defthm dimb-cast/addsub-to-cast-unop-equiv-congruence-on-plus/minus (implies (unop-equiv plus/minus plus/minus-equiv) (equal (dimb-cast/addsub-to-cast tyname inc/dec arg plus/minus) (dimb-cast/addsub-to-cast tyname inc/dec arg plus/minus-equiv))) :rule-classes :congruence)