Modularization of BinInt, related fixes in the stdlib

 All the functions about Z is now in a separated file BinIntDef,
 which is Included in BinInt.Z. This BinInt.Z directly
 implements ZAxiomsSig, and instantiates derived properties ZProp.

 Note that we refer to Z instead of t inside BinInt.Z,
 otherwise ring breaks later on @eq Z.t

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

6 files changed, 59 insertions, 62 deletions

diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
index c73451e5c..12607b3ad 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -61,19 +61,19 @@ Extract Constant N.modulo =>
  "fun a b -> if Big.eq b Big.zero then Big.zero else Big.modulo a b".
 Extract Constant N.compare => "Big.compare_case Eq Lt Gt".
 
-Extract Constant Zplus => "Big.add".
-Extract Constant Zsucc => "Big.succ".
-Extract Constant Zpred => "Big.pred".
-Extract Constant Zminus => "Big.sub".
-Extract Constant Zmult => "Big.mult".
-Extract Constant Zopp => "Big.opp".
-Extract Constant Zabs => "Big.abs".
-Extract Constant Zmin => "Big.min".
-Extract Constant Zmax => "Big.max".
-Extract Constant Zcompare => "Big.compare_case Eq Lt Gt".
-
-Extract Constant Z_of_N => "fun p -> p".
-Extract Constant Zabs_N => "Big.abs".
+Extract Constant Z.add => "Big.add".
+Extract Constant Z.succ => "Big.succ".
+Extract Constant Z.pred => "Big.pred".
+Extract Constant Z.sub => "Big.sub".
+Extract Constant Z.mul => "Big.mult".
+Extract Constant Z.opp => "Big.opp".
+Extract Constant Z.abs => "Big.abs".
+Extract Constant Z.min => "Big.min".
+Extract Constant Z.max => "Big.max".
+Extract Constant Z.compare => "Big.compare_case Eq Lt Gt".
+
+Extract Constant Z.of_N => "fun p -> p".
+Extract Constant Z.abs_N => "Big.abs".
 
 (** Zdiv and Zmod are quite complex to define in terms of (/) and (mod).
     For the moment we don't even try *)
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index 4f6332d3d..55ba0ca1c 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -59,20 +59,20 @@ Extract Constant N.compare =>
  "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
 
 
-Extract Constant Zplus => "(+)".
-Extract Constant Zsucc => "succ".
-Extract Constant Zpred => "pred".
-Extract Constant Zminus => "(-)".
-Extract Constant Zmult => "( * )".
-Extract Constant Zopp => "(~-)".
-Extract Constant Zabs => "abs".
-Extract Constant Zmin => "min".
-Extract Constant Zmax => "max".
-Extract Constant Zcompare =>
+Extract Constant Z.add => "(+)".
+Extract Constant Z.succ => "succ".
+Extract Constant Z.pred => "pred".
+Extract Constant Z.sub => "(-)".
+Extract Constant Z.mul => "( * )".
+Extract Constant Z.opp => "(~-)".
+Extract Constant Z.abs => "abs".
+Extract Constant Z.min => "min".
+Extract Constant Z.max => "max".
+Extract Constant Z.compare =>
  "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
 
-Extract Constant Z_of_N => "fun p -> p".
-Extract Constant Zabs_N => "abs".
+Extract Constant Z.of_N => "fun p -> p".
+Extract Constant Z.abs_N => "abs".
 
 (** Zdiv and Zmod are quite complex to define in terms of (/) and (mod).
     For the moment we don't even try *)
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 6d0f40ac1..2db4db676 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -1009,12 +1009,7 @@ Definition eval := eval_formula.
 
 Definition prod_pos_nat := prod positive nat.
 
-Definition n_of_Z (z:Z) : N :=
-  match z with
-    | Z0 => N0
-    | Zpos p => Npos p
-    | Zneg p => N0
-  end.
+Notation n_of_Z := Z.to_N (only parsing).
 
 (* Local Variables: *)
 (* coding: utf-8 *)
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index f4368a1bb..bb9a8c2e7 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -15,21 +15,27 @@ type result =
  | Kimp of Term.constr * Term.constr
  | Kufo;;
 
+let meaningful_submodule = [ "Z"; "N"; "Pos" ]
+
+let string_of_global r =
+  let dp = Nametab.dirpath_of_global r in
+  let prefix = match Names.repr_dirpath dp with
+    | [] -> ""
+    | m::_ ->
+      let s = Names.string_of_id m in
+      if List.mem s meaningful_submodule then s^"." else ""
+  in
+  prefix^(Names.string_of_id (Nametab.basename_of_global r))
+
 let destructurate t =
   let c, args = Term.decompose_app t in
   match Term.kind_of_term c, args with
     | Term.Const sp, args ->
-	Kapp (Names.string_of_id
-		(Nametab.basename_of_global (Libnames.ConstRef sp)),
-	      args)
+	Kapp (string_of_global (Libnames.ConstRef sp), args)
     | Term.Construct csp , args ->
-	Kapp (Names.string_of_id
-		(Nametab.basename_of_global (Libnames.ConstructRef csp)),
-	      args)
+	Kapp (string_of_global (Libnames.ConstructRef csp), args)
     | Term.Ind isp, args ->
-	Kapp (Names.string_of_id
-		(Nametab.basename_of_global (Libnames.IndRef isp)),
-	      args)
+	Kapp (string_of_global (Libnames.IndRef isp), args)
     | Term.Var id,[] -> Kvar(Names.string_of_id id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
     | Term.Prod (Names.Name _,_,_),[] ->
@@ -272,10 +278,10 @@ end
 module Z : Int = struct
 
 let typ = lazy (constant "Z")
-let plus = lazy (constant "Zplus")
-let mult = lazy (constant  "Zmult")
-let opp = lazy (constant "Zopp")
-let minus = lazy (constant "Zminus")
+let plus = lazy (constant "Z.add")
+let mult = lazy (constant  "Z.mul")
+let opp = lazy (constant "Z.opp")
+let minus = lazy (constant "Z.sub")
 
 let coq_xH = lazy (constant "xH")
 let coq_xO = lazy (constant "xO")
@@ -318,12 +324,12 @@ let mk = mk_Z
 
 let parse_term t =
   try match destructurate t with
-    | Kapp("Zplus",[t1;t2]) -> Tplus (t1,t2)
-    | Kapp("Zminus",[t1;t2]) -> Tminus (t1,t2)
-    | Kapp("Zmult",[t1;t2]) -> Tmult (t1,t2)
-    | Kapp("Zopp",[t]) -> Topp t
-    | Kapp("Zsucc",[t]) -> Tsucc t
-    | Kapp("Zpred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one))
+    | Kapp("Z.add",[t1;t2]) -> Tplus (t1,t2)
+    | Kapp("Z.sub",[t1;t2]) -> Tminus (t1,t2)
+    | Kapp("Z.mul",[t1;t2]) -> Tmult (t1,t2)
+    | Kapp("Z.opp",[t]) -> Topp t
+    | Kapp("Z.succ",[t]) -> Tsucc t
+    | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one))
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) ->
 	(try Tnum (recognize t) with _ -> Tother)
     | _ -> Tother
@@ -334,17 +340,17 @@ let parse_rel gl t =
     | Kapp("eq",[typ;t1;t2])
       when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) -> Req (t1,t2)
     | Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
-    | Kapp("Zle",[t1;t2]) -> Rle (t1,t2)
-    | Kapp("Zlt",[t1;t2]) -> Rlt (t1,t2)
-    | Kapp("Zge",[t1;t2]) -> Rge (t1,t2)
-    | Kapp("Zgt",[t1;t2]) -> Rgt (t1,t2)
+    | Kapp("Z.le",[t1;t2]) -> Rle (t1,t2)
+    | Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2)
+    | Kapp("Z.ge",[t1;t2]) -> Rge (t1,t2)
+    | Kapp("Z.gt",[t1;t2]) -> Rgt (t1,t2)
     | _ -> parse_logic_rel t
   with e when Logic.catchable_exception e -> Rother
 
 let is_scalar t =
   let rec aux t = match destructurate t with
-    | Kapp(("Zplus"|"Zminus"|"Zmult"),[t1;t2]) -> aux t1 & aux t2
-    | Kapp(("Zopp"|"Zsucc"|"Zpred"),[t]) -> aux t
+    | Kapp(("Z.add"|"Z.sub"|"Z.mul"),[t1;t2]) -> aux t1 & aux t2
+    | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true
     | _ -> false in
   try aux t with _ -> false
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 31372a001..766473c6f 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -835,7 +835,7 @@ destruct n.
   assert
      (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z.
  change  ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z).
- rewrite <- Zplus_assoc. rewrite (Zplus_assoc  (- Zpos p4)).
+ rewrite <- Zplus_assoc. rewrite (Zplus_assoc  (- Zpos p4)%Z).
  simpl. rewrite Pcompare_refl. simpl. reflexivity.
  unfold Zminus, Zopp in H0. simpl in H0.
   rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial.
diff --git a/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v
index 92a753929..d3ed36ee9 100644
--- a/plugins/setoid_ring/ZArithRing.v
+++ b/plugins/setoid_ring/ZArithRing.v
@@ -27,11 +27,7 @@ Ltac isZpow_coef t :=
   | _ => constr:false
   end.
 
-Definition N_of_Z x :=
- match x with
- | Zpos p => Npos p
- | _ => N0
- end.
+Notation N_of_Z := Z.to_N (only parsing).
 
 Ltac Zpow_tac t :=
  match isZpow_coef t with