From a2ea73d84be2fe95eeda42f5f5ac458f0af9968f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 24 Feb 2019 01:57:59 +0100 Subject: [proofs] Store hooks in the proof object. As of now, hooks were stored in the terminators as closures, we place them instead in the proof object and are thus passed back at proof closing time. This helps towards the reification and unification of terminators. --- plugins/derive/derive.ml | 4 +-- stm/stm.ml | 11 ++++---- vernac/lemmas.ml | 70 ++++++++++++++++++++++++++++-------------------- vernac/lemmas.mli | 27 ++++++++++++------- vernac/obligations.ml | 12 ++++----- vernac/vernacentries.mli | 2 +- vernac/vernacstate.ml | 6 ++--- vernac/vernacstate.mli | 2 +- 8 files changed, 77 insertions(+), 57 deletions(-) diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index aad3967f6d..f8b5f455d1 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -56,9 +56,9 @@ let start_deriving f suchthat name : Lemmas.t = let (opaque,f_def,lemma_def) = match com with | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") - | Lemmas.Proved (_,Some _,_) -> + | Lemmas.Proved (_,Some _,_, _) -> CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.") - | Lemmas.Proved (opaque, None, obj) -> + | Lemmas.Proved (opaque, None, obj,_) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> opaque <> Proof_global.Transparent , f_def , lemma_def diff --git a/stm/stm.ml b/stm/stm.ml index d77e37c910..a0247e0d8f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1532,14 +1532,15 @@ end = struct (* {{{ *) (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) State.unfreeze st; - let pobject, _ = + let pobject, _terminator, _hook = PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in + let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator []) in let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_vernac_interp stop - ~proof:(pobject, terminator) st + ~proof:(pobject, terminator, None) st { verbose = false; indentation = 0; strlen = 0; expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); @@ -1676,10 +1677,10 @@ end = struct (* {{{ *) let opaque = Proof_global.Opaque in (* The original terminator, a hook, has not been saved in the .vio*) - let pterm, _invalid_terminator = + let pterm, _invalid_terminator, _hook = PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in - let proof = pterm , Lemmas.standard_proof_terminator [] in + let proof = pterm , Lemmas.standard_proof_terminator [], None in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) @@ -1734,7 +1735,7 @@ end = struct (* {{{ *) | `ERROR -> exit 1 | `ERROR_ADMITTED -> cst, false | `OK_ADMITTED -> cst, false - | `OK (po,_) -> + | `OK (po,_,_) -> let con = Nametab.locate_constant (Libnames.qualid_of_ident po.Proof_global.id) in diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 7aba64fb93..695da1fcee 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -34,12 +34,12 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit -type declaration_hook = hook_type +type declaration_hook = hook_type CEphemeron.key -let mk_hook hook = hook +let mk_hook hook = CEphemeron.create hook let call_hook ?hook ?fix_exn uctx trans l c = - try Option.iter (fun hook -> hook uctx trans l c) hook + try Option.iter (fun hook -> CEphemeron.get hook uctx trans l c) hook with e when CErrors.noncritical e -> let e = CErrors.push e in let e = Option.cata (fun fix -> fix e) e fix_exn in @@ -49,10 +49,18 @@ let call_hook ?hook ?fix_exn uctx trans l c = [that can be saved] *) type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of Proof_global.opacity_flag * - lident option * - Proof_global.proof_object + | Admitted of + Names.Id.t * + Decl_kinds.goal_kind * + Entries.parameter_entry * + UState.t * + declaration_hook option + + | Proved of + Proof_global.opacity_flag * + lident option * + Proof_global.proof_object * + declaration_hook option type proof_terminator = (proof_ending -> unit) CEphemeron.key @@ -60,9 +68,10 @@ type proof_terminator = (proof_ending -> unit) CEphemeron.key type t = { proof : Proof_global.t ; terminator : proof_terminator + ; hook : declaration_hook option } -let pf_map f { proof; terminator} = { proof = f proof; terminator } +let pf_map f { proof; terminator; hook } = { proof = f proof; terminator; hook } let pf_fold f ps = f ps.proof let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t) @@ -76,12 +85,13 @@ let apply_terminator f = CEphemeron.get f (** Gets the current terminator without checking that the proof has been completed. Useful for the likes of [Admitted]. *) let get_terminator ps = ps.terminator +let get_hook ps = ps.hook end -let by tac { proof; terminator } = +let by tac { proof; terminator; hook } = let proof, res = Pfedit.by tac proof in - { proof; terminator}, res + { proof; terminator; hook}, res (* Support for mutually proved theorems *) @@ -316,13 +326,13 @@ let admit ?hook ctx (id,k,e) pl () = (* Starting a goal *) -let standard_proof_terminator ?(hook : declaration_hook option) compute_guard = +let standard_proof_terminator compute_guard = let open Proof_global in - CEphemeron.create begin function - | Admitted (id,k,pe,ctx) -> + Internal.make_terminator begin function + | Admitted (id,k,pe,ctx,hook) -> let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in Feedback.feedback Feedback.AddedAxiom - | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) -> + | Proved (opaque,idopt, { id; entries=[const]; persistence; universes }, hook ) -> let is_opaque, export_seff = match opaque with | Transparent -> false, true | Opaque -> true, false @@ -333,7 +343,7 @@ let standard_proof_terminator ?(hook : declaration_hook option) compute_guard = | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in let () = save ~export_seff id const universes compute_guard persistence hook universes in () - | Proved (opaque,idopt, _ ) -> + | Proved (opaque,idopt, _, hook) -> CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term") end @@ -381,8 +391,8 @@ end let start_lemma id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c = let terminator = match terminator with - | None -> standard_proof_terminator ?hook compute_guard - | Some terminator -> terminator ?hook compute_guard + | None -> standard_proof_terminator compute_guard + | Some terminator -> terminator compute_guard in let sign = match sign with @@ -391,15 +401,15 @@ let start_lemma id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c in let goals = [ Global.env_of_context sign , c ] in let proof = Proof_global.start_proof sigma id ?pl kind goals in - { proof ; terminator } + { proof ; terminator; hook } let start_dependent_lemma id ?pl kind ?terminator ?sign ?(compute_guard=[]) ?hook telescope = let terminator = match terminator with - | None -> standard_proof_terminator ?hook compute_guard - | Some terminator -> terminator ?hook compute_guard + | None -> standard_proof_terminator compute_guard + | Some terminator -> terminator compute_guard in let proof = Proof_global.start_dependent_proof id ?pl kind telescope in - { proof ; terminator } + { proof ; terminator; hook } let rec_tac_initializer finite guard thms snl = if finite then @@ -447,6 +457,7 @@ let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl = List.iter (fun (ref,imps) -> maybe_declare_manual_implicits false ref imps; call_hook ?hook ctx [] strength ref) thms_data in + let hook = mk_hook hook in let lemma = start_lemma id ~pl:decl kind sigma t ~hook ~compute_guard:guard in let lemma = pf_map (Proof_global.map_proof (fun p -> match init_tac with @@ -505,7 +516,7 @@ let save_lemma_admitted ?proof ~(lemma : t) = let pe = let open Proof_global in match proof with - | Some ({ id; entries; persistence = k; universes }, _) -> + | Some ({ id; entries; persistence = k; universes }, _, hook) -> if List.length entries <> 1 then user_err Pp.(str "Admitted does not support multiple statements"); let { const_entry_secctx; const_entry_type } = List.hd entries in @@ -514,7 +525,7 @@ let save_lemma_admitted ?proof ~(lemma : t) = let typ = Option.get const_entry_type in let ctx = UState.univ_entry ~poly:(pi2 k) universes in let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in - Admitted(id, k, (sec_vars, (typ, ctx), None), universes) + Admitted(id, k, (sec_vars, (typ, ctx), None), universes, hook) | None -> let pftree = Proof_global.get_proof lemma.proof in let gk = Proof_global.get_persistence lemma.proof in @@ -542,7 +553,7 @@ let save_lemma_admitted ?proof ~(lemma : t) = | _ -> None in let decl = Proof_global.get_universe_decl lemma.proof in let ctx = UState.check_univ_decl ~poly universes decl in - Admitted(name,gk,(sec_vars, (typ, ctx), None), universes) + Admitted(name,gk,(sec_vars, (typ, ctx), None), universes, lemma.hook) in CEphemeron.get lemma.terminator pe @@ -550,13 +561,14 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt = (* Invariant (uh) *) if Option.is_empty lemma && Option.is_empty proof then user_err (str "No focused proof (No proof-editing in progress)."); - let (proof_obj,terminator) = + let proof_obj,terminator, hook = match proof with | None -> (* XXX: The close_proof and proof state API should be refactored so it is possible to insert proofs properly into the state *) - let { proof; terminator } = Option.get lemma in - Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, terminator - | Some proof -> proof + let { proof; terminator; hook } = Option.get lemma in + Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, terminator, hook + | Some (proof, terminator, hook) -> + proof, terminator, hook in - CEphemeron.get terminator (Proved (opaque,idopt,proof_obj)) + CEphemeron.get terminator (Proved (opaque,idopt,proof_obj,hook)) diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 25c5b24e91..03cd45b8bf 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -65,8 +65,7 @@ module Stack : sig end val standard_proof_terminator - : ?hook:declaration_hook - -> Proof_global.lemma_possible_guards + : Proof_global.lemma_possible_guards -> proof_terminator val set_endline_tactic : Genarg.glob_generic_argument -> t -> t @@ -82,7 +81,7 @@ val start_lemma -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map - -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> proof_terminator) + -> ?terminator:(Proof_global.lemma_possible_guards -> proof_terminator) -> ?sign:Environ.named_context_val -> ?compute_guard:Proof_global.lemma_possible_guards -> ?hook:declaration_hook @@ -93,7 +92,7 @@ val start_dependent_lemma : Id.t -> ?pl:UState.universe_decl -> goal_kind - -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> proof_terminator) + -> ?terminator:(Proof_global.lemma_possible_guards -> proof_terminator) -> ?sign:Environ.named_context_val -> ?compute_guard:Proof_global.lemma_possible_guards -> ?hook:declaration_hook @@ -126,12 +125,12 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val (** {6 Saving proofs } *) val save_lemma_admitted - : ?proof:(Proof_global.proof_object * proof_terminator) + : ?proof:(Proof_global.proof_object * proof_terminator * declaration_hook option) -> lemma:t -> unit val save_lemma_proved - : ?proof:(Proof_global.proof_object * proof_terminator) + : ?proof:(Proof_global.proof_object * proof_terminator * declaration_hook option) -> ?lemma:t -> opaque:Proof_global.opacity_flag -> idopt:Names.lident option @@ -139,16 +138,24 @@ val save_lemma_proved (* API to build a terminator, should go away *) type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of Proof_global.opacity_flag * - Names.lident option * - Proof_global.proof_object + | Admitted of + Names.Id.t * + Decl_kinds.goal_kind * + Entries.parameter_entry * + UState.t * + declaration_hook option + | Proved of + Proof_global.opacity_flag * + lident option * + Proof_global.proof_object * + declaration_hook option (** This stuff is internal and will be removed in the future. *) module Internal : sig (** Only needed due to the Proof_global compatibility layer. *) val get_terminator : t -> proof_terminator + val get_hook : t -> declaration_hook option (** Only needed by obligations, should be reified soon *) val make_terminator : (proof_ending -> unit) -> proof_terminator diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 6ef2f80067..4a564e705e 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -839,13 +839,13 @@ let solve_by_tac ?loc name evi t poly ctx = warn_solve_errored ?loc err; None -let obligation_terminator ?hook name num guard auto pf = +let obligation_terminator name num guard auto pf = let open Proof_global in let open Lemmas in - let term = standard_proof_terminator ?hook guard in + let term = standard_proof_terminator guard in match pf with | Admitted _ -> Internal.apply_terminator term pf - | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin + | Proved (opq, id, { entries=[entry]; universes=uctx }, hook ) -> begin let env = Global.env () in let ty = entry.Entries.const_entry_type in let body, eff = Future.force entry.const_entry_body in @@ -905,7 +905,7 @@ let obligation_terminator ?hook name num guard auto pf = let e = CErrors.push e in pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) end - | Proved (_, _, _ ) -> + | Proved (_, _, _,_ ) -> CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term") let obligation_hook prg obl num auto ctx' _ _ gr = @@ -964,9 +964,9 @@ let rec solve_obligation prg num tac = let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n tac oblset = auto_solve_obligations n ~oblset tac in - let terminator ?hook guard = + let terminator guard = Lemmas.Internal.make_terminator - (obligation_terminator prg.prg_name num guard ?hook auto) in + (obligation_terminator prg.prg_name num guard auto) in let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in let lemma = fst @@ Lemmas.by !default_tactic lemma in diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index f1c8b29313..8d1d9abc0b 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -22,7 +22,7 @@ val vernac_require : (** The main interpretation function of vernacular expressions *) val interp : ?verbosely:bool -> - ?proof:(Proof_global.proof_object * Lemmas.proof_terminator) -> + ?proof:(Proof_global.proof_object * Lemmas.proof_terminator * Lemmas.declaration_hook option) -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t (** Prepare a "match" template for a given inductive type. diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index c51d3c30f4..0cdf748ce9 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -131,18 +131,18 @@ module Proof_global = struct s_lemmas := Some stack; res - type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator + type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator * Lemmas.declaration_hook option let return_proof ?allow_partial () = cc (return_proof ?allow_partial) let close_future_proof ~opaque ~feedback_id pf = cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt, - Internal.get_terminator pt) + Internal.get_terminator pt, Internal.get_hook pt) let close_proof ~opaque ~keep_body_ucst_separate f = cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate f)) pt, - Internal.get_terminator pt) + Internal.get_terminator pt, Internal.get_hook pt) let discard_all () = s_lemmas := None let update_global_env () = dd (update_global_env) diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 9f4e366e1c..15b8aaefb6 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -51,7 +51,7 @@ module Proof_global : sig val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output - type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator + type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator * Lemmas.declaration_hook option val close_future_proof : opaque:Proof_global.opacity_flag -> -- cgit v1.2.3 From a296e879112f2e88b2fdfbf2fe90f1807f90b890 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 24 Feb 2019 02:24:47 +0100 Subject: [proof] Unify obligation proof save path: Part I, declareObl We move obligation declaration-specific functions to their own file. This way, `Lemmas` can access them, and in the next part we can factorize common parts in the save proof. --- stm/stm.ml | 6 +- vernac/comProgramFixpoint.ml | 10 +- vernac/declareObl.ml | 556 +++++++++++++++++++++++++++++++++++++++++++ vernac/declareObl.mli | 110 +++++++++ vernac/lemmas.ml | 2 +- vernac/obligations.ml | 545 +++--------------------------------------- vernac/obligations.mli | 29 +-- vernac/vernac.mllib | 1 + 8 files changed, 717 insertions(+), 542 deletions(-) create mode 100644 vernac/declareObl.ml create mode 100644 vernac/declareObl.mli diff --git a/stm/stm.ml b/stm/stm.ml index a0247e0d8f..4f435f1fa5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -208,7 +208,7 @@ let mkTransCmd cast cids ceff cqueue = (* Parts of the system state that are morally part of the proof state *) let summary_pstate = Evarutil.meta_counter_summary_tag, Evd.evar_counter_summary_tag, - Obligations.program_tcc_summary_tag + DeclareObl.program_tcc_summary_tag type cached_state = | EmptyState @@ -884,7 +884,7 @@ end = struct (* {{{ *) Lemmas.Stack.t option * int * (* Evarutil.meta_counter_summary_tag *) int * (* Evd.evar_counter_summary_tag *) - Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) + DeclareObl.program_info CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) type partial_state = [ `Full of Vernacstate.t @@ -3238,7 +3238,7 @@ let unreachable_state_hook = Hooks.unreachable_state_hook let document_add_hook = Hooks.document_add_hook let document_edit_hook = Hooks.document_edit_hook let sentence_exec_hook = Hooks.sentence_exec_hook -let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref) +let () = Hook.set DeclareObl.stm_get_fix_exn (fun () -> !State.fix_exn_ref) type document = VCS.vcs let backup () = VCS.backup () diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 69e2a209eb..6296347fd0 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -248,7 +248,7 @@ let collect_evars_of_term evd c ty = evars (Evd.from_ctx (Evd.evar_universe_context evd)) let do_program_recursive local poly fixkind fixl ntns = - let cofix = fixkind = Obligations.IsCoFixpoint in + let cofix = fixkind = DeclareObl.IsCoFixpoint in let (env, rec_sign, pl, evd), fix, info = interp_recursive ~cofix ~program_mode:true fixl ntns in @@ -289,8 +289,8 @@ let do_program_recursive local poly fixkind fixl ntns = end in let ctx = Evd.evar_universe_context evd in let kind = match fixkind with - | Obligations.IsFixpoint _ -> (local, poly, Fixpoint) - | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint) + | DeclareObl.IsFixpoint _ -> (local, poly, Fixpoint) + | DeclareObl.IsCoFixpoint -> (local, poly, CoFixpoint) in Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind @@ -316,7 +316,7 @@ let do_program_fixpoint local poly l = | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> let fixl,ntns = extract_fixpoint_components ~structonly:true l in - let fixkind = Obligations.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in + let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in do_program_recursive local poly fixkind fixl ntns | _, _ -> @@ -341,5 +341,5 @@ let do_fixpoint local poly l = let do_cofixpoint local poly l = let fixl,ntns = extract_cofixpoint_components l in - do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns; + do_program_recursive local poly DeclareObl.IsCoFixpoint fixl ntns; if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml new file mode 100644 index 0000000000..564e83efd5 --- /dev/null +++ b/vernac/declareObl.ml @@ -0,0 +1,556 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* constr + ; prg_hook : Lemmas.declaration_hook option + ; prg_opaque : bool + ; prg_sign : named_context_val } + +(* Saving an obligation *) + +let get_shrink_obligations = + Goptions.declare_bool_option_and_ref ~depr:true (* remove in 8.8 *) + ~name:"Shrinking of Program obligations" ~key:["Shrink"; "Obligations"] + ~value:true + +(* XXX: Is this the right place for this? *) +let it_mkLambda_or_LetIn_or_clean t ctx = + let open Context.Rel.Declaration in + let fold t decl = + if is_local_assum decl then Term.mkLambda_or_LetIn decl t + else if noccurn 1 t then subst1 mkProp t + else Term.mkLambda_or_LetIn decl t + in + Context.Rel.fold_inside fold ctx ~init:t + +(* XXX: Is this the right place for this? *) +let decompose_lam_prod c ty = + let open Context.Rel.Declaration in + let rec aux ctx c ty = + match (Constr.kind c, Constr.kind ty) with + | LetIn (x, b, t, c), LetIn (x', b', t', ty) + when Constr.equal b b' && Constr.equal t t' -> + let ctx' = Context.Rel.add (LocalDef (x, b', t')) ctx in + aux ctx' c ty + | _, LetIn (x', b', t', ty) -> + let ctx' = Context.Rel.add (LocalDef (x', b', t')) ctx in + aux ctx' (lift 1 c) ty + | LetIn (x, b, t, c), _ -> + let ctx' = Context.Rel.add (LocalDef (x, b, t)) ctx in + aux ctx' c (lift 1 ty) + | Lambda (x, b, t), Prod (x', b', t') + (* By invariant, must be convertible *) -> + let ctx' = Context.Rel.add (LocalAssum (x, b')) ctx in + aux ctx' t t' + | Cast (c, _, _), _ -> aux ctx c ty + | _, _ -> (ctx, c, ty) + in + aux Context.Rel.empty c ty + +let shrink_body c ty = + let ctx, b, ty = + match ty with + | None -> + let ctx, b = Term.decompose_lam_assum c in + (ctx, b, None) + | Some ty -> + let ctx, b, ty = decompose_lam_prod c ty in + (ctx, b, Some ty) + in + let b', ty', n, args = + List.fold_left + (fun (b, ty, i, args) decl -> + if noccurn 1 b && Option.cata (noccurn 1) true ty then + (subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args) + else + let open Context.Rel.Declaration in + let args = if is_local_assum decl then mkRel i :: args else args in + ( Term.mkLambda_or_LetIn decl b + , Option.map (Term.mkProd_or_LetIn decl) ty + , succ i + , args ) ) + (b, ty, 1, []) ctx + in + (ctx, b', ty', Array.of_list args) + +let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] + +let add_hint local prg cst = + Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst) + +(***********************************************************************) +(* Saving an obligation *) +(***********************************************************************) + +(* true = hide obligations *) +let get_hide_obligations = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"Hidding of Program obligations" + ~key:["Hide"; "Obligations"] + ~value:false + +let declare_obligation prg obl body ty uctx = + let body = prg.prg_reduce body in + let ty = Option.map prg.prg_reduce ty in + match obl.obl_status with + | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)}) + | force, Evar_kinds.Define opaque -> + let opaque = (not force) && opaque in + let poly = pi2 prg.prg_kind in + let ctx, body, ty, args = + if get_shrink_obligations () && not poly then shrink_body body ty + else ([], body, ty, [||]) + in + let body = + ((body, Univ.ContextSet.empty), Evd.empty_side_effects) + in + let ce = + { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body + ; const_entry_secctx = None + ; const_entry_type = ty + ; const_entry_universes = uctx + ; const_entry_opaque = opaque + ; const_entry_inline_code = false + ; const_entry_feedback = None } + in + (* ppedrot: seems legit to have obligations as local *) + let constant = + Declare.declare_constant obl.obl_name ~local:ImportNeedQualified + (DefinitionEntry ce, IsProof Property) + in + if not opaque then + add_hint (Locality.make_section_locality None) prg constant; + Declare.definition_message obl.obl_name; + let body = + match uctx with + | Polymorphic_entry (_, uctx) -> + Some (DefinedObl (constant, Univ.UContext.instance uctx)) + | Monomorphic_entry _ -> + Some + (TermObl + (it_mkLambda_or_LetIn_or_clean + (mkApp (mkConst constant, args)) + ctx)) + in + (true, {obl with obl_body = body}) + +(* Updating the obligation meta-info on close *) + +let not_transp_msg = + Pp.( + str "Obligation should be transparent but was declared opaque." + ++ spc () + ++ str "Use 'Defined' instead.") + +let pperror cmd = CErrors.user_err ~hdr:"Program" cmd +let err_not_transp () = pperror not_transp_msg + +module ProgMap = Id.Map + +let from_prg, program_tcc_summary_tag = + Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" + +(* In all cases, the use of the map is read-only so we don't expose the ref *) +let get_prg_info_map () = !from_prg + +let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] + +let close sec = + if not (ProgMap.is_empty !from_prg) then + let keys = map_keys !from_prg in + CErrors.user_err ~hdr:"Program" + Pp.( + str "Unsolved obligations when closing " + ++ str sec ++ str ":" ++ spc () + ++ prlist_with_sep spc (fun x -> Id.print x) keys + ++ ( str (if Int.equal (List.length keys) 1 then " has " else " have ") + ++ str "unsolved obligations" )) + +let input : program_info CEphemeron.key ProgMap.t -> Libobject.obj = + let open Libobject in + declare_object + { (default_object "Program state") with + cache_function = (fun (na, pi) -> from_prg := pi) + ; load_function = (fun _ (_, pi) -> from_prg := pi) + ; discharge_function = + (fun _ -> + close "section"; + None ) + ; classify_function = + (fun _ -> + close "module"; + Dispose ) } + +let map_replace k v m = + ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) + +let progmap_remove prg = + Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg)) + +let progmap_add n prg = + Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg)) + +let progmap_replace prg' = + Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg)) + +let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0 + +let obligations_message rem = + if rem > 0 then + if Int.equal rem 1 then + Flags.if_verbose Feedback.msg_info + Pp.(int rem ++ str " obligation remaining") + else + Flags.if_verbose Feedback.msg_info + Pp.(int rem ++ str " obligations remaining") + else + Flags.if_verbose Feedback.msg_info Pp.(str "No more obligations remaining") + +type progress = Remain of int | Dependent | Defined of GlobRef.t + +let get_obligation_body expand obl = + match obl.obl_body with + | None -> None + | Some c -> ( + if expand && snd obl.obl_status == Evar_kinds.Expand then + match c with + | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc) + | TermObl c -> Some c + else + match c with DefinedObl pc -> Some (mkConstU pc) | TermObl c -> Some c ) + +let obl_substitution expand obls deps = + Int.Set.fold + (fun x acc -> + let xobl = obls.(x) in + match get_obligation_body expand xobl with + | None -> acc + | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc ) + deps [] + +let rec intset_to = function + | -1 -> Int.Set.empty + | n -> Int.Set.add n (intset_to (pred n)) + +let obligation_substitution expand prg = + let obls, _ = prg.prg_obligations in + let ints = intset_to (pred (Array.length obls)) in + obl_substitution expand obls ints + +let hide_obligation () = + Coqlib.check_required_library ["Coq"; "Program"; "Tactics"]; + UnivGen.constr_of_monomorphic_global + (Coqlib.lib_ref "program.tactics.obligation") + +(* XXX: Is this the right place? *) +let rec prod_app t n = + match + Constr.kind + (EConstr.Unsafe.to_constr + (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) + (* FIXME *) + with + | Prod (_, _, b) -> subst1 n b + | LetIn (_, b, t, b') -> prod_app (subst1 b b') n + | _ -> + CErrors.user_err ~hdr:"prod_app" + Pp.(str "Needed a product, but didn't find one" ++ fnl ()) + +(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) +let prod_applist t nL = List.fold_left prod_app t nL + +let replace_appvars subst = + let rec aux c = + let f, l = decompose_app c in + if isVar f then + try + let c' = List.map (Constr.map aux) l in + let t, b = Id.List.assoc (destVar f) subst in + mkApp + ( delayed_force hide_obligation + , [|prod_applist t c'; Term.applistc b c'|] ) + with Not_found -> Constr.map aux c + else Constr.map aux c + in + Constr.map aux + +let subst_prog subst prg = + if get_hide_obligations () then + ( replace_appvars subst prg.prg_body + , replace_appvars subst (* Termops.refresh_universes *) prg.prg_type ) + else + let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in + ( Vars.replace_vars subst' prg.prg_body + , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type ) + +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 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:(pi2 prg.prg_kind) uctx prg.prg_univdecl + in + let ce = Declare.definition_entry ~fix_exn ~opaque ~types:typ ~univs body in + let () = progmap_remove prg in + let ubinders = UState.universe_binders uctx in + let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in + DeclareDef.declare_definition prg.prg_name prg.prg_kind ce ubinders + prg.prg_implicits ?hook_data + +let rec lam_index n t acc = + match Constr.kind t with + | Lambda ({binder_name=Name n'}, _, _) when Id.equal n n' -> acc + | Lambda (_, _, b) -> lam_index n b (succ acc) + | _ -> raise Not_found + +let compute_possible_guardness_evidences n fixbody fixtype = + match n with + | Some {CAst.loc; v = n} -> [lam_index n fixbody 0] + | None -> + (* If recursive argument was not given by user, we try all args. + An earlier approach was to look only for inductive arguments, + but doing it properly involves delta-reduction, and it finally + doesn't seem to worth the effort (except for huge mutual + fixpoints ?) *) + let m = + Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) + (* FIXME *) + in + let ctx = fst (Term.decompose_prod_n_assum m fixtype) in + List.map_i (fun i _ -> i) 0 ctx + +let mk_proof c = + ((c, Univ.ContextSet.empty), Evd.empty_side_effects) + +let declare_mutual_definition l = + let len = List.length l in + let first = List.hd l in + let defobl x = + let oblsubst = obligation_substitution true x in + let subs, typ = subst_prog oblsubst x in + let env = Global.env () in + let sigma = Evd.from_ctx x.prg_ctx in + let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in + let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in + let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in + let term = EConstr.to_constr sigma term in + let typ = EConstr.to_constr sigma typ in + let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in + let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in + def, oblsubst + in + let defs, obls = + List.fold_right (fun x (defs, obls) -> + let xdef, xobls = defobl x in + (xdef :: defs, xobls @ obls)) l ([], []) + in + (* let fixdefs = List.map reduce_fix fixdefs in *) + let fixdefs, fixrs,fixtypes, fiximps = List.split4 defs in + let fixkind = Option.get first.prg_fixkind in + let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in + let rvec = Array.of_list fixrs in + let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in + let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in + let local, poly, kind = first.prg_kind in + let fixnames = first.prg_deps in + let opaque = first.prg_opaque in + let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in + let indexes, fixdecls = + match fixkind with + | IsFixpoint wfl -> + let possible_indexes = + List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes + in + let indexes = + Pretyping.search_guard (Global.env ()) possible_indexes fixdecls + in + ( Some indexes + , List.map_i (fun i _ -> mk_proof (mkFix ((indexes, i), fixdecls))) 0 l + ) + | IsCoFixpoint -> + (None, List.map_i (fun i _ -> mk_proof (mkCoFix (i, fixdecls))) 0 l) + in + (* Declare the recursive definitions *) + let univs = UState.univ_entry ~poly first.prg_ctx in + let fix_exn = Hook.get get_fix_exn () in + let kns = + List.map4 + (DeclareDef.declare_fix ~opaque (local, poly, kind) + UnivNames.empty_binders univs) + fixnames fixdecls fixtypes fiximps + in + (* Declare notations *) + List.iter + (Metasyntax.add_notation_interpretation (Global.env ())) + first.prg_notations; + Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; + let gr = List.hd kns in + Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr; + List.iter progmap_remove l; + gr + +let update_obls prg obls rem = + let prg' = {prg with prg_obligations = (obls, rem)} in + progmap_replace prg'; + obligations_message rem; + if rem > 0 then Remain rem + else + match prg'.prg_deps with + | [] -> + let kn = declare_definition prg' in + progmap_remove prg'; + Defined kn + | l -> + let progs = + List.map + (fun x -> CEphemeron.get (ProgMap.find x !from_prg)) + prg'.prg_deps + in + if List.for_all (fun x -> obligations_solved x) progs then + let kn = declare_mutual_definition progs in + Defined kn + else Dependent + +let dependencies obls n = + let res = ref Int.Set.empty in + Array.iteri + (fun i obl -> + if (not (Int.equal i n)) && Int.Set.mem n obl.obl_deps then + res := Int.Set.add i !res ) + obls; + !res + +let obligation_terminator name num guard auto pf = + let open Proof_global in + let open Lemmas in + let term = standard_proof_terminator guard in + match pf with + | Admitted _ -> Internal.apply_terminator term pf + | Proved (opq, id, { entries=[entry]; universes=uctx }, hook ) -> begin + let env = Global.env () in + let ty = entry.Entries.const_entry_type in + let body, eff = Future.force entry.const_entry_body in + let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in + let sigma = Evd.from_ctx uctx in + let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in + 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 ctx = Evd.evar_universe_context sigma in + let obls, rem = prg.prg_obligations in + let obl = obls.(num) in + let status = + match obl.obl_status, opq with + | (_, Evar_kinds.Expand), Opaque -> err_not_transp () + | (true, _), Opaque -> err_not_transp () + | (false, _), Opaque -> Evar_kinds.Define true + | (_, Evar_kinds.Define true), Transparent -> + Evar_kinds.Define false + | (_, status), Transparent -> status + in + let obl = { obl with obl_status = false, status } in + let ctx = + if pi2 prg.prg_kind then ctx + else UState.union prg.prg_ctx ctx + in + let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let (defined, obl) = declare_obligation prg obl body ty uctx in + let obls = Array.copy obls in + let () = obls.(num) <- obl in + let prg_ctx = + if pi2 (prg.prg_kind) then (* Polymorphic *) + (* We merge the new universes and constraints of the + polymorphic obligation with the existing ones *) + UState.union prg.prg_ctx ctx + 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 (Global.universes ()) + else ctx + in + let prg = { prg with prg_ctx } in + try + ignore (update_obls prg obls (pred rem)); + if pred rem > 0 then + begin + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then + ignore (auto (Some name) None deps) + end + with e when CErrors.noncritical e -> + let e = CErrors.push e in + pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) + end + | Proved (_, _, _,_ ) -> + CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term") diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli new file mode 100644 index 0000000000..3974954870 --- /dev/null +++ b/vernac/declareObl.mli @@ -0,0 +1,110 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* constr + ; prg_hook : Lemmas.declaration_hook option + ; prg_opaque : bool + ; prg_sign : Environ.named_context_val } + +val declare_obligation : + program_info + -> obligation + -> Constr.types + -> Constr.types option + -> Entries.universes_entry + -> bool * obligation +(** [declare_obligation] Save an obligation *) + +module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set + +val declare_definition : program_info -> Names.GlobRef.t + +val obligation_terminator : + ProgMap.key + -> int + -> Proof_global.lemma_possible_guards + -> (ProgMap.key option -> 'a option -> Int.Set.t -> 'b) + -> Lemmas.proof_ending + -> unit +(** [obligation_terminator] part 2 of saving an obligation *) + +type progress = + (* Resolution status of a program *) + | Remain of int + (* n obligations remaining *) + | Dependent + (* Dependent on other definitions *) + | Defined of GlobRef.t + (* Defined as id *) + +val update_obls : + program_info + -> obligation array + -> int + -> progress +(** [update_obls prg obls n progress] What does this do? *) + +(** { 2 Util } *) + +val get_prg_info_map : unit -> program_info CEphemeron.key ProgMap.t + +val program_tcc_summary_tag : + program_info CEphemeron.key Id.Map.t Summary.Dyn.tag + +val obl_substitution : + bool + -> obligation array + -> Int.Set.t + -> (ProgMap.key * (Constr.types * Constr.types)) list + +val dependencies : obligation array -> int -> Int.Set.t + +val err_not_transp : unit -> unit +val progmap_add : ProgMap.key -> program_info CEphemeron.key -> unit + +(* This is a hack to make it possible for Obligations to craft a Qed + * behind the scenes. The fix_exn the Stm attaches to the Future proof + * is not available here, so we provide a side channel to get it *) +val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 695da1fcee..d7e9e83649 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -243,7 +243,7 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes gr in definition_message id; - call_hook ?hook universes [] locality r + call_hook ~fix_exn ?hook universes [] locality r with e when CErrors.noncritical e -> let e = CErrors.push e in iraise (fix_exn e) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 4a564e705e..98dec7930c 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1,8 +1,16 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + | (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 @@ -186,7 +193,7 @@ let sort_dependencies evl = open Environ -let eterm_obligations env name evm fs ?status t ty = +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 @@ -253,10 +260,6 @@ let eterm_obligations env name evm fs ?status t ty = 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 hide_obligation () = - Coqlib.check_required_library ["Coq";"Program";"Tactics"]; - UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "program.tactics.obligation") - let pperror cmd = CErrors.user_err ~hdr:"Program" cmd let error s = pperror (str s) @@ -276,386 +279,27 @@ type obligation_info = (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array -type 'a obligation_body = - | DefinedObl of 'a - | TermObl of constr - -type obligation = - { obl_name : Id.t; - obl_type : types; - obl_location : Evar_kinds.t Loc.located; - obl_body : pconstant obligation_body option; - obl_status : bool * Evar_kinds.obligation_definition_status; - obl_deps : Int.Set.t; - obl_tac : unit Proofview.tactic option; - } - -type obligations = (obligation array * int) - -type fixpoint_kind = - | IsFixpoint of lident option list - | IsCoFixpoint - -type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list - -type program_info_aux = { - prg_name: Id.t; - prg_body: constr; - prg_type: constr; - prg_ctx: UState.t; - prg_univdecl: UState.universe_decl; - prg_obligations: obligations; - prg_deps : Id.t list; - prg_fixkind : fixpoint_kind option ; - prg_implicits : Impargs.manual_implicits; - prg_notations : notations ; - prg_kind : definition_kind; - prg_reduce : constr -> constr; - prg_hook : Lemmas.declaration_hook option; - prg_opaque : bool; - prg_sign: named_context_val; -} - -type program_info = program_info_aux CEphemeron.key - -let get_info x = - try CEphemeron.get x - with CEphemeron.InvalidKey -> - CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker.") - let assumption_message = Declare.assumption_message let default_tactic = ref (Proofview.tclUNIT ()) -(* true = hide obligations *) -let get_hide_obligations = - Goptions.declare_bool_option_and_ref - ~depr:false - ~name:"Hiding of Program obligations" - ~key:["Hide";"Obligations"] - ~value:false - - -let get_shrink_obligations = - Goptions.declare_bool_option_and_ref - ~depr:true (* remove in 8.8 *) - ~name:"Shrinking of Program obligations" - ~key:["Shrink";"Obligations"] - ~value:true - let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type) -let get_obligation_body expand obl = - match obl.obl_body with - | None -> None - | Some c -> - if expand && snd obl.obl_status == Evar_kinds.Expand then - match c with - | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc) - | TermObl c -> Some c - else (match c with - | DefinedObl pc -> Some (mkConstU pc) - | TermObl c -> Some c) - -let obl_substitution expand obls deps = - Int.Set.fold - (fun x acc -> - let xobl = obls.(x) in - match get_obligation_body expand xobl with - | None -> acc - | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc) - deps [] - let subst_deps expand obls deps t = let osubst = obl_substitution expand obls deps in (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t) -let rec prod_app t n = - match Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (* FIXME *) with - | Prod (_,_,b) -> subst1 n b - | LetIn (_, b, t, b') -> prod_app (subst1 b b') n - | _ -> - user_err ~hdr:"prod_app" - (str"Needed a product, but didn't find one" ++ fnl ()) - - -(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) -let prod_applist t nL = List.fold_left prod_app t nL - -let replace_appvars subst = - let rec aux c = - let f, l = decompose_app c in - if isVar f then - try - let c' = List.map (Constr.map aux) l in - let (t, b) = Id.List.assoc (destVar f) subst in - mkApp (delayed_force hide_obligation, - [| prod_applist t c'; applistc b c' |]) - with Not_found -> Constr.map aux c - else Constr.map aux c - in Constr.map aux - let subst_deps_obl obls obl = let t' = subst_deps true obls obl.obl_deps obl.obl_type in { obl with obl_type = t' } -module ProgMap = Id.Map - -let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m) - -let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m [] - -let from_prg, program_tcc_summary_tag = - Summary.ref_tag ProgMap.empty ~name:"program-tcc-table" - -let close sec = - if not (ProgMap.is_empty !from_prg) then - let keys = map_keys !from_prg in - user_err ~hdr:"Program" - (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++ - prlist_with_sep spc (fun x -> Id.print x) keys ++ - (str (if Int.equal (List.length keys) 1 then " has " else " have ") ++ - str "unsolved obligations")) - -let input : program_info ProgMap.t -> obj = - declare_object - { (default_object "Program state") with - cache_function = (fun (na, pi) -> from_prg := pi); - load_function = (fun _ (_, pi) -> from_prg := pi); - discharge_function = (fun _ -> close "section"; None); - classify_function = (fun _ -> close "module"; Dispose) } - open Evd -let progmap_remove prg = - Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg)) - -let progmap_add n prg = - Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg)) - -let progmap_replace prg' = - Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg)) - -let rec intset_to = function - -1 -> Int.Set.empty - | n -> Int.Set.add n (intset_to (pred n)) - -let subst_prog subst prg = - if get_hide_obligations () then - (replace_appvars subst prg.prg_body, - replace_appvars subst ((* Termops.refresh_universes *) prg.prg_type)) - else - let subst' = List.map (fun (n, (_, b)) -> n, b) subst in - (Vars.replace_vars subst' prg.prg_body, - Vars.replace_vars subst' ((* Termops.refresh_universes *) prg.prg_type)) - -let obligation_substitution expand prg = - let obls, _ = prg.prg_obligations in - let ints = intset_to (pred (Array.length obls)) in - obl_substitution expand obls ints - -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 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:(pi2 prg.prg_kind) uctx prg.prg_univdecl in - let ce = definition_entry ~fix_exn ~opaque ~types:typ ~univs body in - let () = progmap_remove prg in - let ubinders = UState.universe_binders uctx in - let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in - DeclareDef.declare_definition prg.prg_name - prg.prg_kind ce ubinders prg.prg_implicits ?hook_data - -let rec lam_index n t acc = - match Constr.kind t with - | Lambda ({binder_name=Name n'}, _, _) when Id.equal n n' -> - acc - | Lambda (_, _, b) -> - lam_index n b (succ acc) - | _ -> raise Not_found - -let compute_possible_guardness_evidences n fixbody fixtype = - match n with - | Some { CAst.loc; v = n } -> [lam_index n fixbody 0] - | None -> - (* If recursive argument was not given by user, we try all args. - An earlier approach was to look only for inductive arguments, - but doing it properly involves delta-reduction, and it finally - doesn't seem to worth the effort (except for huge mutual - fixpoints ?) *) - let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (* FIXME *) in - let ctx = fst (decompose_prod_n_assum m fixtype) in - List.map_i (fun i _ -> i) 0 ctx - -let mk_proof c = ((c, Univ.ContextSet.empty), Evd.empty_side_effects) - -let declare_mutual_definition l = - let len = List.length l in - let first = List.hd l in - let defobl x = - let oblsubst = obligation_substitution true x in - let subs, typ = subst_prog oblsubst x in - let env = Global.env () in - let sigma = Evd.from_ctx x.prg_ctx in - let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in - let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in - let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in - let term = EConstr.to_constr sigma term in - let typ = EConstr.to_constr sigma typ in - let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in - let oblsubst = List.map (fun (id, (_, c)) -> id, c) oblsubst in - def, oblsubst - in - let defs, obls = - List.fold_right (fun x (defs, obls) -> - let xdef, xobls = defobl x in - (xdef :: defs, xobls @ obls)) l ([], []) - in -(* let fixdefs = List.map reduce_fix fixdefs in *) - let fixdefs, fixrs, fixtypes, fiximps = List.split4 defs in - let fixkind = Option.get first.prg_fixkind in - let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in - let rvec = Array.of_list fixrs in - let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in - let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in - let (local,poly,kind) = first.prg_kind in - let fixnames = first.prg_deps in - let opaque = first.prg_opaque in - let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in - let indexes, fixdecls = - match fixkind with - | IsFixpoint wfl -> - let possible_indexes = - List.map3 compute_possible_guardness_evidences - wfl fixdefs fixtypes in - let indexes = - Pretyping.search_guard (Global.env()) - possible_indexes fixdecls in - Some indexes, - List.map_i (fun i _ -> - mk_proof (mkFix ((indexes,i),fixdecls))) 0 l - | IsCoFixpoint -> - None, - List.map_i (fun i _ -> - mk_proof (mkCoFix (i,fixdecls))) 0 l - in - (* Declare the recursive definitions *) - let univs = UState.univ_entry ~poly first.prg_ctx in - let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs) - fixnames fixdecls fixtypes fiximps in - (* Declare notations *) - List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; - Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; - let gr = List.hd kns in - Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr; - List.iter progmap_remove l; gr - -let decompose_lam_prod c ty = - let open Context.Rel.Declaration in - let rec aux ctx c ty = - match Constr.kind c, Constr.kind ty with - | LetIn (x, b, t, c), LetIn (x', b', t', ty) - when Constr.equal b b' && Constr.equal t t' -> - let ctx' = Context.Rel.add (LocalDef (x,b',t')) ctx in - aux ctx' c ty - | _, LetIn (x', b', t', ty) -> - let ctx' = Context.Rel.add (LocalDef (x',b',t')) ctx in - aux ctx' (lift 1 c) ty - | LetIn (x, b, t, c), _ -> - let ctx' = Context.Rel.add (LocalDef (x,b,t)) ctx in - aux ctx' c (lift 1 ty) - | Lambda (x, b, t), Prod (x', b', t') - (* By invariant, must be convertible *) -> - let ctx' = Context.Rel.add (LocalAssum (x,b')) ctx in - aux ctx' t t' - | Cast (c, _, _), _ -> aux ctx c ty - | _, _ -> ctx, c, ty - in aux Context.Rel.empty c ty - -let shrink_body c ty = - let ctx, b, ty = - match ty with - | None -> - let ctx, b = decompose_lam_assum c in - ctx, b, None - | Some ty -> - let ctx, b, ty = decompose_lam_prod c ty in - ctx, b, Some ty - in - let b', ty', n, args = - List.fold_left (fun (b, ty, i, args) decl -> - if noccurn 1 b && Option.cata (noccurn 1) true ty then - subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args - else - let open Context.Rel.Declaration in - let args = if is_local_assum decl then mkRel i :: args else args in - mkLambda_or_LetIn decl b, Option.map (mkProd_or_LetIn decl) ty, - succ i, args) - (b, ty, 1, []) ctx - in ctx, b', ty', Array.of_list args - let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] let add_hint local prg cst = Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst) -let it_mkLambda_or_LetIn_or_clean t ctx = - let open Context.Rel.Declaration in - let fold t decl = - if is_local_assum decl then mkLambda_or_LetIn decl t - else - if noccurn 1 t then subst1 mkProp t - else mkLambda_or_LetIn decl t - in - Context.Rel.fold_inside fold ctx ~init:t - -let declare_obligation prg obl body ty uctx = - let body = prg.prg_reduce body in - let ty = Option.map prg.prg_reduce ty in - match obl.obl_status with - | _, Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) } - | force, Evar_kinds.Define opaque -> - let opaque = not force && opaque in - let poly = pi2 prg.prg_kind in - let ctx, body, ty, args = - if get_shrink_obligations () && not poly then - shrink_body body ty else [], body, ty, [||] - in - let body = ((body,Univ.ContextSet.empty), Evd.empty_side_effects) in - let ce = - { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; - const_entry_secctx = None; - const_entry_type = ty; - const_entry_universes = uctx; - const_entry_opaque = opaque; - const_entry_inline_code = false; - const_entry_feedback = None; - } in - (* ppedrot: seems legit to have obligations as local *) - let constant = Declare.declare_constant obl.obl_name ~local:ImportNeedQualified - (DefinitionEntry ce,IsProof Property) - in - if not opaque then add_hint (Locality.make_section_locality None) prg constant; - definition_message obl.obl_name; - let body = match uctx with - | Polymorphic_entry (_, uctx) -> - Some (DefinedObl (constant, Univ.UContext.instance uctx)) - | Monomorphic_entry _ -> - Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) - in - true, { obl with obl_body = body } - let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind notations obls impls kind reduce = let obls', b = @@ -671,27 +315,27 @@ let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind | Some b -> Array.mapi (fun i (n, t, l, o, d, tac) -> - { obl_name = n ; obl_body = None; + { obl_name = n ; obl_body = None; obl_location = l; obl_type = t; obl_status = o; obl_deps = d; obl_tac = tac }) obls, b in let ctx = UState.make_flexible_nonalgebraic ctx in - { prg_name = n ; prg_body = b; prg_type = reduce t; + { prg_name = n ; prg_body = b; prg_type = reduce t; prg_ctx = ctx; prg_univdecl = udecl; prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; - prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; + prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; prg_hook = hook; prg_opaque = opaque; prg_sign = sign } let map_cardinal m = let i = ref 0 in ProgMap.iter (fun _ v -> - if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m; + if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m; !i -exception Found of program_info +exception Found of program_info CEphemeron.key let map_first m = try @@ -702,28 +346,28 @@ let map_first m = with Found x -> x let get_prog name = - let prg_infos = !from_prg in + let prg_infos = get_prg_info_map () in match name with Some n -> - (try get_info (ProgMap.find n prg_infos) + (try CEphemeron.get (ProgMap.find n prg_infos) with Not_found -> raise (NoObligations (Some n))) | None -> (let n = map_cardinal prg_infos in match n with 0 -> raise (NoObligations None) - | 1 -> get_info (map_first prg_infos) + | 1 -> CEphemeron.get (map_first prg_infos) | _ -> let progs = Id.Set.elements (ProgMap.domain prg_infos) in let prog = List.hd progs in let progs = prlist_with_sep pr_comma Id.print progs in - user_err + user_err (str "More than one program with unsolved obligations: " ++ progs ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print prog ++ str "\"")) let get_any_prog () = - let prg_infos = !from_prg in + let prg_infos = get_prg_info_map () in let n = map_cardinal prg_infos in - if n > 0 then get_info (map_first prg_infos) + if n > 0 then CEphemeron.get (map_first prg_infos) else raise (NoObligations None) let get_prog_err n = @@ -732,42 +376,8 @@ let get_prog_err n = let get_any_prog_err () = try get_any_prog () with NoObligations id -> pperror (explain_no_obligations id) -let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0 - let all_programs () = - ProgMap.fold (fun k p l -> p :: l) !from_prg [] - -type progress = - | Remain of int - | Dependent - | Defined of GlobRef.t - -let obligations_message rem = - if rem > 0 then - if Int.equal rem 1 then - Flags.if_verbose Feedback.msg_info (int rem ++ str " obligation remaining") - else - Flags.if_verbose Feedback.msg_info (int rem ++ str " obligations remaining") - else - Flags.if_verbose Feedback.msg_info (str "No more obligations remaining") - -let update_obls prg obls rem = - let prg' = { prg with prg_obligations = (obls, rem) } in - progmap_replace prg'; - obligations_message rem; - if rem > 0 then Remain rem - else ( - match prg'.prg_deps with - | [] -> - let kn = declare_definition prg' in - progmap_remove prg'; - Defined kn - | l -> - let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in - if List.for_all (fun x -> obligations_solved x) progs then - let kn = declare_mutual_definition progs in - Defined kn - else Dependent) + ProgMap.fold (fun k p l -> p :: l) (get_prg_info_map ()) [] let is_defined obls x = not (Option.is_empty obls.(x).obl_body) @@ -778,14 +388,6 @@ let deps_remaining obls deps = else x :: acc) deps [] -let dependencies obls n = - let res = ref Int.Set.empty in - Array.iteri - (fun i obl -> - if not (Int.equal i n) && Int.Set.mem n obl.obl_deps then - res := Int.Set.add i !res) - obls; - !res let goal_kind poly = Decl_kinds.(Global ImportNeedQualified, poly, DefinitionBody Definition) @@ -798,12 +400,6 @@ let kind_of_obligation poly o = | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly | _ -> goal_proof_kind poly -let not_transp_msg = - str "Obligation should be transparent but was declared opaque." ++ spc () ++ - str"Use 'Defined' instead." - -let err_not_transp () = pperror not_transp_msg - let rec string_of_list sep f = function [] -> "" | x :: [] -> f x @@ -839,81 +435,12 @@ let solve_by_tac ?loc name evi t poly ctx = warn_solve_errored ?loc err; None -let obligation_terminator name num guard auto pf = - let open Proof_global in - let open Lemmas in - let term = standard_proof_terminator guard in - match pf with - | Admitted _ -> Internal.apply_terminator term pf - | Proved (opq, id, { entries=[entry]; universes=uctx }, hook ) -> begin - let env = Global.env () in - let ty = entry.Entries.const_entry_type in - let body, eff = Future.force entry.const_entry_body in - let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in - let sigma = Evd.from_ctx uctx in - let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in - Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); - (* Declare the obligation ourselves and drop the hook *) - let prg = get_info (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 ctx = Evd.evar_universe_context sigma in - let obls, rem = prg.prg_obligations in - let obl = obls.(num) in - let status = - match obl.obl_status, opq with - | (_, Evar_kinds.Expand), Opaque -> err_not_transp () - | (true, _), Opaque -> err_not_transp () - | (false, _), Opaque -> Evar_kinds.Define true - | (_, Evar_kinds.Define true), Transparent -> - Evar_kinds.Define false - | (_, status), Transparent -> status - in - let obl = { obl with obl_status = false, status } in - let ctx = - if pi2 prg.prg_kind then ctx - else UState.union prg.prg_ctx ctx - in - let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in - let (defined, obl) = declare_obligation prg obl body ty uctx in - let obls = Array.copy obls in - let () = obls.(num) <- obl in - let prg_ctx = - if pi2 (prg.prg_kind) then (* Polymorphic *) - (* We merge the new universes and constraints of the - polymorphic obligation with the existing ones *) - UState.union prg.prg_ctx ctx - 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 (Global.universes ()) - else ctx - in - let prg = { prg with prg_ctx } in - try - ignore (update_obls prg obls (pred rem)); - if pred rem > 0 then - begin - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then - ignore (auto (Some name) None deps) - end - with e when CErrors.noncritical e -> - let e = CErrors.push e in - pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) - end - | Proved (_, _, _,_ ) -> - CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term") - let obligation_hook prg obl num auto ctx' _ _ gr = let obls, rem = prg.prg_obligations in let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in let transparent = evaluable_constant cst (Global.env ()) in let () = match obl.obl_status with - (true, Evar_kinds.Expand) + (true, Evar_kinds.Expand) | (true, Evar_kinds.Define true) -> if not transparent then err_not_transp () | _ -> () @@ -1049,7 +576,7 @@ and solve_obligations n tac = solve_prg_obligations prg tac and solve_all_obligations tac = - ProgMap.iter (fun k v -> ignore(solve_prg_obligations (get_info v) tac)) !from_prg + ProgMap.iter (fun k v -> ignore(solve_prg_obligations (CEphemeron.get v) tac)) (get_prg_info_map ()) and try_solve_obligation n prg tac = let prg = get_prog prg in @@ -1091,9 +618,9 @@ let show_obligations ?(msg=true) n = let progs = match n with | None -> all_programs () | Some n -> - try [ProgMap.find n !from_prg] + try [ProgMap.find n (get_prg_info_map ())] with Not_found -> raise (NoObligations (Some n)) - in List.iter (fun x -> show_obligations_of_prg ~msg (get_info x)) progs + in List.iter (fun x -> show_obligations_of_prg ~msg (CEphemeron.get x)) progs let show_term n = let prg = get_prog_err n in @@ -1113,8 +640,8 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose Feedback.msg_info (info ++ str "."); - let cst = declare_definition prg in - Defined cst) + let cst = DeclareObl.declare_definition prg in + Defined cst) else ( let len = Array.length obls in let () = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in @@ -1140,8 +667,8 @@ let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic else let res = auto_solve_obligations (Some x) tactic in match res with - | Defined _ -> - (* If one definition is turned into a constant, + | Defined _ -> + (* If one definition is turned into a constant, the whole block is defined. *) true | _ -> false) false deps @@ -1150,7 +677,7 @@ let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic let admit_prog prg = let obls, rem = prg.prg_obligations in let obls = Array.copy obls in - Array.iteri + Array.iteri (fun i x -> match x.obl_body with | None -> diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 18a7e10733..5e6339e9b9 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -13,11 +13,6 @@ open Constr open Evd open Names -(* This is a hack to make it possible for Obligations to craft a Qed - * behind the scenes. The fix_exn the Stm attaches to the Future proof - * is not available here, so we provide a side channel to get it *) -val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t - val check_evars : env -> evar_map -> unit val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t @@ -45,11 +40,6 @@ type obligation_info = (* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *) -type progress = (* Resolution status of a program *) - | Remain of int (* n obligations remaining *) - | Dependent (* Dependent on other definitions *) - | Defined of GlobRef.t (* Defined as id *) - val default_tactic : unit Proofview.tactic ref val add_definition @@ -64,14 +54,7 @@ val add_definition -> ?hook:Lemmas.declaration_hook -> ?opaque:bool -> obligation_info - -> progress - -type notations = - (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list - -type fixpoint_kind = - | IsFixpoint of lident option list - | IsCoFixpoint + -> DeclareObl.progress val add_mutual_definitions : (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list -> @@ -81,8 +64,8 @@ val add_mutual_definitions : ?kind:Decl_kinds.definition_kind -> ?reduce:(constr -> constr) -> ?hook:Lemmas.declaration_hook -> ?opaque:bool -> - notations -> - fixpoint_kind -> unit + DeclareObl.notations -> + DeclareObl.fixpoint_kind -> unit val obligation : int * Names.Id.t option * Constrexpr.constr_expr option @@ -94,7 +77,8 @@ val next_obligation -> Genarg.glob_generic_argument option -> Lemmas.t -val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress +val solve_obligations : Names.Id.t option -> unit Proofview.tactic option + -> DeclareObl.progress (* Number of remaining obligations to be solved for this program *) val solve_all_obligations : unit Proofview.tactic option -> unit @@ -114,6 +98,3 @@ exception NoObligations of Names.Id.t option val explain_no_obligations : Names.Id.t option -> Pp.t val check_program_libraries : unit -> unit - -type program_info -val program_tcc_summary_tag : program_info Id.Map.t Summary.Dyn.tag diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 57c56a58f9..f58af33f08 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -20,6 +20,7 @@ Auto_ind_decl Search Indschemes DeclareDef +DeclareObl Obligations ComDefinition Classes -- cgit v1.2.3 From 7dc04f0244aeb277b62070f87590cbc2cafd8396 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 24 Feb 2019 20:27:09 +0100 Subject: [proof] drop parameter from terminator type This makes the type of terminator simpler, progressing towards its total reification. --- plugins/derive/derive.ml | 6 ++-- proofs/proof_global.ml | 3 -- proofs/proof_global.mli | 2 -- stm/stm.ml | 13 ++++----- vernac/comFixpoint.mli | 3 +- vernac/declareObl.ml | 8 +++--- vernac/declareObl.mli | 3 +- vernac/lemmas.ml | 71 +++++++++++++++++++++++------------------------- vernac/lemmas.mli | 35 +++++++++++++----------- vernac/obligations.ml | 5 ++-- vernac/vernacentries.mli | 2 +- vernac/vernacstate.ml | 8 +++--- vernac/vernacstate.mli | 2 +- 13 files changed, 76 insertions(+), 85 deletions(-) diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index f8b5f455d1..0f0bec0129 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -56,9 +56,9 @@ let start_deriving f suchthat name : Lemmas.t = let (opaque,f_def,lemma_def) = match com with | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") - | Lemmas.Proved (_,Some _,_, _) -> + | Lemmas.Proved (_,Some _,_,_,_) -> CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.") - | Lemmas.Proved (opaque, None, obj,_) -> + | Lemmas.Proved (opaque, None, obj,_,_) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> opaque <> Proof_global.Transparent , f_def , lemma_def @@ -99,7 +99,7 @@ let start_deriving f suchthat name : Lemmas.t = ignore (Declare.declare_constant name lemma_def) in - let terminator ?hook _ = Lemmas.Internal.make_terminator terminator in + let terminator = Lemmas.Internal.make_terminator terminator in let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in Lemmas.pf_map (Proof_global.map_proof begin fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 96d90e9252..a871a3fc95 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -24,9 +24,6 @@ module NamedDecl = Context.Named.Declaration (*** Proof Global Environment ***) -(* Extra info on proofs. *) -type lemma_possible_guards = int list list - type proof_object = { id : Names.Id.t; entries : Evd.side_effects Entries.definition_entry list; diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index f84ec27df7..9c2ada2457 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -31,8 +31,6 @@ val compact_the_proof : t -> t function which takes a [proof_object] together with a [proof_end] (i.e. an proof ending command) and registers the appropriate values. *) -type lemma_possible_guards = int list list - type proof_object = { id : Names.Id.t; entries : Evd.side_effects Entries.definition_entry list; diff --git a/stm/stm.ml b/stm/stm.ml index 4f435f1fa5..13996aca0f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1532,15 +1532,12 @@ end = struct (* {{{ *) (* Unfortunately close_future_proof and friends are not pure so we need to set the state manually here *) State.unfreeze st; - let pobject, _terminator, _hook = + let pobject, _info = PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in - let terminator = (* The one sent by master is an InvalidKey *) - Lemmas.(standard_proof_terminator []) in - let st = Vernacstate.freeze_interp_state ~marshallable:false in stm_vernac_interp stop - ~proof:(pobject, terminator, None) st + ~proof:(pobject, Lemmas.default_info) st { verbose = false; indentation = 0; strlen = 0; expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in ignore(Future.join checked_proof); @@ -1677,10 +1674,10 @@ end = struct (* {{{ *) let opaque = Proof_global.Opaque in (* The original terminator, a hook, has not been saved in the .vio*) - let pterm, _invalid_terminator, _hook = + let pterm, _info = PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in - let proof = pterm , Lemmas.standard_proof_terminator [], None in + let proof = pterm, Lemmas.default_info in (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) @@ -1735,7 +1732,7 @@ end = struct (* {{{ *) | `ERROR -> exit 1 | `ERROR_ADMITTED -> cst, false | `OK_ADMITTED -> cst, false - | `OK (po,_,_) -> + | `OK (po,_) -> let con = Nametab.locate_constant (Libnames.qualid_of_ident po.Proof_global.id) in diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 1ded9f3d29..ea9ab33346 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -88,7 +88,8 @@ val declare_fixpoint : locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * (Constr.rel_context * Impargs.manual_implicits * int option) list -> - Proof_global.lemma_possible_guards -> decl_notation list -> unit + Lemmas.lemma_possible_guards -> decl_notation list -> + unit val declare_cofixpoint : locality -> polymorphic -> diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 564e83efd5..2afd056950 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -486,13 +486,13 @@ let dependencies obls n = obls; !res -let obligation_terminator name num guard auto pf = +let obligation_terminator name num auto pf = let open Proof_global in let open Lemmas in - let term = standard_proof_terminator guard in + let term = Lemmas.standard_proof_terminator in match pf with | Admitted _ -> Internal.apply_terminator term pf - | Proved (opq, id, { entries=[entry]; universes=uctx }, hook ) -> begin + | Proved (opq, id, { entries=[entry]; universes=uctx }, hook, compute_guard ) -> begin let env = Global.env () in let ty = entry.Entries.const_entry_type in let body, eff = Future.force entry.const_entry_body in @@ -552,5 +552,5 @@ let obligation_terminator name num guard auto pf = let e = CErrors.push e in pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) end - | Proved (_, _, _,_ ) -> + | Proved (_, _, _,_,_) -> CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term") diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index 3974954870..ab305da3af 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -62,9 +62,8 @@ module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set val declare_definition : program_info -> Names.GlobRef.t val obligation_terminator : - ProgMap.key + Id.t -> int - -> Proof_global.lemma_possible_guards -> (ProgMap.key option -> 'a option -> Int.Set.t -> 'b) -> Lemmas.proof_ending -> unit diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index d7e9e83649..0ca273a02d 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -48,6 +48,8 @@ let call_hook ?hook ?fix_exn uctx trans l c = (* Support for terminators and proofs with an associated constant [that can be saved] *) +type lemma_possible_guards = int list list + type proof_ending = | Admitted of Names.Id.t * @@ -60,7 +62,8 @@ type proof_ending = Proof_global.opacity_flag * lident option * Proof_global.proof_object * - declaration_hook option + declaration_hook option * + lemma_possible_guards type proof_terminator = (proof_ending -> unit) CEphemeron.key @@ -69,10 +72,11 @@ type t = { proof : Proof_global.t ; terminator : proof_terminator ; hook : declaration_hook option + ; compute_guard : lemma_possible_guards } -let pf_map f { proof; terminator; hook } = { proof = f proof; terminator; hook } -let pf_fold f ps = f ps.proof +let pf_map f pf = { pf with proof = f pf.proof } +let pf_fold f pf = f pf.proof let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t) @@ -84,14 +88,14 @@ let apply_terminator f = CEphemeron.get f (** Gets the current terminator without checking that the proof has been completed. Useful for the likes of [Admitted]. *) -let get_terminator ps = ps.terminator -let get_hook ps = ps.hook +let get_info ps = ps.terminator, ps.hook, ps.compute_guard end +(* Internal *) -let by tac { proof; terminator; hook } = - let proof, res = Pfedit.by tac proof in - { proof; terminator; hook}, res +let by tac pf = + let proof, res = Pfedit.by tac pf.proof in + { pf with proof }, res (* Support for mutually proved theorems *) @@ -326,13 +330,13 @@ let admit ?hook ctx (id,k,e) pl () = (* Starting a goal *) -let standard_proof_terminator compute_guard = +let standard_proof_terminator = let open Proof_global in Internal.make_terminator begin function | Admitted (id,k,pe,ctx,hook) -> let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in Feedback.feedback Feedback.AddedAxiom - | Proved (opaque,idopt, { id; entries=[const]; persistence; universes }, hook ) -> + | Proved (opaque,idopt, { id; entries=[const]; persistence; universes }, hook, compute_guard ) -> let is_opaque, export_seff = match opaque with | Transparent -> false, true | Opaque -> true, false @@ -343,7 +347,7 @@ let standard_proof_terminator compute_guard = | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in let () = save ~export_seff id const universes compute_guard persistence hook universes in () - | Proved (opaque,idopt, _, hook) -> + | Proved (opaque,idopt, _, hook,_) -> CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term") end @@ -382,34 +386,22 @@ module Stack = struct let (pn, pns) = map Proof.(function pf -> (data (prj pf.proof)).name) pf in pn :: pns - let copy_terminators ~src ~tgt = + let copy_info ~src ~tgt = let (ps, psl), (ts,tsl) = src, tgt in assert(List.length psl = List.length tsl); - {ts with terminator = ps.terminator}, List.map2 (fun op p -> { p with terminator = op.terminator }) psl tsl + { ps with proof = ts.proof }, + List.map2 (fun op p -> { op with proof = p.proof }) psl tsl end -let start_lemma id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c = - let terminator = match terminator with - | None -> standard_proof_terminator compute_guard - | Some terminator -> terminator compute_guard - in - let sign = - match sign with - | Some sign -> sign - | None -> initialize_named_context_for_proof () - in +let start_lemma id ?pl kind sigma ?(terminator=standard_proof_terminator) ?(sign=initialize_named_context_for_proof()) ?(compute_guard=[]) ?hook c = let goals = [ Global.env_of_context sign , c ] in let proof = Proof_global.start_proof sigma id ?pl kind goals in - { proof ; terminator; hook } + { proof ; terminator; hook; compute_guard } -let start_dependent_lemma id ?pl kind ?terminator ?sign ?(compute_guard=[]) ?hook telescope = - let terminator = match terminator with - | None -> standard_proof_terminator compute_guard - | Some terminator -> terminator compute_guard - in +let start_dependent_lemma id ?pl kind ?(terminator=standard_proof_terminator) ?sign ?(compute_guard=[]) ?hook telescope = let proof = Proof_global.start_dependent_proof id ?pl kind telescope in - { proof ; terminator; hook } + { proof; terminator; hook; compute_guard } let rec_tac_initializer finite guard thms snl = if finite then @@ -516,7 +508,7 @@ let save_lemma_admitted ?proof ~(lemma : t) = let pe = let open Proof_global in match proof with - | Some ({ id; entries; persistence = k; universes }, _, hook) -> + | Some ({ id; entries; persistence = k; universes }, (_, hook, _)) -> if List.length entries <> 1 then user_err Pp.(str "Admitted does not support multiple statements"); let { const_entry_secctx; const_entry_type } = List.hd entries in @@ -557,18 +549,23 @@ let save_lemma_admitted ?proof ~(lemma : t) = in CEphemeron.get lemma.terminator pe +type proof_info = proof_terminator * declaration_hook option * lemma_possible_guards + +let default_info = standard_proof_terminator, None, [] + let save_lemma_proved ?proof ?lemma ~opaque ~idopt = (* Invariant (uh) *) if Option.is_empty lemma && Option.is_empty proof then user_err (str "No focused proof (No proof-editing in progress)."); - let proof_obj,terminator, hook = + let proof_obj, proof_info = match proof with | None -> (* XXX: The close_proof and proof state API should be refactored so it is possible to insert proofs properly into the state *) - let { proof; terminator; hook } = Option.get lemma in - Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, terminator, hook - | Some (proof, terminator, hook) -> - proof, terminator, hook + let { proof; terminator; hook; compute_guard } = Option.get lemma in + Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, (terminator, hook, compute_guard) + | Some (proof, info) -> + proof, info in - CEphemeron.get terminator (Proved (opaque,idopt,proof_obj,hook)) + let terminator, hook, compute_guard = proof_info in + CEphemeron.get terminator (Proved (opaque,idopt,proof_obj,hook,compute_guard)) diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 03cd45b8bf..3efaac672a 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -41,6 +41,7 @@ val call_hook (* Proofs that define a constant + terminators *) type t type proof_terminator +type lemma_possible_guards = int list list module Stack : sig @@ -58,15 +59,13 @@ module Stack : sig val get_all_proof_names : t -> Names.Id.t list - val copy_terminators : src:t -> tgt:t -> t - (** Gets the current terminator without checking that the proof has - been completed. Useful for the likes of [Admitted]. *) + val copy_info : src:t -> tgt:t -> t + (** Gets the current info without checking that the proof has been + completed. Useful for the likes of [Admitted]. *) end -val standard_proof_terminator - : Proof_global.lemma_possible_guards - -> proof_terminator +val standard_proof_terminator : proof_terminator val set_endline_tactic : Genarg.glob_generic_argument -> t -> t val pf_map : (Proof_global.t -> Proof_global.t) -> t -> t @@ -81,9 +80,9 @@ val start_lemma -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map - -> ?terminator:(Proof_global.lemma_possible_guards -> proof_terminator) + -> ?terminator:proof_terminator -> ?sign:Environ.named_context_val - -> ?compute_guard:Proof_global.lemma_possible_guards + -> ?compute_guard:lemma_possible_guards -> ?hook:declaration_hook -> EConstr.types -> t @@ -92,9 +91,9 @@ val start_dependent_lemma : Id.t -> ?pl:UState.universe_decl -> goal_kind - -> ?terminator:(Proof_global.lemma_possible_guards -> proof_terminator) + -> ?terminator:proof_terminator -> ?sign:Environ.named_context_val - -> ?compute_guard:Proof_global.lemma_possible_guards + -> ?compute_guard:lemma_possible_guards -> ?hook:declaration_hook -> Proofview.telescope -> t @@ -108,7 +107,7 @@ val start_lemma_com val start_lemma_with_initialization : ?hook:declaration_hook -> goal_kind -> Evd.evar_map -> UState.universe_decl - -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option + -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> (Id.t (* name of thm *) * (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_implicits))) list @@ -124,13 +123,17 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val (** {6 Saving proofs } *) +type proof_info + +val default_info : proof_info + val save_lemma_admitted - : ?proof:(Proof_global.proof_object * proof_terminator * declaration_hook option) + : ?proof:(Proof_global.proof_object * proof_info) -> lemma:t -> unit val save_lemma_proved - : ?proof:(Proof_global.proof_object * proof_terminator * declaration_hook option) + : ?proof:(Proof_global.proof_object * proof_info) -> ?lemma:t -> opaque:Proof_global.opacity_flag -> idopt:Names.lident option @@ -148,14 +151,14 @@ type proof_ending = Proof_global.opacity_flag * lident option * Proof_global.proof_object * - declaration_hook option + declaration_hook option * + lemma_possible_guards (** This stuff is internal and will be removed in the future. *) module Internal : sig (** Only needed due to the Proof_global compatibility layer. *) - val get_terminator : t -> proof_terminator - val get_hook : t -> declaration_hook option + val get_info : t -> proof_info (** Only needed by obligations, should be reified soon *) val make_terminator : (proof_ending -> unit) -> proof_terminator diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 98dec7930c..b6f2c47f98 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -491,9 +491,8 @@ let rec solve_obligation prg num tac = let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n tac oblset = auto_solve_obligations n ~oblset tac in - let terminator guard = - Lemmas.Internal.make_terminator - (obligation_terminator prg.prg_name num guard auto) in + let terminator = Lemmas.Internal.make_terminator + (obligation_terminator prg.prg_name num auto) in let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in let lemma = fst @@ Lemmas.by !default_tactic lemma in diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 8d1d9abc0b..2895d0e4df 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -22,7 +22,7 @@ val vernac_require : (** The main interpretation function of vernacular expressions *) val interp : ?verbosely:bool -> - ?proof:(Proof_global.proof_object * Lemmas.proof_terminator * Lemmas.declaration_hook option) -> + ?proof:(Proof_global.proof_object * Lemmas.proof_info) -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t (** Prepare a "match" template for a given inductive type. diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 0cdf748ce9..c387c5c5f1 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -131,18 +131,18 @@ module Proof_global = struct s_lemmas := Some stack; res - type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator * Lemmas.declaration_hook option + type closed_proof = Proof_global.proof_object * Lemmas.proof_info let return_proof ?allow_partial () = cc (return_proof ?allow_partial) let close_future_proof ~opaque ~feedback_id pf = cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt, - Internal.get_terminator pt, Internal.get_hook pt) + Internal.get_info pt) let close_proof ~opaque ~keep_body_ucst_separate f = cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate f)) pt, - Internal.get_terminator pt, Internal.get_hook pt) + Internal.get_info pt) let discard_all () = s_lemmas := None let update_global_env () = dd (update_global_env) @@ -158,6 +158,6 @@ module Proof_global = struct | None, None -> None | Some _ , None -> None | None, Some x -> Some x - | Some src, Some tgt -> Some (Stack.copy_terminators ~src ~tgt) + | Some src, Some tgt -> Some (Stack.copy_info ~src ~tgt) end diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index 15b8aaefb6..b78b252579 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -51,7 +51,7 @@ module Proof_global : sig val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output - type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator * Lemmas.declaration_hook option + type closed_proof = Proof_global.proof_object * Lemmas.proof_info val close_future_proof : opaque:Proof_global.opacity_flag -> -- cgit v1.2.3 From 873281c256fc33941d93044acc3db8eda0a148ee Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 24 Feb 2019 20:38:21 +0100 Subject: [proof] Move declaration hooks to DeclareDef. This way both `Lemmas` and `DeclareObl` can depend on it, removing one more difficulty on the unification of terminators. --- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/indfun_common.ml | 2 +- plugins/funind/indfun_common.mli | 2 +- plugins/funind/recdef.ml | 4 +-- plugins/ltac/rewrite.ml | 2 +- vernac/class.ml | 4 +-- vernac/class.mli | 4 +-- vernac/classes.ml | 4 +-- vernac/comDefinition.mli | 2 +- vernac/comProgramFixpoint.ml | 2 +- vernac/declareDef.ml | 25 ++++++++++++++++- vernac/declareDef.mli | 32 ++++++++++++++++++++-- vernac/declareObl.ml | 4 +-- vernac/declareObl.mli | 2 +- vernac/lemmas.ml | 28 ++++++------------- vernac/lemmas.mli | 39 +++++---------------------- vernac/obligations.ml | 2 +- vernac/obligations.mli | 4 +-- vernac/vernac.mllib | 8 +++--- vernac/vernacentries.ml | 2 +- 20 files changed, 93 insertions(+), 81 deletions(-) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 8af5dc818b..08acb754f7 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -307,7 +307,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin in let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in evd := sigma; - let hook = Lemmas.mk_hook (hook new_principle_type) in + let hook = DeclareDef.Hook.make (hook new_principle_type) in let lemma = Lemmas.start_lemma new_princ_name diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7683ce1757..732a0d818f 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -137,7 +137,7 @@ let save id const ?hook uctx (locality,_,kind) = let kn = declare_constant id ~local (DefinitionEntry const, k) in ConstRef kn in - Lemmas.call_hook ?hook ~fix_exn uctx [] locality r; + DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r; definition_message id let with_full_print f a = diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 4078c34331..8dd990775b 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -45,7 +45,7 @@ val jmeq_refl : unit -> EConstr.constr val save : Id.t -> Evd.side_effects Entries.definition_entry - -> ?hook:Lemmas.declaration_hook + -> ?hook:DeclareDef.Hook.t -> UState.t -> Decl_kinds.goal_kind -> unit diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2b5c0a01db..8169ff459f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1371,7 +1371,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type let lemma = Lemmas.start_lemma na Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) - sigma gls_type ~hook:(Lemmas.mk_hook hook) in + sigma gls_type ~hook:(DeclareDef.Hook.make hook) in let lemma = if Indfun_common.is_strict_tcc () then fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma @@ -1592,5 +1592,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type term_id using_lemmas (List.length res_vars) - evd (Lemmas.mk_hook hook)) + evd (DeclareDef.Hook.make hook)) () diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2da6584aba..2bab55ef74 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2006,7 +2006,7 @@ let add_morphism_interactive atts m n : Lemmas.t = declare_projection n instance_id (ConstRef cst) | _ -> assert false in - let hook = Lemmas.mk_hook hook in + let hook = DeclareDef.Hook.make hook in Flags.silently (fun () -> let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in diff --git a/vernac/class.ml b/vernac/class.ml index 58cef5db4f..eed7107b39 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -366,7 +366,7 @@ let add_coercion_hook poly _uctx _trans local ref = let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg -let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly) +let add_coercion_hook poly = DeclareDef.Hook.make (add_coercion_hook poly) let add_subclass_hook poly _uctx _trans local ref = let stre = match local with @@ -377,4 +377,4 @@ let add_subclass_hook poly _uctx _trans local ref = let cl = class_of_global ref in try_add_new_coercion_subclass cl ~local:stre poly -let add_subclass_hook poly = Lemmas.mk_hook (add_subclass_hook poly) +let add_subclass_hook poly = DeclareDef.Hook.make (add_subclass_hook poly) diff --git a/vernac/class.mli b/vernac/class.mli index 80d6d4383c..85266739ad 100644 --- a/vernac/class.mli +++ b/vernac/class.mli @@ -42,8 +42,8 @@ val try_add_new_coercion_with_source : GlobRef.t -> local:bool -> val try_add_new_identity_coercion : Id.t -> local:bool -> Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit -val add_coercion_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook +val add_coercion_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t -val add_subclass_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook +val add_subclass_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t val class_of_global : GlobRef.t -> cl_typ diff --git a/vernac/classes.ml b/vernac/classes.ml index bd5a211f1d..74903d196f 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -364,7 +364,7 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt in obls, Some constr, typ | None -> [||], None, termtype in - let hook = Lemmas.mk_hook hook in + let hook = DeclareDef.Hook.make hook in let ctx = Evd.evar_universe_context sigma in ignore(Obligations.add_definition id ?term:constr ~univdecl:decl typ ctx ~kind:(Global ImportDefaultBehavior,poly,Instance) ~hook obls) @@ -379,7 +379,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te let sigma = Evd.reset_future_goals sigma in let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in let lemma = Lemmas.start_lemma id ~pl:decl kind sigma (EConstr.of_constr termtype) - ~hook:(Lemmas.mk_hook + ~hook:(DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook)) in (* spiwack: I don't know what to do with the status here. *) let lemma = diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 0d9df47ee8..cf309d6bbd 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -18,7 +18,7 @@ open Constrexpr val do_definition : program_mode:bool - -> ?hook:Lemmas.declaration_hook + -> ?hook:DeclareDef.Hook.t -> Id.t -> definition_kind -> universe_decl_expr option diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 6296347fd0..3bb9b0f6a1 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -229,7 +229,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = in hook, recname, typ in (* XXX: Capturing sigma here... bad bad *) - let hook = Lemmas.mk_hook (hook sigma) in + let hook = DeclareDef.Hook.make (hook sigma) in Obligations.check_evars env sigma; let evars, _, evars_def, evars_typ = Obligations.eterm_obligations env recname sigma 0 def typ diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 652dbf0858..f80884c124 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -14,6 +14,29 @@ open Entries open Globnames open Impargs +(* Hooks naturally belong here as they apply to both definitions and lemmas *) +module Hook = struct + module S = struct + type t = UState.t + -> (Names.Id.t * Constr.t) list + -> Decl_kinds.locality + -> Names.GlobRef.t + -> unit + end + + type t = S.t CEphemeron.key + + let make hook = CEphemeron.create hook + + let call ?hook ?fix_exn uctx trans l c = + try Option.iter (fun hook -> CEphemeron.get hook uctx trans l c) hook + with e when CErrors.noncritical e -> + let e = CErrors.push e in + let e = Option.cata (fun fix -> fix e) e fix_exn in + Util.iraise e +end + +(* Locality stuff *) let declare_definition ident (local, p, k) ?hook_data ce pl imps = let fix_exn = Future.fix_exn_of ce.const_entry_body in let gr = match local with @@ -32,7 +55,7 @@ let declare_definition ident (local, p, k) ?hook_data ce pl imps = match hook_data with | None -> () | Some (hook, uctx, extra_defs) -> - Lemmas.call_hook ~fix_exn ~hook uctx extra_defs local gr + Hook.call ~fix_exn ~hook uctx extra_defs local gr end; gr diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 909aa41a30..5b656a2f5a 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -11,10 +11,38 @@ open Names open Decl_kinds +(** Declaration hooks *) +module Hook : sig + type t + + (** Hooks allow users of the API to perform arbitrary actions at + proof/definition saving time. For example, to register a constant + as a Coercion, perform some cleanup, update the search database, + etc... *) + module S : sig + (** [S.t] passes to the client: *) + type t + = UState.t + (** [ustate]: universe constraints obtained when the term was closed *) + -> (Id.t * Constr.t) list + (** [(n1,t1),...(nm,tm)]: association list between obligation + name and the corresponding defined term (might be a constant, + but also an arbitrary term in the Expand case of obligations) *) + -> Decl_kinds.locality + (** [locality]: Locality of the original declaration *) + -> GlobRef.t + (** [ref]: identifier of the origianl declaration *) + -> unit + end + + val make : S.t -> t + val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t +end + val declare_definition : Id.t -> definition_kind - -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list) + -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> Evd.side_effects Entries.definition_entry -> UnivNames.universe_binders -> Impargs.manual_implicits @@ -22,7 +50,7 @@ val declare_definition val declare_fix : ?opaque:bool - -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list) + -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) -> definition_kind -> UnivNames.universe_binders -> Entries.universes_entry diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 2afd056950..b269f69ece 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -50,7 +50,7 @@ type program_info = ; prg_notations : notations ; prg_kind : definition_kind ; prg_reduce : constr -> constr - ; prg_hook : Lemmas.declaration_hook option + ; prg_hook : DeclareDef.Hook.t option ; prg_opaque : bool ; prg_sign : named_context_val } @@ -451,7 +451,7 @@ let declare_mutual_definition l = first.prg_notations; Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in - Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr; + DeclareDef.Hook.call ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr; List.iter progmap_remove l; gr diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index ab305da3af..5d02639245 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -44,7 +44,7 @@ type program_info = ; prg_notations : notations ; prg_kind : Decl_kinds.definition_kind ; prg_reduce : constr -> constr - ; prg_hook : Lemmas.declaration_hook option + ; prg_hook : DeclareDef.Hook.t option ; prg_opaque : bool ; prg_sign : Environ.named_context_val } diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 0ca273a02d..98c7c0d077 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -33,18 +33,6 @@ open Impargs module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit -type declaration_hook = hook_type CEphemeron.key - -let mk_hook hook = CEphemeron.create hook - -let call_hook ?hook ?fix_exn uctx trans l c = - try Option.iter (fun hook -> CEphemeron.get hook uctx trans l c) hook - with e when CErrors.noncritical e -> - let e = CErrors.push e in - let e = Option.cata (fun fix -> fix e) e fix_exn in - iraise e - (* Support for terminators and proofs with an associated constant [that can be saved] *) @@ -56,13 +44,13 @@ type proof_ending = Decl_kinds.goal_kind * Entries.parameter_entry * UState.t * - declaration_hook option + DeclareDef.Hook.t option | Proved of Proof_global.opacity_flag * lident option * Proof_global.proof_object * - declaration_hook option * + DeclareDef.Hook.t option * lemma_possible_guards type proof_terminator = (proof_ending -> unit) CEphemeron.key @@ -71,7 +59,7 @@ type proof_terminator = (proof_ending -> unit) CEphemeron.key type t = { proof : Proof_global.t ; terminator : proof_terminator - ; hook : declaration_hook option + ; hook : DeclareDef.Hook.t option ; compute_guard : lemma_possible_guards } @@ -247,7 +235,7 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes gr in definition_message id; - call_hook ~fix_exn ?hook universes [] locality r + DeclareDef.Hook.call ~fix_exn ?hook universes [] locality r with e when CErrors.noncritical e -> let e = CErrors.push e in iraise (fix_exn e) @@ -326,7 +314,7 @@ let admit ?hook ctx (id,k,e) pl () = let kn = declare_constant id ~local (ParameterEntry e, IsAssumption Conjectural) in let () = assumption_message id in Declare.declare_univ_binders (ConstRef kn) pl; - call_hook ?hook ctx [] (Global local) (ConstRef kn) + DeclareDef.Hook.call ?hook ctx [] (Global local) (ConstRef kn) (* Starting a goal *) @@ -448,8 +436,8 @@ let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl = let thms_data = (ref,imps)::other_thms_data in List.iter (fun (ref,imps) -> maybe_declare_manual_implicits false ref imps; - call_hook ?hook ctx [] strength ref) thms_data in - let hook = mk_hook hook in + DeclareDef.Hook.call ?hook ctx [] strength ref) thms_data in + let hook = DeclareDef.Hook.make hook in let lemma = start_lemma id ~pl:decl kind sigma t ~hook ~compute_guard:guard in let lemma = pf_map (Proof_global.map_proof (fun p -> match init_tac with @@ -549,7 +537,7 @@ let save_lemma_admitted ?proof ~(lemma : t) = in CEphemeron.get lemma.terminator pe -type proof_info = proof_terminator * declaration_hook option * lemma_possible_guards +type proof_info = proof_terminator * DeclareDef.Hook.t option * lemma_possible_guards let default_info = standard_proof_terminator, None, [] diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 3efaac672a..961c1e41ef 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -11,33 +11,6 @@ open Names open Decl_kinds -(* Declaration hooks *) -type declaration_hook - -(* Hooks allow users of the API to perform arbitrary actions at - * proof/definition saving time. For example, to register a constant - * as a Coercion, perform some cleanup, update the search database, - * etc... - * - * Here, we use an extended hook type suitable for obligations / - * equations. - *) -(** [hook_type] passes to the client: - - [ustate]: universe constraints obtained when the term was closed - - [(n1,t1),...(nm,tm)]: association list between obligation - name and the corresponding defined term (might be a constant, - but also an arbitrary term in the Expand case of obligations) - - [locality]: Locality of the original declaration - - [ref]: identifier of the origianl declaration - *) -type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit - -val mk_hook : hook_type -> declaration_hook -val call_hook - : ?hook:declaration_hook - -> ?fix_exn:Future.fix_exn - -> hook_type - (* Proofs that define a constant + terminators *) type t type proof_terminator @@ -83,7 +56,7 @@ val start_lemma -> ?terminator:proof_terminator -> ?sign:Environ.named_context_val -> ?compute_guard:lemma_possible_guards - -> ?hook:declaration_hook + -> ?hook:DeclareDef.Hook.t -> EConstr.types -> t @@ -94,18 +67,18 @@ val start_dependent_lemma -> ?terminator:proof_terminator -> ?sign:Environ.named_context_val -> ?compute_guard:lemma_possible_guards - -> ?hook:declaration_hook + -> ?hook:DeclareDef.Hook.t -> Proofview.telescope -> t val start_lemma_com : program_mode:bool -> ?inference_hook:Pretyping.inference_hook - -> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list + -> ?hook:DeclareDef.Hook.t -> goal_kind -> Vernacexpr.proof_expr list -> t val start_lemma_with_initialization - : ?hook:declaration_hook + : ?hook:DeclareDef.Hook.t -> goal_kind -> Evd.evar_map -> UState.universe_decl -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> (Id.t (* name of thm *) * @@ -146,12 +119,12 @@ type proof_ending = Decl_kinds.goal_kind * Entries.parameter_entry * UState.t * - declaration_hook option + DeclareDef.Hook.t option | Proved of Proof_global.opacity_flag * lident option * Proof_global.proof_object * - declaration_hook option * + DeclareDef.Hook.t option * lemma_possible_guards (** This stuff is internal and will be removed in the future. *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index b6f2c47f98..9a34bda423 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -493,7 +493,7 @@ let rec solve_obligation prg num tac = let auto n tac oblset = auto_solve_obligations n ~oblset tac in let terminator = Lemmas.Internal.make_terminator (obligation_terminator prg.prg_name num auto) in - let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in + let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in let lemma = fst @@ Lemmas.by !default_tactic lemma in let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 5e6339e9b9..87da73c534 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -51,7 +51,7 @@ val add_definition -> ?kind:Decl_kinds.definition_kind -> ?tactic:unit Proofview.tactic -> ?reduce:(constr -> constr) - -> ?hook:Lemmas.declaration_hook + -> ?hook:DeclareDef.Hook.t -> ?opaque:bool -> obligation_info -> DeclareObl.progress @@ -63,7 +63,7 @@ val add_mutual_definitions : ?tactic:unit Proofview.tactic -> ?kind:Decl_kinds.definition_kind -> ?reduce:(constr -> constr) -> - ?hook:Lemmas.declaration_hook -> ?opaque:bool -> + ?hook:DeclareDef.Hook.t -> ?opaque:bool -> DeclareObl.notations -> DeclareObl.fixpoint_kind -> unit diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index f58af33f08..0749314301 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -11,16 +11,16 @@ Egramml Vernacextend Ppvernac Proof_using +Egramcoq +Metasyntax +DeclareDef Lemmas +DeclareObl Canonical Class -Egramcoq -Metasyntax Auto_ind_decl Search Indschemes -DeclareDef -DeclareObl Obligations ComDefinition Classes diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 112c4b6451..bf57866d95 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -588,7 +588,7 @@ let vernac_definition_hook p = function | Coercion -> Some (Class.add_coercion_hook p) | CanonicalStructure -> - Some (Lemmas.mk_hook (fun _ _ _ -> Canonical.declare_canonical_structure)) + Some (DeclareDef.Hook.make (fun _ _ _ -> Canonical.declare_canonical_structure)) | SubClass -> Some (Class.add_subclass_hook p) | _ -> None -- cgit v1.2.3 From 9b97d4368aa714aa5f0ae0a91bec7bab7eb1a394 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 24 Feb 2019 20:40:34 +0100 Subject: [proof] Remove terminator type, unifying regular and obligation ones. We radically redesign how proof closing information is stored. Instead of a user-defined closure, we now reify control into a single data structure containing the needed information. In this scheme, the `Lemmas` module can get extra information with obligation info when opening the proof, and will correspondingly call the right closing function based on this. This is the start of what could be a much bigger unification of all the proof save paths. --- plugins/derive/derive.ml | 78 +++------------------- vernac/declareObl.ml | 37 ++++++----- vernac/declareObl.mli | 21 +++--- vernac/lemmas.ml | 165 +++++++++++++++++++++++++++++------------------ vernac/lemmas.mli | 42 ++++-------- vernac/obligations.ml | 9 ++- vernac/vernac.mllib | 2 +- 7 files changed, 165 insertions(+), 189 deletions(-) diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 0f0bec0129..0447b79dcd 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -8,16 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Constr open Context open Context.Named.Declaration -let map_const_entry_body (f:constr->constr) (x: Evd.side_effects Entries.const_entry_body) - : Evd.side_effects Entries.const_entry_body = - Future.chain x begin fun ((b,ctx),fx) -> - (f b , ctx) , fx - end - (** [start_deriving f suchthat lemma] starts a proof of [suchthat] (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] @@ -36,71 +29,18 @@ let start_deriving f suchthat name : Lemmas.t = (* create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *) let goals = let open Proofview in - TCons ( env , sigma , f_type_type , (fun sigma f_type -> + TCons ( env , sigma , f_type_type , (fun sigma f_type -> TCons ( env , sigma , f_type , (fun sigma ef -> - let f_type = EConstr.Unsafe.to_constr f_type in - let ef = EConstr.Unsafe.to_constr ef in - let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in - let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in - TCons ( env' , sigma , suchthat , (fun sigma _ -> - TNil sigma)))))) - in - - (* The terminator handles the registering of constants when the proof is closed. *) - let terminator com = - (* Extracts the relevant information from the proof. [Admitted] - and [Save] result in user errors. [opaque] is [true] if the - proof was concluded by [Qed], and [false] if [Defined]. [f_def] - and [lemma_def] correspond to the proof of [f] and of - [suchthat], respectively. *) - let (opaque,f_def,lemma_def) = - match com with - | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") - | Lemmas.Proved (_,Some _,_,_,_) -> - CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.") - | Lemmas.Proved (opaque, None, obj,_,_) -> - match Proof_global.(obj.entries) with - | [_;f_def;lemma_def] -> - opaque <> Proof_global.Transparent , f_def , lemma_def - | _ -> assert false - in - (* The opacity of [f_def] is adjusted to be [false], as it - must. Then [f] is declared in the global environment. *) - let f_def = { f_def with Entries.const_entry_opaque = false } in - let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in - let f_kn = Declare.declare_constant f f_def in - let f_kn_term = mkConst f_kn in - (* In the type and body of the proof of [suchthat] there can be - references to the variable [f]. It needs to be replaced by - references to the constant [f] declared above. This substitution - performs this precise action. *) - let substf c = Vars.replace_vars [f,f_kn_term] c in - (* Extracts the type of the proof of [suchthat]. *) - let lemma_pretype = - match Entries.(lemma_def.const_entry_type) with - | Some t -> t - | None -> assert false (* Proof_global always sets type here. *) - in - (* The references of [f] are subsituted appropriately. *) - let lemma_type = substf lemma_pretype in - (* The same is done in the body of the proof. *) - let lemma_body = - map_const_entry_body substf Entries.(lemma_def.const_entry_body) - in - let lemma_def = let open Entries in { lemma_def with - const_entry_body = lemma_body ; - const_entry_type = Some lemma_type ; - const_entry_opaque = opaque ; } - in - let lemma_def = - Entries.DefinitionEntry lemma_def , - Decl_kinds.(IsProof Proposition) - in - ignore (Declare.declare_constant name lemma_def) + let f_type = EConstr.Unsafe.to_constr f_type in + let ef = EConstr.Unsafe.to_constr ef in + let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in + let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in + TCons ( env' , sigma , suchthat , (fun sigma _ -> + TNil sigma)))))) in - let terminator = Lemmas.Internal.make_terminator terminator in - let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in + let proof_ending = Lemmas.Proof_ending.(End_derive {f; name}) in + let lemma = Lemmas.start_dependent_lemma name kind goals ~proof_ending in Lemmas.pf_map (Proof_global.map_proof begin fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p end) lemma diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index b269f69ece..71215d2a3e 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -486,13 +486,16 @@ let dependencies obls n = obls; !res -let obligation_terminator name num auto pf = +type obligation_qed_info = + { name : Id.t + ; num : int + ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress + } + +let obligation_terminator opq entries uctx { name; num; auto } = let open Proof_global in - let open Lemmas in - let term = Lemmas.standard_proof_terminator in - match pf with - | Admitted _ -> Internal.apply_terminator term pf - | Proved (opq, id, { entries=[entry]; universes=uctx }, hook, compute_guard ) -> begin + match entries with + | [entry] -> let env = Global.env () in let ty = entry.Entries.const_entry_type in let body, eff = Future.force entry.const_entry_body in @@ -539,18 +542,20 @@ let obligation_terminator name num auto pf = if defined then UState.make (Global.universes ()) else ctx in - let prg = { prg with prg_ctx } in - try + let prg = {prg with prg_ctx} in + begin try ignore (update_obls prg obls (pred rem)); if pred rem > 0 then - begin - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then - ignore (auto (Some name) None deps) - end + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then + ignore (auto (Some name) deps None) with e when CErrors.noncritical e -> let e = CErrors.push e in pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) - end - | Proved (_, _, _,_,_) -> - CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term") + end + | _ -> + CErrors.anomaly + Pp.( + str + "[obligation_terminator] close_proof returned more than one proof \ + term") diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli index 5d02639245..70a4601ac6 100644 --- a/vernac/declareObl.mli +++ b/vernac/declareObl.mli @@ -61,14 +61,6 @@ module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set val declare_definition : program_info -> Names.GlobRef.t -val obligation_terminator : - Id.t - -> int - -> (ProgMap.key option -> 'a option -> Int.Set.t -> 'b) - -> Lemmas.proof_ending - -> unit -(** [obligation_terminator] part 2 of saving an obligation *) - type progress = (* Resolution status of a program *) | Remain of int @@ -78,6 +70,19 @@ type progress = | Defined of GlobRef.t (* Defined as id *) +type obligation_qed_info = + { name : Id.t + ; num : int + ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress + } + +val obligation_terminator + : Proof_global.opacity_flag + -> Evd.side_effects Entries.definition_entry list + -> UState.t + -> obligation_qed_info -> unit +(** [obligation_terminator] part 2 of saving an obligation *) + val update_obls : program_info -> obligation array diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 98c7c0d077..686f52565c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -38,29 +38,22 @@ module NamedDecl = Context.Named.Declaration type lemma_possible_guards = int list list -type proof_ending = - | Admitted of - Names.Id.t * - Decl_kinds.goal_kind * - Entries.parameter_entry * - UState.t * - DeclareDef.Hook.t option - - | Proved of - Proof_global.opacity_flag * - lident option * - Proof_global.proof_object * - DeclareDef.Hook.t option * - lemma_possible_guards - -type proof_terminator = (proof_ending -> unit) CEphemeron.key +module Proof_ending = struct + + type t = + | Regular + | End_obligation of DeclareObl.obligation_qed_info + | End_derive of { f : Id.t; name : Id.t } + +end (* Proofs with a save constant function *) type t = { proof : Proof_global.t - ; terminator : proof_terminator ; hook : DeclareDef.Hook.t option ; compute_guard : lemma_possible_guards + ; proof_ending : Proof_ending.t CEphemeron.key + (* This could be improved and the CEphemeron removed *) } let pf_map f pf = { pf with proof = f pf.proof } @@ -71,12 +64,9 @@ let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t) (* To be removed *) module Internal = struct -let make_terminator f = CEphemeron.create f -let apply_terminator f = CEphemeron.get f - (** Gets the current terminator without checking that the proof has been completed. Useful for the likes of [Admitted]. *) -let get_info ps = ps.terminator, ps.hook, ps.compute_guard +let get_info ps = ps.hook, ps.compute_guard, ps.proof_ending end (* Internal *) @@ -209,7 +199,6 @@ let look_for_possibly_mutual_statements sigma = function | [] -> anomaly (Pp.str "Empty list of theorems.") (* Saving a goal *) - let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes = let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in try @@ -316,15 +305,14 @@ let admit ?hook ctx (id,k,e) pl () = Declare.declare_univ_binders (ConstRef kn) pl; DeclareDef.Hook.call ?hook ctx [] (Global local) (ConstRef kn) -(* Starting a goal *) +let finish_admitted id k pe ctx hook = + let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in + Feedback.feedback Feedback.AddedAxiom -let standard_proof_terminator = +let finish_proved opaque idopt po hook compute_guard = let open Proof_global in - Internal.make_terminator begin function - | Admitted (id,k,pe,ctx,hook) -> - let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in - Feedback.feedback Feedback.AddedAxiom - | Proved (opaque,idopt, { id; entries=[const]; persistence; universes }, hook, compute_guard ) -> + match po with + | { id; entries=[const]; persistence; universes } -> let is_opaque, export_seff = match opaque with | Transparent -> false, true | Opaque -> true, false @@ -335,9 +323,8 @@ let standard_proof_terminator = | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in let () = save ~export_seff id const universes compute_guard persistence hook universes in () - | Proved (opaque,idopt, _, hook,_) -> - CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term") - end + | _ -> + CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term") let initialize_named_context_for_proof () = let sign = Global.named_context () in @@ -382,14 +369,17 @@ module Stack = struct end -let start_lemma id ?pl kind sigma ?(terminator=standard_proof_terminator) ?(sign=initialize_named_context_for_proof()) ?(compute_guard=[]) ?hook c = +(* Starting a goal *) +let start_lemma id ?pl kind sigma ?(proof_ending = Proof_ending.Regular) + ?(sign=initialize_named_context_for_proof()) ?(compute_guard=[]) ?hook c = let goals = [ Global.env_of_context sign , c ] in let proof = Proof_global.start_proof sigma id ?pl kind goals in - { proof ; terminator; hook; compute_guard } + { proof ; hook; compute_guard; proof_ending = CEphemeron.create proof_ending } -let start_dependent_lemma id ?pl kind ?(terminator=standard_proof_terminator) ?sign ?(compute_guard=[]) ?hook telescope = +let start_dependent_lemma id ?pl kind ?(proof_ending = Proof_ending.Regular) + ?(compute_guard=[]) ?hook telescope = let proof = Proof_global.start_dependent_proof id ?pl kind telescope in - { proof; terminator; hook; compute_guard } + { proof; hook; compute_guard; proof_ending = CEphemeron.create proof_ending } let rec_tac_initializer finite guard thms snl = if finite then @@ -480,23 +470,17 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind thms = start_lemma_with_initialization ?hook kind evd decl recguard thms snl (* Saving a proof *) - -let keep_admitted_vars = ref true - -let () = - let open Goptions in - declare_bool_option - { optdepr = false; - optname = "keep section variables in admitted proofs"; - optkey = ["Keep"; "Admitted"; "Variables"]; - optread = (fun () -> !keep_admitted_vars); - optwrite = (fun b -> keep_admitted_vars := b) } +let get_keep_admitted_vars = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"keep section variables in admitted proofs" + ~key:["Keep"; "Admitted"; "Variables"] + ~value:true let save_lemma_admitted ?proof ~(lemma : t) = - let pe = let open Proof_global in match proof with - | Some ({ id; entries; persistence = k; universes }, (_, hook, _)) -> + | Some ({ id; entries; persistence = k; universes }, (hook, _, _)) -> if List.length entries <> 1 then user_err Pp.(str "Admitted does not support multiple statements"); let { const_entry_secctx; const_entry_type } = List.hd entries in @@ -504,8 +488,8 @@ let save_lemma_admitted ?proof ~(lemma : t) = user_err Pp.(str "Admitted requires an explicit statement"); let typ = Option.get const_entry_type in let ctx = UState.univ_entry ~poly:(pi2 k) universes in - let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in - Admitted(id, k, (sec_vars, (typ, ctx), None), universes, hook) + let sec_vars = if get_keep_admitted_vars () then const_entry_secctx else None in + finish_admitted id k (sec_vars, (typ, ctx), None) universes hook | None -> let pftree = Proof_global.get_proof lemma.proof in let gk = Proof_global.get_persistence lemma.proof in @@ -522,7 +506,7 @@ let save_lemma_admitted ?proof ~(lemma : t) = let pproofs, _univs = Proof_global.return_proof ~allow_partial:true lemma.proof in let sec_vars = - if not !keep_admitted_vars then None + if not (get_keep_admitted_vars ()) then None else match Proof_global.get_used_variables lemma.proof, pproofs with | Some _ as x, _ -> x | None, (pproof, _) :: _ -> @@ -533,13 +517,64 @@ let save_lemma_admitted ?proof ~(lemma : t) = | _ -> None in let decl = Proof_global.get_universe_decl lemma.proof in let ctx = UState.check_univ_decl ~poly universes decl in - Admitted(name,gk,(sec_vars, (typ, ctx), None), universes, lemma.hook) - in - CEphemeron.get lemma.terminator pe + finish_admitted name gk (sec_vars, (typ, ctx), None) universes lemma.hook + +(************************************************************************) +(* Saving a lemma-like constant *) +(************************************************************************) + +type proof_info = DeclareDef.Hook.t option * lemma_possible_guards * Proof_ending.t CEphemeron.key -type proof_info = proof_terminator * DeclareDef.Hook.t option * lemma_possible_guards +let default_info = None, [], CEphemeron.create Proof_ending.Regular -let default_info = standard_proof_terminator, None, [] +let finish_derive ~f ~name ~idopt ~opaque ~entries = + (* Extracts the relevant information from the proof. [Admitted] and + [Save] result in user errors. [opaque] is [true] if the proof was + concluded by [Qed], and [false] if [Defined]. [f_def] and + [lemma_def] 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 opaque, f_def, lemma_def = + match entries with + | [_;f_def;lemma_def] -> + opaque <> Proof_global.Transparent , f_def , lemma_def + | _ -> assert false + in + (* The opacity of [f_def] is adjusted to be [false], as it + must. Then [f] is declared in the global environment. *) + let f_def = { f_def with Entries.const_entry_opaque = false } in + let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in + let f_kn = Declare.declare_constant f f_def in + let f_kn_term = mkConst f_kn in + (* In the type and body of the proof of [suchthat] there can be + references to the variable [f]. It needs to be replaced by + references to the constant [f] declared above. This substitution + performs this precise action. *) + let substf c = Vars.replace_vars [f,f_kn_term] c in + (* Extracts the type of the proof of [suchthat]. *) + let lemma_pretype = + match Entries.(lemma_def.const_entry_type) with + | Some t -> t + | None -> assert false (* Proof_global always sets type here. *) + in + (* The references of [f] are subsituted appropriately. *) + let lemma_type = substf lemma_pretype in + (* The same is done in the body of the proof. *) + let lemma_body = Future.chain Entries.(lemma_def.const_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in + let lemma_def = let open Entries in + { lemma_def with + const_entry_body = lemma_body ; + const_entry_type = Some lemma_type ; + const_entry_opaque = opaque ; } + in + let lemma_def = + Entries.DefinitionEntry lemma_def , + Decl_kinds.(IsProof Proposition) + in + ignore (Declare.declare_constant name lemma_def) let save_lemma_proved ?proof ?lemma ~opaque ~idopt = (* Invariant (uh) *) @@ -550,10 +585,18 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt = | None -> (* XXX: The close_proof and proof state API should be refactored so it is possible to insert proofs properly into the state *) - let { proof; terminator; hook; compute_guard } = Option.get lemma in - Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, (terminator, hook, compute_guard) + let { proof; hook; compute_guard; proof_ending } = Option.get lemma in + Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, (hook, compute_guard, proof_ending) | Some (proof, info) -> proof, info in - let terminator, hook, compute_guard = proof_info in - CEphemeron.get terminator (Proved (opaque,idopt,proof_obj,hook,compute_guard)) + let hook, compute_guard, proof_ending = proof_info in + let open Proof_global in + let open Proof_ending in + match CEphemeron.default proof_ending Regular with + | Regular -> + finish_proved opaque idopt proof_obj hook compute_guard + | End_obligation oinfo -> + DeclareObl.obligation_terminator opaque proof_obj.entries proof_obj.universes oinfo + | End_derive { f ; name } -> + finish_derive ~f ~name ~idopt ~opaque ~entries:proof_obj.entries diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 961c1e41ef..51eada978a 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -11,9 +11,8 @@ open Names open Decl_kinds -(* Proofs that define a constant + terminators *) +(* Proofs that define a constant *) type t -type proof_terminator type lemma_possible_guards = int list list module Stack : sig @@ -38,8 +37,6 @@ module Stack : sig end -val standard_proof_terminator : proof_terminator - val set_endline_tactic : Genarg.glob_generic_argument -> t -> t val pf_map : (Proof_global.t -> Proof_global.t) -> t -> t val pf_fold : (Proof_global.t -> 'a) -> t -> 'a @@ -48,12 +45,21 @@ val by : unit Proofview.tactic -> t -> t * bool (* Start of high-level proofs with an associated constant *) +module Proof_ending : sig + + type t = + | Regular + | End_obligation of DeclareObl.obligation_qed_info + | End_derive of { f : Id.t; name : Id.t } + +end + val start_lemma : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map - -> ?terminator:proof_terminator + -> ?proof_ending:Proof_ending.t -> ?sign:Environ.named_context_val -> ?compute_guard:lemma_possible_guards -> ?hook:DeclareDef.Hook.t @@ -64,8 +70,7 @@ val start_dependent_lemma : Id.t -> ?pl:UState.universe_decl -> goal_kind - -> ?terminator:proof_terminator - -> ?sign:Environ.named_context_val + -> ?proof_ending:Proof_ending.t -> ?compute_guard:lemma_possible_guards -> ?hook:DeclareDef.Hook.t -> Proofview.telescope @@ -112,29 +117,8 @@ val save_lemma_proved -> idopt:Names.lident option -> unit -(* API to build a terminator, should go away *) -type proof_ending = - | Admitted of - Names.Id.t * - Decl_kinds.goal_kind * - Entries.parameter_entry * - UState.t * - DeclareDef.Hook.t option - | Proved of - Proof_global.opacity_flag * - lident option * - Proof_global.proof_object * - DeclareDef.Hook.t option * - lemma_possible_guards - -(** This stuff is internal and will be removed in the future. *) +(* To be removed *) module Internal : sig - (** Only needed due to the Proof_global compatibility layer. *) val get_info : t -> proof_info - - (** Only needed by obligations, should be reified soon *) - val make_terminator : (proof_ending -> unit) -> proof_terminator - val apply_terminator : proof_terminator -> proof_ending -> unit - end diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 9a34bda423..cd8d22ac9a 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -471,7 +471,7 @@ let obligation_hook prg obl num auto ctx' _ _ gr = if pred rem > 0 then begin let deps = dependencies obls num in if not (Int.Set.is_empty deps) then - ignore (auto (Some prg.prg_name) None deps) + ignore (auto (Some prg.prg_name) deps None) end let rec solve_obligation prg num tac = @@ -490,11 +490,10 @@ let rec solve_obligation prg num tac = let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in - let auto n tac oblset = auto_solve_obligations n ~oblset tac in - let terminator = Lemmas.Internal.make_terminator - (obligation_terminator prg.prg_name num auto) in + let auto n oblset tac = auto_solve_obligations n ~oblset tac in + let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in - let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in + let lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~proof_ending ~hook in let lemma = fst @@ Lemmas.by !default_tactic lemma in let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in lemma diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 0749314301..d28eeb341d 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -14,9 +14,9 @@ Proof_using Egramcoq Metasyntax DeclareDef -Lemmas DeclareObl Canonical +Lemmas Class Auto_ind_decl Search -- cgit v1.2.3 From c870ce7c386d12310ad15851ed3344a77943883a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 3 Apr 2019 04:03:52 +0200 Subject: [lemmas] Refactoring in saving goal. Just a cleanup, should bring no functional code change. --- vernac/lemmas.ml | 156 +++++++++++++++++++++++++++---------------------------- 1 file changed, 76 insertions(+), 80 deletions(-) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 686f52565c..416c92afaf 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -75,6 +75,10 @@ let by tac pf = let proof, res = Pfedit.by tac pf.proof in { pf with proof }, res +(************************************************************************) +(* Creating a lemma-like constant *) +(************************************************************************) + (* Support for mutually proved theorems *) let retrieve_first_recthm uctx = function @@ -198,37 +202,6 @@ let look_for_possibly_mutual_statements sigma = function Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds) | [] -> anomaly (Pp.str "Empty list of theorems.") -(* Saving a goal *) -let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes = - let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in - try - let const = adjust_guardness_conditions const do_guard in - let k = Kindops.logical_kind_of_goal_kind kind in - let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in - let r = match locality with - | Discharge -> - let c = SectionLocalDef const in - let _ = declare_variable id (Lib.cwd(), c, k) in - let () = if should_suggest - then Proof_using.suggest_variable (Global.env ()) id - in - VarRef id - | Global local -> - let kn = - declare_constant ?export_seff id ~local (DefinitionEntry const, k) in - let () = if should_suggest - then Proof_using.suggest_constant (Global.env ()) kn - in - let gr = ConstRef kn in - Declare.declare_univ_binders gr (UState.universe_binders uctx); - gr - in - definition_message id; - DeclareDef.Hook.call ~fix_exn ?hook universes [] locality r - with e when CErrors.noncritical e -> - let e = CErrors.push e in - iraise (fix_exn e) - let default_thm_id = Id.of_string "Unnamed_thm" let check_name_freshness locality {CAst.loc;v=id} : unit = @@ -285,47 +258,6 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i let kn = declare_constant id ~local (DefinitionEntry const, k) in (ConstRef kn,imps) -let check_anonymity id save_ident = - if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then - user_err Pp.(str "This command can only be used for unnamed theorem.") - -(* Admitted *) -let warn_let_as_axiom = - CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" - (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++ - spc () ++ strbrk "declared as a local axiom.") - -let admit ?hook ctx (id,k,e) pl () = - let local = match k with - | Global local, _, _ -> local - | Discharge, _, _ -> warn_let_as_axiom id; ImportNeedQualified - in - let kn = declare_constant id ~local (ParameterEntry e, IsAssumption Conjectural) in - let () = assumption_message id in - Declare.declare_univ_binders (ConstRef kn) pl; - DeclareDef.Hook.call ?hook ctx [] (Global local) (ConstRef kn) - -let finish_admitted id k pe ctx hook = - let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in - Feedback.feedback Feedback.AddedAxiom - -let finish_proved opaque idopt po hook compute_guard = - let open Proof_global in - match po with - | { id; entries=[const]; persistence; universes } -> - let is_opaque, export_seff = match opaque with - | Transparent -> false, true - | Opaque -> true, false - in - assert (is_opaque == const.const_entry_opaque); - let id = match idopt with - | None -> id - | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in - let () = save ~export_seff id const universes compute_guard persistence hook universes in - () - | _ -> - CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term") - let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right @@ -469,7 +401,31 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind thms = in start_lemma_with_initialization ?hook kind evd decl recguard thms snl -(* Saving a proof *) +(************************************************************************) +(* Admitting a lemma-like constant *) +(************************************************************************) + +let check_anonymity id save_ident = + if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then + user_err Pp.(str "This command can only be used for unnamed theorem.") + +(* Admitted *) +let warn_let_as_axiom = + CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" + (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++ + spc () ++ strbrk "declared as an axiom.") + +let finish_admitted id k pe ctx hook = + let local = match k with + | Global local, _, _ -> local + | Discharge, _, _ -> warn_let_as_axiom id; ImportNeedQualified + in + let kn = declare_constant id ~local (ParameterEntry pe, IsAssumption Conjectural) in + let () = assumption_message id in + Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx); + DeclareDef.Hook.call ?hook ctx [] (Global local) (ConstRef kn); + Feedback.feedback Feedback.AddedAxiom + let get_keep_admitted_vars = Goptions.declare_bool_option_and_ref ~depr:false @@ -527,12 +483,52 @@ type proof_info = DeclareDef.Hook.t option * lemma_possible_guards * Proof_endin let default_info = None, [], CEphemeron.create Proof_ending.Regular -let finish_derive ~f ~name ~idopt ~opaque ~entries = - (* Extracts the relevant information from the proof. [Admitted] and - [Save] result in user errors. [opaque] is [true] if the proof was - concluded by [Qed], and [false] if [Defined]. [f_def] and - [lemma_def] correspond to the proof of [f] and of [suchthat], - respectively. *) +let finish_proved opaque idopt po hook compute_guard = + let open Proof_global in + match po with + | { id; entries=[const]; persistence=locality,poly,kind; universes } -> + let is_opaque, export_seff = match opaque with + | Transparent -> false, true + | Opaque -> true, false + in + assert (is_opaque == const.const_entry_opaque); + let id = match idopt with + | None -> id + | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in + let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in + let () = try + let const = adjust_guardness_conditions const compute_guard in + let k = Kindops.logical_kind_of_goal_kind kind in + let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in + let r = match locality with + | Discharge -> + let c = SectionLocalDef const in + let _ = declare_variable id (Lib.cwd(), c, k) in + let () = if should_suggest + then Proof_using.suggest_variable (Global.env ()) id + in + VarRef id + | Global local -> + let kn = + declare_constant ~export_seff id ~local (DefinitionEntry const, k) in + let () = if should_suggest + then Proof_using.suggest_constant (Global.env ()) kn + in + let gr = ConstRef kn in + Declare.declare_univ_binders gr (UState.universe_binders universes); + gr + in + definition_message id; + DeclareDef.Hook.call ~fix_exn ?hook universes [] locality r + with e when CErrors.noncritical e -> + let e = CErrors.push e in + iraise (fix_exn e) + in () + | _ -> + CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term") + +let finish_derived ~f ~name ~idopt ~opaque ~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."); @@ -599,4 +595,4 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt = | End_obligation oinfo -> DeclareObl.obligation_terminator opaque proof_obj.entries proof_obj.universes oinfo | End_derive { f ; name } -> - finish_derive ~f ~name ~idopt ~opaque ~entries:proof_obj.entries + finish_derived ~f ~name ~idopt ~opaque ~entries:proof_obj.entries -- cgit v1.2.3 From 0ad30b6fce3eb757d06808e160a4c92e45686072 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 7 Jun 2019 21:28:07 +0200 Subject: [proof] Add proof save path for equations. We add the and routine the regular proof save path of Equations was using. I don't understand what is going on here, these are a few remarks: - Equations does capture `sigma` at the time of `start_dependent_lemma` - A custom hook is also captured, along with telescopes - The shrink function seems like a duplicate with things already in Coq's [abstract.ml / declareObl.ml] I guess the preferred option would be to merge this with the obligations save path; but I need help from experts. --- vernac/lemmas.ml | 87 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ vernac/lemmas.mli | 6 ++++ 2 files changed, 93 insertions(+) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 416c92afaf..091ff32009 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -44,6 +44,15 @@ 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 @@ -572,6 +581,82 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries = in ignore (Declare.declare_constant name lemma_def) +(* XXX several versions of shrink do appear in abstract, declareobl and here *) +module Equations = struct + let rec decompose len c t accu = + let open Constr in + let open Context.Rel.Declaration in + if len = 0 then (c, t, accu) + else match kind c, kind t with + | Lambda (na, u, c), Prod (_, _, t) -> + decompose (pred len) c t (LocalAssum (na, u) :: accu) + | LetIn (na, b, u, c), LetIn (_, _, _, t) -> + decompose (pred len) c t (LocalDef (na, b, u) :: accu) + | _ -> assert false + + let rec shrink ctx sign c t accu = + let open Constr in + let open Vars in + match ctx, sign with + | [], [] -> (c, t, accu) + | p :: ctx, decl :: sign -> + if noccurn 1 c && noccurn 1 t then + let c = subst1 mkProp c in + let t = subst1 mkProp t in + shrink ctx sign c t accu + else + let c = Term.mkLambda_or_LetIn p c in + let t = Term.mkProd_or_LetIn p t in + let accu = if RelDecl.is_local_assum p + then mkVar (NamedDecl.get_id decl) :: accu + else accu + in + shrink ctx sign c t accu + | _ -> assert false + + let shrink_entry sign const = + let open Entries in + let typ = match const.const_entry_type with + | None -> assert false + | Some t -> t + in + (* The body has been forced by the call to [build_constant_by_tactic] *) + (* let () = assert (Future.is_over const.const_entry_body) in *) + let ((body, uctx), eff) = Future.force const.const_entry_body in + let (body, typ, ctx) = decompose (List.length sign) body typ [] in + let (body, typ, args) = shrink ctx sign body typ [] in + let const = { const with + const_entry_body = Future.from_val ((body, uctx), eff); + const_entry_type = Some typ; + } in + (const, args) + + let finish_proved opaque lid proof_obj hook i types wits sigma = + + let open Decl_kinds in + let obls = ref 1 in + let kind = match pi3 proof_obj.Proof_global.persistence with + | DefinitionBody d -> IsDefinition d + | Proof p -> IsProof p + in + let evd = ref sigma in + let recobls = + CList.map2 (fun (wit, (evar_env, ev, evi, local_context, type_)) entry -> + let id = + match Evd.evar_ident ev sigma with + | Some id -> id + | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) + in + let entry, args = shrink_entry local_context entry in + let cst = Declare.declare_constant id (Entries.DefinitionEntry entry, kind) in + let sigma, app = Evarutil.new_global !evd (ConstRef cst) in + evd := Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma; + cst) + (CList.combine (List.rev !wits) types) proof_obj.Proof_global.entries + in + hook recobls !evd +end + let save_lemma_proved ?proof ?lemma ~opaque ~idopt = (* Invariant (uh) *) if Option.is_empty lemma && Option.is_empty proof then @@ -596,3 +681,5 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt = DeclareObl.obligation_terminator opaque proof_obj.entries proof_obj.universes oinfo | End_derive { f ; name } -> finish_derived ~f ~name ~idopt ~opaque ~entries:proof_obj.entries + | End_equations { hook; i; types; wits; sigma } -> + Equations.finish_proved opaque idopt proof_obj hook i types wits sigma diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 51eada978a..c5903bc874 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -51,6 +51,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 -- cgit v1.2.3 From 75e7c5b596d2a3e9b54e84788a15299568792584 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 11 Jun 2019 02:16:51 +0200 Subject: [equations] [proof] Remove duplicate shrink function. Equation's terminator had exactly duplicated the shrink function used in `Abstract`, we remove this duplicity. --- tactics/abstract.mli | 8 +++++ vernac/declareObl.ml | 1 + vernac/lemmas.ml | 99 +++++++++++++--------------------------------------- 3 files changed, 33 insertions(+), 75 deletions(-) diff --git a/tactics/abstract.mli b/tactics/abstract.mli index 9d4f3cfb27..0c74e898d2 100644 --- a/tactics/abstract.mli +++ b/tactics/abstract.mli @@ -20,3 +20,11 @@ val cache_term_by_tactic_then -> unit Proofview.tactic val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic + +(* Internal but used in a few places; should likely be made intro a + proper library function, or incorporated into the generic constant + save path *) +val shrink_entry + : ('a, 'b) Context.Named.Declaration.pt list + -> 'c Entries.definition_entry + -> 'c Entries.definition_entry * Constr.t list diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 71215d2a3e..30aa347692 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -95,6 +95,7 @@ let decompose_lam_prod c ty = in aux Context.Rel.empty c ty +(* XXX: What's the relation of this with Abstract.shrink ? *) let shrink_body c ty = let ctx, b, ty = match ty with diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 091ff32009..a1345f444b 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -581,81 +581,30 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries = in ignore (Declare.declare_constant name lemma_def) -(* XXX several versions of shrink do appear in abstract, declareobl and here *) -module Equations = struct - let rec decompose len c t accu = - let open Constr in - let open Context.Rel.Declaration in - if len = 0 then (c, t, accu) - else match kind c, kind t with - | Lambda (na, u, c), Prod (_, _, t) -> - decompose (pred len) c t (LocalAssum (na, u) :: accu) - | LetIn (na, b, u, c), LetIn (_, _, _, t) -> - decompose (pred len) c t (LocalDef (na, b, u) :: accu) - | _ -> assert false - - let rec shrink ctx sign c t accu = - let open Constr in - let open Vars in - match ctx, sign with - | [], [] -> (c, t, accu) - | p :: ctx, decl :: sign -> - if noccurn 1 c && noccurn 1 t then - let c = subst1 mkProp c in - let t = subst1 mkProp t in - shrink ctx sign c t accu - else - let c = Term.mkLambda_or_LetIn p c in - let t = Term.mkProd_or_LetIn p t in - let accu = if RelDecl.is_local_assum p - then mkVar (NamedDecl.get_id decl) :: accu - else accu - in - shrink ctx sign c t accu - | _ -> assert false +let finish_proved_equations opaque lid proof_obj hook i types wits sigma = - let shrink_entry sign const = - let open Entries in - let typ = match const.const_entry_type with - | None -> assert false - | Some t -> t - in - (* The body has been forced by the call to [build_constant_by_tactic] *) - (* let () = assert (Future.is_over const.const_entry_body) in *) - let ((body, uctx), eff) = Future.force const.const_entry_body in - let (body, typ, ctx) = decompose (List.length sign) body typ [] in - let (body, typ, args) = shrink ctx sign body typ [] in - let const = { const with - const_entry_body = Future.from_val ((body, uctx), eff); - const_entry_type = Some typ; - } in - (const, args) - - let finish_proved opaque lid proof_obj hook i types wits sigma = - - let open Decl_kinds in - let obls = ref 1 in - let kind = match pi3 proof_obj.Proof_global.persistence with - | DefinitionBody d -> IsDefinition d - | Proof p -> IsProof p - in - let evd = ref sigma in - let recobls = - CList.map2 (fun (wit, (evar_env, ev, evi, local_context, type_)) entry -> - let id = - match Evd.evar_ident ev sigma with - | Some id -> id - | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) - in - let entry, args = shrink_entry local_context entry in - let cst = Declare.declare_constant id (Entries.DefinitionEntry entry, kind) in - let sigma, app = Evarutil.new_global !evd (ConstRef cst) in - evd := Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma; - cst) - (CList.combine (List.rev !wits) types) proof_obj.Proof_global.entries - in - hook recobls !evd -end + let open Decl_kinds in + let obls = ref 1 in + let kind = match pi3 proof_obj.Proof_global.persistence with + | DefinitionBody d -> IsDefinition d + | Proof p -> IsProof p + in + let evd = ref sigma in + let recobls = + CList.map2 (fun (wit, (evar_env, ev, evi, local_context, type_)) entry -> + let id = + match Evd.evar_ident ev sigma with + | Some id -> id + | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) + in + let entry, args = Abstract.shrink_entry local_context entry in + let cst = Declare.declare_constant id (Entries.DefinitionEntry entry, kind) in + let sigma, app = Evarutil.new_global !evd (ConstRef cst) in + evd := Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma; + cst) + (CList.combine (List.rev !wits) types) proof_obj.Proof_global.entries + in + hook recobls !evd let save_lemma_proved ?proof ?lemma ~opaque ~idopt = (* Invariant (uh) *) @@ -682,4 +631,4 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt = | End_derive { f ; name } -> finish_derived ~f ~name ~idopt ~opaque ~entries:proof_obj.entries | End_equations { hook; i; types; wits; sigma } -> - Equations.finish_proved opaque idopt proof_obj hook i types wits sigma + finish_proved_equations opaque idopt proof_obj hook i types wits sigma -- cgit v1.2.3 From f147f7826aad760920efa7001586aa63002847d6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 11 Jun 2019 02:26:27 +0200 Subject: [equations] [proof] Remove reference to evar_map Small refactoring to pass the `sigma` functionally. --- vernac/lemmas.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index a1345f444b..2b204cb3de 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -581,7 +581,7 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries = in ignore (Declare.declare_constant name lemma_def) -let finish_proved_equations opaque lid proof_obj hook i types wits sigma = +let finish_proved_equations opaque lid proof_obj hook i types wits sigma0 = let open Decl_kinds in let obls = ref 1 in @@ -589,22 +589,21 @@ let finish_proved_equations opaque lid proof_obj hook i types wits sigma = | DefinitionBody d -> IsDefinition d | Proof p -> IsProof p in - let evd = ref sigma in - let recobls = - CList.map2 (fun (wit, (evar_env, ev, evi, local_context, type_)) entry -> + let sigma, recobls = + CList.fold_left2_map (fun sigma (wit, (evar_env, ev, evi, local_context, type_)) entry -> let id = - match Evd.evar_ident ev sigma with + match Evd.evar_ident ev sigma0 with | Some id -> id | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) in let entry, args = Abstract.shrink_entry local_context entry in let cst = Declare.declare_constant id (Entries.DefinitionEntry entry, kind) in - let sigma, app = Evarutil.new_global !evd (ConstRef cst) in - evd := Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma; - cst) + let sigma, app = Evarutil.new_global sigma (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 in - hook recobls !evd + hook recobls sigma let save_lemma_proved ?proof ?lemma ~opaque ~idopt = (* Invariant (uh) *) -- cgit v1.2.3 From a0d2a039a62e26b5d87a8cd9d77f4678f2bfda4a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 11 Jun 2019 03:03:20 +0200 Subject: [proof] Respond to a comment by Pierre-Marie --- proofs/proof_global.ml | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index a871a3fc95..ea08d0dda4 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -261,14 +261,22 @@ let return_proof ?(allow_partial=false) ps = let evd = Proof.return ~pid proof in let eff = Evd.eval_side_effects evd in let evd = Evd.minimize_universes evd in - (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate - side-effects... This may explain why one need to uniquize side-effects - thereafter... *) let proof_opt c = match EConstr.to_constr_opt evd c with | Some p -> p | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain") in + (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate + side-effects... This may explain why one need to uniquize side-effects + thereafter... *) + (* EJGA: actually side-effects de-duplication and this codepath is + unrelated. Duplicated side-effects arise from incorrect scheme + generation code, the main bulk of it was mostly fixed by #9836 + but duplication can still happen because of rewriting schemes I + think; however the code below is mostly untested, the only + code-paths that generate several proof entries are derive and + equations and so far there is no code in the CI that will + actually call those and do a side-effect, TTBOMK *) let proofs = List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in proofs, Evd.evar_universe_context evd -- cgit v1.2.3 From d5566d72e6dbefc3cf55cf4da13c99b8391c6d8b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 7 Jun 2019 22:03:21 +0200 Subject: [ci] Overlays for #9645 --- dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh diff --git a/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh b/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh new file mode 100644 index 0000000000..3029f3019c --- /dev/null +++ b/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "9645" ] || [ "$CI_BRANCH" = "proof+sayonara_baby" ]; then + + equations_CI_REF=proof+sayonara_baby + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + mtac2_CI_REF=proof+sayonara_baby + mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 + + paramcoq_CI_REF=proof+sayonara_baby + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + +fi -- cgit v1.2.3