diff options
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 124 |
1 files changed, 70 insertions, 54 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 74c6189a65..eca22869d2 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 *) @@ -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,31 +107,21 @@ 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 @@ -151,50 +140,81 @@ the polymorphic case let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in j, uctx in - let c = Constr.hcons j.uj_val in + let c = j.uj_val in feedback_completion_typecheck feedback_id; - c, uctx) 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 = 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 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 + (** [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 = 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_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' + let { const_entry_type = typ; _ } = c in + let { const_entry_body = (body, ctx); const_entry_feedback = feedback_id; _ } = c in + let () = match trust with + | Pure -> () + | SideEffects _ -> assert false in - let env, usubst, univs, private_univs = match c.const_entry_universes with + let env, usubst, univs = match c.const_entry_universes with | Monomorphic_entry univs -> let ctx = Univ.ContextSet.union univs ctx in 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.") + let () = + if not (Univ.ContextSet.is_empty ctx) then + 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,17 +225,13 @@ 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 (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; @@ -312,7 +328,6 @@ let build_constant_declaration 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 } @@ -328,9 +343,9 @@ 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 = +let translate_recipe env _kn r = let open Cooking in - let result = Cooking.cook_constant ~hcons r 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 @@ -339,21 +354,19 @@ let translate_recipe ~hcons env _kn r = 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 - let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in + let body = (centry.secdef_body, Univ.ContextSet.empty) in let centry = { const_entry_body = 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 @@ -378,7 +391,10 @@ let translate_local_def env _id centry = 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 + let () = match cst with + | Opaqueproof.PrivateMonomorphic ctx -> assert (Univ.ContextSet.is_empty ctx) + | Opaqueproof.PrivatePolymorphic (_, ctx) -> assert (Univ.ContextSet.is_empty ctx) + in p | Undef _ | Primitive _ -> assert false in |