From ff996b19faeff112a156f5db6c9ab9f26e855145 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 27 Mar 2017 00:22:51 +0200 Subject: Fix hashconsing of terms in the kernel. In one case, the hashconsed type of a judgement was not used anywhere else. In another case, the Opaqueproof module was rehashconsing terms that had already gone through a hashconsing phase. Indeed, most OpaqueDef constructor applications actually called it beforehand, so that the one performed in Opaqueproof was most often useless. The only case where this was not true was at section closing time, so that we tweak the Cooking.cook_constant to perform hashconsing for us. --- kernel/term_typing.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 2eb2c040e1..2eba1eb2a7 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -186,7 +186,8 @@ let rec unzip ctx j = unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) } let hcons_j j = - { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} + (** Do not hashcons type: it is not used by the callers of this function. *) + { uj_val = hcons_constr j.uj_val; uj_type = j.uj_type} let feedback_completion_typecheck = let open Feedback in @@ -507,7 +508,9 @@ let translate_local_assum env t = t let translate_recipe env kn r = - build_constant_declaration kn env (Cooking.cook_constant env r) + let (_, dir, _) = Constant.repr3 kn in + let hcons = DirPath.is_empty dir in + build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) let translate_local_def mb env id centry = let def,typ,proj,poly,univs,inline_code,ctx = -- cgit v1.2.3 From 11b4703ed83eeda9d959464f08185aedd3f7c250 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 26 Mar 2017 22:28:18 +0200 Subject: More efficient check in validity of side-effects. We don't need to look for the size of the whole list to find whether we can extract a suffix from it, as we can do it in one go instead. This slowness was observable in abstract-heavy code. --- kernel/term_typing.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 2eba1eb2a7..c171ba2bbf 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -139,6 +139,12 @@ let inline_side_effects env body ctx side_eff = (* CAVEAT: we assure a proper order *) List.fold_left handle_sideff (body,ctx,[]) (uniq_seff_rev side_eff) +let rec is_nth_suffix n l suf = + if Int.equal n 0 then l == suf + else match l with + | [] -> false + | _ :: l -> is_nth_suffix (pred n) l suf + (* Given the list of signatures of side effects, checks if they match. * I.e. if they are ordered descendants of the current revstruct *) let check_signatures curmb sl = @@ -151,7 +157,7 @@ let check_signatures curmb sl = match sl with | None -> sl, None | Some n -> - if List.length mb >= how_many && CList.skipn how_many mb == curmb + if is_nth_suffix how_many mb curmb then Some (n + how_many), Some mb else None, None with CEphemeron.InvalidKey -> None, None in -- cgit v1.2.3 From 78aca729a95d5e622c251d247abf29159dfe66a4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 6 Apr 2017 18:49:58 +0200 Subject: Documenting the fact terms are only hashconsed outside of a section. --- kernel/term_typing.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index c171ba2bbf..e203fce9a8 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -514,6 +514,8 @@ let translate_local_assum env t = t let translate_recipe env kn r = + (** We only hashcons the term when outside of a section, otherwise this would + be useless. It is detected by the dirpath of the constant being empty. *) let (_, dir, _) = Constant.repr3 kn in let hcons = DirPath.is_empty dir in build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) -- cgit v1.2.3 From d939a024cd077c8abce709dd69eb805cab9068db Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 7 Apr 2017 01:21:41 +0200 Subject: Inline the only use of hcons_j in Term_typing. --- kernel/term_typing.ml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index e203fce9a8..6dfa64357c 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -191,10 +191,6 @@ let rec unzip ctx j = | `Cut (n,ty,arg) :: ctx -> unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) } -let hcons_j j = - (** Do not hashcons type: it is not used by the callers of this function. *) - { uj_val = hcons_constr j.uj_val; uj_type = j.uj_type} - let feedback_completion_typecheck = let open Feedback in Option.iter (fun state_id -> @@ -231,13 +227,13 @@ let infer_declaration ~trust env kn dcl = let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = infer env body in unzip ectx j in - let j = hcons_j j in let subst = Univ.LMap.empty in let _ = judge_of_cast env j DEFAULTcast tyj in assert (eq_constr typ tyj.utj_val); + let c = hcons_constr j.uj_val in let _typ = RegularArity (Vars.subst_univs_level_constr subst typ) in feedback_completion_typecheck feedback_id; - j.uj_val, uctx) in + c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in def, RegularArity typ, None, c.const_entry_polymorphic, c.const_entry_universes, -- cgit v1.2.3