diff options
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 226 |
1 files changed, 101 insertions, 125 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index faa4411e92..b65e62ba30 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -31,7 +31,7 @@ type 'a effect_handler = type _ trust = | Pure : unit trust -| SideEffects : 'a effect_handler -> 'a trust +| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust let skip_trusted_seff sl b e = let rec aux sl b e acc = @@ -74,12 +74,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let j = Typeops.infer env t in let usubst, univs = Declareops.abstract_universes uctx in let r = Typeops.assumption_of_judgment env j in - let t = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in + let t = Vars.subst_univs_level_constr usubst j.uj_val in { Cooking.cook_body = Undef nl; cook_type = t; cook_universes = univs; - cook_private_univs = None; cook_relevance = r; cook_inline = false; cook_context = ctx; @@ -95,7 +94,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | Some typ -> let typ = Typeops.infer_type env typ in Typeops.check_primitive_type env op_t typ.utj_val; - Constr.hcons typ.utj_val + typ.utj_val | None -> match op_t with | CPrimitives.OT_op op -> Typeops.type_of_prim env op @@ -108,93 +107,95 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = cd; cook_type = ty; cook_universes = Monomorphic uctxt; - cook_private_univs = None; cook_inline = false; cook_context = None; cook_relevance = Sorts.Relevant; } (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, - so we delay the typing and hash consing of its body. - Remark: when the universe quantification is given explicitly, we could - delay even in the polymorphic case. *) + so we delay the typing and hash consing of its body. *) -(** Definition is opaque (Qed) and non polymorphic with known type, so we delay -the typing and hash consing of its body. - -TODO: if the universe quantification is given explicitly, we could delay even in -the polymorphic case - *) - | DefinitionEntry ({ const_entry_type = Some typ; - const_entry_opaque = true; - const_entry_universes = Monomorphic_entry univs; _ } as c) -> + | OpaqueEntry ({ opaque_entry_type = typ; + opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> let env = push_context_set ~strict:true univs env in - let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in + let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in let tyj = Typeops.infer_type env typ in let proofterm = - Future.chain body (fun ((body,uctx),side_eff) -> + 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 j, uctx = match trust with - | Pure -> - let env = push_context_set uctx env in - let j = Typeops.infer env body in - let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in - j, uctx - | SideEffects handle -> - 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 - j, uctx - in - let c = Constr.hcons j.uj_val 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, uctx) in - let def = OpaqueDef (Opaqueproof.create proofterm) in + c, Opaqueproof.PrivateMonomorphic uctx + end in + let def = OpaqueDef proofterm in { Cooking.cook_body = def; cook_type = tyj.utj_val; cook_universes = Monomorphic univs; - cook_private_univs = None; cook_relevance = Sorts.relevance_of_sort tyj.utj_type; - cook_inline = c.const_entry_inline_code; - cook_context = c.const_entry_secctx; + cook_inline = false; + cook_context = Some c.opaque_entry_secctx; + } + + (** Similar case for polymorphic entries. *) + + | 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 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 typ = Vars.subst_univs_level_constr usubst tj.utj_val in + { + Cooking.cook_body = def; + cook_type = typ; + cook_universes = Polymorphic auctx; + cook_relevance = Sorts.relevance_of_sort tj.utj_type; + cook_inline = false; + cook_context = Some c.opaque_entry_secctx; } (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> - let { const_entry_type = typ; const_entry_opaque = opaque ; _ } = c in + let { const_entry_type = typ; _ } = c in let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in - let (body, ctx), side_eff = Future.join body in - let body, ctx = match trust with - | Pure -> body, ctx - | SideEffects handle -> - let body, ctx', _ = handle env body side_eff in - body, Univ.ContextSet.union ctx ctx' - in - let env, usubst, univs, private_univs = match c.const_entry_universes with - | Monomorphic_entry univs -> - let ctx = Univ.ContextSet.union univs ctx 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 - env, Univ.empty_level_subst, Monomorphic ctx, None + env, Univ.empty_level_subst, Monomorphic ctx | Polymorphic_entry (nas, uctx) -> (** [ctx] must contain local universes, such that it has no impact on the rest of the graph (up to transitivity). *) let env = push_context ~strict:false uctx env in let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in - let env, local = - if opaque then - push_subgraph ctx env, Some (on_snd (Univ.subst_univs_level_constraints sbst) ctx) - else - if Univ.ContextSet.is_empty ctx then env, None - else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") - in - env, sbst, Polymorphic auctx, local + env, sbst, Polymorphic auctx in let j = Typeops.infer env body in let typ = match typ with @@ -205,34 +206,19 @@ the polymorphic case let _ = Typeops.judge_of_cast env j DEFAULTcast tj in Vars.subst_univs_level_constr usubst tj.utj_val 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))) - else Def (Mod_subst.from_val def) - in + let def = Vars.subst_univs_level_constr usubst j.uj_val in + let def = Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; { Cooking.cook_body = def; cook_type = typ; cook_universes = univs; - cook_private_univs = private_univs; cook_relevance = Retypeops.relevance_of_term env j.uj_val; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } -let record_aux env s_ty s_bo = - let in_ty = keep_hyps env s_ty in - let v = - String.concat " " - (CList.map_filter (fun decl -> - let id = NamedDecl.get_id decl in - if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None - else Some (Id.to_string id)) - (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 env result = let open Cooking in let typ = result.cook_type in let check declared inferred = @@ -263,27 +249,22 @@ let build_constant_declaration _kn env result = let context_ids = List.map NamedDecl.get_id (named_context env) in let def = result.cook_body in match result.cook_context with - | None when not (List.is_empty context_ids) -> + | None -> + if List.is_empty context_ids then + (* Empty section context: no need to check *) + [], def + else (* No declared section vars, and non-empty section context: we must look at the body NOW, if any *) let ids_typ = global_vars_set env typ in let ids_def = match def with | 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); - if !Flags.record_aux_file then record_aux env ids_typ vars; - vars + | OpaqueDef _ -> + (* Opaque definitions always come with their section variables *) + assert false in keep_hyps env (Id.Set.union ids_typ ids_def), def - | None -> - if !Flags.record_aux_file then - record_aux env Id.Set.empty Id.Set.empty; - [], def (* Empty section context: no need to check *) | Some declared -> (* We use the declared set and chain a check of correctness *) sort declared, @@ -296,11 +277,15 @@ 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 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 = 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 @@ -311,15 +296,14 @@ let build_constant_declaration _kn env result = const_type = typ; 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 } (*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 = + build_constant_declaration env (infer_declaration ~trust:mb env ce) let translate_local_assum env t = @@ -327,47 +311,39 @@ 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 env _kn r = + let open Cooking in + let result = Cooking.cook_constant 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_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 - let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in let centry = { - const_entry_body = body; + const_entry_body = centry.secdef_body; const_entry_secctx = centry.secdef_secctx; const_entry_feedback = centry.secdef_feedback; const_entry_type = centry.secdef_type; const_entry_universes = Monomorphic_entry Univ.ContextSet.empty; - const_entry_opaque = false; const_entry_inline_code = false; } in let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in let typ = decl.cook_type in - if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin - match decl.cook_body with - | Undef _ -> () - | Primitive _ -> () - | 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 - record_aux env ids_typ ids_def - end; let () = match decl.cook_universes with | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx) | Polymorphic _ -> assert false in 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 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 - p - | Undef _ | Primitive _ -> assert false + | Undef _ | Primitive _ | OpaqueDef _ -> assert false in c, decl.cook_relevance, typ |