From bd21ec85ff71e49b12d48e4ed3bf72a3f48a60d2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 26 May 2019 02:12:01 +0200 Subject: Ensure dynamically that opaque definitions come with their type. The only lawbreaker was the Add Ring command. We generate a type for the declaration to fix the code. --- kernel/term_typing.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 088dd98db8..af2c511db9 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -169,6 +169,7 @@ the polymorphic case | 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 () = assert (not (opaque && Option.is_empty typ)) in let (body, ctx), side_eff = Future.join body in let body, ctx = match trust with | Pure -> body, ctx -- cgit v1.2.3 From 5eda6e5c0f4875c0222eeba5d1210b7ec59f5496 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 26 May 2019 02:34:14 +0200 Subject: Ensure dynamically that non-opaque definitions are always side-effect free. It is guaranteed by Declare, but a little dynamic check does not hurt. --- kernel/term_typing.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index af2c511db9..eea04bbf9a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -174,6 +174,7 @@ the polymorphic case let body, ctx = match trust with | Pure -> body, ctx | SideEffects handle -> + let () = assert opaque in let body, ctx', _ = handle env body side_eff in body, Univ.ContextSet.union ctx ctx' in -- cgit v1.2.3 From 46cb90082e783e362cb13238721f83c806bfe3c3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 26 May 2019 02:37:50 +0200 Subject: Specific code path for opaque polymorphic constants. For now this is just a specialized version of the previous generic code. This simplifies tracking of the changes. --- kernel/term_typing.ml | 68 +++++++++++++++++++++++++++++++++++---------------- 1 file changed, 47 insertions(+), 21 deletions(-) (limited to 'kernel') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index eea04bbf9a..5395fec2c6 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -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) -> @@ -165,19 +157,59 @@ the polymorphic case 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 + (** 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 () = assert (not (opaque && Option.is_empty typ)) in let (body, ctx), side_eff = Future.join body in let body, ctx = match trust with | Pure -> body, ctx | SideEffects handle -> - let () = assert opaque in 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_context ~strict:false uctx env in + let sbst, auctx = Univ.abstract_universes nas uctx in + let usubst = Univ.make_instance_subst sbst in + 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 typ = + let tj = Typeops.infer_type env typ in + let _ = Typeops.judge_of_cast env j DEFAULTcast tj in + Vars.subst_univs_level_constr usubst tj.utj_val + in + let def = Vars.subst_univs_level_constr usubst j.uj_val in + let def = OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) 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 = Retypeops.relevance_of_term env j.uj_val; + 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; _ } = c in + let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c 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 -> + 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 -> let ctx = Univ.ContextSet.union univs ctx in @@ -190,9 +222,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 @@ -208,10 +237,7 @@ the polymorphic case Vars.subst_univs_level_constr usubst tj.utj_val in let def = 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 = Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; { Cooking.cook_body = def; -- cgit v1.2.3 From 90ab5eab23dfbd04b8fc6181debc133e436f5211 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 26 May 2019 15:52:15 +0200 Subject: Fix #10251: Type-checking of polymorphic opaque constr entry types is broken. We use the right environment. --- kernel/term_typing.ml | 35 ++++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) (limited to 'kernel') diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 5395fec2c6..f984088f47 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -164,35 +164,36 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = 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 (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_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 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 typ = - let tj = Typeops.infer_type env typ 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 - Vars.subst_univs_level_constr usubst tj.utj_val + let def = Vars.subst_univs_level_constr usubst j.uj_val in + def, private_univs in - let def = Vars.subst_univs_level_constr usubst j.uj_val 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 = Retypeops.relevance_of_term env j.uj_val; + cook_relevance = Sorts.relevance_of_sort tj.utj_type; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } -- cgit v1.2.3