diff options
56 files changed, 1396 insertions, 1055 deletions
diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli index 81109887ba..4ace6e78d2 100644 --- a/coqpp/coqpp_ast.mli +++ b/coqpp/coqpp_ast.mli @@ -103,7 +103,7 @@ type classification = type vernac_rule = { vernac_atts : (string * string) list option; - vernac_state: string option; + vernac_state : string option; vernac_toks : ext_token list; vernac_class : code option; vernac_depr : bool; @@ -114,6 +114,7 @@ type vernac_ext = { vernacext_name : string; vernacext_entry : code option; vernacext_class : classification; + vernacext_state : string option; vernacext_rules : vernac_rule list; } diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll index 81ba8ad98c..9c6b78dc98 100644 --- a/coqpp/coqpp_lex.mll +++ b/coqpp/coqpp_lex.mll @@ -103,6 +103,7 @@ rule extend = parse | "PLUGIN" { PLUGIN } | "DEPRECATED" { DEPRECATED } | "CLASSIFIED" { CLASSIFIED } +| "STATE" { STATE } | "PRINTED" { PRINTED } | "TYPED" { TYPED } | "INTERPRETED" { INTERPRETED } diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 42fe13e4eb..d5aedfcbb1 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -357,22 +357,31 @@ let print_atts_right fmt = function let nota = match atts with [_] -> "" | _ -> "Attributes.Notations." in fprintf fmt "(Attributes.parse %s%a atts)" nota aux atts -let print_body_wrapper fmt r = - match r.vernac_state with - | Some "proof" -> - fprintf fmt "let proof = (%a) ~pstate:st.Vernacstate.proof in { st with Vernacstate.proof }" print_code r.vernac_body - | None -> - fprintf fmt "let () = %a in st" print_code r.vernac_body - | Some x -> - fatal ("unsupported state specifier: " ^ x) - -let print_body_fun fmt r = - fprintf fmt "let coqpp_body %a%a ~st = @[%a@] in " - print_binders r.vernac_toks print_atts_left r.vernac_atts print_body_wrapper r - -let print_body fmt r = - fprintf fmt "@[(%afun %a~atts@ ~st@ -> coqpp_body %a%a ~st)@]" - print_body_fun r print_binders r.vernac_toks +let understand_state = function + | "close_proof" -> "VtCloseProof", false + | "open_proof" -> "VtOpenProof", true + | "proof" -> "VtModifyProof", false + | "proof_opt_query" -> "VtReadProofOpt", false + | "proof_query" -> "VtReadProof", false + | s -> fatal ("unsupported state specifier: " ^ s) + +let print_body_state state fmt r = + let state = match r.vernac_state with Some _ as s -> s | None -> state in + match state with + | None -> fprintf fmt "Vernacextend.VtDefault (fun () -> %a)" print_code r.vernac_body + | Some "CUSTOM" -> print_code fmt r.vernac_body + | Some state -> + let state, unit_wrap = understand_state state in + fprintf fmt "Vernacextend.%s (%s%a)" state (if unit_wrap then "fun () ->" else "") + print_code r.vernac_body + +let print_body_fun state fmt r = + fprintf fmt "let coqpp_body %a%a = @[%a@] in " + print_binders r.vernac_toks print_atts_left r.vernac_atts (print_body_state state) r + +let print_body state fmt r = + fprintf fmt "@[(%afun %a~atts@ -> coqpp_body %a%a)@]" + (print_body_fun state) r print_binders r.vernac_toks print_binders r.vernac_toks print_atts_right r.vernac_atts let rec print_sig fmt = function @@ -383,12 +392,12 @@ let rec print_sig fmt = function fprintf fmt "@[Vernacextend.TyNonTerminal (%a, %a)@]" print_symbol symb print_sig rem -let print_rule fmt r = +let print_rule state fmt r = fprintf fmt "Vernacextend.TyML (%b, %a, %a, %a)" - r.vernac_depr print_sig r.vernac_toks print_body r print_rule_classifier r + r.vernac_depr print_sig r.vernac_toks (print_body state) r print_rule_classifier r -let print_rules fmt rules = - print_list fmt (fun fmt r -> fprintf fmt "(%a)" print_rule r) rules +let print_rules state fmt rules = + print_list fmt (fun fmt r -> fprintf fmt "(%a)" (print_rule state) r) rules let print_classifier fmt = function | ClassifDefault -> fprintf fmt "" @@ -407,7 +416,7 @@ let print_ast fmt ext = let pr fmt () = fprintf fmt "Vernacextend.vernac_extend ~command:\"%s\" %a ?entry:%a %a" ext.vernacext_name print_classifier ext.vernacext_class - print_entry ext.vernacext_entry print_rules ext.vernacext_rules + print_entry ext.vernacext_entry (print_rules ext.vernacext_state) ext.vernacext_rules in let () = fprintf fmt "let () = @[%a@]@\n" pr () in () diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly index f7959f8201..128e02e85f 100644 --- a/coqpp/coqpp_parse.mly +++ b/coqpp/coqpp_parse.mly @@ -64,7 +64,7 @@ let parse_user_entry s sep = %token <int> INT %token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED ARGUMENT %token RAW_PRINTED GLOB_PRINTED -%token COMMAND CLASSIFIED PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS +%token COMMAND CLASSIFIED STATE PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS %token BANGBRACKET HASHBRACKET LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR %token LPAREN RPAREN COLON SEMICOLON %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA @@ -183,12 +183,13 @@ argtype: ; vernac_extend: -| VERNAC vernac_entry EXTEND IDENT vernac_classifier vernac_rules END +| VERNAC vernac_entry EXTEND IDENT vernac_classifier vernac_state vernac_rules END { VernacExt { vernacext_name = $4; vernacext_entry = $2; vernacext_class = $5; - vernacext_rules = $6; + vernacext_state = $6; + vernacext_rules = $7; } } ; @@ -203,16 +204,21 @@ vernac_classifier: | CLASSIFIED AS IDENT { ClassifName $3 } ; +vernac_state: +| { None } +| STATE IDENT { Some $2 } +; + vernac_rules: | vernac_rule { [$1] } | vernac_rule vernac_rules { $1 :: $2 } ; vernac_rule: -| PIPE vernac_attributes_opt vernac_state_opt LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE +| PIPE vernac_attributes_opt rule_state LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE { { vernac_atts = $2; - vernac_state= $3; + vernac_state = $3; vernac_toks = $5; vernac_depr = $7; vernac_class= $8; @@ -220,6 +226,11 @@ vernac_rule: } } ; +rule_state: +| { None } +| BANGBRACKET IDENT RBRACKET { Some $2 } +; + vernac_attributes_opt: | { None } | HASHBRACKET vernac_attributes RBRACKET { Some $2 } @@ -236,14 +247,6 @@ vernac_attribute: | qualid_or_ident { ($1, $1) } ; -vernac_state_opt: -| { None } -| BANGBRACKET vernac_state RBRACKET { Some $2 } -; - -vernac_state: -| qualid_or_ident { $1 } - rule_deprecation: | { false } | DEPRECATED { true } diff --git a/dev/ci/user-overlays/10215-gares-less-ontop.sh b/dev/ci/user-overlays/10215-gares-less-ontop.sh new file mode 100644 index 0000000000..bceb5ad0e8 --- /dev/null +++ b/dev/ci/user-overlays/10215-gares-less-ontop.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "10215" ] || [ "$CI_BRANCH" = "custom-typing" ]; then + + equations_CI_REF=pass-less-ontop + equations_CI_GITURL=https://github.com/gares/Coq-Equations + + mtac2_CI_REF=pass-less-ontop + mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 + + paramcoq_CI_REF=pass-less-ontop + paramcoq_CI_GITURL=https://github.com/gares/paramcoq + + quickchick_CI_REF=pass-less-ontop + quickchick_CI_GITURL=https://github.com/gares/QuickChick + +fi diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 2859b56cbe..4ce87faaa1 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -532,7 +532,7 @@ let _ = let open Vernacextend in let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in - let cmd_fn c ~atts ~st = in_current_context econstr_display c; st in + let cmd_fn c ~atts = VtDefault (fun () -> in_current_context econstr_display c) in let cmd_class _ = VtQuery,VtNow in let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in vernac_extend ~command:"PrintConstr" [cmd] @@ -541,7 +541,7 @@ let _ = let open Vernacextend in let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in - let cmd_fn c ~atts ~st = in_current_context print_pure_econstr c; st in + let cmd_fn c ~atts = VtDefault (fun () -> in_current_context print_pure_econstr c) in let cmd_class _ = VtQuery,VtNow in let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in vernac_extend ~command:"PrintPureConstr" [cmd] diff --git a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst new file mode 100644 index 0000000000..21ec7f8e5b --- /dev/null +++ b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst @@ -0,0 +1,11 @@ +- Function always opens a proof when used with a ``measure`` or ``wf`` + annotation, see :ref:`advanced-recursive-functions` for the updated + documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, + by Enrico Tassi). + +- The legacy command Add Morphism always opens a proof and cannot be used + inside a module type. In order to declare a module type parameter that + happens to be a morphism, use ``Parameter Morphism``. See + :ref:`deprecated_syntax_for_generalized_rewriting` for the updated + documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, + by Enrico Tassi). diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 75251d8e33..300d62285a 100644 --- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -145,12 +145,11 @@ END it gives an error message that is basically impossible to understand. *) VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY -| ![ proof ] [ "Cmd9" ] -> +| ![ proof_query ] [ "Cmd9" ] -> { fun ~pstate -> - Option.iter (fun (pstate : Proof_global.t) -> - 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 } + 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) + } END diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index e58049b8d0..2ea0861e47 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -563,6 +563,7 @@ Printing relations and morphisms of morphisms, the :cmd:`Print Instances` command can be useful to understand what additional morphisms should be registered. +.. _deprecated_syntax_for_generalized_rewriting: Deprecated syntax and backward incompatibilities ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -589,6 +590,12 @@ Deprecated syntax and backward incompatibilities bi-implication in place of a simple implication. In practice, porting an old development to the new semantics is usually quite simple. +.. cmd:: Declare Morphism @ident : @ident + :name: Declare Morphism + + This commands is to be used in a module type to declare a parameter that + is a morphism. + Notice that several limitations of the old implementation have been lifted. In particular, it is now possible to declare several relations with the same carrier and several signatures for the same morphism. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 8c5ad785e4..c93984661e 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -737,7 +737,7 @@ used by ``Function``. A more precise description is given below. decreases at each recursive call of :token:`term`. The order must be well-founded. Parameters of the function are bound in :token:`term`. - Depending on the annotation, the user is left with some proof + If the annotation is ``measure`` or ``fw``, the user is left with some proof obligations that will be used to define the function. These proofs are: proofs that each recursive call is actually decreasing with respect to the given criteria, and (if the criteria is `wf`) a proof 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/g_derive.mlg b/plugins/derive/g_derive.mlg index 214a9d8bb5..526989fdf3 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -22,7 +22,7 @@ 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) } +VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof +| [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> + { Derive.(start_deriving f suchthat lemma) } 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..7d04fee7c1 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.t -> unit diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index db1a389fe7..9ea3fbeaf4 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -177,7 +177,7 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF END (* Show the extraction of the current proof *) -VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY -| ![ proof ] [ "Show" "Extraction" ] - -> { fun ~pstate -> let () = show_extraction ~pstate in pstate } +VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY STATE proof_query +| [ "Show" "Extraction" ] + -> { show_extraction } 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..833ff9f1ed 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -173,24 +173,41 @@ let () = let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer +let is_proof_termination_interactively_checked recsl = + List.exists (function + | _,((_,( Some { CAst.v = CMeasureRec _ } + | Some { CAst.v = CWfRec _}),_,_,_),_) -> true + | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_) + | _,((_,None,_,_,_),_) -> false) recsl + +let classify_as_Fixpoint recsl = + Vernac_classifier.classify_vernac + (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) + +let classify_funind recsl = + match classify_as_Fixpoint recsl with + | Vernacextend.VtSideff ids, _ + when is_proof_termination_interactively_checked recsl -> + Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) + | x -> x + +let is_interactive recsl = + match classify_funind recsl with + | Vernacextend.VtStartProof _, _ -> true + | _ -> false + } -(* TASSI: n'importe quoi ! *) -VERNAC COMMAND EXTEND Function -| ![ proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] - => { let hard = List.exists (function - | _,((_,(Some { CAst.v = CMeasureRec _ } - | Some { CAst.v = CWfRec _}),_,_,_),_) -> true - | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_) - | _,((_,None,_,_,_),_) -> false) recsl in - match - Vernac_classifier.classify_vernac - (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) - with - | Vernacextend.VtSideff ids, _ when hard -> - Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) - | x -> x } - -> { do_generate_principle false (List.map snd recsl) } +VERNAC COMMAND EXTEND Function STATE CUSTOM +| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] + => { classify_funind recsl } + -> { + if is_interactive recsl then + Vernacextend.VtOpenProof (fun () -> + do_generate_principle_interactive (List.map snd recsl)) + else + Vernacextend.VtDefault (fun () -> + do_generate_principle (List.map snd recsl)) } END { @@ -225,33 +242,32 @@ let warning_error names e = } VERNAC COMMAND EXTEND NewFunctionalScheme -| ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] +| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } -> - { fun ~pstate -> - begin + { begin try - Functional_principles_types.build_scheme fas; pstate + Functional_principles_types.build_scheme fas 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 + make_graph (Smartlocate.global_with_alias fun_name); + try Functional_principles_types.build_scheme fas 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 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 end } END @@ -265,6 +281,6 @@ END (***** debug only ***) VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY -| ![ proof ] ["Generate" "graph" "for" reference(c)] -> +| ["Generate" "graph" "for" reference(c)] -> { make_graph (Smartlocate.global_with_alias c) } END diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a6b088de0c..241da053b7 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 + ComFixpoint.do_fixpoint Global false fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> @@ -448,7 +448,7 @@ 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 generate_correction_proof_wf f_ref tcc_lemma_ref @@ -459,7 +459,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation -let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body +let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body pre_hook = let type_of_f = Constrexpr_ops.mkCProdN args ret_type in @@ -500,8 +500,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas (* No proof done *) () in - Recdef.recursive_definition - is_mes fname rec_impls + Recdef.recursive_definition ~interactive_proof + ~is_mes fname rec_impls type_of_f wf_rel_expr rec_arg_num @@ -510,7 +510,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas using_lemmas -let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas args ret_type body = +let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas args ret_type body = let wf_arg_type,wf_arg = match wf_arg with | None -> @@ -570,7 +570,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas in wf_rel_with_mes,false in - register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg + register_wf interactive_proof ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg using_lemmas args ret_type body let map_option f = function @@ -633,7 +633,7 @@ 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 +let do_generate_principle_aux pconstants on_error register_built interactive_proof (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option = 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 = @@ -660,8 +660,8 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive true 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 + then register_wf interactive_proof name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, 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 @@ -684,8 +684,8 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive true 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 + then register_mes interactive_proof 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 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,9 @@ 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 (f_ref : GlobRef.t) = + let env = Global.env() in + let sigma = Evd.from_env env in let c,c_body = match f_ref with | ConstRef c -> @@ -902,11 +902,27 @@ 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_aux [c,Univ.Instance.empty] error_error false false expr_list in + assert (Option.is_empty pstate); (* We register the infos *) List.iter (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) - expr_list; - pstate) - -let do_generate_principle = do_generate_principle [] warning_error true + expr_list) + +(* *************** statically typed entrypoints ************************* *) + +let do_generate_principle_interactive fixl : Proof_global.t = + match + do_generate_principle_aux [] warning_error true true fixl + with + | Some pstate -> pstate + | None -> + CErrors.anomaly + (Pp.str"indfun: leaving no open proof in interactive mode") + +let do_generate_principle fixl : unit = + match do_generate_principle_aux [] warning_error true false fixl with + | Some _pstate -> + CErrors.anomaly + (Pp.str"indfun: leaving a goal open in non-interactive mode") + | None -> () diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index acf85f539e..1ba245a45d 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -5,10 +5,12 @@ 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 -> - bool -> +val do_generate_principle : + (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit + +val do_generate_principle_interactive : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - Proof_global.t option + Proof_global.t val functional_induction : bool -> @@ -17,4 +19,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 : GlobRef.t -> unit 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..e2321d233c 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 @@ -1396,12 +1395,10 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type ) tclIDTAC) g end) pstate in - try - Some (fst @@ by (Proofview.V82.tactic tclIDTAC) pstate) (* raises UserError _ if the proof is complete *) - with UserError _ -> - defined pstate + if Proof_global.get_open_goals pstate = 0 then (defined pstate; None) else Some pstate let com_terminate + interactive_proof tcc_lemma_name tcc_lemma_ref is_mes @@ -1413,7 +1410,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 +1428,8 @@ let com_terminate with EmptySubgoals -> (* a non recursive function declared with measure ! *) tcc_lemma_ref := Not_needed; - defined pstate + if interactive_proof then Some pstate + else (defined pstate; None) let start_equation (f:GlobRef.t) (term_f:GlobRef.t) (cont_tactic:Id.t list -> tactic) g = @@ -1459,7 +1457,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,12 +1487,12 @@ 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 +let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : Proof_global.t option = let open Term in let open Constr in @@ -1585,6 +1583,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num (* XXX STATE Why do we need this... why is the toplevel protection not enough *) funind_purify (fun () -> let pstate = com_terminate + interactive_proof tcc_lemma_name tcc_lemma_constr is_mes functional_ref diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index a006c2c354..b92ac3a0ec 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -5,15 +5,19 @@ val tclUSER_if_not_mes : bool -> Names.Id.t list option -> Tacmach.tactic -val recursive_definition : -bool -> - Names.Id.t -> - Constrintern.internalization_env -> - Constrexpr.constr_expr -> - Constrexpr.constr_expr -> - int -> Constrexpr.constr_expr -> (pconstant -> - Indfun_common.tcc_lemma_value ref -> - pconstant -> - pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option - +val recursive_definition : + interactive_proof:bool -> + is_mes:bool -> + Names.Id.t -> + Constrintern.internalization_env -> + Constrexpr.constr_expr -> + Constrexpr.constr_expr -> + int -> + Constrexpr.constr_expr -> + (pconstant -> + Indfun_common.tcc_lemma_value ref -> + pconstant -> + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> + Constrexpr.constr_expr list -> + Proof_global.t option diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 4c186dce09..0ded60d9c7 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -931,10 +931,10 @@ END (* spiwack: I put it in extratactics because it is somewhat tied with the semantics of the LCF-style tactics, hence with the classic tactic mode. *) -VERNAC COMMAND EXTEND GrabEvars -| ![ proof ] [ "Grab" "Existential" "Variables" ] +VERNAC COMMAND EXTEND GrabEvars STATE proof +| [ "Grab" "Existential" "Variables" ] => { classify_as_proofstep } - -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p)) pstate } + -> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.V82.grab_evars p) pstate } END (* Shelves all the goals under focus. *) @@ -963,10 +963,10 @@ TACTIC EXTEND unshelve END (* Command to add every unshelved variables to the focus *) -VERNAC COMMAND EXTEND Unshelve -| ![ proof ] [ "Unshelve" ] +VERNAC COMMAND EXTEND Unshelve STATE proof +| [ "Unshelve" ] => { classify_as_proofstep } - -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p)) pstate } + -> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.unshelve p) pstate } END (* Gives up on the goals under focus: the goals are considered solved, @@ -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 -> Proof_global.compact_the_proof pstate } | [ "Optimize" "Heap" ] => { classify_as_proofstep } -> { Gc.compact () } END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 7eb34158e8..960e5b76f8 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -376,7 +376,7 @@ let () = declare_int_option { let vernac_solve ~pstate n info tcom b = let open Goal_select in - let pstate, status = Proof_global.with_current_proof (fun etac p -> + let pstate, status = Proof_global.with_proof (fun etac p -> let with_end_tac = if b then Some etac else None in let global = match n with SelectAll | SelectList _ -> true | _ -> false in let info = Option.append info !print_info_trace in @@ -388,7 +388,7 @@ let vernac_solve ~pstate n info tcom b = let p = Proof.maximal_unfocus Vernacentries.command_focus p in p,status) pstate in if not status then Feedback.feedback Feedback.AddedAxiom; - Some pstate + pstate let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s @@ -434,13 +434,13 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false } -VERNAC { tactic_mode } EXTEND VernacSolve -| ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +VERNAC { tactic_mode } EXTEND VernacSolve STATE proof +| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in - Vernacentries.vernac_require_open_proof vernac_solve g n t def + vernac_solve g n t def } -| ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => +| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => { let anon_abstracting_tac = is_anonymous_abstract t in let solving_tac = is_explicit_terminator t in @@ -450,7 +450,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve VtLater } -> { let t = rm_abstract t in - Vernacentries.vernac_require_open_proof vernac_solve Goal_select.SelectAll n t def + vernac_solve Goal_select.SelectAll n t def } END diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index de3a9c9fa9..58c8dabd79 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -80,25 +80,25 @@ 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 obl tac = with_tac (fun t -> Obligations.obligation obl t) tac +let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater) } -VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } -| ![ proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> +VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_proof +| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> { obligation (num, Some name, Some t) tac } -| ![ proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> +| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> { obligation (num, Some name, None) tac } -| ![ proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> +| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> { obligation (num, None, Some t) tac } -| ![ proof ] [ "Obligation" integer(num) withtac(tac) ] -> +| [ "Obligation" integer(num) withtac(tac) ] -> { obligation (num, None, None) tac } -| ![ proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> +| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> { next_obligation (Some name) tac } -| ![ proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } +| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } END VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 2fad1f6b6a..1a84158df7 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -180,34 +180,34 @@ TACTIC EXTEND setoid_rewrite END VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) (Some lemma2) None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) None None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> { declare_relation atts a aeq n None None None } END VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts a aeq n None (Some lemma2) None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) None (Some lemma3) } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts a aeq n None None (Some lemma3) } END @@ -234,65 +234,63 @@ GRAMMAR EXTEND Gram END VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) None None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None None None } END VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None (Some lemma2) None } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> { declare_relation atts ~binders:b a aeq n None None (Some lemma3) } END VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> { add_setoid atts [] a aeq t n } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> { add_setoid atts binders a aeq t n } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] - (* 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 - } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] + | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] + => { VtStartProof(GuaranteesOpacity, [n]), VtLater } + -> { if Lib.is_modtype () then + CErrors.user_err Pp.(str "Add Morphism cannot be used in a module type. Use Parameter Morphism instead."); + add_morphism_interactive atts m n } + | #[ atts = rewrite_attributes; ] [ "Declare" "Morphism" constr(m) ":" ident(n) ] + => { VtSideff([n]), VtLater } + -> { add_morphism_as_parameter atts m n } + | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { VtStartProof(GuaranteesOpacity,[n]), VtLater } - -> { - add_morphism atts [] m s n - } - | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) + -> { add_morphism atts [] m s n } + | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { VtStartProof(GuaranteesOpacity,[n]), VtLater } - -> { - add_morphism atts binders m s n - } + -> { add_morphism atts binders m s n } END TACTIC EXTEND setoid_symmetry diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 164bd7e118..7b286e69dc 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -23,7 +23,6 @@ open Tacticals.New open Tactics open Pretype_errors open Typeclasses -open Classes open Constrexpr open Globnames open Evd @@ -43,13 +42,13 @@ module NamedDecl = Context.Named.Declaration (** Typeclass-based generalized rewriting. *) -type rewrite_attributes = { polymorphic : bool; program : bool; global : bool } +type rewrite_attributes = { polymorphic : bool; global : bool } let rewrite_attributes = let open Attributes.Notations in Attributes.(polymorphic ++ program ++ locality) >>= fun ((polymorphic, program), locality) -> let global = not (Locality.make_section_locality locality) in - Attributes.Notations.return { polymorphic; program; global } + Attributes.Notations.return { polymorphic; global } (** Constants used by the tactic. *) @@ -1795,15 +1794,16 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] -let anew_instance ~pstate atts binders (name,t) fields = - let program_mode = atts.program in - new_instance ~pstate ~program_mode atts.polymorphic - name binders t (Some (true, CAst.make @@ CRecord (fields))) - ~global:atts.global ~generalize:false Hints.empty_hint_info +let anew_instance atts binders (name,t) fields = + let _id = Classes.new_instance atts.polymorphic + name binders t (true, CAst.make @@ CRecord (fields)) + ~global:atts.global ~generalize:false Hints.empty_hint_info + in + () -let declare_instance_refl ~pstate atts binders a aeq n lemma = +let declare_instance_refl atts binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" - in anew_instance ~pstate atts binders instance + in anew_instance atts binders instance [(qualid_of_ident (Id.of_string "reflexivity"),lemma)] let declare_instance_sym atts binders a aeq n lemma = @@ -1816,44 +1816,44 @@ let declare_instance_trans atts binders a aeq n lemma = in anew_instance atts binders instance [(qualid_of_ident (Id.of_string "transitivity"),lemma)] -let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans = +let declare_relation atts ?(binders=[]) a aeq n refl symm trans = init_setoid (); let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in - let _, pstate = anew_instance ~pstate atts binders instance [] in + let () = anew_instance atts binders instance [] in match (refl,symm,trans) with - (None, None, None) -> pstate - | (Some lemma1, None, None) -> - snd @@ declare_instance_refl ~pstate atts binders a aeq n lemma1 - | (None, Some lemma2, None) -> - snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2 - | (None, None, Some lemma3) -> - snd @@ declare_instance_trans ~pstate atts binders a aeq n lemma3 - | (Some lemma1, Some lemma2, None) -> - let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in - snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2 - | (Some lemma1, None, Some lemma3) -> - let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in - let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in - snd @@ anew_instance ~pstate atts binders instance - [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1); - (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)] - | (None, Some lemma2, Some lemma3) -> - let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in - let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in - snd @@ anew_instance ~pstate atts binders instance - [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2); - (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)] - | (Some lemma1, Some lemma2, Some lemma3) -> - let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in - let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in - let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in - let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in - snd @@ anew_instance ~pstate atts binders instance - [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1); - (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2); - (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)] + (None, None, None) -> () + | (Some lemma1, None, None) -> + declare_instance_refl atts binders a aeq n lemma1 + | (None, Some lemma2, None) -> + declare_instance_sym atts binders a aeq n lemma2 + | (None, None, Some lemma3) -> + declare_instance_trans atts binders a aeq n lemma3 + | (Some lemma1, Some lemma2, None) -> + let () = declare_instance_refl atts binders a aeq n lemma1 in + declare_instance_sym atts binders a aeq n lemma2 + | (Some lemma1, None, Some lemma3) -> + let () = declare_instance_refl atts binders a aeq n lemma1 in + let () = declare_instance_trans atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in + anew_instance atts binders instance + [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1); + (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)] + | (None, Some lemma2, Some lemma3) -> + let () = declare_instance_sym atts binders a aeq n lemma2 in + let () = declare_instance_trans atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in + anew_instance atts binders instance + [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2); + (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)] + | (Some lemma1, Some lemma2, Some lemma3) -> + let () = declare_instance_refl atts binders a aeq n lemma1 in + let () = declare_instance_sym atts binders a aeq n lemma2 in + let () = declare_instance_trans atts binders a aeq n lemma3 in + let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in + anew_instance atts binders instance + [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1); + (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2); + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)] let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) @@ -1949,18 +1949,18 @@ let warn_add_setoid_deprecated = CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () -> Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation.")) -let add_setoid ~pstate atts binders a aeq t n = +let add_setoid atts binders a aeq t n = warn_add_setoid_deprecated ?loc:a.CAst.loc (); init_setoid (); - let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in - let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in - let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in + let () = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in + let () = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in + let () = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in - snd @@ anew_instance ~pstate atts binders instance - [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); - (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); - (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])] + anew_instance atts binders instance + [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); + (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])] let make_tactic name = @@ -1972,45 +1972,48 @@ 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_as_parameter atts m n : unit = + init_setoid (); + let instance_id = add_suffix n "_Proper" in + let env = Global.env () in + let evd = Evd.from_env env in + let uctx, instance = build_morphism_signature env evd m in + let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in + let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id + (Entries.ParameterEntry + (None,(instance,uctx),None), + Decl_kinds.IsAssumption Decl_kinds.Logical) + in + Classes.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) + +let add_morphism_interactive atts m n : Proof_global.t = warn_add_morphism_deprecated ?loc:m.CAst.loc (); init_setoid (); - (* NB: atts.program is ignored, program mode automatically set by vernacentries *) let instance_id = add_suffix n "_Proper" in let env = Global.env () in let evd = Evd.from_env env in let uctx, instance = build_morphism_signature env evd m in - if Lib.is_modtype () then - let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id - (Entries.ParameterEntry - (None,(instance,uctx),None), - Decl_kinds.IsAssumption Decl_kinds.Logical) - in - 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 - else - let kind = Decl_kinds.Global, atts.polymorphic, - Decl_kinds.DefinitionBody Decl_kinds.Instance - in - let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in - let hook _ _ _ = function - | Globnames.ConstRef cst -> - 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) - | _ -> assert false - in - 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 - Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) () + let kind = Decl_kinds.Global, atts.polymorphic, + Decl_kinds.DefinitionBody Decl_kinds.Instance + in + let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in + let hook _ _ _ = function + | Globnames.ConstRef cst -> + Classes.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) + | _ -> assert false + in + let hook = Lemmas.mk_hook hook in + Flags.silently + (fun () -> + let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in + fst Pfedit.(by (Tacinterp.interp tac) pstate)) () -let add_morphism ~pstate atts binders m s n = +let add_morphism atts binders m s n = init_setoid (); let instance_id = add_suffix n "_Proper" in let instance_name = (CAst.make @@ Name instance_id),None in @@ -2020,12 +2023,12 @@ let add_morphism ~pstate atts binders m s n = [cHole; s; m]) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - let _, pstate = new_instance ~pstate - ~program_mode:atts.program ~global:atts.global atts.polymorphic - instance_name binders instance_t None + let _id, pstate = Classes.new_instance_interactive + ~global:atts.global atts.polymorphic + instance_name binders instance_t ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in - pstate + pstate (* no instance body -> always open proof *) (** Bind to "rewrite" too *) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index a200cb5ced..3ef33c6dc9 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -81,18 +81,36 @@ val cl_rewrite_clause : val is_applied_rewrite_relation : env -> evar_map -> rel_context -> constr -> types option -val declare_relation : pstate:Proof_global.t option -> rewrite_attributes -> - ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> - constr_expr option -> constr_expr option -> constr_expr option -> Proof_global.t option - -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 : pstate:Proof_global.t option -> - rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option +val declare_relation + : rewrite_attributes + -> ?binders:local_binder_expr list + -> constr_expr + -> constr_expr + -> Id.t + -> constr_expr option + -> constr_expr option + -> constr_expr option + -> unit + +val add_setoid + : rewrite_attributes + -> local_binder_expr list + -> constr_expr + -> constr_expr + -> constr_expr + -> Id.t + -> unit + +val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t +val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit + +val add_morphism + : rewrite_attributes + -> local_binder_expr list + -> constr_expr + -> constr_expr + -> Id.t + -> Proof_global.t val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr 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/proof_global.ml b/proofs/proof_global.ml index 40ae4acc88..b642e8eea7 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -45,7 +45,7 @@ type proof_ending = type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator -type pstate = { +type t = { terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; section_vars : Constr.named_context option; @@ -56,30 +56,47 @@ type pstate = { (* The head of [t] is the actual current proof, the other ones are to be resumed when the current proof is closed or aborted. *) -type t = pstate * pstate list +type stack = t * t list let pstate_map f (pf, pfl) = (f pf, List.map f pfl) let make_terminator f = f let apply_terminator f = f +let get_current_pstate (ps,_) = ps + (* combinators for the current_proof lists *) let push ~ontop a = match ontop with | None -> a , [] | Some (l,ls) -> a, (l :: ls) +let maybe_push ~ontop = function + | Some pstate -> Some (push ~ontop pstate) + | None -> ontop + (*** Proof Global manipulation ***) -let get_all_proof_names (pf : t) = +let get_all_proof_names (pf : stack) = let (pn, pns) = pstate_map Proof.(function pf -> (data pf.proof).name) pf in pn :: pns -let give_me_the_proof (ps,_) = ps.proof -let get_current_proof_name (ps,_) = (Proof.data ps.proof).Proof.name -let get_current_persistence (ps,_) = ps.strength +let 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..aff48b9636 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -13,12 +13,16 @@ environment. *) type t +type stack + +val get_current_pstate : stack -> t + val get_current_proof_name : t -> Names.Id.t val get_current_persistence : t -> Decl_kinds.goal_kind -val get_all_proof_names : t -> Names.Id.t list +val get_all_proof_names : stack -> Names.Id.t list -val discard : Names.lident -> t -> t option -val discard_current : t -> t option +val discard : Names.lident -> stack -> stack option +val discard_current : stack -> stack option val give_me_the_proof : t -> Proof.t val compact_the_proof : t -> t @@ -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:stack option -> t -> stack + +val maybe_push : ontop:stack option -> t option -> stack option + (** [start_proof ~ontop id str pl goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this @@ -60,14 +68,14 @@ 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 (** 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 @@ -78,7 +86,8 @@ val update_global_env : t -> t (* Takes a function to add to the exceptions data relative to the state in which the proof was built *) -val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> t -> closed_proof +val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Future.fix_exn -> + t -> closed_proof (* Intermediate step necessary to delegate the future. * Both access the current proof state. The former is supposed to be @@ -102,9 +111,15 @@ val get_open_goals : t -> int no current proof. The return boolean is set to [false] if an unsafe tactic has been used. *) val with_current_proof : - (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a + (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> stack -> stack * 'a val simple_with_current_proof : - (unit Proofview.tactic -> Proof.t -> Proof.t) -> t -> t + (unit Proofview.tactic -> Proof.t -> Proof.t) -> stack -> stack + +val with_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a +val modify_proof : (Proof.t -> Proof.t) -> t -> t + +val with_current_pstate : (t -> t * 'a) -> stack -> stack * 'a +val modify_current_pstate : (t -> t) -> stack -> stack (** Sets the tactic to be used when a tactic line is closed with [...] *) val set_endline_tactic : Genarg.glob_generic_argument -> t -> t @@ -120,4 +135,4 @@ val get_used_variables : t -> Constr.named_context option (** Get the universe declaration associated to the current proof. *) val get_universe_decl : t -> UState.universe_decl -val copy_terminators : src:t -> tgt:t -> t +val copy_terminators : src:stack -> tgt:stack -> stack 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..0efea0b8e0 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -881,7 +881,7 @@ end = struct (* {{{ *) let invalidate_cur_state () = cur_id := Stateid.dummy type proof_part = - Proof_global.t option * + Proof_global.stack option * int * (* Evarutil.meta_counter_summary_tag *) int * (* Evd.evar_counter_summary_tag *) Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *) @@ -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/test-suite/bugs/closed/bug_1618.v b/test-suite/bugs/closed/bug_1618.v index a7be12e26f..041055a38f 100644 --- a/test-suite/bugs/closed/bug_1618.v +++ b/test-suite/bugs/closed/bug_1618.v @@ -20,3 +20,4 @@ a := match a return (P a) with | A1 n => f n end. +Proof. Defined. diff --git a/test-suite/bugs/closed/bug_4306.v b/test-suite/bugs/closed/bug_4306.v index 80c348d207..f1bce04451 100644 --- a/test-suite/bugs/closed/bug_4306.v +++ b/test-suite/bugs/closed/bug_4306.v @@ -30,3 +30,5 @@ Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) | Gt => y :: foo (xs, ys') end end. +Proof. +Defined. diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 890ed76d52..bd1f925486 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -90,7 +90,6 @@ let tac2def_typ = Entry.create "tactic:tac2def_typ" let tac2def_ext = Entry.create "tactic:tac2def_ext" let tac2def_syn = Entry.create "tactic:tac2def_syn" let tac2def_mut = Entry.create "tactic:tac2def_mut" -let tac2def_run = Entry.create "tactic:tac2def_run" let tac2mode = Entry.create "vernac:ltac2_command" let ltac1_expr = Pltac.tactic_expr @@ -114,7 +113,7 @@ let pattern_of_qualid qid = GRAMMAR EXTEND Gram GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn - tac2def_mut tac2def_run; + tac2def_mut; tac2pat: [ "1" LEFTA [ qid = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> { @@ -288,9 +287,6 @@ GRAMMAR EXTEND Gram tac2def_mut: [ [ "Set"; qid = Prim.qualid; ":="; e = tac2expr -> { StrMut (qid, e) } ] ] ; - tac2def_run: - [ [ "Eval"; e = tac2expr -> { StrRun e } ] ] - ; tac2typ_knd: [ [ t = tac2type -> { CTydDef (Some t) } | "["; ".."; "]" -> { CTydOpn } @@ -878,20 +874,27 @@ PRINTED BY { pr_ltac2entry } | [ tac2def_ext(e) ] -> { e } | [ tac2def_syn(e) ] -> { e } | [ tac2def_mut(e) ] -> { e } -| [ tac2def_run(e) ] -> { e } +END + +VERNAC ARGUMENT EXTEND ltac2_expr +PRINTED BY { pr_ltac2expr } +| [ tac2expr(e) ] -> { e } END { let classify_ltac2 = function | StrSyn _ -> Vernacextend.(VtSideff [], VtNow) -| StrMut _ | StrVal _ | StrPrm _ | StrTyp _ | StrRun _ -> Vernacextend.classify_as_sideeff +| StrMut _ | StrVal _ | StrPrm _ | StrTyp _ -> Vernacextend.classify_as_sideeff } VERNAC COMMAND EXTEND VernacDeclareTactic2Definition -| #[ local = locality ] ![proof] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> { - fun ~pstate -> Tac2entries.register_struct ?local ~pstate e; pstate +| #[ local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> { + Tac2entries.register_struct ?local e + } +| ![proof_opt_query] [ "Ltac2" "Eval" ltac2_expr(e) ] => { Vernacextend.classify_as_sideeff } -> { + fun ~pstate -> Tac2entries.perform_eval ~pstate e } END @@ -899,15 +902,6 @@ END let _ = Pvernac.register_proof_mode "Ltac2" tac2mode -} - -VERNAC ARGUMENT EXTEND ltac2_expr -PRINTED BY { pr_ltac2expr } -| [ tac2expr(e) ] -> { e } -END - -{ - open G_ltac open Vernacextend @@ -917,9 +911,7 @@ VERNAC { tac2mode } EXTEND VernacLtac2 | ![proof] [ ltac2_expr(t) ltac_use_default(default) ] => { classify_as_proofstep } -> { (* let g = Option.default (Proof_global.get_default_goal_selector ()) g in *) - fun ~pstate -> - Option.map (fun pstate -> Tac2entries.call ~pstate ~default t) pstate - } + fun ~pstate -> Tac2entries.call ~pstate ~default t } END { diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 254c2e5086..246fe47c4a 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -769,13 +769,12 @@ let perform_eval ~pstate e = (** Toplevel entries *) -let register_struct ?local ~pstate str = match str with +let register_struct ?local str = match str with | StrVal (mut, isrec, e) -> register_ltac ?local ~mut isrec e | StrTyp (isrec, t) -> register_type ?local isrec t | StrPrm (id, t, ml) -> register_primitive ?local id t ml | StrSyn (tok, lev, e) -> register_notation ?local tok lev e | StrMut (qid, e) -> register_redefinition ?local qid e -| StrRun e -> perform_eval ~pstate e (** Toplevel exception *) @@ -857,7 +856,7 @@ let print_ltac qid = (** Calling tactics *) let solve ~pstate default tac = - let pstate, status = Proof_global.with_current_proof begin fun etac p -> + let pstate, status = Proof_global.with_proof begin fun etac p -> let with_end_tac = if default then Some etac else None in let g = Goal_select.get_default_goal_selector () in let (p, status) = Pfedit.solve g None tac ?with_end_tac p in diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli index d493192bb3..80d48f67ba 100644 --- a/user-contrib/Ltac2/tac2entries.mli +++ b/user-contrib/Ltac2/tac2entries.mli @@ -23,13 +23,14 @@ val register_primitive : ?local:bool -> val register_struct : ?local:bool - -> pstate:Proof_global.t option -> strexpr -> unit val register_notation : ?local:bool -> sexpr list -> int option -> raw_tacexpr -> unit +val perform_eval : pstate:Proof_global.t option -> raw_tacexpr -> unit + (** {5 Notations} *) type scope_rule = diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli index 2e7dfc42db..af7bc32785 100644 --- a/user-contrib/Ltac2/tac2expr.mli +++ b/user-contrib/Ltac2/tac2expr.mli @@ -168,8 +168,6 @@ type strexpr = (** Syntactic extensions *) | StrMut of qualid * raw_tacexpr (** Redefinition of mutable globals *) -| StrRun of raw_tacexpr - (** Toplevel evaluation of an expression *) (** {5 Dynamic semantics} *) diff --git a/vernac/classes.ml b/vernac/classes.ml index ea66234993..9cc8467c57 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,9 +331,9 @@ 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 do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id = let subst = List.fold_left2 (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') [] subst (snd k.cl_context) @@ -344,136 +344,78 @@ 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 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 - 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 = - match props with - | Some (true, { CAst.v = CRecord fs }) -> - if List.length fs > List.length k.cl_props then - mismatched_props env' (List.map snd fs) k.cl_props; - Some (Inl fs) - | Some (_, t) -> Some (Inr t) - | None -> - if program_mode then Some (Inl []) - else None +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 subst, sigma = - match props with - | None -> - (if List.is_empty k.cl_props then Some (Inl subst) else None), sigma - | Some (Inr term) -> - let sigma, c = interp_casted_constr_evars ~program_mode env' sigma term cty in - Some (Inr (c, subst)), sigma - | Some (Inl props) -> - let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in - let props, rest = - List.fold_left - (fun (props, rest) decl -> - if is_local_assum decl then - try - let is_id (id', _) = match RelDecl.get_name decl, get_id id' with - | Name id, {CAst.v=id'} -> Id.equal id id' - | Anonymous, _ -> false - in - let (loc_mid, c) = List.find is_id rest in - let rest' = List.filter (fun v -> not (is_id v)) rest - in - let {CAst.loc;v=mid} = get_id loc_mid in - List.iter (fun (n, _, x) -> - if Name.equal n (Name mid) then - Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs; - c :: props, rest' - with Not_found -> - ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest - else props, rest) - ([], props) k.cl_props - in - match rest with - | (n, _) :: _ -> - unbound_method env' sigma k.cl_impl (get_id n) - | _ -> - let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in - let sigma, res = type_ctx_instance ~program_mode (push_rel_context ctx' env') sigma kcl_props props subst in - Some (Inl res), sigma + 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 term, termtype = - match subst with - | None -> let termtype = it_mkProd_or_LetIn cty ctx in - None, termtype - | Some (Inl subst) -> - let subst = List.fold_left2 - (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst') - [] subst (k.cl_props @ snd k.cl_context) + 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 + 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 (app, ty_constr) = instance_constructor (k,u) subst in - let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let term = it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in - Some term, termtype - | Some (Inr (def, subst)) -> - let termtype = it_mkProd_or_LetIn cty ctx in - let term = it_mkLambda_or_LetIn def ctx in - Some term, termtype + 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_subst_constructor_and_ty subst k u ctx = + let subst = + List.fold_left2 (fun subst' s decl -> + if is_local_assum decl then s :: subst' else subst') + [] subst (k.cl_props @ snd k.cl_context) + in + let (app, ty_constr) = instance_constructor (k,u) subst in + let termtype = it_mkProd_or_LetIn ty_constr ctx in + let term = it_mkLambda_or_LetIn (Option.get app) ctx in + term, termtype + +let do_instance_resolve_TC term termtype sigma env = let sigma = Evarutil.nf_evar_map sigma in let sigma = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env sigma in (* Try resolving fields that are typeclasses automatically. *) @@ -484,17 +426,110 @@ let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode ct (* Check that the type is free of evars now. *) Pretyping.check_evars env (Evd.from_env env) sigma termtype; let termtype = to_constr sigma termtype in - 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 - else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in - id, pstate - -let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass = + termtype, sigma + +let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst = + let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in + let props, rest = + List.fold_left + (fun (props, rest) decl -> + if is_local_assum decl then + try + let is_id (id', _) = match RelDecl.get_name decl, get_id id' with + | Name id, {CAst.v=id'} -> Id.equal id id' + | Anonymous, _ -> false + in + let (loc_mid, c) = List.find is_id rest in + let rest' = List.filter (fun v -> not (is_id v)) rest + in + let {CAst.loc;v=mid} = get_id loc_mid in + List.iter (fun (n, _, x) -> + if Name.equal n (Name mid) then + Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs; + c :: props, rest' + with Not_found -> + ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest + else props, rest) + ([], props) k.cl_props + in + match rest with + | (n, _) :: _ -> + unbound_method env' sigma k.cl_impl (get_id n) + | _ -> + let kcl_props = List.map (Termops.map_rel_decl of_constr) k.cl_props in + let sigma, res = + type_ctx_instance ~program_mode + (push_rel_context ctx' env') sigma kcl_props props subst in + res, sigma + +let do_instance_interactive env sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id = + let term, termtype = + if List.is_empty k.cl_props then + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + Some term, termtype + else + None, it_mkProd_or_LetIn cty ctx in + let termtype, sigma = do_instance_resolve_TC term termtype sigma env in + Flags.silently (fun () -> + declare_instance_open sigma ?hook ~tac ~global ~poly + id pri imps decl (List.map RelDecl.get_name ctx) term termtype) + () + +let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id props = + let term, termtype, sigma = + match props with + | (true, { CAst.v = CRecord fs }) -> + if List.length fs > List.length k.cl_props then + mismatched_props env' (List.map snd fs) k.cl_props; + let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:false subst in + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + term, termtype, sigma + | (_, term) -> + let sigma, def = + interp_casted_constr_evars ~program_mode:false env' sigma term cty in + let termtype = it_mkProd_or_LetIn cty ctx in + let term = it_mkLambda_or_LetIn def ctx in + term, termtype, sigma in + let termtype, sigma = do_instance_resolve_TC (Some term) termtype sigma env in + if Evd.has_undefined sigma then + CErrors.user_err Pp.(str "Unsolved obligations remaining.") + else + let term = to_constr sigma term in + declare_instance_constant pri global imps ?hook id decl poly sigma term termtype + +let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props = + let term, termtype, sigma = + match opt_props with + | Some (true, { CAst.v = CRecord fs }) -> + if List.length fs > List.length k.cl_props then + mismatched_props env' (List.map snd fs) k.cl_props; + let subst, sigma = + do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:true subst in + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + Some term, termtype, sigma + | Some (_, term) -> + let sigma, def = + interp_casted_constr_evars ~program_mode:true env' sigma term cty in + let termtype = it_mkProd_or_LetIn cty ctx in + let term = it_mkLambda_or_LetIn def ctx in + Some term, termtype, sigma + | None -> + let subst, sigma = + do_instance_type_ctx_instance [] k env' ctx' sigma ~program_mode:true subst in + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + Some term, termtype, sigma in + let termtype, sigma = do_instance_resolve_TC term termtype sigma env in + if not (Evd.has_undefined sigma) && not (Option.is_empty opt_props) then + let term = to_constr sigma (Option.get term) in + declare_instance_constant pri global imps ?hook id decl poly sigma term termtype + else + declare_instance_program env sigma ~global ~poly id pri imps decl term termtype + +let interp_instance_context ~program_mode env ctx ~generalize pl tclass = let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in let tclass = if generalize then CAst.make @@ CGeneralization (Implicit, Some AbsPi, tclass) @@ -522,14 +557,12 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in sigma, cl, u, c', ctx', ctx, imps, args, decl -let new_instance ~pstate ?(global=false) ~program_mode - poly instid ctx cl props - ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = - let env = Global.env() in +let new_instance_common ~program_mode ~generalize env instid ctx cl = let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = interp_instance_context ~program_mode env ~generalize ctx pl cl in + (* The name generator should not be here *) let id = match instid with | Name id -> id @@ -538,13 +571,41 @@ let new_instance ~pstate ?(global=false) ~program_mode Namegen.next_global_ident_away i (Termops.vars_of_env env) in let env' = push_rel_context ctx env in - do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode - cty k u ctx ctx' pri decl imps subst id props + id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl + +let new_instance_interactive ?(global=false) + poly instid ctx cl + ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = + let env = Global.env() in + let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = + new_instance_common ~program_mode:false ~generalize env instid ctx cl in + id, do_instance_interactive env sigma ?hook ~tac ~global ~poly + cty k u ctx ctx' pri decl imps subst id + +let new_instance_program ?(global=false) + poly instid ctx cl opt_props + ?(generalize=true) ?hook pri = + let env = Global.env() in + let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = + new_instance_common ~program_mode:true ~generalize env instid ctx cl in + do_instance_program env env' sigma ?hook ~global ~poly + cty k u ctx ctx' pri decl imps subst id opt_props; + id + +let new_instance ?(global=false) + poly instid ctx cl props + ?(generalize=true) ?hook pri = + let env = Global.env() in + let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl = + new_instance_common ~program_mode:false ~generalize env instid ctx cl in + do_instance env env' sigma ?hook ~global ~poly + cty k u ctx ctx' pri decl imps subst id props; + id let declare_new_instance ?(global=false) ~program_mode poly instid ctx cl pri = let env = Global.env() in let ({CAst.loc;v=instid}, pl) = instid in let sigma, k, u, cty, ctx', ctx, imps, subst, decl = - interp_instance_context ~program_mode env ctx pl cl + interp_instance_context ~program_mode ~generalize:false env ctx pl cl in - do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid + do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst instid diff --git a/vernac/classes.mli b/vernac/classes.mli index 8d5f3e3a06..e61935c87a 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -31,34 +31,41 @@ 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_interactive : + ?global:bool (** Not global by default. *) + -> Decl_kinds.polymorphic + -> name_decl + -> local_binder_expr list + -> constr_expr + -> ?generalize:bool + -> ?tac:unit Proofview.tactic + -> ?hook:(GlobRef.t -> unit) + -> Hints.hint_info_expr + -> Id.t * Proof_global.t val new_instance : - pstate:Proof_global.t option - -> ?global:bool (** Not global by default. *) - -> program_mode:bool + ?global:bool (** Not global by default. *) + -> Decl_kinds.polymorphic + -> name_decl + -> local_binder_expr list + -> constr_expr + -> (bool * constr_expr) + -> ?generalize:bool + -> ?hook:(GlobRef.t -> unit) + -> Hints.hint_info_expr + -> Id.t + +val new_instance_program : + ?global:bool (** Not global by default. *) -> Decl_kinds.polymorphic -> name_decl -> local_binder_expr list -> constr_expr -> (bool * constr_expr) option -> ?generalize:bool - -> ?tac:unit Proofview.tactic -> ?hook:(GlobRef.t -> unit) -> Hints.hint_info_expr - -> Id.t * Proof_global.t option (* May open a proof *) + -> Id.t val declare_new_instance : ?global:bool (** Not global by default. *) diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index a428c42e49..7a4e6d8698 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -255,80 +255,79 @@ 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 pstate = - if List.exists Option.is_empty fixdefs then - (* Some bodies to define by proof *) - let thms = - List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps)))) - fixnames fixtypes fiximps in - let init_tac = - 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 (local,poly,DefinitionBody Fixpoint) - evd pl (Some(false,indexes,init_tac)) thms None) - else begin - (* We shortcut the proof process *) - let fixdefs = List.map Option.get fixdefs in - let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in - let env = Global.env() in - let indexes = search_guard env indexes fixdecls in - let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in - let fixdecls = - List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in - let evd = Evd.from_ctx ctx in - let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl ~poly evd pl in - let pl = Evd.universe_binders evd in - let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in - ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) - fixnames fixdecls fixtypes fiximps); - (* Declare the recursive definitions *) - fixpoint_message (Some indexes) fixnames; - None - end in - (* Declare notations *) - List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; +let declare_fixpoint_notations ntns = + List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns + +let declare_fixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = + (* Some bodies to define by proof *) + let thms = + List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps)))) + fixnames fixtypes fiximps in + let init_tac = + Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) + fixdefs) in + let evd = Evd.from_ctx ctx in + let pstate = Lemmas.start_proof_with_initialization (local,poly,DefinitionBody Fixpoint) + evd pl (Some(false,indexes,init_tac)) thms None in + declare_fixpoint_notations ntns; pstate -let declare_cofixpoint ~ontop 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 *) - let thms = - List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps)))) - fixnames fixtypes fiximps in - let init_tac = - 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) - evd pl (Some(true,[],init_tac)) thms None) - else begin - (* We shortcut the proof process *) - let fixdefs = List.map Option.get fixdefs in - let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in - let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let vars = Vars.universes_of_constr (List.hd fixdecls) in - let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in - let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in - let evd = Evd.from_ctx ctx in - let evd = Evd.restrict_universe_context evd vars in - let ctx = Evd.check_univ_decl ~poly evd pl in - let pl = Evd.universe_binders evd in - ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) - fixnames fixdecls fixtypes fiximps); - (* Declare the recursive definitions *) - cofixpoint_message fixnames; - None - end in - (* Declare notations *) - List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; +let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = + (* We shortcut the proof process *) + let fixdefs = List.map Option.get fixdefs in + let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in + let env = Global.env() in + let indexes = search_guard env indexes fixdecls in + let fiximps = List.map (fun (n,r,p) -> r) fiximps in + let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in + let fixdecls = + List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in + let evd = Evd.from_ctx ctx in + let evd = Evd.restrict_universe_context evd vars in + let ctx = Evd.check_univ_decl ~poly evd pl in + let pl = Evd.universe_binders evd in + let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in + ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) + fixnames fixdecls fixtypes fiximps); + (* Declare the recursive definitions *) + fixpoint_message (Some indexes) fixnames; + declare_fixpoint_notations ntns + +let declare_cofixpoint_notations = declare_fixpoint_notations + +let declare_cofixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = + (* Some bodies to define by proof *) + let thms = + List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps)))) + fixnames fixtypes fiximps in + let init_tac = + Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) + fixdefs) in + let evd = Evd.from_ctx ctx in + let pstate = Lemmas.start_proof_with_initialization + (Global,poly, DefinitionBody CoFixpoint) + evd pl (Some(true,[],init_tac)) thms None in + declare_cofixpoint_notations ntns; pstate +let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns = + (* We shortcut the proof process *) + let fixdefs = List.map Option.get fixdefs in + let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in + let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in + let vars = Vars.universes_of_constr (List.hd fixdecls) in + let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in + let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in + let evd = Evd.from_ctx ctx in + let evd = Evd.restrict_universe_context evd vars in + let ctx = Evd.check_univ_decl ~poly evd pl in + let pl = Evd.universe_binders evd in + ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) + fixnames fixdecls fixtypes fiximps); + (* Declare the recursive definitions *) + cofixpoint_message fixnames; + declare_cofixpoint_notations ntns + let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with | CStructRec na -> na | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na @@ -366,18 +365,33 @@ 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_common 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 + fixl, ntns, fix, List.map compute_possible_guardness_evidences info + +let do_fixpoint_interactive local poly l = + let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in + let pstate = declare_fixpoint_interactive 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_fixpoint local poly l = + let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in + declare_fixpoint local poly fix possible_indexes ntns; + if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () + +let do_cofixpoint_common 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 + ntns, interp_fixpoint ~cofix:true fixl ntns + +let do_cofixpoint_interactive local poly l = + let ntns, cofix = do_cofixpoint_common l in + let pstate = declare_cofixpoint_interactive local poly cofix ntns in if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); pstate + +let do_cofixpoint local poly l = + let ntns, cofix = do_cofixpoint_common l in + declare_cofixpoint local poly cofix ntns; + if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 5937842f17..c8d617da5f 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -18,15 +18,17 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) +val do_fixpoint_interactive : + locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Proof_global.t + 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 -> unit + +val do_cofixpoint_interactive : + locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Proof_global.t 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 -> unit (************************************************************************) (** Internal API *) @@ -83,20 +85,16 @@ 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.lemma_possible_guards -> decl_notation list -> unit 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 + decl_notation list -> unit (** Very private function, do not use *) val compute_possible_guardness_evidences : diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 5eec8aed1e..63e6dd247f 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -50,7 +50,6 @@ let def_body = Entry.create "vernac:def_body" let decl_notation = Entry.create "vernac:decl_notation" let record_field = Entry.create "vernac:record_field" let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion" -let instance_name = Entry.create "vernac:instance_name" let section_subset_expr = Entry.create "vernac:section_subset_expr" let make_bullet s = @@ -683,7 +682,7 @@ END (* Extensions: implicits, coercions, etc. *) GRAMMAR EXTEND Gram - GLOBAL: gallina_ext instance_name hint_info; + GLOBAL: gallina_ext hint_info; gallina_ext: [ [ (* Transparent and Opaque *) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 740b9031cc..d14c7ddf8f 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -207,12 +207,8 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes let default_thm_id = Id.of_string "Unnamed_thm" -let fresh_name_for_anonymous_theorem ~pstate = - let avoid = match pstate with - | None -> Id.Set.empty - | Some pstate -> Id.Set.of_list (Proof_global.get_all_proof_names pstate) - in - next_global_ident_away default_thm_id avoid +let fresh_name_for_anonymous_theorem () = + next_global_ident_away default_thm_id Id.Set.empty let check_name_freshness locality {CAst.loc;v=id} : unit = (* We check existence here: it's a bit late at Qed time *) @@ -329,7 +325,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 +336,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 +352,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 +384,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 +423,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 +483,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..3df543156d 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -37,7 +37,7 @@ 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 -> @@ -45,12 +45,11 @@ val start_proof : ontop:Proof_global.t option -> Id.t -> ?pl:UState.universe_dec 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 -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 -> @@ -62,7 +61,7 @@ val standard_proof_terminator : ?hook:declaration_hook -> Proof_global.lemma_possible_guards -> Proof_global.proof_terminator -val fresh_name_for_anonymous_theorem : pstate:Proof_global.t option -> Id.t +val fresh_name_for_anonymous_theorem : unit -> Id.t (* Prepare global named context for proof session: remove proofs of opaque section definitions and remove vm-compiled code *) @@ -78,7 +77,13 @@ val save_proof_admitted val save_proof_proved : ?proof:Proof_global.closed_proof - -> ?pstate:Proof_global.t + -> ?ontop:Proof_global.stack -> opaque:Proof_global.opacity_flag -> idopt:Names.lident option - -> Proof_global.t option + -> Proof_global.stack option + +val save_pstate_proved + : pstate:Proof_global.t + -> 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..3b77039de5 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -86,14 +86,12 @@ 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 val next_obligation - : ontop:Proof_global.t option - -> Names.Id.t option + : Names.Id.t option -> Genarg.glob_generic_argument option -> Proof_global.t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 337cb233a2..18e0fde296 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -47,15 +47,20 @@ let vernac_pperr_endline pp = let there_are_pending_proofs ~pstate = not Option.(is_empty pstate) -let check_no_pending_proof ~pstate = - if there_are_pending_proofs ~pstate then - user_err Pp.(str "Command not supported (Open proofs remain)") - +(* EJGA: Only used in close_proof 2, can remove once ?proof hack is away *) let vernac_require_open_proof ~pstate f = match pstate with | Some pstate -> f ~pstate | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)") +let with_pstate ~pstate f = + vernac_require_open_proof ~pstate + (fun ~pstate -> f ~pstate:(Proof_global.get_current_pstate pstate)) + + let modify_pstate ~pstate f = + vernac_require_open_proof ~pstate (fun ~pstate -> + Some (Proof_global.modify_current_pstate (fun pstate -> f ~pstate) pstate)) + let get_current_or_global_context ~pstate = match pstate with | None -> let env = Global.env () in Evd.(from_env env, env) @@ -91,6 +96,25 @@ module DefAttributes = struct { polymorphic; program; locality; deprecated } end +let with_locality ~atts f = + let local = Attributes.(parse locality atts) in + f ~local + +let with_section_locality ~atts f = + let local = Attributes.(parse locality atts) in + let section_local = make_section_locality local in + f ~section_local + +let with_module_locality ~atts f = + let local = Attributes.(parse locality atts) in + let module_local = make_module_locality local in + f ~module_local + +let with_def_attributes ~atts f = + let atts = DefAttributes.parse atts in + if atts.DefAttributes.program then Obligations.check_program_libraries (); + f ~atts + (*******************) (* "Show" commands *) @@ -540,7 +564,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 +586,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,60 +597,63 @@ 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_name lid local = + let lid = + match lid with + | { v = Name.Anonymous; loc } -> + CAst.make ?loc (fresh_name_for_anonymous_theorem ()) + | { v = Name.Name n; loc } -> CAst.make ?loc n in + let () = + match local with + | Discharge -> Dumpglob.dump_definition lid true "var" + | Local | Global -> Dumpglob.dump_definition lid false "def" + in + lid + +let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let open DefAttributes in let local = enforce_locality_exp atts.locality discharge in let hook = vernac_definition_hook atts.polymorphic kind in - let () = - match id with - | Anonymous -> () - | Name n -> let lid = CAst.make ?loc n in - match local with - | Discharge -> Dumpglob.dump_definition lid true "var" - | Local | Global -> Dumpglob.dump_definition lid false "def" - in let program_mode = atts.program in - let name = - match id with - | Anonymous -> fresh_name_for_anonymous_theorem ~pstate - | Name n -> n - in - (match def with - | ProveBody (bl,t) -> (* local binders, typ *) - Some (start_proof_and_print ~program_mode ~pstate (local, atts.polymorphic, DefinitionBody kind) - ?hook [(CAst.make ?loc name, pl), (bl, t)]) - | DefineBody (bl,red_option,c,typ_opt) -> - let red_option = match red_option with - | None -> None - | Some r -> - let sigma, env = get_current_or_global_context ~pstate in - 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 - ) + let name = vernac_definition_name lid local in + start_proof_and_print ~program_mode (local, atts.polymorphic, DefinitionBody kind) ?hook [(name, pl), (bl, t)] -let vernac_start_proof ~atts ~pstate kind l = +let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt = + let open DefAttributes in + let local = enforce_locality_exp atts.locality discharge in + let hook = vernac_definition_hook atts.polymorphic kind in + let program_mode = atts.program in + let name = vernac_definition_name lid local in + let red_option = match red_option with + | None -> None + | Some r -> + let env = Global.env () in + let sigma = Evd.from_env env in + Some (snd (Hook.get f_interp_redexp env sigma r)) in + ComDefinition.do_definition ~program_mode name.v + (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook + +(* NB: pstate argument to use combinators easily *) +let vernac_start_proof ~atts kind l = 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) + 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 = (* 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 - if not status then Feedback.feedback Feedback.AddedAxiom; - pstate + let () = save_pstate_proved ~pstate ~opaque:Proof_global.Opaque ~idopt:None in + if not status then Feedback.feedback Feedback.AddedAxiom let vernac_assumption ~atts discharge kind l nl = let open DefAttributes in @@ -804,30 +831,46 @@ 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 open DefAttributes in - let local = enforce_locality_exp atts.locality discharge in +let vernac_fixpoint_common ~atts discharge l = if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - (* XXX: Switch to the attribute system and match on ~atts *) - let do_fixpoint = if atts.program then - fun local sign l -> ComProgramFixpoint.do_fixpoint local sign l; None - else - ComFixpoint.do_fixpoint ~ontop:pstate - in - do_fixpoint local atts.polymorphic l + enforce_locality_exp atts.DefAttributes.locality discharge -let vernac_cofixpoint ~atts ~pstate discharge l = +let vernac_fixpoint_interactive ~atts discharge l = let open DefAttributes in - let local = enforce_locality_exp atts.locality discharge in + let local = vernac_fixpoint_common ~atts discharge l in + if atts.program then + CErrors.user_err Pp.(str"Program Fixpoint requires a body"); + ComFixpoint.do_fixpoint_interactive local atts.polymorphic l + +let vernac_fixpoint ~atts discharge l = + let open DefAttributes in + let local = vernac_fixpoint_common ~atts discharge l in + if atts.program then + (* XXX: Switch to the attribute system and match on ~atts *) + ComProgramFixpoint.do_fixpoint local atts.polymorphic l + else + ComFixpoint.do_fixpoint local atts.polymorphic l + +let vernac_cofixpoint_common ~atts discharge l = if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") 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 - in - do_cofixpoint local atts.polymorphic l + enforce_locality_exp atts.DefAttributes.locality discharge + +let vernac_cofixpoint_interactive ~atts discharge l = + let open DefAttributes in + let local = vernac_cofixpoint_common ~atts discharge l in + if atts.program then + CErrors.user_err Pp.(str"Program CoFixpoint requires a body"); + ComFixpoint.do_cofixpoint_interactive local atts.polymorphic l + +let vernac_cofixpoint ~atts discharge l = + let open DefAttributes in + let local = vernac_cofixpoint_common ~atts discharge l in + if atts.program then + ComProgramFixpoint.do_cofixpoint local atts.polymorphic l + else + ComFixpoint.do_cofixpoint local atts.polymorphic l let vernac_scheme l = if Dumpglob.dump () then @@ -883,14 +926,13 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export -let vernac_define_module ~pstate export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l = +let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then user_err Pp.(str "Modules and Module Types are not allowed inside sections."); match mexpr_ast_l with | [] -> - check_no_pending_proof ~pstate; let binders_ast,argsexport = List.fold_right (fun (export,idl,ty) (args,argsexport) -> @@ -930,13 +972,12 @@ let vernac_end_module export {loc;v=id} = Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined"); Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export -let vernac_declare_module_type ~pstate {loc;v=id} binders_ast mty_sign mty_ast_l = +let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = if Lib.sections_are_opened () then user_err Pp.(str "Modules and Module Types are not allowed inside sections."); match mty_ast_l with | [] -> - check_no_pending_proof ~pstate; let binders_ast,argsexport = List.fold_right (fun (export,idl,ty) (args,argsexport) -> @@ -983,8 +1024,7 @@ let vernac_include l = (* Sections *) -let vernac_begin_section ~pstate ({v=id} as lid) = - check_no_pending_proof ~pstate; +let vernac_begin_section ({v=id} as lid) = Dumpglob.dump_definition lid true "sec"; Lib.open_section id @@ -997,8 +1037,7 @@ let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set (* Dispatcher of the "End" command *) -let vernac_end_segment ~pstate ({v=id} as lid) = - check_no_pending_proof ~pstate; +let vernac_end_segment ({v=id} as lid) = match Lib.find_opening_node id with | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid @@ -1058,18 +1097,42 @@ let vernac_identity_coercion ~atts id qids qidt = (* Type classes *) -let vernac_instance ~atts name bl t props pri = - let open DefAttributes in - let global = not (make_section_locality atts.locality) in +let vernac_instance_program ~atts name bl t props info = Dumpglob.dump_constraint (fst name) false "inst"; - let program_mode = atts.program in - Classes.new_instance ~program_mode ~global atts.polymorphic name bl t props pri + let (program, locality), polymorphic = + Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + in + let global = not (make_section_locality locality) in + let _id : Id.t = Classes.new_instance_program ~global polymorphic name bl t props info in + () + +let vernac_instance_interactive ~atts name bl t info = + Dumpglob.dump_constraint (fst name) false "inst"; + let (program, locality), polymorphic = + Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + in + let global = not (make_section_locality locality) in + let _id, pstate = + Classes.new_instance_interactive ~global polymorphic name bl t info in + pstate + +let vernac_instance ~atts name bl t props info = + Dumpglob.dump_constraint (fst name) false "inst"; + let (program, locality), polymorphic = + Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + in + let global = not (make_section_locality locality) in + let _id : Id.t = + Classes.new_instance ~global polymorphic name bl t props info in + () let vernac_declare_instance ~atts id bl inst pri = - let open DefAttributes in - let global = not (make_section_locality atts.locality) in Dumpglob.dump_definition (fst id) false "inst"; - Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic id bl inst pri + let (program, locality), polymorphic = + Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + in + let global = not (make_section_locality locality) in + Classes.declare_new_instance ~program_mode:program ~global polymorphic id bl inst pri let vernac_context ~poly l = if not (ComAssumption.context poly l) then Feedback.feedback Feedback.AddedAxiom @@ -1094,7 +1157,7 @@ let focus_command_cond = Proof.no_cond command_focus all tactics fail if there are no further goals to prove. *) let vernac_solve_existential ~pstate n com = - Proof_global.simple_with_current_proof (fun _ p -> + Proof_global.modify_proof (fun p -> let intern env sigma = Constrintern.intern_constr env sigma com in Proof.V82.instantiate_evar (Global.env ()) n intern p) pstate @@ -1118,9 +1181,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 *) @@ -1928,7 +1989,7 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = let sigma, env = get_current_or_global_context ~pstate in print_about env sigma ref_or_by_not udecl -let vernac_print ~(pstate : Proof_global.t option) ~atts = +let vernac_print ~pstate ~atts = let sigma, env = get_current_or_global_context ~pstate in function | PrintTables -> print_tables () @@ -2085,10 +2146,8 @@ let vernac_locate ~pstate = function | LocateOther (s, qid) -> print_located_other s qid | LocateFile f -> locate_file f -let vernac_register ~pstate qid r = +let vernac_register qid r = let gr = Smartlocate.global_with_alias qid in - if there_are_pending_proofs ~pstate then - user_err Pp.(str "Cannot register a primitive while in proof editing mode."); match r with | RegisterInline -> begin match gr with @@ -2116,19 +2175,21 @@ let vernac_register ~pstate qid r = (********************) (* Proof management *) -let vernac_focus gln = - Proof_global.simple_with_current_proof (fun _ p -> +let vernac_focus ~pstate gln = + Proof_global.modify_proof (fun p -> match gln with | None -> Proof.focus focus_command_cond () 1 p | Some 0 -> user_err Pp.(str "Invalid goal number: 0. Goal numbering starts with 1.") | Some n -> Proof.focus focus_command_cond () n p) + pstate (* Unfocuses one step in the focus stack. *) -let vernac_unfocus () = - Proof_global.simple_with_current_proof - (fun _ p -> Proof.unfocus command_focus p ()) +let vernac_unfocus ~pstate = + Proof_global.modify_proof + (fun p -> Proof.unfocus command_focus p ()) + pstate (* Checks that a proof is fully unfocused. Raises an error if not. *) let vernac_unfocused ~pstate = @@ -2145,29 +2206,33 @@ let vernac_unfocused ~pstate = let subproof_kind = Proof.new_focus_kind () let subproof_cond = Proof.done_cond subproof_kind -let vernac_subproof gln = - Proof_global.simple_with_current_proof (fun _ p -> +let vernac_subproof gln ~pstate = + Proof_global.modify_proof (fun p -> match gln with | None -> Proof.focus subproof_cond () 1 p | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p | Some (Goal_select.SelectId id) -> Proof.focus_id subproof_cond () id p | _ -> user_err ~hdr:"bracket_selector" (str "Brackets do not support multi-goal selectors.")) + pstate -let vernac_end_subproof () = - Proof_global.simple_with_current_proof (fun _ p -> - Proof.unfocus subproof_kind p ()) +let vernac_end_subproof ~pstate = + Proof_global.modify_proof (fun p -> + Proof.unfocus subproof_kind p ()) + pstate -let vernac_bullet (bullet : Proof_bullet.t) = - Proof_global.simple_with_current_proof (fun _ p -> - Proof_bullet.put p bullet) +let vernac_bullet (bullet : Proof_bullet.t) ~pstate = + Proof_global.modify_proof (fun p -> + Proof_bullet.put p bullet) pstate +(* Stack is needed due to show proof names, should deprecate / remove + and take pstate *) let vernac_show ~pstate = match pstate 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.") @@ -2185,7 +2250,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) + Id.print (Proof_global.get_current_proof_name pstate) | ShowIntros all -> show_intro ~pstate all | ShowProof -> show_proof ~pstate:(Some pstate) | ShowMatch id -> show_match id @@ -2203,26 +2268,6 @@ let vernac_check_guard ~pstate = (str ("Condition violated: ") ++s) in message -(* Attributes *) -let with_locality ~atts f = - let local = Attributes.(parse locality atts) in - f ~local - -let with_section_locality ~atts f = - let local = Attributes.(parse locality atts) in - let section_local = make_section_locality local in - f ~section_local - -let with_module_locality ~atts f = - let local = Attributes.(parse locality atts) in - let module_local = make_module_locality local in - f ~module_local - -let with_def_attributes ~atts f = - let atts = DefAttributes.parse atts in - if atts.DefAttributes.program then Obligations.check_program_libraries (); - f ~atts - (** A global default timeout, controlled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) @@ -2277,338 +2322,388 @@ let locate_if_not_already ?loc (e, info) = exception End_of_input -(* "locality" is the prefix "Local" attribute, while the "local" component - * is the outdated/deprecated "Local" attribute of some vernacular commands - * still parsed as the obsolete_locality grammar entry for retrocompatibility. - * loc is the Loc.t of the vernacular command being interpreted. *) -let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = - let pstate = st.Vernacstate.proof in - vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); +let interp_typed_vernac c ~pstate = + let open Proof_global in + let open Vernacextend in match c with - - (* The STM should handle that, but LOAD bypasses the STM... *) - | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command") - | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command") - | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command") - | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command") - - (* Resetting *) - | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") - | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") - | VernacBack _ -> anomaly (str "VernacBack not handled by Stm.") - | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm.") - - (* This one is possible to handle here *) - | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") - - (* Loading a file requires access to the control interpreter so - [vernac_load] is mutually-recursive with [interp_expr] *) - | VernacLoad (verbosely,fname) -> - unsupported_attributes atts; - vernac_load ?proof ~verbosely ~st fname - + | VtDefault f -> f (); pstate + | VtNoProof f -> + if there_are_pending_proofs ~pstate then + user_err Pp.(str "Command not supported (Open proofs remain)"); + let () = f () in + pstate + | VtCloseProof f -> + vernac_require_open_proof ~pstate (fun ~pstate -> + f ~pstate:(Proof_global.get_current_pstate pstate); + Proof_global.discard_current pstate) + | VtOpenProof f -> + Some (push ~ontop:pstate (f ())) + | VtModifyProof f -> + modify_pstate f ~pstate + | VtReadProofOpt f -> + f ~pstate:(Option.map get_current_pstate pstate); + pstate + | VtReadProof f -> + with_pstate ~pstate f; + pstate + +(* We interpret vernacular commands to a DSL that specifies their + allowed actions on proof states *) +let translate_vernac ~atts v = let open Vernacextend in match v with + | VernacEndProof _ + | VernacAbortAll + | VernacRestart + | VernacUndo _ + | VernacUndoTo _ + | VernacResetName _ + | VernacResetInitial + | VernacBack _ + | VernacBackTo _ + | VernacAbort _ + | VernacLoad _ -> + anomaly (str "type_vernac") (* Syntax *) | VernacSyntaxExtension (infix, sl) -> - with_module_locality ~atts vernac_syntax_extension infix sl; - pstate + VtDefault(fun () -> with_module_locality ~atts vernac_syntax_extension infix sl) | VernacDeclareScope sc -> - with_module_locality ~atts vernac_declare_scope sc; - pstate + VtDefault(fun () -> with_module_locality ~atts vernac_declare_scope sc) | VernacDelimiters (sc,lr) -> - with_module_locality ~atts vernac_delimiters sc lr; - pstate + VtDefault(fun () -> with_module_locality ~atts vernac_delimiters sc lr) | VernacBindScope (sc,rl) -> - with_module_locality ~atts vernac_bind_scope sc rl; - pstate + VtDefault(fun () -> with_module_locality ~atts vernac_bind_scope sc rl) | VernacOpenCloseScope (b, s) -> - with_section_locality ~atts vernac_open_close_scope (b,s); - pstate + VtDefault(fun () -> with_section_locality ~atts vernac_open_close_scope (b,s)) | VernacInfix (mv,qid,sc) -> - with_module_locality ~atts vernac_infix mv qid sc; - pstate + VtDefault(fun () -> with_module_locality ~atts vernac_infix mv qid sc) | VernacNotation (c,infpl,sc) -> - with_module_locality ~atts vernac_notation c infpl sc; - pstate + VtDefault(fun () -> with_module_locality ~atts vernac_notation c infpl sc) | VernacNotationAddFormat(n,k,v) -> - unsupported_attributes atts; - Metasyntax.add_notation_extra_printing_rule n k v; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + Metasyntax.add_notation_extra_printing_rule n k v) | VernacDeclareCustomEntry s -> - with_module_locality ~atts vernac_custom_entry s; - pstate + VtDefault(fun () -> with_module_locality ~atts vernac_custom_entry s) (* Gallina *) - | VernacDefinition ((discharge,kind),lid,d) -> - with_def_attributes ~atts vernac_definition ~pstate discharge kind lid d + + | VernacDefinition (discharge,lid,DefineBody (bl,red_option,c,typ)) -> + VtDefault (fun () -> + with_def_attributes ~atts + vernac_definition discharge lid bl red_option c typ) + | VernacDefinition (discharge,lid,ProveBody(bl,typ)) -> + VtOpenProof(fun () -> + with_def_attributes ~atts + vernac_definition_interactive discharge lid bl typ) + | VernacStartTheoremProof (k,l) -> - with_def_attributes ~atts vernac_start_proof ~pstate k l - | VernacEndProof e -> - unsupported_attributes atts; - vernac_end_proof ?proof ?pstate e + VtOpenProof(fun () -> with_def_attributes ~atts vernac_start_proof k l) | VernacExactProof c -> - unsupported_attributes atts; - vernac_require_open_proof ~pstate (vernac_exact_proof c) + VtCloseProof(fun ~pstate -> + unsupported_attributes atts; + vernac_exact_proof ~pstate c) + + | VernacDefineModule (export,lid,bl,mtys,mexprl) -> + let i () = + unsupported_attributes atts; + vernac_define_module export lid bl mtys mexprl in + (* XXX: We should investigate if eventually this should be made + VtNoProof in all cases. *) + if List.is_empty mexprl then VtNoProof i else VtDefault i + + | VernacDeclareModuleType (lid,bl,mtys,mtyo) -> + VtNoProof(fun () -> + unsupported_attributes atts; + vernac_declare_module_type lid bl mtys mtyo) | VernacAssumption ((discharge,kind),nl,l) -> - with_def_attributes ~atts vernac_assumption discharge kind l nl; - pstate + VtDefault(fun () -> with_def_attributes ~atts vernac_assumption discharge kind l nl) | VernacInductive (cum, priv, finite, l) -> - vernac_inductive ~atts cum priv finite l; - pstate + VtDefault(fun () -> vernac_inductive ~atts cum priv finite l) | VernacFixpoint (discharge, l) -> - with_def_attributes ~atts vernac_fixpoint ~pstate discharge l + let opens = List.exists (fun ((_,_,_,_,p),_) -> Option.is_empty p) l in + if opens then + VtOpenProof (fun () -> + with_def_attributes ~atts vernac_fixpoint_interactive discharge l) + else + VtDefault (fun () -> + with_def_attributes ~atts vernac_fixpoint discharge l) | VernacCoFixpoint (discharge, l) -> - with_def_attributes ~atts vernac_cofixpoint ~pstate discharge l + let opens = List.exists (fun ((_,_,_,p),_) -> Option.is_empty p) l in + if opens then + VtOpenProof(fun () -> with_def_attributes ~atts vernac_cofixpoint_interactive discharge l) + else + VtDefault(fun () -> with_def_attributes ~atts vernac_cofixpoint discharge l) + | VernacScheme l -> - unsupported_attributes atts; - vernac_scheme l; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_scheme l) | VernacCombinedScheme (id, l) -> - unsupported_attributes atts; - vernac_combined_scheme id l; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_combined_scheme id l) | VernacUniverse l -> - vernac_universe ~poly:(only_polymorphism atts) l; - pstate + VtDefault(fun () -> vernac_universe ~poly:(only_polymorphism atts) l) | VernacConstraint l -> - vernac_constraint ~poly:(only_polymorphism atts) l; - pstate + VtDefault(fun () -> vernac_constraint ~poly:(only_polymorphism atts) l) (* Modules *) | VernacDeclareModule (export,lid,bl,mtyo) -> - unsupported_attributes atts; - vernac_declare_module export lid bl mtyo; - pstate - | VernacDefineModule (export,lid,bl,mtys,mexprl) -> - unsupported_attributes atts; - vernac_define_module ~pstate export lid bl mtys mexprl; - pstate - | VernacDeclareModuleType (lid,bl,mtys,mtyo) -> - unsupported_attributes atts; - vernac_declare_module_type ~pstate lid bl mtys mtyo; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_declare_module export lid bl mtyo) | VernacInclude in_asts -> - unsupported_attributes atts; - vernac_include in_asts; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_include in_asts) (* Gallina extensions *) | VernacBeginSection lid -> - unsupported_attributes atts; - vernac_begin_section ~pstate lid; - pstate - + VtNoProof(fun () -> + unsupported_attributes atts; + vernac_begin_section lid) | VernacEndSegment lid -> - unsupported_attributes atts; - vernac_end_segment ~pstate lid; - pstate - + VtNoProof(fun () -> + unsupported_attributes atts; + vernac_end_segment lid) | VernacNameSectionHypSet (lid, set) -> - unsupported_attributes atts; - vernac_name_sec_hyp lid set; - pstate - + VtDefault(fun () -> + unsupported_attributes atts; + vernac_name_sec_hyp lid set) | VernacRequire (from, export, qidl) -> - unsupported_attributes atts; - vernac_require from export qidl; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_require from export qidl) | VernacImport (export,qidl) -> - unsupported_attributes atts; - vernac_import export qidl; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_import export qidl) | VernacCanonical qid -> - unsupported_attributes atts; - vernac_canonical qid; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_canonical qid) | VernacCoercion (r,s,t) -> - vernac_coercion ~atts r s t; - pstate + VtDefault(fun () -> vernac_coercion ~atts r s t) | VernacIdentityCoercion ({v=id},s,t) -> - vernac_identity_coercion ~atts id s t; - pstate + VtDefault(fun () -> vernac_identity_coercion ~atts id s t) (* Type classes *) | VernacInstance (name, bl, t, props, info) -> - snd @@ with_def_attributes ~atts (vernac_instance ~pstate name bl t props info) + let { DefAttributes.program } = DefAttributes.parse atts in + if program then + VtDefault (fun () -> vernac_instance_program ~atts name bl t props info) + else begin match props with + | None -> + VtOpenProof(fun () -> + vernac_instance_interactive ~atts name bl t info) + | Some props -> + VtDefault(fun () -> + vernac_instance ~atts name bl t props info) + end + | VernacDeclareInstance (id, bl, inst, info) -> - with_def_attributes ~atts vernac_declare_instance id bl inst info; - pstate + VtDefault(fun () -> vernac_declare_instance ~atts id bl inst info) | VernacContext sup -> - let () = vernac_context ~poly:(only_polymorphism atts) sup in - pstate + VtDefault(fun () -> vernac_context ~poly:(only_polymorphism atts) sup) | VernacExistingInstance insts -> - with_section_locality ~atts vernac_existing_instance insts; - pstate + VtDefault(fun () -> with_section_locality ~atts vernac_existing_instance insts) | VernacExistingClass id -> - unsupported_attributes atts; - vernac_existing_class id; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_existing_class id) (* Solving *) | VernacSolveExistential (n,c) -> - unsupported_attributes atts; - Some (vernac_require_open_proof ~pstate (vernac_solve_existential n c)) - + VtModifyProof(fun ~pstate -> + unsupported_attributes atts; + vernac_solve_existential ~pstate n c) (* Auxiliary file and library management *) | VernacAddLoadPath (isrec,s,alias) -> - unsupported_attributes atts; - vernac_add_loadpath isrec s alias; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_add_loadpath isrec s alias) | VernacRemoveLoadPath s -> - unsupported_attributes atts; - vernac_remove_loadpath s; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_remove_loadpath s) | VernacAddMLPath (isrec,s) -> - unsupported_attributes atts; - vernac_add_ml_path isrec s; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_add_ml_path isrec s) | VernacDeclareMLModule l -> - with_locality ~atts vernac_declare_ml_module l; - pstate + VtDefault(fun () -> with_locality ~atts vernac_declare_ml_module l) | VernacChdir s -> - unsupported_attributes atts; - vernac_chdir s; - pstate + VtDefault(fun () -> unsupported_attributes atts; vernac_chdir s) (* State management *) | VernacWriteState s -> - unsupported_attributes atts; - vernac_write_state s; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_write_state s) | VernacRestoreState s -> - unsupported_attributes atts; - vernac_restore_state s; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_restore_state s) (* Commands *) | VernacCreateHintDb (dbname,b) -> - with_module_locality ~atts vernac_create_hintdb dbname b; - pstate + VtDefault(fun () -> + with_module_locality ~atts vernac_create_hintdb dbname b) | VernacRemoveHints (dbnames,ids) -> - with_module_locality ~atts vernac_remove_hints dbnames ids; - pstate + VtDefault(fun () -> + with_module_locality ~atts vernac_remove_hints dbnames ids) | VernacHints (dbnames,hints) -> - vernac_hints ~atts dbnames hints; - pstate + VtDefault(fun () -> + vernac_hints ~atts dbnames hints) | VernacSyntacticDefinition (id,c,b) -> - with_module_locality ~atts vernac_syntactic_definition id c b; - pstate - | VernacArguments (qid, args, more_implicits, nargs, nargs_before_bidi, flags) -> - with_section_locality ~atts vernac_arguments qid args more_implicits nargs nargs_before_bidi flags; - pstate + VtDefault(fun () -> + with_module_locality ~atts vernac_syntactic_definition id c b) + | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) -> + VtDefault(fun () -> + with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags)) | VernacReserve bl -> - unsupported_attributes atts; - vernac_reserve bl; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_reserve bl) | VernacGeneralizable gen -> - with_locality ~atts vernac_generalizable gen; - pstate + VtDefault(fun () -> with_locality ~atts vernac_generalizable gen) | VernacSetOpacity qidl -> - with_locality ~atts vernac_set_opacity qidl; - pstate + VtDefault(fun () -> with_locality ~atts vernac_set_opacity qidl) | VernacSetStrategy l -> - with_locality ~atts vernac_set_strategy l; - pstate + VtDefault(fun () -> with_locality ~atts vernac_set_strategy l) | VernacSetOption (export, key,v) -> - vernac_set_option ~local:(only_locality atts) export key v; - pstate + VtDefault(fun () -> + vernac_set_option ~local:(only_locality atts) export key v) | VernacRemoveOption (key,v) -> - unsupported_attributes atts; - vernac_remove_option key v; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_remove_option key v) | VernacAddOption (key,v) -> - unsupported_attributes atts; - vernac_add_option key v; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_add_option key v) | VernacMemOption (key,v) -> - unsupported_attributes atts; - vernac_mem_option key v; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_mem_option key v) | VernacPrintOption key -> - unsupported_attributes atts; - vernac_print_option key; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + vernac_print_option key) | VernacCheckMayEval (r,g,c) -> - Feedback.msg_notice @@ - vernac_check_may_eval ~pstate ~atts r g c; - pstate + VtReadProofOpt(fun ~pstate -> + Feedback.msg_notice @@ + vernac_check_may_eval ~pstate ~atts r g c) | VernacDeclareReduction (s,r) -> - with_locality ~atts vernac_declare_reduction s r; - pstate + VtDefault(fun () -> + with_locality ~atts vernac_declare_reduction s r) | VernacGlobalCheck c -> - unsupported_attributes atts; - Feedback.msg_notice @@ vernac_global_check c; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + Feedback.msg_notice @@ vernac_global_check c) | VernacPrint p -> - Feedback.msg_notice @@ vernac_print ~pstate ~atts p; - pstate + VtReadProofOpt(fun ~pstate -> + Feedback.msg_notice @@ vernac_print ~pstate ~atts p) | VernacSearch (s,g,r) -> - unsupported_attributes atts; - vernac_search ~pstate ~atts s g r; - pstate + VtReadProofOpt( + unsupported_attributes atts; + vernac_search ~atts s g r) | VernacLocate l -> unsupported_attributes atts; - Feedback.msg_notice @@ vernac_locate ~pstate l; - pstate + VtReadProofOpt(fun ~pstate -> + Feedback.msg_notice @@ vernac_locate ~pstate l) | VernacRegister (qid, r) -> - unsupported_attributes atts; - vernac_register ~pstate qid r; - pstate + VtNoProof(fun () -> + unsupported_attributes atts; + vernac_register qid r) | VernacPrimitive (id, prim, typopt) -> - unsupported_attributes atts; - ComAssumption.do_primitive id prim typopt; - pstate + VtDefault(fun () -> + unsupported_attributes atts; + ComAssumption.do_primitive id prim typopt) | VernacComments l -> - unsupported_attributes atts; - Flags.if_verbose Feedback.msg_info (str "Comments ok\n"); - pstate - + VtDefault(fun () -> + unsupported_attributes atts; + Flags.if_verbose Feedback.msg_info (str "Comments ok\n")) (* Proof management *) | VernacFocus n -> - unsupported_attributes atts; - Option.map (vernac_focus n) pstate + VtModifyProof(unsupported_attributes atts;vernac_focus n) | VernacUnfocus -> - unsupported_attributes atts; - Option.map (vernac_unfocus ()) pstate + VtModifyProof(unsupported_attributes atts;vernac_unfocus) | VernacUnfocused -> - unsupported_attributes atts; - Option.iter (fun pstate -> Feedback.msg_notice @@ vernac_unfocused ~pstate) pstate; - pstate + VtReadProof(fun ~pstate -> + unsupported_attributes atts; + Feedback.msg_notice @@ vernac_unfocused ~pstate) | VernacBullet b -> - unsupported_attributes atts; - Option.map (vernac_bullet b) pstate + VtModifyProof( + unsupported_attributes atts; + vernac_bullet b) | VernacSubproof n -> - unsupported_attributes atts; - Option.map (vernac_subproof n) pstate + VtModifyProof( + unsupported_attributes atts; + vernac_subproof n) | VernacEndSubproof -> - unsupported_attributes atts; - Option.map (vernac_end_subproof ()) pstate + VtModifyProof( + unsupported_attributes atts; + vernac_end_subproof) | VernacShow s -> - unsupported_attributes atts; - Feedback.msg_notice @@ vernac_show ~pstate s; - pstate + VtReadProofOpt(fun ~pstate -> + unsupported_attributes atts; + Feedback.msg_notice @@ vernac_show ~pstate s) | VernacCheckGuard -> - unsupported_attributes atts; - Feedback.msg_notice @@ - vernac_require_open_proof ~pstate (vernac_check_guard); - pstate + VtReadProof(fun ~pstate -> + unsupported_attributes atts; + Feedback.msg_notice @@ vernac_check_guard ~pstate) | VernacProof (tac, using) -> + VtModifyProof(fun ~pstate -> unsupported_attributes atts; let using = Option.append using (Proof_using.get_default_proof_using ()) in let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in 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 -> - let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in - Option.cata (vernac_set_used_variables ~pstate) pstate using) - in Some pstate + let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in + Option.cata (vernac_set_used_variables ~pstate) pstate using) | VernacProofMode mn -> - unsupported_attributes atts; - pstate + VtDefault(fun () -> unsupported_attributes atts) (* Extensions *) | VernacExtend (opn,args) -> - (* XXX: Here we are returning the state! :) *) - let st : Vernacstate.t = Vernacextend.call ~atts opn args ~st in - st.Vernacstate.proof + Vernacextend.type_vernac ~atts opn args + +(* "locality" is the prefix "Local" attribute, while the "local" component + * is the outdated/deprecated "Local" attribute of some vernacular commands + * still parsed as the obsolete_locality grammar entry for retrocompatibility. + * loc is the Loc.t of the vernacular command being interpreted. *) +let rec interp_expr ?proof ~atts ~st c = + let pstate = st.Vernacstate.proof in + vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c); + match c with + + (* The STM should handle that, but LOAD bypasses the STM... *) + | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command") + | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command") + | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command") + | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command") + + (* Resetting *) + | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm.") + | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.") + | VernacBack _ -> anomaly (str "VernacBack not handled by Stm.") + | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm.") + + (* This one is possible to handle here *) + | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") + + (* Loading a file requires access to the control interpreter so + [vernac_load] is mutually-recursive with [interp_expr] *) + | VernacLoad (verbosely,fname) -> + unsupported_attributes atts; + vernac_load ?proof ~verbosely ~st fname + + (* Special: ?proof parameter doesn't allow for uniform pstate pop :S *) + | VernacEndProof e -> + unsupported_attributes atts; + vernac_end_proof ?proof ?pstate e + + | v -> + let fv = translate_vernac ~atts v in + interp_typed_vernac ~pstate fv (* XXX: This won't properly set the proof mode, as of today, it is controlled by the STM. Thus, we would need access information from diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 12451370c8..d94ddc1aaf 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -42,7 +42,11 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr Evd.evar_map * Redexpr.red_expr) Hook.t (** Helper *) -val vernac_require_open_proof : pstate:Proof_global.t option -> (pstate:Proof_global.t -> 'a) -> 'a +val vernac_require_open_proof : pstate:Proof_global.stack option -> (pstate:Proof_global.stack -> 'a) -> 'a + +val with_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.t -> 'a) -> 'a + +val modify_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.t -> Proof_global.t) -> Proof_global.stack option (* Flag set when the test-suite is called. Its only effect to display verbose information for `Fail` *) diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 730f5fd6da..6f8a4e8a3c 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -53,14 +53,23 @@ type vernac_when = | VtLater type vernac_classification = vernac_type * vernac_when -type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t +type typed_vernac = + | VtDefault of (unit -> unit) + | VtNoProof of (unit -> unit) + | VtCloseProof of (pstate:Proof_global.t -> unit) + | VtOpenProof of (unit -> Proof_global.t) + | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t) + | VtReadProofOpt of (pstate:Proof_global.t option -> unit) + | VtReadProof of (pstate:Proof_global.t -> unit) + +type vernac_command = atts:Attributes.vernac_flags -> typed_vernac type plugin_args = Genarg.raw_generic_argument list (* Table of vernac entries *) let vernac_tab = (Hashtbl.create 211 : - (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t) + (Vernacexpr.extend_name, bool * (plugin_args -> vernac_command)) Hashtbl.t) let vinterp_add depr s f = try @@ -83,7 +92,7 @@ let warn_deprecated_command = (* Interpretation of a vernac command *) -let call opn converted_args ~atts ~st = +let type_vernac opn converted_args ~atts = let phase = ref "Looking up command" in try let depr, callback = vinterp_map opn in @@ -99,7 +108,7 @@ let call opn converted_args ~atts ~st = phase := "Checking arguments"; let hunk = callback converted_args in phase := "Executing command"; - hunk ~atts ~st + hunk ~atts with | reraise -> let reraise = CErrors.push reraise in @@ -125,7 +134,7 @@ let classify_as_sideeff = VtSideff [], VtLater let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater type (_, _) ty_sig = -| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig +| TyNil : (vernac_command, vernac_classification) ty_sig | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig @@ -151,7 +160,7 @@ let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = functio end (** Stupid GADTs forces us to duplicate the definition just for typing *) -let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function +let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args -> vernac_command = function | TyNil -> fun f args -> begin match args with | [] -> f diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index b37e527f47..60e371a6d9 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -71,18 +71,27 @@ type vernac_classification = vernac_type * vernac_when (** Interpretation of extended vernac phrases. *) -type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t +type typed_vernac = + | VtDefault of (unit -> unit) + | VtNoProof of (unit -> unit) + | VtCloseProof of (pstate:Proof_global.t -> unit) + | VtOpenProof of (unit -> Proof_global.t) + | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t) + | VtReadProofOpt of (pstate:Proof_global.t option -> unit) + | VtReadProof of (pstate:Proof_global.t -> unit) + +type vernac_command = atts:Attributes.vernac_flags -> typed_vernac type plugin_args = Genarg.raw_generic_argument list -val call : Vernacexpr.extend_name -> plugin_args -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t +val type_vernac : Vernacexpr.extend_name -> plugin_args -> vernac_command (** {5 VERNAC EXTEND} *) type classifier = Genarg.raw_generic_argument list -> vernac_classification type (_, _) ty_sig = -| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig +| TyNil : (vernac_command, vernac_classification) ty_sig | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 77f54361da..0fbde1ade5 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -30,10 +30,12 @@ end type t = { parsing : Parser.state; system : States.state; (* summary + libstack *) - proof : Proof_global.t option; (* proof state *) + proof : Proof_global.stack option; (* proof state *) shallow : bool (* is the state trimmed down (libstack) *) } +let pstate st = Option.map Proof_global.get_current_pstate st.proof + let s_cache = ref None let s_proof = ref None @@ -96,17 +98,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 +124,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 diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index dff81ad9bb..b0f3c572e5 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -21,10 +21,12 @@ end type t = { parsing : Parser.state; system : States.state; (* summary + libstack *) - proof : Proof_global.t option; (* proof state *) + proof : Proof_global.stack option; (* proof state *) shallow : bool (* is the state trimmed down (libstack) *) } +val pstate : t -> Proof_global.t option + val freeze_interp_state : marshallable:bool -> t val unfreeze_interp_state : t -> unit @@ -39,11 +41,11 @@ module Proof_global : sig open Proof_global (* Low-level stuff *) - val get : unit -> t option - val set : t option -> unit + val get : unit -> stack option + val set : stack option -> unit - val freeze : marshallable:bool -> t option - val unfreeze : t -> unit + val freeze : marshallable:bool -> stack option + val unfreeze : stack -> unit exception NoCurrentProof @@ -61,7 +63,7 @@ module Proof_global : sig val with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a - val install_state : t -> unit + val install_state : stack -> unit val return_proof : ?allow_partial:bool -> unit -> closed_proof_output @@ -79,7 +81,7 @@ module Proof_global : sig val get_all_proof_names : unit -> Names.Id.t list - val copy_terminators : src:t option -> tgt:t option -> t option + val copy_terminators : src:stack option -> tgt:stack option -> stack option end [@@ocaml.deprecated "This module is internal and should not be used, instead, thread the proof state"] |