diff options
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 85 |
1 files changed, 57 insertions, 28 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 74c6189a65..f984088f47 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -74,7 +74,7 @@ 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; @@ -95,7 +95,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 @@ -115,16 +115,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = } (** 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) -> @@ -151,7 +143,7 @@ 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 let def = OpaqueDef proofterm in @@ -165,16 +157,59 @@ the polymorphic case cook_context = c.const_entry_secctx; } + (** Similar case for polymorphic entries. TODO: also delay type-checking of + the body. *) + + | DefinitionEntry ({ const_entry_type = Some typ; + const_entry_opaque = true; + const_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> + let { const_entry_body = body; const_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 (def, private_univs) = + 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 + (** [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 + def, private_univs + in + let def = OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) in + let typ = Vars.subst_univs_level_constr usubst tj.utj_val in + feedback_completion_typecheck feedback_id; + { + Cooking.cook_body = def; + cook_type = typ; + cook_universes = Polymorphic auctx; + cook_private_univs = Some private_univs; + cook_relevance = Sorts.relevance_of_sort tj.utj_type; + cook_inline = c.const_entry_inline_code; + cook_context = c.const_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 + (* Opaque constants must be provided with a non-empty const_entry_type, + and thus should have been treated above. *) + let () = assert (not c.const_entry_opaque) 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' + | Pure -> + let (body, ctx), () = Future.join body in + body, ctx + | SideEffects _ -> assert false in let env, usubst, univs, private_univs = match c.const_entry_universes with | Monomorphic_entry univs -> @@ -188,9 +223,6 @@ the polymorphic case 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 @@ -205,11 +237,8 @@ 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; @@ -328,9 +357,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 |