Add mul_split_cps'

It unfolds to Z.mul_split_at_bitwidth rather than
Z.mul_split_at_bitwidth_cps.  This is useful when reification still
needs to recognize Z.mul_split_at_bitwidth.

1 files changed, 12 insertions, 0 deletions

diff --git a/src/Util/ZUtil/CPS.v b/src/Util/ZUtil/CPS.v
index a875247a6..754f6cf56 100644
--- a/src/Util/ZUtil/CPS.v
+++ b/src/Util/ZUtil/CPS.v
@@ -144,4 +144,16 @@ Module Z.
     : @mul_split_cps T s x y f = f (Z.mul_split s x y).
   Proof. prove_cps_correct (). Qed.
   Hint Rewrite @mul_split_cps_correct : uncps.
+
+  Definition mul_split_cps' {T} (s x y : Z) (f : Z * Z -> T) : T
+    := eqb_cps
+         s (2^Z.log2 s)
+         (fun b
+          => if b
+             then f (Z.mul_split_at_bitwidth (Z.log2 s) x y)
+             else f ((x * y) mod s, (x * y) / s)).
+  Lemma mul_split_cps'_correct {T} (s x y : Z) (f : Z * Z -> T)
+    : @mul_split_cps' T s x y f = f (Z.mul_split s x y).
+  Proof. prove_cps_correct (). Qed.
+  Hint Rewrite @mul_split_cps'_correct : uncps.
 End Z.