Hash-consing of mutual_inductive_body (and Univ.constraints)

 Inductive definitions aren't that big, but they may contain some
 constr (in types, rel_context, etc), hence if we hash-cons the
 constr in Definition but not these ones, we may loose some sharing.

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

6 files changed, 132 insertions, 55 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index f092c8261..1a84b9876 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -83,11 +83,6 @@ type constant_def =
   | Def of constr_substituted
   | OpaqueDef of lazy_constr
 
-let subst_constant_def sub = function
-  | Undef inl -> Undef inl
-  | Def c -> Def (subst_constr_subst sub c)
-  | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
-
 type constant_body = {
     const_hyps : section_context; (* New: younger hyp at top *)
     const_body : constant_def;
@@ -108,8 +103,7 @@ let is_opaque cb = match cb.const_body with
   | OpaqueDef _ -> true
   | Undef _ | Def _ -> false
 
-(*s Inductive types (internal representation with redundant
-    information). *)
+(* Substitutions of [constant_body] *)
 
 let subst_rel_declaration sub (id,copt,t as x) =
   let copt' = Option.smartmap (subst_mps sub) copt in
@@ -118,6 +112,69 @@ let subst_rel_declaration sub (id,copt,t as x) =
 
 let subst_rel_context sub = list_smartmap (subst_rel_declaration sub)
 
+(* TODO: these substitution functions could avoid duplicating things
+   when the substitution have preserved all the fields *)
+
+let subst_const_type sub arity =
+  if is_empty_subst sub then arity
+  else match arity with
+    | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
+    | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s)
+
+let subst_const_def sub = function
+  | Undef inl -> Undef inl
+  | Def c -> Def (subst_constr_subst sub c)
+  | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
+
+let subst_const_body sub cb = {
+  const_hyps = (assert (cb.const_hyps=[]); []);
+  const_body = subst_const_def sub cb.const_body;
+  const_type = subst_const_type sub cb.const_type;
+  const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
+  const_constraints = cb.const_constraints}
+
+(* Hash-consing of [constant_body] *)
+
+let hcons_rel_decl ((n,oc,t) as d) =
+  let n' = hcons_name n
+  and oc' = Option.smartmap hcons_constr oc
+  and t' = hcons_types t
+  in if n' == n && oc' == oc && t' == t then d else (n',oc',t')
+
+let hcons_rel_context l = list_smartmap hcons_rel_decl l
+
+let hcons_polyarity ar =
+  { poly_param_levels =
+      list_smartmap (Option.smartmap hcons_univ) ar.poly_param_levels;
+    poly_level = hcons_univ ar.poly_level }
+
+let hcons_const_type = function
+  | NonPolymorphicType t ->
+    NonPolymorphicType (hcons_constr t)
+  | PolymorphicArity (ctx,s) ->
+    PolymorphicArity (hcons_rel_context ctx, hcons_polyarity s)
+
+let hcons_const_def = function
+  | Undef inl -> Undef inl
+  | Def l_constr ->
+    let constr = force l_constr in
+    Def (from_val (hcons_constr constr))
+  | OpaqueDef lc ->
+    if lazy_constr_is_val lc then
+      let constr = force_opaque lc in
+      OpaqueDef (opaque_from_val (hcons_constr constr))
+    else OpaqueDef lc
+
+let hcons_const_body cb =
+  { cb with
+    const_body = hcons_const_def cb.const_body;
+    const_type = hcons_const_type cb.const_type;
+    const_constraints = hcons_constraints cb.const_constraints }
+
+
+(*s Inductive types (internal representation with redundant
+    information). *)
+
 type recarg =
   | Norec
   | Mrec of inductive
@@ -256,22 +313,7 @@ type mutual_inductive_body = {
 
   }
 
-let subst_arity sub arity =
-  if is_empty_subst sub then arity
-  else match arity with
-    | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
-    | PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s)
-	
-(* TODO: should be changed to non-coping after Term.subst_mps *)
-let subst_const_body sub cb = {
-  const_hyps = (assert (cb.const_hyps=[]); []);
-  const_body = subst_constant_def sub cb.const_body;
-  const_type = subst_arity sub cb.const_type;
-  const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
-  (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*)
-  const_constraints = cb.const_constraints}
-
-let subst_arity sub = function
+let subst_indarity sub = function
 | Monomorphic s ->
     Monomorphic {
       mind_user_arity = subst_mps sub s.mind_user_arity;
@@ -285,7 +327,7 @@ let subst_mind_packet sub mbp =
     mind_typename = mbp.mind_typename;
     mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc;
     mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
-    mind_arity = subst_arity sub mbp.mind_arity;
+    mind_arity = subst_indarity sub mbp.mind_arity;
     mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc;
     mind_nrealargs = mbp.mind_nrealargs;
     mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt;
@@ -295,7 +337,6 @@ let subst_mind_packet sub mbp =
     mind_nb_args = mbp.mind_nb_args;
     mind_reloc_tbl = mbp.mind_reloc_tbl }
 
-
 let subst_mind sub mib =
   { mind_record = mib.mind_record ;
     mind_finite = mib.mind_finite ;
@@ -308,6 +349,26 @@ let subst_mind sub mib =
     mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
     mind_constraints = mib.mind_constraints  }
 
+let hcons_indarity = function
+  | Monomorphic a ->
+    Monomorphic { mind_user_arity = hcons_constr a.mind_user_arity;
+		  mind_sort = hcons_sorts a.mind_sort }
+  | Polymorphic a -> Polymorphic (hcons_polyarity a)
+
+let hcons_mind_packet oib =
+ { oib with
+   mind_typename = hcons_ident oib.mind_typename;
+   mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
+   mind_arity = hcons_indarity oib.mind_arity;
+   mind_consnames = array_smartmap hcons_ident oib.mind_consnames;
+   mind_user_lc = array_smartmap hcons_types oib.mind_user_lc;
+   mind_nf_lc = array_smartmap hcons_types oib.mind_nf_lc }
+
+let hcons_mind mib =
+  { mib with
+    mind_packets = array_smartmap hcons_mind_packet mib.mind_packets;
+    mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
+    mind_constraints = hcons_constraints mib.mind_constraints }
 
 (*s Modules: signature component specifications, module types, and
   module declarations *)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index ebedd17e6..5b800edec 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -62,8 +62,6 @@ type constant_def =
   | Def of constr_substituted
   | OpaqueDef of lazy_constr
 
-val subst_constant_def : substitution -> constant_def -> constant_def
-
 type constant_body = {
     const_hyps : section_context; (** New: younger hyp at top *)
     const_body : constant_def;
@@ -71,6 +69,7 @@ type constant_body = {
     const_body_code : to_patch_substituted;
     const_constraints : constraints }
 
+val subst_const_def : substitution -> constant_def -> constant_def
 val subst_const_body : substitution -> constant_body -> constant_body
 
 (** Is there a actual body in const_body or const_body_opaque ? *)
@@ -233,3 +232,13 @@ and module_type_body =
       typ_constraints : constraints;
       (** quotiented set of equivalent constant and inductive name  *)
       typ_delta :delta_resolver}
+
+
+(** Hash-consing *)
+
+(** Here, strictly speaking, we don't perform true hash-consing
+    of the structure, but simply hash-cons all inner constr
+    and other known elements *)
+
+val hcons_const_body : constant_body -> constant_body
+val hcons_mind : mutual_inductive_body -> mutual_inductive_body
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0e5af7737..e5b8412ec 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -255,37 +255,14 @@ type global_declaration =
   | ConstantEntry of constant_entry
   | GlobalRecipe of Cooking.recipe
 
-let hcons_const_type = function
-  | NonPolymorphicType t ->
-      NonPolymorphicType (hcons_constr t)
-  | PolymorphicArity (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 (hcons_constr constr))
-  | OpaqueDef lc ->
-    if lazy_constr_is_val lc then
-      let constr = Declarations.force_opaque lc in
-      OpaqueDef (Declarations.opaque_from_val (hcons_constr constr))
-    else OpaqueDef lc
-
-let hcons_constant_body cb =
-  { cb with
-    const_body = hcons_const_body cb.const_body;
-    const_type = hcons_const_type cb.const_type }
-
 let add_constant dir l decl senv =
   check_label l senv;
   let kn = make_con senv.modinfo.modpath dir l in
-  let cb =
-    match decl with
-      | ConstantEntry ce -> translate_constant senv.env kn ce
-      | GlobalRecipe r ->
-	  let cb = translate_recipe senv.env kn r in
-	    if dir = empty_dirpath then hcons_constant_body cb else cb
+  let cb = match decl with
+    | ConstantEntry ce -> translate_constant senv.env kn ce
+    | GlobalRecipe r ->
+      let cb = translate_recipe senv.env kn r in
+      if dir = empty_dirpath then hcons_const_body cb else cb
   in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
   let senv'' = match cb.const_body with
@@ -310,6 +287,7 @@ let add_mind dir l mie senv =
        all labels *)
   let kn = make_mind senv.modinfo.modpath dir l in
   let mib = translate_mind senv.env kn mie in
+  let mib = if mib.mind_hyps <> [] then mib else hcons_mind mib in
   let senv' = add_field (l,SFBmind mib) (I kn) senv in
   kn, senv'
 
diff --git a/kernel/term.mli b/kernel/term.mli
index c556d0a07..7992c0bab 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -626,6 +626,7 @@ val hash_constr : constr -> int
 
 (*********************************************************************)
 
+val hcons_sorts : sorts -> sorts
 val hcons_constr : constr -> constr
 val hcons_types : types -> types
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 96990d696..7f458f64c 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -861,3 +861,30 @@ module Huniv =
 let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.f Names.hcons_dirpath
 let hcons_univ = Hashcons.simple_hcons Huniv.f hcons_univlevel
 
+module Hconstraint =
+  Hashcons.Make(
+    struct
+      type t = univ_constraint
+      type u = universe_level -> universe_level
+      let hash_sub hul (l1,k,l2) = (hul l1, k, hul l2)
+      let equal (l1,k,l2) (l1',k',l2') =
+	l1 == l1' && k = k' && l2 == l2'
+      let hash = Hashtbl.hash
+    end)
+
+module Hconstraints =
+  Hashcons.Make(
+    struct
+      type t = constraints
+      type u = univ_constraint -> univ_constraint
+      let hash_sub huc s =
+	Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
+      let equal s s' =
+	list_for_all2eq (==)
+	  (Constraint.elements s)
+	  (Constraint.elements s')
+      let hash = Hashtbl.hash
+    end)
+
+let hcons_constraint = Hashcons.simple_hcons Hconstraint.f hcons_univlevel
+let hcons_constraints = Hashcons.simple_hcons Hconstraints.f hcons_constraint
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 0dfa4a5e3..a55775372 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -105,3 +105,4 @@ val dump_universes :
 
 val hcons_univlevel : universe_level -> universe_level
 val hcons_univ : universe -> universe
+val hcons_constraints : constraints -> constraints