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

2 files changed, 2 insertions, 102 deletions

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.";