Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernel

4 files changed, 25 insertions, 83 deletions

diff --git a/library/coqlib.ml b/library/coqlib.ml
index 408e259196..36a9598f36 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -47,7 +47,7 @@ let gen_reference_in_modules locstr dirs s =
   let dirs = List.map make_dir dirs in
   let qualid = qualid_of_string s in
   let all = Nametab.locate_all qualid in
-  let all = List.sort_uniquize RefOrdered_env.compare all in
+  let all = List.sort_uniquize GlobRef.Ordered_env.compare all in
   let these = List.filter (has_suffix_in_dirs dirs) all in
   match these with
     | [x] -> x
diff --git a/library/globnames.ml b/library/globnames.ml
index 6383a1f8f6..6bbdd36489 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -87,65 +87,14 @@ let printable_constr_of_global = function
   | ConstructRef sp -> mkConstruct sp
   | IndRef sp -> mkInd sp
 
-let global_eq_gen eq_cst eq_ind eq_cons x y =
-  x == y ||
-  match x, y with
-  | ConstRef cx, ConstRef cy -> eq_cst cx cy
-  | IndRef indx, IndRef indy -> eq_ind indx indy
-  | ConstructRef consx, ConstructRef consy -> eq_cons consx consy
-  | VarRef v1, VarRef v2 -> Id.equal v1 v2
-  | (VarRef _ | ConstRef _ | IndRef _ | ConstructRef _), _ -> false
-
-let global_ord_gen ord_cst ord_ind ord_cons x y =
-  if x == y then 0
-  else match x, y with
-  | VarRef v1, VarRef v2 -> Id.compare v1 v2
-  | VarRef _, _ -> -1
-  | _, VarRef _ -> 1
-  | ConstRef cx, ConstRef cy -> ord_cst cx cy
-  | ConstRef _, _ -> -1
-  | _, ConstRef _ -> 1
-  | IndRef indx, IndRef indy -> ord_ind indx indy
-  | IndRef _, _ -> -1
-  | _ , IndRef _ -> 1
-  | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
-
-let global_hash_gen hash_cst hash_ind hash_cons gr =
-  let open Hashset.Combine in
-  match gr with
-  | ConstRef c -> combinesmall 1 (hash_cst c)
-  | IndRef i -> combinesmall 2 (hash_ind i)
-  | ConstructRef c -> combinesmall 3 (hash_cons c)
-  | VarRef id -> combinesmall 4 (Id.hash id)
-
-(* By default, [global_reference] are ordered on their canonical part *)
-
-module RefOrdered = struct
-  open Constant.CanOrd
-  type t = global_reference
-  let compare gr1 gr2 =
-    global_ord_gen compare ind_ord constructor_ord gr1 gr2
-  let equal gr1 gr2 = global_eq_gen equal eq_ind eq_constructor gr1 gr2
-  let hash gr = global_hash_gen hash ind_hash constructor_hash gr
-end
-
-module RefOrdered_env = struct
-  open Constant.UserOrd
-  type t = global_reference
-  let compare gr1 gr2 =
-    global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2
-  let equal gr1 gr2 =
-    global_eq_gen equal eq_user_ind eq_user_constructor gr1 gr2
-  let hash gr = global_hash_gen hash ind_user_hash constructor_user_hash gr
-end
-
-module Refmap = HMap.Make(RefOrdered)
-module Refset = Refmap.Set
+module RefOrdered = Names.GlobRef.Ordered
+module RefOrdered_env = Names.GlobRef.Ordered_env
 
-(* Alternative sets and maps indexed by the user part of the kernel names *)
+module Refmap = Names.GlobRef.Map
+module Refset = Names.GlobRef.Set
 
-module Refmap_env = HMap.Make(RefOrdered_env)
-module Refset_env = Refmap_env.Set
+module Refmap_env = Names.GlobRef.Map_env
+module Refset_env = Names.GlobRef.Set_env
 
 (* Extended global references *)
 
@@ -164,14 +113,14 @@ module ExtRefOrdered = struct
   let equal x y =
     x == y ||
     match x, y with
-    | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.equal rx ry
+    | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.equal rx ry
     | SynDef knx, SynDef kny -> KerName.equal knx kny
     | (TrueGlobal _ | SynDef _), _ -> false
 
   let compare x y =
     if x == y then 0
     else match x, y with
-      | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.compare rx ry
+      | TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.compare rx ry
       | SynDef knx, SynDef kny -> KerName.compare knx kny
       | TrueGlobal _, SynDef _ -> -1
       | SynDef _, TrueGlobal _ -> 1
@@ -179,7 +128,7 @@ module ExtRefOrdered = struct
   open Hashset.Combine
 
   let hash = function
-  | TrueGlobal gr -> combinesmall 1 (RefOrdered_env.hash gr)
+  | TrueGlobal gr -> combinesmall 1 (GlobRef.Ordered_env.hash gr)
   | SynDef kn -> combinesmall 2 (KerName.hash kn)
 
 end
diff --git a/library/globnames.mli b/library/globnames.mli
index 15fcd5bdd9..45ee069b06 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Util
 open Names
 open Constr
 open Mod_subst
@@ -49,27 +48,21 @@ val printable_constr_of_global : GlobRef.t -> constr
    raise [Not_found] if not a global reference *)
 val global_of_constr : constr -> GlobRef.t
 
-module RefOrdered : sig
-  type t = GlobRef.t
-  val compare : t -> t -> int
-  val equal : t -> t -> bool
-  val hash : t -> int
-end
+module RefOrdered = Names.GlobRef.Ordered
+[@@ocaml.deprecated "Use Names.GlobRef.Ordered"]
 
-module RefOrdered_env : sig
-  type t = GlobRef.t
-  val compare : t -> t -> int
-  val equal : t -> t -> bool
-  val hash : t -> int
-end
+module RefOrdered_env = Names.GlobRef.Ordered_env
+[@@ocaml.deprecated "Use Names.GlobRef.Ordered_env"]
 
-module Refset : CSig.SetS with type elt = GlobRef.t
-module Refmap : Map.ExtS
-  with type key = GlobRef.t and module Set := Refset
+module Refset = Names.GlobRef.Set
+[@@ocaml.deprecated "Use Names.GlobRef.Set"]
+module Refmap = Names.GlobRef.Map
+[@@ocaml.deprecated "Use Names.GlobRef.Map"]
 
-module Refset_env : CSig.SetS with type elt = GlobRef.t
-module Refmap_env : Map.ExtS
-  with type key = GlobRef.t and module Set := Refset_env
+module Refset_env = GlobRef.Set_env
+[@@ocaml.deprecated "Use Names.GlobRef.Set_env"]
+module Refmap_env = GlobRef.Map_env
+[@@ocaml.deprecated "Use Names.GlobRef.Map_env"]
 
 (** {6 Extended global references } *)
 
diff --git a/library/keys.ml b/library/keys.ml
index 3cadcb6472..a74d13c600 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -31,7 +31,7 @@ module KeyOrdered = struct
 
   let hash gr =
     match gr with
-    | KGlob gr -> 8 + RefOrdered.hash gr
+    | KGlob gr -> 8 + GlobRef.Ordered.hash gr
     | KLam -> 0
     | KLet -> 1
     | KProd -> 2
@@ -43,14 +43,14 @@ module KeyOrdered = struct
 
   let compare gr1 gr2 =
     match gr1, gr2 with
-    | KGlob gr1, KGlob gr2 -> RefOrdered.compare gr1 gr2
+    | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.compare gr1 gr2
     | _, KGlob _ -> -1
     | KGlob _, _ -> 1
     | k, k' -> Int.compare (hash k) (hash k')
     
   let equal k1 k2 =
     match k1, k2 with
-    | KGlob gr1, KGlob gr2 -> RefOrdered.equal gr1 gr2
+    | KGlob gr1, KGlob gr2 -> GlobRef.Ordered.equal gr1 gr2
     | _, KGlob _ -> false
     | KGlob _, _ -> false
     | k, k' -> k == k'