diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.ml | 13 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 6 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 66 |
3 files changed, 24 insertions, 61 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 2d29c3ee19..bc389e9fcf 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -57,17 +57,15 @@ type mutual_inductive_entry = { } (** {6 Constants (Definition/Axiom) } *) -type 'a proof_output = constr Univ.in_universe_context_set * 'a -type 'a const_entry_body = 'a proof_output Future.computation type definition_entry = { - const_entry_body : constr Univ.in_universe_context_set; + const_entry_body : constr; (* List of section variables *) const_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; - const_entry_type : types option; - const_entry_universes : universes_entry; + const_entry_type : types option; + const_entry_universes : universes_entry; const_entry_inline_code : bool } type section_def_entry = { @@ -80,7 +78,7 @@ type section_def_entry = { type 'a opaque_entry = { opaque_entry_body : 'a; (* List of section variables *) - opaque_entry_secctx : Constr.named_context option; + opaque_entry_secctx : Constr.named_context; (* State id on which the completion of type checking is reported *) opaque_entry_feedback : Stateid.t option; opaque_entry_type : types; @@ -98,6 +96,9 @@ type primitive_entry = { prim_entry_content : CPrimitives.op_or_type; } +type 'a proof_output = constr Univ.in_universe_context_set * 'a +type 'a const_entry_body = 'a proof_output Future.computation + type 'a constant_entry = | DefinitionEntry of definition_entry | OpaqueEntry of 'a const_entry_body opaque_entry diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a0cc2974d9..2c434d4edf 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -691,15 +691,15 @@ let constant_entry_of_side_effect eff = if Declareops.is_opaque cb then OpaqueEntry { opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); - opaque_entry_secctx = None; + opaque_entry_secctx = cb.const_hyps; opaque_entry_feedback = None; opaque_entry_type = cb.const_type; opaque_entry_universes = univs; } else DefinitionEntry { - const_entry_body = (p, Univ.ContextSet.empty); - const_entry_secctx = None; + const_entry_body = p; + const_entry_secctx = Some cb.const_hyps; const_entry_feedback = None; const_entry_type = Some cb.const_type; const_entry_universes = univs; diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index eca22869d2..5844bd89f8 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -151,7 +151,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_universes = Monomorphic univs; cook_relevance = Sorts.relevance_of_sort tyj.utj_type; cook_inline = false; - cook_context = c.opaque_entry_secctx; + cook_context = Some c.opaque_entry_secctx; } (** Similar case for polymorphic entries. *) @@ -188,20 +188,19 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_universes = Polymorphic auctx; cook_relevance = Sorts.relevance_of_sort tj.utj_type; cook_inline = false; - cook_context = c.opaque_entry_secctx; + cook_context = Some c.opaque_entry_secctx; } (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> let { const_entry_type = typ; _ } = c in - let { const_entry_body = (body, ctx); const_entry_feedback = feedback_id; _ } = c in + let { const_entry_body = body; 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 - | Monomorphic_entry univs -> - let ctx = Univ.ContextSet.union univs ctx in + | Monomorphic_entry ctx -> let env = push_context_set ~strict:true ctx env in env, Univ.empty_level_subst, Monomorphic ctx | Polymorphic_entry (nas, uctx) -> @@ -210,10 +209,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = 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 () = - if not (Univ.ContextSet.is_empty ctx) then - CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") - in env, sbst, Polymorphic auctx in let j = Typeops.infer env body in @@ -237,17 +232,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_context = c.const_entry_secctx; } -let record_aux env s_ty s_bo = - let in_ty = keep_hyps env s_ty in - let v = - String.concat " " - (CList.map_filter (fun decl -> - let id = NamedDecl.get_id decl in - if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None - else Some (Id.to_string id)) - (keep_hyps env s_bo)) in - Aux_file.record_in_aux "context_used" v - let build_constant_declaration env result = let open Cooking in let typ = result.cook_type in @@ -279,24 +263,22 @@ let build_constant_declaration env result = let context_ids = List.map NamedDecl.get_id (named_context env) in let def = result.cook_body in match result.cook_context with - | None when not (List.is_empty context_ids) -> + | None -> + if List.is_empty context_ids then + (* Empty section context: no need to check *) + [], def + else (* No declared section vars, and non-empty section context: we must look at the body NOW, if any *) let ids_typ = global_vars_set env typ in let ids_def = match def with | Undef _ | Primitive _ -> Id.Set.empty | Def cs -> global_vars_set env (Mod_subst.force_constr cs) - | OpaqueDef lc -> - let (lc, _) = Future.force lc in - let vars = global_vars_set env lc in - if !Flags.record_aux_file then record_aux env ids_typ vars; - vars + | OpaqueDef _ -> + (* Opaque definitions always come with their section variables *) + assert false in keep_hyps env (Id.Set.union ids_typ ids_def), def - | None -> - if !Flags.record_aux_file then - record_aux env Id.Set.empty Id.Set.empty; - [], def (* Empty section context: no need to check *) | Some declared -> (* We use the declared set and chain a check of correctness *) sort declared, @@ -360,9 +342,8 @@ let translate_recipe env _kn r = let translate_local_def env _id centry = let open Cooking in - let body = (centry.secdef_body, Univ.ContextSet.empty) in let centry = { - const_entry_body = body; + const_entry_body = centry.secdef_body; const_entry_secctx = centry.secdef_secctx; const_entry_feedback = centry.secdef_feedback; const_entry_type = centry.secdef_type; @@ -371,31 +352,12 @@ let translate_local_def env _id centry = } in let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in let typ = decl.cook_type in - if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin - match decl.cook_body with - | Undef _ -> () - | Primitive _ -> () - | Def _ -> () - | OpaqueDef lc -> - let ids_typ = global_vars_set env typ in - let ids_def = global_vars_set env (fst (Future.force lc)) in - record_aux env ids_typ ids_def - end; let () = match decl.cook_universes with | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx) | Polymorphic _ -> assert false in let c = match decl.cook_body with | Def c -> Mod_subst.force_constr c - | OpaqueDef o -> - 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 () = 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 + | Undef _ | Primitive _ | OpaqueDef _ -> assert false in c, decl.cook_relevance, typ |