diff options
| author | Gaëtan Gilbert | 2019-05-02 19:46:02 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:42 +0200 |
| commit | 8abacf00c6c39ec98085d531737d18edc9c19b2a (patch) | |
| tree | 52127cb4b3909e94e53996cd9e170de1f2ea6726 | |
| parent | 1c228b648cb1755cad3ec1f38690110d6fe14bc5 (diff) | |
Proof_global: pass only 1 pstate when we don't want the proof stack
Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.
Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).
We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.
Behaviour should be similar modulo bugs, let's see what CI says.
41 files changed, 385 insertions, 315 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 75251d8e33..147b0df567 100644 --- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -146,11 +146,12 @@ END VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY | ![ proof ] [ "Cmd9" ] -> - { fun ~pstate -> - Option.iter (fun (pstate : Proof_global.t) -> + { fun ~pstate:ontop -> + Option.iter (fun ontop -> + let pstate = Proof_global.get_current_pstate ontop in let sigma, env = Pfedit.get_current_context pstate in let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in Feedback.msg_notice - (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) pstate; - pstate } + (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) ontop; + ontop } END diff --git a/ide/idetop.ml b/ide/idetop.ml index 970d7cf650..90bd2f314d 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -340,6 +340,7 @@ let import_search_constraint = function let search flags = let pstate = Vernacstate.Proof_global.get () in + let pstate = Option.map Proof_global.get_current_pstate 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 4769c2dc53..9c1882dc9a 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -101,8 +101,8 @@ let start_deriving f suchthat lemma = in let terminator = Proof_global.make_terminator terminator in - let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in - Proof_global.simple_with_current_proof begin fun _ p -> + 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 diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 6bb923118e..6e4bffa0b6 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -12,4 +12,4 @@ (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 -> Proof_global.pstate diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index 214a9d8bb5..ee076f5ae3 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 } | ![ proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - { fun ~pstate -> Some Derive.(start_deriving f suchthat lemma) } + { fun ~pstate -> Some (Proof_global.push ~ontop:pstate Derive.(start_deriving f suchthat lemma)) } END diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 8f17f7b2dd..c5439ffaf6 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -751,10 +751,6 @@ let extract_and_compile l = (* Show the extraction of the current ongoing proof *) let show_extraction ~pstate = - let pstate = match pstate with - | None -> CErrors.user_err Pp.(str "No ongoing proof") - | Some pstate -> pstate - in init ~inner:true false false; let prf = Proof_global.give_me_the_proof pstate in let sigma, env = Pfedit.get_current_context pstate in diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 7ba7e05019..efd5b5575f 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -40,4 +40,4 @@ val structure_for_compute : (* Show the extraction of the current ongoing proof *) -val show_extraction : pstate:Proof_global.t option -> unit +val show_extraction : pstate:Proof_global.pstate -> unit diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index db1a389fe7..d43d90af60 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -179,5 +179,11 @@ END VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY | ![ proof ] [ "Show" "Extraction" ] - -> { fun ~pstate -> let () = show_extraction ~pstate in pstate } + -> { fun ~pstate:ontop -> + let pstate = Option.map Proof_global.get_current_pstate ontop in + let pstate = match pstate with + | None -> CErrors.user_err Pp.(str "No ongoing proof") + | Some pstate -> pstate + in + let () = show_extraction ~pstate in ontop } END diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f2b9ba2ec6..e38ea992ab 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 ~ontop:None + let pstate = Lemmas.start_proof (*i The next call to mk_equation_id is valid since we are constructing the lemma Ensures by: obvious i*) @@ -1000,8 +1000,9 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num lemma_type in let pstate,_ = Pfedit.by (Proofview.V82.tactic prove_replacement) pstate in - let pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in - pstate, evd + let ontop = Proof_global.push ~ontop:None pstate in + ignore(Lemmas.save_proof_proved ?proof:None ~ontop ~opaque:Proof_global.Transparent ~idopt:None); + evd let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g = @@ -1015,7 +1016,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a Ensures by: obvious i*) let equation_lemma_id = (mk_equation_id f_id) in - evd := snd @@ generate_equation_lemma !evd all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num; + evd := generate_equation_lemma !evd all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num; let _ = match e with | Option.IsNone -> diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 2c107d39d9..7b26cb0c74 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -309,7 +309,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin evd := sigma; let hook = Lemmas.mk_hook (hook new_principle_type) in let pstate = - Lemmas.start_proof ~ontop:None + Lemmas.start_proof new_princ_name (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) !evd @@ -328,8 +328,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pstate in match entries with | [entry] -> - let pstate = discard_current pstate in - (id,(entry,persistence)), hook, pstate + (id,(entry,persistence)), hook | _ -> CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") @@ -381,7 +380,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) register_with_sort InProp; register_with_sort InSet in - let ((id,(entry,g_kind)),hook,pstate) = + let ((id,(entry,g_kind)),hook) = build_functional_principle evd interactive_proof old_princ_type new_sorts funs i proof_tac hook in @@ -520,7 +519,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ s::l_schemes -> s,l_schemes | _ -> anomaly (Pp.str "") in - let ((_,(const,_)),_,pstate) = + let ((_,(const,_)),_) = try build_functional_principle evd false first_type @@ -580,7 +579,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ (* If we reach this point, the two principle are not mutually recursive We fall back to the previous method *) - let ((_,(const,_)),_,pstate) = + let ((_,(const,_)),_) = build_functional_principle evd false diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index dbfc0fc91d..b8db3dc5ce 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -190,7 +190,9 @@ VERNAC COMMAND EXTEND Function | Vernacextend.VtSideff ids, _ when hard -> Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) | x -> x } - -> { do_generate_principle false (List.map snd recsl) } + -> { fun ~pstate:ontop -> + let pstate = do_generate_principle false (List.map snd recsl) in + Proof_global.maybe_push ~ontop pstate} END { @@ -228,30 +230,30 @@ VERNAC COMMAND EXTEND NewFunctionalScheme | ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } -> - { fun ~pstate -> + { fun ~pstate:ontop -> begin try - Functional_principles_types.build_scheme fas; pstate + Functional_principles_types.build_scheme fas; ontop with | Functional_principles_types.No_graph_found -> begin match fas with | (_,fun_name,_)::_ -> begin - let pstate = make_graph ~pstate (Smartlocate.global_with_alias fun_name) in - try Functional_principles_types.build_scheme fas; pstate + let ontop = make_graph ~ontop (Smartlocate.global_with_alias fun_name) in + try Functional_principles_types.build_scheme fas; ontop with | Functional_principles_types.No_graph_found -> CErrors.user_err Pp.(str "Cannot generate induction principle(s)") | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in - warning_error names e; pstate + warning_error names e; ontop end | _ -> assert false (* we can only have non empty list *) end | e when CErrors.noncritical e -> let names = List.map (fun (_,na,_) -> na) fas in - warning_error names e; pstate + warning_error names e; ontop end } END @@ -266,5 +268,5 @@ END (***** debug only ***) VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY | ![ proof ] ["Generate" "graph" "for" reference(c)] -> - { make_graph (Smartlocate.global_with_alias c) } + { fun ~pstate:ontop -> make_graph ~ontop (Smartlocate.global_with_alias c) } END diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a6b088de0c..d47c12a7cb 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -410,7 +410,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error with e when CErrors.noncritical e -> on_error names e -let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = +let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in @@ -432,9 +432,9 @@ let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * V (Evd.from_env (Global.env ()),[]) fixpoint_exprl in - pstate, evd,List.rev rev_pconstants + None, evd,List.rev rev_pconstants | _ -> - let pstate = ComFixpoint.do_fixpoint ~ontop:pstate Global false fixpoint_exprl in + let pstate = ComFixpoint.do_fixpoint Global false fixpoint_exprl in let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> @@ -633,8 +633,8 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex fixpoint_exprl_with_new_bl -let do_generate_principle ~pstate pconstants on_error register_built interactive_proof - (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option = +let do_generate_principle pconstants on_error register_built interactive_proof + (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.pstate 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 = match fixpoint_exprl with @@ -661,7 +661,7 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive in if register_built then register_wf name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false - else pstate, false + else None, false |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with @@ -685,7 +685,7 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive in if register_built then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true - else pstate, true + else None, true | _ -> List.iter (function ((_na,ord,_args,_body,_type),_not) -> match ord with @@ -704,8 +704,8 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive let is_rec = List.exists (is_rec fix_names) recdefs in let pstate,evd,pconstants = if register_built - then register_struct ~pstate is_rec fixpoint_exprl - else pstate, Evd.from_env (Global.env ()), pconstants + then register_struct is_rec fixpoint_exprl + else None, Evd.from_env (Global.env ()), pconstants in let evd = ref evd in generate_principle @@ -839,9 +839,7 @@ let rec get_args b t : Constrexpr.local_binder_expr list * | _ -> [],b,t -let make_graph ~pstate (f_ref : GlobRef.t) = - let sigma, env = Option.cata Pfedit.get_current_context - (let e = Global.env () in Evd.from_env e, e) pstate in +let make_graph env sigma (f_ref : GlobRef.t) = let c,c_body = match f_ref with | ConstRef c -> @@ -902,11 +900,18 @@ let make_graph ~pstate (f_ref : GlobRef.t) = [((CAst.make id,None),None,nal_tas,t,Some b),[]] in let mp = Constant.modpath c in - let pstate = do_generate_principle ~pstate [c,Univ.Instance.empty] error_error false false expr_list in + let pstate = do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list in (* We register the infos *) List.iter (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) expr_list; pstate) +let make_graph ~ontop f_ref = + let pstate = Option.map Proof_global.get_current_pstate ontop in + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in + Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop + (make_graph env sigma f_ref) + let do_generate_principle = do_generate_principle [] warning_error true diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index acf85f539e..cf4ef23d1a 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -5,10 +5,10 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit -val do_generate_principle : pstate:Proof_global.t option -> +val do_generate_principle : bool -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - Proof_global.t option + Proof_global.pstate option val functional_induction : bool -> @@ -17,4 +17,4 @@ val functional_induction : Ltac_plugin.Tacexpr.or_and_intro_pattern option -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma -val make_graph : pstate:Proof_global.t option -> GlobRef.t -> Proof_global.t option +val make_graph : ontop:Proof_global.t option -> GlobRef.t -> Proof_global.t option diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 2a0140f02c..03568fc6c7 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -803,7 +803,7 @@ 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 ~ontop:None + let pstate = Lemmas.start_proof lem_id (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem))) !evd @@ -811,7 +811,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let pstate = fst @@ Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i))) pstate in - let _ = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in + let () = Lemmas.save_pstate_proved ~pstate ~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 ~ontop:None lem_id + let pstate = Lemmas.start_proof lem_id (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma (fst lemmas_types_infos.(i)) in let pstate = fst (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i))) pstate) in - let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in + let () = Lemmas.save_pstate_proved ~pstate ~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 de1b592337..b4d0f092d8 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -72,7 +72,7 @@ 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_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None +let defined pstate = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None let def_of_const t = match (Constr.kind t) with @@ -1367,10 +1367,9 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type ) g) in - let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None in - () + Lemmas.save_pstate_proved ~pstate ~opaque:opacity ~idopt:None in - let pstate = Lemmas.start_proof ~ontop:(Some pstate) + let pstate = Lemmas.start_proof na (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) sigma gls_type ~hook:(Lemmas.mk_hook hook) in @@ -1399,7 +1398,7 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type try Some (fst @@ by (Proofview.V82.tactic tclIDTAC) pstate) (* raises UserError _ if the proof is complete *) with UserError _ -> - defined pstate + (defined pstate; None) let com_terminate tcc_lemma_name @@ -1413,7 +1412,7 @@ let com_terminate nb_args ctx hook = let start_proof env ctx (tac_start:tactic) (tac_end:tactic) = - let pstate = Lemmas.start_proof ~ontop:None thm_name + let pstate = Lemmas.start_proof thm_name (Global, 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 @@ -1431,7 +1430,8 @@ let com_terminate with EmptySubgoals -> (* a non recursive function declared with measure ! *) tcc_lemma_ref := Not_needed; - defined pstate + defined pstate; + None let start_equation (f:GlobRef.t) (term_f:GlobRef.t) (cont_tactic:Id.t list -> tactic) g = @@ -1459,7 +1459,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation let evd = Evd.from_ctx uctx in let f_constr = constr_of_monomorphic_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - let pstate = Lemmas.start_proof ~ontop:None eq_name (Global, false, Proof Lemma) ~sign evd + let pstate = Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign evd (EConstr.of_constr equation_lemma_type) in let pstate = fst @@ by (Proofview.V82.tactic (start_equation f_ref terminate_ref @@ -1489,13 +1489,13 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation } ) )) pstate in - let _ = Flags.silently (fun () -> Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None) () in + let _ = Flags.silently (fun () -> Lemmas.save_pstate_proved ~pstate ~opaque:opacity ~idopt:None) () in () (* Pp.msgnl (fun _ _ -> str "eqn finished"); *) let recursive_definition 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 : Proof_global.pstate option = let open Term in let open Constr in let open CVars in diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index a006c2c354..84d7a399e1 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -14,6 +14,4 @@ bool -> 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 - - + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.pstate option diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 4c186dce09..5e4969567d 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -1118,7 +1118,7 @@ END VERNAC COMMAND EXTEND OptimizeProof | ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } -> - { fun ~pstate -> Option.map Proof_global.compact_the_proof pstate } + { fun ~pstate -> Option.map Proof_global.(modify_current_pstate compact_the_proof) pstate } | [ "Optimize" "Heap" ] => { classify_as_proofstep } -> { Gc.compact () } END diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index de3a9c9fa9..d7918a58ac 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -80,8 +80,8 @@ GRAMMAR EXTEND Gram open Obligations -let obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.obligation ~ontop:pstate obl t) tac) -let next_obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.next_obligation ~ontop:pstate obl t) tac) +let obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.obligation obl t) tac)) +let next_obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.next_obligation obl t) tac)) let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater) diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 2fad1f6b6a..e3f4b8ef59 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -280,7 +280,8 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF (* This command may or may not open a goal *) => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater } -> { - add_morphism_infer atts m n + fun ~pstate:ontop -> + Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop (add_morphism_infer atts m n) } | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { VtStartProof(GuaranteesOpacity,[n]), VtLater } diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 6f84e6c18d..efca411754 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1974,7 +1974,7 @@ let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id")) -let add_morphism_infer ~pstate atts m n : Proof_global.t option = +let add_morphism_infer atts m n : Proof_global.pstate option = warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); let instance_id = add_suffix n "_Proper" in @@ -1991,7 +1991,7 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option = add_instance (Classes.mk_instance (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst)); declare_projection n instance_id (ConstRef cst); - pstate + None else let kind = Decl_kinds.Global, atts.polymorphic, Decl_kinds.DefinitionBody Decl_kinds.Instance @@ -2008,7 +2008,7 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option = let hook = Lemmas.mk_hook hook in Flags.silently (fun () -> - let pstate = Lemmas.start_proof ~ontop:pstate ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in + let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) () let add_morphism ~pstate atts binders m s n = diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index a200cb5ced..cab7d0065e 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -89,7 +89,7 @@ val add_setoid : pstate:Proof_global.t option -> rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option -val add_morphism_infer : pstate:Proof_global.t option -> rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option +val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.pstate option val add_morphism : pstate:Proof_global.t option -> rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 7333114eae..66b47a64a7 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -108,7 +108,7 @@ let solve ?with_end_tac gi info_lvl tac pr = in (p,status) -let by tac = Proof_global.with_current_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) +let by tac = Proof_global.with_proof (fun _ -> solve (Goal_select.SelectNth 1) None tac) (**********************************************************************) (* Shortcut to build a term using tactics *) @@ -121,7 +121,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo 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 ~ontop:None evd id goal_kind goals terminator in + let pf = Proof_global.start_proof evd id goal_kind goals terminator in try let pf, status = by tac pf in let open Proof_global in diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 77d701b41f..ec52d2d5cf 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -23,17 +23,17 @@ exception NoSuchGoal the current focused proof or raises a [UserError] if there is no focused proof or if there is no more subgoals *) -val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env +val get_goal_context : Proof_global.pstate -> int -> Evd.evar_map * env (** [get_current_goal_context ()] works as [get_goal_context 1] *) -val get_current_goal_context : Proof_global.t -> Evd.evar_map * env +val get_current_goal_context : Proof_global.pstate -> Evd.evar_map * env (** [get_current_context ()] returns the context of the current focused goal. If there is no focused goal but there is a proof in progress, it returns the corresponding evar_map. If there is no pending proof then it returns the current global environment and empty evar_map. *) -val get_current_context : Proof_global.t -> Evd.evar_map * env +val get_current_context : Proof_global.pstate -> Evd.evar_map * env (** {6 ... } *) @@ -49,7 +49,7 @@ val solve : ?with_end_tac:unit Proofview.tactic -> focused proof. Returns [false] if an unsafe tactic has been used. *) -val by : unit Proofview.tactic -> Proof_global.t -> Proof_global.t * bool +val by : unit Proofview.tactic -> Proof_global.pstate -> Proof_global.pstate * bool (** Option telling if unification heuristics should be used. *) val use_unification_heuristics : unit -> bool diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 40ae4acc88..8d7960829b 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -63,23 +63,40 @@ 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 + (*** Proof Global manipulation ***) let get_all_proof_names (pf : t) = 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 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 with_current_proof f (ps, psl) = +let with_proof f ps = let et = match ps.endline_tactic with | None -> Proofview.tclUNIT () @@ -92,16 +109,23 @@ let with_current_proof f (ps, psl) = in let (newpr,ret) = f et ps.proof in let ps = { ps with proof = newpr } in - (ps, psl), ret + 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 compact_the_proof pf = simple_with_current_proof (fun _ -> Proof.compact) pf +let simple_with_proof f ps = + let ps, () = with_proof (fun t ps -> f t ps, ()) ps in ps + +let compact_the_proof pf = simple_with_proof (fun _ -> Proof.compact) pf (* Sets the tactic to be used when a tactic line is closed with [...] *) -let set_endline_tactic tac (ps, psl) = - { ps with endline_tactic = Some tac }, psl +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 @@ -112,8 +136,10 @@ let discard {CAst.loc;v=id} (ps, psl) = | [] -> None | ps :: psl -> Some (ps, psl) -let discard_current (ps, psl) = - if List.is_empty psl then None else Some List.(hd psl, tl 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 [id] with goals [goals] (a list of pairs of environment and @@ -123,30 +149,26 @@ let discard_current (ps, 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 ~ontop sigma name ?(pl=UState.default_univ_decl) kind goals terminator = - let initial_state = { - terminator = CEphemeron.create terminator; +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 } in - push ~ontop initial_state + strength = kind } -let start_dependent_proof ~ontop name ?(pl=UState.default_univ_decl) kind goals terminator = - let initial_state = { - terminator = CEphemeron.create terminator; +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 } in - push ~ontop initial_state + strength = kind } -let get_used_variables (pf,_) = pf.section_vars -let get_universe_decl (pf,_) = pf.universe_decl +let get_used_variables pf = pf.section_vars +let get_universe_decl pf = pf.universe_decl -let set_used_variables (ps,psl) l = +let set_used_variables ps l = let open Context.Named.Declaration in let env = Global.env () in let ids = List.fold_right Id.Set.add l Id.Set.empty in @@ -170,9 +192,9 @@ let set_used_variables (ps,psl) l = if not (Option.is_empty ps.section_vars) then CErrors.user_err Pp.(str "Used section variables can be declared only once"); (* EJGA: This is always empty thus we should modify the type *) - (ctx, []), ({ ps with section_vars = Some ctx}, psl) + (ctx, []), { ps with section_vars = Some ctx} -let get_open_goals (ps, _) = +let get_open_goals ps = let Proof.{ goals; stack; shelf } = Proof.data ps.proof in List.length goals + List.fold_left (+) 0 @@ -293,7 +315,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now universes }, fun pr_ending -> CEphemeron.get terminator pr_ending -let return_proof ?(allow_partial=false) (ps,_) = +let return_proof ?(allow_partial=false) ps = let { proof } = ps in if allow_partial then begin let proofs = Proof.partial_proof proof in @@ -322,27 +344,27 @@ let return_proof ?(allow_partial=false) (ps,_) = List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in proofs, Evd.evar_universe_context evd -let close_future_proof ~opaque ~feedback_id (ps, psl) proof = +let close_future_proof ~opaque ~feedback_id ps proof = close_proof ~opaque ~keep_body_ucst_separate:true ~feedback_id ~now:false proof ps -let close_proof ~opaque ~keep_body_ucst_separate fix_exn (ps, psl) = +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,psl))) ps + (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, psl) = - { ps with terminator = CEphemeron.create hook }, psl +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 : t) = +let update_global_env pf = let res, () = - with_current_proof (fun _ p -> + 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 diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index e2e457483b..6984fff63a 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -12,16 +12,20 @@ toplevel. In particular it defines the global proof environment. *) +type pstate type t -val get_current_proof_name : t -> Names.Id.t -val get_current_persistence : t -> Decl_kinds.goal_kind + +val get_current_pstate : t -> pstate + +val get_current_proof_name : pstate -> Names.Id.t +val get_current_persistence : pstate -> Decl_kinds.goal_kind val get_all_proof_names : t -> Names.Id.t list val discard : Names.lident -> t -> t option val discard_current : t -> t option -val give_me_the_proof : t -> Proof.t -val compact_the_proof : t -> t +val give_me_the_proof : pstate -> Proof.t +val compact_the_proof : pstate -> pstate (** When a proof is closed, it is reified into a [proof_object], where [id] is the name of the proof, [entries] the list of the proof terms @@ -52,6 +56,10 @@ 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:t option -> pstate -> t + +val maybe_push : ontop:t option -> pstate option -> t option + (** [start_proof ~ontop id str pl goals terminator] 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 @@ -60,25 +68,26 @@ val apply_terminator : proof_terminator -> proof_ending -> unit morphism). The proof is started in the evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) -val start_proof : ontop:t option -> +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 + proof_terminator -> pstate (** Like [start_proof] except that there may be dependencies between initial goals. *) -val start_dependent_proof : ontop:t option -> +val start_dependent_proof : Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> - Proofview.telescope -> proof_terminator -> t + Proofview.telescope -> proof_terminator -> pstate (** Update the proofs global environment after a side-effecting command (e.g. a sublemma definition) has been run inside it. Assumes there_are_pending_proofs. *) -val update_global_env : t -> t +val update_global_env : pstate -> pstate (* 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 -> + pstate -> closed_proof (* Intermediate step necessary to delegate the future. * Both access the current proof state. The former is supposed to be @@ -88,15 +97,15 @@ type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * USt (* If allow_partial is set (default no) then an incomplete proof * 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 -> +val return_proof : ?allow_partial:bool -> pstate -> closed_proof_output +val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t -> pstate -> closed_proof_output Future.computation -> closed_proof (** 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 +val get_terminator : pstate -> proof_terminator +val set_terminator : proof_terminator -> pstate -> pstate +val get_open_goals : pstate -> int (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is no current proof. @@ -106,18 +115,24 @@ val with_current_proof : val simple_with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t) -> t -> t +val with_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> pstate -> pstate * 'a +val modify_proof : (Proof.t -> Proof.t) -> pstate -> pstate + +val with_current_pstate : (pstate -> pstate * 'a) -> t -> t * 'a +val modify_current_pstate : (pstate -> pstate) -> t -> t + (** Sets the tactic to be used when a tactic line is closed with [...] *) -val set_endline_tactic : Genarg.glob_generic_argument -> t -> t +val set_endline_tactic : Genarg.glob_generic_argument -> pstate -> pstate (** Sets the section variables assumed by the proof, returns its closure * (w.r.t. type dependencies and let-ins covered by it) + a list of * ids to be cleared *) -val set_used_variables : t -> - Names.Id.t list -> (Constr.named_context * Names.lident list) * t +val set_used_variables : pstate -> + Names.Id.t list -> (Constr.named_context * Names.lident list) * pstate -val get_used_variables : t -> Constr.named_context option +val get_used_variables : pstate -> Constr.named_context option (** Get the universe declaration associated to the current proof. *) -val get_universe_decl : t -> UState.universe_decl +val get_universe_decl : pstate -> UState.universe_decl val copy_terminators : src:t -> tgt:t -> t diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index 04f10e7399..dfa681395a 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -50,6 +50,7 @@ let is_focused_goal_simple ~doc id = | `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 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 diff --git a/stm/stm.ml b/stm/stm.ml index b2bfa552b4..64f9e4aacf 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1168,7 +1168,9 @@ end = struct (* {{{ *) let get_proof ~doc id = match state_of_id ~doc id with - | `Valid (Some vstate) -> Option.map Proof_global.give_me_the_proof vstate.Vernacstate.proof + | `Valid (Some vstate) -> + Option.map (fun p -> Proof_global.(give_me_the_proof (get_current_pstate p))) + vstate.Vernacstate.proof | _ -> None let undo_vernac_classifier v ~doc = diff --git a/tactics/hints.mli b/tactics/hints.mli index 7b8f96cdd8..396c3e2fed 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -292,7 +292,7 @@ val wrap_hint_warning_fun : env -> evar_map -> (** Printing hints *) val pr_searchtable : env -> evar_map -> Pp.t -val pr_applicable_hint : Proof_global.t -> Pp.t +val pr_applicable_hint : Proof_global.pstate -> Pp.t val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 890ed76d52..49c547a979 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -891,7 +891,7 @@ let classify_ltac2 = function VERNAC COMMAND EXTEND VernacDeclareTactic2Definition | #[ local = locality ] ![proof] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> { - fun ~pstate -> Tac2entries.register_struct ?local ~pstate e; pstate + fun ~pstate -> Tac2entries.register_struct ?local ~pstate:(Option.map Proof_global.get_current_pstate pstate) e; pstate } END diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli index d493192bb3..e02c126e71 100644 --- a/user-contrib/Ltac2/tac2entries.mli +++ b/user-contrib/Ltac2/tac2entries.mli @@ -23,7 +23,7 @@ val register_primitive : ?local:bool -> val register_struct : ?local:bool - -> pstate:Proof_global.t option + -> pstate:Proof_global.pstate option -> strexpr -> unit diff --git a/vernac/classes.ml b/vernac/classes.ml index ea66234993..c783531f91 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -309,7 +309,7 @@ let id_of_class cl = mip.(0).Declarations.mind_typename | _ -> assert false -let instance_hook k info global imps ?hook cst = +let instance_hook info global imps ?hook cst = Impargs.maybe_declare_manual_implicits false cst imps; let info = intern_info info in let env = Global.env () in @@ -317,7 +317,7 @@ let instance_hook k info global imps ?hook cst = declare_instance env sigma (Some info) (not global) cst; (match hook with Some h -> h cst | None -> ()) -let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = +let declare_instance_constant info global imps ?hook id decl poly sigma term termtype = (* XXX: Duplication of the declare_constant path *) let kind = IsDefinition Instance in let sigma = @@ -331,7 +331,7 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t let kn = Declare.declare_constant id cdecl in Declare.definition_message id; Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders sigma); - instance_hook k info global imps ?hook (ConstRef kn) + instance_hook info global imps ?hook (ConstRef kn) let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst id = let subst = List.fold_left2 @@ -344,66 +344,65 @@ let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id (ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); - instance_hook k pri global imps (ConstRef cst) + instance_hook pri global imps (ConstRef cst) -let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype = +let declare_instance_program env sigma ~global ~poly id pri imps decl term termtype = + let hook _ _ vis gr = + let cst = match gr with ConstRef kn -> kn | _ -> assert false in + Impargs.declare_manual_implicits false gr imps; + let pri = intern_info pri in + let env = Global.env () in + let sigma = Evd.from_env env in + declare_instance env sigma (Some pri) (not global) (ConstRef cst) + in + let obls, constr, typ = + match term with + | Some t -> + let termtype = EConstr.of_constr termtype in + let obls, _, constr, typ = + Obligations.eterm_obligations env id sigma 0 t termtype + in obls, Some constr, typ + | None -> [||], None, termtype + in + let hook = Lemmas.mk_hook hook in + let ctx = Evd.evar_universe_context sigma in + ignore(Obligations.add_definition id ?term:constr + ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls) + + +let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids term termtype = + (* spiwack: it is hard to reorder the actions to do + the pretyping after the proof has opened. As a + consequence, we use the low-level primitives to code + the refinement manually.*) + let gls = List.rev (Evd.future_goals sigma) in + let sigma = Evd.reset_future_goals sigma in let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in - if program_mode then - let hook _ _ vis gr = - let cst = match gr with ConstRef kn -> kn | _ -> assert false in - Impargs.declare_manual_implicits false gr imps; - let pri = intern_info pri in - let env = Global.env () in - let sigma = Evd.from_env env in - declare_instance env sigma (Some pri) (not global) (ConstRef cst) - in - let obls, constr, typ = - match term with - | Some t -> - let termtype = EConstr.of_constr termtype in - let obls, _, constr, typ = - Obligations.eterm_obligations env id sigma 0 t termtype - in obls, Some constr, typ - | None -> [||], None, termtype - in - let hook = Lemmas.mk_hook hook in - let ctx = Evd.evar_universe_context sigma in - let _progress = Obligations.add_definition id ?term:constr - ~univdecl:decl typ ctx ~kind:(Global,poly,Instance) ~hook obls in + let pstate = Lemmas.start_proof 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 = + if not (Option.is_empty term) then + let init_refine = + Tacticals.New.tclTHENLIST [ + Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term)); + Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls); + Tactics.New.reduce_after_refine; + ] + in + let pstate, _ = Pfedit.by init_refine pstate in + pstate + else + let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in + pstate + in + match tac with + | Some tac -> + let pstate, _ = Pfedit.by tac pstate in + pstate + | None -> pstate - else - Some Flags.(silently (fun () -> - (* spiwack: it is hard to reorder the actions to do - the pretyping after the proof has opened. As a - consequence, we use the low-level primitives to code - the refinement manually.*) - let gls = List.rev (Evd.future_goals sigma) in - let sigma = Evd.reset_future_goals sigma in - let pstate = Lemmas.start_proof ~ontop:pstate id ~pl:decl kind sigma (EConstr.of_constr termtype) - ~hook:(Lemmas.mk_hook - (fun _ _ _ -> instance_hook k pri global imps ?hook)) in - (* spiwack: I don't know what to do with the status here. *) - let pstate = - if not (Option.is_empty term) then - let init_refine = - Tacticals.New.tclTHENLIST [ - Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term)); - Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls); - Tactics.New.reduce_after_refine; - ] - in - let pstate, _ = Pfedit.by init_refine pstate in - pstate - else - let pstate, _ = Pfedit.by (Tactics.auto_intros_tac ids) pstate in - pstate - in - match tac with - | Some tac -> - let pstate, _ = Pfedit.by tac pstate in - pstate - | None -> - pstate) ()) let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = let props = @@ -487,10 +486,18 @@ let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode ct let pstate = if not (Evd.has_undefined sigma) && not (Option.is_empty props) then let term = to_constr sigma (Option.get term) in - (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype; - None) - else if program_mode || Option.is_empty props then - declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype + (declare_instance_constant pri global imps ?hook id decl poly sigma term termtype; + pstate) + else if program_mode then + (declare_instance_program env sigma ~global ~poly id pri imps decl term termtype ; pstate) + else if Option.is_empty props then + let pstate' = + Flags.silently (fun () -> + declare_instance_open sigma ?hook ~tac ~global ~poly + id pri imps decl (List.map RelDecl.get_name ctx) term termtype) + () + in + Some (Proof_global.push ~ontop:pstate pstate') else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in id, pstate diff --git a/vernac/classes.mli b/vernac/classes.mli index 8d5f3e3a06..f80dbb9897 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -31,20 +31,6 @@ 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 declare_instance_constant : - typeclass -> - Hints.hint_info_expr (** priority *) -> - bool (** globality *) -> - Impargs.manual_explicitation list (** implicits *) -> - ?hook:(GlobRef.t -> unit) -> - Id.t (** name *) -> - UState.universe_decl -> - bool (** polymorphic *) -> - Evd.evar_map (** Universes *) -> - Constr.t (** body *) -> - Constr.types (** type *) -> - unit - val new_instance : pstate:Proof_global.t option -> ?global:bool (** Not global by default. *) diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index a428c42e49..006ac314a5 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -255,7 +255,7 @@ let interp_fixpoint ~cofix l ntns = let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) -let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = +let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = let pstate = if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) @@ -267,7 +267,7 @@ let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx fixdefs) in let evd = Evd.from_ctx ctx in Some - (Lemmas.start_proof_with_initialization ~ontop (local,poly,DefinitionBody Fixpoint) + (Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint) evd pl (Some(false,indexes,init_tac)) thms None) else begin (* We shortcut the proof process *) @@ -294,7 +294,7 @@ let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; pstate -let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = +let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = let pstate = if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) @@ -305,7 +305,7 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in let evd = Evd.from_ctx ctx in - Some (Lemmas.start_proof_with_initialization ~ontop (Global,poly, DefinitionBody CoFixpoint) + Some (Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint) evd pl (Some(true,[],init_tac)) thms None) else begin (* We shortcut the proof process *) @@ -366,18 +366,18 @@ let check_safe () = let flags = Environ.typing_flags (Global.env ()) in flags.check_universes && flags.check_guarded -let do_fixpoint ~ontop local poly l = +let do_fixpoint local poly l = let fixl, ntns = extract_fixpoint_components ~structonly:true l in let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in let possible_indexes = List.map compute_possible_guardness_evidences info in - let pstate = declare_fixpoint ~ontop local poly fix possible_indexes ntns in + let pstate = declare_fixpoint local poly fix possible_indexes ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); pstate -let do_cofixpoint ~ontop local poly l = +let do_cofixpoint local poly l = let fixl,ntns = extract_cofixpoint_components l in let cofix = interp_fixpoint ~cofix:true fixl ntns in - let pstate = declare_cofixpoint ~ontop local poly cofix ntns in + let pstate = declare_cofixpoint local poly cofix ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); pstate diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 5937842f17..d36593332e 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -19,14 +19,12 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint : - ontop:Proof_global.t option -> (* When [false], assume guarded. *) - locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t option + locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.pstate option val do_cofixpoint : - ontop:Proof_global.t option -> (* When [false], assume guarded. *) - locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t option + locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.pstate option (************************************************************************) (** Internal API *) @@ -83,20 +81,18 @@ val interp_fixpoint : (** [Not used so far] *) val declare_fixpoint : - ontop:Proof_global.t option -> locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * (Constr.rel_context * Impargs.manual_implicits * int option) list -> Proof_global.lemma_possible_guards -> decl_notation list -> - Proof_global.t option + Proof_global.pstate option val declare_cofixpoint : - ontop:Proof_global.t option -> locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * (Constr.rel_context * Impargs.manual_implicits * int option) list -> decl_notation list -> - Proof_global.t option + Proof_global.pstate option (** Very private function, do not use *) val compute_possible_guardness_evidences : diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 740b9031cc..d0ec575eb3 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -329,7 +329,7 @@ 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 ~ontop id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c = +let start_proof 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 @@ -340,7 +340,7 @@ let start_proof ~ontop id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ? | None -> initialize_named_context_for_proof () in let goals = [ Global.env_of_context sign , c ] in - Proof_global.start_proof ~ontop sigma id ?pl kind goals terminator + Proof_global.start_proof sigma id ?pl kind goals terminator let rec_tac_initializer finite guard thms snl = if finite then @@ -356,7 +356,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 ~ontop ?hook kind sigma decl recguard thms snl = +let start_proof_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) -> @@ -388,14 +388,14 @@ let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms s List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; call_hook ?hook ctx [] strength ref) thms_data in - let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in - let pstate = Proof_global.simple_with_current_proof (fun _ p -> + let pstate = start_proof id ~pl:decl kind sigma t ~hook ~compute_guard:guard in + let pstate = Proof_global.modify_proof (fun p -> match init_tac with | None -> p | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in pstate -let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms = +let start_proof_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 @@ -427,7 +427,7 @@ let start_proof_com ~program_mode ~ontop ?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 ~ontop ?hook kind evd decl recguard thms snl + start_proof_with_initialization ?hook kind evd decl recguard thms snl (* Saving a proof *) @@ -487,20 +487,26 @@ let save_proof_admitted ?proof ~pstate = in Proof_global.apply_terminator (Proof_global.get_terminator pstate) pe -let save_proof_proved ?proof ?pstate ~opaque ~idopt = +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))) + +let save_proof_proved ?proof ?ontop ~opaque ~idopt = (* Invariant (uh) *) - if Option.is_empty pstate && Option.is_empty proof then + if Option.is_empty ontop && 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 = Option.get pstate in + 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 | Some proof -> proof in (* if the proof is given explicitly, nothing has to be deleted *) - let pstate = if Option.is_empty proof then Proof_global.discard_current Option.(get pstate) else pstate in + 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))); - pstate + ontop diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 1f70cfa1ad..ad6eb024aa 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -37,26 +37,25 @@ val call_hook -> ?fix_exn:Future.fix_exn -> hook_type -val start_proof : ontop:Proof_global.t option -> Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> +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 + ?hook:declaration_hook -> EConstr.types -> Proof_global.pstate val start_proof_com : program_mode:bool - -> ontop:Proof_global.t option -> ?inference_hook:Pretyping.inference_hook -> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list - -> Proof_global.t + -> Proof_global.pstate -val start_proof_with_initialization : ontop:Proof_global.t option -> +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 + -> int list option -> Proof_global.pstate val standard_proof_terminator : ?hook:declaration_hook -> Proof_global.lemma_possible_guards -> @@ -73,12 +72,18 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val val save_proof_admitted : ?proof:Proof_global.closed_proof - -> pstate:Proof_global.t + -> pstate:Proof_global.pstate -> unit val save_proof_proved : ?proof:Proof_global.closed_proof - -> ?pstate:Proof_global.t + -> ?ontop:Proof_global.t -> opaque:Proof_global.opacity_flag -> idopt:Names.lident option -> Proof_global.t option + +val save_pstate_proved + : pstate:Proof_global.pstate + -> opaque:Proof_global.opacity_flag + -> idopt:Names.lident option + -> unit diff --git a/vernac/obligations.ml b/vernac/obligations.ml index bc741a0ec7..0d93e19723 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -760,7 +760,7 @@ let update_obls prg obls rem = match prg'.prg_deps with | [] -> let kn = declare_definition prg' in - progmap_remove prg'; + progmap_remove prg'; Defined kn | l -> let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in @@ -944,7 +944,7 @@ let obligation_hook prg obl num auto ctx' _ _ gr = ignore (auto (Some prg.prg_name) None deps) end -let rec solve_obligation ~ontop prg num tac = +let rec solve_obligation prg num tac = let user_num = succ num in let obls, rem = prg.prg_obligations in let obl = obls.(num) in @@ -965,19 +965,19 @@ let rec solve_obligation ~ontop prg num tac = Proof_global.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 ~ontop ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator ~hook 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 -and obligation ~ontop (user_num, name, typ) tac = +and obligation (user_num, name, typ) tac = let num = pred user_num in let prg = get_prog_err name in let obls, rem = prg.prg_obligations in if num >= 0 && num < Array.length obls then let obl = obls.(num) in match obl.obl_body with - | None -> solve_obligation ~ontop prg num tac + | None -> solve_obligation prg num tac | Some r -> error "Obligation already solved" else error (sprintf "Unknown obligation number %i" (succ num)) @@ -1177,7 +1177,7 @@ let admit_obligations n = let prg = get_prog_err n in admit_prog prg -let next_obligation ~ontop n tac = +let next_obligation n tac = let prg = match n with | None -> get_any_prog_err () | Some _ -> get_prog_err n @@ -1188,7 +1188,7 @@ let next_obligation ~ontop n tac = | Some i -> i | None -> anomaly (Pp.str "Could not find a solvable obligation.") in - solve_obligation ~ontop prg i tac + solve_obligation prg i tac let check_program_libraries () = Coqlib.check_required_library Coqlib.datatypes_module_name; diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 9214ddd4b9..7db094a75d 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -86,16 +86,14 @@ val add_mutual_definitions : fixpoint_kind -> unit val obligation - : ontop:Proof_global.t option - -> 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 + -> Proof_global.pstate val next_obligation - : ontop:Proof_global.t option - -> Names.Id.t option + : Names.Id.t option -> Genarg.glob_generic_argument option - -> Proof_global.t + -> Proof_global.pstate 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/search.mli b/vernac/search.mli index 0f94ddc5b6..f8074a67ff 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -39,13 +39,13 @@ val search_about_filter : glob_search_about_item -> filter_function goal and the global environment for things matching [pattern] and satisfying module exclude/include clauses of [modinout]. *) -val search_by_head : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool +val search_by_head : ?pstate:Proof_global.pstate -> int option -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search_rewrite : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool +val search_rewrite : ?pstate:Proof_global.pstate -> int option -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search_pattern : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool +val search_pattern : ?pstate:Proof_global.pstate -> int option -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search_about : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list +val search_about : ?pstate:Proof_global.pstate -> int option -> (bool * glob_search_about_item) list -> DirPath.t list * bool -> display_function -> unit type search_constraint = @@ -66,12 +66,12 @@ type 'a coq_object = { coq_object_object : 'a; } -val interface_search : ?pstate:Proof_global.t -> ?glnum:int -> (search_constraint * bool) list -> +val interface_search : ?pstate:Proof_global.pstate -> ?glnum:int -> (search_constraint * bool) list -> constr coq_object list (** {6 Generic search function} *) -val generic_search : ?pstate:Proof_global.t -> int option -> display_function -> unit +val generic_search : ?pstate:Proof_global.pstate -> int option -> display_function -> unit (** This function iterates over all hypothesis of the goal numbered [glnum] (if present) and all known declarations. *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 337cb233a2..f92c1f9c27 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -56,6 +56,10 @@ let vernac_require_open_proof ~pstate f = | Some pstate -> f ~pstate | 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 get_current_or_global_context ~pstate = match pstate with | None -> let env = Global.env () in Evd.(from_env env, env) @@ -540,7 +544,7 @@ let () = (***********) (* Gallina *) -let start_proof_and_print ~program_mode ~pstate ?hook k l = +let start_proof_and_print ~program_mode ?hook k l = let inference_hook = if program_mode then let hook env sigma ev = @@ -562,7 +566,7 @@ let start_proof_and_print ~program_mode ~pstate ?hook k l = in Some hook else None in - start_proof_com ~program_mode ~ontop:pstate ?inference_hook ?hook k l + start_proof_com ~program_mode ?inference_hook ?hook k l let vernac_definition_hook p = function | Coercion -> @@ -573,7 +577,7 @@ let vernac_definition_hook p = function Some (Class.add_subclass_hook p) | _ -> None -let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def = +let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def ~pstate = let open DefAttributes in let local = enforce_locality_exp atts.locality discharge in let hook = vernac_definition_hook atts.polymorphic kind in @@ -593,9 +597,10 @@ let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def = in (match def with | ProveBody (bl,t) -> (* local binders, typ *) - Some (start_proof_and_print ~program_mode ~pstate (local, atts.polymorphic, DefinitionBody kind) + Some (start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind) ?hook [(CAst.make ?loc name, pl), (bl, t)]) | DefineBody (bl,red_option,c,typ_opt) -> + let pstate = Option.map Proof_global.get_current_pstate pstate in let red_option = match red_option with | None -> None | Some r -> @@ -603,30 +608,31 @@ let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def = Some (snd (Hook.get f_interp_redexp env sigma r)) in ComDefinition.do_definition ~program_mode name (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook; - pstate + None ) -let vernac_start_proof ~atts ~pstate kind l = +(* NB: pstate argument to use combinators easily *) +let vernac_start_proof ~atts kind l ~pstate = let open DefAttributes in let local = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - Some (start_proof_and_print ~pstate ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l) + Some (start_proof_and_print ~program_mode:atts.program (local, atts.polymorphic, Proof kind) l) -let vernac_end_proof ?pstate ?proof = function +let vernac_end_proof ?pstate:ontop ?proof = function | Admitted -> - vernac_require_open_proof ~pstate (save_proof_admitted ?proof); - pstate + with_pstate ~pstate:ontop (save_proof_admitted ?proof); + ontop | Proved (opaque,idopt) -> - save_proof_proved ?pstate ?proof ~opaque ~idopt + save_proof_proved ?ontop ?proof ~opaque ~idopt -let vernac_exact_proof ~pstate c = +let vernac_exact_proof ~pstate:ontop 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 pstate = save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Opaque ~idopt:None in + let pstate, status = Pfedit.by (Tactics.exact_proof c) (Proof_global.get_current_pstate ontop) in + let () = save_pstate_proved ~pstate ~opaque:Proof_global.Opaque ~idopt:None in if not status then Feedback.feedback Feedback.AddedAxiom; - pstate + Proof_global.discard_current ontop let vernac_assumption ~atts discharge kind l nl = let open DefAttributes in @@ -804,7 +810,7 @@ let vernac_inductive ~atts cum lo finite indl = in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]] *) -let vernac_fixpoint ~atts ~pstate discharge l : Proof_global.t option = +let vernac_fixpoint ~atts discharge l ~pstate = let open DefAttributes in let local = enforce_locality_exp atts.locality discharge in if Dumpglob.dump () then @@ -813,11 +819,11 @@ let vernac_fixpoint ~atts ~pstate discharge l : Proof_global.t option = let do_fixpoint = if atts.program then fun local sign l -> ComProgramFixpoint.do_fixpoint local sign l; None else - ComFixpoint.do_fixpoint ~ontop:pstate + ComFixpoint.do_fixpoint in do_fixpoint local atts.polymorphic l -let vernac_cofixpoint ~atts ~pstate discharge l = +let vernac_cofixpoint ~atts discharge l ~pstate = let open DefAttributes in let local = enforce_locality_exp atts.locality discharge in if Dumpglob.dump () then @@ -825,7 +831,7 @@ let vernac_cofixpoint ~atts ~pstate discharge l = let do_cofixpoint = if atts.program then fun local sign l -> ComProgramFixpoint.do_cofixpoint local sign l; None else - ComFixpoint.do_cofixpoint ~ontop:pstate + ComFixpoint.do_cofixpoint in do_cofixpoint local atts.polymorphic l @@ -1104,7 +1110,7 @@ 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 : Proof_global.pstate) e : Proof_global.pstate = let env = Global.env () in let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in let tys = @@ -1118,9 +1124,7 @@ let vernac_set_used_variables ~(pstate : Proof_global.t) e : Proof_global.t = (str "Unknown variable: " ++ Id.print id)) l; let _, pstate = Proof_global.set_used_variables pstate l in - fst @@ Proof_global.with_current_proof begin fun _ p -> - (p, ()) - end pstate + pstate (*****************************) (* Auxiliary file management *) @@ -1829,6 +1833,7 @@ let query_command_selector ?loc = function (str "Query commands only support the single numbered goal selector.") let vernac_check_may_eval ~pstate ~atts redexp glopt rc = + let pstate = Option.map Proof_global.get_current_pstate pstate in let glopt = query_command_selector glopt in let sigma, env = get_current_context_of_args ~pstate glopt in let sigma, c = interp_open_constr env sigma rc in @@ -1929,6 +1934,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = print_about env sigma ref_or_by_not udecl let vernac_print ~(pstate : Proof_global.t option) ~atts = + let pstate = Option.map Proof_global.get_current_pstate pstate in let sigma, env = get_current_or_global_context ~pstate in function | PrintTables -> print_tables () @@ -2040,6 +2046,7 @@ let () = optwrite = (:=) search_output_name_only } let vernac_search ~pstate ~atts s gopt r = + let pstate = Option.map Proof_global.get_current_pstate pstate in let gopt = query_command_selector gopt in let r = interp_search_restriction r in let env,gopt = @@ -2077,6 +2084,7 @@ let vernac_locate ~pstate = function | LocateTerm {v=AN qid} -> print_located_term qid | LocateAny {v=ByNotation (ntn, sc)} (* TODO : handle Ltac notations *) | LocateTerm {v=ByNotation (ntn, sc)} -> + let pstate = Option.map Proof_global.get_current_pstate pstate in let _, env = get_current_or_global_context ~pstate in Notation.locate_notation (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc @@ -2132,6 +2140,7 @@ let vernac_unfocus () = (* Checks that a proof is fully unfocused. Raises an error if not. *) let vernac_unfocused ~pstate = + let pstate = Proof_global.get_current_pstate pstate in let p = Proof_global.give_me_the_proof pstate in if Proof.unfocused p then str"The proof is indeed fully unfocused." @@ -2162,18 +2171,19 @@ let vernac_bullet (bullet : Proof_bullet.t) = Proof_global.simple_with_current_proof (fun _ p -> Proof_bullet.put p bullet) -let vernac_show ~pstate = - match pstate with +let vernac_show ~pstate:ontop = + match ontop with (* Show functions that don't require a proof state *) | None -> begin function - | ShowProof -> show_proof ~pstate + | ShowProof -> show_proof ~pstate:None | ShowMatch id -> show_match id | _ -> user_err (str "This command requires an open proof.") end (* Show functions that require a proof state *) - | Some pstate -> + | Some ontop -> + let pstate = Proof_global.get_current_pstate ontop in begin function | ShowGoal goalref -> let proof = Proof_global.give_me_the_proof pstate in @@ -2185,7 +2195,7 @@ let vernac_show ~pstate = | ShowExistentials -> show_top_evars ~pstate | ShowUniverses -> show_universes ~pstate | ShowProofNames -> - pr_sequence Id.print (Proof_global.get_all_proof_names pstate) + pr_sequence Id.print (Proof_global.get_all_proof_names ontop) | ShowIntros all -> show_intro ~pstate all | ShowProof -> show_proof ~pstate:(Some pstate) | ShowMatch id -> show_match id @@ -2223,6 +2233,10 @@ let with_def_attributes ~atts f = if atts.DefAttributes.program then Obligations.check_program_libraries (); f ~atts +let with_maybe_open_proof ~pstate f = + let opt = f ~pstate in + Proof_global.maybe_push ~ontop:pstate opt + (** A global default timeout, controlled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) @@ -2339,9 +2353,9 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = (* Gallina *) | VernacDefinition ((discharge,kind),lid,d) -> - with_def_attributes ~atts vernac_definition ~pstate discharge kind lid d + with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_definition discharge kind lid d) | VernacStartTheoremProof (k,l) -> - with_def_attributes ~atts vernac_start_proof ~pstate k l + with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_start_proof k l) | VernacEndProof e -> unsupported_attributes atts; vernac_end_proof ?proof ?pstate e @@ -2355,9 +2369,9 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = vernac_inductive ~atts cum priv finite l; pstate | VernacFixpoint (discharge, l) -> - with_def_attributes ~atts vernac_fixpoint ~pstate discharge l + with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_fixpoint discharge l) | VernacCoFixpoint (discharge, l) -> - with_def_attributes ~atts vernac_cofixpoint ~pstate discharge l + with_maybe_open_proof ~pstate (with_def_attributes ~atts vernac_cofixpoint discharge l) | VernacScheme l -> unsupported_attributes atts; vernac_scheme l; @@ -2587,7 +2601,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = | VernacCheckGuard -> unsupported_attributes atts; Feedback.msg_notice @@ - vernac_require_open_proof ~pstate (vernac_check_guard); + with_pstate ~pstate (vernac_check_guard); pstate | VernacProof (tac, using) -> unsupported_attributes atts; @@ -2596,10 +2610,14 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = let usings = if Option.is_empty using then "using:no" else "using:yes" in Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings); let pstate = - vernac_require_open_proof ~pstate (fun ~pstate -> + vernac_require_open_proof ~pstate (fun ~pstate:ontop -> + Proof_global.modify_current_pstate (fun pstate -> + let pstate = Proof_global.get_current_pstate ontop in let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in Option.cata (vernac_set_used_variables ~pstate) pstate using) - in Some pstate + ontop) + in + Some pstate | VernacProofMode mn -> unsupported_attributes atts; pstate diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 77f54361da..9ab2d00fc2 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -96,17 +96,21 @@ module Proof_global = struct | None -> raise NoCurrentProof | Some x -> f x + let cc1 f = cc (fun p -> f (Proof_global.get_current_pstate p)) + let dd f = match !s_proof with | None -> raise NoCurrentProof | Some x -> s_proof := Some (f x) + let dd1 f = dd (fun p -> Proof_global.modify_current_pstate f p) + let there_are_pending_proofs () = !s_proof <> None - let get_open_goals () = cc get_open_goals + let get_open_goals () = cc1 get_open_goals - let set_terminator x = dd (set_terminator x) - let give_me_the_proof_opt () = Option.map give_me_the_proof !s_proof - let give_me_the_proof () = cc give_me_the_proof - let get_current_proof_name () = cc get_current_proof_name + 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 simple_with_current_proof f = dd (simple_with_current_proof f) @@ -118,18 +122,18 @@ module Proof_global = struct let install_state s = s_proof := Some s let return_proof ?allow_partial () = - cc (return_proof ?allow_partial) + cc1 (return_proof ?allow_partial) let close_future_proof ~opaque ~feedback_id pf = - cc (fun st -> close_future_proof ~opaque ~feedback_id st pf) + cc1 (fun st -> close_future_proof ~opaque ~feedback_id st pf) let close_proof ~opaque ~keep_body_ucst_separate f = - cc (close_proof ~opaque ~keep_body_ucst_separate f) + cc1 (close_proof ~opaque ~keep_body_ucst_separate f) let discard_all () = s_proof := None - let update_global_env () = dd update_global_env + let update_global_env () = dd1 update_global_env - let get_current_context () = cc Pfedit.get_current_context + let get_current_context () = cc1 Pfedit.get_current_context let get_all_proof_names () = try cc get_all_proof_names |