Split up assignments with complex right-hand sides.
(vl-assign-split x delta) → (mv new-x delta)
This is a little more interesting than usual. We want to split up the right-hand side of an assignment only if it is a compound expression that involves unsliceable arguments. That is, we don't want to split up assignments like:
But we do want to split up anything more complicated, for instance, if we have:
foo = bar + (baz + 1)
Then we want to split, because we have a top-level operator who has an
argument,
Function:
(defun vl-assign-split (x delta) (declare (xargs :guard (and (vl-assign-p x) (vl-delta-p delta)))) (let ((__function__ 'vl-assign-split)) (declare (ignorable __function__)) (b* (((vl-assign x) x) ((when (vl-nosplit-p x.expr)) (mv x delta)) (args (vl-nonatom->args x.expr)) ((when (vl-nosplitlist-p args)) (mv x delta)) ((mv new-args delta) (vl-exprlist-split args x delta)) (new-expr (change-vl-nonatom x.expr :args new-args)) (x-prime (change-vl-assign x :expr new-expr))) (mv x-prime delta))))
Theorem:
(defthm vl-assign-p-of-vl-assign-split.new-x (implies (and (force (vl-assign-p x)) (force (vl-delta-p delta))) (b* (((mv ?new-x ?delta) (vl-assign-split x delta))) (vl-assign-p new-x))) :rule-classes :rewrite)
Theorem:
(defthm vl-delta-p-of-vl-assign-split.delta (implies (and (force (vl-assign-p x)) (force (vl-delta-p delta))) (b* (((mv ?new-x ?delta) (vl-assign-split x delta))) (vl-delta-p delta))) :rule-classes :rewrite)