From 4457e6d75affd20c1c13c0d798c490129525bcb5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 4 Jul 2017 13:38:22 +0200 Subject: More precise type for universe entries. We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure. --- kernel/term_typing.ml | 30 +++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index cf82d54ec1..9102234657 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -251,8 +251,8 @@ let infer_declaration ~trust env kn dcl = delay even in the polymorphic case. *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; - const_entry_polymorphic = false} as c) -> - let env = push_context ~strict:true c.const_entry_universes env in + const_entry_universes = Monomorphic_const_entry univs } as c) -> + let env = push_context ~strict:true univs env in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = @@ -271,7 +271,7 @@ let infer_declaration ~trust env kn dcl = c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in def, RegularArity typ, None, - (Monomorphic_const c.const_entry_universes), + (Monomorphic_const univs), c.const_entry_inline_code, c.const_entry_secctx (** Other definitions have to be processed immediately. *) @@ -279,18 +279,22 @@ let infer_declaration ~trust env kn dcl = let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in - let univsctx = Univ.ContextSet.of_context c.const_entry_universes in + let poly, univs = match c.const_entry_universes with + | Monomorphic_const_entry univs -> false, univs + | Polymorphic_const_entry univs -> true, univs + in + let univsctx = Univ.ContextSet.of_context univs in let body, ctx, _ = inline_side_effects env body (Univ.ContextSet.union univsctx ctx) side_eff in - let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in - let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in + let env = push_context_set ~strict:(not poly) ctx env in + let abstract = poly && not (Option.is_empty kn) in let usubst, univs = abstract_constant_universes abstract (Univ.ContextSet.to_context ctx) in let j = infer env body in let typ = match typ with | None -> - if not c.const_entry_polymorphic then (* Old-style polymorphism *) + if not poly then (* Old-style polymorphism *) make_polymorphic_if_constant_for_ind env j else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type) | Some t -> @@ -461,11 +465,12 @@ let translate_constant mb env kn ce = (infer_declaration ~trust:mb env (Some kn) ce) let constant_entry_of_side_effect cb u = - let poly, univs = + let univs = match cb.const_universes with - | Monomorphic_const ctx -> false, ctx + | Monomorphic_const uctx -> + Monomorphic_const_entry uctx | Polymorphic_const auctx -> - true, Univ.AUContext.repr auctx + Polymorphic_const_entry (Univ.AUContext.repr auctx) in let pt = match cb.const_body, u with @@ -478,7 +483,6 @@ let constant_entry_of_side_effect cb u = const_entry_feedback = None; const_entry_type = (match cb.const_type with RegularArity t -> Some t | _ -> None); - const_entry_polymorphic = poly; const_entry_universes = univs; const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } @@ -592,6 +596,10 @@ let translate_local_def mb env id centry = env ids_def ids_typ context_ids in record_aux env ids_typ ids_def expr end; + let univs = match univs with + | Monomorphic_const ctx -> ctx + | Polymorphic_const _ -> assert false + in def, typ, univs (* Insertion of inductive types. *) -- cgit v1.2.3 From 9961577dfbb93f0b691c355ba99822665def037f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 4 Jul 2017 17:00:48 +0200 Subject: Using a record type for Cooking.result. --- kernel/term_typing.ml | 71 ++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 50 insertions(+), 21 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 9102234657..c809e4791c 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -243,7 +243,14 @@ let infer_declaration ~trust env kn dcl = in let c = Typeops.assumption_of_judgment env j in let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in - Undef nl, RegularArity t, None, univs, false, ctx + { + Cooking.cook_body = Undef nl; + cook_type = RegularArity t; + cook_proj = None; + cook_universes = univs; + cook_inline = false; + cook_context = ctx; + } (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, so we delay the typing and hash consing of its body. @@ -270,9 +277,14 @@ let infer_declaration ~trust env kn dcl = feedback_completion_typecheck feedback_id; c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in - def, RegularArity typ, None, - (Monomorphic_const univs), - c.const_entry_inline_code, c.const_entry_secctx + { + Cooking.cook_body = def; + cook_type = RegularArity typ; + cook_proj = None; + cook_universes = Monomorphic_const univs; + cook_inline = c.const_entry_inline_code; + cook_context = c.const_entry_secctx; + } (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> @@ -308,7 +320,14 @@ let infer_declaration ~trust env kn dcl = else Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; - def, typ, None, univs, c.const_entry_inline_code, c.const_entry_secctx + { + Cooking.cook_body = def; + cook_type = typ; + cook_proj = None; + cook_universes = univs; + cook_inline = c.const_entry_inline_code; + cook_context = c.const_entry_secctx; + } | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} -> let mib, _ = Inductive.lookup_mind_specif env (ind,0) in @@ -328,8 +347,14 @@ let infer_declaration ~trust env kn dcl = Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi) in let term, typ = pb.proj_eta in - Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb, - univs, false, None + { + Cooking.cook_body = Def (Mod_subst.from_val (hcons_constr term)); + cook_type = RegularArity typ; + cook_proj = Some pb; + cook_universes = univs; + cook_inline = false; + cook_context = None; + } let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t @@ -353,7 +378,9 @@ let record_aux env s_ty s_bo suggested_expr = let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f -let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = +let build_constant_declaration kn env result = + let open Cooking in + let typ = result.cook_type in let check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in @@ -380,7 +407,8 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = (* We try to postpone the computation of used section variables *) let hyps, def = let context_ids = List.map NamedDecl.get_id (named_context env) in - match ctx with + let def = result.cook_body in + match result.cook_context with | None when not (List.is_empty context_ids) -> (* No declared section vars, and non-empty section context: we must look at the body NOW, if any *) @@ -423,9 +451,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = let ids_def = global_vars_set env c in let inferred = keep_hyps env (Idset.union ids_typ ids_def) in check declared inferred) lc) in + let univs = result.cook_universes in let tps = let res = - match proj with + match result.cook_proj with | None -> compile_constant_body env univs def | Some pb -> (* The compilation of primitive projections is a bit tricky, because @@ -438,10 +467,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = { const_hyps = hyps; const_body = def; const_type = typ; - const_proj = proj; + const_proj = result.cook_proj; const_body_code = None; const_universes = univs; - const_inline_code = inline_code; + const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env; } in @@ -452,10 +481,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = { const_hyps = hyps; const_body = def; const_type = typ; - const_proj = proj; + const_proj = result.cook_proj; const_body_code = tps; const_universes = univs; - const_inline_code = inline_code; + const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } (*s Global and local constant declaration. *) @@ -579,11 +608,11 @@ let translate_recipe env kn r = build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) let translate_local_def mb env id centry = - let def,typ,proj,univs,inline_code,ctx = - infer_declaration ~trust:mb env None (DefinitionEntry centry) in - let typ = type_of_constant_type env typ in - if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin - match def with + let open Cooking in + let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in + let typ = type_of_constant_type env decl.cook_type in + if Option.is_empty decl.cook_context && !Flags.compilation_mode = Flags.BuildVo then begin + match decl.cook_body with | Undef _ -> () | Def _ -> () | OpaqueDef lc -> @@ -596,11 +625,11 @@ let translate_local_def mb env id centry = env ids_def ids_typ context_ids in record_aux env ids_typ ids_def expr end; - let univs = match univs with + let univs = match decl.cook_universes with | Monomorphic_const ctx -> ctx | Polymorphic_const _ -> assert false in - def, typ, univs + decl.cook_body, typ, univs (* Insertion of inductive types. *) -- cgit v1.2.3 From 3c6679676c3963b7c3ec7c1eadbf24ae70311408 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 14 Jul 2017 15:43:40 +0200 Subject: More precise type of entries capturing their lack of side-effects. We sprinkle a few GADTs in the kernel in order to statically ensure that entries are pure, so that we get stronger invariants. --- kernel/term_typing.ml | 45 ++++++++++++++++++++++++++++++--------------- 1 file changed, 30 insertions(+), 15 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index c809e4791c..03bd8426fe 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -77,6 +77,10 @@ end type side_effects = SideEffects.t +type _ trust = +| Pure : unit trust +| SideEffects : structure_body -> side_effects trust + let uniq_seff_rev = SideEffects.repr let uniq_seff l = List.rev (SideEffects.repr l) @@ -232,7 +236,7 @@ let abstract_constant_universes abstract uctx = let sbst, auctx = Univ.abstract_universes uctx in sbst, Polymorphic_const auctx -let infer_declaration ~trust env kn dcl = +let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context ~strict:(not poly) uctx env in @@ -264,15 +268,22 @@ let infer_declaration ~trust env kn dcl = let tyj = infer_type env typ in let proofterm = Future.chain ~pure:true body (fun ((body,uctx),side_eff) -> - let body, uctx, signatures = - inline_side_effects env body uctx side_eff in - let valid_signatures = check_signatures trust signatures in - let env = push_context_set uctx env in - let j = + let j, uctx = match trust with + | Pure -> + let env = push_context_set uctx env in + let j = infer env body in + let _ = judge_of_cast env j DEFAULTcast tyj in + j, uctx + | SideEffects trust -> + let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in + let valid_signatures = check_signatures trust signatures in + let env = push_context_set uctx env in let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = infer env body in - unzip ectx j in - let _ = judge_of_cast env j DEFAULTcast tyj in + let j = unzip ectx j in + let _ = judge_of_cast env j DEFAULTcast tyj in + j, uctx + in let c = hcons_constr j.uj_val in feedback_completion_typecheck feedback_id; c, uctx) in @@ -296,8 +307,11 @@ let infer_declaration ~trust env kn dcl = | Polymorphic_const_entry univs -> true, univs in let univsctx = Univ.ContextSet.of_context univs in - let body, ctx, _ = inline_side_effects env body - (Univ.ContextSet.union univsctx ctx) side_eff in + let ctx = Univ.ContextSet.union univsctx ctx in + let body, ctx, _ = match trust with + | Pure -> body, ctx, [] + | SideEffects _ -> inline_side_effects env body ctx side_eff + in let env = push_context_set ~strict:(not poly) ctx env in let abstract = poly && not (Option.is_empty kn) in let usubst, univs = @@ -507,7 +521,7 @@ let constant_entry_of_side_effect cb u = | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty | _ -> assert false in DefinitionEntry { - const_entry_body = Future.from_val (pt, empty_seff); + const_entry_body = Future.from_val (pt, ()); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = @@ -530,17 +544,18 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effects constant_entry * side_effect_role + constant * constant_body * unit constant_entry * side_effect_role let export_side_effects mb env ce = match ce with - | ParameterEntry _ | ProjectionEntry _ -> [], ce + | ParameterEntry e -> [], ParameterEntry e + | ProjectionEntry e -> [], ProjectionEntry e | DefinitionEntry c -> let { const_entry_body = body } = c in let _, eff = Future.force body in let ce = DefinitionEntry { c with const_entry_body = Future.chain ~pure:true body - (fun (b_ctx, _) -> b_ctx, empty_seff) } in + (fun (b_ctx, _) -> b_ctx, ()) } in let not_exists (c,_,_,_) = try ignore(Environ.lookup_constant c env); false with Not_found -> true in @@ -580,7 +595,7 @@ let export_side_effects mb env ce = let env, cbs = List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> let ce = constant_entry_of_side_effect ocb u in - let cb = translate_constant mb env kn ce in + let cb = translate_constant Pure env kn ce in (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) (env,[]) cbs in translate_seff sl rest (cbs @ acc) env -- cgit v1.2.3 From ce830b204ad52f8b3655d2cb4672662120d83101 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 16 Jul 2017 00:05:03 +0200 Subject: Further simplication: do not recreate entries for side-effects. This is actually useless, the code does not depend on the value of the entry for side-effects. --- kernel/term_typing.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 03bd8426fe..23c5b6f58e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -544,7 +544,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * unit constant_entry * side_effect_role + constant * constant_body * side_effect_role let export_side_effects mb env ce = match ce with @@ -596,7 +596,7 @@ let export_side_effects mb env ce = List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> let ce = constant_entry_of_side_effect ocb u in let cb = translate_constant Pure env kn ce in - (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) + (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) (env,[]) cbs in translate_seff sl rest (cbs @ acc) env | Some sl, cbs :: rest -> @@ -604,7 +604,7 @@ let export_side_effects mb env ce = let cbs = List.map turn_direct cbs in let env = List.fold_left push_seff env cbs in let ecbs = List.map (fun (kn,cb,u,r) -> - kn, cb, constant_entry_of_side_effect cb u, r) cbs in + kn, cb, r) cbs in translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env in translate_seff trusted seff [] env -- cgit v1.2.3 From 665256fec8465ff0adb943063c25f07a6ca54618 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 18 Jul 2017 18:16:43 +0200 Subject: Statically ensuring that inlined entries out of the kernel have no effects. This was an easy to prove property that I somehow overlooked. --- kernel/term_typing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 23c5b6f58e..ed53df01f1 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -654,7 +654,7 @@ let inline_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> let body, ctx',_ = inline_side_effects env body ctx side_eff in - (body, ctx'), empty_seff); + (body, ctx'), ()); } let inline_side_effects env body side_eff = -- cgit v1.2.3 From 906b48ff401f22be6059a6cdde8723b858102690 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 19 Jul 2017 14:05:52 +0200 Subject: Avoiding a variable shadowing in the kernel. This ought to ease the understanding of the code. --- kernel/term_typing.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index ed53df01f1..43c099712a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -274,9 +274,9 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry let j = infer env body in let _ = judge_of_cast env j DEFAULTcast tyj in j, uctx - | SideEffects trust -> + | SideEffects mb -> let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in - let valid_signatures = check_signatures trust signatures in + let valid_signatures = check_signatures mb signatures in let env = push_context_set uctx env in let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = infer env body in -- cgit v1.2.3