Disambiguate an ambiguous cast or conjunction expression to be a cast expression.
(dimb-cast/and-to-cast tyname inc/dec arg) → expr
This is analogous in purpose to dimb-cast/call-to-cast,
but for a different kind of ambiguous expression.
Note that the
Function:
(defun dimb-cast/and-to-cast (tyname inc/dec arg) (declare (xargs :guard (and (tynamep tyname) (inc/dec-op-listp inc/dec) (exprp arg)))) (let ((__function__ 'dimb-cast/and-to-cast)) (declare (ignorable __function__)) (b* (((mv bin? op arg1 arg2) (check-expr-binary arg)) ((unless (and bin? (member-eq (binop-kind op) '(:mul :div :rem :add :sub :shl :shr :lt :gt :le :ge :eq :ne)))) (make-expr-cast :type tyname :arg (make-expr-unary :op (unop-address) :arg (apply-pre-inc/dec-ops inc/dec arg)))) (expr (dimb-cast/and-to-cast tyname inc/dec arg1))) (make-expr-binary :op op :arg1 expr :arg2 arg2))))
Theorem:
(defthm exprp-of-dimb-cast/and-to-cast (b* ((expr (dimb-cast/and-to-cast tyname inc/dec arg))) (exprp expr)) :rule-classes :rewrite)
Theorem:
(defthm expr-unambp-of-dimb-cast/and-to-cast (implies (and (tyname-unambp tyname) (expr-unambp arg)) (b* ((?expr (dimb-cast/and-to-cast tyname inc/dec arg))) (expr-unambp expr))))
Theorem:
(defthm dimb-cast/and-to-cast-of-tyname-fix-tyname (equal (dimb-cast/and-to-cast (tyname-fix tyname) inc/dec arg) (dimb-cast/and-to-cast tyname inc/dec arg)))
Theorem:
(defthm dimb-cast/and-to-cast-tyname-equiv-congruence-on-tyname (implies (tyname-equiv tyname tyname-equiv) (equal (dimb-cast/and-to-cast tyname inc/dec arg) (dimb-cast/and-to-cast tyname-equiv inc/dec arg))) :rule-classes :congruence)
Theorem:
(defthm dimb-cast/and-to-cast-of-inc/dec-op-list-fix-inc/dec (equal (dimb-cast/and-to-cast tyname (inc/dec-op-list-fix inc/dec) arg) (dimb-cast/and-to-cast tyname inc/dec arg)))
Theorem:
(defthm dimb-cast/and-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/and-to-cast tyname inc/dec arg) (dimb-cast/and-to-cast tyname inc/dec-equiv arg))) :rule-classes :congruence)
Theorem:
(defthm dimb-cast/and-to-cast-of-expr-fix-arg (equal (dimb-cast/and-to-cast tyname inc/dec (expr-fix arg)) (dimb-cast/and-to-cast tyname inc/dec arg)))
Theorem:
(defthm dimb-cast/and-to-cast-expr-equiv-congruence-on-arg (implies (expr-equiv arg arg-equiv) (equal (dimb-cast/and-to-cast tyname inc/dec arg) (dimb-cast/and-to-cast tyname inc/dec arg-equiv))) :rule-classes :congruence)