Hash-consing of constr could share more

 - An inductive is hidden inside case_info.
   (btw, maybe we could get rid of this ci_ind altogether,
    since the information is already in the predicate of the match)

 - Typical situation where user kn and canonical kn are initially (==)
   was not preserved by hconsing of constant / mutual_inductive

 - inductive = (mutual_inductive * int) and
   constructor = inductive * int were not properly shared

 This should fix the strange situation of Udine/PiCalc taking *more*
 vo space after the last round of hcons tweaks.

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

8 files changed, 115 insertions, 60 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index d926779430..65331b6315 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -370,35 +370,61 @@ module Hmod = Hashcons.Make(
     let hash = Hashtbl.hash
   end)
 
+module Hkn = Hashcons.Make(
+  struct
+    type t = kernel_name
+    type u = (module_path -> module_path)
+	* (dir_path -> dir_path) * (string -> string)
+    let hash_sub (hmod,hdir,hstr) (md,dir,l) =
+      (hmod md, hdir dir, hstr l)
+    let equal (mod1,dir1,l1) (mod2,dir2,l2) =
+      mod1 == mod2 && dir1 == dir2 && l1 == l2
+    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 ==. *)
+(** For [constant] and [mutual_inductive], we discriminate only on
+    the user part : having the same user part implies having the
+    same canonical part (invariant of the system). *)
 
 module Hcn = Hashcons.Make(
-  struct 
+  struct
     type t = kernel_name*kernel_name
-    type u = (module_path -> module_path)
-	* (dir_path -> dir_path) * (string -> string)
-    let hash_sub (hmod,hdir,hstr) ((md,dir,l),(mde,dire,le)) = 
-      ((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 x = Hashtbl.hash (fst x)
+    type u = kernel_name -> kernel_name
+    let hash_sub hkn (user,can) = (hkn user, hkn can)
+    let equal (user1,_) (user2,_) = user1 == user2
+    let hash (user,_) = Hashtbl.hash user
+  end)
+
+module Hind = Hashcons.Make(
+  struct
+    type t = inductive
+    type u = mutual_inductive -> mutual_inductive
+    let hash_sub hmind (mind, i) = (hmind mind, i)
+    let equal (mind1,i1) (mind2,i2) = mind1 == mind2 && i1 = i2
+    let hash = Hashtbl.hash
+  end)
+
+module Hconstruct = Hashcons.Make(
+  struct
+    type t = constructor
+    type u = inductive -> inductive
+    let hash_sub hind (ind, j) = (hind ind, j)
+    let equal (ind1,j1) (ind2,j2) = ind1 == ind2 && j1 = j2
+    let hash = Hashtbl.hash
   end)
 
-let hcons_names =
-  let hstring = Hashcons.simple_hcons Hashcons.Hstring.f () 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 (hident,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)
+let hcons_string = Hashcons.simple_hcons Hashcons.Hstring.f ()
+let hcons_ident = hcons_string
+let hcons_name = Hashcons.simple_hcons Hname.f hcons_ident
+let hcons_dirpath = Hashcons.simple_hcons Hdir.f hcons_ident
+let hcons_uid = Hashcons.simple_hcons Huniqid.f (hcons_ident,hcons_dirpath)
+let hcons_mp =
+  Hashcons.simple_hcons Hmod.f (hcons_dirpath,hcons_uid,hcons_string)
+let hcons_kn = Hashcons.simple_hcons Hkn.f (hcons_mp,hcons_dirpath,hcons_string)
+let hcons_con = Hashcons.simple_hcons Hcn.f hcons_kn
+let hcons_mind = Hashcons.simple_hcons Hcn.f hcons_kn
+let hcons_ind = Hashcons.simple_hcons Hind.f hcons_mind
+let hcons_construct = Hashcons.simple_hcons Hconstruct.f hcons_ind
 
 
 (*******)
diff --git a/kernel/names.mli b/kernel/names.mli
index 38fcebafa5..a16bed6bb4 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -197,11 +197,15 @@ val eq_egr : evaluable_global_reference ->  evaluable_global_reference
   -> bool
 
 (** Hash-consing *)
-val hcons_names :
-  (constant -> constant) *
-  (mutual_inductive -> mutual_inductive) * (dir_path -> dir_path) *
-  (name -> name) * (identifier -> identifier)
 
+val hcons_string : string -> string
+val hcons_ident : identifier -> identifier
+val hcons_name : name -> name
+val hcons_dirpath : dir_path -> dir_path
+val hcons_con : constant -> constant
+val hcons_mind : mutual_inductive -> mutual_inductive
+val hcons_ind : inductive -> inductive
+val hcons_construct : constructor -> constructor
 
 (******)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index bdffa68022..b8fe1571c8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -255,19 +255,19 @@ type global_declaration =
 
 let hcons_const_type = function
   | NonPolymorphicType t ->
-      NonPolymorphicType (hcons1_constr t)
+      NonPolymorphicType (hcons_constr t)
   | PolymorphicArity (ctx,s) ->
-      PolymorphicArity (map_rel_context hcons1_constr ctx,s)
+      PolymorphicArity (map_rel_context hcons_constr ctx,s)
 
 let hcons_const_body = function
   | Undef inl -> Undef inl
   | Def l_constr ->
     let constr = Declarations.force l_constr in
-    Def (Declarations.from_val (hcons1_constr constr))
+    Def (Declarations.from_val (hcons_constr constr))
   | OpaqueDef lc ->
     if lazy_constr_is_val lc then
       let constr = Declarations.force_opaque lc in
-      OpaqueDef (Declarations.opaque_from_val (hcons1_constr constr))
+      OpaqueDef (Declarations.opaque_from_val (hcons_constr constr))
     else OpaqueDef lc
 
 let hcons_constant_body cb =
diff --git a/kernel/term.ml b/kernel/term.ml
index a6519e226e..06c5a28ce0 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1213,10 +1213,11 @@ let rec isArity c =
 *)
 
 let array_eqeq t1 t2 =
-  Array.length t1 = Array.length t2 &&
-  let rec aux i =
-    (i = Array.length t1) || (t1.(i) == t2.(i) && aux (i + 1))
-  in aux 0
+  t1 == t2 ||
+  (Array.length t1 = Array.length t2 &&
+   let rec aux i =
+     (i = Array.length t1) || (t1.(i) == t2.(i) && aux (i + 1))
+   in aux 0)
 
 let equals_constr t1 t2 =
   match t1, t2 with
@@ -1249,6 +1250,9 @@ let equals_constr t1 t2 =
       & array_eqeq bl1 bl2
     | _ -> false
 
+(** Note that the following Make has the side effect of creating
+    once and for all the table we'll use for hash-consing all constr *)
+
 module H = Hashtbl_alt.Make(struct type t = constr let equals = equals_constr end)
 
 open Hashtbl_alt.Combine
@@ -1256,7 +1260,9 @@ open Hashtbl_alt.Combine
 (* [hcons_term hash_consing_functions constr] computes an hash-consed
    representation for [constr] using [hash_consing_functions] on
    leaves. *)
-let hcons_term (sh_sort,sh_con,sh_kn,sh_na,sh_id) =
+let hcons_term (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
+
+  (* Note : we hash-cons constr arrays *in place* *)
 
   let rec hash_term_array t =
     let accu = ref 0 in
@@ -1299,16 +1305,16 @@ let hcons_term (sh_sort,sh_con,sh_kn,sh_na,sh_id) =
 	(Evar (e, l), combinesmall 8 (combine (Hashtbl.hash e) hl))
       | Const c ->
 	(Const (sh_con c), combinesmall 9 (Hashtbl.hash c))
-      | Ind (kn,i) ->
-	(Ind (sh_kn kn, i), combinesmall 9 (combine (Hashtbl.hash kn) i))
-      | Construct ((kn,i),j) ->
-	(Construct ((sh_kn kn, i), j), combinesmall 10 (combine3 (Hashtbl.hash kn) i j))
-      | Case (ci,p,c,bl) -> (* TO DO: extract ind_kn *)
+      | Ind ((kn,i) as ind) ->
+	(Ind (sh_ind ind), combinesmall 9 (combine (Hashtbl.hash kn) i))
+      | Construct (((kn,i),j) as c)->
+	(Construct (sh_construct c), combinesmall 10 (combine3 (Hashtbl.hash kn) i j))
+      | Case (ci,p,c,bl) ->
 	let p, hp = sh_rec p
 	and c, hc = sh_rec c in
 	let bl, hbl = hash_term_array  bl in
 	let hbl = combine (combine hc hp) hbl in
-	(Case (ci, p, c, bl), combinesmall 11 hbl)
+	(Case (sh_ci ci, p, c, bl), combinesmall 11 hbl)
       | Fix (ln,(lna,tl,bl)) ->
 	let bl, hbl = hash_term_array  bl in
 	let tl, htl = hash_term_array  tl in
@@ -1337,6 +1343,8 @@ let hcons_term (sh_sort,sh_con,sh_kn,sh_na,sh_id) =
   in
   fun t -> fst (sh_rec t)
 
+(* Exported hashing fonction on constr, used mainly in plugins.
+   Appears to have slight differences from [snd (hash_term t)] above ? *)
 
 let rec hash_constr t =
   match kind_of_term t with
@@ -1385,14 +1393,34 @@ module Hsorts =
       let hash = Hashtbl.hash
     end)
 
-let hsort = Hsorts.f
+module Hcaseinfo =
+  Hashcons.Make(
+    struct
+      type t = case_info
+      type u = inductive -> inductive
+      let hash_sub hind ci = { ci with ci_ind = hind ci.ci_ind }
+      let equal ci ci' =
+	ci.ci_ind == ci'.ci_ind &&
+	ci.ci_npar = ci'.ci_npar &&
+	ci.ci_cstr_ndecls = ci'.ci_cstr_ndecls && (* we use (=) on purpose *)
+	ci.ci_pp_info = ci'.ci_pp_info  (* we use (=) on purpose *)
+      let hash = Hashtbl.hash
+    end)
+
+let hcons_sorts = Hashcons.simple_hcons Hsorts.f hcons_univ
+let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.f hcons_ind
 
-let hcons1_constr =
-  let (hcon,hkn,hdir,hname,hident) = hcons_names in
-  let hsortscci = Hashcons.simple_hcons hsort hcons1_univ in
-  hcons_term (hsortscci,hcon,hkn,hname,hident)
+let hcons_constr =
+  hcons_term
+    (hcons_sorts,
+     hcons_caseinfo,
+     hcons_construct,
+     hcons_ind,
+     hcons_con,
+     hcons_name,
+     hcons_ident)
 
-let hcons1_types = hcons1_constr
+let hcons_types = hcons_constr
 
 (*******)
 (* Type of abstract machine values *)
diff --git a/kernel/term.mli b/kernel/term.mli
index 2ec1bd9b96..c556d0a077 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -626,8 +626,8 @@ val hash_constr : constr -> int
 
 (*********************************************************************)
 
-val hcons1_constr : constr -> constr
-val hcons1_types : types -> types
+val hcons_constr : constr -> constr
+val hcons_types : types -> types
 
 (**************************************)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 7551c31d40..cc9366c116 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -94,8 +94,8 @@ let infer_declaration env dcl =
   | DefinitionEntry c ->
       let (j,cst) = infer env c.const_entry_body in
       let j =
-        {uj_val = hcons1_constr j.uj_val;
-         uj_type = hcons1_constr j.uj_type} in
+        {uj_val = hcons_constr j.uj_val;
+         uj_type = hcons_constr j.uj_type} in
       let (typ,cst) = constrain_type env j cst c.const_entry_type in
       let def =
 	if c.const_entry_opaque
@@ -105,7 +105,7 @@ let infer_declaration env dcl =
       def, typ, cst
   | ParameterEntry (t,nl) ->
       let (j,cst) = infer env t in
-      let t = hcons1_constr (Typeops.assumption_of_judgment env j) in
+      let t = hcons_constr (Typeops.assumption_of_judgment env j) in
       Undef nl, NonPolymorphicType t, cst
 
 let global_vars_set_constant_type env = function
diff --git a/kernel/univ.ml b/kernel/univ.ml
index ba14771aab..96990d696c 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -858,9 +858,6 @@ module Huniv =
       let hash = Hashtbl.hash
     end)
 
-let hcons1_univlevel =
-  let _,_,hdir,_,_ = Names.hcons_names in
-  Hashcons.simple_hcons Hunivlevel.f hdir
-
-let hcons1_univ = Hashcons.simple_hcons Huniv.f hcons1_univlevel
+let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.f Names.hcons_dirpath
+let hcons_univ = Hashcons.simple_hcons Huniv.f hcons_univlevel
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 63f07fc998..0dfa4a5e33 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -103,5 +103,5 @@ val dump_universes :
 
 (** {6 Hash-consing } *)
 
-val hcons1_univlevel : universe_level -> universe_level
-val hcons1_univ : universe -> universe
+val hcons_univlevel : universe_level -> universe_level
+val hcons_univ : universe -> universe