More BigNum cleanup:

 * View of Int31 as a Z/nZ moved to file Z31Z.v (TO FINISH: specs are still admitted!)
 * Modular specification of Z/nZ moved to ZnZ and renamed CyclicType
 * More isolation between Cyclic/Abstract and Cyclic/DoubleCyclic
 * A few comments



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

9 files changed, 158 insertions, 122 deletions

diff --git a/Makefile.common b/Makefile.common
index 730e5678d9..6ffc7f82ac 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -620,7 +620,7 @@ CYCLICABSTRACTVO:=$(addprefix theories/Numbers/Cyclic/Abstract/, \
  ZnZ.vo )
 
 CYCLICINT31VO:=$(addprefix theories/Numbers/Cyclic/Int31/, \
- Int31.vo )
+ Int31.vo Z31Z.vo )
 
 CYCLICDOUBLECYCLICVO:=$(addprefix theories/Numbers/Cyclic/DoubleCyclic/, \
  Basic_type.vo	GenBase.vo	GenAdd.vo	GenSub.vo	\
diff --git a/theories/Numbers/Cyclic/Abstract/ZnZ.v b/theories/Numbers/Cyclic/Abstract/ZnZ.v
index 877e49c11e..9ec7648e61 100644
--- a/theories/Numbers/Cyclic/Abstract/ZnZ.v
+++ b/theories/Numbers/Cyclic/Abstract/ZnZ.v
@@ -16,11 +16,13 @@ Set Implicit Arguments.
 
 Require Import ZArith.
 Require Import Znumtheory.
+Require Import BigNumPrelude.
 Require Import Basic_type.
-Require Import GenBase.
 
 Open Local Scope Z_scope.
 
+(** First, a description via operator records and spec records. *)
+
 Section ZnZ_Op.
 
  Variable znz : Set.
@@ -90,7 +92,7 @@ Section ZnZ_Op.
 
 End ZnZ_Op.
 
-Section Spec.
+Section ZnZ_Spec.
  Variable w : Set.
  Variable w_op : znz_op w.
 
@@ -164,9 +166,6 @@ Section Spec.
 
  Notation "[|| x ||]" :=
    (zn2z_to_Z wB w_to_Z x)  (at level 0, x at level 99).
- 
- Notation "[! n | x !]" := (gen_to_Z w_digits w_to_Z n x) 
-       (at level 0, x at level 99).
 
  Record znz_spec : Set := mk_znz_spec {
 
@@ -271,8 +270,11 @@ Section Spec.
        [|w_sqrt x|] ^ 2 <= [|x|] < ([|w_sqrt x|] + 1) ^ 2
   }.
 
-End Spec.
+End ZnZ_Spec.
+
+
 
+(** Injecting [Z] numbers into a cyclic structure *)
 
 Section znz_of_pos.
  
@@ -315,3 +317,12 @@ Section znz_of_pos.
  intros p1 (H1, _); contradict H1; apply Zlt_not_le; red; simpl; auto.
  Qed.
 End znz_of_pos.
+
+
+(** A modular specification grouping the earlier records. *)
+
+Module Type CyclicType.
+ Parameter w : Set.
+ Parameter w_op : znz_op w.
+ Parameter w_spec : znz_spec w_op.
+End CyclicType.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v b/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v
index 60fa09584f..95f3c88e61 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v
@@ -15,6 +15,8 @@ Set Implicit Arguments.
 Require Import ZArith.
 Open Local Scope Z_scope.
 
+Definition base digits := Zpower 2 (Zpos digits).
+
 Section Carry.
 
  Variable A : Set.
@@ -29,6 +31,12 @@ Section Zn2Z.
 
  Variable znz : Set.
 
+ (** From a type [znz] representing a cyclic structure Z/nZ, 
+     we produce a representation of Z/2nZ by pairs of elements of [znz]
+     (plus a special case for zero). High half of the new number comes 
+     first. 
+ *)
+
  Inductive zn2z : Set :=
   | W0 : zn2z
   | WW : znz -> znz -> zn2z.
@@ -39,8 +47,6 @@ Section Zn2Z.
   | WW xh xl => w_to_Z xh * wB + w_to_Z xl
   end.
 
- Definition base digits := Zpower 2 (Zpos digits).
-
  Definition interp_carry sign B (interp:znz -> Z) c :=
   match c with
   | C0 x => interp x
@@ -51,11 +57,11 @@ End Zn2Z.
 
 Implicit Arguments W0 [znz].
 
-Fixpoint word_tr (w:Set) (n:nat) {struct n} : Set :=
- match n with
- | O => w
- | S n => word_tr (zn2z w) n
- end.
+(** From a cyclic representation [w], we iterate the [zn2z] construct 
+    [n] times, gaining the type of binary trees of depth at most [n], 
+    whose leafs are either W0 (if depth < n) or elements of w 
+    (if depth = n). 
+*)
 
 Fixpoint word (w:Set) (n:nat) {struct n} : Set :=
  match n with
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v b/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v
index eb517c0607..8d07c6dee9 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v
@@ -15,7 +15,6 @@ Set Implicit Arguments.
 Require Import ZArith.
 Require Import BigNumPrelude.
 Require Import Basic_type.
-Require Import JMeq.
 
 Open Local Scope Z_scope.
 
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 032326c81f..5cd504a34a 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -16,11 +16,17 @@ Require Export Basic_type.
 
 Unset Boxed Definitions.
 
-Inductive digits : Type := |D0 |D1.
+Inductive digits : Type := D0 | D1.
 
 Inductive int31 : Type :=
-| I31 : digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits ->digits -> int31
-.
+ | I31 : digits -> digits -> digits -> digits ->
+         digits -> digits -> digits -> digits ->
+         digits -> digits -> digits -> digits ->
+         digits -> digits -> digits -> digits ->
+         digits -> digits -> digits -> digits ->
+         digits -> digits -> digits -> digits ->
+         digits -> digits -> digits -> digits ->
+         digits -> digits -> digits -> int31.
 
 (* spiwack: Registration of the type of integers, so that the matchs in
    the functions below perform dynamic decompilation (otherwise some segfault
diff --git a/theories/Numbers/Cyclic/Int31/Z31Z.v b/theories/Numbers/Cyclic/Int31/Z31Z.v
new file mode 100644
index 0000000000..1a0046f8f6
--- /dev/null
+++ b/theories/Numbers/Cyclic/Int31/Z31Z.v
@@ -0,0 +1,114 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(** * Int31 numbers defines indeed a cyclic structure : Z/31Z *)
+
+(**
+Author: Arnaud Spiwack
+*)
+
+Require Export Int31.
+Require Import ZnZ.
+
+Open Scope int31_scope.
+
+Definition int31_op : znz_op int31.
+ split.
+
+ (* Conversion functions with Z *)
+ exact (31%positive). (* number of digits *)
+ exact (31). (* number of digits *)
+ exact (phi). (* conversion to Z *)
+ exact (positive_to_int31). (* positive -> N*int31 :  p => N,i where p = N*2^31+phi i *)
+ exact head031.  (* number of head 0 *)
+ exact tail031.  (* number of tail 0 *)
+
+ (* Basic constructors *)
+ exact 0. (* 0 *)
+ exact 1. (* 1 *)
+ exact Tn. (* 2^31 - 1 *)
+ (* A function which given two int31 i and j, returns a double word
+    which is worth i*2^31+j *)
+ exact (fun i j => match (match i ?= 0 with | Eq =>  j ?= 0 | not0 => not0 end) with | Eq => W0 | _ => WW i j end).
+ (* two special cases where i and j are respectively taken equal to 0 *)
+ exact (fun i => match i ?= 0 with | Eq => W0 | _ => WW i 0 end).
+ exact (fun j => match j ?= 0 with | Eq => W0 | _ => WW 0 j end).
+
+ (* Comparison *)
+ exact compare31.
+ exact (fun i => match i ?= 0 with | Eq => true | _ => false end).
+
+ (* Basic arithmetic operations *)
+ (* opposite functions *)
+ exact (fun i => 0 -c i).
+ exact (fun i => 0 - i).
+ exact (fun i => 0-i-1). (* the carry is always -1*)
+ (* successor and addition functions *)
+ exact (fun i => i +c 1).
+ exact add31c.
+ exact add31carryc.
+ exact (fun i => i + 1).
+ exact add31.
+ exact (fun i j => i + j + 1).
+ (* predecessor and subtraction functions *)
+ exact (fun i => i -c 1).
+ exact sub31c.
+ exact sub31carryc.
+ exact (fun i => i - 1).
+ exact sub31.
+ exact (fun i j => i - j - 1).
+ (* multiplication functions *)
+ exact mul31c.
+ exact mul31.
+ exact (fun x => x *c x).
+
+ (* special (euclidian) division operations *)
+ exact div3121.
+ exact div31. (* this is supposed to be the special case of division a/b where a > b *)
+ exact div31.
+ (* euclidian division remainder *)
+ (* again special case for a > b *)
+ exact (fun i j => let (_,r) := i/j in r).
+ exact (fun i j => let (_,r) := i/j in r).
+ (* gcd functions *)
+ exact gcd31. (*gcd_gt*)
+ exact gcd31. (*gcd*)
+ 
+ (* shift operations *)
+ exact addmuldiv31. (*add_mul_div  *)
+(*modulo 2^p  *)
+ exact (fun p i => 
+     match compare31 p 32 with
+     | Lt => addmuldiv31 p 0 (addmuldiv31 (31-p) i 0)
+     | _ => i
+     end).
+
+ (* is i even ? *)
+ exact (fun i => let (_,r) := i/2 in 
+                          match r ?= 0 with
+                          | Eq => true
+                          | _ => false
+                          end).
+
+ (* square root operations *)
+ exact sqrt312. (* sqrt2 *)
+ exact sqrt31. (* sqr *)
+Defined.
+
+
+Definition int31_spec : znz_spec int31_op.
+Admitted.
+
+
+Module Int31_words <: CyclicType.
+  Definition w := int31.
+  Definition w_op := int31_op.
+  Definition w_spec := int31_spec.
+End Int31_words.
diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
index 2bb9bec4b3..591d245a68 100644
--- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v
+++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
@@ -11,12 +11,12 @@
 (*i $Id$ i*)
 
 Require Export NZAxioms.
-Require Import NMake. (* contains W0Type *)
+Require Import NMake. (* contains CyclicType *)
 Require Import ZnZ.
 Require Import Basic_type. (* contains base *)
 Require Import BigNumPrelude.
 
-Module NZBigIntsAxiomsMod (Import BoundedIntsMod : W0Type) <: NZAxiomsSig.
+Module NZBigIntsAxiomsMod (Import BoundedIntsMod : CyclicType) <: NZAxiomsSig.
 
 Open Local Scope Z_scope.
 
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index ecb4578ebe..db4cd89650 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -15,105 +15,12 @@ Author: Arnaud Spiwack
 *)
 
 Require Export Int31.
+Require Import Z31Z.
 Require Import NMake.
 Require Import ZnZ.
 
 Open Scope int31_scope.
 
-Definition int31_op : znz_op int31.
- split.
-
- (* Conversion functions with Z *)
- exact (31%positive). (* number of digits *)
- exact (31). (* number of digits *)
- exact (phi). (* conversion to Z *)
- exact (positive_to_int31). (* positive -> N*int31 :  p => N,i where p = N*2^31+phi i *)
- exact head031.  (* number of head 0 *)
- exact tail031.  (* number of tail 0 *)
-
- (* Basic constructors *)
- exact 0. (* 0 *)
- exact 1. (* 1 *)
- exact Tn. (* 2^31 - 1 *)
- (* A function which given two int31 i and j, returns a double word
-    which is worth i*2^31+j *)
- exact (fun i j => match (match i ?= 0 with | Eq =>  j ?= 0 | not0 => not0 end) with | Eq => W0 | _ => WW i j end).
- (* two special cases where i and j are respectively taken equal to 0 *)
- exact (fun i => match i ?= 0 with | Eq => W0 | _ => WW i 0 end).
- exact (fun j => match j ?= 0 with | Eq => W0 | _ => WW 0 j end).
-
- (* Comparison *)
- exact compare31.
- exact (fun i => match i ?= 0 with | Eq => true | _ => false end).
-
- (* Basic arithmetic operations *)
- (* opposite functions *)
- exact (fun i => 0 -c i).
- exact (fun i => 0 - i).
- exact (fun i => 0-i-1). (* the carry is always -1*)
- (* successor and addition functions *)
- exact (fun i => i +c 1).
- exact add31c.
- exact add31carryc.
- exact (fun i => i + 1).
- exact add31.
- exact (fun i j => i + j + 1).
- (* predecessor and subtraction functions *)
- exact (fun i => i -c 1).
- exact sub31c.
- exact sub31carryc.
- exact (fun i => i - 1).
- exact sub31.
- exact (fun i j => i - j - 1).
- (* multiplication functions *)
- exact mul31c.
- exact mul31.
- exact (fun x => x *c x).
-
- (* special (euclidian) division operations *)
- exact div3121.
- exact div31. (* this is supposed to be the special case of division a/b where a > b *)
- exact div31.
- (* euclidian division remainder *)
- (* again special case for a > b *)
- exact (fun i j => let (_,r) := i/j in r).
- exact (fun i j => let (_,r) := i/j in r).
- (* gcd functions *)
- exact gcd31. (*gcd_gt*)
- exact gcd31. (*gcd*)
- 
- (* shift operations *)
- exact addmuldiv31. (*add_mul_div  *)
-(*modulo 2^p  *)
- exact (fun p i => 
-     match compare31 p 32 with
-     | Lt => addmuldiv31 p 0 (addmuldiv31 (31-p) i 0)
-     | _ => i
-     end).
-
- (* is i even ? *)
- exact (fun i => let (_,r) := i/2 in 
-                          match r ?= 0 with
-                          | Eq => true
-                          | _ => false
-                          end).
-
- (* square root operations *)
- exact sqrt312. (* sqrt2 *)
- exact sqrt31. (* sqr *)
-Defined.
-
-Definition int31_spec : znz_spec int31_op.
-Admitted.
-
-
-
-Module Int31_words <: W0Type.
-  Definition w := int31.
-  Definition w_op := int31_op.
-  Definition w_spec := int31_spec.
-End Int31_words.
-
 Module BigN := NMake.Make Int31_words.
 
 Definition bigN := BigN.t.
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index a180ed1e03..48e116564c 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -80,14 +80,7 @@ let _ =
   pr "Require Import Wf_nat.";
   pr "Require Import StreamMemo.";
   pr "";
-  pr "Module Type W0Type.";
-  pr " Parameter w : Set.";
-  pr " Parameter w_op : znz_op w.";
-  pr " Parameter w_spec : znz_spec w_op.";
-  pr "End W0Type.";
-  pr "";
-  pr "Module Make (W0:W0Type).";
-  pr " Import W0.";
+  pr "Module Make (Import W0:CyclicType).";
   pr "";
 
   pr " Definition w0 := W0.w.";