diff options
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 |