From 908dcd613b12645f3b62bf44c2696b80a0b16940 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 16:46:42 +0100 Subject: Avoid type checking private_constants (side_eff) again during Qed (#4357). Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large. --- kernel/declareops.ml | 18 ++++-------------- 1 file changed, 4 insertions(+), 14 deletions(-) (limited to 'kernel/declareops.ml') diff --git a/kernel/declareops.ml b/kernel/declareops.ml index a7051d5c13..248504c1b1 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -304,17 +304,7 @@ let hcons_mind mib = (** {6 Stm machinery } *) -let string_of_side_effect = function - | SEsubproof (c,_,_) -> Names.string_of_con c - | SEscheme (cl,_) -> - String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) -type side_effects = side_effect list -let no_seff = ([] : side_effects) -let iter_side_effects f l = List.iter f (List.rev l) -let fold_side_effects f a l = List.fold_left f a l -let uniquize_side_effects l = List.rev (CList.uniquize (List.rev l)) -let union_side_effects l1 l2 = l1 @ l2 -let flatten_side_effects l = List.flatten l -let side_effects_of_list l = l -let cons_side_effects x l = x :: l -let side_effects_is_empty = List.is_empty +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) ^ ")" -- cgit v1.2.3 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.ml | 85 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 85 insertions(+) (limited to 'kernel/declareops.ml') diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 248504c1b1..73cfd01221 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 -- cgit v1.2.3 From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- kernel/declareops.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'kernel/declareops.ml') diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 73cfd01221..803df78270 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -391,5 +391,3 @@ and hcons_module_body mb = mod_delta = delta'; mod_retroknowledge = retroknowledge'; } - -and hcons_module_type_body mtb = hcons_module_body mtb -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- kernel/declareops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/declareops.ml') diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 73cfd01221..6239d3c8d6 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -254,7 +254,7 @@ let subst_mind_body sub mib = mind_nparams = mib.mind_nparams; mind_nparams_rec = mib.mind_nparams_rec; mind_params_ctxt = - Context.map_rel_context (subst_mps sub) mib.mind_params_ctxt; + Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_polymorphic = mib.mind_polymorphic; mind_universes = mib.mind_universes; -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/declareops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/declareops.ml') diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 248504c1b1..d9bd5c445e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- kernel/declareops.ml | 35 ++++++++++++++++++++++++++--------- 1 file changed, 26 insertions(+), 9 deletions(-) (limited to 'kernel/declareops.ml') diff --git a/kernel/declareops.ml b/kernel/declareops.ml index f73eea030f..cb67135ad4 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -87,10 +87,18 @@ let is_opaque cb = match cb.const_body with (** {7 Constant substitutions } *) -let subst_rel_declaration sub (id,copt,t as x) = - let copt' = Option.smartmap (subst_mps sub) copt in - let t' = subst_mps sub t in - if copt == copt' && t == t' then x else (id,copt',t') +let subst_rel_declaration sub x = + let open Context.Rel.Declaration in + match x with + | LocalAssum (id,t) -> + let t' = subst_mps sub t in + if t == t' then x + else LocalAssum (id,t') + | LocalDef (id,v,t) -> + let v' = subst_mps sub v in + let t' = subst_mps sub t in + if v == v' && t == t' then x + else LocalDef (id,v',t') let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) @@ -140,11 +148,20 @@ let subst_const_body sub cb = share internal fields (e.g. constr), and not the records themselves. But would it really bring substantial gains ? *) -let hcons_rel_decl ((n,oc,t) as d) = - let n' = Names.Name.hcons n - and oc' = Option.smartmap Term.hcons_constr oc - and t' = Term.hcons_types t - in if n' == n && oc' == oc && t' == t then d else (n',oc',t') +let hcons_rel_decl d = + let open Context.Rel.Declaration in + match d with + | LocalAssum (n,t) -> + let n' = Names.Name.hcons n + and t' = Term.hcons_types t in + if n' == n && t' == t then d + else LocalAssum (n',t') + | LocalDef (n,v,t) -> + let n' = Names.Name.hcons n + and v' = Term.hcons_constr v + and t' = Term.hcons_types t in + if n' == n && v' == v && t' == t then d + else LocalDef (n',v',t') let hcons_rel_context l = List.smartmap hcons_rel_decl l -- cgit v1.2.3 From 4f041384cb27f0d24fa14b272884b4b7f69cacbe Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 15 Feb 2016 11:55:43 +0100 Subject: CLEANUP: Simplifying the changes done in "kernel/*" ... ... ... ... ... ... ... ... ... ... ... ... ... ... --- kernel/declareops.ml | 31 +++++-------------------------- 1 file changed, 5 insertions(+), 26 deletions(-) (limited to 'kernel/declareops.ml') diff --git a/kernel/declareops.ml b/kernel/declareops.ml index cb67135ad4..a09a8b7862 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -9,6 +9,7 @@ open Declarations open Mod_subst open Util +open Context.Rel.Declaration (** Operations concernings types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -87,18 +88,8 @@ let is_opaque cb = match cb.const_body with (** {7 Constant substitutions } *) -let subst_rel_declaration sub x = - let open Context.Rel.Declaration in - match x with - | LocalAssum (id,t) -> - let t' = subst_mps sub t in - if t == t' then x - else LocalAssum (id,t') - | LocalDef (id,v,t) -> - let v' = subst_mps sub v in - let t' = subst_mps sub t in - if v == v' && t == t' then x - else LocalDef (id,v',t') +let subst_rel_declaration sub = + map_constr (subst_mps sub) let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) @@ -148,20 +139,8 @@ let subst_const_body sub cb = share internal fields (e.g. constr), and not the records themselves. But would it really bring substantial gains ? *) -let hcons_rel_decl d = - let open Context.Rel.Declaration in - match d with - | LocalAssum (n,t) -> - let n' = Names.Name.hcons n - and t' = Term.hcons_types t in - if n' == n && t' == t then d - else LocalAssum (n',t') - | LocalDef (n,v,t) -> - let n' = Names.Name.hcons n - and v' = Term.hcons_constr v - and t' = Term.hcons_types t in - if n' == n && v' == v && t' == t then d - else LocalDef (n',v',t') +let hcons_rel_decl = + map_type Term.hcons_types % map_value Term.hcons_constr % map_name Names.Name.hcons let hcons_rel_context l = List.smartmap hcons_rel_decl l -- cgit v1.2.3