From 4ceadecf179e9210eed42ef4847aa5ab8fa28bd6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 19 Jun 2019 21:17:09 +0200 Subject: Take advantage of the change of entry representation to split opacity status. Mere isomorphism for now, but will allow more invariants ultimately. --- kernel/entries.ml | 2 +- kernel/safe_typing.ml | 10 +++++++++- kernel/term_typing.ml | 13 +++++-------- 3 files changed, 15 insertions(+), 10 deletions(-) (limited to 'kernel') diff --git a/kernel/entries.ml b/kernel/entries.ml index de1ce609fd..1a25337512 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -68,7 +68,6 @@ type 'a definition_entry = { const_entry_feedback : Stateid.t option; const_entry_type : types option; const_entry_universes : universes_entry; - const_entry_opaque : bool; const_entry_inline_code : bool } type section_def_entry = { @@ -91,6 +90,7 @@ type primitive_entry = { type 'a constant_entry = | DefinitionEntry of 'a definition_entry + | OpaqueEntry of 'a definition_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a980d22e42..c99edccda7 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -688,13 +688,21 @@ let constant_entry_of_side_effect eff = | OpaqueDef b -> b | Def b -> Mod_subst.force_constr b | _ -> assert false in + if Declareops.is_opaque cb then + OpaqueEntry { + const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = Some cb.const_type; + const_entry_universes = univs; + const_entry_inline_code = cb.const_inline_code } + else DefinitionEntry { const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = Some cb.const_type; const_entry_universes = univs; - const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } let export_eff eff = diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 165feca1b6..e28849c953 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -115,9 +115,9 @@ 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. *) - | DefinitionEntry ({ const_entry_type = Some typ; - const_entry_opaque = true; + | OpaqueEntry ({ const_entry_type = typ; const_entry_universes = Monomorphic_entry univs; _ } as c) -> + let typ = match typ with None -> assert false | Some typ -> typ in let env = push_context_set ~strict:true univs env in let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in let tyj = Typeops.infer_type env typ in @@ -155,12 +155,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_context = c.const_entry_secctx; } - (** Similar case for polymorphic entries. TODO: also delay type-checking of - the body. *) + (** Similar case for polymorphic entries. *) - | DefinitionEntry ({ const_entry_type = Some typ; - const_entry_opaque = true; + | OpaqueEntry ({ const_entry_type = typ; const_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> + let typ = match typ with None -> assert false | Some typ -> typ in 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 @@ -200,7 +199,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = 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 @@ -375,7 +373,6 @@ let translate_local_def env _id centry = 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 -- cgit v1.2.3 From be3bba54e39a316ded975b7c5ac5723fed41aa88 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 19 Jun 2019 21:24:36 +0200 Subject: Enforce that transparent entries are forced beforehand. --- kernel/entries.ml | 6 +++--- kernel/safe_typing.ml | 2 +- kernel/term_typing.ml | 12 ++++-------- 3 files changed, 8 insertions(+), 12 deletions(-) (limited to 'kernel') diff --git a/kernel/entries.ml b/kernel/entries.ml index 1a25337512..3f33df3f74 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -61,7 +61,7 @@ type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation type 'a definition_entry = { - const_entry_body : 'a const_entry_body; + const_entry_body : 'a; (* List of section variables *) const_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) @@ -89,8 +89,8 @@ type primitive_entry = { } type 'a constant_entry = - | DefinitionEntry of 'a definition_entry - | OpaqueEntry of 'a definition_entry + | DefinitionEntry of constr Univ.in_universe_context_set definition_entry + | OpaqueEntry of 'a const_entry_body definition_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index c99edccda7..ab58321ac7 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -698,7 +698,7 @@ let constant_entry_of_side_effect eff = const_entry_inline_code = cb.const_inline_code } else DefinitionEntry { - const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); + const_entry_body = (p, Univ.ContextSet.empty); const_entry_secctx = None; const_entry_feedback = None; const_entry_type = Some cb.const_type; diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index e28849c953..3b689953c8 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -196,13 +196,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = (** 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 body, ctx = match trust with - | Pure -> - let (body, ctx), () = Future.join body in - body, ctx + 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 = match c.const_entry_universes with @@ -366,7 +362,7 @@ let translate_recipe env _kn r = 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; -- cgit v1.2.3 From bbec0ea51b4dfef1ddb09a2f876323aa1547f643 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 20 Jun 2019 08:14:28 +0200 Subject: Dedicated type for opaque entries in the kernel. Even more invariants can be enforced this way. --- kernel/entries.ml | 12 +++++++++++- kernel/safe_typing.ml | 12 ++++++------ kernel/term_typing.ml | 20 ++++++++++---------- 3 files changed, 27 insertions(+), 17 deletions(-) (limited to 'kernel') diff --git a/kernel/entries.ml b/kernel/entries.ml index 3f33df3f74..62aab7c391 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -77,6 +77,16 @@ type section_def_entry = { secdef_type : types option; } +type 'a opaque_entry = { + opaque_entry_body : 'a; + (* List of section variables *) + opaque_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + opaque_entry_feedback : Stateid.t option; + opaque_entry_type : types option; + opaque_entry_universes : universes_entry; + opaque_entry_inline_code : bool } + type inline = int option (* inlining level, None for no inlining *) type parameter_entry = @@ -90,7 +100,7 @@ type primitive_entry = { type 'a constant_entry = | DefinitionEntry of constr Univ.in_universe_context_set definition_entry - | OpaqueEntry of 'a const_entry_body definition_entry + | OpaqueEntry of 'a const_entry_body opaque_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ab58321ac7..5dac469a40 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -690,12 +690,12 @@ let constant_entry_of_side_effect eff = | _ -> assert false in if Declareops.is_opaque cb then OpaqueEntry { - const_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); - const_entry_secctx = None; - const_entry_feedback = None; - const_entry_type = Some cb.const_type; - const_entry_universes = univs; - const_entry_inline_code = cb.const_inline_code } + opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); + opaque_entry_secctx = None; + opaque_entry_feedback = None; + opaque_entry_type = Some cb.const_type; + opaque_entry_universes = univs; + opaque_entry_inline_code = cb.const_inline_code } else DefinitionEntry { const_entry_body = (p, Univ.ContextSet.empty); diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 3b689953c8..2c31a237ce 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -115,11 +115,11 @@ 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. *) - | OpaqueEntry ({ const_entry_type = typ; - const_entry_universes = Monomorphic_entry univs; _ } as c) -> + | OpaqueEntry ({ opaque_entry_type = typ; + opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> let typ = match typ with None -> assert false | Some typ -> typ in 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 begin fun ((body,uctx),side_eff) -> @@ -151,16 +151,16 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_type = tyj.utj_val; cook_universes = Monomorphic univs; cook_relevance = Sorts.relevance_of_sort tyj.utj_type; - cook_inline = c.const_entry_inline_code; - cook_context = c.const_entry_secctx; + cook_inline = c.opaque_entry_inline_code; + cook_context = c.opaque_entry_secctx; } (** Similar case for polymorphic entries. *) - | OpaqueEntry ({ const_entry_type = typ; - const_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> + | OpaqueEntry ({ opaque_entry_type = typ; + opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> let typ = match typ with None -> assert false | Some typ -> typ 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 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 @@ -189,8 +189,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_type = typ; cook_universes = Polymorphic auctx; cook_relevance = Sorts.relevance_of_sort tj.utj_type; - cook_inline = c.const_entry_inline_code; - cook_context = c.const_entry_secctx; + cook_inline = c.opaque_entry_inline_code; + cook_context = c.opaque_entry_secctx; } (** Other definitions have to be processed immediately. *) -- cgit v1.2.3 From c20eb3a73c4868533bb50555d1979f5b9d821256 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 20 Jun 2019 08:22:28 +0200 Subject: Enforce that opaque entries carry their type. --- kernel/entries.ml | 2 +- kernel/safe_typing.ml | 2 +- kernel/term_typing.ml | 2 -- 3 files changed, 2 insertions(+), 4 deletions(-) (limited to 'kernel') diff --git a/kernel/entries.ml b/kernel/entries.ml index 62aab7c391..6016510189 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -83,7 +83,7 @@ type 'a opaque_entry = { opaque_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) opaque_entry_feedback : Stateid.t option; - opaque_entry_type : types option; + opaque_entry_type : types; opaque_entry_universes : universes_entry; opaque_entry_inline_code : bool } diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 5dac469a40..6cb7a22a15 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -693,7 +693,7 @@ let constant_entry_of_side_effect eff = opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); opaque_entry_secctx = None; opaque_entry_feedback = None; - opaque_entry_type = Some cb.const_type; + opaque_entry_type = cb.const_type; opaque_entry_universes = univs; opaque_entry_inline_code = cb.const_inline_code } else diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 2c31a237ce..86d79ba044 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -117,7 +117,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | OpaqueEntry ({ opaque_entry_type = typ; opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> - let typ = match typ with None -> assert false | Some typ -> typ in let env = push_context_set ~strict:true univs env in let { opaque_entry_body = body; opaque_entry_feedback = feedback_id; _ } = c in let tyj = Typeops.infer_type env typ in @@ -159,7 +158,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | OpaqueEntry ({ opaque_entry_type = typ; opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> - let typ = match typ with None -> assert false | Some typ -> typ in 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 -- cgit v1.2.3 From 5de7daa41e677798e4169a3e6350af0df12017e8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 20 Jun 2019 09:32:25 +0200 Subject: Remove the unused opaque_entry_inline_code field from opaque entries. --- kernel/entries.ml | 2 +- kernel/safe_typing.ml | 2 +- kernel/term_typing.ml | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel') diff --git a/kernel/entries.ml b/kernel/entries.ml index 6016510189..f73111d35f 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -85,7 +85,7 @@ type 'a opaque_entry = { opaque_entry_feedback : Stateid.t option; opaque_entry_type : types; opaque_entry_universes : universes_entry; - opaque_entry_inline_code : bool } +} type inline = int option (* inlining level, None for no inlining *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6cb7a22a15..a0cc2974d9 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -695,7 +695,7 @@ let constant_entry_of_side_effect eff = opaque_entry_feedback = None; opaque_entry_type = cb.const_type; opaque_entry_universes = univs; - opaque_entry_inline_code = cb.const_inline_code } + } else DefinitionEntry { const_entry_body = (p, Univ.ContextSet.empty); diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 86d79ba044..eca22869d2 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -150,7 +150,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_type = tyj.utj_val; cook_universes = Monomorphic univs; cook_relevance = Sorts.relevance_of_sort tyj.utj_type; - cook_inline = c.opaque_entry_inline_code; + cook_inline = false; cook_context = c.opaque_entry_secctx; } @@ -187,7 +187,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_type = typ; cook_universes = Polymorphic auctx; cook_relevance = Sorts.relevance_of_sort tj.utj_type; - cook_inline = c.opaque_entry_inline_code; + cook_inline = false; cook_context = c.opaque_entry_secctx; } -- cgit v1.2.3 From fd2daea8c6f2ab36125964c4e085377fd2ebdde3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 20 Jun 2019 09:39:28 +0200 Subject: Code simplification for definition_entry type. --- kernel/entries.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'kernel') diff --git a/kernel/entries.ml b/kernel/entries.ml index f73111d35f..2d29c3ee19 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -60,8 +60,8 @@ type mutual_inductive_entry = { type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation -type 'a definition_entry = { - const_entry_body : 'a; +type definition_entry = { + const_entry_body : constr Univ.in_universe_context_set; (* List of section variables *) const_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) @@ -99,7 +99,7 @@ type primitive_entry = { } type 'a constant_entry = - | DefinitionEntry of constr Univ.in_universe_context_set definition_entry + | DefinitionEntry of definition_entry | OpaqueEntry of 'a const_entry_body opaque_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry -- cgit v1.2.3