From 27468ae02bbbf018743d53a9db49efa34b6d6a3e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 16 May 2019 00:02:54 +0200 Subject: Ensure statically that declarations built by Term_typing are direct. This removes a lot of cruft breaking the opaque proof abstraction in Safe_typing and similar. --- kernel/term_typing.ml | 44 +++++++++++++++++++++++--------------------- 1 file changed, 23 insertions(+), 21 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index faa4411e92..9e33b431fc 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -154,7 +154,7 @@ the polymorphic case let c = Constr.hcons j.uj_val in feedback_completion_typecheck feedback_id; c, uctx) in - let def = OpaqueDef (Opaqueproof.create proofterm) in + let def = OpaqueDef proofterm in { Cooking.cook_body = def; cook_type = tyj.utj_val; @@ -207,7 +207,7 @@ the polymorphic case in let def = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in let def = - if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty))) + if opaque then OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) else Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; @@ -232,7 +232,7 @@ let record_aux env s_ty s_bo = (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" v -let build_constant_declaration _kn env result = +let build_constant_declaration ~force ~iter env result = let open Cooking in let typ = result.cook_type in let check declared inferred = @@ -271,11 +271,8 @@ let build_constant_declaration _kn env result = | Undef _ | Primitive _ -> Id.Set.empty | Def cs -> global_vars_set env (Mod_subst.force_constr cs) | OpaqueDef lc -> - let vars = - global_vars_set env - (Opaqueproof.force_proof (opaque_tables env) lc) in - (* we force so that cst are added to the env immediately after *) - ignore(Opaqueproof.force_constraints (opaque_tables env) lc); + let (lc, _) = force lc in + let vars = global_vars_set env lc in if !Flags.record_aux_file then record_aux env ids_typ vars; vars in @@ -296,11 +293,14 @@ let build_constant_declaration _kn env result = check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) - OpaqueDef (Opaqueproof.iter_direct_opaque (fun c -> - let ids_typ = global_vars_set env typ in - let ids_def = global_vars_set env c in - let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in - check declared inferred) lc) in + let kont c = + let ids_typ = global_vars_set env typ in + let ids_def = global_vars_set env c in + let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in + check declared inferred + in + OpaqueDef (iter kont lc) + in let univs = result.cook_universes in let tps = let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in @@ -318,8 +318,10 @@ let build_constant_declaration _kn env result = (*s Global and local constant declaration. *) -let translate_constant mb env kn ce = - build_constant_declaration kn env +let translate_constant mb env _kn ce = + let force cu = Future.force cu in + let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in + build_constant_declaration ~force ~iter env (infer_declaration ~trust:mb env ce) let translate_local_assum env t = @@ -327,8 +329,10 @@ let translate_local_assum env t = let t = Typeops.assumption_of_judgment env j in j.uj_val, t -let translate_recipe ~hcons env kn r = - build_constant_declaration kn env (Cooking.cook_constant ~hcons r) +let translate_recipe ~hcons env _kn r = + let force o = Opaqueproof.force_direct o in + let iter k o = Opaqueproof.iter_direct_opaque k o in + build_constant_declaration ~force ~iter env (Cooking.cook_constant ~hcons r) let translate_local_def env _id centry = let open Cooking in @@ -351,8 +355,7 @@ let translate_local_def env _id centry = | Def _ -> () | OpaqueDef lc -> let ids_typ = global_vars_set env typ in - let ids_def = global_vars_set env - (Opaqueproof.force_proof (opaque_tables env) lc) in + let ids_def = global_vars_set env (fst (Future.force lc)) in record_aux env ids_typ ids_def end; let () = match decl.cook_universes with @@ -362,8 +365,7 @@ let translate_local_def env _id centry = let c = match decl.cook_body with | Def c -> Mod_subst.force_constr c | OpaqueDef o -> - let p = Opaqueproof.force_proof (Environ.opaque_tables env) o in - let cst = Opaqueproof.force_constraints (Environ.opaque_tables env) o in + let (p, cst) = Future.force o in (** Let definitions are ensured to have no extra constraints coming from the body by virtue of the typing of [Entries.section_def_entry]. *) let () = assert (Univ.ContextSet.is_empty cst) in -- cgit v1.2.3 From e69e4f7fd9aaba0e3fd6c38624e3fdb0bd96026c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 17 May 2019 14:18:25 +0200 Subject: Do not perform the section variable check on global recipes. By construction, we know that Cooking is returning the right set of used variables. This set has been checked already once at the time when the definition was performed inside the section. --- kernel/term_typing.ml | 26 ++++++++++++++++++-------- 1 file changed, 18 insertions(+), 8 deletions(-) (limited to 'kernel/term_typing.ml') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 9e33b431fc..74c6189a65 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -232,7 +232,7 @@ let record_aux env s_ty s_bo = (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" v -let build_constant_declaration ~force ~iter env result = +let build_constant_declaration env result = let open Cooking in let typ = result.cook_type in let check declared inferred = @@ -271,7 +271,7 @@ let build_constant_declaration ~force ~iter env result = | Undef _ | Primitive _ -> Id.Set.empty | Def cs -> global_vars_set env (Mod_subst.force_constr cs) | OpaqueDef lc -> - let (lc, _) = force lc in + let (lc, _) = Future.force lc in let vars = global_vars_set env lc in if !Flags.record_aux_file then record_aux env ids_typ vars; vars @@ -293,6 +293,7 @@ let build_constant_declaration ~force ~iter env result = 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 @@ -319,9 +320,7 @@ let build_constant_declaration ~force ~iter env result = (*s Global and local constant declaration. *) let translate_constant mb env _kn ce = - let force cu = Future.force cu in - let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in - build_constant_declaration ~force ~iter env + build_constant_declaration env (infer_declaration ~trust:mb env ce) let translate_local_assum env t = @@ -330,9 +329,20 @@ let translate_local_assum env t = j.uj_val, t let translate_recipe ~hcons env _kn r = - let force o = Opaqueproof.force_direct o in - let iter k o = Opaqueproof.iter_direct_opaque k o in - build_constant_declaration ~force ~iter env (Cooking.cook_constant ~hcons r) + let open Cooking in + let result = Cooking.cook_constant ~hcons r in + let univs = result.cook_universes in + let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in + let tps = Option.map Cemitcodes.from_val res in + { const_hyps = Option.get result.cook_context; + const_body = result.cook_body; + const_type = result.cook_type; + const_body_code = tps; + const_universes = univs; + const_private_poly_univs = result.cook_private_univs; + const_relevance = result.cook_relevance; + const_inline_code = result.cook_inline; + const_typing_flags = Environ.typing_flags env } let translate_local_def env _id centry = let open Cooking in -- cgit v1.2.3