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

1 files changed, 31 insertions, 25 deletions

diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index f4368a1bb2..bb9a8c2e72 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