diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-13 14:41:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-15 18:51:12 +0100 |
| commit | 6cd0ac247b7b6fa757a8e0b5369b6d27a0e0ebd9 (patch) | |
| tree | 8eca1824a25a12cf56dd473fc9f8871ae98be1e2 /kernel/names.mli | |
| parent | 73c9ad1ff19915fbaf053119c5498ff1314e92e3 (diff) | |
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.
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 77139f1c3..c5a7d8f3c 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} *) |