Make use of id_tuple_with_alt_cps'

mit-plv · Nov 6, 2017 · 3d3e033 · 3d3e033
1 parent 52a8476
commit 3d3e033
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 9 deletions.
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
@@ -1076,15 +1076,15 @@ Hint Unfold
      Positional.select_cps
      Positional.select
      modulo div modulo_cps div_cps
-     id_tuple_with_alt id_tuple'_with_alt
+     id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps'
      Z.add_get_carry_full Z.add_get_carry_full_cps
   : basesystem_partial_evaluation_unfolder.
 
 Hint Unfold
      B.limb ListUtil.sum ListUtil.sum_firstn
      CPSUtil.Tuple.mapi_with_cps CPSUtil.Tuple.mapi_with'_cps CPSUtil.flat_map_cps CPSUtil.on_tuple_cps CPSUtil.fold_right_cps2
      Decidable.dec Decidable.dec_eq_Z
-     id_tuple_with_alt id_tuple'_with_alt
+     id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps'
      Z.add_get_carry_full Z.add_get_carry_full_cps Z.mul_split Z.mul_split_cps Z.mul_split_cps'
   : basesystem_partial_evaluation_unfolder.
 
@@ -1110,7 +1110,7 @@ Ltac basesystem_partial_evaluation_unfolder t :=
         Associational.carryterm_cps Associational.carryterm
         Associational.carry_cps Associational.carry
         Associational.negate_snd_cps Associational.negate_snd div modulo
-        id_tuple_with_alt id_tuple'_with_alt
+        id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps'
         Z.add_get_carry_full Z.add_get_carry_full_cps
     ] in t.
 

diff --git a/src/Arithmetic/CoreUnfolder.v b/src/Arithmetic/CoreUnfolder.v
@@ -3,6 +3,7 @@ Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.ZUtil.Definitions.
 Require Import Crypto.Util.ZUtil.CPS.
 Require Import Crypto.Util.IdfunWithAlt.
+Require Import Crypto.Util.CPSUtil.
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.Tactics.VM.
 
@@ -16,7 +17,7 @@ Ltac make_parameterized_sig t :=
                         B.limb ListUtil.sum ListUtil.sum_firstn
                         CPSUtil.Tuple.mapi_with_cps CPSUtil.Tuple.mapi_with'_cps CPSUtil.flat_map_cps CPSUtil.on_tuple_cps CPSUtil.fold_right_cps2
                         Decidable.dec Decidable.dec_eq_Z
-                        id_tuple_with_alt id_tuple'_with_alt
+                        id_tuple_with_alt id_tuple'_with_alt id_tuple_with_alt_cps'
                         Z.add_get_carry_full Z.mul_split
                         Z.add_get_carry_full_cps Z.mul_split_cps Z.mul_split_cps'
                         Z.add_get_carry_cps];

diff --git a/src/Arithmetic/Karatsuba.v b/src/Arithmetic/Karatsuba.v
@@ -78,7 +78,7 @@ Context (weight : nat -> Z)
     actually run and a version to bounds-check, along with a proof
     that they are exactly equal. This works around cases where the
     bounds proof requires high-level reasoning. *)
-  Local Notation id_with_alt_bounds := id_tuple_with_alt.
+  Local Notation id_with_alt_bounds_cps := id_tuple_with_alt_cps'.
 
   (*
     If:
@@ -134,27 +134,28 @@ Context (weight : nat -> Z)
       (fun sum_y => mul_cps weight sum_x sum_y
       (fun mul_sumxy =>
 
-      dlet z1 := id_with_alt_bounds (unbalanced_sub_cps weight mul_sumxy z0 id) (
+      id_with_alt_bounds_cps (fun f =>
+      (unbalanced_sub_cps weight mul_sumxy z0 f)) (fun f =>
 
       (mul_cps weight (fst x0_x1) (snd y0_y1)
       (fun x0_y1 => mul_cps weight (snd x0_x1) (fst y0_y1)
       (fun x1_y0 => mul_cps weight (fst x0_x1) (fst y0_y1)
       (fun z0 => mul_cps weight (snd x0_x1) (snd y0_y1)
       (fun z2 => add_cps weight z0 z2
       (fun sum_z => add_cps weight x0_y1 x1_y0
-      (fun z1' => add_cps weight z1' z2 id))))))))  in
+      (fun z1' => add_cps weight z1' z2 f)))))))) (fun z1 =>
 
                  Positional.to_associational_cps weight z1
       (fun z1 => Associational.mul_cps (pair s 1::nil) z1
       (fun sz1 => Positional.to_associational_cps weight sum_z
       (fun sum_z => Positional.from_associational_cps weight _ (sum_z++sz1) f
-      ))))))))))).
+      )))))))))))).
 
   Definition goldilocks_mul s xs ys := goldilocks_mul_cps s xs ys id.
   Lemma goldilocks_mul_id s xs ys R f :
     @goldilocks_mul_cps s xs ys R f = f (goldilocks_mul s xs ys).
   Proof.
-    cbv [goldilocks_mul goldilocks_mul_cps id_with_alt_bounds Let_In].
+    cbv [goldilocks_mul goldilocks_mul_cps Let_In].
     repeat autounfold. autorewrite with uncps push_id.
     reflexivity.
   Qed.