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/term_typing.ml | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) (limited to 'kernel/term_typing.ml') 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/term_typing.ml | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) (limited to 'kernel/term_typing.ml') 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/term_typing.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'kernel/term_typing.ml') 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/term_typing.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'kernel/term_typing.ml') 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/term_typing.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'kernel/term_typing.ml') 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