diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 28 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 142 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 14 |
3 files changed, 94 insertions, 90 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index fc55720583..4dbc009324 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -767,22 +767,24 @@ let export_side_effects mb env (b_ctx, eff) = let kn = eff.seff_constant in let ce = constant_entry_of_side_effect eff in let open Entries in - let open Term_typing in let cb = match ce with | DefinitionEff ce -> - Term_typing.translate_constant Pure env kn (DefinitionEntry ce) + Term_typing.translate_constant env kn (DefinitionEntry ce) | OpaqueEff ce -> - let handle _env c () = (c, Univ.ContextSet.empty, 0) in - Term_typing.translate_constant (SideEffects handle) env kn (OpaqueEntry ce) + Term_typing.translate_constant env kn (OpaqueEntry ce) in - let map cu = - let (c, u) = Future.force cu in + let map ctx = match ce with + | OpaqueEff e -> + let body = Future.force e.Entries.opaque_entry_body in + let handle _env c () = (c, Univ.ContextSet.empty, 0) in + let (c, u) = Term_typing.check_delayed handle ctx body in let () = match u with | Opaqueproof.PrivateMonomorphic ctx | Opaqueproof.PrivatePolymorphic (_, ctx) -> assert (Univ.ContextSet.is_empty ctx) in c + | _ -> assert false in let cb = map_constant map cb in let eff = { eff with seff_body = cb } in @@ -824,15 +826,23 @@ let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constan let kn = Constant.make2 senv.modpath l in let cb = match decl with - | ConstantEntry (EffectEntry, ce) -> + | ConstantEntry (EffectEntry, Entries.OpaqueEntry e) -> let handle env body eff = let body, uctx, signatures = inline_side_effects env body eff in let trusted = check_signatures senv.revstruct signatures in body, uctx, trusted in - Term_typing.translate_constant (Term_typing.SideEffects handle) senv.env kn ce + let cb = Term_typing.translate_constant senv.env kn (Entries.OpaqueEntry e) in + let ctx = match cb.const_body with + | OpaqueDef ctx -> ctx + | _ -> assert false + in + let map pf = Term_typing.check_delayed handle ctx pf in + let pf = Future.chain e.Entries.opaque_entry_body map in + { cb with const_body = OpaqueDef pf } | ConstantEntry (PureEntry, ce) -> - Term_typing.translate_constant Term_typing.Pure senv.env kn ce + let cb = Term_typing.translate_constant senv.env kn ce in + map_constant (fun _ -> assert false) cb in let senv = let senv, cb, delayed_cst = match cb.const_body with diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f70b2960cf..1e0db8026f 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -29,10 +29,6 @@ module NamedDecl = Context.Named.Declaration type 'a effect_handler = env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) -type _ trust = -| Pure : unit trust -| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust - let skip_trusted_seff sl b e = let rec aux sl b e acc = let open Context.Rel.Declaration in @@ -64,7 +60,11 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> Feedback.feedback ~id:state_id Feedback.Complete) -let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = +type typing_context = +| MonoTyCtx of Environ.env * unsafe_type_judgment * Univ.ContextSet.t * Id.Set.t * Stateid.t option +| PolyTyCtx of Environ.env * unsafe_type_judgment * Univ.universe_level_subst * Univ.AUContext.t * Id.Set.t * Stateid.t option + +let infer_declaration (type a) env (dcl : a constant_entry) = match dcl with | ParameterEntry (ctx,(t,uctx),nl) -> let env = match uctx with @@ -118,25 +118,10 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | OpaqueEntry ({ opaque_entry_type = typ; opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> let env = push_context_set ~strict:true univs env in - let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in + let { opaque_entry_feedback = feedback_id; _ } = c in let tyj = Typeops.infer_type env typ in - let proofterm = - Future.chain body begin fun ((body,uctx),side_eff) -> - (* don't redeclare universes which are declared for the type *) - let uctx = Univ.ContextSet.diff uctx univs in - let SideEffects handle = trust in - let (body, uctx', valid_signatures) = handle env body side_eff in - let uctx = Univ.ContextSet.union uctx uctx' in - let env = push_context_set uctx env in - let body,env,ectx = skip_trusted_seff valid_signatures body env in - let j = Typeops.infer env body in - let j = unzip ectx j in - let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in - let c = j.uj_val in - feedback_completion_typecheck feedback_id; - c, Opaqueproof.PrivateMonomorphic uctx - end in - let def = OpaqueDef proofterm in + let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in + let def = OpaqueDef context in { Cooking.cook_body = def; cook_type = tyj.utj_val; @@ -150,26 +135,13 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | OpaqueEntry ({ opaque_entry_type = typ; opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> - let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in + let { opaque_entry_feedback = feedback_id; _ } = c in let env = push_context ~strict:false uctx env in let tj = Typeops.infer_type env typ in let sbst, auctx = Univ.abstract_universes nas uctx in let usubst = Univ.make_instance_subst sbst in - let proofterm = Future.chain body begin fun ((body, ctx), side_eff) -> - let SideEffects handle = trust in - let body, ctx', _ = handle env body side_eff in - let ctx = Univ.ContextSet.union ctx ctx' in - (** [ctx] must contain local universes, such that it has no impact - on the rest of the graph (up to transitivity). *) - let env = push_subgraph ctx env in - let private_univs = on_snd (Univ.subst_univs_level_constraints usubst) ctx in - let j = Typeops.infer env body in - let _ = Typeops.judge_of_cast env j DEFAULTcast tj in - let def = Vars.subst_univs_level_constr usubst j.uj_val in - let () = feedback_completion_typecheck feedback_id in - def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs) - end in - let def = OpaqueDef proofterm in + let context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in + let def = OpaqueDef context in let typ = Vars.subst_univs_level_constr usubst tj.utj_val in { Cooking.cook_body = def; @@ -184,7 +156,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | DefinitionEntry c -> let { const_entry_type = typ; _ } = c in let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in - let Pure = trust in let env, usubst, univs = match c.const_entry_universes with | Monomorphic_entry ctx -> let env = push_context_set ~strict:true ctx env in @@ -218,25 +189,29 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_context = c.const_entry_secctx; } +let check_section_variables env declared_set typ body = + let ids_typ = global_vars_set env typ in + let ids_def = global_vars_set env body in + let inferred_set = Environ.really_needed env (Id.Set.union ids_typ ids_def) in + if not (Id.Set.subset inferred_set declared_set) then + let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in + let n = List.length l in + let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_set) in + let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_set) in + let missing_vars = Pp.pr_sequence Id.print (List.rev l) in + user_err Pp.(prlist str + ["The following section "; (String.plural n "variable"); " "; + (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++ + missing_vars ++ str "." ++ fnl () ++ fnl () ++ + str "You can either update your proof to not depend on " ++ missing_vars ++ + str ", or you can update your Proof line from" ++ fnl () ++ + str "Proof using " ++ declared_vars ++ fnl () ++ + str "to" ++ fnl () ++ + str "Proof using " ++ inferred_vars) + let build_constant_declaration env result = let open Cooking in let typ = result.cook_type in - let check declared_set inferred_set = - if not (Id.Set.subset inferred_set declared_set) then - let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in - let n = List.length l in - let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_set) in - let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_set) in - let missing_vars = Pp.pr_sequence Id.print (List.rev l) in - user_err Pp.(prlist str - ["The following section "; (String.plural n "variable"); " "; - (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++ - missing_vars ++ str "." ++ fnl () ++ fnl () ++ - str "You can either update your proof to not depend on " ++ missing_vars ++ - str ", or you can update your Proof line from" ++ fnl () ++ - str "Proof using " ++ declared_vars ++ fnl () ++ - str "to" ++ fnl () ++ - str "Proof using " ++ inferred_vars) in (* 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 @@ -265,22 +240,10 @@ let build_constant_declaration env result = (* We use the declared set and chain a check of correctness *) declared, match def with - | Undef _ | Primitive _ as x -> x (* nothing to check *) + | Undef _ | Primitive _ | OpaqueDef _ as x -> x (* nothing to check *) | Def cs as x -> - let ids_typ = global_vars_set env typ in - let ids_def = global_vars_set env (Mod_subst.force_constr cs) in - let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in - check declared inferred; - x - | OpaqueDef lc -> (* In this case we can postpone the check *) - let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in - let kont c = - let ids_typ = global_vars_set env typ in - let ids_def = global_vars_set env c in - let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in - check declared inferred - in - OpaqueDef (iter kont lc) + let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in + x in let univs = result.cook_universes in let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in @@ -297,11 +260,42 @@ let build_constant_declaration env result = const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } +let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_output) = match tyenv with +| MonoTyCtx (env, tyj, univs, declared, feedback_id) -> + let ((body, uctx), side_eff) = body in + (* don't redeclare universes which are declared for the type *) + let uctx = Univ.ContextSet.diff uctx univs in + let (body, uctx', valid_signatures) = handle env body side_eff in + let uctx = Univ.ContextSet.union uctx uctx' in + let env = push_context_set uctx env in + let body,env,ectx = skip_trusted_seff valid_signatures body env in + let j = Typeops.infer env body in + let j = unzip ectx j in + let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in + let c = j.uj_val in + let () = check_section_variables env declared tyj.utj_val body in + feedback_completion_typecheck feedback_id; + c, Opaqueproof.PrivateMonomorphic uctx +| PolyTyCtx (env, tj, usubst, auctx, declared, feedback_id) -> + let ((body, ctx), side_eff) = body in + let body, ctx', _ = handle env body side_eff in + let ctx = Univ.ContextSet.union ctx ctx' in + (** [ctx] must contain local universes, such that it has no impact + on the rest of the graph (up to transitivity). *) + let env = push_subgraph ctx env in + let private_univs = on_snd (Univ.subst_univs_level_constraints usubst) ctx in + let j = Typeops.infer env body in + let _ = Typeops.judge_of_cast env j DEFAULTcast tj in + let () = check_section_variables env declared tj.utj_val body in + let def = Vars.subst_univs_level_constr usubst j.uj_val in + let () = feedback_completion_typecheck feedback_id in + def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs) + (*s Global and local constant declaration. *) -let translate_constant mb env _kn ce = +let translate_constant env _kn ce = build_constant_declaration env - (infer_declaration ~trust:mb env ce) + (infer_declaration env ce) let translate_local_assum env t = let j = Typeops.infer env t in @@ -336,7 +330,7 @@ let translate_local_def env _id centry = const_entry_universes = Monomorphic_entry Univ.ContextSet.empty; const_entry_inline_code = false; } in - let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in + let decl = infer_declaration env (DefinitionEntry centry) in let typ = decl.cook_type in let () = match decl.cook_universes with | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index ef01ece185..f82312245b 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -22,9 +22,7 @@ open Entries type 'a effect_handler = env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) -type _ trust = -| Pure : unit trust -| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust +type typing_context val translate_local_def : env -> Id.t -> section_def_entry -> constr * Sorts.relevance * types @@ -32,15 +30,17 @@ val translate_local_def : env -> Id.t -> section_def_entry -> val translate_local_assum : env -> types -> types * Sorts.relevance val translate_constant : - 'a trust -> env -> Constant.t -> 'a constant_entry -> - Opaqueproof.proofterm constant_body + env -> Constant.t -> 'a constant_entry -> + typing_context constant_body val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body +val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes) + (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:'a trust -> env -> - 'a constant_entry -> Opaqueproof.proofterm Cooking.result +val infer_declaration : env -> + 'a constant_entry -> typing_context Cooking.result val build_constant_declaration : env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body |