From 5749a2360f9d0d7c8901a1264863339442964ca7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Mar 2020 03:30:21 -0400 Subject: [lemma] Remove special case for first constant in mutual definition save path. This could still use some more work due to the way proofs are structured, in particular: - the handling of the primary type w.r.t. Econstr - refining Info.t so open/close invariants hold by typing Very interestingly, better typing means that the tension between tension between `start_dependent_lemma` and the handling of mutual definitions starts to surface. In particular, the information contained in `Info.thms` is not to be used by all non-standard terminators. However, it seems that such refactoring would better fit once we have finished cleaning up the regular save path. --- vernac/lemmas.ml | 131 +++++++++++++++++++++++++++++------------------- vernac/lemmas.mli | 3 +- vernac/vernacentries.ml | 4 +- 3 files changed, 83 insertions(+), 55 deletions(-) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index e08d2ce117..ed2a2056d5 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -43,22 +43,21 @@ module Info = struct type t = { hook : DeclareDef.Hook.t option - ; compute_guard : lemma_possible_guards - ; impargs : Impargs.manual_implicits ; proof_ending : Proof_ending.t CEphemeron.key (* This could be improved and the CEphemeron removed *) - ; other_thms : DeclareDef.Recthm.t list ; scope : DeclareDef.locality ; kind : Decls.logical_kind + (* thms and compute guard are specific only to start_lemma_with_initialization + regular terminator *) + ; thms : DeclareDef.Recthm.t list + ; compute_guard : lemma_possible_guards } let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.(IsProof Lemma)) () = { hook ; compute_guard = [] - ; impargs = [] ; proof_ending = CEphemeron.create proof_ending - ; other_thms = [] + ; thms = [] ; scope ; kind } @@ -100,18 +99,30 @@ let initialize_named_context_for_proof () = let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val +let add_first_thm ~info ~name ~typ ~impargs = + let thms = + { DeclareDef.Recthm.name + ; impargs + ; typ = EConstr.Unsafe.to_constr typ + ; args = [] } :: info.Info.thms + in + { info with Info.thms } + (* Starting a goal *) let start_lemma ~name ~poly ?(udecl=UState.default_univ_decl) - ?(info=Info.make ()) - sigma c = + ?(info=Info.make ()) ?(impargs=[]) sigma c = (* We remove the bodies of variables in the named context marked "opaque", this is a hack tho, see #10446 *) let sign = initialize_named_context_for_proof () in let goals = [ Global.env_of_context sign , c ] in let proof = Proof_global.start_proof sigma ~name ~udecl ~poly goals in - { proof ; info } + let info = add_first_thm ~info ~name ~typ:c ~impargs in + { proof; info } +(* Note that proofs opened by start_dependent lemma cannot be closed + by the regular terminators, thus we don't need to update the [thms] + field. We will capture this invariant by typing in the future *) let start_dependent_lemma ~name ~poly ?(udecl=UState.default_univ_decl) ?(info=Info.make ()) telescope = @@ -153,17 +164,18 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua intro_tac (List.hd thms), [] in match thms with | [] -> CErrors.anomaly (Pp.str "No proof to start.") - | { DeclareDef.Recthm.name; typ; impargs; _}::other_thms -> + | { DeclareDef.Recthm.name; typ; impargs; _} :: thms -> let info = Info.{ hook - ; impargs ; compute_guard - ; other_thms ; proof_ending = CEphemeron.create Proof_ending.Regular + ; thms ; scope ; kind } in - let lemma = start_lemma ~name ~poly ~udecl ~info sigma (EConstr.of_constr typ) in + (* start_lemma has the responsibility to add (name, impargs, typ) + to thms, once Info.t is more refined this won't be necessary *) + let lemma = start_lemma ~name ~impargs ~poly ~udecl ~info sigma (EConstr.of_constr typ) in pf_map (Proof_global.map_proof (fun p -> pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)) lemma @@ -191,9 +203,8 @@ module MutualEntry : sig -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> uctx:UState.t -> ?hook_data:DeclareDef.Hook.t * UState.t * (Names.Id.t * Constr.t) list - (* Only for the first constant, introduced by compat *) + (* [ubind] is only for the first constant, introduced by compat *) -> ubind:UnivNames.universe_binders - -> name:Id.t -> Evd.side_effects Declare.proof_entry -> Names.GlobRef.t list @@ -210,8 +221,7 @@ end = struct ; info : Info.t } - (* XXX: Refactor this with the code in - [ComFixpoint.declare_fixpoint_generic] *) + (* XXX: Refactor this with the code in [DeclareDef.declare_mutdef] *) let guess_decreasing env possible_indexes ((body, ctx), eff) = let open Constr in match Constr.kind body with @@ -258,7 +268,8 @@ end = struct is used when declaring mutual cofixpoints *) DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe | Mutual pe -> - (* if typ = None , we don't touch the type; used in the base case *) + (* if typ = None , we don't touch the type; this is for compat + but not clear it is the right thing to do *) let pe = match typ with | None -> pe @@ -269,26 +280,29 @@ end = struct ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe - let declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name { entry; info } = - (* At some point make this a single iteration *) - (* At some point make this a single iteration *) - (* impargs here are special too, fixed in upcoming PRs *) - let impargs = info.Info.impargs in - let r = declare_mutdef ?fix_exn ~info ~ubind ?hook_data ~uctx ~name ~impargs entry 0 in - (* Before we used to do this, check if that's right *) - let ubind = UnivNames.empty_binders in + let declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind { entry; info } = let rs = List.map_i ( fun i { DeclareDef.Recthm.name; typ; impargs } -> - declare_mutdef ?fix_exn ~name ~info ~ubind ?hook_data ~uctx ~typ ~impargs entry i) 1 info.Info.other_thms - in r :: rs + (* See start_dependent_proof ~typ:mkProp to understand why + we don't we use the type stored here. This is obviously a + fixme [was like this for long time] + + Regarding ubind, before we used to do this too, check if + that's the right thing to do *) + let typ, ubind = if i = 0 + then None, ubind + else Some typ, UnivNames.empty_binders in + declare_mutdef ?fix_exn ~name ~info ~ubind ?hook_data ~uctx ?typ ~impargs entry i) + 0 info.Info.thms + in rs let declare_variable ~info ~uctx ~ubind ~name pe = - declare_mutdef ~uctx ~ubind ~name { entry = NoBody pe; info } + declare_mutdef ~uctx ~ubind { entry = NoBody pe; info } - let declare_mutdef ~info ?fix_exn ~uctx ?hook_data ~ubind ~name const = + let declare_mutdef ~info ?fix_exn ~uctx ?hook_data ~ubind const = let mutpe = adjust_guardness_conditions ~info const in - declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name mutpe + declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind mutpe end @@ -340,26 +354,17 @@ let save_lemma_admitted ~(lemma : t) : unit = (* Saving a lemma-like constant *) (************************************************************************) -let default_thm_id = Id.of_string "Unnamed_thm" - -let check_anonymity id save_ident = - if not (String.equal (Nameops.atompart_of_id id) (Id.to_string (default_thm_id))) then - CErrors.user_err Pp.(str "This command can only be used for unnamed theorem.") - -let finish_proved idopt po info = +let finish_proved po info = let open Proof_global in let { Info.hook } = info in match po with | { name; entries=[const]; uctx; udecl } -> - let name = match idopt with - | None -> name - | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in let fix_exn = Declare.Internal.get_fix_exn const in let () = try let hook_data = Option.map (fun hook -> hook, uctx, []) hook in let ubind = UState.universe_binders uctx in let _r : Names.GlobRef.t list = - MutualEntry.declare_mutdef ~info ~fix_exn ~uctx ?hook_data ~ubind ~name const + MutualEntry.declare_mutdef ~info ~fix_exn ~uctx ?hook_data ~ubind const in () with e when CErrors.noncritical e -> let e = Exninfo.capture e in @@ -368,12 +373,9 @@ let finish_proved idopt po info = | _ -> CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term") -let finish_derived ~f ~name ~idopt ~entries = +let finish_derived ~f ~name ~entries = (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *) - if Option.has_some idopt then - CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name."); - let f_def, lemma_def = match entries with | [_;f_def;lemma_def] -> @@ -406,7 +408,7 @@ let finish_derived ~f ~name ~idopt ~entries = let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in () -let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = +let finish_proved_equations kind proof_obj hook i types wits sigma0 = let obls = ref 1 in let sigma, recobls = @@ -425,23 +427,40 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = in hook recobls sigma -let finalize_proof idopt proof_obj proof_info = +let finalize_proof proof_obj proof_info = let open Proof_global in let open Proof_ending in match CEphemeron.default proof_info.Info.proof_ending Regular with | Regular -> - finish_proved idopt proof_obj proof_info + finish_proved proof_obj proof_info | End_obligation oinfo -> DeclareObl.obligation_terminator proof_obj.entries proof_obj.uctx oinfo | End_derive { f ; name } -> - finish_derived ~f ~name ~idopt ~entries:proof_obj.entries + finish_derived ~f ~name ~entries:proof_obj.entries | End_equations { hook; i; types; wits; sigma } -> - finish_proved_equations idopt proof_info.Info.kind proof_obj hook i types wits sigma + finish_proved_equations proof_info.Info.kind proof_obj hook i types wits sigma + +let err_save_forbidden_in_place_of_qed () = + CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode") + +let process_idopt_for_save ~idopt info = + match idopt with + | None -> info + | Some { CAst.v = save_name } -> + (* Save foo was used; we override the info in the first theorem *) + let thms = + match info.Info.thms, CEphemeron.default info.Info.proof_ending Proof_ending.Regular with + | [ { DeclareDef.Recthm.name; _} as decl ], Proof_ending.Regular -> + [ { decl with DeclareDef.Recthm.name = save_name } ] + | _ -> + err_save_forbidden_in_place_of_qed () + in { info with Info.thms } let save_lemma_proved ~lemma ~opaque ~idopt = (* Env and sigma are just used for error printing in save_remaining_recthms *) let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) lemma.proof in - finalize_proof idopt proof_obj lemma.info + let proof_info = process_idopt_for_save ~idopt lemma.info in + finalize_proof proof_obj proof_info (***********************************************************************) (* Special case to close a lemma without forcing a proof *) @@ -462,4 +481,12 @@ let save_lemma_admitted_delayed ~proof ~info = let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in finish_admitted ~name ~uctx ~info (sec_vars, (typ, ctx), None) -let save_lemma_proved_delayed ~proof ~info ~idopt = finalize_proof idopt proof info +let save_lemma_proved_delayed ~proof ~info ~idopt = + (* vio2vo calls this but with invalid info, we have to workaround + that to add the name to the info structure *) + if CList.is_empty info.Info.thms then + let info = add_first_thm ~info ~name:proof.Proof_global.name ~typ:EConstr.mkSet ~impargs:[] in + finalize_proof proof info + else + let info = process_idopt_for_save ~idopt info in + finalize_proof proof info diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 6a1f8c09f3..0f0a37202a 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -68,6 +68,7 @@ val start_lemma -> poly:bool -> ?udecl:UState.universe_decl -> ?info:Info.t + -> ?impargs:Impargs.manual_implicits -> Evd.evar_map -> EConstr.types -> t @@ -95,8 +96,6 @@ val start_lemma_with_initialization -> int list option -> t -val default_thm_id : Names.Id.t - (** {4 Saving proofs} *) val save_lemma_admitted : lemma:t -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 963b5f2084..5497bd84ac 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -527,8 +527,10 @@ let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref))) | _ -> None +let default_thm_id = Id.of_string "Unnamed_thm" + let fresh_name_for_anonymous_theorem () = - Namegen.next_global_ident_away Lemmas.default_thm_id Id.Set.empty + Namegen.next_global_ident_away default_thm_id Id.Set.empty let vernac_definition_name lid local = let lid = -- cgit v1.2.3 From 5f937b2f8532b2ccf36c62557934cc2c9150005b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Mar 2020 06:32:00 -0400 Subject: [proof] Miscellaneous cleanup on proof info handling After the refactorings proof information is organized in a slightly different way thus the lower layers don't need to pass info back anymore. --- plugins/funind/gen_principle.ml | 2 +- tactics/proof_global.ml | 4 +-- tactics/proof_global.mli | 2 -- vernac/declareDef.ml | 29 ++++++++++------ vernac/declareDef.mli | 2 +- vernac/declareObl.ml | 3 +- vernac/lemmas.ml | 73 ++++++++++++++++------------------------- 7 files changed, 52 insertions(+), 63 deletions(-) diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 446026c4c8..28cf5c7d98 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -199,7 +199,7 @@ let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_ (* end; *) let open Proof_global in - let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in + let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in match entries with | [entry] -> entry, hook diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index 623e6b8a42..620afbaf23 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -18,9 +18,9 @@ module NamedDecl = Context.Named.Declaration type proof_object = { name : Names.Id.t + (* [name] only used in the STM *) ; entries : Evd.side_effects Declare.proof_entry list ; uctx: UState.t - ; udecl : UState.universe_decl } type opacity_flag = Opaque | Transparent @@ -231,7 +231,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body in let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in - { name; entries; uctx; udecl } + { name; entries; uctx } let return_proof ?(allow_partial=false) ps = let { proof } = ps in diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli index e1c75c0649..d820fc8b40 100644 --- a/tactics/proof_global.mli +++ b/tactics/proof_global.mli @@ -33,8 +33,6 @@ type proof_object = (** list of the proof terms (in a form suitable for definitions). *) ; uctx: UState.t (** universe state *) - ; udecl : UState.universe_decl - (** universe declaration *) } type opacity_flag = Opaque | Transparent diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index fc53abdcea..b0c8fe90c4 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -34,17 +34,12 @@ module Hook = struct let make hook = CEphemeron.create hook - let call ?hook ?fix_exn x = - try Option.iter (fun hook -> CEphemeron.get hook x) hook - with e when CErrors.noncritical e -> - let e = Exninfo.capture e in - let e = Option.cata (fun fix -> fix e) e fix_exn in - Exninfo.iraise e + let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook + end (* Locality stuff *) let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = - let fix_exn = Declare.Internal.get_fix_exn ce in let should_suggest = ce.Declare.proof_entry_opaque && Option.is_empty ce.Declare.proof_entry_secctx in let dref = match scope with @@ -65,10 +60,17 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = match hook_data with | None -> () | Some (hook, uctx, obls) -> - Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref } + Hook.call ~hook { Hook.S.uctx; obls; scope; dref } end; dref +let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = + let fix_exn = Declare.Internal.get_fix_exn ce in + try declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce + with exn -> + let exn = Exninfo.capture exn in + Exninfo.iraise (fix_exn exn) + let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = match possible_indexes with | Some possible_indexes -> @@ -127,7 +129,7 @@ let warn_let_as_axiom = Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++ spc () ++ strbrk "declared as an axiom.") -let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = +let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe = let local = match scope with | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified | Global local -> local @@ -139,9 +141,16 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = let () = Impargs.maybe_declare_manual_implicits false dref impargs in let () = Declare.assumption_message name in let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in - let () = Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref}) in + let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in dref +let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = + try declare_assumption ~name ~scope ~hook ~impargs ~uctx pe + with exn -> + let exn = Exninfo.capture exn in + let exn = Option.cata (fun fix -> fix exn) exn fix_exn in + Exninfo.iraise exn + (* Preparing proof entries *) let check_definition_evars ~allow_evars sigma = diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 1d7fd3a3bf..e999027b44 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -36,7 +36,7 @@ module Hook : sig end val make : (S.t -> unit) -> t - val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t -> unit + val call : ?hook:t -> S.t -> unit end val declare_definition diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 98a9e4b9c9..24a52eaca4 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -464,9 +464,8 @@ let declare_mutual_definition l = ~restrict_ucontext:false fixitems in (* Only for the first constant *) - let fix_exn = Hook.get get_fix_exn () in let dref = List.hd kns in - DeclareDef.Hook.(call ?hook:first.prg_hook ~fix_exn { S.uctx = first.prg_ctx; obls; scope; dref }); + DeclareDef.Hook.(call ?hook:first.prg_hook { S.uctx = first.prg_ctx; obls; scope; dref }); List.iter progmap_remove l; dref diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index ed2a2056d5..2e17a9736b 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -191,20 +191,13 @@ module MutualEntry : sig val declare_variable : info:Info.t -> uctx:UState.t - (* Only for the first constant, introduced by compat *) - -> ubind:UnivNames.universe_binders - -> name:Id.t -> Entries.parameter_entry -> Names.GlobRef.t list val declare_mutdef (* Common to all recthms *) : info:Info.t - -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> uctx:UState.t - -> ?hook_data:DeclareDef.Hook.t * UState.t * (Names.Id.t * Constr.t) list - (* [ubind] is only for the first constant, introduced by compat *) - -> ubind:UnivNames.universe_binders -> Evd.side_effects Declare.proof_entry -> Names.GlobRef.t list @@ -258,7 +251,7 @@ end = struct Pp.(str "Not a proof by induction: " ++ Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".") - let declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name ?typ ~impargs ~info mutpe i = + let declare_mutdef ?fix_exn ~uctx ?hook_data ~name ?typ ~impargs ~info mutpe i = let { Info.hook; compute_guard; scope; kind; _ } = info in match mutpe with | NoBody pe -> @@ -266,43 +259,44 @@ end = struct | Single pe -> (* We'd like to do [assert (i = 0)] here, however this codepath is used when declaring mutual cofixpoints *) + let ubind = UState.universe_binders uctx in + let hook_data = Option.map (fun hook -> hook, uctx, []) info.Info.hook in DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe | Mutual pe -> - (* if typ = None , we don't touch the type; this is for compat + (* if i = 0 , we don't touch the type; this is for compat but not clear it is the right thing to do *) + (* See start_dependent_proof ~typ:mkProp to understand why + we don't we use the type stored here. This is obviously a + fixme [was like this for long time] + *) let pe = match typ with | None -> pe | Some typ -> - Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ) + if i > 0 + then Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ) + else pe in + let hook_data = Option.map (fun hook -> hook, uctx, []) info.Info.hook in + let ubind = if i = 0 then UState.universe_binders uctx else UnivNames.empty_binders in let pe = Declare.Internal.map_entry_body pe ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe - let declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind { entry; info } = + let declare_mutdef ?fix_exn ~uctx { entry; info } = let rs = List.map_i ( fun i { DeclareDef.Recthm.name; typ; impargs } -> - (* See start_dependent_proof ~typ:mkProp to understand why - we don't we use the type stored here. This is obviously a - fixme [was like this for long time] - - Regarding ubind, before we used to do this too, check if - that's the right thing to do *) - let typ, ubind = if i = 0 - then None, ubind - else Some typ, UnivNames.empty_binders in - declare_mutdef ?fix_exn ~name ~info ~ubind ?hook_data ~uctx ?typ ~impargs entry i) + declare_mutdef ?fix_exn ~name ~info ~uctx ~typ ~impargs entry i) 0 info.Info.thms in rs - let declare_variable ~info ~uctx ~ubind ~name pe = - declare_mutdef ~uctx ~ubind { entry = NoBody pe; info } + let declare_variable ~info ~uctx pe = + declare_mutdef ~uctx { entry = NoBody pe; info } - let declare_mutdef ~info ?fix_exn ~uctx ?hook_data ~ubind const = + let declare_mutdef ~info ~uctx const = let mutpe = adjust_guardness_conditions ~info const in - declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind mutpe + declare_mutdef ~uctx mutpe end @@ -330,14 +324,13 @@ let compute_proof_using_for_admitted proof typ pproofs = Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) | _ -> None -let finish_admitted ~name ~info ~uctx pe = - let ubind = UnivNames.empty_binders in - let _r : Names.GlobRef.t list = MutualEntry.declare_variable ~info ~uctx ~ubind ~name pe in +let finish_admitted ~info ~uctx pe = + let _r : Names.GlobRef.t list = MutualEntry.declare_variable ~info ~uctx pe in () let save_lemma_admitted ~(lemma : t) : unit = let udecl = Proof_global.get_universe_decl lemma.proof in - let Proof.{ name; poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in + let Proof.{ poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in let typ = match Proofview.initial_goals entry with | [typ] -> snd typ | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.") @@ -348,7 +341,7 @@ let save_lemma_admitted ~(lemma : t) : unit = let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in let universes = Proof_global.get_initial_euctx lemma.proof in let ctx = UState.check_univ_decl ~poly universes udecl in - finish_admitted ~name ~info:lemma.info ~uctx:universes (sec_vars, (typ, ctx), None) + finish_admitted ~info:lemma.info ~uctx:universes (sec_vars, (typ, ctx), None) (************************************************************************) (* Saving a lemma-like constant *) @@ -356,20 +349,10 @@ let save_lemma_admitted ~(lemma : t) : unit = let finish_proved po info = let open Proof_global in - let { Info.hook } = info in match po with - | { name; entries=[const]; uctx; udecl } -> - let fix_exn = Declare.Internal.get_fix_exn const in - let () = try - let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - let ubind = UState.universe_binders uctx in - let _r : Names.GlobRef.t list = - MutualEntry.declare_mutdef ~info ~fix_exn ~uctx ?hook_data ~ubind const - in () - with e when CErrors.noncritical e -> - let e = Exninfo.capture e in - Exninfo.iraise (fix_exn e) - in () + | { entries=[const]; uctx } -> + let _r : Names.GlobRef.t list = MutualEntry.declare_mutdef ~info ~uctx const in + () | _ -> CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term") @@ -467,7 +450,7 @@ let save_lemma_proved ~lemma ~opaque ~idopt = (***********************************************************************) let save_lemma_admitted_delayed ~proof ~info = let open Proof_global in - let { name; entries; uctx; udecl } = proof in + let { entries; uctx } = proof in if List.length entries <> 1 then CErrors.user_err Pp.(str "Admitted does not support multiple statements"); let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in @@ -479,7 +462,7 @@ let save_lemma_admitted_delayed ~proof ~info = | Some typ -> typ in let ctx = UState.univ_entry ~poly uctx in let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in - finish_admitted ~name ~uctx ~info (sec_vars, (typ, ctx), None) + finish_admitted ~uctx ~info (sec_vars, (typ, ctx), None) let save_lemma_proved_delayed ~proof ~info ~idopt = (* vio2vo calls this but with invalid info, we have to workaround -- cgit v1.2.3 From dc71c61e76b4ffff09b8d41e69ae403348e064fe Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Mar 2020 07:20:18 -0400 Subject: [lemmas] [internal] Reify handling of mutual assumptions This gets us closer to the code in `DeclareDef` for the non-interactive case. --- vernac/lemmas.ml | 57 +++++++++++++++++++++----------------------------------- 1 file changed, 21 insertions(+), 36 deletions(-) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 2e17a9736b..a7cf1bfb76 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -204,16 +204,10 @@ module MutualEntry : sig end = struct (* Body with the fix *) - type et = - | NoBody of Entries.parameter_entry + type t = | Single of Evd.side_effects Declare.proof_entry | Mutual of Evd.side_effects Declare.proof_entry - type t = - { entry : et - ; info : Info.t - } - (* XXX: Refactor this with the code in [DeclareDef.declare_mutdef] *) let guess_decreasing env possible_indexes ((body, ctx), eff) = let open Constr in @@ -225,7 +219,7 @@ end = struct | _ -> (body, ctx), eff let adjust_guardness_conditions ~info const = - let entry = match info.Info.compute_guard with + match info.Info.compute_guard with | [] -> (* Not a recursive statement *) Single const @@ -236,7 +230,6 @@ end = struct ~f:(guess_decreasing env possible_indexes) in Mutual pe - in { entry; info } let rec select_body i t = let open Constr in @@ -251,11 +244,9 @@ end = struct Pp.(str "Not a proof by induction: " ++ Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".") - let declare_mutdef ?fix_exn ~uctx ?hook_data ~name ?typ ~impargs ~info mutpe i = - let { Info.hook; compute_guard; scope; kind; _ } = info in + let declare_mutdef ~uctx ~info mutpe i DeclareDef.Recthm.{ name; impargs; typ; _} = + let { Info.hook; scope; kind; _ } = info in match mutpe with - | NoBody pe -> - DeclareDef.declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe | Single pe -> (* We'd like to do [assert (i = 0)] here, however this codepath is used when declaring mutual cofixpoints *) @@ -264,18 +255,16 @@ end = struct DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe | Mutual pe -> (* if i = 0 , we don't touch the type; this is for compat - but not clear it is the right thing to do *) - (* See start_dependent_proof ~typ:mkProp to understand why + but not clear it is the right thing to do + + See start_dependent_proof ~typ:mkProp to understand why we don't we use the type stored here. This is obviously a fixme [was like this for long time] *) let pe = - match typ with - | None -> pe - | Some typ -> - if i > 0 - then Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ) - else pe + if i > 0 + then Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ) + else pe in let hook_data = Option.map (fun hook -> hook, uctx, []) info.Info.hook in let ubind = if i = 0 then UState.universe_binders uctx else UnivNames.empty_binders in @@ -283,20 +272,16 @@ end = struct ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe - let declare_mutdef ?fix_exn ~uctx { entry; info } = - let rs = - List.map_i ( - fun i { DeclareDef.Recthm.name; typ; impargs } -> - declare_mutdef ?fix_exn ~name ~info ~uctx ~typ ~impargs entry i) - 0 info.Info.thms - in rs - - let declare_variable ~info ~uctx pe = - declare_mutdef ~uctx { entry = NoBody pe; info } - let declare_mutdef ~info ~uctx const = let mutpe = adjust_guardness_conditions ~info const in - declare_mutdef ~uctx mutpe + List.map_i (declare_mutdef ~info ~uctx mutpe) 0 info.Info.thms + + let declare_variable ~info ~uctx pe = + let { Info.scope; hook } = info in + List.map_i ( + fun i { DeclareDef.Recthm.name; typ; impargs } -> + DeclareDef.declare_assumption ~name ~scope ~hook ~impargs ~uctx pe + ) 0 info.Info.thms end @@ -339,9 +324,9 @@ let save_lemma_admitted ~(lemma : t) : unit = let proof = Proof_global.get_proof lemma.proof in let pproofs = Proof.partial_proof proof in let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in - let universes = Proof_global.get_initial_euctx lemma.proof in - let ctx = UState.check_univ_decl ~poly universes udecl in - finish_admitted ~info:lemma.info ~uctx:universes (sec_vars, (typ, ctx), None) + let uctx = Proof_global.get_initial_euctx lemma.proof in + let univs = UState.check_univ_decl ~poly uctx udecl in + finish_admitted ~info:lemma.info ~uctx (sec_vars, (typ, univs), None) (************************************************************************) (* Saving a lemma-like constant *) -- cgit v1.2.3 From 5da15336a01d1f74fac653f69cd0a509ba05a3ab Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 9 Mar 2020 05:24:03 -0400 Subject: [comFixpoint] Minor cleanups in type declarations. --- vernac/comFixpoint.ml | 16 +++++++++++----- vernac/comFixpoint.mli | 11 ++++++----- 2 files changed, 17 insertions(+), 10 deletions(-) diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 6580495295..cbf0affc12 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -140,8 +140,8 @@ let compute_possible_guardness_evidences (ctx,_,recindex) = fixpoints ?) *) List.interval 0 (Context.Rel.nhyps ctx - 1) -type recursive_preentry = - Id.t list * Sorts.relevance list * Constr.t option list * Constr.types list +type ('constr, 'types) recursive_preentry = + Id.t list * Sorts.relevance list * 'constr option list * 'types list (* Wellfounded definition *) @@ -230,7 +230,11 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) = let fixtypes = List.map EConstr.(to_constr evd) fixtypes in Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes) -let interp_fixpoint ~cofix l = +(* XXX: Unify with interp_recursive *) +let interp_fixpoint ~cofix l : + ( (Constr.t, Constr.types) recursive_preentry * + UState.universe_decl * UState.t * + (EConstr.rel_context * Impargs.manual_implicits * int option) list) = let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in check_recursive true env evd fix; let uctx,fix = ground_fixpoint env evd fix in @@ -243,8 +247,10 @@ let build_recthms ~indexes fixnames fixtypes fiximps = in let thms = List.map3 (fun name typ (ctx,impargs,_) -> - { DeclareDef.Recthm.name; typ - ; args = List.map Context.Rel.Declaration.get_name ctx; impargs}) + { DeclareDef.Recthm.name + ; typ + ; args = List.map Context.Rel.Declaration.get_name ctx + ; impargs}) fixnames fixtypes fiximps in fix_kind, cofix, thms diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 2ad6c03bae..a19b96f0f3 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Constr open Vernacexpr (** {6 Fixpoints and cofixpoints} *) @@ -40,6 +39,9 @@ val adjust_rec_order -> Constrexpr.recursion_order_expr option -> lident option +(** names / relevance / defs / types *) +type ('constr, 'types) recursive_preentry = Id.t list * Sorts.relevance list * 'constr option list * 'types list + (** Exported for Program *) val interp_recursive : (* Misc arguments *) @@ -49,18 +51,17 @@ val interp_recursive : (* env / signature / univs / evar_map *) (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (* names / defs / types *) - (Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) * + (EConstr.t, EConstr.types) recursive_preentry * (* ctx per mutual def / implicits / struct annotations *) (EConstr.rel_context * Impargs.manual_implicits * int option) list (** Exported for Funind *) -type recursive_preentry = Id.t list * Sorts.relevance list * constr option list * types list - val interp_fixpoint : cofix:bool -> lident option fix_expr_gen list - -> recursive_preentry * UState.universe_decl * UState.t * + -> (Constr.t, Constr.types) recursive_preentry * + UState.universe_decl * UState.t * (EConstr.rel_context * Impargs.manual_implicits * int option) list (** Very private function, do not use *) -- cgit v1.2.3 From 07a0ec4416fae0f98c610752bc73a30a30f1bd64 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Mar 2020 06:31:58 -0400 Subject: [lemmas] Remove workaround for non-uniform mutual body In previous versions of Coq `abstract` could create non-uniform bodies for mutually recursive definitions (c.f. bug #5065) Thanks to changes to the trusted base this is not the case anymore, thus we can remove the workaround. This way mutual bodies are handled the same in the interactive and non-interactive case. --- vernac/lemmas.ml | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index a7cf1bfb76..638e6ecb54 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -231,14 +231,11 @@ end = struct in Mutual pe - let rec select_body i t = + let select_body i t = let open Constr in match Constr.kind t with | Fix ((nv,0),decls) -> mkFix ((nv,i),decls) | CoFix (0,decls) -> mkCoFix (i,decls) - | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, select_body i t2) - | Lambda(na,ty,t) -> mkLambda(na,ty, select_body i t) - | App (t, args) -> mkApp (select_body i t, args) | _ -> CErrors.anomaly Pp.(str "Not a proof by induction: " ++ -- cgit v1.2.3 From 76115e703751cfde99d7e86be9eea8fb32398e8a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 13 Mar 2020 06:46:47 -0400 Subject: [lemmas] Cleanup in handling of mutual definitions This is a tiny step towards making the code closer to its counterpart in `DeclareDef`. --- vernac/lemmas.ml | 78 ++++++++++++++++++++++---------------------------------- 1 file changed, 31 insertions(+), 47 deletions(-) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 638e6ecb54..e4a625d65c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -203,11 +203,6 @@ module MutualEntry : sig end = struct - (* Body with the fix *) - type t = - | Single of Evd.side_effects Declare.proof_entry - | Mutual of Evd.side_effects Declare.proof_entry - (* XXX: Refactor this with the code in [DeclareDef.declare_mutdef] *) let guess_decreasing env possible_indexes ((body, ctx), eff) = let open Constr in @@ -218,19 +213,6 @@ end = struct (mkFix ((indexes,0),fixdecls), ctx), eff | _ -> (body, ctx), eff - let adjust_guardness_conditions ~info const = - match info.Info.compute_guard with - | [] -> - (* Not a recursive statement *) - Single const - | possible_indexes -> - (* Try all combinations... not optimal *) - let env = Global.env() in - let pe = Declare.Internal.map_entry_body const - ~f:(guess_decreasing env possible_indexes) - in - Mutual pe - let select_body i t = let open Constr in match Constr.kind t with @@ -241,37 +223,39 @@ end = struct Pp.(str "Not a proof by induction: " ++ Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".") - let declare_mutdef ~uctx ~info mutpe i DeclareDef.Recthm.{ name; impargs; typ; _} = - let { Info.hook; scope; kind; _ } = info in - match mutpe with - | Single pe -> - (* We'd like to do [assert (i = 0)] here, however this codepath - is used when declaring mutual cofixpoints *) - let ubind = UState.universe_binders uctx in - let hook_data = Option.map (fun hook -> hook, uctx, []) info.Info.hook in - DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe - | Mutual pe -> - (* if i = 0 , we don't touch the type; this is for compat - but not clear it is the right thing to do - - See start_dependent_proof ~typ:mkProp to understand why - we don't we use the type stored here. This is obviously a - fixme [was like this for long time] - *) - let pe = - if i > 0 - then Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ) - else pe - in - let hook_data = Option.map (fun hook -> hook, uctx, []) info.Info.hook in - let ubind = if i = 0 then UState.universe_binders uctx else UnivNames.empty_binders in - let pe = Declare.Internal.map_entry_body pe - ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in - DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe + let declare_mutdef ~uctx ~info pe i DeclareDef.Recthm.{ name; impargs; typ; _} = + let { Info.hook; scope; kind; compute_guard; _ } = info in + (* if i = 0 , we don't touch the type; this is for compat + but not clear it is the right thing to do. + *) + let pe, ubind = + if i > 0 && not (CList.is_empty compute_guard) + then Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ), UnivNames.empty_binders + else pe, UState.universe_binders uctx + in + let hook_data = Option.map (fun hook -> hook, uctx, []) info.Info.hook in + (* We when compute_guard was [] in the previous step we should not + substitute the body *) + let pe = match compute_guard with + | [] -> pe + | _ -> + Declare.Internal.map_entry_body pe + ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) + in + DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe let declare_mutdef ~info ~uctx const = - let mutpe = adjust_guardness_conditions ~info const in - List.map_i (declare_mutdef ~info ~uctx mutpe) 0 info.Info.thms + let pe = match info.Info.compute_guard with + | [] -> + (* Not a recursive statement *) + const + | possible_indexes -> + (* Try all combinations... not optimal *) + let env = Global.env() in + Declare.Internal.map_entry_body const + ~f:(guess_decreasing env possible_indexes) + in + List.map_i (declare_mutdef ~info ~uctx pe) 0 info.Info.thms let declare_variable ~info ~uctx pe = let { Info.scope; hook } = info in -- cgit v1.2.3 From 9be8376b9c8b1b3fc9b37d1617b26ef54b172ca6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 02:27:54 -0400 Subject: [ComDefinition] Split program from regular declarations Proof "preparation" [as in `DeclareDef.prepare_definition`] is fairly more complicated in the Program case; in particular, it includes checking the existential variables, and elaborating a list of entries from the holes. Indeed, in the `Program` case we cannot use `DeclareDef.prepare_definition` while keeping a good level of abstraction, so we should introduce a `prepare_obligation` function. This PR is in preparation for that. --- plugins/funind/gen_principle.ml | 1 - vernac/comDefinition.ml | 56 +++++++++++++++++++++++------------------ vernac/comDefinition.mli | 16 ++++++++++-- vernac/vernacentries.ml | 4 ++- 4 files changed, 49 insertions(+), 28 deletions(-) diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 28cf5c7d98..4242da2802 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -375,7 +375,6 @@ let register_struct is_rec fixpoint_exprl = | None -> CErrors.user_err ~hdr:"Function" Pp.(str "Body of Function must be given") in ComDefinition.do_definition - ~program_mode:false ~name:fname.CAst.v ~poly:false ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index ba2c1ac115..c1be95fa67 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -79,30 +79,38 @@ let check_definition ~program_mode (ce, evd, _, imps) = check_evars_are_solved ~program_mode env evd; ce -let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = +let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = + let program_mode = false in let (ce, evd, udecl, impargs as def) = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - if program_mode then - let env = Global.env () in - let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in - assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); - assert(Univ.ContextSet.is_empty ctx); - Obligations.check_evars env evd; - let c = EConstr.of_constr c in - let typ = match ce.Declare.proof_entry_type with - | Some t -> EConstr.of_constr t - | None -> Retyping.get_type_of env evd c - in - let obls, _, c, cty = - Obligations.eterm_obligations env name evd 0 c typ - in - let uctx = Evd.evar_universe_context evd in - ignore(Obligations.add_definition - ~name ~term:c cty ~uctx ~udecl ~impargs ~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 - let kind = Decls.IsDefinition kind in - ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind:(Evd.universe_binders evd) ce ~impargs) + 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 + let kind = Decls.IsDefinition kind in + let ubind = Evd.universe_binders evd in + let _ : Names.GlobRef.t = + DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ce ~impargs + in () + +let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = + let program_mode = true in + let (ce, evd, udecl, impargs as def) = + interp_definition ~program_mode udecl bl ~poly red_option c ctypopt + in + let env = Global.env () in + let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in + assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); + assert(Univ.ContextSet.is_empty ctx); + Obligations.check_evars env evd; + let c = EConstr.of_constr c in + let typ = match ce.Declare.proof_entry_type with + | Some t -> EConstr.of_constr t + | None -> Retyping.get_type_of env evd c + in + let obls, _, c, cty = Obligations.eterm_obligations env name evd 0 c typ in + let uctx = Evd.evar_universe_context evd in + let _ : DeclareObl.progress = + Obligations.add_definition + ~name ~term:c cty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls + in () diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 6c6da8952e..7902b0ef09 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -15,8 +15,20 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition - : program_mode:bool - -> ?hook:DeclareDef.Hook.t + : ?hook:DeclareDef.Hook.t + -> name:Id.t + -> scope:DeclareDef.locality + -> poly:bool + -> kind:Decls.definition_object_kind + -> universe_decl_expr option + -> local_binder_expr list + -> red_expr option + -> constr_expr + -> constr_expr option + -> unit + +val do_definition_program + : ?hook:DeclareDef.Hook.t -> name:Id.t -> scope:DeclareDef.locality -> poly:bool diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 5497bd84ac..4806c6bb9c 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -567,7 +567,9 @@ let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt 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:name.v + let do_definition = + ComDefinition.(if program_mode then do_definition_program else do_definition) in + do_definition ~name:name.v ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook (* NB: pstate argument to use combinators easily *) -- cgit v1.2.3 From 56ffe818ab7706a82d79b538fdf3af8b23d95f40 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 03:07:42 -0400 Subject: [declare] [obligations] Refactor preparation of obligation entry Preparation of obligation/program entries requires low-level manipulation that does break the abstraction over `proof_entry`; we thus introduce `prepare_obligation`, and move the code that prepares the obligation entry to its own module. This seems to improve separation of concerns, and helps clarify the two of three current models in which Coq operates w.r.t. definitions: - single, ground entries with possibly mutual definitions [regular lemmas] - single, non-ground entries with possibly mutual definitions [obligations] - multiple entries [equations] --- doc/plugin_tutorial/tuto1/src/simple_declare.ml | 2 +- vernac/classes.ml | 4 +- vernac/comDefinition.ml | 32 +-- vernac/comDefinition.mli | 16 -- vernac/comProgramFixpoint.ml | 6 +- vernac/declareDef.ml | 25 +- vernac/declareDef.mli | 14 +- vernac/obligations.ml | 241 ------------------- vernac/obligations.mli | 40 +--- vernac/retrieveObl.ml | 296 ++++++++++++++++++++++++ vernac/retrieveObl.mli | 46 ++++ vernac/vernac.mllib | 1 + 12 files changed, 396 insertions(+), 327 deletions(-) create mode 100644 vernac/retrieveObl.ml create mode 100644 vernac/retrieveObl.mli diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 2fdca15552..3b906324f4 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,5 +1,5 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt = - let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false + let sigma, ce = DeclareDef.prepare_definition ~opaque ~poly sigma ~udecl ~types:tyopt ~body in let uctx = Evd.evar_universe_context sigma in let ubind = Evd.universe_binders sigma in diff --git a/vernac/classes.ml b/vernac/classes.ml index dafd1cc5e4..e0bf9e777c 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -315,7 +315,7 @@ let instance_hook info global imps ?hook cst = let declare_instance_constant info global imps ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in let sigma, entry = DeclareDef.prepare_definition - ~allow_evars:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in + ~poly sigma ~udecl ~types:(Some termtype) ~body:term in let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in Declare.definition_message name; DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); @@ -343,7 +343,7 @@ let declare_instance_program env sigma ~global ~poly name pri imps udecl term te let sigma = Evd.from_env env in declare_instance env sigma (Some pri) (not global) (GlobRef.ConstRef cst) in - let obls, _, term, typ = Obligations.eterm_obligations env name sigma 0 term termtype in + let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in let hook = DeclareDef.Hook.make hook in let uctx = Evd.evar_universe_context sigma in let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index c1be95fa67..eb70ad0ac0 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -68,49 +68,35 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt = (* Declare the definition *) let c = EConstr.it_mkLambda_or_LetIn c ctx in let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in + (c, tyopt), evd, udecl, imps - let evd, ce = DeclareDef.prepare_definition ~allow_evars:program_mode - ~opaque:false ~poly evd ~udecl ~types:tyopt ~body:c in - - (ce, evd, udecl, imps) - -let check_definition ~program_mode (ce, evd, _, imps) = +let check_definition ~program_mode (ce, evd) = let env = Global.env () in check_evars_are_solved ~program_mode env evd; ce let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let program_mode = false in - let (ce, evd, udecl, impargs as def) = + let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let ce = check_definition ~program_mode def in + let evd, ce = DeclareDef.prepare_definition ~opaque:false ~poly evd ~udecl ~types ~body in + let ce = check_definition ~program_mode (ce, evd) in let uctx = Evd.evar_universe_context evd in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in let kind = Decls.IsDefinition kind in let ubind = Evd.universe_binders evd in let _ : Names.GlobRef.t = - DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ce ~impargs + DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce in () let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let program_mode = true in - let (ce, evd, udecl, impargs as def) = + let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let env = Global.env () in - let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in - assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); - assert(Univ.ContextSet.is_empty ctx); - Obligations.check_evars env evd; - let c = EConstr.of_constr c in - let typ = match ce.Declare.proof_entry_type with - | Some t -> EConstr.of_constr t - | None -> Retyping.get_type_of env evd c - in - let obls, _, c, cty = Obligations.eterm_obligations env name evd 0 c typ in - let uctx = Evd.evar_universe_context evd in + let term, ty, uctx, obls = DeclareDef.prepare_obligation ~name ~poly ~body ~types ~udecl evd in let _ : DeclareObl.progress = Obligations.add_definition - ~name ~term:c cty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls + ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls in () diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 7902b0ef09..337da22018 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -39,19 +39,3 @@ val do_definition_program -> constr_expr -> constr_expr option -> unit - -(************************************************************************) -(** Internal API *) -(************************************************************************) - -(** Not used anywhere. *) -val interp_definition - : program_mode:bool - -> universe_decl_expr option - -> local_binder_expr list - -> poly:bool - -> red_expr option - -> constr_expr - -> constr_expr option - -> Evd.side_effects Declare.proof_entry * - Evd.evar_map * UState.universe_decl * Impargs.manual_implicits diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 3bac0419ef..f20b294499 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -254,9 +254,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = in (* XXX: Capturing sigma here... bad bad *) let hook = DeclareDef.Hook.make (hook sigma) in - Obligations.check_evars env sigma; + RetrieveObl.check_evars env sigma; let evars, _, evars_def, evars_typ = - Obligations.eterm_obligations env recname sigma 0 def typ + RetrieveObl.retrieve_obligations env recname sigma 0 def typ in let uctx = Evd.evar_universe_context sigma in ignore(Obligations.add_definition ~name:recname ~term:evars_def ~udecl @@ -287,7 +287,7 @@ let do_program_recursive ~scope ~poly fixkind fixl = let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = - Obligations.eterm_obligations env id evm + RetrieveObl.retrieve_obligations env id evm (List.length rec_sign) def typ in (id, def, typ, imps, evars) in diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index b0c8fe90c4..f283f700b7 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -157,7 +157,8 @@ let check_definition_evars ~allow_evars sigma = let env = Global.env () in if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma -let prepare_definition ~allow_evars ?opaque ?inline ~poly ~udecl ~types ~body sigma = +let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma = + let allow_evars = false in check_definition_evars ~allow_evars sigma; let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars) sigma (fun nf -> nf body, Option.map nf types) @@ -165,6 +166,28 @@ let prepare_definition ~allow_evars ?opaque ?inline ~poly ~udecl ~types ~body si let univs = Evd.check_univ_decl ~poly sigma udecl in sigma, definition_entry ?opaque ?inline ?types ~univs body +let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = + let allow_evars = true in + check_definition_evars ~allow_evars sigma; + let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars) + sigma (fun nf -> nf body, Option.map nf types) + in + let univs = Evd.check_univ_decl ~poly sigma udecl in + let ce = definition_entry ?opaque ?inline ?types ~univs body in + let env = Global.env () in + let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in + assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private); + assert(Univ.ContextSet.is_empty ctx); + RetrieveObl.check_evars env sigma; + let c = EConstr.of_constr c in + let typ = match ce.Declare.proof_entry_type with + | Some t -> EConstr.of_constr t + | None -> Retyping.get_type_of env sigma c + in + let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in + let uctx = Evd.evar_universe_context sigma in + c, cty, uctx, obls + let prepare_parameter ~allow_evars ~poly ~udecl ~types sigma = check_definition_evars ~allow_evars sigma; let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars) diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index e999027b44..27d9460382 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -89,8 +89,7 @@ val declare_mutually_recursive -> Names.GlobRef.t list val prepare_definition - : allow_evars:bool - -> ?opaque:bool + : ?opaque:bool -> ?inline:bool -> poly:bool -> udecl:UState.universe_decl @@ -99,6 +98,17 @@ val prepare_definition -> Evd.evar_map -> Evd.evar_map * Evd.side_effects Declare.proof_entry +val prepare_obligation + : ?opaque:bool + -> ?inline:bool + -> name:Id.t + -> poly:bool + -> udecl:UState.universe_decl + -> types:EConstr.t option + -> body:EConstr.t + -> Evd.evar_map + -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info + val prepare_parameter : allow_evars:bool -> poly:bool diff --git a/vernac/obligations.ml b/vernac/obligations.ml index a29ba44907..0ffcea3867 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -10,252 +10,16 @@ open Printf -(** - - Get types of existentials ; - - Flatten dependency tree (prefix order) ; - - Replace existentials by de Bruijn indices in term, applied to the right arguments ; - - Apply term prefixed by quantification on "existentials". -*) - -open Constr open Names open Pp open CErrors open Util -module NamedDecl = Context.Named.Declaration - (* For the records fields, opens should go away one these types are private *) open DeclareObl open DeclareObl.Obligation open DeclareObl.ProgramDecl -let succfix (depth, fixrels) = - (succ depth, List.map succ fixrels) - -let check_evars env evm = - Evar.Map.iter - (fun key evi -> - if Evd.is_obligation_evar evm key then () - else - let (loc,k) = Evd.evar_source key evm in - Pretype_errors.error_unsolvable_implicit ?loc env evm key None) - (Evd.undefined_map evm) - -type oblinfo = - { ev_name: int * Id.t; - ev_hyps: EConstr.named_context; - ev_status: bool * Evar_kinds.obligation_definition_status; - ev_chop: int option; - ev_src: Evar_kinds.t Loc.located; - ev_typ: types; - ev_tac: unit Proofview.tactic option; - ev_deps: Int.Set.t } - -(** Substitute evar references in t using de Bruijn indices, - where n binders were passed through. *) - -let subst_evar_constr evm evs n idf t = - let seen = ref Int.Set.empty in - let transparent = ref Id.Set.empty in - let evar_info id = List.assoc_f Evar.equal id evs in - let rec substrec (depth, fixrels) c = match EConstr.kind evm c with - | Evar (k, args) -> - let { ev_name = (id, idstr) ; - ev_hyps = hyps ; ev_chop = chop } = - try evar_info k - with Not_found -> - anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found.") - in - seen := Int.Set.add id !seen; - (* Evar arguments are created in inverse order, - and we must not apply to defined ones (i.e. LetIn's) - *) - let args = - let n = match chop with None -> 0 | Some c -> c in - let (l, r) = List.chop n (List.rev (Array.to_list args)) in - List.rev r - in - let args = - let rec aux hyps args acc = - let open Context.Named.Declaration in - match hyps, args with - (LocalAssum _ :: tlh), (c :: tla) -> - aux tlh tla ((substrec (depth, fixrels) c) :: acc) - | (LocalDef _ :: tlh), (_ :: tla) -> - aux tlh tla acc - | [], [] -> acc - | _, _ -> acc (*failwith "subst_evars: invalid argument"*) - in aux hyps args [] - in - if List.exists - (fun x -> match EConstr.kind evm x with - | Rel n -> Int.List.mem n fixrels - | _ -> false) args - then - transparent := Id.Set.add idstr !transparent; - EConstr.mkApp (idf idstr, Array.of_list args) - | Fix _ -> - EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c - | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c - in - let t' = substrec (0, []) t in - EConstr.to_constr evm t', !seen, !transparent - - -(** Substitute variable references in t using de Bruijn indices, - where n binders were passed through. *) -let subst_vars acc n t = - let var_index id = Util.List.index Id.equal id acc in - let rec substrec depth c = match Constr.kind c with - | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c) - | _ -> Constr.map_with_binders succ substrec depth c - in - substrec 0 t - -(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ]) - to a product : forall H1 : t1, ..., forall Hn : tn, concl. - Changes evars and hypothesis references to variable references. -*) -let etype_of_evar evm evs hyps concl = - let open Context.Named.Declaration in - let rec aux acc n = function - decl :: tl -> - let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar (NamedDecl.get_type decl) in - let t'' = subst_vars acc 0 t' in - let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in - let s' = Int.Set.union s s' in - let trans' = Id.Set.union trans trans' in - (match decl with - | LocalDef (id,c,_) -> - let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in - let c' = subst_vars acc 0 c' in - Term.mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest, - Int.Set.union s'' s', - Id.Set.union trans'' trans' - | LocalAssum (id,_) -> - Term.mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') - | [] -> - let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in - subst_vars acc 0 t', s, trans - in aux [] 0 (List.rev hyps) - -let trunc_named_context n ctx = - let len = List.length ctx in - List.firstn (len - n) ctx - -let rec chop_product n t = - let pop t = Vars.lift (-1) t in - if Int.equal n 0 then Some t - else - match Constr.kind t with - | Prod (_, _, b) -> if Vars.noccurn 1 b then chop_product (pred n) (pop b) else None - | _ -> None - -let evar_dependencies evm oev = - let one_step deps = - Evar.Set.fold (fun ev s -> - let evi = Evd.find evm ev in - let deps' = Evd.evars_of_filtered_evar_info evm evi in - if Evar.Set.mem oev deps' then - invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev) - else Evar.Set.union deps' s) - deps deps - in - let rec aux deps = - let deps' = one_step deps in - if Evar.Set.equal deps deps' then deps - else aux deps' - in aux (Evar.Set.singleton oev) - -let move_after (id, ev, deps as obl) l = - let rec aux restdeps = function - | (id', _, _) as obl' :: tl -> - let restdeps' = Evar.Set.remove id' restdeps in - if Evar.Set.is_empty restdeps' then - obl' :: obl :: tl - else obl' :: aux restdeps' tl - | [] -> [obl] - in aux (Evar.Set.remove id deps) l - -let sort_dependencies evl = - let rec aux l found list = - match l with - | (id, ev, deps) as obl :: tl -> - let found' = Evar.Set.union found (Evar.Set.singleton id) in - if Evar.Set.subset deps found' then - aux tl found' (obl :: list) - else aux (move_after obl tl) found list - | [] -> List.rev list - in aux evl Evar.Set.empty [] - -let eterm_obligations env name evm fs ?status t ty = - (* 'Serialize' the evars *) - let nc = Environ.named_context env in - let nc_len = Context.Named.length nc in - let evm = Evarutil.nf_evar_map_undefined evm in - let evl = Evarutil.non_instantiated evm in - let evl = Evar.Map.bindings evl in - let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in - let sevl = sort_dependencies evl in - let evl = List.map (fun (id, ev, _) -> id, ev) sevl in - let evn = - let i = ref (-1) in - List.rev_map (fun (id, ev) -> incr i; - (id, (!i, Id.of_string - (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i))), - ev)) evl - in - let evts = - (* Remove existential variables in types and build the corresponding products *) - List.fold_right - (fun (id, (n, nstr), ev) l -> - let hyps = Evd.evar_filtered_context ev in - let hyps = trunc_named_context nc_len hyps in - let evtyp, deps, transp = etype_of_evar evm l hyps ev.Evd.evar_concl in - let evtyp, hyps, chop = - match chop_product fs evtyp with - | Some t -> t, trunc_named_context fs hyps, fs - | None -> evtyp, hyps, 0 - in - let loc, k = Evd.evar_source id evm in - let status = match k with - | Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o - | _ -> match status with - | Some o -> o - | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ())) - in - let force_status, status, chop = match status with - | Evar_kinds.Define true as stat -> - if not (Int.equal chop fs) then true, Evar_kinds.Define false, None - else false, stat, Some chop - | s -> false, s, None - in - let info = { ev_name = (n, nstr); - ev_hyps = hyps; ev_status = force_status, status; ev_chop = chop; - ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = None } - in (id, info) :: l) - evn [] - in - let t', _, transparent = (* Substitute evar refs in the term by variables *) - subst_evar_constr evm evts 0 EConstr.mkVar t - in - let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in - let evars = - List.map (fun (ev, info) -> - let { ev_name = (_, name); ev_status = force_status, status; - ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info - in - let force_status, status = match status with - | Evar_kinds.Define true when Id.Set.mem name transparent -> - true, Evar_kinds.Define false - | _ -> force_status, status - in name, typ, src, (force_status, status), deps, tac) evts - in - let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in - let evmap f c = pi1 (subst_evar_constr evm evts 0 f c) in - Array.of_list (List.rev evars), (evnames, evmap), t', ty - let pperror cmd = CErrors.user_err ~hdr:"Program" cmd let error s = pperror (str s) @@ -270,11 +34,6 @@ let explain_no_obligations = function Some ident -> str "No obligations for program " ++ Id.print ident | None -> str "No obligations remaining" -type obligation_info = - (Names.Id.t * types * Evar_kinds.t Loc.located * - (bool * Evar_kinds.obligation_definition_status) - * Int.Set.t * unit Proofview.tactic option) array - let assumption_message = Declare.assumption_message let default_tactic = ref (Proofview.tclUNIT ()) diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 101958072a..280b9a0c50 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -8,43 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Environ open Constr -open Evd -open Names - -val check_evars : env -> evar_map -> unit - -val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t -val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar_info * Evar.Set.t) list - -(* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *) -type obligation_info = - (Id.t * types * Evar_kinds.t Loc.located * - (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array - -(* env, id, evars, number of function prototypes to try to clear from - evars contexts, object and type *) -val eterm_obligations - : env - -> Id.t - -> evar_map - -> int - -> ?status:Evar_kinds.obligation_definition_status - -> EConstr.constr - -> EConstr.types - -> obligation_info * - - (* Existential key, obl. name, type as product, location of the - original evar, associated tactic, status and dependencies as - indexes into the array *) - ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * - - (* Translations from existential identifiers to obligation - identifiers and for terms with existentials to closed terms, - given a translation from obligation identifiers to constrs, - new term, new type *) - constr * types val default_tactic : unit Proofview.tactic ref @@ -61,12 +25,12 @@ val add_definition -> ?reduce:(constr -> constr) -> ?hook:DeclareDef.Hook.t -> ?opaque:bool - -> obligation_info + -> RetrieveObl.obligation_info -> DeclareObl.progress val add_mutual_definitions (* XXX: unify with MutualEntry *) - : (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list + : (Names.Id.t * constr * types * Impargs.manual_implicits * RetrieveObl.obligation_info) list -> uctx:UState.t -> ?udecl:UState.universe_decl (** Universe binders and constraints *) diff --git a/vernac/retrieveObl.ml b/vernac/retrieveObl.ml new file mode 100644 index 0000000000..c529972b8d --- /dev/null +++ b/vernac/retrieveObl.ml @@ -0,0 +1,296 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + if Evd.is_obligation_evar evm key then () + else + let loc, k = Evd.evar_source key evm in + Pretype_errors.error_unsolvable_implicit ?loc env evm key None) + (Evd.undefined_map evm) + +type obligation_info = + ( Names.Id.t + * Constr.types + * Evar_kinds.t Loc.located + * (bool * Evar_kinds.obligation_definition_status) + * Int.Set.t + * unit Proofview.tactic option ) + array + +type oblinfo = + { ev_name : int * Id.t + ; ev_hyps : EConstr.named_context + ; ev_status : bool * Evar_kinds.obligation_definition_status + ; ev_chop : int option + ; ev_src : Evar_kinds.t Loc.located + ; ev_typ : Constr.types + ; ev_tac : unit Proofview.tactic option + ; ev_deps : Int.Set.t } + +(** Substitute evar references in t using de Bruijn indices, + where n binders were passed through. *) + +let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) + +let subst_evar_constr evm evs n idf t = + let seen = ref Int.Set.empty in + let transparent = ref Id.Set.empty in + let evar_info id = CList.assoc_f Evar.equal id evs in + let rec substrec (depth, fixrels) c = + match EConstr.kind evm c with + | Constr.Evar (k, args) -> + let {ev_name = id, idstr; ev_hyps = hyps; ev_chop = chop} = + try evar_info k + with Not_found -> + CErrors.anomaly ~label:"eterm" + Pp.( + str "existential variable " + ++ int (Evar.repr k) + ++ str " not found.") + in + seen := Int.Set.add id !seen; + (* Evar arguments are created in inverse order, + and we must not apply to defined ones (i.e. LetIn's) + *) + let args = + let n = match chop with None -> 0 | Some c -> c in + let l, r = CList.chop n (List.rev (Array.to_list args)) in + List.rev r + in + let args = + let rec aux hyps args acc = + let open Context.Named.Declaration in + match (hyps, args) with + | LocalAssum _ :: tlh, c :: tla -> + aux tlh tla (substrec (depth, fixrels) c :: acc) + | LocalDef _ :: tlh, _ :: tla -> aux tlh tla acc + | [], [] -> acc + | _, _ -> acc + (*failwith "subst_evars: invalid argument"*) + in + aux hyps args [] + in + if + List.exists + (fun x -> + match EConstr.kind evm x with + | Constr.Rel n -> Int.List.mem n fixrels + | _ -> false) + args + then transparent := Id.Set.add idstr !transparent; + EConstr.mkApp (idf idstr, Array.of_list args) + | Constr.Fix _ -> + EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c + | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c + in + let t' = substrec (0, []) t in + (EConstr.to_constr evm t', !seen, !transparent) + +(** Substitute variable references in t using de Bruijn indices, + where n binders were passed through. *) +let subst_vars acc n t = + let var_index id = Util.List.index Id.equal id acc in + let rec substrec depth c = + match Constr.kind c with + | Constr.Var v -> ( + try Constr.mkRel (depth + var_index v) with Not_found -> c ) + | _ -> Constr.map_with_binders succ substrec depth c + in + substrec 0 t + +(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ]) + to a product : forall H1 : t1, ..., forall Hn : tn, concl. + Changes evars and hypothesis references to variable references. +*) +let etype_of_evar evm evs hyps concl = + let open Context.Named.Declaration in + let rec aux acc n = function + | decl :: tl -> ( + let t', s, trans = + subst_evar_constr evm evs n EConstr.mkVar + (Context.Named.Declaration.get_type decl) + in + let t'' = subst_vars acc 0 t' in + let rest, s', trans' = + aux (Context.Named.Declaration.get_id decl :: acc) (succ n) tl + in + let s' = Int.Set.union s s' in + let trans' = Id.Set.union trans trans' in + match decl with + | LocalDef (id, c, _) -> + let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in + let c' = subst_vars acc 0 c' in + ( Term.mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest + , Int.Set.union s'' s' + , Id.Set.union trans'' trans' ) + | LocalAssum (id, _) -> + (Term.mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') ) + | [] -> + let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in + (subst_vars acc 0 t', s, trans) + in + aux [] 0 (List.rev hyps) + +let trunc_named_context n ctx = + let len = List.length ctx in + CList.firstn (len - n) ctx + +let rec chop_product n t = + let pop t = Vars.lift (-1) t in + if Int.equal n 0 then Some t + else + match Constr.kind t with + | Constr.Prod (_, _, b) -> + if Vars.noccurn 1 b then chop_product (pred n) (pop b) else None + | _ -> None + +let evar_dependencies evm oev = + let one_step deps = + Evar.Set.fold + (fun ev s -> + let evi = Evd.find evm ev in + let deps' = Evd.evars_of_filtered_evar_info evm evi in + if Evar.Set.mem oev deps' then + invalid_arg + ( "Ill-formed evar map: cycle detected for evar " + ^ Pp.string_of_ppcmds @@ Evar.print oev ) + else Evar.Set.union deps' s) + deps deps + in + let rec aux deps = + let deps' = one_step deps in + if Evar.Set.equal deps deps' then deps else aux deps' + in + aux (Evar.Set.singleton oev) + +let move_after ((id, ev, deps) as obl) l = + let rec aux restdeps = function + | ((id', _, _) as obl') :: tl -> + let restdeps' = Evar.Set.remove id' restdeps in + if Evar.Set.is_empty restdeps' then obl' :: obl :: tl + else obl' :: aux restdeps' tl + | [] -> [obl] + in + aux (Evar.Set.remove id deps) l + +let sort_dependencies evl = + let rec aux l found list = + match l with + | ((id, ev, deps) as obl) :: tl -> + let found' = Evar.Set.union found (Evar.Set.singleton id) in + if Evar.Set.subset deps found' then aux tl found' (obl :: list) + else aux (move_after obl tl) found list + | [] -> List.rev list + in + aux evl Evar.Set.empty [] + +let retrieve_obligations env name evm fs ?status t ty = + (* 'Serialize' the evars *) + let nc = Environ.named_context env in + let nc_len = Context.Named.length nc in + let evm = Evarutil.nf_evar_map_undefined evm in + let evl = Evarutil.non_instantiated evm in + let evl = Evar.Map.bindings evl in + let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in + let sevl = sort_dependencies evl in + let evl = List.map (fun (id, ev, _) -> (id, ev)) sevl in + let evn = + let i = ref (-1) in + List.rev_map + (fun (id, ev) -> + incr i; + ( id + , ( !i + , Id.of_string + (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i)) ) + , ev )) + evl + in + let evts = + (* Remove existential variables in types and build the corresponding products *) + List.fold_right + (fun (id, (n, nstr), ev) l -> + let hyps = Evd.evar_filtered_context ev in + let hyps = trunc_named_context nc_len hyps in + let evtyp, deps, transp = etype_of_evar evm l hyps ev.Evd.evar_concl in + let evtyp, hyps, chop = + match chop_product fs evtyp with + | Some t -> (t, trunc_named_context fs hyps, fs) + | None -> (evtyp, hyps, 0) + in + let loc, k = Evd.evar_source id evm in + let status = + match k with + | Evar_kinds.QuestionMark {Evar_kinds.qm_obligation = o} -> o + | _ -> ( + match status with + | Some o -> o + | None -> + Evar_kinds.Define (not (Program.get_proofs_transparency ())) ) + in + let force_status, status, chop = + match status with + | Evar_kinds.Define true as stat -> + if not (Int.equal chop fs) then (true, Evar_kinds.Define false, None) + else (false, stat, Some chop) + | s -> (false, s, None) + in + let info = + { ev_name = (n, nstr) + ; ev_hyps = hyps + ; ev_status = (force_status, status) + ; ev_chop = chop + ; ev_src = (loc, k) + ; ev_typ = evtyp + ; ev_deps = deps + ; ev_tac = None } + in + (id, info) :: l) + evn [] + in + let t', _, transparent = + (* Substitute evar refs in the term by variables *) + subst_evar_constr evm evts 0 EConstr.mkVar t + in + let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in + let evars = + List.map + (fun (ev, info) -> + let { ev_name = _, name + ; ev_status = force_status, status + ; ev_src = src + ; ev_typ = typ + ; ev_deps = deps + ; ev_tac = tac } = + info + in + let force_status, status = + match status with + | Evar_kinds.Define true when Id.Set.mem name transparent -> + (true, Evar_kinds.Define false) + | _ -> (force_status, status) + in + (name, typ, src, (force_status, status), deps, tac)) + evts + in + let evnames = List.map (fun (ev, info) -> (ev, snd info.ev_name)) evts in + let evmap f c = Util.pi1 (subst_evar_constr evm evts 0 f c) in + (Array.of_list (List.rev evars), (evnames, evmap), t', ty) diff --git a/vernac/retrieveObl.mli b/vernac/retrieveObl.mli new file mode 100644 index 0000000000..c9c45bd889 --- /dev/null +++ b/vernac/retrieveObl.mli @@ -0,0 +1,46 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Evd.evar_map -> unit + +type obligation_info = + ( Names.Id.t + * Constr.types + * Evar_kinds.t Loc.located + * (bool * Evar_kinds.obligation_definition_status) + * Int.Set.t + * unit Proofview.tactic option ) + array +(** ident, type, location of the original evar, (opaque or + transparent, expand or define), dependencies as indexes into the + array, tactic to solve it *) + +val retrieve_obligations : + Environ.env + -> Names.Id.t + -> Evd.evar_map + -> int + -> ?status:Evar_kinds.obligation_definition_status + -> EConstr.t + -> EConstr.types + -> obligation_info + * ( (Evar.t * Names.Id.t) list + * ((Names.Id.t -> EConstr.t) -> EConstr.t -> Constr.t) ) + * Constr.t + * Constr.t +(** [retrieve_obligations env id sigma fs ?status body type] returns + [obls, (evnames, evmap), nbody, ntype] a list of obligations built + from evars in [body, type]. + + [fs] is the number of function prototypes to try to clear from + evars contexts. [evnames, evmap) is the list of names / + substitution functions used to program with holes. This is not used + in Coq, but in the equations plugin; [evnames] is actually + redundant with the information contained in [obls] *) diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 6e398d87ca..5a2bdb43d4 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -14,6 +14,7 @@ Proof_using Egramcoq Metasyntax DeclareUniv +RetrieveObl DeclareDef DeclareObl Canonical -- cgit v1.2.3 From d507679b5b6dfac944e038b6a3ebd9fb8e6998ff Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 03:19:15 -0400 Subject: [declareDef] Cleanup of allow_evars and check_evars We don't the parameter anymore as the paths are too different now. Note that this removes a duplicate `check_evars` that has been in `master` quite some time [double check in `ComDefinition` and in `DeclareDef.prepare_definition`] --- vernac/classes.ml | 2 +- vernac/comDefinition.ml | 7 ------- vernac/declareDef.ml | 21 ++++++++------------- vernac/declareDef.mli | 3 +-- 4 files changed, 10 insertions(+), 23 deletions(-) diff --git a/vernac/classes.ml b/vernac/classes.ml index e0bf9e777c..65d20a13a1 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -328,7 +328,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst in let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma ~udecl ~types:termtype in + let sigma, entry = DeclareDef.prepare_parameter ~poly sigma ~udecl ~types:termtype in let cst = Declare.declare_constant ~name ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index eb70ad0ac0..73b523f0b3 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -12,7 +12,6 @@ open Pp open Util open Redexpr open Constrintern -open Pretyping (* Commands of the interface: Constant definitions *) @@ -70,18 +69,12 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt = let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in (c, tyopt), evd, udecl, imps -let check_definition ~program_mode (ce, evd) = - let env = Global.env () in - check_evars_are_solved ~program_mode env evd; - ce - let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let program_mode = false in let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in let evd, ce = DeclareDef.prepare_definition ~opaque:false ~poly evd ~udecl ~types ~body in - let ce = check_definition ~program_mode (ce, evd) in let uctx = Evd.evar_universe_context evd in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in let kind = Decls.IsDefinition kind in diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index f283f700b7..2528dfd38f 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -153,23 +153,17 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = (* Preparing proof entries *) -let check_definition_evars ~allow_evars sigma = - let env = Global.env () in - if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma - let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma = - let allow_evars = false in - check_definition_evars ~allow_evars sigma; - let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars) + let env = Global.env () in + Pretyping.check_evars_are_solved ~program_mode:false env sigma; + let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true sigma (fun nf -> nf body, Option.map nf types) in let univs = Evd.check_univ_decl ~poly sigma udecl in sigma, definition_entry ?opaque ?inline ?types ~univs body let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = - let allow_evars = true in - check_definition_evars ~allow_evars sigma; - let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars) + let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false sigma (fun nf -> nf body, Option.map nf types) in let univs = Evd.check_univ_decl ~poly sigma udecl in @@ -188,9 +182,10 @@ let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = let uctx = Evd.evar_universe_context sigma in c, cty, uctx, obls -let prepare_parameter ~allow_evars ~poly ~udecl ~types sigma = - check_definition_evars ~allow_evars sigma; - let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars) +let prepare_parameter ~poly ~udecl ~types sigma = + let env = Global.env () in + Pretyping.check_evars_are_solved ~program_mode:false env sigma; + let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:true sigma (fun nf -> nf types) in let univs = Evd.check_univ_decl ~poly sigma udecl in diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 27d9460382..f72954d8c2 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -110,8 +110,7 @@ val prepare_obligation -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info val prepare_parameter - : allow_evars:bool - -> poly:bool + : poly:bool -> udecl:UState.universe_decl -> types:EConstr.types -> Evd.evar_map -- cgit v1.2.3 From 8ac27a8261f5f3fb5d4bf2a207a144df07477910 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 03:42:57 -0400 Subject: [declare] Make the type of closed entries opaque. This is a step in forcing all entry creation go thru the preparation functions. We still need to handle plain `Declare.` calls, but this will be next step. We need to leave a backdoor for interactive proofs until we unify proof preparation happening in `Proof_global` with the one happening in `DeclareDef`, but we are getting there. TODO: see how to avoid the normalization problems in DeclareObl --- plugins/funind/gen_principle.ml | 1 + vernac/classes.ml | 23 ++++++++++++----------- vernac/comAssumption.ml | 2 ++ vernac/declareDef.ml | 11 +++++++++-- vernac/declareDef.mli | 15 +++++++++++++-- vernac/declareObl.ml | 29 +++++++++-------------------- vernac/lemmas.ml | 1 + 7 files changed, 47 insertions(+), 35 deletions(-) diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 4242da2802..47e56b81aa 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -291,6 +291,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) *) let uctx = Evd.evar_universe_context sigma in let hook_data = hook, uctx, [] in + let entry = DeclareDef.ClosedDef.of_proof_entry entry in let _ : Names.GlobRef.t = DeclareDef.declare_definition ~name:new_princ_name ~hook_data ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) diff --git a/vernac/classes.ml b/vernac/classes.ml index 65d20a13a1..88b6ab34ff 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -304,22 +304,21 @@ let id_of_class cl = mip.(0).Declarations.mind_typename | _ -> assert false -let instance_hook info global imps ?hook cst = - Impargs.maybe_declare_manual_implicits false cst imps; +let instance_hook info global ?hook cst = let info = intern_info info in let env = Global.env () in let sigma = Evd.from_env env in declare_instance env sigma (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant info global imps ?hook name udecl poly sigma term termtype = +let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in let sigma, entry = DeclareDef.prepare_definition ~poly sigma ~udecl ~types:(Some termtype) ~body:term in - let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in - Declare.definition_message name; - DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); - instance_hook info global imps ?hook (GlobRef.ConstRef kn) + let ubind = Evd.universe_binders sigma in + let scope = DeclareDef.Global Declare.ImportDefaultBehavior in + let kn = DeclareDef.declare_definition ~name ~kind ~scope ~ubind ~impargs entry in + instance_hook info global ?hook kn let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name = let subst = List.fold_left2 @@ -332,7 +331,9 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst let cst = Declare.declare_constant ~name ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); - instance_hook pri global impargs (GlobRef.ConstRef cst) + let cst = (GlobRef.ConstRef cst) in + Impargs.maybe_declare_manual_implicits false cst impargs; + instance_hook pri global cst let declare_instance_program env sigma ~global ~poly name pri imps udecl term termtype = let hook { DeclareDef.Hook.S.scope; dref; _ } = @@ -351,7 +352,7 @@ let declare_instance_program env sigma ~global ~poly name pri imps udecl term te Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook typ ~uctx obls in () -let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype = +let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype = (* spiwack: it is hard to reorder the actions to do the pretyping after the proof has opened. As a consequence, we use the low-level primitives to code @@ -359,12 +360,12 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in let kind = Decls.(IsDefinition Instance) in - let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in + let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in let info = Lemmas.Info.make ~hook ~kind () in (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails! This is due to a bug in proof_global :( *) let termtype = Evarutil.nf_evar sigma termtype in - let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma termtype in + let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info ~impargs sigma termtype in (* spiwack: I don't know what to do with the status here. *) let lemma = match term with diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index dc9c8e2d3c..cb9acda770 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -203,6 +203,8 @@ let context_insection sigma ~poly ctx = else Monomorphic_entry Univ.ContextSet.empty in let entry = Declare.definition_entry ~univs ~types:t b in + (* XXX Fixme: Use DeclareDef.prepare_definition *) + let entry = DeclareDef.ClosedDef.of_proof_entry entry in let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge ~kind:Decls.(IsDefinition Definition) ~ubind:UnivNames.empty_binders ~impargs:[] entry in diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 2528dfd38f..84310cba65 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -38,6 +38,13 @@ module Hook = struct end +module ClosedDef = struct + + type t = Evd.side_effects Declare.proof_entry + + let of_proof_entry x = x +end + (* Locality stuff *) let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = let should_suggest = ce.Declare.proof_entry_opaque && @@ -153,14 +160,14 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe = (* Preparing proof entries *) -let prepare_definition ?opaque ?inline ~poly ~udecl ~types ~body sigma = +let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma = let env = Global.env () in Pretyping.check_evars_are_solved ~program_mode:false env sigma; let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true sigma (fun nf -> nf body, Option.map nf types) in let univs = Evd.check_univ_decl ~poly sigma udecl in - sigma, definition_entry ?opaque ?inline ?types ~univs body + sigma, definition_entry ?fix_exn ?opaque ?inline ?types ~univs body let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index f72954d8c2..9c5cd6fc2a 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -39,6 +39,13 @@ module Hook : sig val call : ?hook:t -> S.t -> unit end +module ClosedDef : sig + type t + + (* Don't use for non-interactive proofs *) + val of_proof_entry : Evd.side_effects Declare.proof_entry -> t +end + val declare_definition : name:Id.t -> scope:locality @@ -46,7 +53,7 @@ val declare_definition -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> ubind:UnivNames.universe_binders -> impargs:Impargs.manual_implicits - -> Evd.side_effects Declare.proof_entry + -> ClosedDef.t -> GlobRef.t val declare_assumption @@ -88,15 +95,19 @@ val declare_mutually_recursive -> Recthm.t list -> Names.GlobRef.t list +(* The common use of the returned evar_map is to obtain the universe + binders and context for the hook; we should refactor that soon by + merging prepare and declare. *) val prepare_definition : ?opaque:bool -> ?inline:bool + -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> poly:bool -> udecl:UState.universe_decl -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map - -> Evd.evar_map * Evd.side_effects Declare.proof_entry + -> Evd.evar_map * ClosedDef.t val prepare_obligation : ?opaque:bool diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 24a52eaca4..e643ffa98d 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -362,28 +362,17 @@ let get_fix_exn, stm_get_fix_exn = Hook.make () let declare_definition prg = let varsubst = obligation_substitution true prg in - let body, typ = subst_prog varsubst prg in - let nf = - UnivSubst.nf_evars_and_universes_opt_subst - (fun x -> None) - (UState.subst prg.prg_ctx) - in - let opaque = prg.prg_opaque in + let sigma = Evd.from_ctx prg.prg_ctx in + let body, types = subst_prog varsubst prg in + let body, types = EConstr.(of_constr body, Some (of_constr types)) in + let opaque, poly, udecl = prg.prg_opaque, prg.prg_poly, prg.prg_univdecl in let fix_exn = Hook.get get_fix_exn () in - let typ = nf typ in - let body = nf body in - let obls = List.map (fun (id, (_, c)) -> (id, nf c)) varsubst in - let uvars = - Univ.LSet.union - (Vars.universes_of_constr typ) - (Vars.universes_of_constr body) - in - let uctx = UState.restrict prg.prg_ctx uvars in - let univs = - 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 obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in + (* XXX: This is doing normalization twice *) + let sigma, ce = + DeclareDef.prepare_definition ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma in let () = progmap_remove prg in + let uctx = Evd.evar_universe_context sigma in let ubind = UState.universe_binders uctx in let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in DeclareDef.declare_definition diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index e4a625d65c..a1bcf95bf5 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -242,6 +242,7 @@ end = struct Declare.Internal.map_entry_body pe ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in + let pe = DeclareDef.ClosedDef.of_proof_entry pe in DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe let declare_mutdef ~info ~uctx const = -- cgit v1.2.3 From ef8f09ef2fe338bb783591abb3cf8e6d5f4d404f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 04:36:44 -0400 Subject: [obligations] Remove unnecessary ctx variable `sigma` here is actually created from `uctx`, we also uniformize naming. --- vernac/declareObl.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index e643ffa98d..4b5564129f 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -520,7 +520,6 @@ let obligation_terminator entries uctx { name; num; auto } = (* Ensure universes are substituted properly in body and type *) let body = EConstr.to_constr sigma (EConstr.of_constr body) in let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in - let ctx = Evd.evar_universe_context sigma in let { obls; remaining=rem } = prg.prg_obligations in let obl = obls.(num) in let status = @@ -533,24 +532,24 @@ let obligation_terminator entries uctx { name; num; auto } = | (_, status), false -> status in let obl = { obl with obl_status = false, status } in - let ctx = - if prg.prg_poly then ctx - else UState.union prg.prg_ctx ctx + let uctx = + if prg.prg_poly then uctx + else UState.union prg.prg_ctx uctx in - let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in - let (defined, obl) = declare_obligation prg obl body ty uctx in + let univs = UState.univ_entry ~poly:prg.prg_poly uctx in + let (defined, obl) = declare_obligation prg obl body ty univs in let prg_ctx = 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 + UState.union prg.prg_ctx uctx else (* The first obligation, if defined, declares the univs of the constant, each subsequent obligation declares its own additional universes and constraints if any *) if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) - else ctx + else uctx in update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto | _ -> -- cgit v1.2.3 From dc03a4d9a7b527df0c2e571de55fd200666bdb11 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 05:44:46 -0400 Subject: [declareObl] Remove hack w.r.t. to universe normalization. This was introduced in #6203 , but as far as I can see this re-normalization step is not necessary. --- vernac/declareObl.ml | 3 --- 1 file changed, 3 deletions(-) diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 4b5564129f..f9d842d6a7 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -517,9 +517,6 @@ let obligation_terminator entries uctx { name; num; auto } = Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); (* Declare the obligation ourselves and drop the hook *) let prg = CEphemeron.get (ProgMap.find name !from_prg) in - (* Ensure universes are substituted properly in body and type *) - let body = EConstr.to_constr sigma (EConstr.of_constr body) in - let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in let { obls; remaining=rem } = prg.prg_obligations in let obl = obls.(num) in let status = -- cgit v1.2.3 From 8fbc927ac40cc707b1a940d8339a2a289755d533 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 16:34:30 -0400 Subject: [declareDef] More consistent handling of universe binders The only reasons that `prepare_definition` returned a sigma were: - to obtain the universe binders to be passed to declare - to obtain the UState.t to be passed to the equations hook We handle this automatically now; it seems like a reasonably good API improvement. However, it is not clear what we do now is right for all cases; must check. --- doc/plugin_tutorial/tuto1/src/simple_declare.ml | 7 +--- plugins/funind/gen_principle.ml | 6 +-- vernac/classes.ml | 5 +-- vernac/comAssumption.ml | 5 ++- vernac/comDefinition.ml | 7 +--- vernac/declareDef.ml | 54 ++++++++++++------------- vernac/declareDef.mli | 13 +++--- vernac/declareObl.ml | 15 +++---- vernac/lemmas.ml | 5 +-- 9 files changed, 51 insertions(+), 66 deletions(-) diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 3b906324f4..a2783d80e8 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,10 +1,7 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt = - let sigma, ce = DeclareDef.prepare_definition + let ce = DeclareDef.prepare_definition ~opaque ~poly sigma ~udecl ~types:tyopt ~body in - let uctx = Evd.evar_universe_context sigma in - let ubind = Evd.universe_binders sigma in - let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - DeclareDef.declare_definition ~name ~scope ~kind ~ubind ce ~impargs ?hook_data + DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ce let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 47e56b81aa..ebd280ecf6 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -290,13 +290,11 @@ 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 - let hook_data = hook, uctx, [] in - let entry = DeclareDef.ClosedDef.of_proof_entry entry in + let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in let _ : Names.GlobRef.t = DeclareDef.declare_definition - ~name:new_princ_name ~hook_data + ~name:new_princ_name ~hook ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:Decls.(IsProof Theorem) - ~ubind:UnivNames.empty_binders ~impargs:[] entry in () diff --git a/vernac/classes.ml b/vernac/classes.ml index 88b6ab34ff..a882f6db0a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -313,11 +313,10 @@ let instance_hook info global ?hook cst = let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in - let sigma, entry = DeclareDef.prepare_definition + let entry = DeclareDef.prepare_definition ~poly sigma ~udecl ~types:(Some termtype) ~body:term in - let ubind = Evd.universe_binders sigma in let scope = DeclareDef.Global Declare.ImportDefaultBehavior in - let kn = DeclareDef.declare_definition ~name ~kind ~scope ~ubind ~impargs entry in + let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs entry in instance_hook info global ?hook kn let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name = diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index cb9acda770..4a82696ea6 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -204,9 +204,10 @@ let context_insection sigma ~poly ctx = in let entry = Declare.definition_entry ~univs ~types:t b in (* XXX Fixme: Use DeclareDef.prepare_definition *) - let entry = DeclareDef.ClosedDef.of_proof_entry entry in + let uctx = Evd.evar_universe_context sigma in + let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge - ~kind:Decls.(IsDefinition Definition) ~ubind:UnivNames.empty_binders ~impargs:[] entry + ~kind:Decls.(IsDefinition Definition) ~impargs:[] entry in () in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 73b523f0b3..bf4567e57f 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -74,13 +74,10 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let evd, ce = DeclareDef.prepare_definition ~opaque:false ~poly evd ~udecl ~types ~body in - let uctx = Evd.evar_universe_context evd in - let hook_data = Option.map (fun hook -> hook, uctx, []) hook in + let ce = DeclareDef.prepare_definition ~opaque:false ~poly evd ~udecl ~types ~body in let kind = Decls.IsDefinition kind in - let ubind = Evd.universe_binders evd in let _ : Names.GlobRef.t = - DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce + DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs ce in () let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 84310cba65..14d3daf453 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -9,7 +9,6 @@ (************************************************************************) open Declare -open Impargs type locality = Discharge | Global of Declare.import_status @@ -40,40 +39,40 @@ end module ClosedDef = struct - type t = Evd.side_effects Declare.proof_entry + type t = + { entry : Evd.side_effects Declare.proof_entry + ; uctx : UState.t + } - let of_proof_entry x = x + let of_proof_entry ~uctx entry = { entry; uctx } end (* Locality stuff *) -let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = - let should_suggest = ce.Declare.proof_entry_opaque && - Option.is_empty ce.Declare.proof_entry_secctx in +let declare_definition ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ce = + let { ClosedDef.entry; uctx } = ce in + let should_suggest = entry.Declare.proof_entry_opaque && + Option.is_empty entry.Declare.proof_entry_secctx in + let ubind = UState.universe_binders uctx in let dref = match scope with | Discharge -> - let () = declare_variable ~name ~kind (SectionLocalDef ce) in + let () = declare_variable ~name ~kind (SectionLocalDef entry) in if should_suggest then Proof_using.suggest_variable (Global.env ()) name; Names.GlobRef.VarRef name | Global local -> - let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in + let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in let gr = Names.GlobRef.ConstRef kn in if should_suggest then Proof_using.suggest_constant (Global.env ()) kn; let () = DeclareUniv.declare_univ_binders gr ubind in gr in - let () = maybe_declare_manual_implicits false dref impargs in + let () = Impargs.maybe_declare_manual_implicits false dref impargs in let () = definition_message name in - begin - match hook_data with - | None -> () - | Some (hook, uctx, obls) -> - Hook.call ~hook { Hook.S.uctx; obls; scope; dref } - end; + Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook; dref -let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce = - let fix_exn = Declare.Internal.get_fix_exn ce in - try declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce +let declare_definition ~name ~scope ~kind ?hook ?obls ~impargs ce = + let fix_exn = Declare.Internal.get_fix_exn ce.ClosedDef.entry in + try declare_definition ~name ~scope ~kind ?hook ?obls ~impargs ce with exn -> let exn = Exninfo.capture exn in Exninfo.iraise (fix_exn exn) @@ -107,22 +106,21 @@ end let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems = let vars, fixdecls, indexes = mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in - let ubind, univs = + let uctx, univs = (* XXX: Obligations don't do this, this seems like a bug? *) if restrict_ucontext then - let evd = Evd.from_ctx uctx in - let evd = Evd.restrict_universe_context evd vars in - let univs = Evd.check_univ_decl ~poly evd udecl in - Evd.universe_binders evd, univs + let uctx = UState.restrict uctx vars in + let univs = UState.check_univ_decl ~poly uctx udecl in + uctx, univs else let univs = UState.univ_entry ~poly uctx in - UnivNames.empty_binders, univs + uctx, univs in let csts = CList.map2 (fun Recthm.{ name; typ; impargs } body -> - let ce = Declare.definition_entry ~opaque ~types:typ ~univs body in - declare_definition ~name ~scope ~kind ~ubind ~impargs ce) + let entry = Declare.definition_entry ~opaque ~types:typ ~univs body in + declare_definition ~name ~scope ~kind ~impargs { ClosedDef.entry; uctx }) fixitems fixdecls in let isfix = Option.is_empty possible_indexes in @@ -167,7 +165,9 @@ let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma sigma (fun nf -> nf body, Option.map nf types) in let univs = Evd.check_univ_decl ~poly sigma udecl in - sigma, definition_entry ?fix_exn ?opaque ?inline ?types ~univs body + let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in + let uctx = Evd.evar_universe_context sigma in + { ClosedDef.entry; uctx } let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 9c5cd6fc2a..8f3db59ba9 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -43,15 +43,17 @@ module ClosedDef : sig type t (* Don't use for non-interactive proofs *) - val of_proof_entry : Evd.side_effects Declare.proof_entry -> t + val of_proof_entry + : uctx:UState.t + -> Evd.side_effects Declare.proof_entry -> t end val declare_definition : name:Id.t -> scope:locality -> kind:Decls.logical_kind - -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> ubind:UnivNames.universe_binders + -> ?hook:Hook.t + -> ?obls:(Id.t * Constr.t) list -> impargs:Impargs.manual_implicits -> ClosedDef.t -> GlobRef.t @@ -95,9 +97,6 @@ val declare_mutually_recursive -> Recthm.t list -> Names.GlobRef.t list -(* The common use of the returned evar_map is to obtain the universe - binders and context for the hook; we should refactor that soon by - merging prepare and declare. *) val prepare_definition : ?opaque:bool -> ?inline:bool @@ -107,7 +106,7 @@ val prepare_definition -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map - -> Evd.evar_map * ClosedDef.t + -> ClosedDef.t val prepare_obligation : ?opaque:bool diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index f9d842d6a7..4c62582c23 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -365,20 +365,15 @@ let declare_definition prg = let sigma = Evd.from_ctx prg.prg_ctx in let body, types = subst_prog varsubst prg in let body, types = EConstr.(of_constr body, Some (of_constr types)) in - let opaque, poly, udecl = prg.prg_opaque, prg.prg_poly, prg.prg_univdecl in + (* All these should be grouped into a struct a some point *) + let opaque, poly, udecl, hook = prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook in + let name, scope, kind, impargs = prg.prg_name, prg.prg_scope, Decls.(IsDefinition prg.prg_kind), prg.prg_implicits in let fix_exn = Hook.get get_fix_exn () in let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in (* XXX: This is doing normalization twice *) - let sigma, ce = - DeclareDef.prepare_definition ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma in + let ce = DeclareDef.prepare_definition ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma in let () = progmap_remove prg in - let uctx = Evd.evar_universe_context sigma in - let ubind = UState.universe_binders uctx in - let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in - DeclareDef.declare_definition - ~name:prg.prg_name ~scope:prg.prg_scope ~ubind - ~kind:Decls.(IsDefinition prg.prg_kind) ce - ~impargs:prg.prg_implicits ?hook_data + DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls ce let rec lam_index n t acc = match Constr.kind t with diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index a1bcf95bf5..042fdd6885 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -233,7 +233,6 @@ end = struct then Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ), UnivNames.empty_binders else pe, UState.universe_binders uctx in - let hook_data = Option.map (fun hook -> hook, uctx, []) info.Info.hook in (* We when compute_guard was [] in the previous step we should not substitute the body *) let pe = match compute_guard with @@ -242,8 +241,8 @@ end = struct Declare.Internal.map_entry_body pe ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in - let pe = DeclareDef.ClosedDef.of_proof_entry pe in - DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe + let pe = DeclareDef.ClosedDef.of_proof_entry ~uctx pe in + DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs pe let declare_mutdef ~info ~uctx const = let pe = match info.Info.compute_guard with -- cgit v1.2.3 From 7b2e166eae2d9f83bf0e14f68075b0be0a8bd668 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 14 Mar 2020 23:14:12 -0400 Subject: [classes] Declare obligation implicits using standard API. --- vernac/classes.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/vernac/classes.ml b/vernac/classes.ml index a882f6db0a..40c1a5d97d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -334,10 +334,9 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst Impargs.maybe_declare_manual_implicits false cst impargs; instance_hook pri global cst -let declare_instance_program env sigma ~global ~poly name pri imps udecl term termtype = +let declare_instance_program env sigma ~global ~poly name pri impargs udecl term termtype = let hook { DeclareDef.Hook.S.scope; dref; _ } = let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in - Impargs.declare_manual_implicits false dref imps; let pri = intern_info pri in let env = Global.env () in let sigma = Evd.from_env env in @@ -348,7 +347,7 @@ let declare_instance_program env sigma ~global ~poly name pri imps udecl term te let uctx = Evd.evar_universe_context sigma in let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in let _ : DeclareObl.progress = - Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook typ ~uctx obls + Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls in () let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype = -- cgit v1.2.3 From fa6836e85808c6d97620104b2f33dff49eb2aa74 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 15 Mar 2020 16:13:24 -0400 Subject: [doc] [obligations] Some notes about `Program` implementation --- vernac/obligations.mli | 117 ++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 92 insertions(+), 25 deletions(-) diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 280b9a0c50..cb54dfdeb2 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -10,13 +10,71 @@ open Constr +(** Coq's Program mode support. This mode extends declarations of + constants and fixpoints with [Program Definition] and [Program + Fixpoint] to support incremental construction of terms using + delayed proofs, called "obligations" + + The mode also provides facilities for managing and auto-solving + sets of obligations. + + The basic code flow of programs/obligations is as follows: + + - [add_definition] / [add_mutual_definitions] are called from the + respective [Program] vernacular command interpretation; at this + point the only extra work we do is to prepare the new definition + [d] using [RetrieveObl], which consists in turning unsolved evars + into obligations. [d] is not sent to the kernel yet, as it is not + complete and cannot be typchecked, but saved in a special + data-structure. Auto-solving of obligations is tried at this stage + (see below) + + - [next_obligation] will retrieve the next obligation + ([RetrieveObl] sorts them by topological order) and will try to + solve it. When all obligations are solved, the original constant + [d] is grounded and sent to the kernel for addition to the global + environment. Auto-solving of obligations is also triggered on + obligation completion. + +{2} Solving of obligations: Solved obligations are stored as regular + global declarations in the global environment, usually with name + [constant_obligation_number] where [constant] is the original + [constant] and [number] is the corresponding (internal) number. + + Solving an obligation can trigger a bit of a complex cascaded + callback path; closing an obligation can indeed allow all other + obligations to be closed, which in turn may trigged the declaration + of the original constant. Care must be taken, as this can modify + [Global.env] in arbitrarily ways. Current code takes some care to + refresh the [env] in the proper boundaries, but the invariants + remain delicate. + +{2} Saving of obligations: as open obligations use the regular proof + mode, a `Qed` will call `Lemmas.save_lemma` first. For this reason + obligations code is split in two: this file, [Obligations], taking + care of the top-level vernac commands, and [DeclareObl], which is + called by `Lemmas` to close an obligation proof and eventually to + declare the top-level [Program]ed constant. + + There is little obligations-specific code in [DeclareObl], so + eventually that file should be integrated in the regular [Declare] + path, as it gains better support for "dependent_proofs". + + *) + val default_tactic : unit Proofview.tactic ref -val add_definition - : name:Names.Id.t - -> ?term:constr -> types +(** Start a [Program Definition c] proof. [uctx] [udecl] [impargs] + [kind] [scope] [poly] etc... come from the interpretation of the + vernacular; `obligation_info` was generated by [RetrieveObl] It + will return whether all the obligations were solved; if so, it will + also register [c] with the kernel. *) +val add_definition : + name:Names.Id.t + -> ?term:constr + -> types -> uctx:UState.t - -> ?udecl:UState.universe_decl (* Universe binders and constraints *) + -> ?udecl:UState.universe_decl (** Universe binders and constraints *) -> ?impargs:Impargs.manual_implicits -> poly:bool -> ?scope:DeclareDef.locality @@ -28,49 +86,58 @@ val add_definition -> RetrieveObl.obligation_info -> DeclareObl.progress -val add_mutual_definitions - (* XXX: unify with MutualEntry *) - : (Names.Id.t * constr * types * Impargs.manual_implicits * RetrieveObl.obligation_info) list +(* XXX: unify with MutualEntry *) + +(** Start a [Program Fixpoint] declaration, similar to the above, + except it takes a list now. *) +val add_mutual_definitions : + ( Names.Id.t + * constr + * types + * Impargs.manual_implicits + * RetrieveObl.obligation_info ) + list -> uctx:UState.t - -> ?udecl:UState.universe_decl - (** Universe binders and constraints *) + -> ?udecl:UState.universe_decl (** Universe binders and constraints *) -> ?tactic:unit Proofview.tactic -> poly:bool -> ?scope:DeclareDef.locality -> ?kind:Decls.definition_object_kind -> ?reduce:(constr -> constr) - -> ?hook:DeclareDef.Hook.t -> ?opaque:bool + -> ?hook:DeclareDef.Hook.t + -> ?opaque:bool -> Vernacexpr.decl_notation list - -> DeclareObl.fixpoint_kind -> unit + -> DeclareObl.fixpoint_kind + -> unit -val obligation - : int * Names.Id.t option * Constrexpr.constr_expr option +(** Implementation of the [Obligation] command *) +val obligation : + int * Names.Id.t option * Constrexpr.constr_expr option -> Genarg.glob_generic_argument option -> Lemmas.t -val next_obligation - : Names.Id.t option - -> Genarg.glob_generic_argument option - -> Lemmas.t +(** Implementation of the [Next Obligation] command *) +val next_obligation : + Names.Id.t option -> Genarg.glob_generic_argument option -> Lemmas.t -val solve_obligations : Names.Id.t option -> unit Proofview.tactic option - -> DeclareObl.progress -(* Number of remaining obligations to be solved for this program *) +(** Implementation of the [Solve Obligation] command *) +val solve_obligations : + Names.Id.t option -> unit Proofview.tactic option -> DeclareObl.progress val solve_all_obligations : unit Proofview.tactic option -> unit -val try_solve_obligation : int -> Names.Id.t option -> unit Proofview.tactic option -> unit +(** Number of remaining obligations to be solved for this program *) +val try_solve_obligation : + int -> Names.Id.t option -> unit Proofview.tactic option -> unit -val try_solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> unit +val try_solve_obligations : + Names.Id.t option -> unit Proofview.tactic option -> unit val show_obligations : ?msg:bool -> Names.Id.t option -> unit - val show_term : Names.Id.t option -> Pp.t - val admit_obligations : Names.Id.t option -> unit exception NoObligations of Names.Id.t option val explain_no_obligations : Names.Id.t option -> Pp.t - val check_program_libraries : unit -> unit -- cgit v1.2.3 From f836b601e3cb81dd24d25ccd910b2506aac998d9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 15 Mar 2020 17:08:16 -0400 Subject: [program] Use common type for fixpoint declarations. --- vernac/comProgramFixpoint.ml | 6 +++--- vernac/obligations.ml | 8 ++++---- vernac/obligations.mli | 7 +------ 3 files changed, 8 insertions(+), 13 deletions(-) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index f20b294499..56780d00a6 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -281,15 +281,15 @@ let do_program_recursive ~scope ~poly fixkind fixl = let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in (* Solve remaining evars *) let evd = nf_evar_map_undefined evd in - let collect_evars id def typ imps = + let collect_evars name def typ impargs = (* Generalize by the recursive prototypes *) let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = - RetrieveObl.retrieve_obligations env id evm + RetrieveObl.retrieve_obligations env name evm (List.length rec_sign) def typ in - (id, def, typ, imps, evars) + ({ DeclareDef.Recthm.name; typ; impargs; args = [] }, def, evars) in let (fixnames,fixrs,fixdefs,fixtypes) = fix in let fiximps = List.map pi2 info in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 0ffcea3867..435085793c 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -330,12 +330,12 @@ let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl) let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce) ?hook ?(opaque = false) notations fixkind = - let deps = List.map (fun (n, b, t, imps, obls) -> n) l in + let deps = List.map (fun ({ DeclareDef.Recthm.name; _ }, _, _) -> name) l in List.iter - (fun (n, b, t, impargs, obls) -> - let prg = ProgramDecl.make ~opaque n ~udecl (Some b) t ~uctx deps (Some fixkind) + (fun ({ DeclareDef.Recthm.name; typ; impargs; _ }, b, obls) -> + let prg = ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps (Some fixkind) notations obls ~impargs ~poly ~scope ~kind reduce ?hook - in progmap_add n (CEphemeron.create prg)) l; + in progmap_add name (CEphemeron.create prg)) l; let _defined = List.fold_left (fun finished x -> if finished then finished diff --git a/vernac/obligations.mli b/vernac/obligations.mli index cb54dfdeb2..f42d199e18 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -91,12 +91,7 @@ val add_definition : (** Start a [Program Fixpoint] declaration, similar to the above, except it takes a list now. *) val add_mutual_definitions : - ( Names.Id.t - * constr - * types - * Impargs.manual_implicits - * RetrieveObl.obligation_info ) - list + (DeclareDef.Recthm.t * Constr.t * RetrieveObl.obligation_info) list -> uctx:UState.t -> ?udecl:UState.universe_decl (** Universe binders and constraints *) -> ?tactic:unit Proofview.tactic -- cgit v1.2.3 From 9e3c7d4c0babf3b69c8646351ca7069704df345d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 17 Mar 2020 06:08:21 -0400 Subject: [lemmas] Minor tweak to Equations API. `wits` is actually not used, it is set in equations to the list of evars corresponding to the goals. --- vernac/lemmas.ml | 25 +++++++++++-------------- vernac/lemmas.mli | 12 ++++++------ 2 files changed, 17 insertions(+), 20 deletions(-) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 042fdd6885..ee4fc4334e 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -27,15 +27,12 @@ module Proof_ending = struct | Regular | End_obligation of DeclareObl.obligation_qed_info | End_derive of { f : Id.t; name : Id.t } - | End_equations of { hook : Constant.t list -> Evd.evar_map -> unit - ; i : Id.t - ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list - ; wits : EConstr.t list ref - (* wits are actually computed by the proof - engine by side-effect after creating the - proof! This is due to the start_dependent_proof API *) - ; sigma : Evd.evar_map - } + | End_equations of + { hook : Constant.t list -> Evd.evar_map -> unit + ; i : Id.t + ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list + ; sigma : Evd.evar_map + } end @@ -357,11 +354,11 @@ let finish_derived ~f ~name ~entries = let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in () -let finish_proved_equations kind proof_obj hook i types wits sigma0 = +let finish_proved_equations ~kind ~hook i proof_obj types sigma0 = let obls = ref 1 in let sigma, recobls = - CList.fold_left2_map (fun sigma (wit, (evar_env, ev, evi, local_context, type_)) entry -> + CList.fold_left2_map (fun sigma (_evar_env, ev, _evi, local_context, _type) entry -> let id = match Evd.evar_ident ev sigma0 with | Some id -> id @@ -372,7 +369,7 @@ let finish_proved_equations kind proof_obj hook i types wits sigma0 = let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in sigma, cst) sigma0 - (CList.combine (List.rev !wits) types) proof_obj.Proof_global.entries + types proof_obj.Proof_global.entries in hook recobls sigma @@ -386,8 +383,8 @@ let finalize_proof proof_obj proof_info = DeclareObl.obligation_terminator proof_obj.entries proof_obj.uctx oinfo | End_derive { f ; name } -> finish_derived ~f ~name ~entries:proof_obj.entries - | End_equations { hook; i; types; wits; sigma } -> - finish_proved_equations proof_info.Info.kind proof_obj hook i types wits sigma + | End_equations { hook; i; types; sigma } -> + finish_proved_equations ~kind:proof_info.Info.kind ~hook i proof_obj types sigma let err_save_forbidden_in_place_of_qed () = CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode") diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 0f0a37202a..8a23daa85f 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -35,12 +35,12 @@ module Proof_ending : sig | Regular | End_obligation of DeclareObl.obligation_qed_info | End_derive of { f : Id.t; name : Id.t } - | End_equations of { hook : Constant.t list -> Evd.evar_map -> unit - ; i : Id.t - ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list - ; wits : EConstr.t list ref - ; sigma : Evd.evar_map - } + | End_equations of + { hook : Constant.t list -> Evd.evar_map -> unit + ; i : Id.t + ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list + ; sigma : Evd.evar_map + } end -- cgit v1.2.3 From 7d46a32dc928af64e3e111d6d62caa00f93c427c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Mar 2020 05:35:41 -0400 Subject: [declare] Fuse prepare and declare for the non-interactive path. This will allow to share the definition metadata for example with obligations; a bit more work is needed to finally move the preparation of interactive proofs from Proof_global to `prepare_entry`. --- doc/plugin_tutorial/tuto1/src/simple_declare.ml | 5 ++- plugins/funind/gen_principle.ml | 5 ++- vernac/classes.ml | 5 ++- vernac/comAssumption.ml | 7 ++-- vernac/comDefinition.ml | 4 +-- vernac/declareDef.ml | 28 ++++++--------- vernac/declareDef.mli | 47 ++++++++++++++----------- vernac/declareObl.ml | 7 ++-- vernac/lemmas.ml | 3 +- 9 files changed, 55 insertions(+), 56 deletions(-) diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index a2783d80e8..8c4dc0e8a6 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,7 +1,6 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt = - let ce = DeclareDef.prepare_definition - ~opaque ~poly sigma ~udecl ~types:tyopt ~body in - DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ce + DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook + ~opaque ~poly ~udecl ~types:tyopt ~body sigma let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index ebd280ecf6..45c46c56f4 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -290,13 +290,12 @@ 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 - let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in - let _ : Names.GlobRef.t = DeclareDef.declare_definition + let _ : Names.GlobRef.t = DeclareDef.declare_entry ~name:new_princ_name ~hook ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:Decls.(IsProof Theorem) ~impargs:[] - entry in + ~uctx entry in () with e when CErrors.noncritical e -> raise (Defining_principle e) diff --git a/vernac/classes.ml b/vernac/classes.ml index 40c1a5d97d..6e929de581 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -313,10 +313,9 @@ let instance_hook info global ?hook cst = let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype = let kind = Decls.(IsDefinition Instance) in - let entry = DeclareDef.prepare_definition - ~poly sigma ~udecl ~types:(Some termtype) ~body:term in let scope = DeclareDef.Global Declare.ImportDefaultBehavior in - let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs entry in + let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs + ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in instance_hook info global ?hook kn let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name = diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 4a82696ea6..47ae03e0a3 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -205,9 +205,10 @@ let context_insection sigma ~poly ctx = let entry = Declare.definition_entry ~univs ~types:t b in (* XXX Fixme: Use DeclareDef.prepare_definition *) let uctx = Evd.evar_universe_context sigma in - let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in - let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge - ~kind:Decls.(IsDefinition Definition) ~impargs:[] entry + let kind = Decls.(IsDefinition Definition) in + let _ : GlobRef.t = + DeclareDef.declare_entry ~name ~scope:DeclareDef.Discharge + ~kind ~impargs:[] ~uctx entry in () in diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index bf4567e57f..3532d16315 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -74,10 +74,10 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let ce = DeclareDef.prepare_definition ~opaque:false ~poly evd ~udecl ~types ~body in let kind = Decls.IsDefinition kind in let _ : Names.GlobRef.t = - DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs ce + DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs + ~opaque:false ~poly evd ~udecl ~types ~body in () let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 14d3daf453..356e8f091e 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -37,19 +37,8 @@ module Hook = struct end -module ClosedDef = struct - - type t = - { entry : Evd.side_effects Declare.proof_entry - ; uctx : UState.t - } - - let of_proof_entry ~uctx entry = { entry; uctx } -end - (* Locality stuff *) -let declare_definition ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ce = - let { ClosedDef.entry; uctx } = ce in +let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry = let should_suggest = entry.Declare.proof_entry_opaque && Option.is_empty entry.Declare.proof_entry_secctx in let ubind = UState.universe_binders uctx in @@ -70,9 +59,9 @@ let declare_definition ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ce = Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook; dref -let declare_definition ~name ~scope ~kind ?hook ?obls ~impargs ce = - let fix_exn = Declare.Internal.get_fix_exn ce.ClosedDef.entry in - try declare_definition ~name ~scope ~kind ?hook ?obls ~impargs ce +let declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry = + let fix_exn = Declare.Internal.get_fix_exn entry in + try declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry with exn -> let exn = Exninfo.capture exn in Exninfo.iraise (fix_exn exn) @@ -120,7 +109,7 @@ let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~re let csts = CList.map2 (fun Recthm.{ name; typ; impargs } body -> let entry = Declare.definition_entry ~opaque ~types:typ ~univs body in - declare_definition ~name ~scope ~kind ~impargs { ClosedDef.entry; uctx }) + declare_entry ~name ~scope ~kind ~impargs ~uctx entry) fixitems fixdecls in let isfix = Option.is_empty possible_indexes in @@ -167,7 +156,12 @@ let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma let univs = Evd.check_univ_decl ~poly sigma udecl in let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in let uctx = Evd.evar_universe_context sigma in - { ClosedDef.entry; uctx } + entry, uctx + +let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook + ?obls ~poly ?inline ~types ~body ?fix_exn sigma = + let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in + declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma = let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 8f3db59ba9..3bc1e25f19 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -39,23 +39,39 @@ module Hook : sig val call : ?hook:t -> S.t -> unit end -module ClosedDef : sig - type t - - (* Don't use for non-interactive proofs *) - val of_proof_entry - : uctx:UState.t - -> Evd.side_effects Declare.proof_entry -> t -end +(** Declare an interactively-defined constant *) +val declare_entry + : name:Id.t + -> scope:locality + -> kind:Decls.logical_kind + -> ?hook:Hook.t + -> ?obls:(Id.t * Constr.t) list + -> impargs:Impargs.manual_implicits + -> uctx:UState.t + -> Evd.side_effects Declare.proof_entry + -> GlobRef.t +(** Declares a non-interactive constant; [body] and [types] will be + normalized w.r.t. the passed [evar_map] [sigma]. Universes should + be handled properly, including minimization and restriction. Note + that [sigma] is checked for unresolved evars, thus you should be + careful not to submit open terms or evar maps with stale, + unresolved existentials *) val declare_definition : name:Id.t -> scope:locality -> kind:Decls.logical_kind + -> opaque:bool + -> impargs:Impargs.manual_implicits + -> udecl:UState.universe_decl -> ?hook:Hook.t -> ?obls:(Id.t * Constr.t) list - -> impargs:Impargs.manual_implicits - -> ClosedDef.t + -> poly:bool + -> ?inline:bool + -> types:EConstr.t option + -> body:EConstr.t + -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) + -> Evd.evar_map -> GlobRef.t val declare_assumption @@ -97,17 +113,6 @@ val declare_mutually_recursive -> Recthm.t list -> Names.GlobRef.t list -val prepare_definition - : ?opaque:bool - -> ?inline:bool - -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) - -> poly:bool - -> udecl:UState.universe_decl - -> types:EConstr.t option - -> body:EConstr.t - -> Evd.evar_map - -> ClosedDef.t - val prepare_obligation : ?opaque:bool -> ?inline:bool diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 4c62582c23..bba3687256 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -371,9 +371,12 @@ let declare_definition prg = let fix_exn = Hook.get get_fix_exn () in let obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in (* XXX: This is doing normalization twice *) - let ce = DeclareDef.prepare_definition ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma in let () = progmap_remove prg in - DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls ce + let kn = + DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls + ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma + in + kn let rec lam_index n t acc = match Constr.kind t with diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index ee4fc4334e..feedf4d71d 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -238,8 +238,7 @@ end = struct Declare.Internal.map_entry_body pe ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in - let pe = DeclareDef.ClosedDef.of_proof_entry ~uctx pe in - DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs pe + DeclareDef.declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe let declare_mutdef ~info ~uctx const = let pe = match info.Info.compute_guard with -- cgit v1.2.3 From dfcc22eeb6e5404a42d28917a5540e1d894b5a71 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 23 Mar 2020 03:43:26 -0400 Subject: [ci] [overlays] Adapt to declare API changes. - problem with metacoq overlay ; it expects to send a non-ground constant to the kernel, now it fails at prepare. Record Sigma (A : Type) (B : A -> Type) : Type := { fst : A ; snd : B fst }. Arguments fst {A B}. Arguments snd {A B}. Quote Recursively Definition foo := (fst, snd). There is a hack on the overlay, we need to discuss it a bit more. --- ...oof+remove_special_case_first_declaration_in_mutual.sh | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh diff --git a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh new file mode 100644 index 0000000000..e3a8eb07f3 --- /dev/null +++ b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "11818" ] || [ "$CI_BRANCH" = "proof+remove_special_case_first_declaration_in_mutual" ]; then + + metacoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual + metacoq_CI_GITURL=https://github.com/ejgallego/metacoq + + elpi_CI_REF=proof+remove_special_case_first_declaration_in_mutual + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + + paramcoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + + equations_CI_REF=proof+remove_special_case_first_declaration_in_mutual + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi -- cgit v1.2.3 From b2b325a1d3c143f90a50a61cc9410efcd437d4b0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 30 Mar 2020 14:59:02 -0400 Subject: [typeclasses] Use label for `fail_evar` parameter. This makes code a bit more clear. --- pretyping/pretyping.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ded159e484..52122c09df 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -231,7 +231,7 @@ let frozen_and_pending_holes (sigma, sigma') = end in FrozenProgress data -let apply_typeclasses ~program_mode env sigma frozen fail_evar = +let apply_typeclasses ~program_mode ~fail_evar env sigma frozen = let filter_frozen = match frozen with | FrozenId map -> fun evk -> Evar.Map.mem evk map | FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen @@ -270,7 +270,7 @@ let apply_heuristics env sigma fail_evar = let check_typeclasses_instances_are_solved ~program_mode env current_sigma frozen = (* Naive way, call resolution again with failure flag *) - apply_typeclasses ~program_mode env current_sigma frozen true + apply_typeclasses ~program_mode ~fail_evar:true env current_sigma frozen let check_extra_evars_are_solved env current_sigma frozen = match frozen with | FrozenId _ -> () @@ -313,7 +313,7 @@ let solve_remaining_evars ?hook flags env ?initial sigma = let frozen = frozen_and_pending_holes (initial, sigma) in let sigma = if flags.use_typeclasses - then apply_typeclasses ~program_mode env sigma frozen false + then apply_typeclasses ~fail_evar:false ~program_mode env sigma frozen else sigma in let sigma = match hook with -- cgit v1.2.3 From 1320d5004b58f33c2274bfdc0629d7f513cd49c4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 30 Mar 2020 15:02:50 -0400 Subject: [declare] [nit] Get `fix_exn` only in the case of an exception. Suggested by Gaëtan Gilbert. --- vernac/declareDef.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 356e8f091e..1607771598 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -60,10 +60,10 @@ let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry = dref let declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry = - let fix_exn = Declare.Internal.get_fix_exn entry in try declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry with exn -> let exn = Exninfo.capture exn in + let fix_exn = Declare.Internal.get_fix_exn entry in Exninfo.iraise (fix_exn exn) let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes = -- cgit v1.2.3