Removing generic hashes in kernel.

3 files changed, 92 insertions, 39 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 61718a7f7..826c7f643 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -715,37 +715,40 @@ let rec hash t =
 and hash_term_array t =
   Array.fold_left (fun acc t -> combine (hash t) acc) 0 t
 
-module Hcaseinfo =
-  Hashcons.Make(
-    struct
-      type t = case_info
-      type u = inductive -> inductive
-      let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind }
-      let pp_info_equal info1 info2 =
-        Int.equal info1.ind_nargs info2.ind_nargs &&
-        info1.style == info2.style
-      let equal ci ci' =
-	ci.ci_ind == ci'.ci_ind &&
-	Int.equal ci.ci_npar ci'.ci_npar &&
-	Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *)
-	pp_info_equal ci.ci_pp_info ci'.ci_pp_info  (* we use (=) on purpose *)
-      open Hashset.Combine
-      let hash_pp_info info =
-        let h = match info.style with
-        | LetStyle -> 0
-        | IfStyle -> 1
-        | LetPatternStyle -> 2
-        | MatchStyle -> 3
-        | RegularStyle -> 4
-        in
-        combine info.ind_nargs h
-      let hash ci =
-        let h1 = ind_hash ci.ci_ind in
-        let h2 = Int.hash ci.ci_npar in
-        let h3 = Array.fold_left combine 0 ci.ci_cstr_ndecls in
-        let h4 = hash_pp_info ci.ci_pp_info in
-        combine4 h1 h2 h3 h4
-    end)
+module CaseinfoHash =
+struct
+  type t = case_info
+  type u = inductive -> inductive
+  let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind }
+  let pp_info_equal info1 info2 =
+    Int.equal info1.ind_nargs info2.ind_nargs &&
+    info1.style == info2.style
+  let equal ci ci' =
+    ci.ci_ind == ci'.ci_ind &&
+    Int.equal ci.ci_npar ci'.ci_npar &&
+    Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *)
+    pp_info_equal ci.ci_pp_info ci'.ci_pp_info  (* we use (=) on purpose *)
+  open Hashset.Combine
+  let hash_pp_info info =
+    let h = match info.style with
+    | LetStyle -> 0
+    | IfStyle -> 1
+    | LetPatternStyle -> 2
+    | MatchStyle -> 3
+    | RegularStyle -> 4
+    in
+    combine info.ind_nargs h
+  let hash ci =
+    let h1 = ind_hash ci.ci_ind in
+    let h2 = Int.hash ci.ci_npar in
+    let h3 = Array.fold_left combine 0 ci.ci_cstr_ndecls in
+    let h4 = hash_pp_info ci.ci_pp_info in
+    combine4 h1 h2 h3 h4
+end
+
+module Hcaseinfo = Hashcons.Make(CaseinfoHash)
+
+let case_info_hash = CaseinfoHash.hash
 
 let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind
 
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 261b6bfb4..858af97b6 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -236,6 +236,7 @@ val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool
 (** {6 Hashconsing} *)
 
 val hash : constr -> int
+val case_info_hash : case_info -> int
 
 (*********************************************************************)
 
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index c431d1075..7dcaf9b13 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -12,6 +12,7 @@
 
 (* This file manages the table of global symbols for the bytecode machine *)
 
+open Util
 open Names
 open Term
 open Context
@@ -54,10 +55,58 @@ let set_global v =
 
 (* table pour les structured_constant et les annotations des switchs *)
 
-let str_cst_tbl = Hashtbl.create 31
-    (* (structured_constant * int) Hashtbl.t*)
-
-let annot_tbl = Hashtbl.create 31
+let rec eq_structured_constant c1 c2 = match c1, c2 with
+| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
+| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
+| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
+| Const_bn (t1, a1), Const_bn (t2, a2) ->
+  Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
+| _ -> false
+
+let rec hash_structured_constant c =
+  let open Hashset.Combine in
+  match c with
+  | Const_sorts s -> combinesmall 1 (Sorts.hash s)
+  | Const_ind i -> combinesmall 2 (ind_hash i)
+  | Const_b0 t -> combinesmall 3 (Int.hash t)
+  | Const_bn (t, a) ->
+    let fold h c = combine h (hash_structured_constant c) in
+    let h = Array.fold_left fold 0 a in
+    combinesmall 4 (combine (Int.hash t) h)
+
+module SConstTable = Hashtbl.Make (struct
+  type t = structured_constant
+  let equal = eq_structured_constant
+  let hash = hash_structured_constant
+end)
+
+let eq_annot_switch asw1 asw2 =
+  let eq_ci ci1 ci2 =
+    eq_ind ci1.ci_ind ci2.ci_ind &&
+    Int.equal ci1.ci_npar ci2.ci_npar &&
+    Array.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls
+  in
+  let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in
+  eq_ci asw1.ci asw2.ci &&
+  Array.equal eq_rlc asw1.rtbl asw2.rtbl &&
+  (asw1.tailcall : bool) == asw2.tailcall
+
+let hash_annot_switch asw =
+  let open Hashset.Combine in
+  let h1 = Constr.case_info_hash asw.ci in
+  let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
+  let h3 = if asw.tailcall then 1 else 0 in
+  combine3 h1 h2 h3
+
+module AnnotTable = Hashtbl.Make (struct
+  type t = annot_switch
+  let equal = eq_annot_switch
+  let hash = hash_annot_switch
+end)
+
+let str_cst_tbl : int SConstTable.t = SConstTable.create 31
+
+let annot_tbl : int AnnotTable.t = AnnotTable.create 31
     (* (annot_switch * int) Hashtbl.t  *)
 
 (*************************************************************)
@@ -80,17 +129,17 @@ let key rk =
    dans la table global, rend sa position dans la table *)
 
 let slot_for_str_cst key =
-  try Hashtbl.find str_cst_tbl key
+  try SConstTable.find str_cst_tbl key
   with Not_found ->
     let n = set_global (val_of_str_const key) in
-    Hashtbl.add str_cst_tbl key n;
+    SConstTable.add str_cst_tbl key n;
     n
 
 let slot_for_annot key =
-  try Hashtbl.find annot_tbl key
+  try AnnotTable.find annot_tbl key
   with Not_found ->
     let n =  set_global (val_of_annot_switch key) in
-    Hashtbl.add annot_tbl key n;
+    AnnotTable.add annot_tbl key n;
     n
 
 let rec slot_for_getglobal env kn =