Disambiguate an ambiguous cast or call expression to be a call expression.
(dimb-cast/call-to-call fun inc/dec rest) → call-expr
The form
In this function,
We perform the latter transformation via a recursion,
because we need to go through the individual postfix constructs of
Function:
(defun dimb-cast/call-to-call-loop (fun rest) (declare (xargs :guard (and (exprp fun) (exprp rest)))) (let ((__function__ 'dimb-cast/call-to-call-loop)) (declare (ignorable __function__)) (b* (((when (expr-case rest :paren)) (b* ((args (expr-to-asg-expr-list (expr-paren->unwrap rest)))) (make-expr-funcall :fun fun :args args))) ((when (expr-case rest :arrsub)) (b* ((expr (dimb-cast/call-to-call-loop fun (expr-arrsub->arg1 rest)))) (make-expr-arrsub :arg1 expr :arg2 (expr-arrsub->arg2 rest)))) ((when (expr-case rest :funcall)) (b* ((expr (dimb-cast/call-to-call-loop fun (expr-funcall->fun rest)))) (make-expr-funcall :fun expr :args (expr-funcall->args rest)))) ((when (expr-case rest :member)) (b* ((expr (dimb-cast/call-to-call-loop fun (expr-member->arg rest)))) (make-expr-member :arg expr :name (expr-member->name rest)))) ((when (expr-case rest :memberp)) (b* ((expr (dimb-cast/call-to-call-loop fun (expr-memberp->arg rest)))) (make-expr-memberp :arg expr :name (expr-memberp->name rest))))) (prog2$ (raise "Internal error: unexpected expression ~x0." (expr-fix fun)) (irr-expr)))))
Theorem:
(defthm exprp-of-dimb-cast/call-to-call-loop (b* ((new-expr (dimb-cast/call-to-call-loop fun rest))) (exprp new-expr)) :rule-classes :rewrite)
Theorem:
(defthm dimb-cast/call-to-call-loop-of-expr-fix-fun (equal (dimb-cast/call-to-call-loop (expr-fix fun) rest) (dimb-cast/call-to-call-loop fun rest)))
Theorem:
(defthm dimb-cast/call-to-call-loop-expr-equiv-congruence-on-fun (implies (expr-equiv fun fun-equiv) (equal (dimb-cast/call-to-call-loop fun rest) (dimb-cast/call-to-call-loop fun-equiv rest))) :rule-classes :congruence)
Theorem:
(defthm dimb-cast/call-to-call-loop-of-expr-fix-rest (equal (dimb-cast/call-to-call-loop fun (expr-fix rest)) (dimb-cast/call-to-call-loop fun rest)))
Theorem:
(defthm dimb-cast/call-to-call-loop-expr-equiv-congruence-on-rest (implies (expr-equiv rest rest-equiv) (equal (dimb-cast/call-to-call-loop fun rest) (dimb-cast/call-to-call-loop fun rest-equiv))) :rule-classes :congruence)
Function:
(defun dimb-cast/call-to-call (fun inc/dec rest) (declare (xargs :guard (and (exprp fun) (inc/dec-op-listp inc/dec) (exprp rest)))) (let ((__function__ 'dimb-cast/call-to-call)) (declare (ignorable __function__)) (b* ((fun (expr-paren fun)) (fun (apply-post-inc/dec-ops fun inc/dec))) (dimb-cast/call-to-call-loop fun rest))))
Theorem:
(defthm exprp-of-dimb-cast/call-to-call (b* ((call-expr (dimb-cast/call-to-call fun inc/dec rest))) (exprp call-expr)) :rule-classes :rewrite)
Theorem:
(defthm dimb-cast/call-to-call-of-expr-fix-fun (equal (dimb-cast/call-to-call (expr-fix fun) inc/dec rest) (dimb-cast/call-to-call fun inc/dec rest)))
Theorem:
(defthm dimb-cast/call-to-call-expr-equiv-congruence-on-fun (implies (expr-equiv fun fun-equiv) (equal (dimb-cast/call-to-call fun inc/dec rest) (dimb-cast/call-to-call fun-equiv inc/dec rest))) :rule-classes :congruence)
Theorem:
(defthm dimb-cast/call-to-call-of-inc/dec-op-list-fix-inc/dec (equal (dimb-cast/call-to-call fun (inc/dec-op-list-fix inc/dec) rest) (dimb-cast/call-to-call fun inc/dec rest)))
Theorem:
(defthm dimb-cast/call-to-call-inc/dec-op-list-equiv-congruence-on-inc/dec (implies (inc/dec-op-list-equiv inc/dec inc/dec-equiv) (equal (dimb-cast/call-to-call fun inc/dec rest) (dimb-cast/call-to-call fun inc/dec-equiv rest))) :rule-classes :congruence)
Theorem:
(defthm dimb-cast/call-to-call-of-expr-fix-rest (equal (dimb-cast/call-to-call fun inc/dec (expr-fix rest)) (dimb-cast/call-to-call fun inc/dec rest)))
Theorem:
(defthm dimb-cast/call-to-call-expr-equiv-congruence-on-rest (implies (expr-equiv rest rest-equiv) (equal (dimb-cast/call-to-call fun inc/dec rest) (dimb-cast/call-to-call fun inc/dec rest-equiv))) :rule-classes :congruence)