From 6cd0ac247b7b6fa757a8e0b5369b6d27a0e0ebd9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 13 Nov 2015 14:41:14 +0100 Subject: 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. --- kernel/declareops.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/declareops.mli') diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 1b8700958..1d0811882 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 -- cgit v1.2.3