Express carry_simple in terms of carry_gen

Also make much of the remaining code outside of Pow2BaseProofs
independent of the precise definition of carry_simple.  (We use [Local
Opaque] to enforce this modularity.

1 files changed, 5 insertions, 10 deletions

diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v
index f434a0c9f..b842fa713 100644
--- a/src/ModularArithmetic/Pow2Base.v
+++ b/src/ModularArithmetic/Pow2Base.v
@@ -55,24 +55,19 @@ Section Pow2Base.
     (*
     Definition add_to_nth n (x:Z) xs :=
       update_nth n (fun y => x + y) xs.
-
+     *)
     Definition carry_and_reduce_single i := fun di =>
       (Z.pow2_mod di (log_cap i),
        Z.shiftr di (log_cap i)).
 
-    Definition carry_gen f i := fun us =>
-      let i := (i mod length us)%nat in
+    Definition carry_gen fc fi i := fun us =>
+      let i := fi (length us) i in
       let di := nth_default 0 us      i in
       let '(di', ci) := carry_and_reduce_single i di in
       let us' := set_nth i di' us in
-      add_to_nth ((S i) mod (length us)) (f ci) us'.
+      add_to_nth (fi (length us) (S i)) (fc ci) us'.
 
-    Definition carry_simple := carry_gen (fun ci => ci).
-     *)
-    Definition carry_simple i := fun us =>
-      let di := nth_default 0 us      i in
-      let us' := set_nth i (Z.pow2_mod di (log_cap i)) us in
-      add_to_nth (S i) (   (Z.shiftr di (log_cap i))) us'.
+    Definition carry_simple := carry_gen (fun ci => ci) (fun _ i => i).
 
     Definition carry_simple_sequence is us := fold_right carry_simple us is.