Better word operations

2 files changed, 61 insertions, 42 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperations.v b/src/ModularArithmetic/ModularBaseSystemListZOperations.v
index 60d887df8..a91dddb1f 100644
--- a/src/ModularArithmetic/ModularBaseSystemListZOperations.v
+++ b/src/ModularArithmetic/ModularBaseSystemListZOperations.v
@@ -14,12 +14,12 @@ Definition cmovne (x y r1 r2 : Z) := if Z.eqb x y then r1 else r2.
    neg 0 = 0 *)
 Definition neg (int_width : Z) (b : Z) := if Z.eqb b 1 then Z.ones int_width else 0%Z.
 
-Definition wcmovl_gen {logsz} x y r1 r2
-  := @ZToWord logsz (cmovl (@wordToZ logsz x) (@wordToZ logsz y) (@wordToZ logsz r1) (@wordToZ logsz r2)).
-Definition wcmovne_gen {logsz} x y r1 r2
-  := @ZToWord logsz (cmovne (@wordToZ logsz x) (@wordToZ logsz y) (@wordToZ logsz r1) (@wordToZ logsz r2)).
-Definition wneg_gen {logsz} (int_width : Z) b
-  := @ZToWord logsz (neg int_width (@wordToZ logsz b)).
+Definition wcmovl_gen {sz} x y r1 r2
+  := @ZToWord_gen sz (cmovl (@wordToZ_gen sz x) (@wordToZ_gen sz y) (@wordToZ_gen sz r1) (@wordToZ_gen sz r2)).
+Definition wcmovne_gen {sz} x y r1 r2
+  := @ZToWord_gen sz (cmovne (@wordToZ_gen sz x) (@wordToZ_gen sz y) (@wordToZ_gen sz r1) (@wordToZ_gen sz r2)).
+Definition wneg_gen {sz} (int_width : Z) b
+  := @ZToWord_gen sz (neg int_width (@wordToZ_gen sz b)).
 
 Definition wcmovl32 x y r1 r2 := ZToWord32 (cmovl (word32ToZ x) (word32ToZ y) (word32ToZ r1) (word32ToZ r2)).
 Definition wcmovne32 x y r1 r2 := ZToWord32 (cmovne (word32ToZ x) (word32ToZ y) (word32ToZ r1) (word32ToZ r2)).
@@ -34,11 +34,11 @@ Definition wcmovne128 x y r1 r2 := ZToWord128 (cmovne (word128ToZ x) (word128ToZ
 Definition wneg128 (int_width : Z) b := ZToWord128 (neg int_width (word128ToZ b)).
 
 Definition wcmovl {logsz}
-  := word_case (T:=fun sz => word sz -> word sz -> word sz -> word sz -> word sz)
-               logsz wcmovl32 wcmovl64 wcmovl128 (@wcmovl_gen).
+  := word_case_dep (T:=fun _ word => word -> word -> word -> word -> word)
+                   logsz wcmovl32 wcmovl64 wcmovl128 (fun _ => @wcmovl_gen _).
 Definition wcmovne {logsz}
-  := word_case (T:=fun sz => word sz -> word sz -> word sz -> word sz -> word sz)
-               logsz wcmovne32 wcmovne64 wcmovne128 (@wcmovne_gen).
+  := word_case_dep (T:=fun _ word => word -> word -> word -> word -> word)
+                   logsz wcmovne32 wcmovne64 wcmovne128 (fun _ => @wcmovne_gen _).
 Definition wneg {logsz}
-  := word_case (T:=fun sz => Z -> word sz -> word sz)
-               logsz wneg32 wneg64 wneg128 (@wneg_gen).
+  := word_case_dep (T:=fun _ word => Z -> word -> word)
+                   logsz wneg32 wneg64 wneg128 (fun _ => @wneg_gen _).
diff --git a/src/Util/FixedWordSizes.v b/src/Util/FixedWordSizes.v
index df5d5240d..8e2484ff6 100644
--- a/src/Util/FixedWordSizes.v
+++ b/src/Util/FixedWordSizes.v
@@ -8,20 +8,39 @@ Definition word64 := word 64. (* 2^6 *)
 Definition word128 := word 128. (* 2^7 *)
 
 Definition word_case {T : nat -> Type} (logsz : nat)
-           (case32 : T 32)
-           (case64 : T 64)
-           (case128 : T 128)
-           (default : forall k, T (2^k))
-  : T (2^logsz)
-  := match logsz return T (2^logsz) with
+           (case32 : T 5)
+           (case64 : T 6)
+           (case128 : T 7)
+           (default : forall k, T k)
+  : T logsz
+  := match logsz return T logsz with
      | 5 => case32
      | 6 => case64
      | 7 => case128
      | logsz' => default _
      end.
 
-Definition ZToWord32 (v : Z) : word32 := NToWord _ (Z.to_N v).
-Definition word32ToZ (v : word32) : Z := Z.of_N (wordToN v).
+Definition wordT logsz := word_case (T:=fun _ => Set) logsz word32 word64 word128 (fun logsz => word (2^logsz)).
+
+Definition word_case_dep {T : nat -> Set -> Type} (logsz : nat)
+           (case32 : T 5 word32)
+           (case64 : T 6 word64)
+           (case128 : T 7 word128)
+           (default : forall k, T k (word (2^k)))
+  : T logsz (wordT logsz)
+  := match logsz return T logsz (wordT logsz) with
+     | 5 => case32
+     | 6 => case64
+     | 7 => case128
+     | logsz' => default _
+     end.
+
+Definition ZToWord_gen {sz} (v : Z) : word sz := NToWord _ (Z.to_N v).
+Definition wordToZ_gen {sz} (v : word sz) : Z := Z.of_N (wordToN v).
+
+
+Definition ZToWord32 : Z -> word32 := @ZToWord_gen _.
+Definition word32ToZ : word32 -> Z := @wordToZ_gen _.
 Definition wadd32 : word32 -> word32 -> word32 := @wplus _.
 Definition wsub32 : word32 -> word32 -> word32 := @wminus _.
 Definition wmul32 : word32 -> word32 -> word32 := @wmult _.
@@ -30,8 +49,8 @@ Definition wshr32 : word32 -> word32 -> word32 := @wordBin N.shiftr _.
 Definition wland32 : word32 -> word32 -> word32 := @wand _.
 Definition wlor32 : word32 -> word32 -> word32 := @wor _.
 
-Definition ZToWord64 (v : Z) : word64 := NToWord _ (Z.to_N v).
-Definition word64ToZ (v : word64) : Z := Z.of_N (wordToN v).
+Definition ZToWord64 : Z -> word64 := @ZToWord_gen _.
+Definition word64ToZ : word64 -> Z := @wordToZ_gen _.
 Definition wadd64 : word64 -> word64 -> word64 := @wplus _.
 Definition wsub64 : word64 -> word64 -> word64 := @wminus _.
 Definition wmul64 : word64 -> word64 -> word64 := @wmult _.
@@ -40,8 +59,8 @@ Definition wshr64 : word64 -> word64 -> word64 := @wordBin N.shiftr _.
 Definition wland64 : word64 -> word64 -> word64 := @wand _.
 Definition wlor64 : word64 -> word64 -> word64 := @wor _.
 
-Definition ZToWord128 (v : Z) : word128 := NToWord _ (Z.to_N v).
-Definition word128ToZ (v : word128) : Z := Z.of_N (wordToN v).
+Definition ZToWord128 : Z -> word128 := @ZToWord_gen _.
+Definition word128ToZ : word128 -> Z := @wordToZ_gen _.
 Definition wadd128 : word128 -> word128 -> word128 := @wplus _.
 Definition wsub128 : word128 -> word128 -> word128 := @wminus _.
 Definition wmul128 : word128 -> word128 -> word128 := @wmult _.
@@ -51,29 +70,29 @@ Definition wland128 : word128 -> word128 -> word128 := @wand _.
 Definition wlor128 : word128 -> word128 -> word128 := @wor _.
 
 Definition ZToWord {logsz}
-  := word_case (T:=fun sz => Z -> word sz)
-               logsz ZToWord32 ZToWord64 ZToWord128 (fun _ v => NToWord _ (Z.to_N v)).
+  := word_case_dep (T:=fun _ word => Z -> word)
+                   logsz ZToWord32 ZToWord64 ZToWord128 (fun _ => @ZToWord_gen _).
 Definition wordToZ {logsz}
-  := word_case (T:=fun sz => word sz -> Z)
-               logsz word32ToZ word64ToZ word128ToZ (fun _ v => Z.of_N (wordToN v)).
+  := word_case_dep (T:=fun _ word => word -> Z)
+                   logsz word32ToZ word64ToZ word128ToZ (fun _ => @wordToZ_gen _).
 Definition wadd {logsz}
-  := word_case (T:=fun sz => word sz -> word sz -> word sz)
-               logsz wadd32 wadd64 wadd128 (fun _ => @wplus _).
+  := word_case_dep (T:=fun _ word => word -> word -> word)
+                   logsz wadd32 wadd64 wadd128 (fun _ => @wplus _).
 Definition wsub {logsz}
-  := word_case (T:=fun sz => word sz -> word sz -> word sz)
-               logsz wsub32 wsub64 wsub128 (fun _ => @wminus _).
+  := word_case_dep (T:=fun _ word => word -> word -> word)
+                   logsz wsub32 wsub64 wsub128 (fun _ => @wminus _).
 Definition wmul {logsz}
-  := word_case (T:=fun sz => word sz -> word sz -> word sz)
-               logsz wmul32 wmul64 wmul128 (fun _ => @wmult _).
+  := word_case_dep (T:=fun _ word => word -> word -> word)
+                   logsz wmul32 wmul64 wmul128 (fun _ => @wmult _).
 Definition wshl {logsz}
-  := word_case (T:=fun sz => word sz -> word sz -> word sz)
-               logsz wshl32 wshl64 wshl128 (fun _ => @wordBin N.shiftl _).
+  := word_case_dep (T:=fun _ word => word -> word -> word)
+                   logsz wshl32 wshl64 wshl128 (fun _ => @wordBin N.shiftl _).
 Definition wshr {logsz}
-  := word_case (T:=fun sz => word sz -> word sz -> word sz)
-               logsz wshr32 wshr64 wshr128 (fun _ => @wordBin N.shiftr _).
+  := word_case_dep (T:=fun _ word => word -> word -> word)
+                   logsz wshr32 wshr64 wshr128 (fun _ => @wordBin N.shiftr _).
 Definition wland {logsz}
-  := word_case (T:=fun sz => word sz -> word sz -> word sz)
-               logsz wland32 wland64 wland128 (fun _ => @wand _).
+  := word_case_dep (T:=fun _ word => word -> word -> word)
+                   logsz wland32 wland64 wland128 (fun _ => @wand _).
 Definition wlor {logsz}
-  := word_case (T:=fun sz => word sz -> word sz -> word sz)
-               logsz wlor32 wlor64 wlor128 (fun _ => @wor _).
+  := word_case_dep (T:=fun _ word => word -> word -> word)
+                   logsz wlor32 wlor64 wlor128 (fun _ => @wor _).