From 9f81b58551958aea2a85bcdd0cc3f88bf4634c92 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 29 Jul 2015 01:26:00 +0200 Subject: Fixing bug #4289 (hash-consing only user part of constant not compatible with a unique bound module name counter which is not synchronous with the backtracking). We changed hash-consing of kernel name pairs to a purely memory management issue, not trying to exploit logical properties such as "syntactically equal user names have syntactically same canonical names" (which is true in a given logical session, but not in memory, at least because of residual values after backtracking). --- kernel/names.ml | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) (limited to 'kernel/names.ml') diff --git a/kernel/names.ml b/kernel/names.ml index f217c932c..19fe62ec8 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -453,6 +453,9 @@ module KNset = KNmap.Set - when user and canonical parts differ, we cannot be in a section anymore, hence the dirpath must be empty - two pairs with the same user part should have the same canonical part + in a given environment (though with backtracking, the hash-table can + contains pairs with same user part but different canonical part from + a previous state of the session) Note: since most of the time the canonical and user parts are equal, we handle this case with a particular constructor to spare some memory *) @@ -504,7 +507,7 @@ module KerPair = struct let debug_print kp = str (debug_to_string kp) (** For ordering kernel pairs, both user or canonical parts may make - sense, according to your needs : user for the environments, canonical + sense, according to your needs: user for the environments, canonical for other uses (ex: non-logical things). *) module UserOrd = struct @@ -521,16 +524,18 @@ module KerPair = struct let hash x = KerName.hash (canonical x) end - (** Default comparison is on the canonical part *) + (** Default (logical) comparison is on the canonical part *) let equal = CanOrd.equal - (** Hash-consing : we discriminate only on the user part, since having - the same user part implies having the same canonical part - (invariant of the system). *) + (** 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 (kn, _) -> KerName.hash kn + | Dual (knu, knc) -> + Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc) module Self_Hashcons = struct @@ -539,7 +544,12 @@ module KerPair = struct let hashcons hkn = function | Same kn -> Same (hkn kn) | Dual (knu,knc) -> make (hkn knu) (hkn knc) - let equal x y = (user x) == (user y) + let equal x y = (* physical comparison on subterms *) + x == y || + match x,y with + | Same x, Same y -> x == y + | Dual (ux,cx), Dual (uy,cy) -> ux == uy && cx == cy + | (Same _ | Dual _), _ -> false let hash = hash end -- cgit v1.2.3