Permalink
Browse files

Using HMaps in global references.

  • Loading branch information...
1 parent adcc150 commit 643e624909ecec7ba43326ff962b13c184991125 @ppedrot ppedrot committed Mar 8, 2014
Showing with 50 additions and 20 deletions.
  1. +4 −0 kernel/names.ml
  2. +3 −0 kernel/names.mli
  3. +34 −14 library/globnames.ml
  4. +7 −4 library/globnames.mli
  5. +1 −1 library/nametab.ml
  6. +1 −1 plugins/extraction/table.mli
View
@@ -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
View
@@ -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 =
View
@@ -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 =
View
@@ -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 =
View
@@ -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)
@@ -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

0 comments on commit 643e624

Please sign in to comment.