From 1ee23d71dadd6211c36afe8d2891b7170535cd62 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 30 Jul 2015 15:55:24 +0200 Subject: Followup of 9f81b58551. The hash function exported by the interface ought to respect the equality. Therefore, we only use the syntactic hash for the hashconsing module while using the canonical hash in the API. --- kernel/names.ml | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index 19fe62ec8..ae2b3b638 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -524,18 +524,9 @@ module KerPair = struct let hash x = KerName.hash (canonical x) end - (** Default (logical) comparison is on the canonical part *) + (** Default (logical) comparison and hash is on the canonical part *) let equal = CanOrd.equal - - (** Hash-consing (despite having the same user part implies having - the same canonical part is a logical invariant of the system, it - is not necessarily an invariant in memory, so we treat kernel - names as they are syntactically for hash-consing) *) - - let hash = function - | Same kn -> KerName.hash kn - | Dual (knu, knc) -> - Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc) + let hash = CanOrd.hash module Self_Hashcons = struct @@ -550,7 +541,14 @@ module KerPair = struct | Same x, Same y -> x == y | Dual (ux,cx), Dual (uy,cy) -> ux == uy && cx == cy | (Same _ | Dual _), _ -> false - let hash = hash + (** Hash-consing (despite having the same user part implies having + the same canonical part is a logical invariant of the system, it + is not necessarily an invariant in memory, so we treat kernel + names as they are syntactically for hash-consing) *) + let hash = function + | Same kn -> KerName.hash kn + | Dual (knu, knc) -> + Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc) end module HashKP = Hashcons.Make(Self_Hashcons) -- cgit v1.2.3