diff options
38 files changed, 642 insertions, 579 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index cc58222fbf..51d90df89f 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -9,6 +9,17 @@ message. Main change to do generally is to change the flag "Global" to "Global ImportDefaultBehavior". +Proof state: + + Proofs that are attached to a top-level constant (such as lemmas) + are represented by `Lemmas.t`, as they do contain additional + information related to the constant declaration. + + Plugins that require access to the information about currently + opened lemmas can add one of the `![proof]` attributes to their + `mlg` entry, which will refine the type accordingly. See + documentation in `vernacentries` for more information. + ## Changes between Coq 8.9 and Coq 8.10 ### ML4 Pre Processing @@ -63,6 +74,19 @@ Coqlib: command then enables to locate the registered constant through its name. The name resolution is dynamic. +Proof state: + +- Handling of proof state has been fully functionalized, thus it is + not possible to call global functions such as `get_current_context ()`. + + The main type for functions that need to handle proof state is + `Proof_global.t`. + + Unfortunately, this change was not possible to do in a + backwards-compatible way, but in most case the api changes are + straightforward, with functions taking and returning an extra + argument. + Macros: - The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 0b005a2341..73d94c2a51 100644 --- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -287,7 +287,7 @@ VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY | ![ proof_query ] [ "ExploreProof" ] -> { fun ~pstate -> let sigma, env = Pfedit.get_current_context pstate in - let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in + let pprf = Proof.partial_proof (Proof_global.get_proof pstate) in Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) } diff --git a/ide/idetop.ml b/ide/idetop.ml index 90bd2f314d..a3b8854e8f 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -339,8 +339,7 @@ let import_search_constraint = function | Interface.Include_Blacklist -> Search.Include_Blacklist let search flags = - let pstate = Vernacstate.Proof_global.get () in - let pstate = Option.map Proof_global.get_current_pstate pstate in + let pstate = Vernacstate.Proof_global.get_pstate () in List.map export_coq_object (Search.interface_search ?pstate ( List.map (fun (c, b) -> (import_search_constraint c, b)) flags) ) diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 7c0f269481..fd5b3a7e48 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -22,7 +22,7 @@ let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Ent (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] and [lemma] as the proof. *) -let start_deriving f suchthat lemma = +let start_deriving f suchthat name : Lemmas.t = let env = Global.env () in let sigma = Evd.from_env env in @@ -48,7 +48,6 @@ let start_deriving f suchthat lemma = (* The terminator handles the registering of constants when the proof is closed. *) let terminator com = - let open Proof_global in (* 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] @@ -56,10 +55,10 @@ let start_deriving f suchthat lemma = [suchthat], respectively. *) let (opaque,f_def,lemma_def) = match com with - | Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.") - | Proved (_,Some _,_) -> + | 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.") - | 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 @@ -97,12 +96,11 @@ let start_deriving f suchthat lemma = Entries.DefinitionEntry lemma_def , Decl_kinds.(IsProof Proposition) in - ignore (Declare.declare_constant lemma lemma_def) - in + ignore (Declare.declare_constant name lemma_def) + in - let terminator = Proof_global.make_terminator terminator in - let pstate = Proof_global.start_dependent_proof lemma kind goals terminator in - Proof_global.modify_proof begin fun p -> - let p,_,() = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in - p - end pstate + let terminator ?hook _ = Lemmas.make_terminator terminator in + let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in + Lemmas.simple_with_proof begin fun _ p -> + Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p + end lemma diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 6bb923118e..ffbc726e22 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -12,4 +12,8 @@ (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] and [lemma] as the proof. *) -val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t +val start_deriving + : Names.Id.t + -> Constrexpr.constr_expr + -> Names.Id.t + -> Lemmas.t diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index 526989fdf3..6c9cd66f96 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -24,5 +24,5 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof | [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - { Derive.(start_deriving f suchthat lemma) } + { Derive.start_deriving f suchthat lemma } END diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index c5439ffaf6..4cd34100bc 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -752,13 +752,13 @@ let extract_and_compile l = (* Show the extraction of the current ongoing proof *) let show_extraction ~pstate = init ~inner:true false false; - let prf = Proof_global.give_me_the_proof pstate in + let prf = Proof_global.get_proof pstate in let sigma, env = Pfedit.get_current_context pstate in let trms = Proof.partial_proof prf in let extr_term t = let ast, ty = extract_constr env sigma t in let mp = Lib.current_mp () in - let l = Label.of_id (Proof_global.get_current_proof_name pstate) in + let l = Label.of_id (Proof_global.get_proof_name pstate) in let fake_ref = ConstRef (Constant.make2 mp l) in let decl = Dterm (fake_ref, ast, ty) in print_one_decl [] mp decl diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index b3a799fb6a..b8e1286b9e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -990,7 +990,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num ] in (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) - let pstate = Lemmas.start_proof + let lemma = Lemmas.start_lemma (*i The next call to mk_equation_id is valid since we are constructing the lemma Ensures by: obvious i*) @@ -999,12 +999,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num evd lemma_type in - let pstate,_ = Pfedit.by (Proofview.V82.tactic prove_replacement) pstate in - let ontop = Proof_global.push ~ontop:None pstate in - ignore(Lemmas.save_proof_proved ?proof:None ~ontop ~opaque:Proof_global.Transparent ~idopt:None); + let lemma,_ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in + let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in evd - let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g = let equation_lemma = try @@ -1725,11 +1723,3 @@ let prove_principle_for_gen ] gl - - - - - - - - diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 965ce68811..d1e540cceb 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -308,8 +308,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin 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 pstate = - Lemmas.start_proof + let lemma = + Lemmas.start_lemma new_princ_name Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) !evd @@ -317,7 +317,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin in (* let _tim1 = System.get_time () in *) let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in - let pstate,_ = Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)) pstate in + let lemma,_ = Lemmas.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)) lemma in (* let _tim2 = System.get_time () in *) (* begin *) (* let dur1 = System.time_difference tim1 tim2 in *) @@ -325,7 +325,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* end; *) let open Proof_global in - let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pstate in + let { id; entries; persistence } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in match entries with | [entry] -> (id,(entry,persistence)), hook diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 7070f01c6f..d710f4490d 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -634,9 +634,9 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex let do_generate_principle_aux pconstants on_error register_built interactive_proof - (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option = + (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Lemmas.t option = List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; - let pstate, _is_struct = + let lemma, _is_struct = match fixpoint_exprl with | [((_,Some {CAst.v = Constrexpr.CWfRec (wf_x,wf_rel)},_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr = @@ -702,7 +702,7 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro (* ok all the expressions are structural *) let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let is_rec = List.exists (is_rec fix_names) recdefs in - let pstate,evd,pconstants = + let lemma,evd,pconstants = if register_built then register_struct is_rec fixpoint_exprl else None, Evd.from_env (Global.env ()), pconstants @@ -720,9 +720,9 @@ let do_generate_principle_aux pconstants on_error register_built interactive_pro (Functional_principles_proofs.prove_princ_for_struct evd interactive_proof); if register_built then begin derive_inversion fix_names; end; - pstate, true + lemma, true in - pstate + lemma let rec add_args id new_args = CAst.map (function | CRef (qid,_) as b -> @@ -911,18 +911,18 @@ let make_graph (f_ref : GlobRef.t) = (* *************** statically typed entrypoints ************************* *) -let do_generate_principle_interactive fixl : Proof_global.t = +let do_generate_principle_interactive fixl : Lemmas.t = match do_generate_principle_aux [] warning_error true true fixl with - | Some pstate -> pstate + | Some lemma -> lemma | None -> - CErrors.anomaly - (Pp.str"indfun: leaving no open proof in interactive mode") + CErrors.anomaly + (Pp.str"indfun: leaving no open proof in interactive mode") let do_generate_principle fixl : unit = match do_generate_principle_aux [] warning_error true false fixl with - | Some _pstate -> - CErrors.anomaly - (Pp.str"indfun: leaving a goal open in non-interactive mode") + | Some _lemma -> + CErrors.anomaly + (Pp.str"indfun: leaving a goal open in non-interactive mode") | None -> () diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 1ba245a45d..3bc52272ac 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -10,7 +10,7 @@ val do_generate_principle : val do_generate_principle_interactive : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - Proof_global.t + Lemmas.t val functional_induction : bool -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8a16326ba3..857b7df96f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -803,15 +803,15 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list i*) let lem_id = mk_correct_id f_id in let (typ,_) = lemmas_types_infos.(i) in - let pstate = Lemmas.start_proof + let lemma = Lemmas.start_lemma lem_id Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) !evd typ in - let pstate = fst @@ Pfedit.by + let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") - (proving_tac i))) pstate in - let () = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None in + (proving_tac i))) lemma in + let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in let finfo = find_Function_infos (fst f_as_constant) in (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) let _,lem_cst_constr = Evd.fresh_global @@ -865,13 +865,13 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - let pstate = Lemmas.start_proof lem_id + let lemma = Lemmas.start_lemma lem_id Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma (fst lemmas_types_infos.(i)) in - let pstate = fst (Pfedit.by + let lemma = fst (Lemmas.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") - (proving_tac i))) pstate) in - let () = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None in + (proving_tac i))) lemma) in + let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in let finfo = find_Function_infos (fst f_as_constant) in let _,lem_cst_constr = Evd.fresh_global (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5bedb360d1..17d962f30f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -34,7 +34,6 @@ open Declare open Decl_kinds open Tacred open Goal -open Pfedit open Glob_term open Pretyping open Termops @@ -72,7 +71,8 @@ let declare_fun f_id kind ?univs value = let ce = definition_entry ?univs value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; -let defined pstate = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None +let defined lemma = + Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None let def_of_const t = match (Constr.kind t) with @@ -1221,7 +1221,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a end let get_current_subgoals_types pstate = - let p = Proof_global.give_me_the_proof pstate in + let p = Proof_global.get_proof pstate in let Proof.{ goals=sgs; sigma; _ } = Proof.data p in sigma, List.map (Goal.V82.abstract_type sigma) sgs @@ -1281,8 +1281,8 @@ let clear_goals sigma = List.map clear_goal -let build_new_goal_type pstate = - let sigma, sub_gls_types = get_current_subgoals_types pstate in +let build_new_goal_type lemma = + let sigma, sub_gls_types = Lemmas.pf_fold get_current_subgoals_types lemma in (* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) let sub_gls_types = clear_goals sigma sub_gls_types in (* Pp.msgnl (str "sub_gls_types2 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) @@ -1297,9 +1297,9 @@ let is_opaque_constant c = | Declarations.Def _ -> Proof_global.Transparent | Declarations.Primitive _ -> Proof_global.Opaque -let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = +let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) - let current_proof_name = Proof_global.get_current_proof_name pstate in + let current_proof_name = Lemmas.pf_fold Proof_global.get_proof_name lemma in let name = match goal_name with | Some s -> s | None -> @@ -1323,7 +1323,7 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type let lid = ref [] in let h_num = ref (-1) in let env = Global.env () in - let pstate = build_proof env (Evd.from_env env) + let lemma = build_proof env (Evd.from_env env) ( fun gls -> let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in observe_tclTHENLIST (fun _ _ -> str "") @@ -1367,17 +1367,17 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type ) g) in - Lemmas.save_pstate_proved ~pstate ~opaque:opacity ~idopt:None + Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None in - let pstate = Lemmas.start_proof + let lemma = Lemmas.start_lemma na Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) sigma gls_type ~hook:(Lemmas.mk_hook hook) in - let pstate = if Indfun_common.is_strict_tcc () + let lemma = if Indfun_common.is_strict_tcc () then - fst @@ by (Proofview.V82.tactic (tclIDTAC)) pstate + fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma else - fst @@ by (Proofview.V82.tactic begin + fst @@ Lemmas.by (Proofview.V82.tactic begin fun g -> tclTHEN (decompose_and_tac) @@ -1393,9 +1393,9 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type ) using_lemmas) ) tclIDTAC) - g end) pstate + g end) lemma in - if Proof_global.get_open_goals pstate = 0 then (defined pstate; None) else Some pstate + if Lemmas.(pf_fold Proof_global.get_open_goals) lemma = 0 then (defined lemma; None) else Some lemma let com_terminate interactive_proof @@ -1410,26 +1410,26 @@ let com_terminate nb_args ctx hook = let start_proof env ctx (tac_start:tactic) (tac_end:tactic) = - let pstate = Lemmas.start_proof thm_name + let lemma = Lemmas.start_lemma thm_name (Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook in - let pstate = fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) pstate in - fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref - input_type relation rec_arg_num ))) pstate + let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) lemma in + fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref + input_type relation rec_arg_num ))) lemma in - let pstate = start_proof Global.(env ()) ctx tclIDTAC tclIDTAC in + let lemma = start_proof Global.(env ()) ctx tclIDTAC tclIDTAC in try - let sigma, new_goal_type = build_new_goal_type pstate in + let sigma, new_goal_type = build_new_goal_type lemma in let sigma = Evd.from_ctx (Evd.evar_universe_context sigma) in - open_new_goal pstate start_proof sigma + open_new_goal ~lemma start_proof sigma using_lemmas tcc_lemma_ref (Some tcc_lemma_name) (new_goal_type) with EmptySubgoals -> (* a non recursive function declared with measure ! *) tcc_lemma_ref := Not_needed; - if interactive_proof then Some pstate - else (defined pstate; None) + if interactive_proof then Some lemma + else (defined lemma; None) let start_equation (f:GlobRef.t) (term_f:GlobRef.t) (cont_tactic:Id.t list -> tactic) g = @@ -1457,9 +1457,9 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation let evd = Evd.from_ctx uctx in let f_constr = constr_of_monomorphic_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - let pstate = Lemmas.start_proof eq_name (Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd + let lemma = Lemmas.start_lemma eq_name (Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd (EConstr.of_constr equation_lemma_type) in - let pstate = fst @@ by + let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (start_equation f_ref terminate_ref (fun x -> prove_eq (fun _ -> tclIDTAC) @@ -1486,14 +1486,14 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation ih = Id.of_string "______"; } ) - )) pstate in - let _ = Flags.silently (fun () -> Lemmas.save_pstate_proved ~pstate ~opaque:opacity ~idopt:None) () in + )) lemma in + let _ = Flags.silently (fun () -> Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None) () in () (* Pp.msgnl (fun _ _ -> str "eqn finished"); *) let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type_of_f r rec_arg_num eq - generate_induction_principle using_lemmas : Proof_global.t option = + generate_induction_principle using_lemmas : Lemmas.t option = let open Term in let open Constr in let open CVars in @@ -1550,8 +1550,9 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type let stop = (* XXX: What is the correct way to get sign at hook time *) let sign = Environ.named_context_val Global.(env ()) in - try com_eqn sign uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); - false + try + com_eqn sign uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); + false with e when CErrors.noncritical e -> begin if do_observe () @@ -1582,15 +1583,15 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type in (* XXX STATE Why do we need this... why is the toplevel protection not enough *) funind_purify (fun () -> - let pstate = com_terminate - interactive_proof - tcc_lemma_name - tcc_lemma_constr - is_mes functional_ref - (EConstr.of_constr rec_arg_type) - relation rec_arg_num - term_id - using_lemmas - (List.length res_vars) - evd (Lemmas.mk_hook hook) - in pstate) () + com_terminate + interactive_proof + tcc_lemma_name + tcc_lemma_constr + is_mes functional_ref + (EConstr.of_constr rec_arg_type) + relation rec_arg_num + term_id + using_lemmas + (List.length res_vars) + evd (Lemmas.mk_hook hook)) + () diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index b92ac3a0ec..e6aa452def 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -1,23 +1,21 @@ open Constr -val tclUSER_if_not_mes : +val tclUSER_if_not_mes : Tacmach.tactic -> - bool -> - Names.Id.t list option -> + bool -> + Names.Id.t list option -> Tacmach.tactic -val recursive_definition : - interactive_proof:bool -> - is_mes:bool -> - Names.Id.t -> - Constrintern.internalization_env -> - Constrexpr.constr_expr -> - Constrexpr.constr_expr -> - int -> - Constrexpr.constr_expr -> - (pconstant -> - Indfun_common.tcc_lemma_value ref -> - pconstant -> - pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> - Constrexpr.constr_expr list -> - Proof_global.t option +val recursive_definition + : interactive_proof:bool + -> is_mes:bool + -> Names.Id.t + -> Constrintern.internalization_env + -> Constrexpr.constr_expr + -> Constrexpr.constr_expr + -> int + -> Constrexpr.constr_expr + -> (pconstant -> Indfun_common.tcc_lemma_value ref -> pconstant -> + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) + -> Constrexpr.constr_expr list + -> Lemmas.t option diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index b99e77ab2b..2da6584aba 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1962,7 +1962,6 @@ let add_setoid atts binders a aeq t n = (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])] - let make_tactic name = let open Tacexpr in let tacqid = Libnames.qualid_of_string name in @@ -1988,7 +1987,7 @@ let add_morphism_as_parameter atts m n : unit = (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); declare_projection n instance_id (ConstRef cst) -let add_morphism_interactive atts m n : Proof_global.t = +let add_morphism_interactive atts m n : Lemmas.t = warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); let instance_id = add_suffix n "_Proper" in @@ -2010,8 +2009,8 @@ let add_morphism_interactive atts m n : Proof_global.t = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in - fst Pfedit.(by (Tacinterp.interp tac) pstate)) () + let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in + fst (Lemmas.by (Tacinterp.interp tac) lemma)) () let add_morphism atts binders m s n = init_setoid (); @@ -2023,12 +2022,12 @@ let add_morphism atts binders m s n = [cHole; s; m]) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - let _id, pstate = Classes.new_instance_interactive + let _id, lemma = Classes.new_instance_interactive ~global:atts.global atts.polymorphic instance_name binders instance_t ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in - pstate (* no instance body -> always open proof *) + lemma (* no instance body -> always open proof *) (** Bind to "rewrite" too *) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 3ef33c6dc9..a5c3782b30 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -101,16 +101,16 @@ val add_setoid -> Id.t -> unit -val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t +val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Lemmas.t val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit val add_morphism - : rewrite_attributes + : rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t - -> Proof_global.t + -> Lemmas.t val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index c7fcc66120..00144e87dc 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -42,11 +42,11 @@ let get_goal_context_gen pf i = (sigma, Refiner.pf_env { it=goal ; sigma=sigma; }) let get_goal_context pf i = - let p = Proof_global.give_me_the_proof pf in + let p = Proof_global.get_proof pf in get_goal_context_gen p i let get_current_goal_context pf = - let p = Proof_global.give_me_the_proof pf in + let p = Proof_global.get_proof pf in try get_goal_context_gen p 1 with | NoSuchGoal -> @@ -57,7 +57,7 @@ let get_current_goal_context pf = Evd.from_env env, env let get_current_context pf = - let p = Proof_global.give_me_the_proof pf in + let p = Proof_global.get_proof pf in try get_goal_context_gen p 1 with | NoSuchGoal -> @@ -119,13 +119,12 @@ let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehavior, false, Proof Theorem) typ tac = let evd = Evd.from_ctx ctx in - let terminator = Proof_global.make_terminator (fun _ -> ()) in let goals = [ (Global.env_of_context sign , typ) ] in - let pf = Proof_global.start_proof evd id goal_kind goals terminator in + let pf = Proof_global.start_proof evd id goal_kind goals in try let pf, status = by tac pf in let open Proof_global in - let { entries; universes } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in + let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in match entries with | [entry] -> let univs = UState.demote_seff_univs entry universes in diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index b642e8eea7..f06b2885e2 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -36,65 +36,20 @@ type proof_object = { type opacity_flag = Opaque | Transparent -type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t - | Proved of opacity_flag * - lident option * - proof_object - -type proof_terminator = proof_ending -> unit -type closed_proof = proof_object * proof_terminator - -type t = { - terminator : proof_terminator CEphemeron.key; - endline_tactic : Genarg.glob_generic_argument option; - section_vars : Constr.named_context option; - proof : Proof.t; - universe_decl: UState.universe_decl; - strength : Decl_kinds.goal_kind; -} - -(* The head of [t] is the actual current proof, the other ones are - to be resumed when the current proof is closed or aborted. *) -type stack = t * t list - -let pstate_map f (pf, pfl) = (f pf, List.map f pfl) - -let make_terminator f = f -let apply_terminator f = f - -let get_current_pstate (ps,_) = ps - -(* combinators for the current_proof lists *) -let push ~ontop a = - match ontop with - | None -> a , [] - | Some (l,ls) -> a, (l :: ls) - -let maybe_push ~ontop = function - | Some pstate -> Some (push ~ontop pstate) - | None -> ontop +type t = + { endline_tactic : Genarg.glob_generic_argument option + ; section_vars : Constr.named_context option + ; proof : Proof.t + ; universe_decl: UState.universe_decl + ; strength : Decl_kinds.goal_kind + } (*** Proof Global manipulation ***) -let get_all_proof_names (pf : stack) = - let (pn, pns) = pstate_map Proof.(function pf -> (data pf.proof).name) pf in - pn :: pns - -let give_me_the_proof ps = ps.proof -let get_current_proof_name ps = (Proof.data ps.proof).Proof.name -let get_current_persistence ps = ps.strength - -let with_current_pstate f (ps,psl) = - let ps, ret = f ps in - (ps, psl), ret - -let modify_current_pstate f (ps,psl) = - f ps, psl - -let modify_proof f ps = - let proof = f ps.proof in - {ps with proof} +let get_proof ps = ps.proof +let get_proof_name ps = (Proof.data ps.proof).Proof.name +let get_persistence ps = ps.strength +let modify_proof f p = { p with proof = f p.proof } let with_proof f ps = let et = @@ -111,13 +66,6 @@ let with_proof f ps = let ps = { ps with proof = newpr } in ps, ret -let with_current_proof f (ps,rest) = - let ps, ret = with_proof f ps in - (ps, rest), ret - -let simple_with_current_proof f pf = - let p, () = with_current_proof (fun t p -> f t p , ()) pf in p - let simple_with_proof f ps = let ps, () = with_proof (fun t ps -> f t ps, ()) ps in ps @@ -127,21 +75,7 @@ let compact_the_proof pf = simple_with_proof (fun _ -> Proof.compact) pf let set_endline_tactic tac ps = { ps with endline_tactic = Some tac } -let pf_name_eq id ps = - let Proof.{ name } = Proof.data ps.proof in - Id.equal name id - -let discard {CAst.loc;v=id} (ps, psl) = - match List.filter (fun pf -> not (pf_name_eq id pf)) (ps :: psl) with - | [] -> None - | ps :: psl -> Some (ps, psl) - -let discard_current (_, psl) = - match psl with - | [] -> None - | ps :: psl -> Some (ps, psl) - -(** [start_proof sigma id pl str goals terminator] starts a proof of name +(** [start_proof sigma id pl str goals] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this is (spiwack: for potential printing, I believe is used only by @@ -149,21 +83,21 @@ let discard_current (_, psl) = end of the proof to close the proof. The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator = - { terminator = CEphemeron.create terminator; - proof = Proof.start ~name ~poly:(pi2 kind) sigma goals; - endline_tactic = None; - section_vars = None; - universe_decl = pl; - strength = kind } - -let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator = - { terminator = CEphemeron.create terminator; - proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals; - endline_tactic = None; - section_vars = None; - universe_decl = pl; - strength = kind } +let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals = + { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals + ; endline_tactic = None + ; section_vars = None + ; universe_decl = pl + ; strength = kind + } + +let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals = + { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals + ; endline_tactic = None + ; section_vars = None + ; universe_decl = pl + ; strength = kind + } let get_used_variables pf = pf.section_vars let get_universe_decl pf = pf.universe_decl @@ -217,7 +151,7 @@ let private_poly_univs = let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now (fpl : closed_proof_output Future.computation) ps = - let { section_vars; proof; terminator; universe_decl; strength } = ps in + let { section_vars; proof; universe_decl; strength } = ps in let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in let opaque = match opaque with Opaque -> true | Transparent -> false in let constrain_variables ctx = @@ -312,8 +246,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now in let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in { id = name; entries = entries; persistence = strength; - universes }, - fun pr_ending -> CEphemeron.get terminator pr_ending + universes } let return_proof ?(allow_partial=false) ps = let { proof } = ps in @@ -351,22 +284,11 @@ let close_proof ~opaque ~keep_body_ucst_separate fix_exn ps = close_proof ~opaque ~keep_body_ucst_separate ~now:true (Future.from_val ~fix_exn (return_proof ps)) ps -(** Gets the current terminator without checking that the proof has - been completed. Useful for the likes of [Admitted]. *) -let get_terminator ps = CEphemeron.get ps.terminator -let set_terminator hook ps = - { ps with terminator = CEphemeron.create hook } - -let copy_terminators ~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 - let update_global_env pf = let res, () = with_proof (fun _ p -> - Proof.in_proof p (fun sigma -> - let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in - let (p,(status,info),()) = Proof.run_tactic (Global.env ()) tac p in - (p, ()))) pf + Proof.in_proof p (fun sigma -> + let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in + let p,(status,info),_ = Proof.run_tactic (Global.env ()) tac p in + (p, ()))) pf in res diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index aff48b9636..84a833fb2c 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -13,18 +13,16 @@ environment. *) type t -type stack -val get_current_pstate : stack -> t - -val get_current_proof_name : t -> Names.Id.t -val get_current_persistence : t -> Decl_kinds.goal_kind -val get_all_proof_names : stack -> Names.Id.t list +(* Should be moved into a proper view *) +val get_proof : t -> Proof.t +val get_proof_name : t -> Names.Id.t +val get_persistence : t -> Decl_kinds.goal_kind +val get_used_variables : t -> Constr.named_context option -val discard : Names.lident -> stack -> stack option -val discard_current : stack -> stack option +(** Get the universe declaration associated to the current proof. *) +val get_universe_decl : t -> UState.universe_decl -val give_me_the_proof : t -> Proof.t val compact_the_proof : t -> t (** When a proof is closed, it is reified into a [proof_object], where @@ -44,23 +42,7 @@ type proof_object = { type opacity_flag = Opaque | Transparent -type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * - UState.t - | Proved of opacity_flag * - Names.lident option * - proof_object -type proof_terminator -type closed_proof = proof_object * proof_terminator - -val make_terminator : (proof_ending -> unit) -> proof_terminator -val apply_terminator : proof_terminator -> proof_ending -> unit - -val push : ontop:stack option -> t -> stack - -val maybe_push : ontop:stack option -> t option -> stack option - -(** [start_proof ~ontop id str pl goals terminator] starts a proof of name +(** [start_proof id str pl goals] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this is; [terminator] is used at the end of the proof to close the proof @@ -68,16 +50,22 @@ val maybe_push : ontop:stack option -> t option -> stack option morphism). The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -val start_proof : - Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl -> - Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> - proof_terminator -> t +val start_proof + : Evd.evar_map + -> Names.Id.t + -> ?pl:UState.universe_decl + -> Decl_kinds.goal_kind + -> (Environ.env * EConstr.types) list + -> t (** Like [start_proof] except that there may be dependencies between initial goals. *) -val start_dependent_proof : - Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> - Proofview.telescope -> proof_terminator -> t +val start_dependent_proof + : Names.Id.t + -> ?pl:UState.universe_decl + -> Decl_kinds.goal_kind + -> Proofview.telescope + -> t (** Update the proofs global environment after a side-effecting command (e.g. a sublemma definition) has been run inside it. Assumes @@ -86,8 +74,7 @@ val update_global_env : t -> t (* Takes a function to add to the exceptions data relative to the state in which the proof was built *) -val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> - t -> closed_proof +val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> proof_object (* Intermediate step necessary to delegate the future. * Both access the current proof state. The former is supposed to be @@ -99,28 +86,17 @@ type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * USt * is allowed (no error), and a warn is given if the proof is complete. *) val return_proof : ?allow_partial:bool -> t -> closed_proof_output val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> t -> - closed_proof_output Future.computation -> closed_proof + closed_proof_output Future.computation -> proof_object -(** Gets the current terminator without checking that the proof has - been completed. Useful for the likes of [Admitted]. *) -val get_terminator : t -> proof_terminator -val set_terminator : proof_terminator -> t -> t val get_open_goals : t -> int (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is no current proof. The return boolean is set to [false] if an unsafe tactic has been used. *) -val with_current_proof : - (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> stack -> stack * 'a -val simple_with_current_proof : - (unit Proofview.tactic -> Proof.t -> Proof.t) -> stack -> stack - val with_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a +val simple_with_proof : (unit Proofview.tactic -> Proof.t -> Proof.t) -> t -> t val modify_proof : (Proof.t -> Proof.t) -> t -> t -val with_current_pstate : (t -> t * 'a) -> stack -> stack * 'a -val modify_current_pstate : (t -> t) -> stack -> stack - (** Sets the tactic to be used when a tactic line is closed with [...] *) val set_endline_tactic : Genarg.glob_generic_argument -> t -> t @@ -129,10 +105,3 @@ val set_endline_tactic : Genarg.glob_generic_argument -> t -> t * ids to be cleared *) val set_used_variables : t -> Names.Id.t list -> (Constr.named_context * Names.lident list) * t - -val get_used_variables : t -> Constr.named_context option - -(** Get the universe declaration associated to the current proof. *) -val get_universe_decl : t -> UState.universe_decl - -val copy_terminators : src:stack -> tgt:stack -> stack diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index dfa681395a..7ff6ed9dfb 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -48,15 +48,14 @@ let simple_goal sigma g gs = let is_focused_goal_simple ~doc id = match state_of_id ~doc id with | `Expired | `Error _ | `Valid None -> `Not - | `Valid (Some { Vernacstate.proof }) -> - Option.cata (fun proof -> - let proof = Proof_global.get_current_pstate proof in - let proof = Proof_global.give_me_the_proof proof in + | `Valid (Some { Vernacstate.lemmas }) -> + Option.cata (Lemmas.Stack.with_top_pstate ~f:(fun proof -> + let proof = Proof_global.get_proof proof in let Proof.{ goals=focused; stack=r1; shelf=r2; given_up=r3; sigma } = Proof.data proof in let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in if List.for_all (fun x -> simple_goal sigma x rest) focused then `Simple focused - else `Not) `Not proof + else `Not)) `Not lemmas type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ] diff --git a/stm/stm.ml b/stm/stm.ml index 5baa6ce251..a282efe265 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -881,7 +881,7 @@ end = struct (* {{{ *) let invalidate_cur_state () = cur_id := Stateid.dummy type proof_part = - Proof_global.stack option * + 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 *) @@ -890,9 +890,9 @@ end = struct (* {{{ *) [ `Full of Vernacstate.t | `ProofOnly of Stateid.t * proof_part ] - let proof_part_of_frozen { Vernacstate.proof; system } = + let proof_part_of_frozen { Vernacstate.lemmas; system } = let st = States.summary_of_state system in - proof, + lemmas, Summary.project_from_summary st Util.(pi1 summary_pstate), Summary.project_from_summary st Util.(pi2 summary_pstate), Summary.project_from_summary st Util.(pi3 summary_pstate) @@ -956,17 +956,17 @@ end = struct (* {{{ *) try let prev = (VCS.visit id).next in if is_cached_and_valid prev - then { s with proof = + then { s with lemmas = PG_compat.copy_terminators - ~src:((get_cached prev).proof) ~tgt:s.proof } + ~src:((get_cached prev).lemmas) ~tgt:s.lemmas } else s with VCS.Expired -> s in VCS.set_state id (FullState s) | `ProofOnly(ontop,(pstate,c1,c2,c3)) -> if is_cached_and_valid ontop then let s = get_cached ontop in - let s = { s with proof = - PG_compat.copy_terminators ~src:s.proof ~tgt:pstate } in + let s = { s with lemmas = + PG_compat.copy_terminators ~src:s.lemmas ~tgt:pstate } in let s = { s with system = States.replace_summary s.system begin @@ -1168,9 +1168,7 @@ end = struct (* {{{ *) let get_proof ~doc id = match state_of_id ~doc id with - | `Valid (Some vstate) -> - Option.map (fun p -> Proof_global.(give_me_the_proof (get_current_pstate p))) - vstate.Vernacstate.proof + | `Valid (Some vstate) -> Option.map (Lemmas.Stack.with_top_pstate ~f:Proof_global.get_proof) vstate.Vernacstate.lemmas | _ -> None let undo_vernac_classifier v ~doc = @@ -2310,8 +2308,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = Proofview.give_up else Proofview.tclUNIT () end in match (VCS.get_info base_state).state with - | FullState { Vernacstate.proof } -> - Option.iter PG_compat.unfreeze proof; + | FullState { Vernacstate.lemmas } -> + Option.iter PG_compat.unfreeze lemmas; PG_compat.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; fst (Pfedit.solve Goal_select.SelectAll None tac p), ()); diff --git a/tactics/hints.ml b/tactics/hints.ml index cc56c1c425..6fcb37d87c 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1518,7 +1518,7 @@ let pr_hint_term env sigma cl = (* print all hints that apply to the concl of the current goal *) let pr_applicable_hint pf = let env = Global.env () in - let pts = Proof_global.give_me_the_proof pf in + let pts = Proof_global.get_proof pf in let Proof.{goals;sigma} = Proof.data pts in match goals with | [] -> CErrors.user_err Pp.(str "No focused goal.") diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 246fe47c4a..10dd1c4f58 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -751,7 +751,7 @@ let perform_eval ~pstate e = Goal_select.SelectAll, Proof.start ~name ~poly sigma [] | Some pstate -> Goal_select.get_default_goal_selector (), - Proof_global.give_me_the_proof pstate + Proof_global.get_proof pstate in let v = match selector with | Goal_select.SelectNth i -> Proofview.tclFOCUS i i v diff --git a/vernac/classes.ml b/vernac/classes.ml index ed207b52dd..b64af52b6e 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -378,11 +378,11 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in let kind = Decl_kinds.(Global ImportDefaultBehavior, poly, DefinitionBody Instance) in - let pstate = Lemmas.start_proof id ~pl:decl kind sigma (EConstr.of_constr termtype) + let lemma = Lemmas.start_lemma id ~pl:decl kind sigma (EConstr.of_constr termtype) ~hook:(Lemmas.mk_hook (fun _ _ _ -> instance_hook pri global imps ?hook)) in (* spiwack: I don't know what to do with the status here. *) - let pstate = + let lemma = if not (Option.is_empty term) then let init_refine = Tacticals.New.tclTHENLIST [ @@ -391,18 +391,18 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te Tactics.New.reduce_after_refine; ] in - let pstate, _ = Pfedit.by init_refine pstate in - pstate + let lemma, _ = Lemmas.by init_refine lemma in + lemma else - let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in - pstate + let lemma, _ = Lemmas.by (Tactics.auto_intros_tac ids) lemma in + lemma in match tac with | Some tac -> - let pstate, _ = Pfedit.by tac pstate in - pstate + let lemma, _ = Lemmas.by tac lemma in + lemma | None -> - pstate + lemma let do_instance_subst_constructor_and_ty subst k u ctx = let subst = diff --git a/vernac/classes.mli b/vernac/classes.mli index e61935c87a..ace9096469 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -31,8 +31,8 @@ val declare_instance : ?warn:bool -> env -> Evd.evar_map -> val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) -val new_instance_interactive : - ?global:bool (** Not global by default. *) +val new_instance_interactive + : ?global:bool (** Not global by default. *) -> Decl_kinds.polymorphic -> name_decl -> local_binder_expr list @@ -41,10 +41,10 @@ val new_instance_interactive : -> ?tac:unit Proofview.tactic -> ?hook:(GlobRef.t -> unit) -> Hints.hint_info_expr - -> Id.t * Proof_global.t + -> Id.t * Lemmas.t -val new_instance : - ?global:bool (** Not global by default. *) +val new_instance + : ?global:bool (** Not global by default. *) -> Decl_kinds.polymorphic -> name_decl -> local_binder_expr list @@ -55,8 +55,8 @@ val new_instance : -> Hints.hint_info_expr -> Id.t -val new_instance_program : - ?global:bool (** Not global by default. *) +val new_instance_program + : ?global:bool (** Not global by default. *) -> Decl_kinds.polymorphic -> name_decl -> local_binder_expr list diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index fa4860b079..c3575594b6 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -33,7 +33,13 @@ val do_definition (************************************************************************) (** Not used anywhere. *) -val interp_definition : program_mode:bool -> - universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> - constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * - UState.universe_decl * Impargs.manual_implicits +val interp_definition + : program_mode:bool + -> universe_decl_expr option + -> local_binder_expr list + -> polymorphic + -> red_expr option + -> constr_expr + -> constr_expr option + -> Safe_typing.private_constants definition_entry * + Evd.evar_map * UState.universe_decl * Impargs.manual_implicits diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index fd88c6c4ad..3a25cb496c 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -267,10 +267,10 @@ let declare_fixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),p Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in - let pstate = Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint) + let lemma = Lemmas.start_lemma_with_initialization (local,poly,DefinitionBody Fixpoint) evd pl (Some(false,indexes,init_tac)) thms None in declare_fixpoint_notations ntns; - pstate + lemma let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = (* We shortcut the proof process *) @@ -304,11 +304,11 @@ let declare_cofixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes) Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in - let pstate = Lemmas.start_proof_with_initialization + let lemma = Lemmas.start_lemma_with_initialization (Global ImportDefaultBehavior,poly, DefinitionBody CoFixpoint) evd pl (Some(true,[],init_tac)) thms None in declare_cofixpoint_notations ntns; - pstate + lemma let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = (* We shortcut the proof process *) diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index c8d617da5f..a31f3c34e0 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -19,13 +19,13 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint_interactive : - locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t + locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Lemmas.t val do_fixpoint : locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint_interactive : - locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t + locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t val do_cofixpoint : locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 7de6d28560..7e70de4209 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -26,7 +26,6 @@ open Decl_kinds open Declare open Pretyping open Termops -open Namegen open Reductionops open Constrintern open Impargs @@ -46,6 +45,46 @@ let call_hook ?hook ?fix_exn uctx trans l c = 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] *) + +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 + +type proof_terminator = proof_ending -> unit + +let make_terminator f = f +let apply_terminator f = f + +(* Proofs with a save constant function *) +type t = + { proof : Proof_global.t + ; terminator : proof_terminator CEphemeron.key + } + +let pf_map f { proof; terminator} = { proof = f proof; terminator } +let pf_fold f ps = f ps.proof + +let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t) + +let with_proof f { proof; terminator } = + let proof, res = Proof_global.with_proof f proof in + { proof; terminator }, res + +let simple_with_proof f ps = fst @@ with_proof (fun t p -> f t p, ()) ps + +let by tac { proof; terminator } = + let proof, res = Pfedit.by tac proof in + { proof; terminator}, res + +(** Gets the current terminator without checking that the proof has + been completed. Useful for the likes of [Admitted]. *) +let get_terminator ps = CEphemeron.get ps.terminator +let set_terminator hook ps = { ps with terminator = CEphemeron.create hook } + (* Support for mutually proved theorems *) let retrieve_first_recthm uctx = function @@ -203,9 +242,6 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes let default_thm_id = Id.of_string "Unnamed_thm" -let fresh_name_for_anonymous_theorem () = - next_global_ident_away default_thm_id Id.Set.empty - let check_name_freshness locality {CAst.loc;v=id} : unit = (* We check existence here: it's a bit late at Qed time *) if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || @@ -265,7 +301,6 @@ let check_anonymity id save_ident = 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 ++ @@ -312,7 +347,41 @@ let initialize_named_context_for_proof () = let d = if variable_opacity id then NamedDecl.drop_body d else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val -let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c = +module Stack = struct + + type lemma = t + type nonrec t = t * t list + + let map f (pf, pfl) = (f pf, List.map f pfl) + + let map_top ~f (pf, pfl) = (f pf, pfl) + let map_top_pstate ~f (pf, pfl) = (pf_map f pf, pfl) + + let pop (ps, p) = match p with + | [] -> ps, None + | pp :: p -> ps, Some (pp, p) + + let with_top (p, _) ~f = f p + let with_top_pstate (p, _) ~f = f p.proof + + let push ontop a = + match ontop with + | None -> a , [] + | Some (l,ls) -> a, (l :: ls) + + let get_all_proof_names (pf : t) = + let prj x = Proof_global.get_proof x in + let (pn, pns) = map Proof.(function pf -> (data (prj pf.proof)).name) pf in + pn :: pns + + let copy_terminators ~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 + +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 @@ -323,7 +392,18 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c | None -> initialize_named_context_for_proof () in let goals = [ Global.env_of_context sign , c ] in - Proof_global.start_proof sigma id ?pl kind goals terminator + let proof = Proof_global.start_proof sigma id ?pl kind goals in + let terminator = CEphemeron.create terminator in + { proof ; terminator } + +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 + in + let proof = Proof_global.start_dependent_proof id ?pl kind telescope in + let terminator = CEphemeron.create terminator in + { proof ; terminator } let rec_tac_initializer finite guard thms snl = if finite then @@ -339,7 +419,7 @@ let rec_tac_initializer finite guard thms snl = | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false -let start_proof_with_initialization ?hook kind sigma decl recguard thms snl = +let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl = let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in let init_tac,guard = match recguard with | Some (finite,guard,init_tac) -> @@ -371,14 +451,14 @@ let start_proof_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 pstate = start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard in - let pstate = Proof_global.modify_proof (fun p -> + let lemma = start_lemma id ~pl:decl kind sigma t ~hook ~compute_guard:guard in + let lemma = simple_with_proof (fun _ p -> match init_tac with | None -> p - | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in - pstate + | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) lemma in + lemma -let start_proof_com ~program_mode ?inference_hook ?hook kind thms = +let start_lemma_com ~program_mode ?inference_hook ?hook kind thms = let env0 = Global.env () in let decl = fst (List.hd thms) in let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in @@ -410,7 +490,7 @@ let start_proof_com ~program_mode ?inference_hook ?hook kind thms = else (* We fix the variables to ensure they won't be lowered to Set *) Evd.fix_undefined_variables evd in - start_proof_with_initialization ?hook kind evd decl recguard thms snl + start_lemma_with_initialization ?hook kind evd decl recguard thms snl (* Saving a proof *) @@ -425,7 +505,7 @@ let () = optread = (fun () -> !keep_admitted_vars); optwrite = (fun b -> keep_admitted_vars := b) } -let save_proof_admitted ?proof ~pstate = +let save_lemma_admitted ?proof ~(lemma : t) = let pe = let open Proof_global in match proof with @@ -440,8 +520,8 @@ let save_proof_admitted ?proof ~pstate = let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in Admitted(id, k, (sec_vars, (typ, ctx), None), universes) | None -> - let pftree = Proof_global.give_me_the_proof pstate in - let gk = Proof_global.get_current_persistence pstate in + let pftree = Proof_global.get_proof lemma.proof in + let gk = Proof_global.get_persistence lemma.proof in let Proof.{ name; poly; entry } = Proof.data pftree in let typ = match Proofview.initial_goals entry with | [typ] -> snd typ @@ -453,10 +533,10 @@ let save_proof_admitted ?proof ~pstate = let universes = Proof.((data pftree).initial_euctx) in (* This will warn if the proof is complete *) let pproofs, _univs = - Proof_global.return_proof ~allow_partial:true pstate in + Proof_global.return_proof ~allow_partial:true lemma.proof in let sec_vars = if not !keep_admitted_vars then None - else match Proof_global.get_used_variables pstate, pproofs with + else match Proof_global.get_used_variables lemma.proof, pproofs with | Some _ as x, _ -> x | None, (pproof, _) :: _ -> let env = Global.env () in @@ -464,32 +544,23 @@ let save_proof_admitted ?proof ~pstate = let ids_def = Environ.global_vars_set env pproof in Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) | _ -> None in - let decl = Proof_global.get_universe_decl pstate 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) in - Proof_global.apply_terminator (Proof_global.get_terminator pstate) pe - -let save_pstate_proved ~pstate ~opaque ~idopt = - let obj, terminator = Proof_global.close_proof ~opaque - ~keep_body_ucst_separate:false (fun x -> x) pstate - in - Proof_global.(apply_terminator terminator (Proved (opaque, idopt, obj))) + CEphemeron.get lemma.terminator pe -let save_proof_proved ?proof ?ontop ~opaque ~idopt = +let save_lemma_proved ?proof ?lemma ~opaque ~idopt = (* Invariant (uh) *) - if Option.is_empty ontop && Option.is_empty proof then + 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) = 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 pstate = Proof_global.get_current_pstate @@ Option.get ontop in - Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) pstate + let { proof; terminator } = Option.get lemma in + Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, CEphemeron.get terminator | Some proof -> proof in - (* if the proof is given explicitly, nothing has to be deleted *) - let ontop = if Option.is_empty proof then Proof_global.discard_current Option.(get ontop) else ontop in - Proof_global.(apply_terminator terminator (Proved (opaque,idopt,proof_obj))); - ontop + terminator (Proved (opaque,idopt,proof_obj)) diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 3df543156d..2c51095786 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -11,6 +11,7 @@ open Names open Decl_kinds +(* Declaration hooks *) type declaration_hook (* Hooks allow users of the API to perform arbitrary actions at @@ -37,53 +38,118 @@ val call_hook -> ?fix_exn:Future.fix_exn -> hook_type -val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> - ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator) -> - ?sign:Environ.named_context_val -> - ?compute_guard:Proof_global.lemma_possible_guards -> - ?hook:declaration_hook -> EConstr.types -> Proof_global.t +(* Proofs that define a constant + terminators *) +type t +type proof_terminator -val start_proof_com +module Stack : sig + + type lemma = t + type t + + val pop : t -> lemma * t option + val push : t option -> lemma -> t + + val map_top : f:(lemma -> lemma) -> t -> t + val map_top_pstate : f:(Proof_global.t -> Proof_global.t) -> t -> t + + val with_top : t -> f:(lemma -> 'a ) -> 'a + val with_top_pstate : t -> f:(Proof_global.t -> 'a ) -> 'a + + 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]. *) + +end + +val standard_proof_terminator + : ?hook:declaration_hook + -> Proof_global.lemma_possible_guards + -> proof_terminator + +val set_endline_tactic : Genarg.glob_generic_argument -> t -> t +val pf_fold : (Proof_global.t -> 'a) -> t -> 'a + +val by : unit Proofview.tactic -> t -> t * bool + +val with_proof : + (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a + +val simple_with_proof : + (unit Proofview.tactic -> Proof.t -> Proof.t) -> t -> t + +(* Start of high-level proofs with an associated constant *) + +val start_lemma + : Id.t + -> ?pl:UState.universe_decl + -> goal_kind + -> Evd.evar_map + -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> proof_terminator) + -> ?sign:Environ.named_context_val + -> ?compute_guard:Proof_global.lemma_possible_guards + -> ?hook:declaration_hook + -> EConstr.types + -> t + +val start_dependent_lemma + : Id.t + -> ?pl:UState.universe_decl + -> goal_kind + -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> proof_terminator) + -> ?sign:Environ.named_context_val + -> ?compute_guard:Proof_global.lemma_possible_guards + -> ?hook:declaration_hook + -> Proofview.telescope + -> t + +val start_lemma_com : program_mode:bool -> ?inference_hook:Pretyping.inference_hook -> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list - -> Proof_global.t - -val start_proof_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 -> - (Id.t (* name of thm *) * - (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list - -> int list option -> Proof_global.t + -> t -val standard_proof_terminator : - ?hook:declaration_hook -> Proof_global.lemma_possible_guards -> - Proof_global.proof_terminator +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 + -> (Id.t (* name of thm *) * + (EConstr.types (* type of thm *) * + (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list + -> int list option + -> t -val fresh_name_for_anonymous_theorem : unit -> Id.t +val default_thm_id : Names.Id.t (* Prepare global named context for proof session: remove proofs of opaque section definitions and remove vm-compiled code *) val initialize_named_context_for_proof : unit -> Environ.named_context_val -(** {6 ... } *) +(** {6 Saving proofs } *) -val save_proof_admitted - : ?proof:Proof_global.closed_proof - -> pstate:Proof_global.t +val save_lemma_admitted + : ?proof:(Proof_global.proof_object * proof_terminator) + -> lemma:t -> unit -val save_proof_proved - : ?proof:Proof_global.closed_proof - -> ?ontop:Proof_global.stack - -> opaque:Proof_global.opacity_flag - -> idopt:Names.lident option - -> Proof_global.stack option - -val save_pstate_proved - : pstate:Proof_global.t +val save_lemma_proved + : ?proof:(Proof_global.proof_object * proof_terminator) + -> ?lemma:t -> opaque:Proof_global.opacity_flag -> 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 + | Proved of Proof_global.opacity_flag * + Names.lident option * + Proof_global.proof_object + +val make_terminator : (proof_ending -> unit) -> proof_terminator +val apply_terminator : proof_terminator -> proof_ending -> unit +val get_terminator : t -> proof_terminator +val set_terminator : proof_terminator -> t -> t diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 36cf9e0a31..f1286e2f1f 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -841,7 +841,8 @@ let solve_by_tac ?loc name evi t poly ctx = let obligation_terminator ?hook name num guard auto pf = let open Proof_global in - let term = Lemmas.standard_proof_terminator ?hook guard in + let open Lemmas in + let term = standard_proof_terminator ?hook guard in match pf with | Admitted _ -> apply_terminator term pf | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin @@ -964,13 +965,13 @@ let rec solve_obligation prg num tac = 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 = - Proof_global.make_terminator + Lemmas.make_terminator (obligation_terminator prg.prg_name num guard ?hook auto) in let hook = Lemmas.mk_hook (obligation_hook prg obl num auto) in - let pstate = Lemmas.start_proof ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook in - let pstate = fst @@ Pfedit.by !default_tactic pstate in - let pstate = Option.cata (fun tac -> Proof_global.set_endline_tactic tac pstate) pstate tac in - pstate + 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 + lemma and obligation (user_num, name, typ) tac = let num = pred user_num in diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 3b77039de5..8734d82970 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -86,14 +86,14 @@ val add_mutual_definitions : fixpoint_kind -> unit val obligation - : int * Names.Id.t option * Constrexpr.constr_expr option + : int * Names.Id.t option * Constrexpr.constr_expr option -> Genarg.glob_generic_argument option - -> Proof_global.t + -> Lemmas.t val next_obligation - : Names.Id.t option + : Names.Id.t option -> Genarg.glob_generic_argument option - -> Proof_global.t + -> Lemmas.t val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress (* Number of remaining obligations to be solved for this program *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4f66f2b790..643d8ce1d6 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -38,28 +38,24 @@ module NamedDecl = Context.Named.Declaration let (f_interp_redexp, interp_redexp_hook) = Hook.make () let debug = false + (* XXX Should move to a common library *) let vernac_pperr_endline pp = if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else () -(* Misc *) - -let there_are_pending_proofs ~pstate = - not Option.(is_empty pstate) +(* Utility functions, at some point they should all disappear and + instead enviroment/state selection should be done at the Vernac DSL + level. *) -(* EJGA: Only used in close_proof 2, can remove once ?proof hack is away *) -let vernac_require_open_proof ~pstate f = - match pstate with - | Some pstate -> f ~pstate +(* EJGA: Only used in close_proof, can remove once the ?proof hack is no more *) +let vernac_require_open_lemma ~stack f = + match stack with + | Some stack -> f ~stack | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)") -let with_pstate ~pstate f = - vernac_require_open_proof ~pstate - (fun ~pstate -> f ~pstate:(Proof_global.get_current_pstate pstate)) - - let modify_pstate ~pstate f = - vernac_require_open_proof ~pstate (fun ~pstate -> - Some (Proof_global.modify_current_pstate (fun pstate -> f ~pstate) pstate)) +let with_pstate ~stack f = + vernac_require_open_lemma ~stack + (fun ~stack -> Stack.with_top_pstate stack ~f:(fun pstate -> f ~pstate)) let get_current_or_global_context ~pstate = match pstate with @@ -122,7 +118,7 @@ let show_proof ~pstate = (* spiwack: this would probably be cooler with a bit of polishing. *) try let pstate = Option.get pstate in - let p = Proof_global.give_me_the_proof pstate in + let p = Proof_global.get_proof pstate in let sigma, env = Pfedit.get_current_context pstate in let pprf = Proof.partial_proof p in Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf @@ -132,24 +128,21 @@ let show_proof ~pstate = | Option.IsNone -> user_err (str "No goals to show.") -let show_top_evars ~pstate = +let show_top_evars ~proof = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) - let pfts = Proof_global.give_me_the_proof pstate in - let Proof.{goals;shelf;given_up;sigma} = Proof.data pfts in + let Proof.{goals;shelf;given_up;sigma} = Proof.data proof in pr_evars_int sigma ~shelf ~given_up 1 (Evd.undefined_map sigma) -let show_universes ~pstate = - let pfts = Proof_global.give_me_the_proof pstate in - let Proof.{goals;sigma} = Proof.data pfts in +let show_universes ~proof = + let Proof.{goals;sigma} = Proof.data proof in let ctx = Evd.universe_context_set (Evd.minimize_universes sigma) in Termops.pr_evar_universe_context (Evd.evar_universe_context sigma) ++ fnl () ++ str "Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx (* Simulate the Intro(s) tactic *) -let show_intro ~pstate all = +let show_intro ~proof all = let open EConstr in - let pf = Proof_global.give_me_the_proof pstate in - let Proof.{goals;sigma} = Proof.data pf in + let Proof.{goals;sigma} = Proof.data proof in if not (List.is_empty goals) then begin let gl = {Evd.it=List.hd goals ; sigma = sigma; } in let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in @@ -586,7 +579,7 @@ let start_proof_and_print ~program_mode ?hook k l = in Some hook else None in - start_proof_com ~program_mode ?inference_hook ?hook k l + start_lemma_com ~program_mode ?inference_hook ?hook k l let vernac_definition_hook p = function | Coercion -> @@ -597,6 +590,9 @@ let vernac_definition_hook p = function Some (Class.add_subclass_hook p) | _ -> None +let fresh_name_for_anonymous_theorem () = + Namegen.next_global_ident_away Lemmas.default_thm_id Id.Set.empty + let vernac_definition_name lid local = let lid = match lid with @@ -641,18 +637,27 @@ let vernac_start_proof ~atts kind l = List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l -let vernac_end_proof ?pstate:ontop ?proof = function +let vernac_end_proof ?stack ?proof = let open Vernacexpr in function | Admitted -> - with_pstate ~pstate:ontop (save_proof_admitted ?proof); - ontop + vernac_require_open_lemma ~stack (fun ~stack -> + let lemma, stack = Stack.pop stack in + save_lemma_admitted ?proof ~lemma; + stack) | Proved (opaque,idopt) -> - save_proof_proved ?ontop ?proof ~opaque ~idopt + let lemma, stack = match stack with + | None -> None, None + | Some stack -> + let lemma, stack = Stack.pop stack in + Some lemma, stack + in + save_lemma_proved ?lemma ?proof ~opaque ~idopt; + stack -let vernac_exact_proof ~pstate c = +let vernac_exact_proof ~lemma c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the beginning of a proof. *) - let pstate, status = Pfedit.by (Tactics.exact_proof c) pstate in - let () = save_pstate_proved ~pstate ~opaque:Proof_global.Opaque ~idopt:None in + let lemma, status = Lemmas.by (Tactics.exact_proof c) lemma in + let () = save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Opaque ~idopt:None in if not status then Feedback.feedback Feedback.AddedAxiom let vernac_assumption ~atts discharge kind l nl = @@ -1167,15 +1172,14 @@ let vernac_set_end_tac ~pstate tac = (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) Proof_global.set_endline_tactic tac pstate -let vernac_set_used_variables ~(pstate : Proof_global.t) e : Proof_global.t = +let vernac_set_used_variables ~pstate e : Proof_global.t = let env = Global.env () in let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in - let tys = - List.map snd (initial_goals (Proof_global.give_me_the_proof pstate)) in + let tys = List.map snd (initial_goals (Proof_global.get_proof pstate)) in let tys = List.map EConstr.Unsafe.to_constr tys in let l = Proof_using.process_expr env e tys in let vars = Environ.named_context env in - List.iter (fun id -> + List.iter (fun id -> if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then user_err ~hdr:"vernac_set_used_variables" (str "Unknown variable: " ++ Id.print id)) @@ -1878,10 +1882,10 @@ let get_current_context_of_args ~pstate = match pstate with | None -> fun _ -> let env = Global.env () in Evd.(from_env env, env) - | Some pstate -> + | Some lemma -> function - | Some n -> Pfedit.get_goal_context pstate n - | None -> Pfedit.get_current_context pstate + | Some n -> Pfedit.get_goal_context lemma n + | None -> Pfedit.get_current_context lemma let query_command_selector ?loc = function | None -> None @@ -1946,7 +1950,7 @@ let vernac_global_check c = let get_nth_goal ~pstate n = - let pf = Proof_global.give_me_the_proof pstate in + let pf = Proof_global.get_proof pstate in let Proof.{goals;sigma} = Proof.data pf in let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in gl @@ -2022,9 +2026,9 @@ let vernac_print ~pstate ~atts = | PrintHintGoal -> begin match pstate with | Some pstate -> - Hints.pr_applicable_hint pstate + Hints.pr_applicable_hint pstate | None -> - str "No proof in progress" + str "No proof in progress" end | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s | PrintHintDb -> Hints.pr_searchtable env sigma @@ -2193,13 +2197,12 @@ let vernac_unfocus ~pstate = (* Checks that a proof is fully unfocused. Raises an error if not. *) let vernac_unfocused ~pstate = - let p = Proof_global.give_me_the_proof pstate in + let p = Proof_global.get_proof pstate in if Proof.unfocused p then str"The proof is indeed fully unfocused." else user_err Pp.(str "The proof is not fully unfocused.") - (* "{" focuses on the first goal, "n: {" focuses on the n-th goal "}" unfocuses, provided that the proof of the goal has been completed. *) @@ -2239,25 +2242,26 @@ let vernac_show ~pstate = end (* Show functions that require a proof state *) | Some pstate -> + let proof = Proof_global.get_proof pstate in begin function | ShowGoal goalref -> - let proof = Proof_global.give_me_the_proof pstate in begin match goalref with | OpenSubgoals -> pr_open_subgoals ~proof | NthGoal n -> pr_nth_open_subgoal ~proof n | GoalId id -> pr_goal_by_id ~proof id end - | ShowExistentials -> show_top_evars ~pstate - | ShowUniverses -> show_universes ~pstate + | ShowExistentials -> show_top_evars ~proof + | ShowUniverses -> show_universes ~proof + (* Deprecate *) | ShowProofNames -> - Id.print (Proof_global.get_current_proof_name pstate) - | ShowIntros all -> show_intro ~pstate all + Id.print (Proof_global.get_proof_name pstate) + | ShowIntros all -> show_intro ~proof all | ShowProof -> show_proof ~pstate:(Some pstate) | ShowMatch id -> show_match id end let vernac_check_guard ~pstate = - let pts = Proof_global.give_me_the_proof pstate in + let pts = Proof_global.get_proof pstate in let pfterm = List.hd (Proof.partial_proof pts) in let message = try @@ -2322,30 +2326,31 @@ let locate_if_not_already ?loc (e, info) = exception End_of_input -let interp_typed_vernac c ~pstate = - let open Proof_global in +let interp_typed_vernac c ~stack = let open Vernacextend in match c with - | VtDefault f -> f (); pstate + | VtDefault f -> f (); stack | VtNoProof f -> - if there_are_pending_proofs ~pstate then + if Option.has_some stack then user_err Pp.(str "Command not supported (Open proofs remain)"); let () = f () in - pstate + stack | VtCloseProof f -> - vernac_require_open_proof ~pstate (fun ~pstate -> - f ~pstate:(Proof_global.get_current_pstate pstate); - Proof_global.discard_current pstate) + vernac_require_open_lemma ~stack (fun ~stack -> + let lemma, stack = Stack.pop stack in + f ~lemma; + stack) | VtOpenProof f -> - Some (push ~ontop:pstate (f ())) + Some (Stack.push stack (f ())) | VtModifyProof f -> - modify_pstate f ~pstate + Option.map (Stack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack | VtReadProofOpt f -> - f ~pstate:(Option.map get_current_pstate pstate); - pstate + let pstate = Option.map (Stack.with_top_pstate ~f:(fun x -> x)) stack in + f ~pstate; + stack | VtReadProof f -> - with_pstate ~pstate f; - pstate + with_pstate ~stack f; + stack (* We interpret vernacular commands to a DSL that specifies their allowed actions on proof states *) @@ -2398,9 +2403,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with | VernacStartTheoremProof (k,l) -> VtOpenProof(fun () -> with_def_attributes ~atts vernac_start_proof k l) | VernacExactProof c -> - VtCloseProof(fun ~pstate -> + VtCloseProof (fun ~lemma -> unsupported_attributes atts; - vernac_exact_proof ~pstate c) + vernac_exact_proof ~lemma c) | VernacDefineModule (export,lid,bl,mtys,mexprl) -> let i () = @@ -2671,7 +2676,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with * still parsed as the obsolete_locality grammar entry for retrocompatibility. * loc is the Loc.t of the vernacular command being interpreted. *) let rec interp_expr ?proof ~atts ~st c = - let pstate = st.Vernacstate.proof in + let stack = st.Vernacstate.lemmas in vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); match c with @@ -2699,11 +2704,11 @@ let rec interp_expr ?proof ~atts ~st c = (* Special: ?proof parameter doesn't allow for uniform pstate pop :S *) | VernacEndProof e -> unsupported_attributes atts; - vernac_end_proof ?proof ?pstate e + vernac_end_proof ?proof ?stack e | v -> let fv = translate_vernac ~atts v in - interp_typed_vernac ~pstate fv + interp_typed_vernac ~stack fv (* XXX: This won't properly set the proof mode, as of today, it is controlled by the STM. Thus, we would need access information from @@ -2712,8 +2717,9 @@ let rec interp_expr ?proof ~atts ~st c = without a considerable amount of refactoring. *) and vernac_load ~verbosely ~st fname = - let pstate = st.Vernacstate.proof in - if there_are_pending_proofs ~pstate then + let there_are_pending_proofs ~stack = not Option.(is_empty stack) in + let stack = st.Vernacstate.lemmas in + if there_are_pending_proofs ~stack then CErrors.user_err Pp.(str "Load is not supported inside proofs."); (* Open the file *) let fname = @@ -2730,29 +2736,29 @@ and vernac_load ~verbosely ~st fname = match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with | Some x -> x | None -> raise End_of_input) in - let rec load_loop ~pstate = + let rec load_loop ~stack = try - let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) pstate in - let pstate = - v_mod (interp_control ?proof:None ~st:{ st with Vernacstate.proof = pstate }) + let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in + let stack = + v_mod (interp_control ?proof:None ~st:{ st with Vernacstate.lemmas = stack }) (parse_sentence proof_mode input) in - load_loop ~pstate + load_loop ~stack with End_of_input -> - pstate + stack in - let pstate = load_loop ~pstate in + let stack = load_loop ~stack in (* If Load left a proof open, we fail too. *) - if there_are_pending_proofs ~pstate then + if there_are_pending_proofs ~stack then CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); - pstate + stack and interp_control ?proof ~st v = match v with | { v=VernacExpr (atts, cmd) } -> interp_expr ?proof ~atts ~st cmd | { v=VernacFail v } -> with_fail ~st (fun () -> interp_control ?proof ~st v); - st.Vernacstate.proof + st.Vernacstate.lemmas | { v=VernacTimeout (timeout,v) } -> vernac_timeout ~timeout (interp_control ?proof ~st) v | { v=VernacRedirect (s, v) } -> @@ -2774,8 +2780,8 @@ let interp ?(verbosely=true) ?proof ~st cmd = Vernacstate.unfreeze_interp_state st; try vernac_timeout (fun st -> let v_mod = if verbosely then Flags.verbosely else Flags.silently in - let pstate = v_mod (interp_control ?proof ~st) cmd in - Vernacstate.Proof_global.set pstate [@ocaml.warning "-3"]; + let ontop = v_mod (interp_control ?proof ~st) cmd in + Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"]; Vernacstate.freeze_interp_state ~marshallable:false ) st with exn -> diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index d94ddc1aaf..f1c8b29313 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.closed_proof -> + ?proof:(Proof_global.proof_object * Lemmas.proof_terminator) -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t (** Prepare a "match" template for a given inductive type. @@ -41,13 +41,6 @@ val command_focus : unit Proof.focus_kind val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t -(** Helper *) -val vernac_require_open_proof : pstate:Proof_global.stack option -> (pstate:Proof_global.stack -> 'a) -> 'a - -val with_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.t -> 'a) -> 'a - -val modify_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.t -> Proof_global.t) -> Proof_global.stack option - (* Flag set when the test-suite is called. Its only effect to display verbose information for `Fail` *) val test_mode : bool ref diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 6f8a4e8a3c..6a52177dd5 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -55,9 +55,10 @@ type vernac_classification = vernac_type * vernac_when type typed_vernac = | VtDefault of (unit -> unit) + | VtNoProof of (unit -> unit) - | VtCloseProof of (pstate:Proof_global.t -> unit) - | VtOpenProof of (unit -> Proof_global.t) + | VtCloseProof of (lemma:Lemmas.t -> unit) + | VtOpenProof of (unit -> Lemmas.t) | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t) | VtReadProofOpt of (pstate:Proof_global.t option -> unit) | VtReadProof of (pstate:Proof_global.t -> unit) diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 60e371a6d9..78b7f21b0d 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -74,8 +74,8 @@ type vernac_classification = vernac_type * vernac_when type typed_vernac = | VtDefault of (unit -> unit) | VtNoProof of (unit -> unit) - | VtCloseProof of (pstate:Proof_global.t -> unit) - | VtOpenProof of (unit -> Proof_global.t) + | VtCloseProof of (lemma:Lemmas.t -> unit) + | VtOpenProof of (unit -> Lemmas.t) | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t) | VtReadProofOpt of (pstate:Proof_global.t option -> unit) | VtReadProof of (pstate:Proof_global.t -> unit) diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 0fbde1ade5..90075cbb70 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -30,18 +30,16 @@ end type t = { parsing : Parser.state; system : States.state; (* summary + libstack *) - proof : Proof_global.stack option; (* proof state *) + lemmas : Lemmas.Stack.t option; (* proofs of lemmas currently opened *) shallow : bool (* is the state trimmed down (libstack) *) } -let pstate st = Option.map Proof_global.get_current_pstate st.proof - let s_cache = ref None -let s_proof = ref None +let s_lemmas = ref None let invalidate_cache () = s_cache := None; - s_proof := None + s_lemmas := None let update_cache rf v = rf := Some v; v @@ -57,14 +55,14 @@ let do_if_not_cached rf f v = let freeze_interp_state ~marshallable = { system = update_cache s_cache (States.freeze ~marshallable); - proof = !s_proof; + lemmas = !s_lemmas; shallow = false; parsing = Parser.cur_state (); } -let unfreeze_interp_state { system; proof; parsing } = +let unfreeze_interp_state { system; lemmas; parsing } = do_if_not_cached s_cache States.unfreeze system; - s_proof := proof; + s_lemmas := lemmas; Pcoq.unfreeze parsing let make_shallow st = @@ -77,11 +75,16 @@ let make_shallow st = (* Compatibility module *) module Proof_global = struct - let get () = !s_proof - let set x = s_proof := x + type t = Lemmas.Stack.t + + let get () = !s_lemmas + let set x = s_lemmas := x + + let get_pstate () = + Option.map (Lemmas.Stack.with_top ~f:(Lemmas.pf_fold (fun x -> x))) !s_lemmas let freeze ~marshallable:_ = get () - let unfreeze x = s_proof := Some x + let unfreeze x = s_lemmas := Some x exception NoCurrentProof @@ -92,53 +95,67 @@ module Proof_global = struct | _ -> raise CErrors.Unhandled end + open Lemmas open Proof_global - let cc f = match !s_proof with + let cc f = match !s_lemmas with | None -> raise NoCurrentProof - | Some x -> f x + | Some x -> Stack.with_top_pstate ~f x - let cc1 f = cc (fun p -> f (Proof_global.get_current_pstate p)) + let cc_lemma f = match !s_lemmas with + | None -> raise NoCurrentProof + | Some x -> Stack.with_top ~f x - let dd f = match !s_proof with + let cc_stack f = match !s_lemmas with | None -> raise NoCurrentProof - | Some x -> s_proof := Some (f x) + | Some x -> f x - let dd1 f = dd (fun p -> Proof_global.modify_current_pstate f p) + let dd f = match !s_lemmas with + | None -> raise NoCurrentProof + | Some x -> s_lemmas := Some (Stack.map_top_pstate ~f x) - let there_are_pending_proofs () = !s_proof <> None - let get_open_goals () = cc1 get_open_goals + let dd_lemma f = match !s_lemmas with + | None -> raise NoCurrentProof + | Some x -> s_lemmas := Some (Stack.map_top ~f x) - let set_terminator x = dd1 (set_terminator x) - let give_me_the_proof_opt () = Option.map (fun p -> give_me_the_proof (Proof_global.get_current_pstate p)) !s_proof - let give_me_the_proof () = cc1 give_me_the_proof - let get_current_proof_name () = cc1 get_current_proof_name + let there_are_pending_proofs () = !s_lemmas <> None + let get_open_goals () = cc get_open_goals - let simple_with_current_proof f = - dd (simple_with_current_proof f) + let set_terminator x = dd_lemma (set_terminator x) + let give_me_the_proof_opt () = Option.map (Stack.with_top_pstate ~f:get_proof) !s_lemmas + let give_me_the_proof () = cc get_proof + let get_current_proof_name () = cc get_proof_name + let simple_with_current_proof f = dd (Proof_global.simple_with_proof f) let with_current_proof f = - let pf, res = cc (with_current_proof f) in - s_proof := Some pf; res + match !s_lemmas with + | None -> raise NoCurrentProof + | Some stack -> + let pf, res = Stack.with_top_pstate stack ~f:(with_proof f) in + let stack = Stack.map_top_pstate stack ~f:(fun _ -> pf) in + s_lemmas := Some stack; + res + + type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator - let install_state s = s_proof := Some s - let return_proof ?allow_partial () = - cc1 (return_proof ?allow_partial) + let return_proof ?allow_partial () = cc (return_proof ?allow_partial) let close_future_proof ~opaque ~feedback_id pf = - cc1 (fun st -> close_future_proof ~opaque ~feedback_id st pf) + cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt, + get_terminator pt) let close_proof ~opaque ~keep_body_ucst_separate f = - cc1 (close_proof ~opaque ~keep_body_ucst_separate f) + cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate f)) pt, + get_terminator pt) - let discard_all () = s_proof := None - let update_global_env () = dd1 update_global_env + let discard_all () = s_lemmas := None + let update_global_env () = dd (update_global_env) - let get_current_context () = cc1 Pfedit.get_current_context + let get_current_context () = cc Pfedit.get_current_context let get_all_proof_names () = - try cc get_all_proof_names + try cc_stack Lemmas.Stack.get_all_proof_names with NoCurrentProof -> [] let copy_terminators ~src ~tgt = @@ -146,6 +163,6 @@ module Proof_global = struct | None, None -> None | Some _ , None -> None | None, Some x -> Some x - | Some src, Some tgt -> Some (copy_terminators ~src ~tgt) + | Some src, Some tgt -> Some (Stack.copy_terminators ~src ~tgt) end diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index b0f3c572e5..1bb18116b5 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -18,14 +18,12 @@ module Parser : sig end -type t = { - parsing : Parser.state; - system : States.state; (* summary + libstack *) - proof : Proof_global.stack option; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) -} - -val pstate : t -> Proof_global.t option +type t = + { parsing : Parser.state + ; system : States.state (* summary + libstack *) + ; lemmas : Lemmas.Stack.t option (* proofs of lemmas currently opened *) + ; shallow : bool (* is the state trimmed down (libstack) *) + } val freeze_interp_state : marshallable:bool -> t val unfreeze_interp_state : t -> unit @@ -38,21 +36,12 @@ val invalidate_cache : unit -> unit (* Compatibility module: Do Not Use *) module Proof_global : sig - open Proof_global - - (* Low-level stuff *) - val get : unit -> stack option - val set : stack option -> unit - - val freeze : marshallable:bool -> stack option - val unfreeze : stack -> unit - exception NoCurrentProof val there_are_pending_proofs : unit -> bool val get_open_goals : unit -> int - val set_terminator : proof_terminator -> unit + val set_terminator : Lemmas.proof_terminator -> unit val give_me_the_proof : unit -> Proof.t val give_me_the_proof_opt : unit -> Proof.t option val get_current_proof_name : unit -> Names.Id.t @@ -63,16 +52,17 @@ module Proof_global : sig val with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a - val install_state : stack -> unit - val return_proof : ?allow_partial:bool -> unit -> closed_proof_output + val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output + + type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator val close_future_proof : - opaque:opacity_flag -> + opaque:Proof_global.opacity_flag -> feedback_id:Stateid.t -> - closed_proof_output Future.computation -> closed_proof + Proof_global.closed_proof_output Future.computation -> closed_proof - val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof + val close_proof : opaque:Proof_global.opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof val discard_all : unit -> unit val update_global_env : unit -> unit @@ -81,7 +71,19 @@ module Proof_global : sig val get_all_proof_names : unit -> Names.Id.t list - val copy_terminators : src:stack option -> tgt:stack option -> stack option + val copy_terminators : src:Lemmas.Stack.t option -> tgt:Lemmas.Stack.t option -> Lemmas.Stack.t option + + (* Handling of the imperative state *) + type t = Lemmas.Stack.t + + (* Low-level stuff *) + val get : unit -> t option + val set : t option -> unit + + val get_pstate : unit -> Proof_global.t option + + val freeze : marshallable:bool -> t option + val unfreeze : t -> unit end [@@ocaml.deprecated "This module is internal and should not be used, instead, thread the proof state"] |