Fixing generic hashes and replacing them with proper ones.

9 files changed, 118 insertions, 34 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 262cbab2f..6e5ac5f33 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -254,7 +254,8 @@ let keymap_find key map =
 
 (* Scopes table : interpretation -> scope_name *)
 let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t)
-let prim_token_key_table = Hashtbl.create 7
+
+let prim_token_key_table = ref KeyMap.empty
 
 let glob_prim_constr_key = function
   | GApp (_,GRef (_,ref),_) | GRef (_,ref) -> RefKey (canonical_gr ref)
@@ -309,8 +310,8 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
   declare_scope sc;
   add_prim_token_interpreter sc interp;
   List.iter (fun pat ->
-      Hashtbl.add prim_token_key_table
-        (glob_prim_constr_key pat) (sc,uninterp,b))
+      prim_token_key_table := KeyMap.add
+        (glob_prim_constr_key pat) (sc,uninterp,b) !prim_token_key_table)
     patl
 
 let mkNumeral n = Numeral n
@@ -487,7 +488,7 @@ let availability_of_notation (ntn_scope,ntn) scopes =
 let uninterp_prim_token c =
   try
     let (sc,numpr,_) =
-      Hashtbl.find prim_token_key_table (glob_prim_constr_key c) in
+      KeyMap.find (glob_prim_constr_key c) !prim_token_key_table in
     match numpr c with
       | None -> raise Notation_ops.No_match
       | Some n -> (sc,n)
@@ -496,8 +497,8 @@ let uninterp_prim_token c =
 let uninterp_prim_token_ind_pattern ind args =
   let ref = IndRef ind in
   try
-    let (sc,numpr,b) = Hashtbl.find prim_token_key_table
-      (RefKey (canonical_gr ref)) in
+    let k = RefKey (canonical_gr ref) in
+    let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in
     if not b then raise Notation_ops.No_match;
     let args' = List.map
       (fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in
@@ -510,7 +511,7 @@ let uninterp_prim_token_ind_pattern ind args =
 let uninterp_prim_token_cases_pattern c =
   try
     let k = cases_pattern_key c in
-    let (sc,numpr,b) = Hashtbl.find prim_token_key_table k in
+    let (sc,numpr,b) = KeyMap.find k !prim_token_key_table in
     if not b then raise Notation_ops.No_match;
     let na,c = glob_constr_of_closed_cases_pattern c in
     match numpr c with
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f81bcceb3..f8724180e 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -40,8 +40,25 @@ type my_global_reference =
   | IndRef of inductive
   | ConstructRef of constructor
 
+module RefHash =
+struct
+  type t = my_global_reference
+  let equal gr1 gr2 = match gr1, gr2 with
+  | ConstRef c1, ConstRef c2 -> Constant.CanOrd.equal c1 c2
+  | IndRef i1, IndRef i2 -> eq_ind i1 i2
+  | ConstructRef c1, ConstructRef c2 -> eq_constructor c1 c2
+  | _ -> false
+  open Hashset.Combine
+  let hash = function
+  | ConstRef c -> combinesmall 1 (Constant.hash c)
+  | IndRef i -> combinesmall 2 (ind_hash i)
+  | ConstructRef c -> combinesmall 3 (constructor_hash c)
+end
+
+module RefTable = Hashtbl.Make(RefHash)
+
 let share cache r (cstl,knl) =
-  try Hashtbl.find cache r
+  try RefTable.find cache r
   with Not_found ->
   let f,l =
     match r with
@@ -52,7 +69,7 @@ let share cache r (cstl,knl) =
     | ConstRef cst ->
 	mkConst (pop_con cst), Cmap.find cst cstl in
   let c = mkApp (f, Array.map mkVar l) in
-  Hashtbl.add cache r c;
+  RefTable.add cache r c;
   c
 
 let update_case_info cache ci modlist =
@@ -129,12 +146,12 @@ let constr_of_def = function
   | OpaqueDef lc -> Opaqueproof.force_proof lc
 
 let cook_constr { Opaqueproof.modlist ; abstract } c =
-  let cache = Hashtbl.create 13 in
+  let cache = RefTable.create 13 in
   let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in
   abstract_constant_body (expmod_constr cache modlist c) hyps
 
 let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
-  let cache = Hashtbl.create 13 in
+  let cache = RefTable.create 13 in
   let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in
   let body = on_body modlist hyps
     (fun c -> abstract_constant_body (expmod_constr cache modlist c) hyps)
@@ -158,4 +175,4 @@ let cook_constant env { from = cb; info = { Opaqueproof.modlist; abstract } } =
   in
   (body, typ, cb.const_constraints, cb.const_inline_code, Some const_hyps)
 
-let expmod_constr modlist c = expmod_constr (Hashtbl.create 13) modlist c
+let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c
diff --git a/kernel/names.mli b/kernel/names.mli
index 816467721..56b812fd0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -371,6 +371,8 @@ sig
   val equal : t -> t -> bool
   (** Default comparison, alias for [CanOrd.equal] *)
 
+  val hash : t -> int
+
   (** Displaying *)
 
   val to_string : t -> string
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 3be56b189..5fa0d41e0 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -80,6 +80,21 @@ let eq_gname gn1 gn2 =
   | Gnamed id1, Gnamed id2 -> Id.equal id1 id2
   | _ -> false
 
+open Hashset.Combine
+
+let gname_hash gn = match gn with
+| Gind (s, i) -> combinesmall 1 (combine (String.hash s) (ind_hash i))
+| Gconstruct (s, c) -> combinesmall 2 (combine (String.hash s) (constructor_hash c))
+| Gconstant (s, c) -> combinesmall 3 (combine (String.hash s) (Constant.hash c))
+| Gcase (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gpred (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gfixtype (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gnorm (l, i) -> combinesmall 7 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gnormtbl (l, i) -> combinesmall 8 (combine (Option.hash Label.hash l) (Int.hash i))
+| Ginternal s -> combinesmall 9 (String.hash s)
+| Grel i -> combinesmall 10 (Int.hash i)
+| Gnamed id -> combinesmall 11 (Id.hash id)
+
 let case_ctr = ref (-1)
 
 let reset_gcase () = case_ctr := -1
@@ -148,11 +163,9 @@ let eq_symbol sy1 sy2 =
      Evar.equal evk1 evk2 && Array.for_all2 eq_constr args1 args2
   | _, _ -> false
 
-open Hashset.Combine
-
 let hash_symbol symb =
   match symb with
-  | SymbValue v -> combinesmall 1 (Hashtbl.hash v)
+  | SymbValue v -> combinesmall 1 (Hashtbl.hash v) (** FIXME *)
   | SymbSort s -> combinesmall 2 (Sorts.hash s)
   | SymbName name -> combinesmall 3 (Name.hash name)
   | SymbConst c -> combinesmall 4 (Constant.hash c)
@@ -266,6 +279,28 @@ let eq_primitive p1 p2 =
   | Mk_evar, Mk_evar -> true
   | _ -> false
 
+let primitive_hash = function
+| Mk_prod -> 1
+| Mk_sort -> 2
+| Mk_ind -> 3
+| Mk_const -> 4
+| Mk_sw -> 5
+| Mk_fix (r, i) ->
+  let h = Array.fold_left (fun h i -> combine h (Int.hash i)) 0 r in
+  combinesmall 6 (combine h (Int.hash i))
+| Mk_cofix i ->
+  combinesmall 7 (Int.hash i)
+| Mk_rel i ->
+  combinesmall 8 (Int.hash i)
+| Mk_var id ->
+  combinesmall 9 (Id.hash id)
+| Is_accu -> 10
+| Cast_accu -> 11
+| Upd_cofix -> 12
+| Force_cofix -> 13
+| Mk_meta -> 14
+| Mk_evar -> 15
+
 type mllambda =
   | MLlocal        of lname 
   | MLglobal       of gname 
@@ -373,8 +408,8 @@ and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 =
 let rec hash_mllambda gn n env t =
   match t with
   | MLlocal ln -> combinesmall 1 (LNmap.find ln env)
-  | MLglobal gn' -> combinesmall 2 (if eq_gname gn gn' then 0 else Hashtbl.hash gn')
-  | MLprimitive prim -> combinesmall 3 (Hashtbl.hash prim)
+  | MLglobal gn' -> combinesmall 2 (if eq_gname gn gn' then 0 else gname_hash gn')
+  | MLprimitive prim -> combinesmall 3 (primitive_hash prim)
   | MLlam (lns, ml) ->
       let env = push_lnames n env lns in
       combinesmall 4 (combine (Array.length lns) (hash_mllambda gn (n+1) env ml))
@@ -397,18 +432,18 @@ let rec hash_mllambda gn n env t =
       let hbr' = hash_mllambda gn n env br' in
       combinesmall 8 (combine3 hcond hbr hbr')
   | MLmatch (annot, c, accu, br) ->
-      let hannot = Hashtbl.hash annot in
+      let hannot = hash_annot_sw annot in
       let hc = hash_mllambda gn n env c in
       let haccu = hash_mllambda gn n env accu in
       combinesmall 9 (hash_mllam_branches gn n env (combine3 hannot hc haccu) br)
   | MLconstruct (pf, cs, args) ->
-      let hpf = Hashtbl.hash pf in
-      let hcs = Hashtbl.hash cs in
+      let hpf = String.hash pf in
+      let hcs = constructor_hash cs in
       combinesmall 10 (hash_mllambda_array gn n env (combine hpf hcs) args)
   | MLint (ty,v) ->
-      combinesmall 11 (combine (Hashtbl.hash ty) v)
+      combinesmall 11 (combine (if ty then 0 else 1) v)
   | MLsetref (id, ml) ->
-      let hid = Hashtbl.hash id in
+      let hid = String.hash id in
       let hml = hash_mllambda gn n env ml in
       combinesmall 12 (combine hid hml)
   | MLsequence (ml, ml') ->
@@ -430,7 +465,7 @@ and hash_mllambda_array gn n env init arr =
 and hash_mllam_branches gn n env init br =
   let hash_cargs (cs, args) body =
     let nargs = Array.length args in
-    let hcs = Hashtbl.hash cs in
+    let hcs = constructor_hash cs in
     let env = opush_lnames n env args in
     let hbody = hash_mllambda gn (n + nargs) env body in
     combine3 nargs hcs hbody
@@ -564,10 +599,10 @@ let hash_global g =
       let env = push_lnames 0 LNmap.empty lns in
       let t = MLmatch (annot,c,accu,br) in
       combinesmall 4 (combine nlns (hash_mllambda gn nlns env t))
-  | Gopen s -> combinesmall 5 (Hashtbl.hash s)
+  | Gopen s -> combinesmall 5 (String.hash s)
   | Gtype (ind, arr) ->
-      combinesmall 6 (combine (Hashtbl.hash ind) (Hashtbl.hash arr))
-  | Gcomment s -> combinesmall 7 (Hashtbl.hash s)
+      combinesmall 6 (combine (ind_hash ind) (Array.fold_left combine 0 arr))
+  | Gcomment s -> combinesmall 7 (String.hash s)
   
 let global_stack = ref ([] : global list)
 
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index e6a579c5b..a757f013a 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -473,18 +473,27 @@ let empty_args = [||]
 module Renv = 
   struct
 
+    module ConstrHash =
+    struct
+      type t = constructor
+      let equal = eq_constructor
+      let hash = constructor_hash
+    end
+
+    module ConstrTable = Hashtbl.Make(ConstrHash)
+
     type constructor_info = tag * int * int (* nparam nrealargs *)
 
     type t = {
 	name_rel : name Vect.t;
-	construct_tbl : (constructor, constructor_info) Hashtbl.t;
+	construct_tbl : constructor_info ConstrTable.t;
 
        }
 
 
     let make () = {
       name_rel = Vect.make 16 Anonymous;
-      construct_tbl = Hashtbl.create 111
+      construct_tbl = ConstrTable.create 111
     }
 
     let push_rel env id = Vect.push env.name_rel id
@@ -501,7 +510,7 @@ module Renv =
       Lrel (Vect.get_last env.name_rel (n-1), n)
 
     let get_construct_info env c =
-      try Hashtbl.find env.construct_tbl c 
+      try ConstrTable.find env.construct_tbl c
       with Not_found -> 
 	let ((mind,j), i) = c in
 	let oib = lookup_mind mind !global_env in
@@ -509,7 +518,7 @@ module Renv =
 	let tag,arity = oip.mind_reloc_tbl.(i-1) in
 	let nparams = oib.mind_nparams in
 	let r = (tag, nparams, arity) in
-	Hashtbl.add env.construct_tbl c r;
+	ConstrTable.add env.construct_tbl c r;
 	r
   end
 
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index c3e2b3ab7..98094f795 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -39,7 +39,7 @@ let eq_annot_sw asw1 asw2 =
 open Hashset.Combine
 
 let hash_annot_sw asw =
-  combine (Hashtbl.hash asw.asw_ind) (Hashtbl.hash asw.asw_prefix)
+  combine (ind_hash asw.asw_ind) (String.hash asw.asw_prefix)
 
 type sort_annot = string * int
 
diff --git a/kernel/vm.ml b/kernel/vm.ml
index bc7116a35..30add56f9 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -304,13 +304,26 @@ let val_of_str_const str = val_of_obj (obj_of_str_const str)
 
 let val_of_atom a = val_of_obj (obj_of_atom a)
 
-let idkey_tbl = Hashtbl.create 31
+module IdKeyHash =
+struct
+  type t = id_key
+  let equal = Names.eq_id_key
+  open Hashset.Combine
+  let hash = function
+  | ConstKey c -> combinesmall 1 (Constant.hash c)
+  | VarKey id -> combinesmall 2 (Id.hash id)
+  | RelKey i -> combinesmall 3 (Int.hash i)
+end
+
+module KeyTable = Hashtbl.Make(IdKeyHash)
+
+let idkey_tbl = KeyTable.create 31
 
 let val_of_idkey key =
-  try Hashtbl.find idkey_tbl key
+  try KeyTable.find idkey_tbl key
   with Not_found ->
     let v = val_of_atom (Aid key) in
-    Hashtbl.add idkey_tbl key v;
+    KeyTable.add idkey_tbl key v;
     v
 
 let val_of_rel k = val_of_idkey (RelKey k)
diff --git a/lib/option.ml b/lib/option.ml
index 1ef45d232..abdae892f 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -35,6 +35,10 @@ let compare f x y = match x, y with
 | None, Some _ -> -1
 | Some _, None -> 1
 
+let hash f = function
+| None -> 0
+| Some x -> f x
+
 exception IsNone
 
 (** [get x] returns [y] where [x] is [Some y]. It raises IsNone
diff --git a/lib/option.mli b/lib/option.mli
index d390edb63..af8696a5e 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -31,6 +31,9 @@ val equal : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool
 (** Same as [equal], but with comparison. *)
 val compare : ('a -> 'a -> int) -> 'a option -> 'a option -> int
 
+(** Lift a hash to option types. *)
+val hash : ('a -> int) -> 'a option -> int
+
 (** [get x] returns [y] where [x] is [Some y]. It raises IsNone
     if [x] equals [None]. *)
 val get : 'a option -> 'a