Hashconsing modules.

Modules inserted into the environment were not hashconsed, leading to an
important redundancy, especially in module signatures that are always fully
expanded.

This patch divides by two the size and memory consumption of module-heavy
files by hashconsing modules before putting them in the environment. Note
that this is not a real hashconsing, in the sense that we only hashcons the
inner terms contained in the modules, that are only mapped over. Compilation
time should globally decrease, even though some files definining a lot of
modules may see their compilation time increase.

Some remaining overhead may persist, as for instance module inclusion is not
hashconsed.

4 files changed, 90 insertions, 0 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index d9bd5c445..f8b5981fa 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -308,3 +308,88 @@ let string_of_side_effect { Entries.eff } = match eff with
   | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")"
   | Entries.SEscheme (cl,_) ->
       "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")"
+
+(** Hashconsing of modules *)
+
+let hcons_functorize hty he hself f = match f with
+| NoFunctor e ->
+  let e' = he e in
+  if e == e' then f else NoFunctor e'
+| MoreFunctor (mid, ty, nf) ->
+  (** FIXME *)
+  let mid' = mid in
+  let ty' = hty ty in
+  let nf' = hself nf in
+  if mid == mid' && ty == ty' && nf == nf' then f
+  else MoreFunctor (mid, ty', nf')
+
+let hcons_module_alg_expr me = me
+
+let rec hcons_structure_field_body sb = match sb with
+| SFBconst cb ->
+  let cb' = hcons_const_body cb in
+  if cb == cb' then sb else SFBconst cb'
+| SFBmind mib ->
+  let mib' = hcons_mind mib in
+  if mib == mib' then sb else SFBmind mib'
+| SFBmodule mb ->
+  let mb' = hcons_module_body mb in
+  if mb == mb' then sb else SFBmodule mb'
+| SFBmodtype mb ->
+  let mb' = hcons_module_body mb in
+  if mb == mb' then sb else SFBmodtype mb'
+
+and hcons_structure_body sb =
+  (** FIXME *)
+  let map (l, sfb as fb) =
+    let l' = Names.Label.hcons l in
+    let sfb' = hcons_structure_field_body sfb in
+    if l == l' && sfb == sfb' then fb else (l', sfb')
+  in
+  List.smartmap map sb
+
+and hcons_module_signature ms =
+  hcons_functorize hcons_module_body hcons_structure_body hcons_module_signature ms
+
+and hcons_module_expression me =
+  hcons_functorize hcons_module_body hcons_module_alg_expr hcons_module_expression me
+
+and hcons_module_implementation mip = match mip with
+| Abstract -> Abstract
+| Algebraic me ->
+  let me' = hcons_module_expression me in
+  if me == me' then mip else Algebraic me'
+| Struct ms ->
+  let ms' = hcons_module_signature ms in
+  if ms == ms' then mip else Struct ms
+| FullStruct -> FullStruct
+
+and hcons_module_body mb =
+  let mp' = mb.mod_mp in
+  let expr' = hcons_module_implementation mb.mod_expr in
+  let type' = hcons_module_signature mb.mod_type in
+  let type_alg' = mb.mod_type_alg in
+  let constraints' = Univ.hcons_universe_context_set mb.mod_constraints in
+  let delta' = mb.mod_delta in
+  let retroknowledge' = mb.mod_retroknowledge in
+
+  if
+    mb.mod_mp == mp' &&
+    mb.mod_expr == expr' &&
+    mb.mod_type == type' &&
+    mb.mod_type_alg == type_alg' &&
+    mb.mod_constraints == constraints' &&
+    mb.mod_delta == delta' &&
+    mb.mod_retroknowledge == retroknowledge'
+  then mb
+  else {
+    mod_mp = mp';
+    mod_expr = expr';
+    mod_type = type';
+    mod_type_alg = type_alg';
+    mod_constraints = constraints';
+    mod_delta = delta';
+    mod_retroknowledge = retroknowledge';
+  }
+
+and hcons_module_type_body mtb = hcons_module_body mtb
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 86ba29b8b..ad2b5d0a6 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -77,3 +77,4 @@ val inductive_context : mutual_inductive_body -> universe_context
 
 val hcons_const_body : constant_body -> constant_body
 val hcons_mind : mutual_inductive_body -> mutual_inductive_body
+val hcons_module_body : module_body -> module_body
diff --git a/kernel/names.mli b/kernel/names.mli
index 72dff03be..1e79f4dde 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -160,6 +160,8 @@ sig
   module Set : Set.S with type elt = t
   module Map : Map.ExtS with type key = t and module Set := Set
 
+  val hcons : t -> t
+
 end
 
 (** {6 Unique names for bound modules} *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0926d35f6..62753962c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -561,6 +561,7 @@ let add_mind dir l mie senv =
 let add_modtype l params_mte inl senv =
   let mp = MPdot(senv.modpath, l) in
   let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte  in
+  let mtb = Declareops.hcons_module_body mtb in
   let senv' = add_field (l,SFBmodtype mtb) MT senv in
   mp, senv'
 
@@ -581,6 +582,7 @@ let full_add_module_type mp mt senv =
 let add_module l me inl senv =
   let mp = MPdot(senv.modpath, l) in
   let mb = Mod_typing.translate_module senv.env mp inl me in
+  let mb = Declareops.hcons_module_body mb in
   let senv' = add_field (l,SFBmodule mb) M senv in
   let senv'' =
     if Modops.is_functor mb.mod_type then senv'