diff options
| -rw-r--r-- | kernel/entries.ml | 12 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 126 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 20 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 212 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 18 | ||||
| -rw-r--r-- | library/global.ml | 3 | ||||
| -rw-r--r-- | library/global.mli | 4 | ||||
| -rw-r--r-- | tactics/abstract.ml | 8 | ||||
| -rw-r--r-- | tactics/declare.ml | 67 | ||||
| -rw-r--r-- | tactics/declare.mli | 2 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 13 |
11 files changed, 263 insertions, 222 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 1e6bc14935..046ea86872 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -99,14 +99,10 @@ type primitive_entry = { type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation -(** Dummy wrapper type discriminable from unit *) -type 'a seff_wrap = { seff_wrap : 'a } - -type _ constant_entry = - | DefinitionEntry : definition_entry -> unit constant_entry - | OpaqueEntry : 'a const_entry_body opaque_entry -> 'a seff_wrap constant_entry - | ParameterEntry : parameter_entry -> unit constant_entry - | PrimitiveEntry : primitive_entry -> unit constant_entry +type constant_entry = + | DefinitionEntry : definition_entry -> constant_entry + | ParameterEntry : parameter_entry -> constant_entry + | PrimitiveEntry : primitive_entry -> constant_entry (** {6 Modules } *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 98465c070b..00559206ee 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -299,13 +299,6 @@ let lift_constant c = in { c with const_body = body } -let map_constant f c = - let body = match c.const_body with - | OpaqueDef o -> OpaqueDef (f o) - | Def _ | Undef _ | Primitive _ as body -> body - in - { c with const_body = body } - let push_private_constants env eff = let eff = side_effects_of_private_constants eff in let add_if_undefined env eff = @@ -579,13 +572,9 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv = let update_resolver f senv = { senv with modresolver = f senv.modresolver } -(** Insertion of constants and parameters in environment *) -type 'a effect_entry = -| EffectEntry : private_constants Entries.seff_wrap effect_entry -| PureEntry : unit effect_entry - type global_declaration = - | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration +| ConstantEntry : Entries.constant_entry -> global_declaration +| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration type exported_private_constant = Constant.t @@ -704,7 +693,7 @@ let check_signatures curmb sl = type side_effect_declaration = | DefinitionEff : Entries.definition_entry -> side_effect_declaration -| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration +| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration let constant_entry_of_side_effect eff = let cb = eff.seff_body in @@ -723,7 +712,7 @@ let constant_entry_of_side_effect eff = | _ -> assert false in if Declareops.is_opaque cb then OpaqueEff { - opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); + opaque_entry_body = p; opaque_entry_secctx = Context.Named.to_vars cb.const_hyps; opaque_entry_feedback = None; opaque_entry_type = cb.const_type; @@ -741,6 +730,25 @@ let constant_entry_of_side_effect eff = let export_eff eff = (eff.seff_constant, eff.seff_body) +let is_empty_private = function +| Opaqueproof.PrivateMonomorphic ctx -> Univ.ContextSet.is_empty ctx +| Opaqueproof.PrivatePolymorphic (_, ctx) -> Univ.ContextSet.is_empty ctx + +let empty_private univs = match univs with +| Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty +| Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty) + +(* Special function to call when the body of an opaque definition is provided. + It performs the type-checking of the body immediately. *) +let translate_direct_opaque env kn ce = + let cb, ctx = Term_typing.translate_opaque env kn ce in + let body = ce.Entries.opaque_entry_body, Univ.ContextSet.empty in + let handle _env c () = (c, Univ.ContextSet.empty, 0) in + let (c, u) = Term_typing.check_delayed handle ctx (body, ()) in + (* No constraints can be generated, we set it empty everywhere *) + let () = assert (is_empty_private u) in + { cb with const_body = OpaqueDef c } + let export_side_effects mb env (b_ctx, eff) = let not_exists e = try ignore(Environ.lookup_constant e.seff_constant env); false @@ -765,26 +773,14 @@ let export_side_effects mb env (b_ctx, eff) = if Int.equal sl 0 then let env, cb = let kn = eff.seff_constant in - let ce = constant_entry_of_side_effect eff in - let open Entries in - let open Term_typing in - let cb = match ce with - | DefinitionEff ce -> - Term_typing.translate_constant Pure env kn (DefinitionEntry ce) - | OpaqueEff ce -> - let handle _env c () = (c, Univ.ContextSet.empty, 0) in - Term_typing.translate_constant (SideEffects handle) env kn (OpaqueEntry ce) - in - let map cu = - let (c, u) = Future.force cu in - let () = match u with - | Opaqueproof.PrivateMonomorphic ctx - | Opaqueproof.PrivatePolymorphic (_, ctx) -> - assert (Univ.ContextSet.is_empty ctx) - in - c + let ce = constant_entry_of_side_effect eff in + let open Entries in + let cb = match ce with + | DefinitionEff ce -> + Term_typing.translate_constant env kn (DefinitionEntry ce) + | OpaqueEff ce -> + translate_direct_opaque env kn ce in - let cb = map_constant map cb in let eff = { eff with seff_body = cb } in (push_seff env eff, export_eff eff) in @@ -805,10 +801,7 @@ let export_private_constants ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in let map senv (kn, c) = match c.const_body with | OpaqueDef p -> - let local = match c.const_universes with - | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty - | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty) - in + let local = empty_private c.const_universes in let senv, o = push_opaque_proof (Future.from_val (p, local)) senv in senv, (kn, { c with const_body = OpaqueDef o }) | Def _ | Undef _ | Primitive _ as body -> @@ -820,19 +813,22 @@ let export_private_constants ce senv = let senv = List.fold_left add_constant_aux senv bodies in (ce, exported), senv -let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constant.t * a) * safe_environment = +let add_constant l decl senv = let kn = Constant.make2 senv.modpath l in - let cb = + let cb = match decl with - | ConstantEntry (EffectEntry, ce) -> + | OpaqueEntry ce -> let handle env body eff = let body, uctx, signatures = inline_side_effects env body eff in let trusted = check_signatures senv.revstruct signatures in body, uctx, trusted in - Term_typing.translate_constant (Term_typing.SideEffects handle) senv.env kn ce - | ConstantEntry (PureEntry, ce) -> - Term_typing.translate_constant Term_typing.Pure senv.env kn ce + let cb, ctx = Term_typing.translate_opaque senv.env kn ce in + let map pf = Term_typing.check_delayed handle ctx pf in + let pf = Future.chain ce.Entries.opaque_entry_body map in + { cb with const_body = OpaqueDef pf } + | ConstantEntry ce -> + Term_typing.translate_constant senv.env kn ce in let senv = let senv, cb, delayed_cst = match cb.const_body with @@ -860,37 +856,39 @@ let add_constant (type a) ~(side_effect : a effect_entry) l decl senv : (Constan let senv = match decl with - | ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) -> + | ConstantEntry (Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ }) -> if sections_are_opened senv then CErrors.anomaly (Pp.str "Primitive type not allowed in sections"); add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv | _ -> senv in - let eff : a = match side_effect with - | PureEntry -> () - | EffectEntry -> - let body, univs = match cb.const_body with - | (Primitive _ | Undef _) -> assert false - | Def c -> (Def c, cb.const_universes) - | OpaqueDef o -> - let (b, delayed) = Future.force o in - match cb.const_universes, delayed with - | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx -> - OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx') - | Polymorphic auctx, Opaqueproof.PrivatePolymorphic (_, ctx) -> - (* Upper layers enforce that there are no internal constraints *) - let () = assert (Univ.ContextSet.is_empty ctx) in - OpaqueDef b, Polymorphic auctx - | (Monomorphic _ | Polymorphic _), (Opaqueproof.PrivateMonomorphic _ | Opaqueproof.PrivatePolymorphic _) -> - assert false + kn, senv + +let add_private_constant l decl senv : (Constant.t * private_constants) * safe_environment = + let kn = Constant.make2 senv.modpath l in + let cb = + match decl with + | OpaqueEff ce -> + translate_direct_opaque senv.env kn ce + | DefinitionEff ce -> + Term_typing.translate_constant senv.env kn (Entries.DefinitionEntry ce) in - let cb = { cb with const_body = body; const_universes = univs } in + let senv, dcb = match cb.const_body with + | Def _ as const_body -> senv, { cb with const_body } + | OpaqueDef c -> + let local = empty_private cb.const_universes in + let senv, o = push_opaque_proof (Future.from_val (c, local)) senv in + senv, { cb with const_body = OpaqueDef o } + | Undef _ | Primitive _ -> assert false + in + let senv = add_constant_aux senv (kn, dcb) in + let eff = let from_env = CEphemeron.create senv.revstruct in let eff = { from_env = from_env; seff_constant = kn; seff_body = cb; } in - { Entries.seff_wrap = SideEffects.add eff empty_private_constants } + SideEffects.add eff empty_private_constants in (kn, eff), senv diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 1ce790ebbb..b2f6668577 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -73,12 +73,13 @@ val is_joined_environment : safe_environment -> bool (** Insertion of global axioms or definitions *) -type 'a effect_entry = -| EffectEntry : private_constants Entries.seff_wrap effect_entry -| PureEntry : unit effect_entry - type global_declaration = - | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration +| ConstantEntry : Entries.constant_entry -> global_declaration +| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration + +type side_effect_declaration = +| DefinitionEff : Entries.definition_entry -> side_effect_declaration +| OpaqueEff : Constr.constr Entries.opaque_entry -> side_effect_declaration type exported_private_constant = Constant.t @@ -86,10 +87,13 @@ val export_private_constants : private_constants Entries.proof_output -> (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer -(** returns the main constant plus a certificate of its validity *) +(** returns the main constant *) val add_constant : - side_effect:'a effect_entry -> Label.t -> global_declaration -> - (Constant.t * 'a) safe_transformer + Label.t -> global_declaration -> Constant.t safe_transformer + +(** Similar to add_constant but also returns a certificate *) +val add_private_constant : + Label.t -> side_effect_declaration -> (Constant.t * private_constants) safe_transformer (** Adding an inductive type *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f70b2960cf..f85b3db413 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -29,10 +29,6 @@ module NamedDecl = Context.Named.Declaration type 'a effect_handler = env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) -type _ trust = -| Pure : unit trust -| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust - let skip_trusted_seff sl b e = let rec aux sl b e acc = let open Context.Rel.Declaration in @@ -64,7 +60,11 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> Feedback.feedback ~id:state_id Feedback.Complete) -let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = +type typing_context = +| MonoTyCtx of Environ.env * unsafe_type_judgment * Univ.ContextSet.t * Id.Set.t * Stateid.t option +| PolyTyCtx of Environ.env * unsafe_type_judgment * Univ.universe_level_subst * Univ.AUContext.t * Id.Set.t * Stateid.t option + +let infer_declaration env (dcl : constant_entry) = match dcl with | ParameterEntry (ctx,(t,uctx),nl) -> let env = match uctx with @@ -112,79 +112,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_relevance = Sorts.Relevant; } - (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, - so we delay the typing and hash consing of its body. *) - - | OpaqueEntry ({ opaque_entry_type = typ; - opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> - 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 - let proofterm = - 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 SideEffects handle = trust in - let (body, uctx', valid_signatures) = handle env body side_eff in - let uctx = Univ.ContextSet.union uctx uctx' in - let env = push_context_set uctx env in - let body,env,ectx = skip_trusted_seff valid_signatures body env in - let j = Typeops.infer env body in - let j = unzip ectx j in - let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in - let c = j.uj_val in - feedback_completion_typecheck feedback_id; - 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_relevance = Sorts.relevance_of_sort tyj.utj_type; - cook_inline = false; - cook_context = Some c.opaque_entry_secctx; - } - - (** Similar case for polymorphic entries. *) - - | 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 proofterm = Future.chain body begin fun ((body, ctx), side_eff) -> - let SideEffects handle = trust in - let body, ctx', _ = handle env body side_eff in - let ctx = 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 - let def = Vars.subst_univs_level_constr usubst j.uj_val 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 - { - Cooking.cook_body = def; - cook_type = typ; - cook_universes = Polymorphic auctx; - cook_relevance = Sorts.relevance_of_sort tj.utj_type; - 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 - let Pure = trust in let env, usubst, univs = match c.const_entry_universes with | Monomorphic_entry ctx -> let env = push_context_set ~strict:true ctx env in @@ -218,25 +148,66 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_context = c.const_entry_secctx; } +(** Definition is opaque (Qed), so we delay the typing of its body. *) +let infer_opaque env = function + | ({ opaque_entry_type = typ; + opaque_entry_universes = Monomorphic_entry univs; _ } as c) -> + let env = push_context_set ~strict:true univs env in + let { opaque_entry_feedback = feedback_id; _ } = c in + let tyj = Typeops.infer_type env typ in + let context = MonoTyCtx (env, tyj, univs, c.opaque_entry_secctx, feedback_id) in + let def = OpaqueDef () in + { + Cooking.cook_body = def; + cook_type = tyj.utj_val; + cook_universes = Monomorphic univs; + cook_relevance = Sorts.relevance_of_sort tyj.utj_type; + cook_inline = false; + cook_context = Some c.opaque_entry_secctx; + }, context + + | ({ opaque_entry_type = typ; + opaque_entry_universes = Polymorphic_entry (nas, uctx); _ } as c) -> + let { 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 context = PolyTyCtx (env, tj, usubst, auctx, c.opaque_entry_secctx, feedback_id) in + let def = OpaqueDef () in + let typ = Vars.subst_univs_level_constr usubst tj.utj_val in + { + Cooking.cook_body = def; + cook_type = typ; + cook_universes = Polymorphic auctx; + cook_relevance = Sorts.relevance_of_sort tj.utj_type; + cook_inline = false; + cook_context = Some c.opaque_entry_secctx; + }, context + +let check_section_variables env declared_set typ body = + let ids_typ = global_vars_set env typ in + let ids_def = global_vars_set env body in + let inferred_set = Environ.really_needed env (Id.Set.union ids_typ ids_def) in + if not (Id.Set.subset inferred_set declared_set) then + let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in + let n = List.length l in + let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_set) in + let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_set) in + let missing_vars = Pp.pr_sequence Id.print (List.rev l) in + user_err Pp.(prlist str + ["The following section "; (String.plural n "variable"); " "; + (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++ + missing_vars ++ str "." ++ fnl () ++ fnl () ++ + str "You can either update your proof to not depend on " ++ missing_vars ++ + str ", or you can update your Proof line from" ++ fnl () ++ + str "Proof using " ++ declared_vars ++ fnl () ++ + str "to" ++ fnl () ++ + str "Proof using " ++ inferred_vars) + let build_constant_declaration env result = let open Cooking in let typ = result.cook_type in - let check declared_set inferred_set = - if not (Id.Set.subset inferred_set declared_set) then - let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in - let n = List.length l in - let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_set) in - let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_set) in - let missing_vars = Pp.pr_sequence Id.print (List.rev l) in - user_err Pp.(prlist str - ["The following section "; (String.plural n "variable"); " "; - (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++ - missing_vars ++ str "." ++ fnl () ++ fnl () ++ - str "You can either update your proof to not depend on " ++ missing_vars ++ - str ", or you can update your Proof line from" ++ fnl () ++ - str "Proof using " ++ declared_vars ++ fnl () ++ - str "to" ++ fnl () ++ - str "Proof using " ++ inferred_vars) in (* We try to postpone the computation of used section variables *) let hyps, def = let context_ids = List.map NamedDecl.get_id (named_context env) in @@ -265,22 +236,10 @@ let build_constant_declaration env result = (* We use the declared set and chain a check of correctness *) declared, match def with - | Undef _ | Primitive _ as x -> x (* nothing to check *) + | Undef _ | Primitive _ | OpaqueDef _ as x -> x (* nothing to check *) | Def cs as x -> - let ids_typ = global_vars_set env typ in - let ids_def = global_vars_set env (Mod_subst.force_constr cs) in - let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in - check declared inferred; - x - | OpaqueDef lc -> (* In this case we can postpone the check *) - let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in - let kont c = - let ids_typ = global_vars_set env typ in - let ids_def = global_vars_set env c in - let inferred = Environ.really_needed env (Id.Set.union ids_typ ids_def) in - check declared inferred - in - OpaqueDef (iter kont lc) + let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in + x in let univs = result.cook_universes in let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in @@ -297,11 +256,46 @@ let build_constant_declaration env result = const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } +let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_output) = match tyenv with +| MonoTyCtx (env, tyj, univs, declared, feedback_id) -> + let ((body, uctx), side_eff) = body in + (* don't redeclare universes which are declared for the type *) + let uctx = Univ.ContextSet.diff uctx univs in + let (body, uctx', valid_signatures) = handle env body side_eff in + let uctx = Univ.ContextSet.union uctx uctx' in + let env = push_context_set uctx env in + let body,env,ectx = skip_trusted_seff valid_signatures body env in + let j = Typeops.infer env body in + let j = unzip ectx j in + let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in + let c = j.uj_val in + let () = check_section_variables env declared tyj.utj_val body in + feedback_completion_typecheck feedback_id; + c, Opaqueproof.PrivateMonomorphic uctx +| PolyTyCtx (env, tj, usubst, auctx, declared, feedback_id) -> + let ((body, ctx), side_eff) = body in + let body, ctx', _ = handle env body side_eff in + let ctx = 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 + let () = check_section_variables env declared tj.utj_val body in + let def = Vars.subst_univs_level_constr usubst j.uj_val in + let () = feedback_completion_typecheck feedback_id in + def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs) + (*s Global and local constant declaration. *) -let translate_constant mb env _kn ce = +let translate_constant env _kn ce = build_constant_declaration env - (infer_declaration ~trust:mb env ce) + (infer_declaration env ce) + +let translate_opaque env _kn ce = + let def, ctx = infer_opaque env ce in + build_constant_declaration env def, ctx let translate_local_assum env t = let j = Typeops.infer env t in @@ -336,7 +330,7 @@ let translate_local_def env _id centry = const_entry_universes = Monomorphic_entry Univ.ContextSet.empty; const_entry_inline_code = false; } in - let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in + let decl = infer_declaration env (DefinitionEntry centry) in let typ = decl.cook_type in let () = match decl.cook_universes with | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index ef01ece185..c9f6d66e36 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -22,9 +22,7 @@ open Entries type 'a effect_handler = env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) -type _ trust = -| Pure : unit trust -| SideEffects : 'a effect_handler -> 'a Entries.seff_wrap trust +type typing_context val translate_local_def : env -> Id.t -> section_def_entry -> constr * Sorts.relevance * types @@ -32,15 +30,21 @@ val translate_local_def : env -> Id.t -> section_def_entry -> val translate_local_assum : env -> types -> types * Sorts.relevance val translate_constant : - 'a trust -> env -> Constant.t -> 'a constant_entry -> - Opaqueproof.proofterm constant_body + env -> Constant.t -> constant_entry -> + 'a constant_body + +val translate_opaque : + env -> Constant.t -> 'a opaque_entry -> + unit constant_body * typing_context val translate_recipe : env -> Constant.t -> Cooking.recipe -> Opaqueproof.opaque constant_body +val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes) + (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:'a trust -> env -> - 'a constant_entry -> Opaqueproof.proofterm Cooking.result +val infer_declaration : env -> + constant_entry -> typing_context Cooking.result val build_constant_declaration : env -> Opaqueproof.proofterm Cooking.result -> Opaqueproof.proofterm constant_body diff --git a/library/global.ml b/library/global.ml index 24cfc57f28..98d3e9cb1f 100644 --- a/library/global.ml +++ b/library/global.ml @@ -103,7 +103,8 @@ let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) let export_private_constants cd = globalize (Safe_typing.export_private_constants cd) -let add_constant ~side_effect id d = globalize (Safe_typing.add_constant ~side_effect (i2l id) d) +let add_constant id d = globalize (Safe_typing.add_constant (i2l id) d) +let add_private_constant id d = globalize (Safe_typing.add_private_constant (i2l id) d) let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl) diff --git a/library/global.mli b/library/global.mli index d689771f0a..f8b1f35f4d 100644 --- a/library/global.mli +++ b/library/global.mli @@ -51,7 +51,9 @@ val export_private_constants : Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list val add_constant : - side_effect:'a Safe_typing.effect_entry -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a + Id.t -> Safe_typing.global_declaration -> Constant.t +val add_private_constant : + Id.t -> Safe_typing.side_effect_declaration -> Constant.t * Safe_typing.private_constants val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t diff --git a/tactics/abstract.ml b/tactics/abstract.ml index edeb27ab88..03ab0a1c13 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -149,9 +149,12 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let (_, info) = CErrors.push src in iraise (e, info) in + let body, effs = Future.force const.Declare.proof_entry_body in + (* We drop the side-effects from the entry, they already exist in the ambient environment *) + let const = { const with Declare.proof_entry_body = Future.from_val (body, ()) } in let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in - let cd = Declare.DefinitionEntry { const with Declare.proof_entry_opaque = opaque } in + let cd = { const with Declare.proof_entry_opaque = opaque } in let kind = if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition) in let cst () = (* do not compute the implicit arguments, it may be costly *) @@ -172,8 +175,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let lem = mkConstU (cst, inst) in let evd = Evd.set_universe_context evd ectx in - let effs = Evd.concat_side_effects eff - (snd (Future.force const.Declare.proof_entry_body)) in + let effs = Evd.concat_side_effects eff effs in let solve = Proofview.tclEFFECTS effs <*> tacK lem args diff --git a/tactics/declare.ml b/tactics/declare.ml index 61321cd605..7d32f1a7e8 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -204,7 +204,11 @@ let cast_proof_entry e = const_entry_inline_code = e.proof_entry_inline_code; } -let cast_opaque_proof_entry e = +type ('a, 'b) effect_entry = +| EffectEntry : (private_constants, private_constants Entries.const_entry_body) effect_entry +| PureEntry : (unit, Constr.constr) effect_entry + +let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proof_entry) : b opaque_entry = let typ = match e.proof_entry_type with | None -> assert false | Some typ -> typ @@ -218,8 +222,15 @@ let cast_opaque_proof_entry e = Id.Set.empty, Id.Set.empty else let ids_typ = global_vars_set env typ in - let (pf, _), eff = Future.force e.proof_entry_body in - let env = Safe_typing.push_private_constants env eff in + let pf, env = match entry with + | PureEntry -> + let (pf, _), () = Future.force e.proof_entry_body in + pf, env + | EffectEntry -> + let (pf, _), eff = Future.force e.proof_entry_body in + let env = Safe_typing.push_private_constants env eff in + pf, env + in let vars = global_vars_set env pf in ids_typ, vars in @@ -227,12 +238,24 @@ let cast_opaque_proof_entry e = Environ.really_needed env (Id.Set.union hyp_typ hyp_def) | Some hyps -> hyps in + let (body, univs : b * _) = match entry with + | PureEntry -> + let (body, uctx), () = Future.force e.proof_entry_body in + let univs = match e.proof_entry_universes with + | Monomorphic_entry uctx' -> Monomorphic_entry (Univ.ContextSet.union uctx uctx') + | Polymorphic_entry _ -> + assert (Univ.ContextSet.is_empty uctx); + e.proof_entry_universes + in + body, univs + | EffectEntry -> e.proof_entry_body, e.proof_entry_universes + in { - opaque_entry_body = e.proof_entry_body; + opaque_entry_body = body; opaque_entry_secctx = secctx; opaque_entry_feedback = e.proof_entry_feedback; opaque_entry_type = typ; - opaque_entry_universes = e.proof_entry_universes; + opaque_entry_universes = univs; } let get_roles export eff = @@ -247,7 +270,7 @@ let is_unsafe_typing_flags () = let flags = Environ.typing_flags (Global.env()) in not (flags.check_universes && flags.check_guarded && flags.check_positive) -let define_constant ~side_effect ~name cd = +let define_constant ~name cd = (* Logically define the constant and its subproofs, no libobject tampering *) let export, decl, unsafe = match cd with | DefinitionEntry de -> @@ -259,39 +282,47 @@ let define_constant ~side_effect ~name cd = let export = get_roles export eff in let de = { de with proof_entry_body = Future.from_val (body, ()) } in let cd = Entries.DefinitionEntry (cast_proof_entry de) in - export, ConstantEntry (PureEntry, cd), false + export, ConstantEntry cd, false else let map (body, eff) = body, eff.Evd.seff_private in let body = Future.chain de.proof_entry_body map in let de = { de with proof_entry_body = body } in - let de = cast_opaque_proof_entry de in - [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de), false + let de = cast_opaque_proof_entry EffectEntry de in + [], OpaqueEntry de, false | ParameterEntry e -> - [], ConstantEntry (PureEntry, Entries.ParameterEntry e), not (Lib.is_modtype_strict()) + [], ConstantEntry (Entries.ParameterEntry e), not (Lib.is_modtype_strict()) | PrimitiveEntry e -> - [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e), false + [], ConstantEntry (Entries.PrimitiveEntry e), false in - let kn, eff = Global.add_constant ~side_effect name decl in + let kn = Global.add_constant name decl in if unsafe || is_unsafe_typing_flags() then feedback_axiom(); - kn, eff, export + kn, export let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd = let () = check_exists name in - let kn, (), export = define_constant ~side_effect:PureEntry ~name cd in + let kn, export = define_constant ~name cd in (* Register the libobjects attached to the constants and its subproofs *) let () = List.iter register_side_effect export in let () = register_constant kn kind local in kn -let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind cd = - let kn, eff, export = define_constant ~side_effect:EffectEntry ~name cd in - let () = assert (CList.is_empty export) in +let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind de = + let kn, eff = + let de = + if not de.proof_entry_opaque then + DefinitionEff (cast_proof_entry de) + else + let de = cast_opaque_proof_entry PureEntry de in + OpaqueEff de + in + Global.add_private_constant name de + in let () = register_constant kn kind local in let seff_roles = match role with | None -> Cmap.empty | Some r -> Cmap.singleton kn r in - let eff = { Evd.seff_private = eff.Entries.seff_wrap; Evd.seff_roles; } in + let eff = { Evd.seff_private = eff; Evd.seff_roles; } in kn, eff (** Declaration of section variables and local definitions *) diff --git a/tactics/declare.mli b/tactics/declare.mli index f4bfdb1547..a6c1374a77 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -78,7 +78,7 @@ val declare_private_constant -> ?local:import_status -> name:Id.t -> kind:Decls.logical_kind - -> Evd.side_effects constant_entry + -> unit proof_entry -> Constant.t * Evd.side_effects (** Since transparent constants' side effects are globally declared, we diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 54393dce00..3f824a94bf 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -124,8 +124,17 @@ let define internal role id c poly univs = let ctx = UState.minimize univs in let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in let univs = UState.univ_entry ~poly ctx in - let entry = Declare.definition_entry ~univs c in - let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in + let entry = { + Declare.proof_entry_body = + Future.from_val ((c,Univ.ContextSet.empty), ()); + proof_entry_secctx = None; + proof_entry_type = None; + proof_entry_universes = univs; + proof_entry_opaque = false; + proof_entry_inline_code = false; + proof_entry_feedback = None; + } in + let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in let () = match internal with | InternalTacticRequest -> () | _-> Declare.definition_message id |