diff options
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 123 |
1 files changed, 36 insertions, 87 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f984088f47..5844bd89f8 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -79,7 +79,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = Undef nl; cook_type = t; cook_universes = univs; - cook_private_univs = None; cook_relevance = r; cook_inline = false; cook_context = ctx; @@ -108,7 +107,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = cd; cook_type = ty; cook_universes = Monomorphic uctxt; - cook_private_univs = None; cook_inline = false; cook_context = None; cook_relevance = Sorts.Relevant; @@ -117,14 +115,13 @@ 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; - const_entry_universes = Monomorphic_entry univs; _ } as c) -> + | OpaqueEntry ({ opaque_entry_type = typ; + opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> 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 (fun ((body,uctx),side_eff) -> + Future.chain body begin fun ((body,uctx),side_eff) -> (* don't redeclare universes which are declared for the type *) let uctx = Univ.ContextSet.diff uctx univs in let j, uctx = match trust with @@ -145,31 +142,28 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = in let c = j.uj_val in feedback_completion_typecheck feedback_id; - c, uctx) in + c, Opaqueproof.PrivateMonomorphic uctx + end in let def = OpaqueDef proofterm in { Cooking.cook_body = def; cook_type = tyj.utj_val; cook_universes = Monomorphic univs; - cook_private_univs = None; cook_relevance = Sorts.relevance_of_sort tyj.utj_type; - cook_inline = c.const_entry_inline_code; - cook_context = c.const_entry_secctx; + cook_inline = false; + cook_context = Some c.opaque_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; - const_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> - let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in + | OpaqueEntry ({ opaque_entry_type = typ; + opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> + 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 let usubst = Univ.make_instance_subst sbst in - let (def, private_univs) = - let (body, ctx), side_eff = Future.join body in + let proofterm = Future.chain body begin fun ((body, ctx), side_eff) -> let body, ctx = match trust with | Pure -> body, ctx | SideEffects handle -> @@ -183,50 +177,39 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = 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 () = feedback_completion_typecheck feedback_id in + def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs) + end in + let def = OpaqueDef proofterm 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; + cook_inline = false; + 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; 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 + let () = match trust with + | Pure -> () | 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 + let env, usubst, univs = match c.const_entry_universes with + | Monomorphic_entry ctx -> let env = push_context_set ~strict:true ctx env in - env, Univ.empty_level_subst, Monomorphic ctx, None + env, Univ.empty_level_subst, Monomorphic ctx | Polymorphic_entry (nas, uctx) -> (** [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 sbst = Univ.make_instance_subst sbst in - let env, local = - if Univ.ContextSet.is_empty ctx then env, None - else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") - in - env, sbst, Polymorphic auctx, local + env, sbst, Polymorphic auctx in let j = Typeops.infer env body in let typ = match typ with @@ -244,23 +227,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = def; cook_type = typ; cook_universes = univs; - cook_private_univs = 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; } -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 @@ -292,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, @@ -341,7 +310,6 @@ let build_constant_declaration env result = const_type = typ; const_body_code = tps; const_universes = univs; - const_private_poly_univs = result.cook_private_univs; const_relevance = result.cook_relevance; const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } @@ -368,47 +336,28 @@ let translate_recipe env _kn r = const_type = result.cook_type; const_body_code = tps; const_universes = univs; - const_private_poly_univs = result.cook_private_univs; const_relevance = result.cook_relevance; const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } let translate_local_def env _id centry = let open Cooking in - let body = Future.from_val ((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; 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 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 () = assert (Univ.ContextSet.is_empty cst) in - p - | Undef _ | Primitive _ -> assert false + | Undef _ | Primitive _ | OpaqueDef _ -> assert false in c, decl.cook_relevance, typ |