Using HMaps in global references.

6 files changed, 50 insertions, 20 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 50402eb83..6b433c482 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -561,6 +561,8 @@ let ind_user_ord (m1, i1) (m2, i2) =
   if Int.equal c 0 then MutInd.UserOrd.compare m1 m2 else c
 let ind_hash (m, i) =
   Hashset.Combine.combine (MutInd.hash m) (Int.hash i)
+let ind_user_hash (m, i) =
+  Hashset.Combine.combine (MutInd.UserOrd.hash m) (Int.hash i)
 
 let eq_constructor (ind1, j1) (ind2, j2) = Int.equal j1 j2 && eq_ind ind1 ind2
 let constructor_ord (ind1, j1) (ind2, j2) =
@@ -571,6 +573,8 @@ let constructor_user_ord (ind1, j1) (ind2, j2) =
   if Int.equal c 0 then ind_user_ord ind1 ind2 else c
 let constructor_hash (ind, i) =
   Hashset.Combine.combine (ind_hash ind) (Int.hash i)
+let constructor_user_hash (ind, i) =
+  Hashset.Combine.combine (ind_user_hash ind) (Int.hash i)
 
 module InductiveOrdered = struct
   type t = inductive
diff --git a/kernel/names.mli b/kernel/names.mli
index a9da13399..b2a363174 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -243,6 +243,7 @@ sig
   (** Comparisons *)
   val compare : t -> t -> int
   val equal : t -> t -> bool
+  val hash : t -> int
 end
 
 module KNset  : CSig.SetS with type elt = KerName.t
@@ -412,10 +413,12 @@ val eq_ind : inductive -> inductive -> bool
 val ind_ord : inductive -> inductive -> int
 val ind_hash : inductive -> int
 val ind_user_ord : inductive -> inductive -> int
+val ind_user_hash : inductive -> int
 val eq_constructor : constructor -> constructor -> bool
 val constructor_ord : constructor -> constructor -> int
 val constructor_user_ord : constructor -> constructor -> int
 val constructor_hash : constructor -> int
+val constructor_user_hash : constructor -> int
 
 (** Better to have it here that in Closure, since required in grammar.cma *)
 type evaluable_global_reference =
diff --git a/library/globnames.ml b/library/globnames.ml
index 1eb21b6eb..7fce6b378 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -26,7 +26,7 @@ let isIndRef = function IndRef _ -> true | _ -> false
 let isConstructRef = function ConstructRef _ -> true | _ -> false
 
 let eq_gr gr1 gr2 =
-  match gr1,gr2 with
+  gr1 == gr2 || match gr1,gr2 with
     | ConstRef con1, ConstRef con2 -> eq_constant con1 con2
     | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2
     | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2
@@ -77,7 +77,9 @@ let constr_of_global = function
 let constr_of_reference = constr_of_global
 let reference_of_constr = global_of_constr
 
-let global_ord_gen ord_cst ord_ind ord_cons = (); fun x y -> match x, y with
+let global_ord_gen ord_cst ord_ind ord_cons x y =
+  if x == y then 0
+  else match x, y with
   | ConstRef cx, ConstRef cy -> ord_cst cx cy
   | IndRef indx, IndRef indy -> ord_ind indx indy
   | ConstructRef consx, ConstructRef consy -> ord_cons consx consy
@@ -90,30 +92,39 @@ let global_ord_gen ord_cst ord_ind ord_cons = (); fun x y -> match x, y with
   | IndRef _, ConstructRef _ -> -1
   | ConstructRef _, (VarRef _ | ConstRef _ | IndRef _) -> 1
 
-let global_ord_can =
-  global_ord_gen Constant.CanOrd.compare ind_ord constructor_ord
-let global_ord_user =
-  global_ord_gen Constant.UserOrd.compare ind_user_ord constructor_user_ord
+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 = global_ord_can
+  let compare gr1 gr2 =
+    global_ord_gen compare ind_ord constructor_ord 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 = global_ord_user
+  let compare gr1 gr2 =
+    global_ord_gen compare ind_user_ord constructor_user_ord gr1 gr2
+  let hash gr = global_hash_gen hash ind_user_hash constructor_user_hash gr
 end
 
-module Refset = Set.Make(RefOrdered)
-module Refmap = Map.Make(RefOrdered)
+module Refmap = HMap.Make(RefOrdered)
+module Refset = Refmap.Set
 
 (* Alternative sets and maps indexed by the user part of the kernel names *)
 
-module Refset_env = Set.Make(RefOrdered_env)
-module Refmap_env = Map.Make(RefOrdered_env)
+module Refmap_env = HMap.Make(RefOrdered_env)
+module Refset_env = Refmap_env.Set
 
 (* Extended global references *)
 
@@ -128,12 +139,21 @@ type extended_global_reference =
 
 module ExtRefOrdered = struct
   type t = extended_global_reference
+
   let compare x y =
-    match x, y with
-      | TrueGlobal rx, TrueGlobal ry -> global_ord_user rx ry
+    if x == y then 0
+    else match x, y with
+      | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.compare rx ry
       | SynDef knx, SynDef kny -> kn_ord knx kny
       | TrueGlobal _, SynDef _ -> -1
       | SynDef _, TrueGlobal _ -> 1
+
+  open Hashset.Combine
+
+  let hash = function
+  | TrueGlobal gr -> combinesmall 1 (RefOrdered_env.hash gr)
+  | SynDef kn -> combinesmall 2 (KerName.hash kn)
+
 end
 
 type global_reference_or_constr = 
diff --git a/library/globnames.mli b/library/globnames.mli
index 7afe80150..4569d8e1f 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -48,19 +48,21 @@ val reference_of_constr : constr -> global_reference
 
 module RefOrdered : sig
   type t = global_reference
-  val compare : global_reference -> global_reference -> int
+  val compare : t -> t -> int
+  val hash : t -> int
 end
 
 module RefOrdered_env : sig
   type t = global_reference
-  val compare : global_reference -> global_reference -> int
+  val compare : t -> t -> int
+  val hash : t -> int
 end
 
-module Refset : Set.S with type elt = global_reference
+module Refset : CSig.SetS with type elt = global_reference
 module Refmap : Map.ExtS
   with type key = global_reference and module Set := Refset
 
-module Refset_env : Set.S with type elt = global_reference
+module Refset_env : CSig.SetS with type elt = global_reference
 module Refmap_env : Map.ExtS
   with type key = global_reference and module Set := Refset_env
 
@@ -75,6 +77,7 @@ type extended_global_reference =
 module ExtRefOrdered : sig
   type t = extended_global_reference
   val compare : t -> t -> int
+  val hash : t -> int
 end
 
 type global_reference_or_constr = 
diff --git a/library/nametab.ml b/library/nametab.ml
index 2863f6cae..08eb02c9d 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -324,7 +324,7 @@ let the_dirtab = ref (DirTab.empty : dirtab)
 (* Reversed name tables ***************************************************)
 
 (* This table translates extended_global_references back to section paths *)
-module Globrevtab = Map.Make(ExtRefOrdered)
+module Globrevtab = HMap.Make(ExtRefOrdered)
 
 type globrevtab = full_path Globrevtab.t
 let the_globrevtab = ref (Globrevtab.empty : globrevtab)
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 91d2531dd..823b710cf 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -12,7 +12,7 @@ open Globnames
 open Miniml
 open Declarations
 
-module Refset' : Set.S with type elt = global_reference
+module Refset' : CSig.SetS with type elt = global_reference
 module Refmap' : Map.S with type key = global_reference
 
 val safe_basename_of_global : global_reference -> Id.t