More twicks on hash-consing

 - When hash-consing, seeing ident as having string as sub-structure
   induces a penalty: two searchs are done in two tables
   (one for string, one for id).
   We simply say now that the hcons function for ident is the one
   for string

 - use more == during hash-consing of Names.uniq_ident and
   Names.module_path

 - clarification concerning hash-cons of Names.constant and
   Names.mutual_inductive: we only hash-cons the canonical part,
   but == could be used nonetheless on the obtained pair. Simply
   note that canonical_con of hash-consed constants will produce
   kernel_names that may be (=) but not (==).

 - Code cleanup : no direct use of string hash-consing apart in Names,
   we hence simplify hcons_names

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14464 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 15 insertions, 20 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 4466f558f9..c65e624c21 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -31,16 +31,6 @@ let id_of_string s = check_ident_soft s; String.copy s
 
 let string_of_id id = String.copy id
 
-(* Hash-consing of identifier *)
-module Hident = Hashcons.Make(
-  struct
-    type t = string
-    type u = string -> string
-    let hash_sub hstr id = hstr id
-    let equal id1 id2 = id1 == id2
-    let hash = Hashtbl.hash
-  end)
-
 module IdOrdered =
   struct
     type t = identifier
@@ -359,7 +349,7 @@ module Huniqid = Hashcons.Make(
     type t = uniq_ident
     type u = (string -> string) * (dir_path -> dir_path)
     let hash_sub (hstr,hdir) (n,s,dir) = (n,hstr s,hdir dir)
-    let equal (n1,s1,dir1) (n2,s2,dir2) = n1 = n2 & s1 = s2 & dir1 == dir2
+    let equal (n1,s1,dir1) (n2,s2,dir2) = n1 = n2 && s1 == s2 && dir1 == dir2
     let hash = Hashtbl.hash
   end)
 
@@ -375,12 +365,18 @@ module Hmod = Hashcons.Make(
     let rec equal d1 d2 = match (d1,d2) with
       | MPfile dir1, MPfile dir2 -> dir1 == dir2
       | MPbound m1, MPbound m2 -> m1 == m2
-      | MPdot (mod1,l1), MPdot (mod2,l2) -> equal mod1 mod2 & l1 = l2
+      | MPdot (mod1,l1), MPdot (mod2,l2) -> l1 == l2 && equal mod1 mod2
       | _ -> false
     let hash = Hashtbl.hash
   end)
 
 
+(** For [constant] and [mutual_inductive], we hash-cons only the user part.
+    If two constants have equal user parts (according to =), then their
+    canonical parts are also equal (invariant of the system), and then
+    the hash-consed versions of these constants will be equal according
+    to ==. *)
+
 module Hcn = Hashcons.Make(
   struct 
     type t = kernel_name*kernel_name
@@ -390,19 +386,19 @@ module Hcn = Hashcons.Make(
       ((hmod md, hdir dir, hstr l),(hmod mde, hdir dire, hstr le))
     let equal ((mod1,dir1,l1),_) ((mod2,dir2,l2),_) =
       mod1 == mod2 && dir1 == dir2 && l1 == l2
-    let hash = Hashtbl.hash
+    let hash x = Hashtbl.hash (fst x)
   end)
 
 let hcons_names () =
   let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () in
-  let hident = Hashcons.simple_hcons Hident.f hstring in
+  let hident = hstring in
   let hname = Hashcons.simple_hcons Hname.f hident in
   let hdir = Hashcons.simple_hcons Hdir.f hident in
   let huniqid = Hashcons.simple_hcons Huniqid.f (hstring,hdir) in
   let hmod = Hashcons.simple_hcons Hmod.f (hdir,huniqid,hstring) in
   let hmind = Hashcons.simple_hcons Hcn.f (hmod,hdir,hstring) in
   let hcn = Hashcons.simple_hcons Hcn.f (hmod,hdir,hstring) in
-  (hcn,hmind,hdir,hname,hident,hstring)
+  (hcn,hmind,hdir,hname,hident)
 
 
 (*******)
diff --git a/kernel/names.mli b/kernel/names.mli
index 1f9f65b5cd..62d2040c28 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -200,7 +200,7 @@ val eq_egr : evaluable_global_reference ->  evaluable_global_reference
 val hcons_names : unit ->
   (constant -> constant) *
   (mutual_inductive -> mutual_inductive) * (dir_path -> dir_path) *
-  (name -> name) * (identifier -> identifier) * (string -> string)
+  (name -> name) * (identifier -> identifier)
 
 
 (******)
diff --git a/kernel/term.ml b/kernel/term.ml
index b4ddbfc8c7..3281154202 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1401,7 +1401,7 @@ module Hsorts =
 
 let hsort = Hsorts.f
 
-let hcons_constr (hcon,hkn,hdir,hname,hident,hstr) =
+let hcons_constr (hcon,hkn,hdir,hname,hident) =
   let hsortscci = Hashcons.simple_hcons hsort hcons1_univ in
   let hcci = hcons_term (hsortscci,hcon,hkn,hname,hident) in
   let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in
diff --git a/kernel/term.mli b/kernel/term.mli
index 68fbd1807e..aa9a55abc0 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -631,8 +631,7 @@ val hcons_constr:
   (mutual_inductive -> mutual_inductive) *
   (dir_path -> dir_path) *
   (name -> name) *
-  (identifier -> identifier) *
-  (string -> string)
+  (identifier -> identifier)
   ->
     (constr -> constr) *
     (types -> types)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 32e08abd82..c68021a209 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -863,7 +863,7 @@ let hcons1_univlevel =
      since it creates internal hash-tables.
      We could/should probably share the other calls to [hcons_names]
      in Term and Declare *)
-  let _,_,hdir,_,_,_ = Names.hcons_names() in
+  let _,_,hdir,_,_ = Names.hcons_names() in
   Hashcons.simple_hcons Hunivlevel.f hdir
 
 let hcons1_univ = Hashcons.simple_hcons Huniv.f hcons1_univlevel