switch theories/Numbers from Set to Type (both the abstract and the bignum part).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10964 85f007b7-540e-0410-9357-904b9bb8a0f7

11 files changed, 47 insertions, 32 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 4bd2331e1..ed099a1fd 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -28,9 +28,9 @@ Open Local Scope Z_scope.
 
 Section Z_nZ_Op.
 
- Variable znz : Set.
+ Variable znz : Type.
 
- Record znz_op : Set := mk_znz_op {
+ Record znz_op := mk_znz_op {
 
     (* Conversion functions with Z *)
     znz_digits : positive;  
@@ -76,7 +76,7 @@ Section Z_nZ_Op.
     znz_square_c    : znz -> zn2z znz;
 
     (* Special divisions operations *)
-    znz_div21       : znz -> znz -> znz -> znz*znz; (* very ad-hoc ?? *)
+    znz_div21       : znz -> znz -> znz -> znz*znz;
     znz_div_gt      : znz -> znz -> znz * znz; (* why this one ? *)
     znz_div         : znz -> znz -> znz * znz;
 
@@ -85,18 +85,22 @@ Section Z_nZ_Op.
 
     znz_gcd_gt      : znz -> znz -> znz; (* why this one ? *)
     znz_gcd         : znz -> znz -> znz; 
-    znz_add_mul_div : znz -> znz -> znz -> znz; (* very ad-hoc *)
+    (* [znz_add_mul_div p i j] is a combination of the [(digits-p)]
+       low bits of [i] above the [p] high bits of [j]: 
+       [znz_add_mul_div p i j = i*2^p+j/2^(digits-p)] *)
+    znz_add_mul_div : znz -> znz -> znz -> znz;
+    (* [znz_pos_mod p i] is [i mod 2^p] *)
     znz_pos_mod     : znz -> znz -> znz;
 
-   (* square root *)
     znz_is_even     : znz -> bool;
+    (* square root *)
     znz_sqrt2       : znz -> znz -> znz * carry znz;
     znz_sqrt        : znz -> znz  }.
 
 End Z_nZ_Op.
 
 Section Z_nZ_Spec.
- Variable w : Set.
+ Variable w : Type.
  Variable w_op : znz_op w.
 
  Let w_digits      := w_op.(znz_digits).
@@ -170,7 +174,7 @@ Section Z_nZ_Spec.
  Notation "[|| x ||]" :=
    (zn2z_to_Z wB w_to_Z x)  (at level 0, x at level 99).
 
- Record znz_spec : Set := mk_znz_spec {
+ Record znz_spec := mk_znz_spec {
 
     (* Conversion functions with Z *)
     spec_to_Z   : forall x, 0 <= [| x |] < wB;
@@ -281,13 +285,13 @@ End Z_nZ_Spec.
 
 Section znz_of_pos.
  
- Variable w : Set.
+ Variable w : Type.
  Variable w_op : znz_op w.
  Variable op_spec : znz_spec w_op.
 
  Notation "[| x |]" := (znz_to_Z w_op x)  (at level 0, x at level 99).
 
- Definition znz_of_Z (w:Set) (op:znz_op w) z :=
+ Definition znz_of_Z (w:Type) (op:znz_op w) z :=
  match z with
  | Zpos p => snd (op.(znz_of_pos) p)
  | _ => op.(znz_0)
@@ -325,7 +329,7 @@ End znz_of_pos.
 (** A modular specification grouping the earlier records. *)
 
 Module Type CyclicType.
- Parameter w : Set.
+ Parameter w : Type.
  Parameter w_op : znz_op w.
  Parameter w_spec : znz_spec w_op.
 End CyclicType.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
index d198361f1..d60af33ec 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
@@ -20,7 +20,7 @@ Require Import DoubleBase.
 Open Local Scope Z_scope.
 
 Section DoubleAdd.
- Variable w : Set.
+ Variable w : Type.
  Variable w_0 : w.
  Variable w_1 : w.
  Variable w_WW : w -> w -> zn2z w.
@@ -76,7 +76,7 @@ Section DoubleAdd.
     end
   end.
 
- Variable R : Set.
+ Variable R : Type.
  Variable f0 f1 : zn2z w -> R.
 
  Definition ww_add_c_cont x y :=
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
index 3d1d1c235..37b9f47b4 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
@@ -19,7 +19,7 @@ Require Import DoubleType.
 Open Local Scope Z_scope.
 
 Section DoubleBase.
- Variable w : Set.
+ Variable w : Type.
  Variable w_0   : w.
  Variable w_1   : w.
  Variable w_Bm1 : w.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 54ff3d354..0a8b281fb 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -30,7 +30,7 @@ Open Local Scope Z_scope.
 
 Section Z_2nZ.
 
- Variable w : Set.
+ Variable w : Type.
  Variable w_op : znz_op w.
  Let w_digits      := w_op.(znz_digits).
  Let w_zdigits      := w_op.(znz_zdigits).
@@ -890,7 +890,7 @@ End Z_2nZ.
  
 Section MulAdd.
  
-  Variable w: Set.
+  Variable w: Type.
   Variable op: znz_op w.
   Variable sop: znz_spec op.
 
@@ -918,5 +918,16 @@ Section MulAdd.
 End MulAdd.
 
 
+(** Modular versions of DoubleCyclic *) 
 
- 
+Module DoubleCyclic (C:CyclicType) <: CyclicType.
+ Definition w := zn2z C.w.
+ Definition w_op := mk_zn2z_op C.w_op.
+ Definition w_spec := mk_znz2_spec C.w_spec.
+End DoubleCyclic.
+
+Module DoubleCyclicKaratsuba (C:CyclicType) <: CyclicType.
+ Definition w := zn2z C.w.
+ Definition w_op := mk_zn2z_op_karatsuba C.w_op.
+ Definition w_spec := mk_znz2_karatsuba_spec C.w_spec.
+End DoubleCyclicKaratsuba.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
index cac2cc5b5..d3dfd2505 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
@@ -27,7 +27,7 @@ Ltac zarith := auto with zarith.
 
 Section POS_MOD.
 
- Variable w:Set.
+ Variable w:Type.
  Variable w_0 : w.
  Variable w_digits : positive.
  Variable w_zdigits : w.
@@ -201,7 +201,7 @@ End POS_MOD.
 
 Section DoubleDiv32.
 
- Variable w             : Set.
+ Variable w             : Type.
  Variable w_0           : w.
  Variable w_Bm1         : w.
  Variable w_Bm2         : w.
@@ -473,7 +473,7 @@ Section DoubleDiv32.
 End DoubleDiv32.
 
 Section DoubleDiv21.
- Variable w : Set.
+ Variable w : Type.
  Variable w_0 : w.
 
  Variable w_0W : w -> zn2z w.
@@ -634,7 +634,7 @@ Section DoubleDiv21.
 End DoubleDiv21.
 
 Section DoubleDivGt.
- Variable w : Set.
+ Variable w : Type.
  Variable w_digits : positive.
  Variable w_0 : w.
 
@@ -1344,7 +1344,7 @@ End DoubleDivGt.
 
 Section DoubleDiv.
 
- Variable w : Set.
+ Variable w : Type.
  Variable w_digits : positive.
  Variable ww_1 : zn2z w.
  Variable ww_compare : zn2z w -> zn2z w -> comparison.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
index 00ba4e4ee..1f1d609f1 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
@@ -21,7 +21,7 @@ Open Local Scope Z_scope.
 
 Section GENDIVN1.
 
- Variable w             : Set.
+ Variable w             : Type.
  Variable w_digits      : positive.
  Variable w_zdigits     : w.
  Variable w_0           : w.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
index 08f46aecd..d9c234093 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
@@ -20,7 +20,7 @@ Require Import DoubleBase.
 Open Local Scope Z_scope.
 
 Section DoubleLift.
- Variable w : Set.
+ Variable w : Type.
  Variable w_0 : w.
  Variable w_WW : w -> w -> zn2z w.
  Variable w_W0 : w ->  zn2z w.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
index bc2508972..cc3221401 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
@@ -20,7 +20,7 @@ Require Import DoubleBase.
 Open Local Scope Z_scope.
 
 Section DoubleMul.
- Variable w : Set.
+ Variable w : Type.
  Variable w_0 : w.
  Variable w_1 : w.
  Variable w_WW : w -> w -> zn2z w.
@@ -178,7 +178,7 @@ Section DoubleMul.
  End DoubleMulAddn1.
 
  Section DoubleMulAddmn1.
-  Variable wn: Set.
+  Variable wn: Type.
   Variable extend_n : w -> wn.
   Variable wn_0W : wn -> zn2z wn.
   Variable wn_WW : wn -> wn -> zn2z wn.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index 01dd3055f..00c7aeec6 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -20,7 +20,7 @@ Require Import DoubleBase.
 Open Local Scope Z_scope.
 
 Section DoubleSqrt.
- Variable w              : Set.
+ Variable w              : Type.
  Variable w_is_even      : w -> bool.
  Variable w_compare      : w -> w -> comparison.
  Variable w_0            : w.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
index 9dbfbb497..638bf6916 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
@@ -20,7 +20,7 @@ Require Import DoubleBase.
 Open Local Scope Z_scope.
 
 Section DoubleSub.
- Variable w : Set.
+ Variable w : Type.
  Variable w_0 : w.
  Variable w_Bm1 : w.
  Variable w_WW : w -> w -> zn2z w.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index dfc8b4e32..73fd266e4 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
@@ -19,9 +19,9 @@ Definition base digits := Zpower 2 (Zpos digits).
 
 Section Carry.
 
- Variable A : Set.
+ Variable A : Type.
 
- Inductive carry : Set :=
+ Inductive carry :=
   | C0 : A -> carry
   | C1 : A -> carry.
 
@@ -35,7 +35,7 @@ End Carry.
 
 Section Zn2Z.
 
- Variable znz : Set.
+ Variable znz : Type.
 
  (** From a type [znz] representing a cyclic structure Z/nZ, 
      we produce a representation of Z/2nZ by pairs of elements of [znz]
@@ -43,7 +43,7 @@ Section Zn2Z.
      first. 
  *)
 
- Inductive zn2z : Set :=
+ Inductive zn2z :=
   | W0 : zn2z
   | WW : znz -> znz -> zn2z.
 
@@ -63,7 +63,7 @@ Implicit Arguments W0 [znz].
     (if depth = n). 
 *)
 
-Fixpoint word (w:Set) (n:nat) {struct n} : Set :=
+Fixpoint word (w:Type) (n:nat) : Type :=
  match n with
  | O => w
  | S n => zn2z (word w n)