diff options
34 files changed, 299 insertions, 281 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index eb8161c2bb..7fbad3ea96 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,14 +1,12 @@ -let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = +let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps = let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false ~opaque ~poly sigma udecl ~types:tyopt ~body in let uctx = Evd.evar_universe_context sigma in let ubinders = Evd.universe_binders sigma in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - DeclareDef.declare_definition ident k ce ubinders imps ?hook_data + DeclareDef.declare_definition ~name ~scope ~kind ubinders ce imps ?hook_data -let declare_definition ~poly ident sigma body = - let k = Decl_kinds.(Global ImportDefaultBehavior, poly, Definition) in +let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in - edeclare ident k ~opaque:false sigma udecl body None [] - -(* But this definition cannot be undone by Reset ident *) + edeclare ~name ~poly ~scope:Decl_kinds.(Global ImportDefaultBehavior) + ~kind:Decl_kinds.Definition ~opaque:false sigma udecl body None [] diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 4b20016ab2..9fed8b7829 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -58,17 +58,12 @@ type assumption_object_kind = Definitional | Logical | Conjectural | Context Logical | Hypothesis | Axiom *) -type assumption_kind = locality * polymorphic * assumption_object_kind -type definition_kind = locality * polymorphic * definition_object_kind - (** Kinds used in proofs *) type goal_object_kind = | DefinitionBody of definition_object_kind | Proof of theorem_kind -type goal_kind = locality * goal_object_kind - (** Kinds used in library *) type logical_kind = diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 8c2cf3c553..e34150f2b3 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -20,7 +20,7 @@ let start_deriving f suchthat name : Lemmas.t = let env = Global.env () in let sigma = Evd.from_env env in let poly = false in - let kind = Decl_kinds.(Global ImportDefaultBehavior,DefinitionBody Definition) in + let kind = Decl_kinds.(DefinitionBody Definition) in (* create a sort variable for the type of [f] *) (* spiwack: I don't know what the rigidity flag does, picked the one @@ -40,8 +40,8 @@ let start_deriving f suchthat name : Lemmas.t = TNil sigma)))))) in - let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) () in - let lemma = Lemmas.start_dependent_lemma ~name ~poly ~kind ~info goals in + let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) ~kind () in + let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in Lemmas.pf_map (Proof_global.map_proof begin fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p end) lemma diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c37e6f7402..0d3c7b365f 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -990,13 +990,17 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num ] in (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) + let info = Lemmas.Info.make + ~scope:Decl_kinds.(Global ImportDefaultBehavior) + ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in + let lemma = Lemmas.start_lemma (*i The next call to mk_equation_id is valid since we are constructing the lemma Ensures by: obvious i*) ~name:(mk_equation_id f_id) ~poly:false - ~kind:(Decl_kinds.(Global ImportDefaultBehavior, Proof Theorem)) + ~info evd lemma_type in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 1b447bd26a..65b114fc03 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -311,7 +311,6 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin Lemmas.start_lemma ~name:new_princ_name ~poly:false - ~kind:(Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem)) !evd (EConstr.of_constr new_principle_type) in @@ -325,10 +324,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* end; *) let open Proof_global in - let { id; entries; persistence } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in + let { id; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in match entries with | [entry] -> - (id,(entry,persistence)), hook + id, entry, hook | _ -> CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") @@ -380,7 +379,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) register_with_sort InProp; register_with_sort InSet in - let ((id,(entry,g_kind)),hook) = + let id,entry,hook = build_functional_principle evd interactive_proof old_princ_type new_sorts funs i proof_tac hook in @@ -388,7 +387,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) Don't forget to close the goal if an error is raised !!!! *) let uctx = Evd.evar_universe_context sigma in - save new_princ_name entry ~hook uctx g_kind + save new_princ_name entry ~hook uctx Decl_kinds.(Global ImportDefaultBehavior) Decl_kinds.(Proof Theorem) with e when CErrors.noncritical e -> raise (Defining_principle e) @@ -519,7 +518,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Pro s::l_schemes -> s,l_schemes | _ -> anomaly (Pp.str "") in - let ((_,(const,_)),_) = + let _,const,_ = try build_functional_principle evd false first_type @@ -577,10 +576,10 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Pro ) ta; - (* If we reach this point, the two principle are not mutually recursive - We fall back to the previous method - *) - let ((_,(const,_)),_) = + (* If we reach this point, the two principle are not mutually recursive + We fall back to the previous method + *) + let _,const,_ = build_functional_principle evd false diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 0ecfbacb09..b07a92658b 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -416,8 +416,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in ComDefinition.do_definition ~program_mode:false - fname - Decl_kinds.(Global ImportDefaultBehavior,false,Definition) pl + ~name:fname + ~poly:false + ~scope:Decl_kinds.(Global ImportDefaultBehavior) + ~kind:Decl_kinds.Definition pl bl None body (Some ret_type); let evd,rev_pconstants = List.fold_left @@ -434,7 +436,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in None, evd,List.rev rev_pconstants | _ -> - ComFixpoint.do_fixpoint (Global ImportDefaultBehavior) false fixpoint_exprl; + ComFixpoint.do_fixpoint ~scope:(Global ImportDefaultBehavior) ~poly:false fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a5a07934ac..8745853180 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -123,7 +123,7 @@ open Declare let definition_message = Declare.definition_message -let save id const ?hook uctx (locality,kind) = +let save id const ?hook uctx locality kind = let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in let r = match locality with | Discharge -> diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 1d096fa488..602f7af57a 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -47,7 +47,8 @@ val save -> Evd.side_effects Proof_global.proof_entry -> ?hook:DeclareDef.Hook.t -> UState.t - -> Decl_kinds.goal_kind + -> Decl_kinds.locality + -> Decl_kinds.goal_object_kind -> unit (* [with_full_print f a] applies [f] to [a] in full printing environment. diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index e5b0a5d032..1ab64ac1b2 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -803,10 +803,13 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list i*) let lem_id = mk_correct_id f_id in let (typ,_) = lemmas_types_infos.(i) in + let info = Lemmas.Info.make + ~scope:Decl_kinds.(Global ImportDefaultBehavior) + ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false - ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem) + ~info !evd typ in let lemma = fst @@ Lemmas.by @@ -866,13 +869,14 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - let lemma = Lemmas.start_lemma ~name:lem_id - ~poly:false - ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem) sigma - (fst lemmas_types_infos.(i)) in + let info = Lemmas.Info.make + ~scope:Decl_kinds.(Global ImportDefaultBehavior) + ~kind:Decl_kinds.(Proof Theorem) () in + let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info + sigma (fst lemmas_types_infos.(i)) in let lemma = fst (Lemmas.by - (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") - (proving_tac i))) lemma) in + (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") + (proving_tac i))) lemma) in let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in let finfo = find_Function_infos (fst f_as_constant) in let _,lem_cst_constr = Evd.fresh_global diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 187d907dc5..6663fa5c60 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1367,11 +1367,12 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type in Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None in - let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in + let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) + ~scope:Decl_kinds.(Global ImportDefaultBehavior) ~kind:Decl_kinds.(Proof Lemma) + () in let lemma = Lemmas.start_lemma ~name:na - ~poly:false (* FIXME *) - ~kind:Decl_kinds.(Global ImportDefaultBehavior, Proof Lemma) ~info + ~poly:false (* FIXME *) ~info sigma gls_type in let lemma = if Indfun_common.is_strict_tcc () then @@ -1410,10 +1411,9 @@ let com_terminate nb_args ctx hook = let start_proof env ctx (tac_start:tactic) (tac_end:tactic) = - let info = Lemmas.Info.make ~hook () in + let info = Lemmas.Info.make ~hook ~scope:(Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in let lemma = Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) - ~kind:(Global ImportDefaultBehavior, Proof Lemma) ~sign:(Environ.named_context_val env) ~info ctx @@ -1462,7 +1462,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation let evd = Evd.from_ctx uctx in let f_constr = constr_of_monomorphic_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~kind:(Global ImportDefaultBehavior, Proof Lemma) ~sign evd + let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~sign evd (EConstr.of_constr equation_lemma_type) in let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (start_equation f_ref terminate_ref diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index d87b7a1770..8d95c22529 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1995,9 +1995,7 @@ let add_morphism_interactive atts m n : Lemmas.t = let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in let poly = atts.polymorphic in - let kind = Decl_kinds.(Global ImportDefaultBehavior), - Decl_kinds.DefinitionBody Decl_kinds.Instance - in + let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in let hook _ _ _ = function | Globnames.ConstRef cst -> @@ -2008,10 +2006,10 @@ let add_morphism_interactive atts m n : Lemmas.t = | _ -> assert false in let hook = DeclareDef.Hook.make hook in - let info = Lemmas.Info.make ~hook () in + let info = Lemmas.Info.make ~hook ~kind () in Flags.silently (fun () -> - let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~kind ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in + let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in fst (Lemmas.by (Tacinterp.interp tac) lemma)) () let add_morphism atts binders m s n = diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 98002de119..7af14d099c 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -112,14 +112,12 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t (**********************************************************************) (* Shortcut to build a term using tactics *) -open Decl_kinds - let next = let n = ref 0 in fun () -> incr n; !n -let build_constant_by_tactic id ctx sign ~poly ?(goal_kind = Global ImportDefaultBehavior, Proof Theorem) typ tac = +let build_constant_by_tactic ~name ctx sign ~poly typ tac = let evd = Evd.from_ctx ctx in let goals = [ (Global.env_of_context sign , typ) ] in - let pf = Proof_global.start_proof ~name:id ~poly ~udecl:UState.default_univ_decl ~kind:goal_kind evd goals in + let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in try let pf, status = by tac pf in let open Proof_global in @@ -135,11 +133,9 @@ let build_constant_by_tactic id ctx sign ~poly ?(goal_kind = Global ImportDefaul iraise reraise let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = - let id = Id.of_string ("temporary_proof"^string_of_int (next())) in + let name = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in - let gk = Global ImportDefaultBehavior, Proof Theorem in - let ce, status, univs = - build_constant_by_tactic id sigma sign ~poly ~goal_kind:gk typ tac in + let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in let body, eff = Future.force ce.Proof_global.proof_entry_body in let (cb, ctx) = if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 51cb3ca0ee..d1d20b9efe 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -59,11 +59,10 @@ val use_unification_heuristics : unit -> bool tactic. *) val build_constant_by_tactic - : Id.t + : name:Id.t -> UState.t -> named_context_val -> poly:bool - -> ?goal_kind:goal_kind -> EConstr.types -> unit Proofview.tactic -> Evd.side_effects Proof_global.proof_entry * bool * UState.t diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 8ac4435539..59ece4296b 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -40,7 +40,6 @@ type proof_object = { id : Names.Id.t ; entries : Evd.side_effects proof_entry list ; poly : bool - ; persistence : Decl_kinds.goal_kind ; universes: UState.t ; udecl : UState.universe_decl } @@ -52,14 +51,12 @@ type t = ; section_vars : Constr.named_context option ; proof : Proof.t ; udecl: UState.universe_decl - ; strength : Decl_kinds.goal_kind } (*** Proof Global manipulation ***) let get_proof ps = ps.proof let get_proof_name ps = (Proof.data ps.proof).Proof.name -let get_persistence ps = ps.strength let map_proof f p = { p with proof = f p.proof } let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res @@ -86,28 +83,23 @@ let compact_the_proof pf = map_proof Proof.compact pf let set_endline_tactic tac ps = { ps with endline_tactic = Some tac } -(** [start_proof sigma id pl str goals] starts a proof of name - [id] with goals [goals] (a list of pairs of environment and - conclusion); [str] describes what kind of theorem/definition this - is (spiwack: for potential printing, I believe is used only by - closing commands and the xml plugin); [terminator] is used at the - end of the proof to close the proof. The proof is started in the - evar map [sigma] (which can typically contain universe - constraints), and with universe bindings pl. *) -let start_proof ~name ~udecl ~poly ~kind sigma goals = +(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of + name [name] with goals [goals] (a list of pairs of environment and + conclusion). The proof is started in the evar map [sigma] (which + can typically contain universe constraints), and with universe + bindings [udecl]. *) +let start_proof ~name ~udecl ~poly sigma goals = { proof = Proof.start ~name ~poly sigma goals ; endline_tactic = None ; section_vars = None ; udecl - ; strength = kind } -let start_dependent_proof ~name ~udecl ~poly ~kind goals = +let start_dependent_proof ~name ~udecl ~poly goals = { proof = Proof.dependent_start ~name ~poly goals ; endline_tactic = None ; section_vars = None ; udecl - ; strength = kind } let get_used_variables pf = pf.section_vars @@ -162,7 +154,7 @@ let private_poly_univs = let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now (fpl : closed_proof_output Future.computation) ps = - let { section_vars; proof; udecl; strength } = ps in + let { section_vars; proof; udecl } = ps in let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in let opaque = match opaque with Opaque -> true | Transparent -> false in let constrain_variables ctx = @@ -256,7 +248,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now proof_entry_universes = univs; } in let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in - { id = name; entries = entries; poly; persistence = strength; universes; udecl } + { id = name; entries = entries; poly; universes; udecl } let return_proof ?(allow_partial=false) ps = let { proof } = ps in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 2c328bcf12..b402008361 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -17,7 +17,6 @@ type t (* Should be moved into a proper view *) val get_proof : t -> Proof.t val get_proof_name : t -> Names.Id.t -val get_persistence : t -> Decl_kinds.goal_kind val get_used_variables : t -> Constr.named_context option (** Get the universe declaration associated to the current proof. *) @@ -47,7 +46,6 @@ type proof_object = { id : Names.Id.t ; entries : Evd.side_effects proof_entry list ; poly : bool - ; persistence : Decl_kinds.goal_kind ; universes: UState.t ; udecl : UState.universe_decl } @@ -66,7 +64,6 @@ val start_proof : name:Names.Id.t -> udecl:UState.universe_decl -> poly:bool - -> kind:Decl_kinds.goal_kind -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t @@ -77,7 +74,6 @@ val start_dependent_proof : name:Names.Id.t -> udecl:UState.universe_decl -> poly:bool - -> kind:Decl_kinds.goal_kind -> Proofview.telescope -> t diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 68a2a0afe0..4ea5b676fb 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -86,10 +86,10 @@ let shrink_entry sign const = } in (const, args) -let name_op_to_name ~name_op ~name ~goal_kind suffix = +let name_op_to_name ~name_op ~name suffix = match name_op with - | Some s -> s, goal_kind - | None -> Nameops.add_suffix name suffix, goal_kind + | Some s -> s + | None -> Nameops.add_suffix name suffix let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let open Tacticals.New in @@ -102,10 +102,10 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = redundancy on constant declaration. This opens up an interesting question, how does abstract behave when discharge is local for example? *) - let goal_kind, suffix = if opaque - then (Global ImportDefaultBehavior,Proof Theorem), "_subproof" - else (Global ImportDefaultBehavior,DefinitionBody Definition), "_subterm" in - let id, goal_kind = name_op_to_name ~name_op ~name ~goal_kind suffix in + let scope, suffix = if opaque + then Global ImportDefaultBehavior, "_subproof" + else Global ImportDefaultBehavior, "_subterm" in + let name = name_op_to_name ~name_op ~name suffix in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in @@ -121,7 +121,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = then (s1,push_named_context_val d s2) else (Context.Named.add d s1,s2)) global_sign (Context.Named.empty, Environ.empty_named_context_val) in - let id = Namegen.next_global_ident_away id (pf_ids_set_of_hyps gl) in + let name = Namegen.next_global_ident_away name (pf_ids_set_of_hyps gl) in let concl = match goal_type with | None -> Proofview.Goal.concl gl | Some ty -> ty in @@ -141,7 +141,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in let ectx = Evd.evar_universe_context evd in let (const, safe, ectx) = - try Pfedit.build_constant_by_tactic ~poly ~goal_kind id ectx secsign concl solve_tac + try Pfedit.build_constant_by_tactic ~poly ~name ectx secsign concl solve_tac with Logic_monad.TacticFailure e as src -> (* if the tactic [tac] fails, it reports a [TacticFailure e], which is an error irrelevant to the proof system (in fact it @@ -158,7 +158,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = (* do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in (* ppedrot: seems legit to have abstracted subproofs as local*) - Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl + Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified name decl in let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Proof_global.proof_entry_universes with diff --git a/vernac/classes.ml b/vernac/classes.ml index bb5ebd7148..c8ae9928a3 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -362,9 +362,8 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt in let hook = DeclareDef.Hook.make hook in let ctx = Evd.evar_universe_context sigma in - ignore(Obligations.add_definition id ?term:constr - ~univdecl:decl typ ctx ~kind:(Global ImportDefaultBehavior,poly,Instance) ~hook obls) - + ignore(Obligations.add_definition ~name:id ?term:constr + ~univdecl:decl ~scope:(Global ImportDefaultBehavior) ~poly ~kind:Instance ~hook typ ctx obls) let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype = (* spiwack: it is hard to reorder the actions to do @@ -373,10 +372,11 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t the refinement manually.*) let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in - let kind = Decl_kinds.Global ImportDefaultBehavior, Decl_kinds.DefinitionBody Decl_kinds.Instance in + let scope = Decl_kinds.(Global ImportDefaultBehavior) in + let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in let hook = DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook) in - let info = Lemmas.Info.make ~hook () in - let lemma = Lemmas.start_lemma ~name:id ~poly ~kind ~udecl ~info sigma (EConstr.of_constr termtype) in + let info = Lemmas.Info.make ~hook ~scope ~kind () in + let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma (EConstr.of_constr termtype) in (* spiwack: I don't know what to do with the status here. *) let lemma = if not (Option.is_empty term) then diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index b0297b7c51..febe28879f 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -43,14 +43,14 @@ let should_axiom_into_instance = function true | Definitional | Logical | Conjectural -> !axiom_into_instance -let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} = -match local with +let declare_assumption is_coe ~poly ~scope ~kind (c,ctx) pl imps impl nl {CAst.v=ident} = +match scope with | Discharge -> let ctx = match ctx with | Monomorphic_entry ctx -> ctx | Polymorphic_entry (_, ctx) -> Univ.ContextSet.of_context ctx in - let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in + let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),poly,impl), IsAssumption kind) in let _ = declare_variable ident decl in let () = assumption_message ident in let r = VarRef ident in @@ -78,7 +78,7 @@ match local with let sigma = Evd.from_env env in let () = if do_instance then Classes.declare_instance env sigma None false gr in let local = match local with ImportNeedQualified -> true | ImportDefaultBehavior -> false in - let () = if is_coe then Class.try_add_new_coercion gr ~local p in + let () = if is_coe then Class.try_add_new_coercion gr ~local poly in let inst = match ctx with | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx | Monomorphic_entry _ -> Univ.Instance.empty @@ -96,11 +96,11 @@ let next_uctx = | Polymorphic_entry _ as uctx -> uctx | Monomorphic_entry _ -> empty_uctx -let declare_assumptions idl is_coe k (c,uctx) pl imps nl = +let declare_assumptions idl is_coe ~scope ~poly ~kind (c,uctx) pl imps nl = let refs, status, _ = List.fold_left (fun (refs,status,uctx) id -> let ref',u',status' = - declare_assumption is_coe k (c,uctx) pl imps false nl id in + declare_assumption is_coe ~scope ~poly ~kind (c,uctx) pl imps false nl id in (ref',u')::refs, status' && status, next_uctx uctx) ([],true,uctx) idl in @@ -115,7 +115,7 @@ let maybe_error_many_udecls = function str "(which will be shared by the whole block).") | (_, None) -> () -let process_assumptions_udecls kind l = +let process_assumptions_udecls ~scope l = let udecl, first_id = match l with | (coe, ((id, udecl)::rest, c))::rest' -> List.iter maybe_error_many_udecls rest; @@ -123,8 +123,8 @@ let process_assumptions_udecls kind l = udecl, id | (_, ([], _))::_ | [] -> assert false in - let () = match kind, udecl with - | (Discharge, _, _), Some _ -> + let () = match scope, udecl with + | Discharge, Some _ -> let loc = first_id.CAst.loc in let msg = Pp.str "Section variables cannot be polymorphic." in user_err ?loc msg @@ -132,13 +132,13 @@ let process_assumptions_udecls kind l = in udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l -let do_assumptions ~program_mode kind nl l = +let do_assumptions ~program_mode ~poly ~scope ~kind nl l = let open Context.Named.Declaration in let env = Global.env () in - let udecl, l = process_assumptions_udecls kind l in + let udecl, l = process_assumptions_udecls ~scope l in let sigma, udecl = interp_univ_decl_opt env udecl in let l = - if pi2 kind (* poly *) then + if poly then (* Separate declarations so that A B : Type puts A and B in different levels. *) List.fold_right (fun (is_coe,(idl,c)) acc -> List.fold_right (fun id acc -> @@ -174,11 +174,11 @@ let do_assumptions ~program_mode kind nl l = IMO, thus I think we should adapt `prepare_parameter` to handle this case too. *) let sigma = Evd.restrict_universe_context sigma uvars in - let uctx = Evd.check_univ_decl ~poly:(pi2 kind) sigma udecl in + let uctx = Evd.check_univ_decl ~poly sigma udecl in let ubinders = Evd.universe_binders sigma in pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) -> let t = replace_vars subst t in - let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in + let refs, status' = declare_assumptions idl is_coe ~poly ~scope ~kind (t,uctx) ubinders imps nl in let subst' = List.map2 (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u))) idl refs @@ -288,17 +288,15 @@ let context poly l = | _ -> false in let impl = List.exists test impls in - let persistence = + let scope = if Lib.sections_are_opened () then Discharge else Global ImportDefaultBehavior in - let decl = (persistence, poly, Context) in let nstatus = match b with | None -> - pi3 (declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl + pi3 (declare_assumption false ~scope ~poly ~kind:Context (t, univs) UnivNames.empty_binders [] impl Declaremods.NoInline (CAst.make id)) | Some b -> - let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~univs ~types:t b in - let _gr = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] in + let _gr = DeclareDef.declare_definition ~name:id ~scope:Discharge ~kind:Definition UnivNames.empty_binders entry [] in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 07e96d87a2..67fa94ceb8 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -16,8 +16,10 @@ open Decl_kinds (** {6 Parameters/Assumptions} *) val do_assumptions - : program_mode:bool - -> locality * polymorphic * assumption_object_kind + : program_mode:bool + -> poly:polymorphic + -> scope:locality + -> kind:assumption_object_kind -> Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list -> bool @@ -26,7 +28,9 @@ val do_assumptions nor in a module type and meant to be instantiated. *) val declare_assumption : coercion_flag - -> assumption_kind + -> poly:bool + -> scope:Decl_kinds.locality + -> kind:assumption_object_kind -> Constr.types Entries.in_universes_entry -> UnivNames.universe_binders -> Impargs.manual_implicits diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index b3cc0a4236..3d5ea319bb 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -79,9 +79,9 @@ let check_definition ~program_mode (ce, evd, _, imps) = check_evars_are_solved ~program_mode env evd; ce -let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = +let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_option c ctypopt = let (ce, evd, univdecl, imps as def) = - interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt + interp_definition ~program_mode univdecl bl poly red_option c ctypopt in if program_mode then let env = Global.env () in @@ -95,13 +95,13 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = | None -> Retyping.get_type_of env evd c in let obls, _, c, cty = - Obligations.eterm_obligations env ident evd 0 c typ + Obligations.eterm_obligations env name evd 0 c typ in let ctx = Evd.evar_universe_context evd in ignore(Obligations.add_definition - ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ?hook obls) + ~name ~term:c cty ctx ~univdecl ~implicits:imps ~scope ~poly ~kind ?hook obls) else let ce = check_definition ~program_mode def in let uctx = Evd.evar_universe_context evd in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps) + ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 256abed6a1..ec59916e3c 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -16,10 +16,12 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition - : program_mode:bool + : program_mode:bool -> ?hook:DeclareDef.Hook.t - -> Id.t - -> definition_kind + -> name:Id.t + -> scope:locality + -> poly:bool + -> kind:definition_object_kind -> universe_decl_expr option -> local_binder_expr list -> red_expr option diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 6d9aa746b9..e3428d6afc 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -255,7 +255,7 @@ let interp_fixpoint ~cofix l ntns = let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) -let declare_fixpoint_interactive_generic ?indexes local poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns = +let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns = let fix_kind, cofix, indexes = match indexes with | Some indexes -> Fixpoint, false, indexes | None -> CoFixpoint, true, [] @@ -269,13 +269,13 @@ let declare_fixpoint_interactive_generic ?indexes local poly ((fixnames,_fixrs,f Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in let lemma = - Lemmas.start_lemma_with_initialization ~poly ~kind:(local,DefinitionBody fix_kind) ~udecl + Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(DefinitionBody fix_kind) ~udecl evd (Some(cofix,indexes,init_tac)) thms None in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; lemma -let declare_fixpoint_generic ?indexes local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = +let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = let indexes, cofix, fix_kind = match indexes with | Some indexes -> indexes, false, Fixpoint @@ -303,7 +303,7 @@ let declare_fixpoint_generic ?indexes local poly ((fixnames,fixrs,fixdefs,fixtyp let pl = Evd.universe_binders evd in let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in let fixdecls = List.map mk_pure fixdecls in - ignore (List.map4 (DeclareDef.declare_fix (local, poly, fix_kind) pl ctx) + ignore (List.map4 (fun name -> DeclareDef.declare_fix ~name ~scope ~kind:fix_kind pl ctx) fixnames fixdecls fixtypes fiximps); recursive_message (not cofix) gidx fixnames; List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; @@ -351,28 +351,28 @@ let do_fixpoint_common l = let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in fixl, ntns, fix, List.map compute_possible_guardness_evidences info -let do_fixpoint_interactive local poly l : Lemmas.t = +let do_fixpoint_interactive ~scope ~poly l : Lemmas.t = let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in - let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes local poly fix ntns in + let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); lemma -let do_fixpoint local poly l = +let do_fixpoint ~scope ~poly l = let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in - declare_fixpoint_generic ~indexes:possible_indexes local poly fix ntns; + declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () let do_cofixpoint_common l = let fixl,ntns = extract_cofixpoint_components l in ntns, interp_fixpoint ~cofix:true fixl ntns -let do_cofixpoint_interactive local poly l = +let do_cofixpoint_interactive ~scope ~poly l = let ntns, cofix = do_cofixpoint_common l in - let lemma = declare_fixpoint_interactive_generic local poly cofix ntns in + let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); lemma -let do_cofixpoint local poly l = +let do_cofixpoint ~scope ~poly l = let ntns, cofix = do_cofixpoint_common l in - declare_fixpoint_generic local poly cofix ntns; + declare_fixpoint_generic ~scope ~poly cofix ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 8d76a30cee..c04cc95837 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -19,16 +19,16 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint_interactive : - locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Lemmas.t + scope:locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> Lemmas.t val do_fixpoint : - locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit + scope:locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint_interactive : - locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t + scope:locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t val do_cofixpoint : - locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit + scope:locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit (************************************************************************) (** Internal API *) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 6c1c23eacb..d804957917 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -234,8 +234,8 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = Obligations.eterm_obligations env recname sigma 0 def typ in let ctx = Evd.evar_universe_context sigma in - ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl - evars_typ ctx evars ~hook) + ignore(Obligations.add_definition ~name:recname ~term:evars_def ~univdecl:decl + ~poly evars_typ ctx evars ~hook) let out_def = function | Some def -> def @@ -246,7 +246,7 @@ let collect_evars_of_term evd c ty = Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) -let do_program_recursive local poly fixkind fixl ntns = +let do_program_recursive ~scope ~poly fixkind fixl ntns = let cofix = fixkind = DeclareObl.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = interp_recursive ~cofix ~program_mode:true fixl ntns @@ -288,12 +288,12 @@ let do_program_recursive local poly fixkind fixl ntns = end in let ctx = Evd.evar_universe_context evd in let kind = match fixkind with - | DeclareObl.IsFixpoint _ -> (local, poly, Fixpoint) - | DeclareObl.IsCoFixpoint -> (local, poly, CoFixpoint) + | DeclareObl.IsFixpoint _ -> Fixpoint + | DeclareObl.IsCoFixpoint -> CoFixpoint in - Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind + Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind -let do_program_fixpoint local poly l = +let do_program_fixpoint ~scope ~poly l = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in match g, l with | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> @@ -316,7 +316,7 @@ let do_program_fixpoint local poly l = | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> let fixl,ntns = extract_fixpoint_components ~structonly:true l in let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in - do_program_recursive local poly fixkind fixl ntns + do_program_recursive ~scope ~poly fixkind fixl ntns | _, _ -> user_err ~hdr:"do_program_fixpoint" @@ -334,11 +334,11 @@ let check_safe () = let flags = Environ.typing_flags (Global.env ()) in flags.check_universes && flags.check_guarded -let do_fixpoint local poly l = - do_program_fixpoint local poly l; +let do_fixpoint ~scope ~poly l = + do_program_fixpoint ~scope ~poly l; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () -let do_cofixpoint local poly l = +let do_cofixpoint ~scope ~poly l = let fixl,ntns = extract_cofixpoint_components l in - do_program_recursive local poly DeclareObl.IsCoFixpoint fixl ntns; + do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli index 943cb8efe6..ba735f9c10 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -5,8 +5,8 @@ open Vernacexpr val do_fixpoint : (* When [false], assume guarded. *) - locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit + scope:locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint : (* When [false], assume guarded. *) - locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit + scope:locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index a467c22ede..e82fb3e3b1 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -36,31 +36,31 @@ module Hook = struct end (* Locality stuff *) -let declare_definition ident (local, p, k) ?hook_data ce pl imps = +let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in - let gr = match local with + let gr = match scope with | Discharge -> - let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in - VarRef ident + let _ = declare_variable name (Lib.cwd(), SectionLocalDef ce, IsDefinition kind) in + VarRef name | Global local -> - let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in + let kn = declare_constant name ~local (DefinitionEntry ce, IsDefinition kind) in let gr = ConstRef kn in - let () = Declare.declare_univ_binders gr pl in + let () = Declare.declare_univ_binders gr udecl in gr in let () = maybe_declare_manual_implicits false gr imps in - let () = definition_message ident in + let () = definition_message name in begin match hook_data with | None -> () | Some (hook, uctx, extra_defs) -> - Hook.call ~fix_exn ~hook uctx extra_defs local gr + Hook.call ~fix_exn ~hook uctx extra_defs scope gr end; gr -let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = +let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~univs ~eff def in - declare_definition f kind ?hook_data ce pl imps + declare_definition ~name ~scope ~kind ?hook_data udecl ce imps let check_definition_evars ~allow_evars sigma = let env = Global.env () in diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index ac4f44608b..708158814e 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -40,21 +40,23 @@ module Hook : sig end val declare_definition - : Id.t - -> definition_kind + : name:Id.t + -> scope:locality + -> kind:definition_object_kind -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> Evd.side_effects Proof_global.proof_entry -> UnivNames.universe_binders + -> Evd.side_effects Proof_global.proof_entry -> Impargs.manual_implicits -> GlobRef.t val declare_fix - : ?opaque:bool + : ?opaque:bool -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> definition_kind + -> name:Id.t + -> scope:locality + -> kind:definition_object_kind -> UnivNames.universe_binders -> Entries.universes_entry - -> Id.t -> Evd.side_effects Entries.proof_output -> Constr.types -> Impargs.manual_implicits diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 4936c9838d..1790932c23 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -48,7 +48,9 @@ type program_info = ; prg_fixkind : fixpoint_kind option ; prg_implicits : Impargs.manual_implicits ; prg_notations : notations - ; prg_kind : definition_kind + ; prg_poly : bool + ; prg_scope : locality + ; prg_kind : definition_object_kind ; prg_reduce : constr -> constr ; prg_hook : DeclareDef.Hook.t option ; prg_opaque : bool @@ -146,7 +148,7 @@ let declare_obligation prg obl body ty uctx = | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)}) | force, Evar_kinds.Define opaque -> let opaque = (not force) && opaque in - let poly = pi2 prg.prg_kind in + let poly = prg.prg_poly in let ctx, body, ty, args = if get_shrink_obligations () && not poly then shrink_body body ty else ([], body, ty, [||]) @@ -355,13 +357,14 @@ let declare_definition prg = in let uctx = UState.restrict prg.prg_ctx uvars in let univs = - UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl + UState.check_univ_decl ~poly:prg.prg_poly uctx prg.prg_univdecl in let ce = Declare.definition_entry ~fix_exn ~opaque ~types:typ ~univs body in let () = progmap_remove prg in let ubinders = UState.universe_binders uctx in let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in - DeclareDef.declare_definition prg.prg_name prg.prg_kind ce ubinders + DeclareDef.declare_definition + ~name:prg.prg_name ~scope:prg.prg_scope ubinders ~kind:prg.prg_kind ce prg.prg_implicits ?hook_data let rec lam_index n t acc = @@ -418,7 +421,6 @@ let declare_mutual_definition l = let rvec = Array.of_list fixrs in let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in - let local, poly, kind = first.prg_kind in let fixnames = first.prg_deps in let opaque = first.prg_opaque in let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in @@ -438,12 +440,14 @@ let declare_mutual_definition l = (None, List.map_i (fun i _ -> mk_proof (mkCoFix (i, fixdecls))) 0 l) in (* Declare the recursive definitions *) + let poly = first.prg_poly in + let scope = first.prg_scope in let univs = UState.univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in let kns = List.map4 - (DeclareDef.declare_fix ~opaque (local, poly, kind) - UnivNames.empty_binders univs) + (fun name -> DeclareDef.declare_fix ~name ~opaque ~scope ~kind + UnivNames.empty_binders univs) fixnames fixdecls fixtypes fiximps in (* Declare notations *) @@ -452,7 +456,7 @@ let declare_mutual_definition l = first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in - DeclareDef.Hook.call ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr; + DeclareDef.Hook.call ?hook:first.prg_hook ~fix_exn first.prg_ctx obls scope gr; List.iter progmap_remove l; gr @@ -523,15 +527,15 @@ let obligation_terminator opq entries uctx { name; num; auto } = in let obl = { obl with obl_status = false, status } in let ctx = - if pi2 prg.prg_kind then ctx + if prg.prg_poly then ctx else UState.union prg.prg_ctx ctx in - let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in let (defined, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let () = obls.(num) <- obl in let prg_ctx = - if pi2 (prg.prg_kind) then (* Polymorphic *) + if prg.prg_poly then (* Polymorphic *) (* We merge the new universes and constraints of the polymorphic obligation with the existing ones *) UState.union prg.prg_ctx ctx diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index f4495181b3..4774d73aa7 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -42,7 +42,9 @@ type program_info = ; prg_fixkind : fixpoint_kind option ; prg_implicits : Impargs.manual_implicits ; prg_notations : notations - ; prg_kind : Decl_kinds.definition_kind + ; prg_poly : bool + ; prg_scope : Decl_kinds.locality + ; prg_kind : Decl_kinds.definition_object_kind ; prg_reduce : constr -> constr ; prg_hook : DeclareDef.Hook.t option ; prg_opaque : bool diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 744cdbfb5f..aa3145bc5a 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -74,14 +74,18 @@ module Info = struct ; proof_ending : Proof_ending.t CEphemeron.key (* This could be improved and the CEphemeron removed *) ; other_thms : Recthm.t list + ; scope : Decl_kinds.locality + ; kind : Decl_kinds.goal_object_kind } - let make ?hook ?(proof_ending=Proof_ending.Regular) () = + let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Global ImportDefaultBehavior) ?(kind=Proof Lemma) () = { hook ; compute_guard = [] ; impargs = [] ; proof_ending = CEphemeron.create proof_ending ; other_thms = [] + ; scope + ; kind } end @@ -246,13 +250,13 @@ let check_name_freshness locality {CAst.loc;v=id} : unit = then user_err ?loc (Id.print id ++ str " already exists.") -let save_remaining_recthms env sigma ~poly (locality,kind) norm univs body opaq i +let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i { Recthm.name; typ; impargs } = let t_i = norm typ in let k = IsAssumption Conjectural in match body with | None -> - (match locality with + (match scope with | Discharge -> let impl = false in (* copy values from Vernacentries *) let univs = match univs with @@ -271,7 +275,6 @@ let save_remaining_recthms env sigma ~poly (locality,kind) norm univs body opaq (ConstRef kn,impargs)) | Some body -> let body = norm body in - let k = Kindops.logical_kind_of_goal_kind kind in let rec body_i t = match Constr.kind t with | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) | CoFix (0,decls) -> mkCoFix (i,decls) @@ -281,7 +284,7 @@ let save_remaining_recthms env sigma ~poly (locality,kind) norm univs body opaq | _ -> anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in let body_i = body_i body in - match locality with + match scope with | Discharge -> let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in let c = SectionLocalDef const in @@ -338,19 +341,19 @@ module Stack = struct end (* Starting a goal *) -let start_lemma ~name ~poly ~kind +let start_lemma ~name ~poly ?(udecl=UState.default_univ_decl) ?(sign=initialize_named_context_for_proof()) ?(info=Info.make ()) sigma c = let goals = [ Global.env_of_context sign , c ] in - let proof = Proof_global.start_proof sigma ~name ~udecl ~poly ~kind goals in + let proof = Proof_global.start_proof sigma ~name ~udecl ~poly goals in { proof ; info } -let start_dependent_lemma ~name ~poly ~kind +let start_dependent_lemma ~name ~poly ?(udecl=UState.default_univ_decl) ?(info=Info.make ()) telescope = - let proof = Proof_global.start_dependent_proof ~name ~udecl ~poly ~kind telescope in + let proof = Proof_global.start_dependent_proof ~name ~udecl ~poly telescope in { proof; info } let rec_tac_initializer finite guard thms snl = @@ -367,7 +370,7 @@ let rec_tac_initializer finite guard thms snl = | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false -let start_lemma_with_initialization ?hook ~poly ~kind ~udecl sigma recguard thms snl = +let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl = let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in let init_tac, compute_guard = match recguard with | Some (finite,guard,init_tac) -> @@ -391,14 +394,16 @@ let start_lemma_with_initialization ?hook ~poly ~kind ~udecl sigma recguard thms ; compute_guard ; other_thms ; proof_ending = CEphemeron.create Proof_ending.Regular + ; scope + ; kind } in - let lemma = start_lemma ~name ~poly ~kind ~udecl ~info sigma typ in + let lemma = start_lemma ~name ~poly ~udecl ~info sigma typ in pf_map (Proof_global.map_proof (fun p -> match init_tac with | None -> p | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma -let start_lemma_com ~program_mode ~poly ~kind ?inference_hook ?hook thms = +let start_lemma_com ~program_mode ~poly ~scope ~kind ?inference_hook ?hook thms = let env0 = Global.env () in let decl = fst (List.hd thms) in let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in @@ -409,7 +414,7 @@ let start_lemma_com ~program_mode ~poly ~kind ?inference_hook ?hook thms = let hook = inference_hook in let evd = solve_remaining_evars ?hook flags env evd in let ids = List.map RelDecl.get_name ctx in - check_name_freshness (fst kind) id; + check_name_freshness scope id; (* XXX: The nf_evar is critical !! *) evd, (id.CAst.v, (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), @@ -431,7 +436,7 @@ let start_lemma_com ~program_mode ~poly ~kind ?inference_hook ?hook thms = else (* We fix the variables to ensure they won't be lowered to Set *) Evd.fix_undefined_variables evd in - start_lemma_with_initialization ?hook ~poly ~kind evd ~udecl recguard thms snl + start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl (************************************************************************) (* Admitting a lemma-like constant *) @@ -449,19 +454,19 @@ let warn_let_as_axiom = (* This declares implicits and calls the hooks for all the theorems, including the main one *) -let process_recthms ?fix_exn ?hook env sigma ctx decl ~poly strength ref imps other_thms = +let process_recthms ?fix_exn ?hook env sigma ctx ~udecl ~poly ~scope ref imps other_thms = let other_thms_data = if List.is_empty other_thms then [] else (* there are several theorems defined mutually *) let body,opaq = retrieve_first_recthm ctx ref in let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in let body = Option.map EConstr.of_constr body in - let uctx = UState.check_univ_decl ~poly ctx decl in - List.map_i (save_remaining_recthms env sigma ~poly strength norm uctx body opaq) 1 other_thms in + let uctx = UState.check_univ_decl ~poly ctx udecl in + List.map_i (save_remaining_recthms env sigma ~poly ~scope norm uctx body opaq) 1 other_thms in let thms_data = (ref,imps)::other_thms_data in List.iter (fun (ref,imps) -> maybe_declare_manual_implicits false ref imps; - DeclareDef.Hook.call ?fix_exn ?hook ctx [] (fst strength) ref) thms_data + DeclareDef.Hook.call ?fix_exn ?hook ctx [] scope ref) thms_data let get_keep_admitted_vars = Goptions.declare_bool_option_and_ref @@ -470,7 +475,7 @@ let get_keep_admitted_vars = ~key:["Keep"; "Admitted"; "Variables"] ~value:true -let finish_admitted env sigma id ~poly (scope,kind) pe ctx hook udecl impargs other_thms = +let finish_admitted env sigma id ~poly ~scope pe ctx hook ~udecl impargs other_thms = let local = match scope with | Global local -> local | Discharge -> warn_let_as_axiom id; ImportNeedQualified @@ -479,14 +484,14 @@ let finish_admitted env sigma id ~poly (scope,kind) pe ctx hook udecl impargs ot let () = assumption_message id in Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx); (* This takes care of the implicits and hook for the current constant*) - process_recthms ?fix_exn:None ?hook env sigma ctx udecl ~poly (Global local,kind) (ConstRef kn) impargs other_thms; + process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (ConstRef kn) impargs other_thms; Feedback.feedback Feedback.AddedAxiom let save_lemma_admitted ?proof ~(lemma : t) = let open Proof_global in let env = Global.env () in match proof with - | Some ({ id; entries; persistence = k; universes; udecl }, { Info.hook; impargs; other_thms; _} ) -> + | Some ({ id; entries; universes; udecl }, { Info.hook; scope; impargs; other_thms; _} ) -> if List.length entries <> 1 then user_err Pp.(str "Admitted does not support multiple statements"); let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in @@ -499,10 +504,10 @@ let save_lemma_admitted ?proof ~(lemma : t) = let ctx = UState.univ_entry ~poly universes in let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in let sigma = Evd.from_env env in - finish_admitted env sigma id k (sec_vars, (typ, ctx), None) universes hook ~poly udecl impargs other_thms + finish_admitted env sigma id ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms | None -> let pftree = Proof_global.get_proof lemma.proof in - let gk = Proof_global.get_persistence lemma.proof in + let scope = lemma.info.Info.scope in let Proof.{ name; poly; entry } = Proof.data pftree in let typ = match Proofview.initial_goals entry with | [typ] -> snd typ @@ -529,7 +534,7 @@ let save_lemma_admitted ?proof ~(lemma : t) = let { Info.hook; impargs; other_thms } = lemma.info in let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in let ctx = UState.check_univ_decl ~poly universes udecl in - finish_admitted env sigma name gk (sec_vars, (typ, ctx), None) universes hook ~poly udecl impargs other_thms + finish_admitted env sigma name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms (************************************************************************) (* Saving a lemma-like constant *) @@ -537,9 +542,9 @@ let save_lemma_admitted ?proof ~(lemma : t) = let finish_proved env sigma opaque idopt po info = let open Proof_global in - let { Info.hook; compute_guard; impargs; other_thms } = info in + let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in match po with - | { id; entries=[const]; persistence=locality,kind; universes; udecl; poly } -> + | { id; entries=[const]; universes; udecl; poly } -> let is_opaque = match opaque with | Transparent -> false | Opaque -> true @@ -553,7 +558,7 @@ let finish_proved env sigma opaque idopt po info = let const = adjust_guardness_conditions const compute_guard in let k = Kindops.logical_kind_of_goal_kind kind in let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in - let r = match locality with + let r = match scope with | Discharge -> let c = SectionLocalDef const in let _ = declare_variable id (Lib.cwd(), c, k) in @@ -573,7 +578,7 @@ let finish_proved env sigma opaque idopt po info = in definition_message id; (* This takes care of the implicits and hook for the current constant*) - process_recthms ~fix_exn ?hook env sigma universes udecl ~poly (locality,kind) r impargs other_thms + process_recthms ~fix_exn ?hook env sigma universes ~udecl ~poly ~scope r impargs other_thms with e when CErrors.noncritical e -> let e = CErrors.push e in iraise (fix_exn e) @@ -626,11 +631,11 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries = in ignore (Declare.declare_constant name lemma_def) -let finish_proved_equations opaque lid proof_obj hook i types wits sigma0 = +let finish_proved_equations opaque lid kind proof_obj hook i types wits sigma0 = let open Decl_kinds in let obls = ref 1 in - let kind = match snd proof_obj.Proof_global.persistence with + let kind = match kind with | DefinitionBody d -> IsDefinition d | Proof p -> IsProof p in @@ -678,4 +683,4 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt = | End_derive { f ; name } -> finish_derived ~f ~name ~idopt ~opaque ~entries:proof_obj.entries | End_equations { hook; i; types; wits; sigma } -> - finish_proved_equations opaque idopt proof_obj hook i types wits sigma + finish_proved_equations opaque idopt proof_info.Info.kind proof_obj hook i types wits sigma diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 1a8b1f2f30..a3df43f80e 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -85,6 +85,10 @@ module Info : sig (** Callback to be executed at the end of the proof *) -> ?proof_ending : Proof_ending.t (** Info for special constants *) + -> ?scope : Decl_kinds.locality + (** locality *) + -> ?kind:goal_object_kind + (** Theorem, etc... *) -> unit -> t @@ -94,7 +98,6 @@ end val start_lemma : name:Id.t -> poly:bool - -> kind:goal_kind -> ?udecl:UState.universe_decl -> ?sign:Environ.named_context_val -> ?info:Info.t @@ -105,7 +108,6 @@ val start_lemma val start_dependent_lemma : name:Id.t -> poly:bool - -> kind:goal_kind -> ?udecl:UState.universe_decl -> ?info:Info.t -> Proofview.telescope @@ -117,7 +119,8 @@ type lemma_possible_guards = int list list val start_lemma_with_initialization : ?hook:DeclareDef.Hook.t -> poly:bool - -> kind:goal_kind + -> scope:locality + -> kind:goal_object_kind -> udecl:UState.universe_decl -> Evd.evar_map -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option @@ -131,7 +134,8 @@ val default_thm_id : Names.Id.t val start_lemma_com : program_mode:bool -> poly:bool - -> kind:goal_kind + -> scope:locality + -> kind:goal_object_kind -> ?inference_hook:Pretyping.inference_hook -> ?hook:DeclareDef.Hook.t -> Vernacexpr.proof_expr list diff --git a/vernac/obligations.ml b/vernac/obligations.ml index b2c5520c0b..ba514f9ab3 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -300,7 +300,7 @@ let add_hint local prg cst = Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst) let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind - notations obls impls kind reduce = + notations obls impls ~scope ~poly ~kind reduce = let obls', b = match b with | None -> @@ -320,13 +320,23 @@ let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind obls, b in let ctx = UState.make_flexible_nonalgebraic ctx in - { prg_name = n ; prg_body = b; prg_type = reduce t; - prg_ctx = ctx; prg_univdecl = udecl; - prg_obligations = (obls', Array.length obls'); - prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; - prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; - prg_hook = hook; prg_opaque = opaque; - prg_sign = sign } + { prg_name = n + ; prg_body = b + ; prg_type = reduce t + ; prg_ctx = ctx + ; prg_univdecl = udecl + ; prg_obligations = (obls', Array.length obls') + ; prg_deps = deps + ; prg_fixkind = fixkind + ; prg_notations = notations + ; prg_implicits = impls + ; prg_poly = poly + ; prg_scope = scope + ; prg_kind = kind + ; prg_reduce = reduce + ; prg_hook = hook + ; prg_opaque = opaque + ; prg_sign = sign } let map_cardinal m = let i = ref 0 in @@ -408,12 +418,11 @@ let warn_solve_errored = CWarnings.create ~name:"solve_obligation_error" ~catego str "This will become an error in the future"]) let solve_by_tac ?loc name evi t poly ctx = - let id = name in (* spiwack: the status is dropped. *) try let (entry,_,ctx') = Pfedit.build_constant_by_tactic - id ~poly ~goal_kind ctx evi.evar_hyps evi.evar_concl t in + ~name ~poly ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in let (body, eff) = Future.force entry.Proof_global.proof_entry_body in let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in @@ -443,7 +452,7 @@ let obligation_hook prg obl num auto ctx' _ _ gr = | _ -> () in let inst, ctx' = - if not (pi2 prg.prg_kind) (* Not polymorphic *) then + if not prg.prg_poly (* Not polymorphic *) then (* The universe context was declared globally, we continue from the new global environment. *) let ctx = UState.make (Global.universes ()) in @@ -484,15 +493,15 @@ let rec solve_obligation prg num tac = ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining)); in let obl = subst_deps_obl obls obl in - let kind = kind_of_obligation (snd obl.obl_status) in + let scope, kind = kind_of_obligation (snd obl.obl_status) in let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n oblset tac = auto_solve_obligations n ~oblset tac in let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in - let info = Lemmas.Info.make ~hook ~proof_ending () in - let poly = pi2 prg.prg_kind in - let lemma = Lemmas.start_lemma ~sign:prg.prg_sign ~name:obl.obl_name ~poly ~kind ~info evd (EConstr.of_constr obl.obl_type) in + let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in + let poly = prg.prg_poly in + let lemma = Lemmas.start_lemma ~sign:prg.prg_sign ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in let lemma = fst @@ Lemmas.by !default_tactic lemma in let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in lemma @@ -527,14 +536,14 @@ and solve_obligation_by_tac prg obls i tac = let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac - (pi2 prg.prg_kind) (Evd.evar_universe_context evd) with + prg.prg_poly (Evd.evar_universe_context evd) with | None -> None | Some (t, ty, ctx) -> - let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in let prg = {prg with prg_ctx = ctx} in let def, obl' = declare_obligation prg obl t ty uctx in obls.(i) <- obl'; - if def && not (pi2 prg.prg_kind) then ( + if def && not prg.prg_poly then ( (* Declare the term constraints with the first obligation only *) let evd = Evd.from_env (Global.env ()) in let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in @@ -628,12 +637,12 @@ let show_term n = Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl () ++ Printer.pr_constr_env env sigma prg.prg_body) -let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) - ?(implicits=[]) ?(kind=Global ImportDefaultBehavior,false,Definition) ?tactic +let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl) + ?(implicits=[]) ~poly ?(scope=Global ImportDefaultBehavior) ?(kind=Definition) ?tactic ?(reduce=reduce) ?hook ?(opaque = false) obls = let sign = Lemmas.initialize_named_context_for_proof () in - let info = Id.print n ++ str " has type-checked" in - let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?hook in + let info = Id.print name ++ str " has type-checked" in + let prg = init_prog_info sign ~opaque name univdecl term t ctx [] None [] obls implicits ~poly ~scope ~kind reduce ?hook in let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose Feedback.msg_info (info ++ str "."); @@ -642,21 +651,21 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) else ( let len = Array.length obls in let () = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in - progmap_add n (CEphemeron.create prg); - let res = auto_solve_obligations (Some n) tactic in + progmap_add name (CEphemeron.create prg); + let res = auto_solve_obligations (Some name) tactic in match res with - | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res + | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some name)) (); res | _ -> res) let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic - ?(kind=Global ImportDefaultBehavior,false,Definition) ?(reduce=reduce) + ~poly ?(scope=Global ImportDefaultBehavior) ?(kind=Definition) ?(reduce=reduce) ?hook ?(opaque = false) notations fixkind = let sign = Lemmas.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter (fun (n, b, t, imps, obls) -> let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind) - notations obls imps kind reduce ?hook + notations obls imps ~poly ~scope ~kind reduce ?hook in progmap_add n (CEphemeron.create prg)) l; let _defined = List.fold_left (fun finished x -> diff --git a/vernac/obligations.mli b/vernac/obligations.mli index a0010a5026..787ab53e66 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -43,12 +43,14 @@ type obligation_info = val default_tactic : unit Proofview.tactic ref val add_definition - : Names.Id.t + : name:Names.Id.t -> ?term:constr -> types -> UState.t -> ?univdecl:UState.universe_decl (* Universe binders and constraints *) -> ?implicits:Impargs.manual_implicits - -> ?kind:Decl_kinds.definition_kind + -> poly:bool + -> ?scope:Decl_kinds.locality + -> ?kind:Decl_kinds.definition_object_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(constr -> constr) -> ?hook:DeclareDef.Hook.t @@ -56,16 +58,19 @@ val add_definition -> obligation_info -> DeclareObl.progress -val add_mutual_definitions : - (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list -> - UState.t -> - ?univdecl:UState.universe_decl -> (* Universe binders and constraints *) - ?tactic:unit Proofview.tactic -> - ?kind:Decl_kinds.definition_kind -> - ?reduce:(constr -> constr) -> - ?hook:DeclareDef.Hook.t -> ?opaque:bool -> - DeclareObl.notations -> - DeclareObl.fixpoint_kind -> unit +val add_mutual_definitions + : (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list + -> UState.t + -> ?univdecl:UState.universe_decl + (** Universe binders and constraints *) + -> ?tactic:unit Proofview.tactic + -> poly:bool + -> ?scope:Decl_kinds.locality + -> ?kind:Decl_kinds.definition_object_kind + -> ?reduce:(constr -> constr) + -> ?hook:DeclareDef.Hook.t -> ?opaque:bool + -> DeclareObl.notations + -> DeclareObl.fixpoint_kind -> unit val obligation : int * Names.Id.t option * Constrexpr.constr_expr option diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index d1377fecc5..ee00bc0e2a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -560,7 +560,7 @@ let () = (***********) (* Gallina *) -let start_proof_and_print ~program_mode ~poly ?hook k l = +let start_proof_and_print ~program_mode ~poly ?hook ~scope ~kind l = let inference_hook = if program_mode then let hook env sigma ev = @@ -582,7 +582,7 @@ let start_proof_and_print ~program_mode ~poly ?hook k l = in Some hook else None in - start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~kind:k l + start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~scope ~kind l let vernac_definition_hook p = function | Coercion -> @@ -616,30 +616,30 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let program_mode = atts.program in let poly = atts.polymorphic in let name = vernac_definition_name lid local in - start_proof_and_print ~program_mode ~poly (local, DefinitionBody kind) ?hook [(name, pl), (bl, t)] + start_proof_and_print ~program_mode ~poly ~scope:local ~kind:(DefinitionBody kind) ?hook [(name, pl), (bl, t)] let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in - let local = enforce_locality_exp atts.locality discharge in + let scope = enforce_locality_exp atts.locality discharge in let hook = vernac_definition_hook atts.polymorphic kind in let program_mode = atts.program in - let name = vernac_definition_name lid local in + let name = vernac_definition_name lid scope in let red_option = match red_option with | None -> None | Some r -> let env = Global.env () in let sigma = Evd.from_env env in Some (snd (Hook.get f_interp_redexp env sigma r)) in - ComDefinition.do_definition ~program_mode name.v - (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook + ComDefinition.do_definition ~program_mode ~name:name.v + ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook (* NB: pstate argument to use combinators easily *) let vernac_start_proof ~atts kind l = let open DefAttributes in - let local = enforce_locality_exp atts.locality NoDischarge in + let scope = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic (local, Proof kind) l + start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Proof kind) l let vernac_end_proof ?stack ?proof = let open Vernacexpr in function | Admitted -> @@ -666,15 +666,14 @@ let vernac_exact_proof ~lemma c = let vernac_assumption ~atts discharge kind l nl = let open DefAttributes in - let local = enforce_locality_exp atts.locality discharge in - let kind = local, atts.polymorphic, kind in + let scope = enforce_locality_exp atts.locality discharge in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then List.iter (fun (lid, _) -> - match local with + match scope with | Global _ -> Dumpglob.dump_definition lid false "ax" | Discharge -> Dumpglob.dump_definition lid true "var") idl) l; - let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in + let status = ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l in if not status then Feedback.feedback Feedback.AddedAxiom let is_polymorphic_inductive_cumulativity = @@ -847,19 +846,19 @@ let vernac_fixpoint_common ~atts discharge l = let vernac_fixpoint_interactive ~atts discharge l = let open DefAttributes in - let local = vernac_fixpoint_common ~atts discharge l in + let scope = vernac_fixpoint_common ~atts discharge l in if atts.program then CErrors.user_err Pp.(str"Program Fixpoint requires a body"); - ComFixpoint.do_fixpoint_interactive local atts.polymorphic l + ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l let vernac_fixpoint ~atts discharge l = let open DefAttributes in - let local = vernac_fixpoint_common ~atts discharge l in + let scope = vernac_fixpoint_common ~atts discharge l in if atts.program then (* XXX: Switch to the attribute system and match on ~atts *) - ComProgramFixpoint.do_fixpoint local atts.polymorphic l + ComProgramFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l else - ComFixpoint.do_fixpoint local atts.polymorphic l + ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l let vernac_cofixpoint_common ~atts discharge l = if Dumpglob.dump () then @@ -868,18 +867,18 @@ let vernac_cofixpoint_common ~atts discharge l = let vernac_cofixpoint_interactive ~atts discharge l = let open DefAttributes in - let local = vernac_cofixpoint_common ~atts discharge l in + let scope = vernac_cofixpoint_common ~atts discharge l in if atts.program then CErrors.user_err Pp.(str"Program CoFixpoint requires a body"); - ComFixpoint.do_cofixpoint_interactive local atts.polymorphic l + ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l let vernac_cofixpoint ~atts discharge l = let open DefAttributes in - let local = vernac_cofixpoint_common ~atts discharge l in + let scope = vernac_cofixpoint_common ~atts discharge l in if atts.program then - ComProgramFixpoint.do_cofixpoint local atts.polymorphic l + ComProgramFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l else - ComFixpoint.do_cofixpoint local atts.polymorphic l + ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l let vernac_scheme l = if Dumpglob.dump () then |