aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-03-03 13:46:59 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-03-03 15:17:36 +0100
commit49a764bd81ac1b21130d54a1808ce95b9992a36d (patch)
treea3763c01ea07c1a33b8464c61de4bbcbc060c4f3 /kernel/constr.ml
parent78fab59413d2861c6414ccda47e2d70f25814523 (diff)
Removing generic hashes in kernel.
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r--kernel/constr.ml65
1 files changed, 34 insertions, 31 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