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.

1 files changed, 2 insertions, 0 deletions

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'