Apply to an expression all the pre-increment and pre-decrement operators in a list.
(make-expr-unary-with-preinc/predec-ops ops expr) → new-expr
The operators are applied starting from the right, i.e. the last one in the list is applied first, then the second-to-last, and so on until the first (i.e. car). If the list is empty, the expression is unchanged.
Function:
(defun make-expr-unary-with-preinc/predec-ops (ops expr) (declare (xargs :guard (and (inc/dec-op-listp ops) (exprp expr)))) (let ((__function__ 'make-expr-unary-with-preinc/predec-ops)) (declare (ignorable __function__)) (b* (((when (endp ops)) (expr-fix expr)) (op (car ops)) (preop (inc/dec-op-case op :inc (unop-preinc) :dec (unop-predec))) (expr1 (make-expr-unary-with-preinc/predec-ops (cdr ops) expr))) (make-expr-unary :op preop :arg expr1))))
Theorem:
(defthm exprp-of-make-expr-unary-with-preinc/predec-ops (b* ((new-expr (make-expr-unary-with-preinc/predec-ops ops expr))) (exprp new-expr)) :rule-classes :rewrite)
Theorem:
(defthm make-expr-unary-with-preinc/predec-ops-of-inc/dec-op-list-fix-ops (equal (make-expr-unary-with-preinc/predec-ops (inc/dec-op-list-fix ops) expr) (make-expr-unary-with-preinc/predec-ops ops expr)))
Theorem:
(defthm make-expr-unary-with-preinc/predec-ops-inc/dec-op-list-equiv-congruence-on-ops (implies (inc/dec-op-list-equiv ops ops-equiv) (equal (make-expr-unary-with-preinc/predec-ops ops expr) (make-expr-unary-with-preinc/predec-ops ops-equiv expr))) :rule-classes :congruence)
Theorem:
(defthm make-expr-unary-with-preinc/predec-ops-of-expr-fix-expr (equal (make-expr-unary-with-preinc/predec-ops ops (expr-fix expr)) (make-expr-unary-with-preinc/predec-ops ops expr)))
Theorem:
(defthm make-expr-unary-with-preinc/predec-ops-expr-equiv-congruence-on-expr (implies (expr-equiv expr expr-equiv) (equal (make-expr-unary-with-preinc/predec-ops ops expr) (make-expr-unary-with-preinc/predec-ops ops expr-equiv))) :rule-classes :congruence)