From 6b5b4db599333546334bcdbd852be72ddb39d9dc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 11 Oct 2018 18:13:12 +0200 Subject: Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro. Those optional arguments did not really make sense. It was pretty clear from our code base, as all instances where triplicating the same type for TYPED, RAW_TYPED and GLOB_TYPED. --- plugins/ltac/extraargs.ml4 | 2 -- plugins/ltac/g_auto.ml4 | 2 -- 2 files changed, 4 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index f4555509cc..0c6d10bf8c 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -285,9 +285,7 @@ let in_clause' = Pltac.in_clause ARGUMENT EXTEND in_clause TYPED AS clause_dft_concl PRINTED BY pr_in_top_clause - RAW_TYPED AS clause_dft_concl RAW_PRINTED BY pr_in_clause - GLOB_TYPED AS clause_dft_concl GLOB_PRINTED BY pr_in_clause | [ in_clause'(cl) ] -> [ cl ] END diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 35ed14fc18..8eadb66edc 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -62,9 +62,7 @@ let pr_auto_using _ _ _ = Pptactic.pr_auto_using ARGUMENT EXTEND auto_using TYPED AS uconstr_list PRINTED BY pr_auto_using - RAW_TYPED AS uconstr_list RAW_PRINTED BY pr_auto_using_raw - GLOB_TYPED AS uconstr_list GLOB_PRINTED BY pr_auto_using_glob | [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ] | [ ] -> [ [] ] -- cgit v1.2.3 From 7f39d17e7c1d7655be595ccbe741a15ba780b785 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 11 Oct 2018 15:15:38 +0200 Subject: Providing a centralized API for ARGUMENT EXTEND. We chose to stick to the most general possible API, even though the macro will not make full use of the possibilities. It makes explicit the various data expected to be provided in an orthogonal way. --- plugins/ltac/ltac_plugin.mlpack | 2 +- plugins/ltac/tacentries.ml | 93 +++++++++++++++++++++++++++++++++++++++++ plugins/ltac/tacentries.mli | 59 ++++++++++++++++++++++++++ 3 files changed, 153 insertions(+), 1 deletion(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack index ec96e1bbdd..e83eab20dc 100644 --- a/plugins/ltac/ltac_plugin.mlpack +++ b/plugins/ltac/ltac_plugin.mlpack @@ -7,10 +7,10 @@ Pltac Taccoerce Tactic_debug Tacintern -Tacentries Profile_ltac Tactic_matching Tacinterp +Tacentries Evar_tactics Tactic_option Extraargs diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index a77a9c2f45..16cff420bd 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -673,3 +673,96 @@ let tactic_extend plugin_name tacname ~level ?deprecation sign = let obj () = add_ml_tactic_notation ml_tactic_name ~level ?deprecation (List.map clause_of_ty_ml sign) in Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign); Mltop.declare_cache_obj obj plugin_name + + +(** ARGUMENT EXTEND *) + +open Geninterp + +type ('a, 'b, 'c) argument_printer = + 'a Pptactic.raw_extra_genarg_printer * + 'b Pptactic.glob_extra_genarg_printer * + 'c Pptactic.extra_genarg_printer + +type ('a, 'b) argument_intern = +| ArgInternFun : ('a, 'b) Genintern.intern_fun -> ('a, 'b) argument_intern +| ArgInternWit : ('a, 'b, 'c) Genarg.genarg_type -> ('a, 'b) argument_intern + +type 'b argument_subst = +| ArgSubstFun : 'b Genintern.subst_fun -> 'b argument_subst +| ArgSubstWit : ('a, 'b, 'c) Genarg.genarg_type -> 'b argument_subst + +type ('b, 'c) argument_interp = +| ArgInterpRet : ('c, 'c) argument_interp +| ArgInterpFun : ('b, Val.t) interp_fun -> ('b, 'c) argument_interp +| ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp +| ArgInterpLegacy : + (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp + +type ('a, 'b, 'c) tactic_argument = { + arg_parsing : 'a Vernacentries.argument_rule; + arg_tag : 'c Val.tag option; + arg_intern : ('a, 'b) argument_intern; + arg_subst : 'b argument_subst; + arg_interp : ('b, 'c) argument_interp; + arg_printer : ('a, 'b, 'c) argument_printer; +} + +let intern_fun (type a b c) name (arg : (a, b, c) tactic_argument) : (a, b) Genintern.intern_fun = +match arg.arg_intern with +| ArgInternFun f -> f +| ArgInternWit wit -> + fun ist v -> + let ans = Genarg.out_gen (glbwit wit) (Tacintern.intern_genarg ist (Genarg.in_gen (rawwit wit) v)) in + (ist, ans) + +let subst_fun (type a b c) (arg : (a, b, c) tactic_argument) : b Genintern.subst_fun = +match arg.arg_subst with +| ArgSubstFun f -> f +| ArgSubstWit wit -> + fun s v -> + let ans = Genarg.out_gen (glbwit wit) (Tacsubst.subst_genarg s (Genarg.in_gen (glbwit wit) v)) in + ans + +let interp_fun (type a b c) name (arg : (a, b, c) tactic_argument) (tag : c Val.tag) : (b, Val.t) interp_fun = +match arg.arg_interp with +| ArgInterpRet -> (fun ist v -> Ftactic.return (Geninterp.Val.inject tag v)) +| ArgInterpFun f -> f +| ArgInterpWit wit -> + (fun ist x -> Tacinterp.interp_genarg ist (Genarg.in_gen (glbwit wit) x)) +| ArgInterpLegacy f -> + (fun ist v -> Ftactic.enter (fun gl -> + let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in + let v = Geninterp.Val.inject tag v in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return v) + )) + +let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) = + let wit = Genarg.create_arg name in + let () = Genintern.register_intern0 wit (intern_fun name arg) in + let () = Genintern.register_subst0 wit (subst_fun arg) in + let tag = match arg.arg_tag with + | None -> + let () = register_val0 wit None in + val_tag (topwit wit) + | Some tag -> + let () = register_val0 wit (Some tag) in + tag + in + let () = register_interp0 wit (interp_fun name arg tag) in + let entry = match arg.arg_parsing with + | Vernacentries.Arg_alias e -> + let () = Pcoq.register_grammar wit e in + e + | Vernacentries.Arg_rules rules -> + let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in + let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in + e + in + let (rpr, gpr, tpr) = arg.arg_printer in + let () = Pptactic.declare_extra_genarg_pprule wit rpr gpr tpr in + let () = create_ltac_quotation name + (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v)) + (entry, None) + in + (wit, entry) diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 0b2b426018..5b4bedb50a 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -70,6 +70,8 @@ val print_ltacs : unit -> unit val print_located_tactic : Libnames.qualid -> unit (** Display the absolute name of a tactic. *) +(** {5 TACTIC EXTEND} *) + type _ ty_sig = | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig | TyIdent : string * 'r ty_sig -> 'r ty_sig @@ -79,3 +81,60 @@ type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml val tactic_extend : string -> string -> level:Int.t -> ?deprecation:deprecation -> ty_ml list -> unit + +(** {5 ARGUMENT EXTEND} *) + +(** + + This is the main entry point for the ARGUMENT EXTEND macro that allows to + easily create user-made Ltac arguments. + + + Each argument has three type parameters. See {!Genarg} for more details. + There are two kinds of Ltac arguments, uniform and non-uniform. The former + have the same type at each level (raw, glob, top) while the latter may vary. + + When declaring an argument one must provide the following data: + - Internalization : raw -> glob + - Substitution : glob -> glob + - Interpretation : glob -> Ltac dynamic value + - Printing for every level + - An optional toplevel tag of type top (with the proviso that the + interpretation function only produces values with this tag) + + This data can be either given explicitly with the [Fun] constructors, or it + can be inherited from another argument with the [Wit] constructors. + +*) + +type ('a, 'b, 'c) argument_printer = + 'a Pptactic.raw_extra_genarg_printer * + 'b Pptactic.glob_extra_genarg_printer * + 'c Pptactic.extra_genarg_printer + +type ('a, 'b) argument_intern = +| ArgInternFun : ('a, 'b) Genintern.intern_fun -> ('a, 'b) argument_intern +| ArgInternWit : ('a, 'b, 'c) Genarg.genarg_type -> ('a, 'b) argument_intern + +type 'b argument_subst = +| ArgSubstFun : 'b Genintern.subst_fun -> 'b argument_subst +| ArgSubstWit : ('a, 'b, 'c) Genarg.genarg_type -> 'b argument_subst + +type ('b, 'c) argument_interp = +| ArgInterpRet : ('c, 'c) argument_interp +| ArgInterpFun : ('b, Geninterp.Val.t) Geninterp.interp_fun -> ('b, 'c) argument_interp +| ArgInterpWit : ('a, 'b, 'r) Genarg.genarg_type -> ('b, 'c) argument_interp +| ArgInterpLegacy : + (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp + +type ('a, 'b, 'c) tactic_argument = { + arg_parsing : 'a Vernacentries.argument_rule; + arg_tag : 'c Geninterp.Val.tag option; + arg_intern : ('a, 'b) argument_intern; + arg_subst : 'b argument_subst; + arg_interp : ('b, 'c) argument_interp; + arg_printer : ('a, 'b, 'c) argument_printer; +} + +val argument_extend : name:string -> ('a, 'b, 'c) tactic_argument -> + ('a, 'b, 'c) Genarg.genarg_type * 'a Pcoq.Entry.t -- cgit v1.2.3 From dba567555fed9c88887b463a975c3d7e0852ebd3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 11 Oct 2018 19:17:47 +0200 Subject: Plug ARGUMENT EXTEND into the argument extension API. --- plugins/ltac/extraargs.ml4 | 1 - plugins/ltac/g_auto.ml4 | 1 - plugins/ltac/g_class.ml4 | 2 -- 3 files changed, 4 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 0c6d10bf8c..4de27e8138 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -9,7 +9,6 @@ (************************************************************************) open Pp -open Genarg open Stdarg open Tacarg open Pcoq.Prim diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 8eadb66edc..6913543c9a 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -10,7 +10,6 @@ open Pp open Constr -open Genarg open Stdarg open Pcoq.Prim open Pcoq.Constr diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 1c2f90b670..265368833b 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -32,8 +32,6 @@ VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF set_transparency cl false ] END -open Genarg - let pr_debug _prc _prlc _prt b = if b then Pp.str "debug" else Pp.mt() -- cgit v1.2.3 From 4da233a9685cd193a84def037ec18a27c9225dce Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 12 Oct 2018 09:22:56 +0200 Subject: Port remaining EXTEND ml4 files to coqpp. Almost all of ml4 were removed in the process. The only remaining files are in the test-suite and probably need a bit of fiddling with coq_makefile, and there only two really remaning ml4 files containing code. --- plugins/ltac/extraargs.ml4 | 310 --------- plugins/ltac/extraargs.mlg | 353 ++++++++++ plugins/ltac/extratactics.ml4 | 1065 ------------------------------ plugins/ltac/extratactics.mlg | 1160 +++++++++++++++++++++++++++++++++ plugins/ltac/g_auto.ml4 | 226 ------- plugins/ltac/g_auto.mlg | 249 +++++++ plugins/ltac/g_class.ml4 | 117 ---- plugins/ltac/g_class.mlg | 137 ++++ plugins/ltac/g_ltac.ml4 | 528 --------------- plugins/ltac/g_ltac.mlg | 560 ++++++++++++++++ plugins/ltac/g_obligations.ml4 | 161 ----- plugins/ltac/g_obligations.mlg | 173 +++++ plugins/ltac/g_rewrite.ml4 | 297 --------- plugins/ltac/g_rewrite.mlg | 318 +++++++++ plugins/ltac/profile_ltac_tactics.ml4 | 74 --- plugins/ltac/profile_ltac_tactics.mlg | 82 +++ 16 files changed, 3032 insertions(+), 2778 deletions(-) delete mode 100644 plugins/ltac/extraargs.ml4 create mode 100644 plugins/ltac/extraargs.mlg delete mode 100644 plugins/ltac/extratactics.ml4 create mode 100644 plugins/ltac/extratactics.mlg delete mode 100644 plugins/ltac/g_auto.ml4 create mode 100644 plugins/ltac/g_auto.mlg delete mode 100644 plugins/ltac/g_class.ml4 create mode 100644 plugins/ltac/g_class.mlg delete mode 100644 plugins/ltac/g_ltac.ml4 create mode 100644 plugins/ltac/g_ltac.mlg delete mode 100644 plugins/ltac/g_obligations.ml4 create mode 100644 plugins/ltac/g_obligations.mlg delete mode 100644 plugins/ltac/g_rewrite.ml4 create mode 100644 plugins/ltac/g_rewrite.mlg delete mode 100644 plugins/ltac/profile_ltac_tactics.ml4 create mode 100644 plugins/ltac/profile_ltac_tactics.mlg (limited to 'plugins/ltac') diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 deleted file mode 100644 index 4de27e8138..0000000000 --- a/plugins/ltac/extraargs.ml4 +++ /dev/null @@ -1,310 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Metasyntax.add_token_obj "<-"; - Metasyntax.add_token_obj "->") - "ltac_plugin" - -let pr_orient _prc _prlc _prt = function - | true -> Pp.mt () - | false -> Pp.str " <-" - -ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient -| [ "->" ] -> [ true ] -| [ "<-" ] -> [ false ] -| [ ] -> [ true ] -END - -let pr_int _ _ _ i = Pp.int i - -let _natural = Pcoq.Prim.natural - -ARGUMENT EXTEND natural TYPED AS int PRINTED BY pr_int -| [ _natural(i) ] -> [ i ] -END - -let pr_orient = pr_orient () () () - - -let pr_int_list = Pp.pr_sequence Pp.int -let pr_int_list_full _prc _prlc _prt l = pr_int_list l - -let pr_occurrences _prc _prlc _prt l = - match l with - | ArgArg x -> pr_int_list x - | ArgVar { CAst.loc = loc; v=id } -> Id.print id - -let occurrences_of = function - | [] -> NoOccurrences - | n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl) - | nl -> - if List.exists (fun n -> n < 0) nl then - CErrors.user_err Pp.(str "Illegal negative occurrence number."); - OnlyOccurrences nl - -let coerce_to_int v = match Value.to_int v with - | None -> raise (CannotCoerceTo "an integer") - | Some n -> n - -let int_list_of_VList v = match Value.to_list v with -| Some l -> List.map (fun n -> coerce_to_int n) l -| _ -> raise (CannotCoerceTo "an integer") - -let interp_occs ist gl l = - match l with - | ArgArg x -> x - | ArgVar ({ CAst.v = id } as locid) -> - (try int_list_of_VList (Id.Map.find id ist.lfun) - with Not_found | CannotCoerceTo _ -> [interp_int ist locid]) -let interp_occs ist gl l = - Tacmach.project gl , interp_occs ist gl l - -let glob_occs ist l = l - -let subst_occs evm l = l - -ARGUMENT EXTEND occurrences - TYPED AS int list - PRINTED BY pr_int_list_full - - INTERPRETED BY interp_occs - GLOBALIZED BY glob_occs - SUBSTITUTED BY subst_occs - - RAW_PRINTED BY pr_occurrences - GLOB_PRINTED BY pr_occurrences - -| [ ne_integer_list(l) ] -> [ ArgArg l ] -| [ var(id) ] -> [ ArgVar id ] -END - -let pr_occurrences = pr_occurrences () () () - -let pr_gen prc _prlc _prtac c = prc c - -let pr_globc _prc _prlc _prtac (_,glob) = - let _, env = Pfedit.get_current_context () in - Printer.pr_glob_constr_env env glob - -let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) - -let glob_glob = Tacintern.intern_constr - -let pr_lconstr _ prc _ c = prc c - -let subst_glob = Tacsubst.subst_glob_constr_and_expr - -ARGUMENT EXTEND glob - PRINTED BY pr_globc - - INTERPRETED BY interp_glob - GLOBALIZED BY glob_glob - SUBSTITUTED BY subst_glob - - RAW_PRINTED BY pr_gen - GLOB_PRINTED BY pr_gen - [ constr(c) ] -> [ c ] -END - -let l_constr = Pcoq.Constr.lconstr - -ARGUMENT EXTEND lconstr - TYPED AS constr - PRINTED BY pr_lconstr - [ l_constr(c) ] -> [ c ] -END - -ARGUMENT EXTEND lglob - TYPED AS glob - PRINTED BY pr_globc - - INTERPRETED BY interp_glob - GLOBALIZED BY glob_glob - SUBSTITUTED BY subst_glob - - RAW_PRINTED BY pr_gen - GLOB_PRINTED BY pr_gen - [ lconstr(c) ] -> [ c ] -END - -let interp_casted_constr ist gl c = - interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c - -ARGUMENT EXTEND casted_constr - TYPED AS constr - PRINTED BY pr_gen - INTERPRETED BY interp_casted_constr - [ constr(c) ] -> [ c ] -END - -type 'id gen_place= ('id * hyp_location_flag,unit) location - -type loc_place = lident gen_place -type place = Id.t gen_place - -let pr_gen_place pr_id = function - ConclLocation () -> Pp.mt () - | HypLocation (id,InHyp) -> str "in " ++ pr_id id - | HypLocation (id,InHypTypeOnly) -> - str "in (type of " ++ pr_id id ++ str ")" - | HypLocation (id,InHypValueOnly) -> - str "in (value of " ++ pr_id id ++ str ")" - -let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id) -let pr_place _ _ _ = pr_gen_place Id.print -let pr_hloc = pr_loc_place () () () - -let intern_place ist = function - ConclLocation () -> ConclLocation () - | HypLocation (id,hl) -> HypLocation (Tacintern.intern_hyp ist id,hl) - -let interp_place ist env sigma = function - ConclLocation () -> ConclLocation () - | HypLocation (id,hl) -> HypLocation (Tacinterp.interp_hyp ist env sigma id,hl) - -let interp_place ist gl p = - Tacmach.project gl , interp_place ist (Tacmach.pf_env gl) (Tacmach.project gl) p - -let subst_place subst pl = pl - -let warn_deprecated_instantiate_syntax = - CWarnings.create ~name:"deprecated-instantiate-syntax" ~category:"deprecated" - (fun (v,v',id) -> - let s = Id.to_string id in - Pp.strbrk - ("Syntax \"in (" ^ v ^ " of " ^ s ^ ")\" is deprecated; use \"in (" ^ v' ^ " of " ^ s ^ ")\".") - ) - -ARGUMENT EXTEND hloc - PRINTED BY pr_place - INTERPRETED BY interp_place - GLOBALIZED BY intern_place - SUBSTITUTED BY subst_place - RAW_PRINTED BY pr_loc_place - GLOB_PRINTED BY pr_loc_place - [ ] -> - [ ConclLocation () ] - | [ "in" "|-" "*" ] -> - [ ConclLocation () ] -| [ "in" ident(id) ] -> - [ HypLocation ((CAst.make id),InHyp) ] -| [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ warn_deprecated_instantiate_syntax ("Type","type",id); - HypLocation ((CAst.make id),InHypTypeOnly) ] -| [ "in" "(" "Value" "of" ident(id) ")" ] -> - [ warn_deprecated_instantiate_syntax ("Value","value",id); - HypLocation ((CAst.make id),InHypValueOnly) ] -| [ "in" "(" "type" "of" ident(id) ")" ] -> - [ HypLocation ((CAst.make id),InHypTypeOnly) ] -| [ "in" "(" "value" "of" ident(id) ")" ] -> - [ HypLocation ((CAst.make id),InHypValueOnly) ] - - END - -let pr_rename _ _ _ (n, m) = Id.print n ++ str " into " ++ Id.print m - -ARGUMENT EXTEND rename - TYPED AS ident * ident - PRINTED BY pr_rename -| [ ident(n) "into" ident(m) ] -> [ (n, m) ] -END - -(* Julien: Mise en commun des differentes version de replace with in by *) - -let pr_by_arg_tac _prc _prlc prtac opt_c = - match opt_c with - | None -> mt () - | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t) - -ARGUMENT EXTEND by_arg_tac - TYPED AS tactic_opt - PRINTED BY pr_by_arg_tac -| [ "by" tactic3(c) ] -> [ Some c ] -| [ ] -> [ None ] -END - -let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c - -let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl -let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl -let in_clause' = Pltac.in_clause - -ARGUMENT EXTEND in_clause - TYPED AS clause_dft_concl - PRINTED BY pr_in_top_clause - RAW_PRINTED BY pr_in_clause - GLOB_PRINTED BY pr_in_clause -| [ in_clause'(cl) ] -> [ cl ] -END - -let local_test_lpar_id_colon = - let err () = raise Stream.Failure in - Pcoq.Gram.Entry.of_parser "lpar_id_colon" - (fun strm -> - match Util.stream_nth 0 strm with - | Tok.KEYWORD "(" -> - (match Util.stream_nth 1 strm with - | Tok.IDENT _ -> - (match Util.stream_nth 2 strm with - | Tok.KEYWORD ":" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) - -let pr_lpar_id_colon _ _ _ _ = mt () - -ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon -| [ local_test_lpar_id_colon(x) ] -> [ () ] -END diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg new file mode 100644 index 0000000000..c4c4e51ecc --- /dev/null +++ b/plugins/ltac/extraargs.mlg @@ -0,0 +1,353 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Metasyntax.add_token_obj "<-"; + Metasyntax.add_token_obj "->") + "ltac_plugin" + +let pr_orient _prc _prlc _prt = function + | true -> Pp.mt () + | false -> Pp.str " <-" + +} + +ARGUMENT EXTEND orient TYPED AS bool PRINTED BY { pr_orient } +| [ "->" ] -> { true } +| [ "<-" ] -> { false } +| [ ] -> { true } +END + +{ + +let pr_int _ _ _ i = Pp.int i + +let _natural = Pcoq.Prim.natural + +} + +ARGUMENT EXTEND natural TYPED AS int PRINTED BY { pr_int } +| [ _natural(i) ] -> { i } +END + +{ + +let pr_orient = pr_orient () () () + +let pr_int_list = Pp.pr_sequence Pp.int +let pr_int_list_full _prc _prlc _prt l = pr_int_list l + +let pr_occurrences _prc _prlc _prt l = + match l with + | ArgArg x -> pr_int_list x + | ArgVar { CAst.loc = loc; v=id } -> Id.print id + +let occurrences_of = function + | [] -> NoOccurrences + | n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl) + | nl -> + if List.exists (fun n -> n < 0) nl then + CErrors.user_err Pp.(str "Illegal negative occurrence number."); + OnlyOccurrences nl + +let coerce_to_int v = match Value.to_int v with + | None -> raise (CannotCoerceTo "an integer") + | Some n -> n + +let int_list_of_VList v = match Value.to_list v with +| Some l -> List.map (fun n -> coerce_to_int n) l +| _ -> raise (CannotCoerceTo "an integer") + +let interp_occs ist gl l = + match l with + | ArgArg x -> x + | ArgVar ({ CAst.v = id } as locid) -> + (try int_list_of_VList (Id.Map.find id ist.lfun) + with Not_found | CannotCoerceTo _ -> [interp_int ist locid]) +let interp_occs ist gl l = + Tacmach.project gl , interp_occs ist gl l + +let glob_occs ist l = l + +let subst_occs evm l = l + +} + +ARGUMENT EXTEND occurrences + TYPED AS int list + PRINTED BY { pr_int_list_full } + + INTERPRETED BY { interp_occs } + GLOBALIZED BY { glob_occs } + SUBSTITUTED BY { subst_occs } + + RAW_PRINTED BY { pr_occurrences } + GLOB_PRINTED BY { pr_occurrences } + +| [ ne_integer_list(l) ] -> { ArgArg l } +| [ var(id) ] -> { ArgVar id } +END + +{ + +let pr_occurrences = pr_occurrences () () () + +let pr_gen prc _prlc _prtac c = prc c + +let pr_globc _prc _prlc _prtac (_,glob) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env glob + +let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) + +let glob_glob = Tacintern.intern_constr + +let pr_lconstr _ prc _ c = prc c + +let subst_glob = Tacsubst.subst_glob_constr_and_expr + +} + +ARGUMENT EXTEND glob + PRINTED BY { pr_globc } + + INTERPRETED BY { interp_glob } + GLOBALIZED BY { glob_glob } + SUBSTITUTED BY { subst_glob } + + RAW_PRINTED BY { pr_gen } + GLOB_PRINTED BY { pr_gen } +| [ constr(c) ] -> { c } +END + +{ + +let l_constr = Pcoq.Constr.lconstr + +} + +ARGUMENT EXTEND lconstr + TYPED AS constr + PRINTED BY { pr_lconstr } +| [ l_constr(c) ] -> { c } +END + +ARGUMENT EXTEND lglob + TYPED AS glob + PRINTED BY { pr_globc } + + INTERPRETED BY { interp_glob } + GLOBALIZED BY { glob_glob } + SUBSTITUTED BY { subst_glob } + + RAW_PRINTED BY { pr_gen } + GLOB_PRINTED BY { pr_gen } +| [ lconstr(c) ] -> { c } +END + +{ + +let interp_casted_constr ist gl c = + interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c + +} + +ARGUMENT EXTEND casted_constr + TYPED AS constr + PRINTED BY { pr_gen } + INTERPRETED BY { interp_casted_constr } +| [ constr(c) ] -> { c } +END + +{ + +type 'id gen_place= ('id * hyp_location_flag,unit) location + +type loc_place = lident gen_place +type place = Id.t gen_place + +let pr_gen_place pr_id = function + ConclLocation () -> Pp.mt () + | HypLocation (id,InHyp) -> str "in " ++ pr_id id + | HypLocation (id,InHypTypeOnly) -> + str "in (type of " ++ pr_id id ++ str ")" + | HypLocation (id,InHypValueOnly) -> + str "in (value of " ++ pr_id id ++ str ")" + +let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id) +let pr_place _ _ _ = pr_gen_place Id.print +let pr_hloc = pr_loc_place () () () + +let intern_place ist = function + ConclLocation () -> ConclLocation () + | HypLocation (id,hl) -> HypLocation (Tacintern.intern_hyp ist id,hl) + +let interp_place ist env sigma = function + ConclLocation () -> ConclLocation () + | HypLocation (id,hl) -> HypLocation (Tacinterp.interp_hyp ist env sigma id,hl) + +let interp_place ist gl p = + Tacmach.project gl , interp_place ist (Tacmach.pf_env gl) (Tacmach.project gl) p + +let subst_place subst pl = pl + +let warn_deprecated_instantiate_syntax = + CWarnings.create ~name:"deprecated-instantiate-syntax" ~category:"deprecated" + (fun (v,v',id) -> + let s = Id.to_string id in + Pp.strbrk + ("Syntax \"in (" ^ v ^ " of " ^ s ^ ")\" is deprecated; use \"in (" ^ v' ^ " of " ^ s ^ ")\".") + ) + +} + +ARGUMENT EXTEND hloc + PRINTED BY { pr_place } + INTERPRETED BY { interp_place } + GLOBALIZED BY { intern_place } + SUBSTITUTED BY { subst_place } + RAW_PRINTED BY { pr_loc_place } + GLOB_PRINTED BY { pr_loc_place } +| [ ] -> + { ConclLocation () } + | [ "in" "|-" "*" ] -> + { ConclLocation () } +| [ "in" ident(id) ] -> + { HypLocation ((CAst.make id),InHyp) } +| [ "in" "(" "Type" "of" ident(id) ")" ] -> + { warn_deprecated_instantiate_syntax ("Type","type",id); + HypLocation ((CAst.make id),InHypTypeOnly) } +| [ "in" "(" "Value" "of" ident(id) ")" ] -> + { warn_deprecated_instantiate_syntax ("Value","value",id); + HypLocation ((CAst.make id),InHypValueOnly) } +| [ "in" "(" "type" "of" ident(id) ")" ] -> + { HypLocation ((CAst.make id),InHypTypeOnly) } +| [ "in" "(" "value" "of" ident(id) ")" ] -> + { HypLocation ((CAst.make id),InHypValueOnly) } + + END + +{ + +let pr_rename _ _ _ (n, m) = Id.print n ++ str " into " ++ Id.print m + +} + +ARGUMENT EXTEND rename + TYPED AS (ident * ident) + PRINTED BY { pr_rename } +| [ ident(n) "into" ident(m) ] -> { (n, m) } +END + +(* Julien: Mise en commun des differentes version de replace with in by *) + +{ + +let pr_by_arg_tac _prc _prlc prtac opt_c = + match opt_c with + | None -> mt () + | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t) + +} + +ARGUMENT EXTEND by_arg_tac + TYPED AS tactic option + PRINTED BY { pr_by_arg_tac } +| [ "by" tactic3(c) ] -> { Some c } +| [ ] -> { None } +END + +{ + +let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c + +let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl +let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl +let in_clause' = Pltac.in_clause + +} + +ARGUMENT EXTEND in_clause + TYPED AS clause_dft_concl + PRINTED BY { pr_in_top_clause } + RAW_PRINTED BY { pr_in_clause } + GLOB_PRINTED BY { pr_in_clause } +| [ in_clause'(cl) ] -> { cl } +END + +{ + +let local_test_lpar_id_colon = + let err () = raise Stream.Failure in + Pcoq.Gram.Entry.of_parser "lpar_id_colon" + (fun strm -> + match Util.stream_nth 0 strm with + | Tok.KEYWORD "(" -> + (match Util.stream_nth 1 strm with + | Tok.IDENT _ -> + (match Util.stream_nth 2 strm with + | Tok.KEYWORD ":" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + +let pr_lpar_id_colon _ _ _ _ = mt () + +} + +ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY { pr_lpar_id_colon } +| [ local_test_lpar_id_colon(x) ] -> { () } +END diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 deleted file mode 100644 index e5b032e638..0000000000 --- a/plugins/ltac/extratactics.ml4 +++ /dev/null @@ -1,1065 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* replace_in_clause_maybe_by c1 c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac)) - -let replace_term ist dir_opt c cl = - with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl) - -TACTIC EXTEND replace - ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] --> [ replace_in_clause_maybe_by ist c1 c2 cl tac ] -END - -TACTIC EXTEND replace_term_left - [ "replace" "->" uconstr(c) clause(cl) ] - -> [ replace_term ist (Some true) c cl ] -END - -TACTIC EXTEND replace_term_right - [ "replace" "<-" uconstr(c) clause(cl) ] - -> [ replace_term ist (Some false) c cl ] -END - -TACTIC EXTEND replace_term - [ "replace" uconstr(c) clause(cl) ] - -> [ replace_term ist None c cl ] -END - -let induction_arg_of_quantified_hyp = function - | AnonHyp n -> None,ElimOnAnonHyp n - | NamedHyp id -> None,ElimOnIdent (CAst.make id) - -(* Versions *_main must come first!! so that "1" is interpreted as a - ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a - ElimOnIdent and not as "constr" *) - -let mytclWithHoles tac with_evars c = - Proofview.Goal.enter begin fun gl -> - let env = Tacmach.New.pf_env gl in - let sigma = Tacmach.New.project gl in - let sigma',c = Tactics.force_destruction_arg with_evars env sigma c in - Tacticals.New.tclWITHHOLES with_evars (tac with_evars (Some c)) sigma' - end - -let elimOnConstrWithHoles tac with_evars c = - Tacticals.New.tclDELAYEDWITHHOLES with_evars c - (fun c -> tac with_evars (Some (None,ElimOnConstr c))) - -TACTIC EXTEND simplify_eq - [ "simplify_eq" ] -> [ dEq ~keep_proofs:None false None ] -| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) false c ] -END -TACTIC EXTEND esimplify_eq -| [ "esimplify_eq" ] -> [ dEq ~keep_proofs:None true None ] -| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) true c ] -END - -let discr_main c = elimOnConstrWithHoles discr_tac false c - -TACTIC EXTEND discriminate -| [ "discriminate" ] -> [ discr_tac false None ] -| [ "discriminate" destruction_arg(c) ] -> - [ mytclWithHoles discr_tac false c ] -END -TACTIC EXTEND ediscriminate -| [ "ediscriminate" ] -> [ discr_tac true None ] -| [ "ediscriminate" destruction_arg(c) ] -> - [ mytclWithHoles discr_tac true c ] -END - -let discrHyp id = - Proofview.tclEVARMAP >>= fun sigma -> - discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) - -let injection_main with_evars c = - elimOnConstrWithHoles (injClause None None) with_evars c - -TACTIC EXTEND injection -| [ "injection" ] -> [ injClause None None false None ] -| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) false c ] -END -TACTIC EXTEND einjection -| [ "einjection" ] -> [ injClause None None true None ] -| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) true c ] -END -TACTIC EXTEND injection_as -| [ "injection" "as" intropattern_list(ipat)] -> - [ injClause None (Some ipat) false None ] -| [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] -> - [ mytclWithHoles (injClause None (Some ipat)) false c ] -END -TACTIC EXTEND einjection_as -| [ "einjection" "as" intropattern_list(ipat)] -> - [ injClause None (Some ipat) true None ] -| [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> - [ mytclWithHoles (injClause None (Some ipat)) true c ] -END -TACTIC EXTEND simple_injection -| [ "simple" "injection" ] -> [ simpleInjClause None false None ] -| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles (simpleInjClause None) false c ] -END - -let injHyp id = - Proofview.tclEVARMAP >>= fun sigma -> - injection_main false (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) - -TACTIC EXTEND dependent_rewrite -| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ] -| [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ] - -> [ rewriteInHyp b c id ] -END - -(** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to - "replace u with t" or "enough (t=u) as <-" and - "cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *) - -TACTIC EXTEND cut_rewrite -| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ] -| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ] - -> [ cutRewriteInHyp b eqn id ] -END - -(**********************************************************************) -(* Decompose *) - -TACTIC EXTEND decompose_sum -| [ "decompose" "sum" constr(c) ] -> [ Elim.h_decompose_or c ] -END - -TACTIC EXTEND decompose_record -| [ "decompose" "record" constr(c) ] -> [ Elim.h_decompose_and c ] -END - -(**********************************************************************) -(* Contradiction *) - -open Contradiction - -TACTIC EXTEND absurd - [ "absurd" constr(c) ] -> [ absurd c ] -END - -let onSomeWithHoles tac = function - | None -> tac None - | Some c -> Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c)) - -TACTIC EXTEND contradiction - [ "contradiction" constr_with_bindings_opt(c) ] -> - [ onSomeWithHoles contradiction c ] -END - -(**********************************************************************) -(* AutoRewrite *) - -open Autorewrite - -let pr_orient _prc _prlc _prt = function - | true -> Pp.mt () - | false -> Pp.str " <-" - -let pr_orient_string _prc _prlc _prt (orient, s) = - pr_orient _prc _prlc _prt orient ++ Pp.spc () ++ Pp.str s - -ARGUMENT EXTEND orient_string TYPED AS (bool * string) PRINTED BY pr_orient_string -| [ orient(r) preident(i) ] -> [ r, i ] -END - -TACTIC EXTEND autorewrite -| [ "autorewrite" "with" ne_preident_list(l) clause(cl) ] -> - [ auto_multi_rewrite l ( cl) ] -| [ "autorewrite" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] -> - [ - auto_multi_rewrite_with (Tacinterp.tactic_of_value ist t) l cl - ] -END - -TACTIC EXTEND autorewrite_star -| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) ] -> - [ auto_multi_rewrite ~conds:AllMatches l cl ] -| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] -> - [ auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_value ist t) l cl ] -END - -(**********************************************************************) -(* Rewrite star *) - -let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) = - let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in - with_delayed_uconstr ist c - (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true) - -TACTIC EXTEND rewrite_star -| [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] -> - [ rewrite_star ist (Some id) o (occurrences_of occ) c tac ] -| [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] -> - [ rewrite_star ist (Some id) o (occurrences_of occ) c tac ] -| [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) by_arg_tac(tac) ] -> - [ rewrite_star ist (Some id) o Locus.AllOccurrences c tac ] -| [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) by_arg_tac(tac) ] -> - [ rewrite_star ist None o (occurrences_of occ) c tac ] -| [ "rewrite" "*" orient(o) uconstr(c) by_arg_tac(tac) ] -> - [ rewrite_star ist None o Locus.AllOccurrences c tac ] - END - -(**********************************************************************) -(* Hint Rewrite *) - -let add_rewrite_hint ~poly bases ort t lcsr = - let env = Global.env() in - let sigma = Evd.from_env env in - let f ce = - let c, ctx = Constrintern.interp_constr env sigma ce in - let c = EConstr.to_constr sigma c in - let ctx = - let ctx = UState.context_set ctx in - if poly then ctx - else (** This is a global universe context that shouldn't be - refreshed at every use of the hint, declare it globally. *) - (Declare.declare_universe_context false ctx; - Univ.ContextSet.empty) - in - CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in - let eqs = List.map f lcsr in - let add_hints base = add_rew_rules base eqs in - List.iter add_hints bases - -let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater - -VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint - [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> - [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o None l; st ] -| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) - ":" preident_list(bl) ] -> - [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l; st ] -| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> - [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l; st ] -| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> - [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l; st ] -END - -(**********************************************************************) -(* Refine *) - -open EConstr -open Vars - -let constr_flags () = { - Pretyping.use_typeclasses = true; - Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics (); - Pretyping.use_hook = Pfedit.solve_by_implicit_tactic (); - Pretyping.fail_evar = false; - Pretyping.expand_evars = true } - -let refine_tac ist simple with_classes c = - Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let env = Proofview.Goal.env gl in - let flags = - { constr_flags () with Pretyping.use_typeclasses = with_classes } in - let expected_type = Pretyping.OfType concl in - let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in - let update = begin fun sigma -> - c env sigma - end in - let refine = Refine.refine ~typecheck:false update in - if simple then refine - else refine <*> - Tactics.New.reduce_after_refine <*> - Proofview.shelve_unifiable - end - -TACTIC EXTEND refine -| [ "refine" uconstr(c) ] -> - [ refine_tac ist false true c ] -END - -TACTIC EXTEND simple_refine -| [ "simple" "refine" uconstr(c) ] -> - [ refine_tac ist true true c ] -END - -TACTIC EXTEND notcs_refine -| [ "notypeclasses" "refine" uconstr(c) ] -> - [ refine_tac ist false false c ] -END - -TACTIC EXTEND notcs_simple_refine -| [ "simple" "notypeclasses" "refine" uconstr(c) ] -> - [ refine_tac ist true false c ] -END - -(* Solve unification constraints using heuristics or fail if any remain *) -TACTIC EXTEND solve_constraints -[ "solve_constraints" ] -> [ Refine.solve_constraints ] -END - -(**********************************************************************) -(* Inversion lemmas (Leminv) *) - -open Inv -open Leminv - -let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater - -(*VERNAC ARGUMENT EXTEND sort_family -| [ "Set" ] -> [ InSet ] -| [ "Prop" ] -> [ InProp ] -| [ "Type" ] -> [ InType ] -END*) - -VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversionClear -| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] - => [ seff na ] - -> [ fun ~atts ~st -> - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac; st ] - -| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ] - -> [ fun ~atts ~st -> - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac; st ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversion -| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] - => [ seff na ] - -> [ fun ~atts ~st -> - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac; st ] - -| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ] - -> [ fun ~atts ~st -> - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac; st ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversion -| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] - => [ seff na ] - -> [ fun ~atts ~st -> - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac; st ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversionClear -| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] - => [ seff na ] - -> [ fun ~atts ~st -> - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac; st ] -END - -(**********************************************************************) -(* Subst *) - -TACTIC EXTEND subst -| [ "subst" ne_var_list(l) ] -> [ subst l ] -| [ "subst" ] -> [ subst_all () ] -END - -let simple_subst_tactic_flags = - { only_leibniz = true; rewrite_dependent_proof = false } - -TACTIC EXTEND simple_subst -| [ "simple" "subst" ] -> [ subst_all ~flags:simple_subst_tactic_flags () ] -END - -open Evar_tactics - -(**********************************************************************) -(* Evar creation *) - -(* TODO: add support for some test similar to g_constr.name_colon so that - expressions like "evar (list A)" do not raise a syntax error *) -TACTIC EXTEND evar - [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name.Name id) typ ] -| [ "evar" constr(typ) ] -> [ let_evar Name.Anonymous typ ] -END - -TACTIC EXTEND instantiate - [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] -> - [ Tacticals.New.tclTHEN (instantiate_tac_by_name id c) Proofview.V82.nf_evar_goals ] -| [ "instantiate" "(" integer(i) ":=" lglob(c) ")" hloc(hl) ] -> - [ Tacticals.New.tclTHEN (instantiate_tac i c hl) Proofview.V82.nf_evar_goals ] -| [ "instantiate" ] -> [ Proofview.V82.nf_evar_goals ] -END - -(**********************************************************************) -(** Nijmegen "step" tactic for setoid rewriting *) - -open Tactics -open Glob_term -open Libobject -open Lib - -(* Registered lemmas are expected to be of the form - x R y -> y == z -> x R z (in the right table) - x R y -> x == z -> z R y (in the left table) -*) - -let transitivity_right_table = Summary.ref [] ~name:"transitivity-steps-r" -let transitivity_left_table = Summary.ref [] ~name:"transitivity-steps-l" - -(* [step] tries to apply a rewriting lemma; then apply [tac] intended to - complete to proof of the last hypothesis (assumed to state an equality) *) - -let step left x tac = - let l = - List.map (fun lem -> - let lem = EConstr.of_constr lem in - Tacticals.New.tclTHENLAST - (apply_with_bindings (lem, ImplicitBindings [x])) - tac) - !(if left then transitivity_left_table else transitivity_right_table) - in - Tacticals.New.tclFIRST l - -(* Main function to push lemmas in persistent environment *) - -let cache_transitivity_lemma (_,(left,lem)) = - if left then - transitivity_left_table := lem :: !transitivity_left_table - else - transitivity_right_table := lem :: !transitivity_right_table - -let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) - -let inTransitivity : bool * Constr.t -> obj = - declare_object {(default_object "TRANSITIVITY-STEPS") with - cache_function = cache_transitivity_lemma; - open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o); - subst_function = subst_transitivity_lemma; - classify_function = (fun o -> Substitute o) } - -(* Main entry points *) - -let add_transitivity_lemma left lem = - let env = Global.env () in - let sigma = Evd.from_env env in - let lem',ctx (*FIXME*) = Constrintern.interp_constr env sigma lem in - let lem' = EConstr.to_constr sigma lem' in - add_anonymous_leaf (inTransitivity (left,lem')) - -(* Vernacular syntax *) - -TACTIC EXTEND stepl -| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (Tacinterp.tactic_of_value ist tac) ] -| ["stepl" constr(c) ] -> [ step true c (Proofview.tclUNIT ()) ] -END - -TACTIC EXTEND stepr -| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (Tacinterp.tactic_of_value ist tac) ] -| ["stepr" constr(c) ] -> [ step false c (Proofview.tclUNIT ()) ] -END - -VERNAC COMMAND EXTEND AddStepl CLASSIFIED AS SIDEFF -| [ "Declare" "Left" "Step" constr(t) ] -> - [ add_transitivity_lemma true t ] -END - -VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF -| [ "Declare" "Right" "Step" constr(t) ] -> - [ add_transitivity_lemma false t ] -END - -let cache_implicit_tactic (_,tac) = match tac with - | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac) - | None -> Pfedit.clear_implicit_tactic () - -let subst_implicit_tactic (subst,tac) = - Option.map (Tacsubst.subst_tactic subst) tac - -let inImplicitTactic : glob_tactic_expr option -> obj = - declare_object {(default_object "IMPLICIT-TACTIC") with - open_function = (fun i o -> if Int.equal i 1 then cache_implicit_tactic o); - cache_function = cache_implicit_tactic; - subst_function = subst_implicit_tactic; - classify_function = (fun o -> Dispose)} - -let warn_deprecated_implicit_tactic = - CWarnings.create ~name:"deprecated-implicit-tactic" ~category:"deprecated" - (fun () -> strbrk "Implicit tactics are deprecated") - -let declare_implicit_tactic tac = - let () = warn_deprecated_implicit_tactic () in - Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac))) - -let clear_implicit_tactic () = - let () = warn_deprecated_implicit_tactic () in - Lib.add_anonymous_leaf (inImplicitTactic None) - -VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF -| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ declare_implicit_tactic tac ] -| [ "Clear" "Implicit" "Tactic" ] -> [ clear_implicit_tactic () ] -END - - - - -(**********************************************************************) -(* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as - defined by Conor McBride *) -TACTIC EXTEND generalize_eqs -| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize ~generalize_vars:false id ] -END -TACTIC EXTEND dep_generalize_eqs -| ["dependent" "generalize_eqs" hyp(id) ] -> [ abstract_generalize ~generalize_vars:false ~force_dep:true id ] -END -TACTIC EXTEND generalize_eqs_vars -| ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize ~generalize_vars:true id ] -END -TACTIC EXTEND dep_generalize_eqs_vars -| ["dependent" "generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize ~force_dep:true ~generalize_vars:true id ] -END - -(** Tactic to automatically simplify hypotheses of the form [Π Δ, x_i = t_i -> T] - where [t_i] is closed w.r.t. Δ. Such hypotheses are automatically generated - during dependent induction. For internal use. *) - -TACTIC EXTEND specialize_eqs -[ "specialize_eqs" hyp(id) ] -> [ specialize_eqs id ] -END - -(**********************************************************************) -(* A tactic that considers a given occurrence of [c] in [t] and *) -(* abstract the minimal set of all the occurrences of [c] so that the *) -(* abstraction [fun x -> t[x/c]] is well-typed *) -(* *) -(* Contributed by Chung-Kil Hur (Winter 2009) *) -(**********************************************************************) - -let subst_var_with_hole occ tid t = - let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in - let locref = ref 0 in - let rec substrec x = match DAst.get x with - | GVar id -> - if Id.equal id tid - then - (decr occref; - if Int.equal !occref 0 then x - else - (incr locref; - DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark { - Evar_kinds.qm_obligation=Evar_kinds.Define true; - Evar_kinds.qm_name=Anonymous; - Evar_kinds.qm_record_field=None; - }, IntroAnonymous, None))) - else x - | _ -> map_glob_constr_left_to_right substrec x in - let t' = substrec t - in - if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t' - -let subst_hole_with_term occ tc t = - let locref = ref 0 in - let occref = ref occ in - let rec substrec c = match DAst.get c with - | GHole (Evar_kinds.QuestionMark { - Evar_kinds.qm_obligation=Evar_kinds.Define true; - Evar_kinds.qm_name=Anonymous; - Evar_kinds.qm_record_field=None; - }, IntroAnonymous, s) -> - decr occref; - if Int.equal !occref 0 then tc - else - (incr locref; - DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark { - Evar_kinds.qm_obligation=Evar_kinds.Define true; - Evar_kinds.qm_name=Anonymous; - Evar_kinds.qm_record_field=None; - },IntroAnonymous,s)) - | _ -> map_glob_constr_left_to_right substrec c - in - substrec t - -open Tacmach - -let hResolve id c occ t = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - let env = Termops.clear_named_body id (Proofview.Goal.env gl) in - let concl = Proofview.Goal.concl gl in - let env_ids = Termops.vars_of_env env in - let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in - let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in - let rec resolve_hole t_hole = - try - Pretyping.understand env sigma t_hole - with - | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e -> - let (e, info) = CErrors.push e in - let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in - resolve_hole (subst_hole_with_term loc_begin c_raw t_hole) - in - let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in - let sigma = Evd.merge_universe_context sigma ctx in - let t_constr_type = Retyping.get_type_of env sigma t_constr in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (change_concl (mkLetIn (Name.Anonymous,t_constr,t_constr_type,concl))) - end - -let hResolve_auto id c t = - let rec resolve_auto n = - try - hResolve id c n t - with - | UserError _ as e -> raise e - | e when CErrors.noncritical e -> resolve_auto (n+1) - in - resolve_auto 1 - -TACTIC EXTEND hresolve_core -| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> [ hResolve id c occ t ] -| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> [ hResolve_auto id c t ] -END - -(** - hget_evar -*) - -TACTIC EXTEND hget_evar -| [ "hget_evar" int_or_var(n) ] -> [ Evar_tactics.hget_evar n ] -END - -(**********************************************************************) - -(**********************************************************************) -(* A tactic that reduces one match t with ... by doing destruct t. *) -(* if t is not a variable, the tactic does *) -(* case_eq t;intros ... heq;rewrite heq in *|-. (but heq itself is *) -(* preserved). *) -(* Contributed by Julien Forest and Pierre Courtieu (july 2010) *) -(**********************************************************************) - -exception Found of unit Proofview.tactic - -let rewrite_except h = - Proofview.Goal.enter begin fun gl -> - let hyps = Tacmach.New.pf_ids_of_hyps gl in - Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else - Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false)) - hyps - end - - -let refl_equal () = Coqlib.lib_ref "core.eq.type" - -(* This is simply an implementation of the case_eq tactic. this code - should be replaced by a call to the tactic but I don't know how to - call it before it is defined. *) -let mkCaseEq a : unit Proofview.tactic = - Proofview.Goal.enter begin fun gl -> - let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in - Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req -> - Tacticals.New.tclTHENLIST - [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))]; - Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let env = Proofview.Goal.env gl in - (** FIXME: this looks really wrong. Does anybody really use this tactic? *) - let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in - change_concl c - end; - simplest_case a] - end - - -let case_eq_intros_rewrite x = - Proofview.Goal.enter begin fun gl -> - let n = nb_prod (Tacmach.New.project gl) (Proofview.Goal.concl gl) in - (* Pp.msgnl (Printer.pr_lconstr x); *) - Tacticals.New.tclTHENLIST [ - mkCaseEq x; - Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let hyps = Tacmach.New.pf_ids_set_of_hyps gl in - let n' = nb_prod (Tacmach.New.project gl) concl in - let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl) in - Tacticals.New.tclTHENLIST [ - Tacticals.New.tclDO (n'-n-1) intro; - introduction h; - rewrite_except h] - end - ] - end - -let rec find_a_destructable_match sigma t = - let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in - let cl = [cl, (None, None), None], None in - let dest = TacAtom (Loc.tag @@ TacInductionDestruct(false, false, cl)) in - match EConstr.kind sigma t with - | Case (_,_,x,_) when closed0 sigma x -> - if isVar sigma x then - (* TODO check there is no rel n. *) - raise (Found (Tacinterp.eval_tactic dest)) - else - (* let _ = Pp.msgnl (Printer.pr_lconstr x) in *) - raise (Found (case_eq_intros_rewrite x)) - | _ -> EConstr.iter sigma (fun c -> find_a_destructable_match sigma c) t - - -let destauto t = - Proofview.tclEVARMAP >>= fun sigma -> - try find_a_destructable_match sigma t; - Tacticals.New.tclZEROMSG (str "No destructable match found") - with Found tac -> tac - -let destauto_in id = - Proofview.Goal.enter begin fun gl -> - let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in -(* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) -(* Pp.msgnl (Printer.pr_lconstr (ctype)); *) - destauto ctype - end - -TACTIC EXTEND destauto -| [ "destauto" ] -> [ Proofview.Goal.enter begin fun gl -> destauto (Proofview.Goal.concl gl) end ] -| [ "destauto" "in" hyp(id) ] -> [ destauto_in id ] -END - -(**********************************************************************) - -(**********************************************************************) -(* A version of abstract constructing transparent terms *) -(* Introduced by Jason Gross and Benjamin Delaware in June 2016 *) -(**********************************************************************) - -TACTIC EXTEND transparent_abstract -| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end ] -| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end ] -END - -(* ********************************************************************* *) - -TACTIC EXTEND constr_eq -| [ "constr_eq" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:false x y ] -END - -TACTIC EXTEND constr_eq_strict -| [ "constr_eq_strict" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:true x y ] -END - -TACTIC EXTEND constr_eq_nounivs -| [ "constr_eq_nounivs" constr(x) constr(y) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - if eq_constr_nounivs sigma x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") ] -END - -TACTIC EXTEND is_evar -| [ "is_evar" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | Evar _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar") - ] -END - -TACTIC EXTEND has_evar -| [ "has_evar" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - if Evarutil.has_undefined_evars sigma x - then Proofview.tclUNIT () - else Tacticals.New.tclFAIL 0 (str "No evars") -] -END - -TACTIC EXTEND is_hyp -| [ "is_var" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | Var _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (str "Not a variable or hypothesis") ] -END - -TACTIC EXTEND is_fix -| [ "is_fix" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | Fix _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") ] -END;; - -TACTIC EXTEND is_cofix -| [ "is_cofix" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | CoFix _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") ] -END;; - -TACTIC EXTEND is_ind -| [ "is_ind" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | Ind _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not an (co)inductive datatype") ] -END;; - -TACTIC EXTEND is_constructor -| [ "is_constructor" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | Construct _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constructor") ] -END;; - -TACTIC EXTEND is_proj -| [ "is_proj" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | Proj _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a primitive projection") ] -END;; - -TACTIC EXTEND is_const -| [ "is_const" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | Const _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constant") ] -END;; - -(* Command to grab the evars left unresolved at the end of a proof. *) -(* 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 -[ "Grab" "Existential" "Variables" ] - => [ Vernac_classifier.classify_as_proofstep ] - -> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) ] -END - -(* Shelves all the goals under focus. *) -TACTIC EXTEND shelve -| [ "shelve" ] -> - [ Proofview.shelve ] -END - -(* Shelves the unifiable goals under focus, i.e. the goals which - appear in other goals under focus (the unfocused goals are not - considered). *) -TACTIC EXTEND shelve_unifiable -| [ "shelve_unifiable" ] -> - [ Proofview.shelve_unifiable ] -END - -(* Unshelves the goal shelved by the tactic. *) -TACTIC EXTEND unshelve -| [ "unshelve" tactic1(t) ] -> - [ - Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) -> - let gls = List.map Proofview.with_empty_state gls in - Proofview.Unsafe.tclGETGOALS >>= fun ogls -> - Proofview.Unsafe.tclSETGOALS (gls @ ogls) - ] -END - -(* Command to add every unshelved variables to the focus *) -VERNAC COMMAND EXTEND Unshelve -[ "Unshelve" ] - => [ Vernac_classifier.classify_as_proofstep ] - -> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) ] -END - -(* Gives up on the goals under focus: the goals are considered solved, - but the proof cannot be closed until the user goes back and solve - these goals. *) -TACTIC EXTEND give_up -| [ "give_up" ] -> - [ Proofview.give_up ] -END - -(* cycles [n] goals *) -TACTIC EXTEND cycle -| [ "cycle" int_or_var(n) ] -> [ Proofview.cycle n ] -END - -(* swaps goals number [i] and [j] *) -TACTIC EXTEND swap -| [ "swap" int_or_var(i) int_or_var(j) ] -> [ Proofview.swap i j ] -END - -(* reverses the list of focused goals *) -TACTIC EXTEND revgoals -| [ "revgoals" ] -> [ Proofview.revgoals ] -END - -type cmp = - | Eq - | Lt | Le - | Gt | Ge - -type 'i test = - | Test of cmp * 'i * 'i - -let pr_cmp = function - | Eq -> Pp.str"=" - | Lt -> Pp.str"<" - | Le -> Pp.str"<=" - | Gt -> Pp.str">" - | Ge -> Pp.str">=" - -let pr_cmp' _prc _prlc _prt = pr_cmp - -let pr_test_gen f (Test(c,x,y)) = - Pp.(f x ++ pr_cmp c ++ f y) - -let pr_test = pr_test_gen (Pputils.pr_or_var Pp.int) - -let pr_test' _prc _prlc _prt = pr_test - -let pr_itest = pr_test_gen Pp.int - -let pr_itest' _prc _prlc _prt = pr_itest - - - -ARGUMENT EXTEND comparison PRINTED BY pr_cmp' -| [ "=" ] -> [ Eq ] -| [ "<" ] -> [ Lt ] -| [ "<=" ] -> [ Le ] -| [ ">" ] -> [ Gt ] -| [ ">=" ] -> [ Ge ] - END - -let interp_test ist gls = function - | Test (c,x,y) -> - project gls , - Test(c,Tacinterp.interp_int_or_var ist x,Tacinterp.interp_int_or_var ist y) - -ARGUMENT EXTEND test - PRINTED BY pr_itest' - INTERPRETED BY interp_test - RAW_PRINTED BY pr_test' - GLOB_PRINTED BY pr_test' -| [ int_or_var(x) comparison(c) int_or_var(y) ] -> [ Test(c,x,y) ] -END - -let interp_cmp = function - | Eq -> Int.equal - | Lt -> ((<):int->int->bool) - | Le -> ((<=):int->int->bool) - | Gt -> ((>):int->int->bool) - | Ge -> ((>=):int->int->bool) - -let run_test = function - | Test(c,x,y) -> interp_cmp c x y - -let guard tst = - if run_test tst then - Proofview.tclUNIT () - else - let msg = Pp.(str"Condition not satisfied:"++ws 1++(pr_itest tst)) in - Tacticals.New.tclZEROMSG msg - - -TACTIC EXTEND guard -| [ "guard" test(tst) ] -> [ guard tst ] -END - -let decompose l c = - Proofview.Goal.enter begin fun gl -> - let sigma = Tacmach.New.project gl in - let to_ind c = - if isInd sigma c then fst (destInd sigma c) - else user_err Pp.(str "not an inductive type") - in - let l = List.map to_ind l in - Elim.h_decompose l c - end - -TACTIC EXTEND decompose -| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ] -END - -(** library/keys *) - -VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF -| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [ - let get_key c = - let env = Global.env () in - let evd = Evd.from_env env in - let (evd, c) = Constrintern.interp_open_constr env evd c in - let kind c = EConstr.kind evd c in - Keys.constr_key kind c - in - let k1 = get_key c in - let k2 = get_key c' in - match k1, k2 with - | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2 - | _ -> () ] -END - -VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY -| [ "Print" "Equivalent" "Keys" ] -> [ Feedback.msg_info (Keys.pr_keys Printer.pr_global) ] -END - - -VERNAC COMMAND EXTEND OptimizeProof -| [ "Optimize" "Proof" ] => [ Vernac_classifier.classify_as_proofstep ] -> - [ Proof_global.compact_the_proof () ] -| [ "Optimize" "Heap" ] => [ Vernac_classifier.classify_as_proofstep ] -> - [ Gc.compact () ] -END - -(** tactic analogous to "OPTIMIZE HEAP" *) - -let tclOPTIMIZE_HEAP = - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> Gc.compact ())) - -TACTIC EXTEND optimize_heap -| [ "optimize_heap" ] -> [ tclOPTIMIZE_HEAP ] -END diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg new file mode 100644 index 0000000000..b660865e8b --- /dev/null +++ b/plugins/ltac/extratactics.mlg @@ -0,0 +1,1160 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* replace_in_clause_maybe_by c1 c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac)) + +let replace_term ist dir_opt c cl = + with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl) + +} + +TACTIC EXTEND replace +| ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] +-> { replace_in_clause_maybe_by ist c1 c2 cl tac } +END + +TACTIC EXTEND replace_term_left +| [ "replace" "->" uconstr(c) clause(cl) ] + -> { replace_term ist (Some true) c cl } +END + +TACTIC EXTEND replace_term_right +| [ "replace" "<-" uconstr(c) clause(cl) ] + -> { replace_term ist (Some false) c cl } +END + +TACTIC EXTEND replace_term +| [ "replace" uconstr(c) clause(cl) ] + -> { replace_term ist None c cl } +END + +{ + +let induction_arg_of_quantified_hyp = function + | AnonHyp n -> None,ElimOnAnonHyp n + | NamedHyp id -> None,ElimOnIdent (CAst.make id) + +(* Versions *_main must come first!! so that "1" is interpreted as a + ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a + ElimOnIdent and not as "constr" *) + +let mytclWithHoles tac with_evars c = + Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let sigma = Tacmach.New.project gl in + let sigma',c = Tactics.force_destruction_arg with_evars env sigma c in + Tacticals.New.tclWITHHOLES with_evars (tac with_evars (Some c)) sigma' + end + +let elimOnConstrWithHoles tac with_evars c = + Tacticals.New.tclDELAYEDWITHHOLES with_evars c + (fun c -> tac with_evars (Some (None,ElimOnConstr c))) + +} + +TACTIC EXTEND simplify_eq +| [ "simplify_eq" ] -> { dEq ~keep_proofs:None false None } +| [ "simplify_eq" destruction_arg(c) ] -> { mytclWithHoles (dEq ~keep_proofs:None) false c } +END +TACTIC EXTEND esimplify_eq +| [ "esimplify_eq" ] -> { dEq ~keep_proofs:None true None } +| [ "esimplify_eq" destruction_arg(c) ] -> { mytclWithHoles (dEq ~keep_proofs:None) true c } +END + +{ + +let discr_main c = elimOnConstrWithHoles discr_tac false c + +} + +TACTIC EXTEND discriminate +| [ "discriminate" ] -> { discr_tac false None } +| [ "discriminate" destruction_arg(c) ] -> + { mytclWithHoles discr_tac false c } +END +TACTIC EXTEND ediscriminate +| [ "ediscriminate" ] -> { discr_tac true None } +| [ "ediscriminate" destruction_arg(c) ] -> + { mytclWithHoles discr_tac true c } +END + +{ + +let discrHyp id = + Proofview.tclEVARMAP >>= fun sigma -> + discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) + +let injection_main with_evars c = + elimOnConstrWithHoles (injClause None None) with_evars c + +} + +TACTIC EXTEND injection +| [ "injection" ] -> { injClause None None false None } +| [ "injection" destruction_arg(c) ] -> { mytclWithHoles (injClause None None) false c } +END +TACTIC EXTEND einjection +| [ "einjection" ] -> { injClause None None true None } +| [ "einjection" destruction_arg(c) ] -> { mytclWithHoles (injClause None None) true c } +END +TACTIC EXTEND injection_as +| [ "injection" "as" intropattern_list(ipat)] -> + { injClause None (Some ipat) false None } +| [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] -> + { mytclWithHoles (injClause None (Some ipat)) false c } +END +TACTIC EXTEND einjection_as +| [ "einjection" "as" intropattern_list(ipat)] -> + { injClause None (Some ipat) true None } +| [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> + { mytclWithHoles (injClause None (Some ipat)) true c } +END +TACTIC EXTEND simple_injection +| [ "simple" "injection" ] -> { simpleInjClause None false None } +| [ "simple" "injection" destruction_arg(c) ] -> { mytclWithHoles (simpleInjClause None) false c } +END + +{ + +let injHyp id = + Proofview.tclEVARMAP >>= fun sigma -> + injection_main false (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) + +} + +TACTIC EXTEND dependent_rewrite +| [ "dependent" "rewrite" orient(b) constr(c) ] -> { rewriteInConcl b c } +| [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ] + -> { rewriteInHyp b c id } +END + +(** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to + "replace u with t" or "enough (t=u) as <-" and + "cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *) + +TACTIC EXTEND cut_rewrite +| [ "cutrewrite" orient(b) constr(eqn) ] -> { cutRewriteInConcl b eqn } +| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ] + -> { cutRewriteInHyp b eqn id } +END + +(**********************************************************************) +(* Decompose *) + +TACTIC EXTEND decompose_sum +| [ "decompose" "sum" constr(c) ] -> { Elim.h_decompose_or c } +END + +TACTIC EXTEND decompose_record +| [ "decompose" "record" constr(c) ] -> { Elim.h_decompose_and c } +END + +(**********************************************************************) +(* Contradiction *) + +{ + +open Contradiction + +} + +TACTIC EXTEND absurd +| [ "absurd" constr(c) ] -> { absurd c } +END + +{ + +let onSomeWithHoles tac = function + | None -> tac None + | Some c -> Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c)) + +} + +TACTIC EXTEND contradiction +| [ "contradiction" constr_with_bindings_opt(c) ] -> + { onSomeWithHoles contradiction c } +END + +(**********************************************************************) +(* AutoRewrite *) + +{ + +open Autorewrite + +let pr_orient _prc _prlc _prt = function + | true -> Pp.mt () + | false -> Pp.str " <-" + +let pr_orient_string _prc _prlc _prt (orient, s) = + pr_orient _prc _prlc _prt orient ++ Pp.spc () ++ Pp.str s + +} + +ARGUMENT EXTEND orient_string TYPED AS (bool * string) PRINTED BY { pr_orient_string } +| [ orient(r) preident(i) ] -> { r, i } +END + +TACTIC EXTEND autorewrite +| [ "autorewrite" "with" ne_preident_list(l) clause(cl) ] -> + { auto_multi_rewrite l ( cl) } +| [ "autorewrite" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] -> + { + auto_multi_rewrite_with (Tacinterp.tactic_of_value ist t) l cl + } +END + +TACTIC EXTEND autorewrite_star +| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) ] -> + { auto_multi_rewrite ~conds:AllMatches l cl } +| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] -> + { auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_value ist t) l cl } +END + +(**********************************************************************) +(* Rewrite star *) + +{ + +let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) = + let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in + with_delayed_uconstr ist c + (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true) + +} + +TACTIC EXTEND rewrite_star +| [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] -> + { rewrite_star ist (Some id) o (occurrences_of occ) c tac } +| [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] -> + { rewrite_star ist (Some id) o (occurrences_of occ) c tac } +| [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) by_arg_tac(tac) ] -> + { rewrite_star ist (Some id) o Locus.AllOccurrences c tac } +| [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) by_arg_tac(tac) ] -> + { rewrite_star ist None o (occurrences_of occ) c tac } +| [ "rewrite" "*" orient(o) uconstr(c) by_arg_tac(tac) ] -> + { rewrite_star ist None o Locus.AllOccurrences c tac } + END + +(**********************************************************************) +(* Hint Rewrite *) + +{ + +let add_rewrite_hint ~poly bases ort t lcsr = + let env = Global.env() in + let sigma = Evd.from_env env in + let f ce = + let c, ctx = Constrintern.interp_constr env sigma ce in + let c = EConstr.to_constr sigma c in + let ctx = + let ctx = UState.context_set ctx in + if poly then ctx + else (** This is a global universe context that shouldn't be + refreshed at every use of the hint, declare it globally. *) + (Declare.declare_universe_context false ctx; + Univ.ContextSet.empty) + in + CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in + let eqs = List.map f lcsr in + let add_hints base = add_rew_rules base eqs in + List.iter add_hints bases + +let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater + +} + +VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY { classify_hint } +| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> + { add_rewrite_hint ~poly:atts.polymorphic bl o None l } +| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) + ":" preident_list(bl) ] -> + { add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l } +| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> + { add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l } +| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> + { add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l } +END + +(**********************************************************************) +(* Refine *) + +{ + +open EConstr +open Vars + +let constr_flags () = { + Pretyping.use_typeclasses = true; + Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics (); + Pretyping.use_hook = Pfedit.solve_by_implicit_tactic (); + Pretyping.fail_evar = false; + Pretyping.expand_evars = true } + +let refine_tac ist simple with_classes c = + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let flags = + { (constr_flags ()) with Pretyping.use_typeclasses = with_classes } in + let expected_type = Pretyping.OfType concl in + let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in + let update = begin fun sigma -> + c env sigma + end in + let refine = Refine.refine ~typecheck:false update in + if simple then refine + else refine <*> + Tactics.New.reduce_after_refine <*> + Proofview.shelve_unifiable + end + +} + +TACTIC EXTEND refine +| [ "refine" uconstr(c) ] -> + { refine_tac ist false true c } +END + +TACTIC EXTEND simple_refine +| [ "simple" "refine" uconstr(c) ] -> + { refine_tac ist true true c } +END + +TACTIC EXTEND notcs_refine +| [ "notypeclasses" "refine" uconstr(c) ] -> + { refine_tac ist false false c } +END + +TACTIC EXTEND notcs_simple_refine +| [ "simple" "notypeclasses" "refine" uconstr(c) ] -> + { refine_tac ist true false c } +END + +(* Solve unification constraints using heuristics or fail if any remain *) +TACTIC EXTEND solve_constraints +| [ "solve_constraints" ] -> { Refine.solve_constraints } +END + +(**********************************************************************) +(* Inversion lemmas (Leminv) *) + +{ + +open Inv +open Leminv + +let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater + +} + +(*VERNAC ARGUMENT EXTEND sort_family +| [ "Set" ] -> { InSet } +| [ "Prop" ] -> { InProp } +| [ "Type" ] -> { InType } +END*) + +VERNAC COMMAND EXTEND DeriveInversionClear +| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] + => { seff na } + -> { + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac } + +| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na } + -> { + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac } +END + +VERNAC COMMAND EXTEND DeriveInversion +| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] + => { seff na } + -> { + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac } + +| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na } + -> { + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac } +END + +VERNAC COMMAND EXTEND DeriveDependentInversion +| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] + => { seff na } + -> { + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac } +END + +VERNAC COMMAND EXTEND DeriveDependentInversionClear +| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] + => { seff na } + -> { + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac } +END + +(**********************************************************************) +(* Subst *) + +TACTIC EXTEND subst +| [ "subst" ne_var_list(l) ] -> { subst l } +| [ "subst" ] -> { subst_all () } +END + +{ + +let simple_subst_tactic_flags = + { only_leibniz = true; rewrite_dependent_proof = false } + +} + +TACTIC EXTEND simple_subst +| [ "simple" "subst" ] -> { subst_all ~flags:simple_subst_tactic_flags () } +END + +{ + +open Evar_tactics + +} + +(**********************************************************************) +(* Evar creation *) + +(* TODO: add support for some test similar to g_constr.name_colon so that + expressions like "evar (list A)" do not raise a syntax error *) +TACTIC EXTEND evar +| [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> { let_evar (Name.Name id) typ } +| [ "evar" constr(typ) ] -> { let_evar Name.Anonymous typ } +END + +TACTIC EXTEND instantiate +| [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] -> + { Tacticals.New.tclTHEN (instantiate_tac_by_name id c) Proofview.V82.nf_evar_goals } +| [ "instantiate" "(" integer(i) ":=" lglob(c) ")" hloc(hl) ] -> + { Tacticals.New.tclTHEN (instantiate_tac i c hl) Proofview.V82.nf_evar_goals } +| [ "instantiate" ] -> { Proofview.V82.nf_evar_goals } +END + +(**********************************************************************) +(** Nijmegen "step" tactic for setoid rewriting *) + +{ + +open Tactics +open Glob_term +open Libobject +open Lib + +(* Registered lemmas are expected to be of the form + x R y -> y == z -> x R z (in the right table) + x R y -> x == z -> z R y (in the left table) +*) + +let transitivity_right_table = Summary.ref [] ~name:"transitivity-steps-r" +let transitivity_left_table = Summary.ref [] ~name:"transitivity-steps-l" + +(* [step] tries to apply a rewriting lemma; then apply [tac] intended to + complete to proof of the last hypothesis (assumed to state an equality) *) + +let step left x tac = + let l = + List.map (fun lem -> + let lem = EConstr.of_constr lem in + Tacticals.New.tclTHENLAST + (apply_with_bindings (lem, ImplicitBindings [x])) + tac) + !(if left then transitivity_left_table else transitivity_right_table) + in + Tacticals.New.tclFIRST l + +(* Main function to push lemmas in persistent environment *) + +let cache_transitivity_lemma (_,(left,lem)) = + if left then + transitivity_left_table := lem :: !transitivity_left_table + else + transitivity_right_table := lem :: !transitivity_right_table + +let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) + +let inTransitivity : bool * Constr.t -> obj = + declare_object {(default_object "TRANSITIVITY-STEPS") with + cache_function = cache_transitivity_lemma; + open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o); + subst_function = subst_transitivity_lemma; + classify_function = (fun o -> Substitute o) } + +(* Main entry points *) + +let add_transitivity_lemma left lem = + let env = Global.env () in + let sigma = Evd.from_env env in + let lem',ctx (*FIXME*) = Constrintern.interp_constr env sigma lem in + let lem' = EConstr.to_constr sigma lem' in + add_anonymous_leaf (inTransitivity (left,lem')) + +} + +(* Vernacular syntax *) + +TACTIC EXTEND stepl +| ["stepl" constr(c) "by" tactic(tac) ] -> { step true c (Tacinterp.tactic_of_value ist tac) } +| ["stepl" constr(c) ] -> { step true c (Proofview.tclUNIT ()) } +END + +TACTIC EXTEND stepr +| ["stepr" constr(c) "by" tactic(tac) ] -> { step false c (Tacinterp.tactic_of_value ist tac) } +| ["stepr" constr(c) ] -> { step false c (Proofview.tclUNIT ()) } +END + +VERNAC COMMAND EXTEND AddStepl CLASSIFIED AS SIDEFF +| [ "Declare" "Left" "Step" constr(t) ] -> + { add_transitivity_lemma true t } +END + +VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF +| [ "Declare" "Right" "Step" constr(t) ] -> + { add_transitivity_lemma false t } +END + +{ + +let cache_implicit_tactic (_,tac) = match tac with + | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac) + | None -> Pfedit.clear_implicit_tactic () + +let subst_implicit_tactic (subst,tac) = + Option.map (Tacsubst.subst_tactic subst) tac + +let inImplicitTactic : glob_tactic_expr option -> obj = + declare_object {(default_object "IMPLICIT-TACTIC") with + open_function = (fun i o -> if Int.equal i 1 then cache_implicit_tactic o); + cache_function = cache_implicit_tactic; + subst_function = subst_implicit_tactic; + classify_function = (fun o -> Dispose)} + +let warn_deprecated_implicit_tactic = + CWarnings.create ~name:"deprecated-implicit-tactic" ~category:"deprecated" + (fun () -> strbrk "Implicit tactics are deprecated") + +let declare_implicit_tactic tac = + let () = warn_deprecated_implicit_tactic () in + Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac))) + +let clear_implicit_tactic () = + let () = warn_deprecated_implicit_tactic () in + Lib.add_anonymous_leaf (inImplicitTactic None) + +} + +VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF +| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> { declare_implicit_tactic tac } +| [ "Clear" "Implicit" "Tactic" ] -> { clear_implicit_tactic () } +END + + + + +(**********************************************************************) +(* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as + defined by Conor McBride *) +TACTIC EXTEND generalize_eqs +| ["generalize_eqs" hyp(id) ] -> { abstract_generalize ~generalize_vars:false id } +END +TACTIC EXTEND dep_generalize_eqs +| ["dependent" "generalize_eqs" hyp(id) ] -> { abstract_generalize ~generalize_vars:false ~force_dep:true id } +END +TACTIC EXTEND generalize_eqs_vars +| ["generalize_eqs_vars" hyp(id) ] -> { abstract_generalize ~generalize_vars:true id } +END +TACTIC EXTEND dep_generalize_eqs_vars +| ["dependent" "generalize_eqs_vars" hyp(id) ] -> { abstract_generalize ~force_dep:true ~generalize_vars:true id } +END + +(** Tactic to automatically simplify hypotheses of the form [Π Δ, x_i = t_i -> T] + where [t_i] is closed w.r.t. Δ. Such hypotheses are automatically generated + during dependent induction. For internal use. *) + +TACTIC EXTEND specialize_eqs +| [ "specialize_eqs" hyp(id) ] -> { specialize_eqs id } +END + +(**********************************************************************) +(* A tactic that considers a given occurrence of [c] in [t] and *) +(* abstract the minimal set of all the occurrences of [c] so that the *) +(* abstraction [fun x -> t[x/c]] is well-typed *) +(* *) +(* Contributed by Chung-Kil Hur (Winter 2009) *) +(**********************************************************************) + +{ + +let subst_var_with_hole occ tid t = + let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in + let locref = ref 0 in + let rec substrec x = match DAst.get x with + | GVar id -> + if Id.equal id tid + then + (decr occref; + if Int.equal !occref 0 then x + else + (incr locref; + DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ + GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Evar_kinds.Define true; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + }, IntroAnonymous, None))) + else x + | _ -> map_glob_constr_left_to_right substrec x in + let t' = substrec t + in + if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t' + +let subst_hole_with_term occ tc t = + let locref = ref 0 in + let occref = ref occ in + let rec substrec c = match DAst.get c with + | GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Evar_kinds.Define true; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + }, IntroAnonymous, s) -> + decr occref; + if Int.equal !occref 0 then tc + else + (incr locref; + DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ + GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Evar_kinds.Define true; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + },IntroAnonymous,s)) + | _ -> map_glob_constr_left_to_right substrec c + in + substrec t + +open Tacmach + +let hResolve id c occ t = + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Termops.clear_named_body id (Proofview.Goal.env gl) in + let concl = Proofview.Goal.concl gl in + let env_ids = Termops.vars_of_env env in + let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in + let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in + let rec resolve_hole t_hole = + try + Pretyping.understand env sigma t_hole + with + | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e -> + let (e, info) = CErrors.push e in + let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in + resolve_hole (subst_hole_with_term loc_begin c_raw t_hole) + in + let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in + let sigma = Evd.merge_universe_context sigma ctx in + let t_constr_type = Retyping.get_type_of env sigma t_constr in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (change_concl (mkLetIn (Name.Anonymous,t_constr,t_constr_type,concl))) + end + +let hResolve_auto id c t = + let rec resolve_auto n = + try + hResolve id c n t + with + | UserError _ as e -> raise e + | e when CErrors.noncritical e -> resolve_auto (n+1) + in + resolve_auto 1 + +} + +TACTIC EXTEND hresolve_core +| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> { hResolve id c occ t } +| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> { hResolve_auto id c t } +END + +(** + hget_evar +*) + +TACTIC EXTEND hget_evar +| [ "hget_evar" int_or_var(n) ] -> { Evar_tactics.hget_evar n } +END + +(**********************************************************************) + +(**********************************************************************) +(* A tactic that reduces one match t with ... by doing destruct t. *) +(* if t is not a variable, the tactic does *) +(* case_eq t;intros ... heq;rewrite heq in *|-. (but heq itself is *) +(* preserved). *) +(* Contributed by Julien Forest and Pierre Courtieu (july 2010) *) +(**********************************************************************) + +{ + +exception Found of unit Proofview.tactic + +let rewrite_except h = + Proofview.Goal.enter begin fun gl -> + let hyps = Tacmach.New.pf_ids_of_hyps gl in + Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else + Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false)) + hyps + end + + +let refl_equal () = Coqlib.lib_ref "core.eq.type" + +(* This is simply an implementation of the case_eq tactic. this code + should be replaced by a call to the tactic but I don't know how to + call it before it is defined. *) +let mkCaseEq a : unit Proofview.tactic = + Proofview.Goal.enter begin fun gl -> + let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in + Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req -> + Tacticals.New.tclTHENLIST + [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))]; + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + (** FIXME: this looks really wrong. Does anybody really use this tactic? *) + let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in + change_concl c + end; + simplest_case a] + end + + +let case_eq_intros_rewrite x = + Proofview.Goal.enter begin fun gl -> + let n = nb_prod (Tacmach.New.project gl) (Proofview.Goal.concl gl) in + (* Pp.msgnl (Printer.pr_lconstr x); *) + Tacticals.New.tclTHENLIST [ + mkCaseEq x; + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let hyps = Tacmach.New.pf_ids_set_of_hyps gl in + let n' = nb_prod (Tacmach.New.project gl) concl in + let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl) in + Tacticals.New.tclTHENLIST [ + Tacticals.New.tclDO (n'-n-1) intro; + introduction h; + rewrite_except h] + end + ] + end + +let rec find_a_destructable_match sigma t = + let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in + let cl = [cl, (None, None), None], None in + let dest = TacAtom (Loc.tag @@ TacInductionDestruct(false, false, cl)) in + match EConstr.kind sigma t with + | Case (_,_,x,_) when closed0 sigma x -> + if isVar sigma x then + (* TODO check there is no rel n. *) + raise (Found (Tacinterp.eval_tactic dest)) + else + (* let _ = Pp.msgnl (Printer.pr_lconstr x) in *) + raise (Found (case_eq_intros_rewrite x)) + | _ -> EConstr.iter sigma (fun c -> find_a_destructable_match sigma c) t + + +let destauto t = + Proofview.tclEVARMAP >>= fun sigma -> + try find_a_destructable_match sigma t; + Tacticals.New.tclZEROMSG (str "No destructable match found") + with Found tac -> tac + +let destauto_in id = + Proofview.Goal.enter begin fun gl -> + let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in +(* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) +(* Pp.msgnl (Printer.pr_lconstr (ctype)); *) + destauto ctype + end + +} + +TACTIC EXTEND destauto +| [ "destauto" ] -> { Proofview.Goal.enter begin fun gl -> destauto (Proofview.Goal.concl gl) end } +| [ "destauto" "in" hyp(id) ] -> { destauto_in id } +END + +(**********************************************************************) + +(**********************************************************************) +(* A version of abstract constructing transparent terms *) +(* Introduced by Jason Gross and Benjamin Delaware in June 2016 *) +(**********************************************************************) + +TACTIC EXTEND transparent_abstract +| [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl -> + Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } +| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl -> + Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } +END + +(* ********************************************************************* *) + +TACTIC EXTEND constr_eq +| [ "constr_eq" constr(x) constr(y) ] -> { Tactics.constr_eq ~strict:false x y } +END + +TACTIC EXTEND constr_eq_strict +| [ "constr_eq_strict" constr(x) constr(y) ] -> { Tactics.constr_eq ~strict:true x y } +END + +TACTIC EXTEND constr_eq_nounivs +| [ "constr_eq_nounivs" constr(x) constr(y) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + if eq_constr_nounivs sigma x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") } +END + +TACTIC EXTEND is_evar +| [ "is_evar" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | Evar _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar") + } +END + +TACTIC EXTEND has_evar +| [ "has_evar" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + if Evarutil.has_undefined_evars sigma x + then Proofview.tclUNIT () + else Tacticals.New.tclFAIL 0 (str "No evars") +} +END + +TACTIC EXTEND is_hyp +| [ "is_var" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | Var _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (str "Not a variable or hypothesis") } +END + +TACTIC EXTEND is_fix +| [ "is_fix" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | Fix _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") } +END + +TACTIC EXTEND is_cofix +| [ "is_cofix" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | CoFix _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") } +END + +TACTIC EXTEND is_ind +| [ "is_ind" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | Ind _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not an (co)inductive datatype") } +END + +TACTIC EXTEND is_constructor +| [ "is_constructor" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | Construct _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constructor") } +END + +TACTIC EXTEND is_proj +| [ "is_proj" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | Proj _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a primitive projection") } +END + +TACTIC EXTEND is_const +| [ "is_const" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | Const _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constant") } +END + +(* Command to grab the evars left unresolved at the end of a proof. *) +(* 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 +| [ "Grab" "Existential" "Variables" ] + => { Vernac_classifier.classify_as_proofstep } + -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) } +END + +(* Shelves all the goals under focus. *) +TACTIC EXTEND shelve +| [ "shelve" ] -> + { Proofview.shelve } +END + +(* Shelves the unifiable goals under focus, i.e. the goals which + appear in other goals under focus (the unfocused goals are not + considered). *) +TACTIC EXTEND shelve_unifiable +| [ "shelve_unifiable" ] -> + { Proofview.shelve_unifiable } +END + +(* Unshelves the goal shelved by the tactic. *) +TACTIC EXTEND unshelve +| [ "unshelve" tactic1(t) ] -> + { + Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) -> + let gls = List.map Proofview.with_empty_state gls in + Proofview.Unsafe.tclGETGOALS >>= fun ogls -> + Proofview.Unsafe.tclSETGOALS (gls @ ogls) + } +END + +(* Command to add every unshelved variables to the focus *) +VERNAC COMMAND EXTEND Unshelve +| [ "Unshelve" ] + => { Vernac_classifier.classify_as_proofstep } + -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) } +END + +(* Gives up on the goals under focus: the goals are considered solved, + but the proof cannot be closed until the user goes back and solve + these goals. *) +TACTIC EXTEND give_up +| [ "give_up" ] -> + { Proofview.give_up } +END + +(* cycles [n] goals *) +TACTIC EXTEND cycle +| [ "cycle" int_or_var(n) ] -> { Proofview.cycle n } +END + +(* swaps goals number [i] and [j] *) +TACTIC EXTEND swap +| [ "swap" int_or_var(i) int_or_var(j) ] -> { Proofview.swap i j } +END + +(* reverses the list of focused goals *) +TACTIC EXTEND revgoals +| [ "revgoals" ] -> { Proofview.revgoals } +END + +{ + +type cmp = + | Eq + | Lt | Le + | Gt | Ge + +type 'i test = + | Test of cmp * 'i * 'i + +let pr_cmp = function + | Eq -> Pp.str"=" + | Lt -> Pp.str"<" + | Le -> Pp.str"<=" + | Gt -> Pp.str">" + | Ge -> Pp.str">=" + +let pr_cmp' _prc _prlc _prt = pr_cmp + +let pr_test_gen f (Test(c,x,y)) = + Pp.(f x ++ pr_cmp c ++ f y) + +let pr_test = pr_test_gen (Pputils.pr_or_var Pp.int) + +let pr_test' _prc _prlc _prt = pr_test + +let pr_itest = pr_test_gen Pp.int + +let pr_itest' _prc _prlc _prt = pr_itest + +} + +ARGUMENT EXTEND comparison PRINTED BY { pr_cmp' } +| [ "=" ] -> { Eq } +| [ "<" ] -> { Lt } +| [ "<=" ] -> { Le } +| [ ">" ] -> { Gt } +| [ ">=" ] -> { Ge } + END + +{ + +let interp_test ist gls = function + | Test (c,x,y) -> + project gls , + Test(c,Tacinterp.interp_int_or_var ist x,Tacinterp.interp_int_or_var ist y) + +} + +ARGUMENT EXTEND test + PRINTED BY { pr_itest' } + INTERPRETED BY { interp_test } + RAW_PRINTED BY { pr_test' } + GLOB_PRINTED BY { pr_test' } +| [ int_or_var(x) comparison(c) int_or_var(y) ] -> { Test(c,x,y) } +END + +{ + +let interp_cmp = function + | Eq -> Int.equal + | Lt -> ((<):int->int->bool) + | Le -> ((<=):int->int->bool) + | Gt -> ((>):int->int->bool) + | Ge -> ((>=):int->int->bool) + +let run_test = function + | Test(c,x,y) -> interp_cmp c x y + +let guard tst = + if run_test tst then + Proofview.tclUNIT () + else + let msg = Pp.(str"Condition not satisfied:"++ws 1++(pr_itest tst)) in + Tacticals.New.tclZEROMSG msg + +} + +TACTIC EXTEND guard +| [ "guard" test(tst) ] -> { guard tst } +END + +{ + +let decompose l c = + Proofview.Goal.enter begin fun gl -> + let sigma = Tacmach.New.project gl in + let to_ind c = + if isInd sigma c then fst (destInd sigma c) + else user_err Pp.(str "not an inductive type") + in + let l = List.map to_ind l in + Elim.h_decompose l c + end + +} + +TACTIC EXTEND decompose +| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> { decompose l c } +END + +(** library/keys *) + +VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF +| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> { + let get_key c = + let env = Global.env () in + let evd = Evd.from_env env in + let (evd, c) = Constrintern.interp_open_constr env evd c in + let kind c = EConstr.kind evd c in + Keys.constr_key kind c + in + let k1 = get_key c in + let k2 = get_key c' in + match k1, k2 with + | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2 + | _ -> () } +END + +VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY +| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_info (Keys.pr_keys Printer.pr_global) } +END + + +VERNAC COMMAND EXTEND OptimizeProof +| [ "Optimize" "Proof" ] => { Vernac_classifier.classify_as_proofstep } -> + { Proof_global.compact_the_proof () } +| [ "Optimize" "Heap" ] => { Vernac_classifier.classify_as_proofstep } -> + { Gc.compact () } +END + +(** tactic analogous to "OPTIMIZE HEAP" *) + +{ + +let tclOPTIMIZE_HEAP = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> Gc.compact ())) + +} + +TACTIC EXTEND optimize_heap +| [ "optimize_heap" ] -> { tclOPTIMIZE_HEAP } +END diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 deleted file mode 100644 index 6913543c9a..0000000000 --- a/plugins/ltac/g_auto.ml4 +++ /dev/null @@ -1,226 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ Eauto.e_assumption ] -END - -TACTIC EXTEND eexact -| [ "eexact" constr(c) ] -> [ Eauto.e_give_exact c ] -END - -let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases - -ARGUMENT EXTEND hintbases - TYPED AS preident_list_opt - PRINTED BY pr_hintbases -| [ "with" "*" ] -> [ None ] -| [ "with" ne_preident_list(l) ] -> [ Some l ] -| [ ] -> [ Some [] ] -END - -let eval_uconstrs ist cs = - let flags = { - Pretyping.use_typeclasses = false; - solve_unification_constraints = true; - use_hook = Pfedit.solve_by_implicit_tactic (); - fail_evar = false; - expand_evars = true - } in - let map c env sigma = c env sigma in - List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs - -let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr -let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> - let _, env = Pfedit.get_current_context () in - Printer.pr_glob_constr_env env c) -let pr_auto_using _ _ _ = Pptactic.pr_auto_using - (let sigma, env = Pfedit.get_current_context () in - Printer.pr_closed_glob_env env sigma) - -ARGUMENT EXTEND auto_using - TYPED AS uconstr_list - PRINTED BY pr_auto_using - RAW_PRINTED BY pr_auto_using_raw - GLOB_PRINTED BY pr_auto_using_glob -| [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ] -| [ ] -> [ [] ] -END - -(** Auto *) - -TACTIC EXTEND trivial -| [ "trivial" auto_using(lems) hintbases(db) ] -> - [ Auto.h_trivial (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND info_trivial -| [ "info_trivial" auto_using(lems) hintbases(db) ] -> - [ Auto.h_trivial ~debug:Info (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND debug_trivial -| [ "debug" "trivial" auto_using(lems) hintbases(db) ] -> - [ Auto.h_trivial ~debug:Debug (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND auto -| [ "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> - [ Auto.h_auto n (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND info_auto -| [ "info_auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> - [ Auto.h_auto ~debug:Info n (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND debug_auto -| [ "debug" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> - [ Auto.h_auto ~debug:Debug n (eval_uconstrs ist lems) db ] -END - -(** Eauto *) - -TACTIC EXTEND prolog -| [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] -> - [ Eauto.prolog_tac (eval_uconstrs ist l) n ] -END - -let make_depth n = snd (Eauto.make_dimension n None) - -TACTIC EXTEND eauto -| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) - hintbases(db) ] -> - [ Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND new_eauto -| [ "new" "auto" int_or_var_opt(n) auto_using(lems) - hintbases(db) ] -> - [ match db with - | None -> Auto.new_full_auto (make_depth n) (eval_uconstrs ist lems) - | Some l -> Auto.new_auto (make_depth n) (eval_uconstrs ist lems) l ] -END - -TACTIC EXTEND debug_eauto -| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) - hintbases(db) ] -> - [ Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND info_eauto -| [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) - hintbases(db) ] -> - [ Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND dfs_eauto -| [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems) - hintbases(db) ] -> - [ Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND autounfold -| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> [ Eauto.autounfold_tac db cl ] -END - -TACTIC EXTEND autounfold_one -| [ "autounfold_one" hintbases(db) "in" hyp(id) ] -> - [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, Locus.InHyp)) ] -| [ "autounfold_one" hintbases(db) ] -> - [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ] - END - -TACTIC EXTEND unify -| ["unify" constr(x) constr(y) ] -> [ Tactics.unify x y ] -| ["unify" constr(x) constr(y) "with" preident(base) ] -> [ - let table = try Some (Hints.searchtable_map base) with Not_found -> None in - match table with - | None -> - let msg = str "Hint table " ++ str base ++ str " not found" in - Tacticals.New.tclZEROMSG msg - | Some t -> - let state = Hints.Hint_db.transparent_state t in - Tactics.unify ~state x y - ] -END - - -TACTIC EXTEND convert_concl_no_check -| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ] -END - -let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid -let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global -let glob_hints_path_atom ist = Hints.glob_hints_path_atom - -ARGUMENT EXTEND hints_path_atom - PRINTED BY pr_hints_path_atom - - GLOBALIZED BY glob_hints_path_atom - - RAW_PRINTED BY pr_pre_hints_path_atom - GLOB_PRINTED BY pr_hints_path_atom -| [ ne_global_list(g) ] -> [ Hints.PathHints g ] -| [ "_" ] -> [ Hints.PathAny ] -END - -let pr_hints_path prc prx pry c = Hints.pp_hints_path c -let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_qualid c -let glob_hints_path ist = Hints.glob_hints_path - -ARGUMENT EXTEND hints_path -PRINTED BY pr_hints_path - -GLOBALIZED BY glob_hints_path -RAW_PRINTED BY pr_pre_hints_path -GLOB_PRINTED BY pr_hints_path - -| [ "(" hints_path(p) ")" ] -> [ p ] -| [ hints_path(p) "*" ] -> [ Hints.PathStar p ] -| [ "emp" ] -> [ Hints.PathEmpty ] -| [ "eps" ] -> [ Hints.PathEpsilon ] -| [ hints_path(p) "|" hints_path(q) ] -> [ Hints.PathOr (p, q) ] -| [ hints_path_atom(a) ] -> [ Hints.PathAtom a ] -| [ hints_path(p) hints_path(q) ] -> [ Hints.PathSeq (p, q) ] -END - -ARGUMENT EXTEND opthints - TYPED AS preident_list_opt - PRINTED BY pr_hintbases -| [ ":" ne_preident_list(l) ] -> [ Some l ] -| [ ] -> [ None ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF -| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ - fun ~atts ~st -> begin - let open Vernacinterp in - let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints ~local:(Locality.make_section_locality atts.locality) - (match dbnames with None -> ["core"] | Some l -> l) entry; - st - end - ] -END - diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg new file mode 100644 index 0000000000..c07b653f3a --- /dev/null +++ b/plugins/ltac/g_auto.mlg @@ -0,0 +1,249 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { Eauto.e_assumption } +END + +TACTIC EXTEND eexact +| [ "eexact" constr(c) ] -> { Eauto.e_give_exact c } +END + +{ + +let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases + +} + +ARGUMENT EXTEND hintbases + TYPED AS preident list option + PRINTED BY { pr_hintbases } +| [ "with" "*" ] -> { None } +| [ "with" ne_preident_list(l) ] -> { Some l } +| [ ] -> { Some [] } +END + +{ + +let eval_uconstrs ist cs = + let flags = { + Pretyping.use_typeclasses = false; + solve_unification_constraints = true; + use_hook = Pfedit.solve_by_implicit_tactic (); + fail_evar = false; + expand_evars = true + } in + let map c env sigma = c env sigma in + List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs + +let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr +let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env c) +let pr_auto_using _ _ _ = Pptactic.pr_auto_using + (let sigma, env = Pfedit.get_current_context () in + Printer.pr_closed_glob_env env sigma) + +} + +ARGUMENT EXTEND auto_using + TYPED AS uconstr list + PRINTED BY { pr_auto_using } + RAW_PRINTED BY { pr_auto_using_raw } + GLOB_PRINTED BY { pr_auto_using_glob } +| [ "using" ne_uconstr_list_sep(l, ",") ] -> { l } +| [ ] -> { [] } +END + +(** Auto *) + +TACTIC EXTEND trivial +| [ "trivial" auto_using(lems) hintbases(db) ] -> + { Auto.h_trivial (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND info_trivial +| [ "info_trivial" auto_using(lems) hintbases(db) ] -> + { Auto.h_trivial ~debug:Info (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND debug_trivial +| [ "debug" "trivial" auto_using(lems) hintbases(db) ] -> + { Auto.h_trivial ~debug:Debug (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND auto +| [ "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> + { Auto.h_auto n (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND info_auto +| [ "info_auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> + { Auto.h_auto ~debug:Info n (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND debug_auto +| [ "debug" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> + { Auto.h_auto ~debug:Debug n (eval_uconstrs ist lems) db } +END + +(** Eauto *) + +TACTIC EXTEND prolog +| [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] -> + { Eauto.prolog_tac (eval_uconstrs ist l) n } +END + +{ + +let make_depth n = snd (Eauto.make_dimension n None) + +} + +TACTIC EXTEND eauto +| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + { Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND new_eauto +| [ "new" "auto" int_or_var_opt(n) auto_using(lems) + hintbases(db) ] -> + { match db with + | None -> Auto.new_full_auto (make_depth n) (eval_uconstrs ist lems) + | Some l -> Auto.new_auto (make_depth n) (eval_uconstrs ist lems) l } +END + +TACTIC EXTEND debug_eauto +| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + { Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND info_eauto +| [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + { Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND dfs_eauto +| [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + { Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND autounfold +| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> { Eauto.autounfold_tac db cl } +END + +TACTIC EXTEND autounfold_one +| [ "autounfold_one" hintbases(db) "in" hyp(id) ] -> + { Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, Locus.InHyp)) } +| [ "autounfold_one" hintbases(db) ] -> + { Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None } + END + +TACTIC EXTEND unify +| ["unify" constr(x) constr(y) ] -> { Tactics.unify x y } +| ["unify" constr(x) constr(y) "with" preident(base) ] -> { + let table = try Some (Hints.searchtable_map base) with Not_found -> None in + match table with + | None -> + let msg = str "Hint table " ++ str base ++ str " not found" in + Tacticals.New.tclZEROMSG msg + | Some t -> + let state = Hints.Hint_db.transparent_state t in + Tactics.unify ~state x y + } +END + + +TACTIC EXTEND convert_concl_no_check +| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl_no_check x DEFAULTcast } +END + +{ + +let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid +let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global +let glob_hints_path_atom ist = Hints.glob_hints_path_atom + +} + +ARGUMENT EXTEND hints_path_atom + PRINTED BY { pr_hints_path_atom } + + GLOBALIZED BY { glob_hints_path_atom } + + RAW_PRINTED BY { pr_pre_hints_path_atom } + GLOB_PRINTED BY { pr_hints_path_atom } +| [ ne_global_list(g) ] -> { Hints.PathHints g } +| [ "_" ] -> { Hints.PathAny } +END + +{ + +let pr_hints_path prc prx pry c = Hints.pp_hints_path c +let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_qualid c +let glob_hints_path ist = Hints.glob_hints_path + +} + +ARGUMENT EXTEND hints_path +PRINTED BY { pr_hints_path } + +GLOBALIZED BY { glob_hints_path } +RAW_PRINTED BY { pr_pre_hints_path } +GLOB_PRINTED BY { pr_hints_path } + +| [ "(" hints_path(p) ")" ] -> { p } +| [ hints_path(p) "*" ] -> { Hints.PathStar p } +| [ "emp" ] -> { Hints.PathEmpty } +| [ "eps" ] -> { Hints.PathEpsilon } +| [ hints_path(p) "|" hints_path(q) ] -> { Hints.PathOr (p, q) } +| [ hints_path_atom(a) ] -> { Hints.PathAtom a } +| [ hints_path(p) hints_path(q) ] -> { Hints.PathSeq (p, q) } +END + +ARGUMENT EXTEND opthints + TYPED AS preident list option + PRINTED BY { pr_hintbases } +| [ ":" ne_preident_list(l) ] -> { Some l } +| [ ] -> { None } +END + +VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF +| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { + let open Vernacinterp in + let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in + Hints.add_hints ~local:(Locality.make_section_locality atts.locality) + (match dbnames with None -> ["core"] | Some l -> l) entry; + } +END + diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 deleted file mode 100644 index 265368833b..0000000000 --- a/plugins/ltac/g_class.ml4 +++ /dev/null @@ -1,117 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* - let gr = Smartlocate.global_with_alias r in - let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in - Classes.set_typeclass_transparency ev (Locality.make_section_locality None) b) cl - -VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF -| [ "Typeclasses" "Transparent" reference_list(cl) ] -> [ - set_transparency cl true ] -END - -VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF -| [ "Typeclasses" "Opaque" reference_list(cl) ] -> [ - set_transparency cl false ] -END - -let pr_debug _prc _prlc _prt b = - if b then Pp.str "debug" else Pp.mt() - -ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug -| [ "debug" ] -> [ true ] -| [ ] -> [ false ] -END - -let pr_search_strategy _prc _prlc _prt = function - | Some Dfs -> Pp.str "dfs" - | Some Bfs -> Pp.str "bfs" - | None -> Pp.mt () - -ARGUMENT EXTEND eauto_search_strategy PRINTED BY pr_search_strategy -| [ "(bfs)" ] -> [ Some Bfs ] -| [ "(dfs)" ] -> [ Some Dfs ] -| [ ] -> [ None ] -END - -(* true = All transparent, false = Opaque if possible *) - -VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF - | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> [ - set_typeclasses_debug d; - Option.iter set_typeclasses_strategy s; - set_typeclasses_depth depth - ] -END - -(** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *) -TACTIC EXTEND typeclasses_eauto - | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] -> - [ typeclasses_eauto ~strategy:Bfs ~depth:d l ] - | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> - [ typeclasses_eauto ~depth:d l ] - | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [ - typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ] -END - -TACTIC EXTEND head_of_constr - [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h c ] -END - -TACTIC EXTEND not_evar - [ "not_evar" constr(ty) ] -> [ not_evar ty ] -END - -TACTIC EXTEND is_ground - [ "is_ground" constr(ty) ] -> [ is_ground ty ] -END - -TACTIC EXTEND autoapply - [ "autoapply" constr(c) "using" preident(i) ] -> [ autoapply c i ] -END - -(** TODO: DEPRECATE *) -(* A progress test that allows to see if the evars have changed *) -open Constr -open Proofview.Notations - -let rec eq_constr_mod_evars sigma x y = - let open EConstr in - match EConstr.kind sigma x, EConstr.kind sigma y with - | Evar (e1, l1), Evar (e2, l2) when not (Evar.equal e1 e2) -> true - | _, _ -> compare_constr sigma (fun x y -> eq_constr_mod_evars sigma x y) x y - -let progress_evars t = - Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let check = - Proofview.Goal.enter begin fun gl' -> - let sigma = Tacmach.New.project gl' in - let newconcl = Proofview.Goal.concl gl' in - if eq_constr_mod_evars sigma concl newconcl - then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)") - else Proofview.tclUNIT () - end - in t <*> check - end - -TACTIC EXTEND progress_evars - [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.tactic_of_value ist t) ] -END diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg new file mode 100644 index 0000000000..9ecc36bdf3 --- /dev/null +++ b/plugins/ltac/g_class.mlg @@ -0,0 +1,137 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + let gr = Smartlocate.global_with_alias r in + let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in + Classes.set_typeclass_transparency ev (Locality.make_section_locality None) b) cl + +} + +VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF +| [ "Typeclasses" "Transparent" reference_list(cl) ] -> { + set_transparency cl true } +END + +VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF +| [ "Typeclasses" "Opaque" reference_list(cl) ] -> { + set_transparency cl false } +END + +{ + +let pr_debug _prc _prlc _prt b = + if b then Pp.str "debug" else Pp.mt() + +} + +ARGUMENT EXTEND debug TYPED AS bool PRINTED BY { pr_debug } +| [ "debug" ] -> { true } +| [ ] -> { false } +END + +{ + +let pr_search_strategy _prc _prlc _prt = function + | Some Dfs -> Pp.str "dfs" + | Some Bfs -> Pp.str "bfs" + | None -> Pp.mt () + +} + +ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy } +| [ "(bfs)" ] -> { Some Bfs } +| [ "(dfs)" ] -> { Some Dfs } +| [ ] -> { None } +END + +(* true = All transparent, false = Opaque if possible *) + +VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF + | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> { + set_typeclasses_debug d; + Option.iter set_typeclasses_strategy s; + set_typeclasses_depth depth + } +END + +(** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *) +TACTIC EXTEND typeclasses_eauto + | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] -> + { typeclasses_eauto ~strategy:Bfs ~depth:d l } + | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> + { typeclasses_eauto ~depth:d l } + | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> { + typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] } +END + +TACTIC EXTEND head_of_constr +| [ "head_of_constr" ident(h) constr(c) ] -> { head_of_constr h c } +END + +TACTIC EXTEND not_evar +| [ "not_evar" constr(ty) ] -> { not_evar ty } +END + +TACTIC EXTEND is_ground +| [ "is_ground" constr(ty) ] -> { is_ground ty } +END + +TACTIC EXTEND autoapply +| [ "autoapply" constr(c) "using" preident(i) ] -> { autoapply c i } +END + +{ + +(** TODO: DEPRECATE *) +(* A progress test that allows to see if the evars have changed *) +open Constr +open Proofview.Notations + +let rec eq_constr_mod_evars sigma x y = + let open EConstr in + match EConstr.kind sigma x, EConstr.kind sigma y with + | Evar (e1, l1), Evar (e2, l2) when not (Evar.equal e1 e2) -> true + | _, _ -> compare_constr sigma (fun x y -> eq_constr_mod_evars sigma x y) x y + +let progress_evars t = + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let check = + Proofview.Goal.enter begin fun gl' -> + let sigma = Tacmach.New.project gl' in + let newconcl = Proofview.Goal.concl gl' in + if eq_constr_mod_evars sigma concl newconcl + then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)") + else Proofview.tclUNIT () + end + in t <*> check + end + +} + +TACTIC EXTEND progress_evars +| [ "progress_evars" tactic(t) ] -> { progress_evars (Tacinterp.tactic_of_value ist t) } +END diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 deleted file mode 100644 index 929390b1c4..0000000000 --- a/plugins/ltac/g_ltac.ml4 +++ /dev/null @@ -1,528 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* a - | e -> Tacexp (e:raw_tactic_expr) - -let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () -let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n -let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat -let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c -let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac - -let reference_to_id qid = - if Libnames.qualid_is_ident qid then - CAst.make ?loc:qid.CAst.loc @@ Libnames.qualid_basename qid - else - CErrors.user_err ?loc:qid.CAst.loc - (str "This expression should be a simple identifier.") - -let tactic_mode = Entry.create "vernac:tactic_command" - -let new_entry name = - let e = Entry.create name in - e - -let toplevel_selector = new_entry "vernac:toplevel_selector" -let tacdef_body = new_entry "tactic:tacdef_body" - -(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for - proof editing and changes nothing else). Then sets it as the default proof mode. *) -let _ = - let mode = { - Proof_global.name = "Classic"; - set = (fun () -> Pvernac.set_command_entry tactic_mode); - reset = (fun () -> Pvernac.(set_command_entry noedit_mode)); - } in - Proof_global.register_proof_mode mode - -(* Hack to parse "[ id" without dropping [ *) -let test_bracket_ident = - Gram.Entry.of_parser "test_bracket_ident" - (fun strm -> - match stream_nth 0 strm with - | KEYWORD "[" -> - (match stream_nth 1 strm with - | IDENT _ -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - -(* Tactics grammar rules *) - -let hint = G_proofs.hint - -GEXTEND Gram - GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint - tactic_mode constr_may_eval constr_eval toplevel_selector - operconstr; - - tactic_then_last: - [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> - Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) - | -> [||] - ] ] - ; - tactic_then_gen: - [ [ ta = tactic_expr; "|"; (first,last) = tactic_then_gen -> (ta::first, last) - | ta = tactic_expr; ".."; l = tactic_then_last -> ([], Some (ta, l)) - | ".."; l = tactic_then_last -> ([], Some (TacId [], l)) - | ta = tactic_expr -> ([ta], None) - | "|"; (first,last) = tactic_then_gen -> (TacId [] :: first, last) - | -> ([TacId []], None) - ] ] - ; - tactic_then_locality: (* [true] for the local variant [TacThens] and [false] - for [TacExtend] *) - [ [ "[" ; l = OPT">" -> if Option.is_empty l then true else false ] ] - ; - tactic_expr: - [ "5" RIGHTA - [ te = binder_tactic -> te ] - | "4" LEFTA - [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1) - | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0,ta1) - | ta0 = tactic_expr; ";"; l = tactic_then_locality; (first,tail) = tactic_then_gen; "]" -> - match l , tail with - | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last)) - | true , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last) - | false , None -> TacThen (ta0,TacDispatch first) - | true , None -> TacThens (ta0,first) ] - | "3" RIGHTA - [ IDENT "try"; ta = tactic_expr -> TacTry ta - | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta) - | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta) - | IDENT "time"; s = OPT string; ta = tactic_expr -> TacTime (s,ta) - | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta - | IDENT "progress"; ta = tactic_expr -> TacProgress ta - | IDENT "once"; ta = tactic_expr -> TacOnce ta - | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta - | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta -(*To do: put Abstract in Refiner*) - | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None) - | IDENT "abstract"; tc = NEXT; "using"; s = ident -> - TacAbstract (tc,Some s) - | sel = selector; ta = tactic_expr -> TacSelect (sel, ta) ] -(*End of To do*) - | "2" RIGHTA - [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1) - | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> TacOr (ta0,ta1) - | IDENT "tryif" ; ta = tactic_expr ; - "then" ; tat = tactic_expr ; - "else" ; tae = tactic_expr -> TacIfThenCatch(ta,tat,tae) - | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1) - | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] - | "1" RIGHTA - [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> - TacMatchGoal (b,false,mrl) - | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; - mrl = match_context_list; "end" -> - TacMatchGoal (b,true,mrl) - | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" -> - TacMatch (b,c,mrl) - | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> - TacFirst l - | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> - TacSolve l - | IDENT "idtac"; l = LIST0 message_token -> TacId l - | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ]; - l = LIST0 message_token -> TacFail (g,n,l) - | st = simple_tactic -> st - | a = tactic_arg -> TacArg(Loc.tag ~loc:!@loc a) - | r = reference; la = LIST0 tactic_arg_compat -> - TacArg(Loc.tag ~loc:!@loc @@ TacCall (Loc.tag ~loc:!@loc (r,la))) ] - | "0" - [ "("; a = tactic_expr; ")" -> a - | "["; ">"; (tf,tail) = tactic_then_gen; "]" -> - begin match tail with - | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) - | None -> TacDispatch tf - end - | a = tactic_atom -> TacArg (Loc.tag ~loc:!@loc a) ] ] - ; - failkw: - [ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ] - ; - (* binder_tactic: level 5 of tactic_expr *) - binder_tactic: - [ RIGHTA - [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> - TacFun (it,body) - | "let"; isrec = [IDENT "rec" -> true | -> false]; - llc = LIST1 let_clause SEP "with"; "in"; - body = tactic_expr LEVEL "5" -> TacLetIn (isrec,llc,body) - | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ] - ; - (* Tactic arguments to the right of an application *) - tactic_arg_compat: - [ [ a = tactic_arg -> a - | c = Constr.constr -> (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) - (* Unambiguous entries: tolerated w/o "ltac:" modifier *) - | "()" -> TacGeneric (genarg_of_unit ()) ] ] - ; - (* Can be used as argument and at toplevel in tactic expressions. *) - tactic_arg: - [ [ c = constr_eval -> ConstrMayEval c - | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l - | IDENT "type_term"; c=uconstr -> TacPretype c - | IDENT "numgoals" -> TacNumgoals ] ] - ; - (* If a qualid is given, use its short name. TODO: have the shortest - non ambiguous name where dots are replaced by "_"? Probably too - verbose most of the time. *) - fresh_id: - [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) - | qid = qualid -> Locus.ArgVar (CAst.make ~loc:!@loc @@ Libnames.qualid_basename qid) ] ] - ; - constr_eval: - [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> - ConstrEval (rtc,c) - | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" -> - ConstrContext (id,c) - | IDENT "type"; IDENT "of"; c = Constr.constr -> - ConstrTypeOf c ] ] - ; - constr_may_eval: (* For extensions *) - [ [ c = constr_eval -> c - | c = Constr.constr -> ConstrTerm c ] ] - ; - tactic_atom: - [ [ n = integer -> TacGeneric (genarg_of_int n) - | r = reference -> TacCall (Loc.tag ~loc:!@loc (r,[])) - | "()" -> TacGeneric (genarg_of_unit ()) ] ] - ; - match_key: - [ [ "match" -> Once - | "lazymatch" -> Select - | "multimatch" -> General ] ] - ; - input_fun: - [ [ "_" -> Name.Anonymous - | l = ident -> Name.Name l ] ] - ; - let_clause: - [ [ idr = identref; ":="; te = tactic_expr -> - (CAst.map (fun id -> Name id) idr, arg_of_expr te) - | na = ["_" -> CAst.make ~loc:!@loc Anonymous]; ":="; te = tactic_expr -> - (na, arg_of_expr te) - | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> - (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) ] ] - ; - match_pattern: - [ [ IDENT "context"; oid = OPT Constr.ident; - "["; pc = Constr.lconstr_pattern; "]" -> - Subterm (oid, pc) - | pc = Constr.lconstr_pattern -> Term pc ] ] - ; - match_hyps: - [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) - | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> Def (na, mpv, mpt) - | na = name; ":="; mpv = match_pattern -> - let t, ty = - match mpv with - | Term t -> (match t with - | { CAst.v = CCast (t, (CastConv ty | CastVM ty | CastNative ty)) } -> Term t, Some (Term ty) - | _ -> mpv, None) - | _ -> mpv, None - in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty) - ] ] - ; - match_context_rule: - [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "=>"; te = tactic_expr -> Pat (largs, mp, te) - | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "]"; "=>"; te = tactic_expr -> Pat (largs, mp, te) - | "_"; "=>"; te = tactic_expr -> All te ] ] - ; - match_context_list: - [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl - | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ] - ; - match_rule: - [ [ mp = match_pattern; "=>"; te = tactic_expr -> Pat ([],mp,te) - | "_"; "=>"; te = tactic_expr -> All te ] ] - ; - match_list: - [ [ mrl = LIST1 match_rule SEP "|" -> mrl - | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ] - ; - message_token: - [ [ id = identref -> MsgIdent id - | s = STRING -> MsgString s - | n = integer -> MsgInt n ] ] - ; - - ltac_def_kind: - [ [ ":=" -> false - | "::=" -> true ] ] - ; - - (* Definitions for tactics *) - tacdef_body: - [ [ name = Constr.global; it=LIST1 input_fun; - redef = ltac_def_kind; body = tactic_expr -> - if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) - else - let id = reference_to_id name in - Tacexpr.TacticDefinition (id, TacFun (it, body)) - | name = Constr.global; redef = ltac_def_kind; - body = tactic_expr -> - if redef then Tacexpr.TacticRedefinition (name, body) - else - let id = reference_to_id name in - Tacexpr.TacticDefinition (id, body) - ] ] - ; - tactic: - [ [ tac = tactic_expr -> tac ] ] - ; - - range_selector: - [ [ n = natural ; "-" ; m = natural -> (n, m) - | n = natural -> (n, n) ] ] - ; - (* We unfold a range selectors list once so that we can make a special case - * for a unique SelectNth selector. *) - range_selector_or_nth: - [ [ n = natural ; "-" ; m = natural; - l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> - Goal_select.SelectList ((n, m) :: Option.default [] l) - | n = natural; - l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> - let open Goal_select in - Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ] - ; - selector_body: - [ [ l = range_selector_or_nth -> l - | test_bracket_ident; "["; id = ident; "]" -> Goal_select.SelectId id ] ] - ; - selector: - [ [ IDENT "only"; sel = selector_body; ":" -> sel ] ] - ; - toplevel_selector: - [ [ sel = selector_body; ":" -> sel - | "!"; ":" -> Goal_select.SelectAlreadyFocused - | IDENT "all"; ":" -> Goal_select.SelectAll ] ] - ; - tactic_mode: - [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g - | g = OPT toplevel_selector; "{" -> Vernacexpr.VernacSubproof g ] ] - ; - command: - [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; - l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] -> - Vernacexpr.VernacProof (Some (in_tac ta), l) - | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; - ta = OPT [ "with"; ta = Pltac.tactic -> in_tac ta ] -> - Vernacexpr.VernacProof (ta,Some l) ] ] - ; - hint: - [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; - tac = Pltac.tactic -> - Hints.HintsExtern (n,c, in_tac tac) ] ] - ; - operconstr: LEVEL "0" - [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> - let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in - CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ] - ; - END - -open Stdarg -open Tacarg -open Vernacexpr -open Vernac_classifier -open Goptions -open Libnames - -let print_info_trace = ref None - -let _ = declare_int_option { - optdepr = false; - optname = "print info trace"; - optkey = ["Info" ; "Level"]; - optread = (fun () -> !print_info_trace); - optwrite = fun n -> print_info_trace := n; -} - -let vernac_solve n info tcom b = - let open Goal_select in - let status = Proof_global.with_current_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 - let (p,status) = - Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p - in - (* in case a strict subtree was completed, - go back to the top of the prooftree *) - let p = Proof.maximal_unfocus Vernacentries.command_focus p in - p,status) in - if not status then Feedback.feedback Feedback.AddedAxiom - -let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s - -VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector -| [ toplevel_selector(s) ] -> [ s ] -END - -let pr_ltac_info n = str "Info" ++ spc () ++ int n - -VERNAC ARGUMENT EXTEND ltac_info PRINTED BY pr_ltac_info -| [ "Info" natural(n) ] -> [ n ] -END - -let pr_ltac_use_default b = - if b then (* Bug: a space is inserted before "..." *) str ".." else mt () - -VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default -| [ "." ] -> [ false ] -| [ "..." ] -> [ true ] -END - -let is_anonymous_abstract = function - | TacAbstract (_,None) -> true - | TacSolve [TacAbstract (_,None)] -> true - | _ -> false -let rm_abstract = function - | TacAbstract (t,_) -> t - | TacSolve [TacAbstract (t,_)] -> TacSolve [t] - | x -> x -let is_explicit_terminator = function TacSolve _ -> true | _ -> false - -VERNAC tactic_mode EXTEND VernacSolve -| [ - 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 - vernac_solve g n t 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 - let parallel = `Yes (solving_tac,anon_abstracting_tac) in - let pbr = if solving_tac then Some "par" else None in - VtProofStep{ parallel = parallel; proof_block_detection = pbr }, - VtLater - ] -> [ - let t = rm_abstract t in - vernac_solve Goal_select.SelectAll n t def - ] -END - -let pr_ltac_tactic_level n = str "(at level " ++ int n ++ str ")" - -VERNAC ARGUMENT EXTEND ltac_tactic_level PRINTED BY pr_ltac_tactic_level -| [ "(" "at" "level" natural(n) ")" ] -> [ n ] -END - -VERNAC ARGUMENT EXTEND ltac_production_sep -| [ "," string(sep) ] -> [ sep ] -END - -let pr_ltac_production_item = function -| Tacentries.TacTerm s -> quote (str s) -| Tacentries.TacNonTerm (_, ((arg, None), None)) -> str arg -| Tacentries.TacNonTerm (_, ((arg, Some _), None)) -> assert false -| Tacentries.TacNonTerm (_, ((arg, sep), Some id)) -> - let sep = match sep with - | None -> mt () - | Some sep -> str "," ++ spc () ++ quote (str sep) - in - str arg ++ str "(" ++ Id.print id ++ sep ++ str ")" - -VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item -| [ string(s) ] -> [ Tacentries.TacTerm s ] -| [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] -> - [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, sep), Some p)) ] -| [ ident(nt) ] -> - [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation -| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => - [ VtSideff [], VtNow ] -> - [ fun ~atts ~st -> let open Vernacinterp in - let n = Option.default 0 n in - let deprecation = atts.deprecated in - Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e; - st - ] -END - -VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY -| [ "Print" "Ltac" reference(r) ] -> - [ Feedback.msg_notice (Tacintern.print_ltac r) ] -END - -VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY -| [ "Locate" "Ltac" reference(r) ] -> - [ Tacentries.print_located_tactic r ] -END - -let pr_ltac_ref = Libnames.pr_qualid - -let pr_tacdef_body tacdef_body = - let id, redef, body = - match tacdef_body with - | TacticDefinition ({CAst.v=id}, body) -> Id.print id, false, body - | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body - in - let idl, body = - match body with - | Tacexpr.TacFun (idl,b) -> idl,b - | _ -> [], body in - id ++ - prlist (function Name.Anonymous -> str " _" - | Name.Name id -> spc () ++ Id.print id) idl - ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) - ++ Pptactic.pr_raw_tactic body - -VERNAC ARGUMENT EXTEND ltac_tacdef_body -PRINTED BY pr_tacdef_body -| [ tacdef_body(t) ] -> [ t ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition -| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ - VtSideff (List.map (function - | TacticDefinition ({CAst.v=r},_) -> r - | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater - ] -> [ fun ~atts ~st -> let open Vernacinterp in - let deprecation = atts.deprecated in - Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l; - st - ] -END - -VERNAC COMMAND EXTEND VernacPrintLtacs CLASSIFIED AS QUERY -| [ "Print" "Ltac" "Signatures" ] -> [ Tacentries.print_ltacs () ] -END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg new file mode 100644 index 0000000000..d62f985350 --- /dev/null +++ b/plugins/ltac/g_ltac.mlg @@ -0,0 +1,560 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* a + | e -> Tacexp (e:raw_tactic_expr) + +let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () +let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n +let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat +let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c +let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac + +let reference_to_id qid = + if Libnames.qualid_is_ident qid then + CAst.make ?loc:qid.CAst.loc @@ Libnames.qualid_basename qid + else + CErrors.user_err ?loc:qid.CAst.loc + (str "This expression should be a simple identifier.") + +let tactic_mode = Entry.create "vernac:tactic_command" + +let new_entry name = + let e = Entry.create name in + e + +let toplevel_selector = new_entry "vernac:toplevel_selector" +let tacdef_body = new_entry "tactic:tacdef_body" + +(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for + proof editing and changes nothing else). Then sets it as the default proof mode. *) +let _ = + let mode = { + Proof_global.name = "Classic"; + set = (fun () -> Pvernac.set_command_entry tactic_mode); + reset = (fun () -> Pvernac.(set_command_entry noedit_mode)); + } in + Proof_global.register_proof_mode mode + +(* Hack to parse "[ id" without dropping [ *) +let test_bracket_ident = + Gram.Entry.of_parser "test_bracket_ident" + (fun strm -> + match stream_nth 0 strm with + | KEYWORD "[" -> + (match stream_nth 1 strm with + | IDENT _ -> () + | _ -> raise Stream.Failure) + | _ -> raise Stream.Failure) + +(* Tactics grammar rules *) + +let hint = G_proofs.hint + +} + +GRAMMAR EXTEND Gram + GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint + tactic_mode constr_may_eval constr_eval toplevel_selector + operconstr; + + tactic_then_last: + [ [ "|"; lta = LIST0 (OPT tactic_expr) SEP "|" -> + { Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) } + | -> { [||] } + ] ] + ; + tactic_then_gen: + [ [ ta = tactic_expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (ta::first, last) } + | ta = tactic_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) } + | ".."; l = tactic_then_last -> { ([], Some (TacId [], l)) } + | ta = tactic_expr -> { ([ta], None) } + | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (TacId [] :: first, last) } + | -> { ([TacId []], None) } + ] ] + ; + tactic_then_locality: (* [true] for the local variant [TacThens] and [false] + for [TacExtend] *) + [ [ "[" ; l = OPT">" -> { if Option.is_empty l then true else false } ] ] + ; + tactic_expr: + [ "5" RIGHTA + [ te = binder_tactic -> { te } ] + | "4" LEFTA + [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) } + | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> { TacThen (ta0,ta1) } + | ta0 = tactic_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> { + let (first,tail) = tg in + match l , tail with + | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last)) + | true , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last) + | false , None -> TacThen (ta0,TacDispatch first) + | true , None -> TacThens (ta0,first) } ] + | "3" RIGHTA + [ IDENT "try"; ta = tactic_expr -> { TacTry ta } + | IDENT "do"; n = int_or_var; ta = tactic_expr -> { TacDo (n,ta) } + | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> { TacTimeout (n,ta) } + | IDENT "time"; s = OPT string; ta = tactic_expr -> { TacTime (s,ta) } + | IDENT "repeat"; ta = tactic_expr -> { TacRepeat ta } + | IDENT "progress"; ta = tactic_expr -> { TacProgress ta } + | IDENT "once"; ta = tactic_expr -> { TacOnce ta } + | IDENT "exactly_once"; ta = tactic_expr -> { TacExactlyOnce ta } + | IDENT "infoH"; ta = tactic_expr -> { TacShowHyps ta } +(*To do: put Abstract in Refiner*) + | IDENT "abstract"; tc = NEXT -> { TacAbstract (tc,None) } + | IDENT "abstract"; tc = NEXT; "using"; s = ident -> + { TacAbstract (tc,Some s) } + | sel = selector; ta = tactic_expr -> { TacSelect (sel, ta) } ] +(*End of To do*) + | "2" RIGHTA + [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) } + | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> { TacOr (ta0,ta1) } + | IDENT "tryif" ; ta = tactic_expr ; + "then" ; tat = tactic_expr ; + "else" ; tae = tactic_expr -> { TacIfThenCatch(ta,tat,tae) } + | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) } + | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> { TacOrelse (ta0,ta1) } ] + | "1" RIGHTA + [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> + { TacMatchGoal (b,false,mrl) } + | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; + mrl = match_context_list; "end" -> + { TacMatchGoal (b,true,mrl) } + | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" -> + { TacMatch (b,c,mrl) } + | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + { TacFirst l } + | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + { TacSolve l } + | IDENT "idtac"; l = LIST0 message_token -> { TacId l } + | g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ]; + l = LIST0 message_token -> { TacFail (g,n,l) } + | st = simple_tactic -> { st } + | a = tactic_arg -> { TacArg(Loc.tag ~loc a) } + | r = reference; la = LIST0 tactic_arg_compat -> + { TacArg(Loc.tag ~loc @@ TacCall (Loc.tag ~loc (r,la))) } ] + | "0" + [ "("; a = tactic_expr; ")" -> { a } + | "["; ">"; tg = tactic_then_gen; "]" -> { + let (tf,tail) = tg in + begin match tail with + | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) + | None -> TacDispatch tf + end } + | a = tactic_atom -> { TacArg (Loc.tag ~loc a) } ] ] + ; + failkw: + [ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ] + ; + (* binder_tactic: level 5 of tactic_expr *) + binder_tactic: + [ RIGHTA + [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> + { TacFun (it,body) } + | "let"; isrec = [IDENT "rec" -> { true } | -> { false } ]; + llc = LIST1 let_clause SEP "with"; "in"; + body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } + | IDENT "info"; tc = tactic_expr LEVEL "5" -> { TacInfo tc } ] ] + ; + (* Tactic arguments to the right of an application *) + tactic_arg_compat: + [ [ a = tactic_arg -> { a } + | c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) } + (* Unambiguous entries: tolerated w/o "ltac:" modifier *) + | "()" -> { TacGeneric (genarg_of_unit ()) } ] ] + ; + (* Can be used as argument and at toplevel in tactic expressions. *) + tactic_arg: + [ [ c = constr_eval -> { ConstrMayEval c } + | IDENT "fresh"; l = LIST0 fresh_id -> { TacFreshId l } + | IDENT "type_term"; c=uconstr -> { TacPretype c } + | IDENT "numgoals" -> { TacNumgoals } ] ] + ; + (* If a qualid is given, use its short name. TODO: have the shortest + non ambiguous name where dots are replaced by "_"? Probably too + verbose most of the time. *) + fresh_id: + [ [ s = STRING -> { Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) } + | qid = qualid -> { Locus.ArgVar (CAst.make ~loc @@ Libnames.qualid_basename qid) } ] ] + ; + constr_eval: + [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> + { ConstrEval (rtc,c) } + | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" -> + { ConstrContext (id,c) } + | IDENT "type"; IDENT "of"; c = Constr.constr -> + { ConstrTypeOf c } ] ] + ; + constr_may_eval: (* For extensions *) + [ [ c = constr_eval -> { c } + | c = Constr.constr -> { ConstrTerm c } ] ] + ; + tactic_atom: + [ [ n = integer -> { TacGeneric (genarg_of_int n) } + | r = reference -> { TacCall (Loc.tag ~loc (r,[])) } + | "()" -> { TacGeneric (genarg_of_unit ()) } ] ] + ; + match_key: + [ [ "match" -> { Once } + | "lazymatch" -> { Select } + | "multimatch" -> { General } ] ] + ; + input_fun: + [ [ "_" -> { Name.Anonymous } + | l = ident -> { Name.Name l } ] ] + ; + let_clause: + [ [ idr = identref; ":="; te = tactic_expr -> + { (CAst.map (fun id -> Name id) idr, arg_of_expr te) } + | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = tactic_expr -> + { (na, arg_of_expr te) } + | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + { (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) } ] ] + ; + match_pattern: + [ [ IDENT "context"; oid = OPT Constr.ident; + "["; pc = Constr.lconstr_pattern; "]" -> + { Subterm (oid, pc) } + | pc = Constr.lconstr_pattern -> { Term pc } ] ] + ; + match_hyps: + [ [ na = name; ":"; mp = match_pattern -> { Hyp (na, mp) } + | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> { Def (na, mpv, mpt) } + | na = name; ":="; mpv = match_pattern -> + { let t, ty = + match mpv with + | Term t -> (match t with + | { CAst.v = CCast (t, (CastConv ty | CastVM ty | CastNative ty)) } -> Term t, Some (Term ty) + | _ -> mpv, None) + | _ -> mpv, None + in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty) } + ] ] + ; + match_context_rule: + [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; + "=>"; te = tactic_expr -> { Pat (largs, mp, te) } + | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; + "]"; "=>"; te = tactic_expr -> { Pat (largs, mp, te) } + | "_"; "=>"; te = tactic_expr -> { All te } ] ] + ; + match_context_list: + [ [ mrl = LIST1 match_context_rule SEP "|" -> { mrl } + | "|"; mrl = LIST1 match_context_rule SEP "|" -> { mrl } ] ] + ; + match_rule: + [ [ mp = match_pattern; "=>"; te = tactic_expr -> { Pat ([],mp,te) } + | "_"; "=>"; te = tactic_expr -> { All te } ] ] + ; + match_list: + [ [ mrl = LIST1 match_rule SEP "|" -> { mrl } + | "|"; mrl = LIST1 match_rule SEP "|" -> { mrl } ] ] + ; + message_token: + [ [ id = identref -> { MsgIdent id } + | s = STRING -> { MsgString s } + | n = integer -> { MsgInt n } ] ] + ; + + ltac_def_kind: + [ [ ":=" -> { false } + | "::=" -> { true } ] ] + ; + + (* Definitions for tactics *) + tacdef_body: + [ [ name = Constr.global; it=LIST1 input_fun; + redef = ltac_def_kind; body = tactic_expr -> + { if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) + else + let id = reference_to_id name in + Tacexpr.TacticDefinition (id, TacFun (it, body)) } + | name = Constr.global; redef = ltac_def_kind; + body = tactic_expr -> + { if redef then Tacexpr.TacticRedefinition (name, body) + else + let id = reference_to_id name in + Tacexpr.TacticDefinition (id, body) } + ] ] + ; + tactic: + [ [ tac = tactic_expr -> { tac } ] ] + ; + + range_selector: + [ [ n = natural ; "-" ; m = natural -> { (n, m) } + | n = natural -> { (n, n) } ] ] + ; + (* We unfold a range selectors list once so that we can make a special case + * for a unique SelectNth selector. *) + range_selector_or_nth: + [ [ n = natural ; "-" ; m = natural; + l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] -> + { Goal_select.SelectList ((n, m) :: Option.default [] l) } + | n = natural; + l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] -> + { let open Goal_select in + Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ] + ; + selector_body: + [ [ l = range_selector_or_nth -> { l } + | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ] + ; + selector: + [ [ IDENT "only"; sel = selector_body; ":" -> { sel } ] ] + ; + toplevel_selector: + [ [ sel = selector_body; ":" -> { sel } + | "!"; ":" -> { Goal_select.SelectAlreadyFocused } + | IDENT "all"; ":" -> { Goal_select.SelectAll } ] ] + ; + tactic_mode: + [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> { tac g } + | g = OPT toplevel_selector; "{" -> { Vernacexpr.VernacSubproof g } ] ] + ; + command: + [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; + l = OPT [ "using"; l = G_vernac.section_subset_expr -> { l } ] -> + { Vernacexpr.VernacProof (Some (in_tac ta), l) } + | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; + ta = OPT [ "with"; ta = Pltac.tactic -> { in_tac ta } ] -> + { Vernacexpr.VernacProof (ta,Some l) } ] ] + ; + hint: + [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; + tac = Pltac.tactic -> + { Hints.HintsExtern (n,c, in_tac tac) } ] ] + ; + operconstr: LEVEL "0" + [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> + { let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in + CAst.make ~loc @@ CHole (None, IntroAnonymous, Some arg) } ] ] + ; + END + +{ + +open Stdarg +open Tacarg +open Vernacexpr +open Vernac_classifier +open Goptions +open Libnames + +let print_info_trace = ref None + +let _ = declare_int_option { + optdepr = false; + optname = "print info trace"; + optkey = ["Info" ; "Level"]; + optread = (fun () -> !print_info_trace); + optwrite = fun n -> print_info_trace := n; +} + +let vernac_solve n info tcom b = + let open Goal_select in + let status = Proof_global.with_current_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 + let (p,status) = + Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p + in + (* in case a strict subtree was completed, + go back to the top of the prooftree *) + let p = Proof.maximal_unfocus Vernacentries.command_focus p in + p,status) in + if not status then Feedback.feedback Feedback.AddedAxiom + +let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s + +} + +VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY { pr_ltac_selector } +| [ toplevel_selector(s) ] -> { s } +END + +{ + +let pr_ltac_info n = str "Info" ++ spc () ++ int n + +} + +VERNAC ARGUMENT EXTEND ltac_info PRINTED BY { pr_ltac_info } +| [ "Info" natural(n) ] -> { n } +END + +{ + +let pr_ltac_use_default b = + if b then (* Bug: a space is inserted before "..." *) str ".." else mt () + +} + +VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY { pr_ltac_use_default } +| [ "." ] -> { false } +| [ "..." ] -> { true } +END + +{ + +let is_anonymous_abstract = function + | TacAbstract (_,None) -> true + | TacSolve [TacAbstract (_,None)] -> true + | _ -> false +let rm_abstract = function + | TacAbstract (t,_) -> t + | TacSolve [TacAbstract (t,_)] -> TacSolve [t] + | x -> x +let is_explicit_terminator = function TacSolve _ -> true | _ -> false + +} + +VERNAC { tactic_mode } EXTEND VernacSolve +| [ 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 + vernac_solve g n t 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 + let parallel = `Yes (solving_tac,anon_abstracting_tac) in + let pbr = if solving_tac then Some "par" else None in + VtProofStep{ parallel = parallel; proof_block_detection = pbr }, + VtLater + } -> { + let t = rm_abstract t in + vernac_solve Goal_select.SelectAll n t def + } +END + +{ + +let pr_ltac_tactic_level n = str "(at level " ++ int n ++ str ")" + +} + +VERNAC ARGUMENT EXTEND ltac_tactic_level PRINTED BY { pr_ltac_tactic_level } +| [ "(" "at" "level" natural(n) ")" ] -> { n } +END + +VERNAC ARGUMENT EXTEND ltac_production_sep +| [ "," string(sep) ] -> { sep } +END + +{ + +let pr_ltac_production_item = function +| Tacentries.TacTerm s -> quote (str s) +| Tacentries.TacNonTerm (_, ((arg, None), None)) -> str arg +| Tacentries.TacNonTerm (_, ((arg, Some _), None)) -> assert false +| Tacentries.TacNonTerm (_, ((arg, sep), Some id)) -> + let sep = match sep with + | None -> mt () + | Some sep -> str "," ++ spc () ++ quote (str sep) + in + str arg ++ str "(" ++ Id.print id ++ sep ++ str ")" + +} + +VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY { pr_ltac_production_item } +| [ string(s) ] -> { Tacentries.TacTerm s } +| [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] -> + { Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, sep), Some p)) } +| [ ident(nt) ] -> + { Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) } +END + +VERNAC COMMAND EXTEND VernacTacticNotation +| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => + { VtSideff [], VtNow } -> + { let open Vernacinterp in + let n = Option.default 0 n in + let deprecation = atts.deprecated in + Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e; + } +END + +VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY +| [ "Print" "Ltac" reference(r) ] -> + { Feedback.msg_notice (Tacintern.print_ltac r) } +END + +VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY +| [ "Locate" "Ltac" reference(r) ] -> + { Tacentries.print_located_tactic r } +END + +{ + +let pr_ltac_ref = Libnames.pr_qualid + +let pr_tacdef_body tacdef_body = + let id, redef, body = + match tacdef_body with + | TacticDefinition ({CAst.v=id}, body) -> Id.print id, false, body + | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body + in + let idl, body = + match body with + | Tacexpr.TacFun (idl,b) -> idl,b + | _ -> [], body in + id ++ + prlist (function Name.Anonymous -> str " _" + | Name.Name id -> spc () ++ Id.print id) idl + ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) + ++ Pptactic.pr_raw_tactic body + +} + +VERNAC ARGUMENT EXTEND ltac_tacdef_body +PRINTED BY { pr_tacdef_body } +| [ tacdef_body(t) ] -> { t } +END + +VERNAC COMMAND EXTEND VernacDeclareTacticDefinition +| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { + VtSideff (List.map (function + | TacticDefinition ({CAst.v=r},_) -> r + | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater + } -> { let open Vernacinterp in + let deprecation = atts.deprecated in + Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l; + } +END + +VERNAC COMMAND EXTEND VernacPrintLtacs CLASSIFIED AS QUERY +| [ "Print" "Ltac" "Signatures" ] -> { Tacentries.print_ltacs () } +END diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 deleted file mode 100644 index 1f56244c75..0000000000 --- a/plugins/ltac/g_obligations.ml4 +++ /dev/null @@ -1,161 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* - snd (get_default_tactic ()) - end in - Obligations.default_tactic := tac - -let with_tac f tac = - let env = Genintern.empty_glob_sign (Global.env ()) in - let tac = match tac with - | None -> None - | Some tac -> - let tac = Genarg.in_gen (Genarg.rawwit wit_ltac) tac in - let _, tac = Genintern.generic_intern env tac in - Some tac - in - f tac - -(* We define new entries for programs, with the use of this module - * Subtac. These entries are named Subtac. - *) - -module Gram = Pcoq.Gram -module Tactic = Pltac - -open Pcoq - -let sigref loc = mkRefC (Libnames.qualid_of_string ~loc "Coq.Init.Specif.sig") - -type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type - -let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = - Genarg.create_arg "withtac" - -let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac) - -GEXTEND Gram - GLOBAL: withtac; - - withtac: - [ [ "with"; t = Tactic.tactic -> Some t - | -> None ] ] - ; - - Constr.closed_binder: - [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> - let typ = mkAppC (sigref !@loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in - [CLocalAssum ([id], default_binder_kind, typ)] - ] ]; - - END - -open Obligations - -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 _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) - -VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl -| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> - [ obligation (num, Some name, Some t) tac ] -| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> - [ obligation (num, Some name, None) tac ] -| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> - [ obligation (num, None, Some t) tac ] -| [ "Obligation" integer(num) withtac(tac) ] -> - [ obligation (num, None, None) tac ] -| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> - [ next_obligation (Some name) tac ] -| [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ] -END - -VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF -| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> - [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> - [ try_solve_obligation num None (Some (Tacinterp.interp t)) ] -END - -VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF -| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> - [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" "with" tactic(t) ] -> - [ try_solve_obligations None (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" ] -> - [ try_solve_obligations None None ] -END - -VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF -| [ "Solve" "All" "Obligations" "with" tactic(t) ] -> - [ solve_all_obligations (Some (Tacinterp.interp t)) ] -| [ "Solve" "All" "Obligations" ] -> - [ solve_all_obligations None ] -END - -VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF -| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ] -| [ "Admit" "Obligations" ] -> [ admit_obligations None ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND Set_Solver CLASSIFIED AS SIDEFF -| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - fun ~atts ~st -> begin - let open Vernacinterp in - set_default_tactic - (Locality.make_section_locality atts.locality) - (Tacintern.glob_tactic t); - st - end] -END - -open Pp - -VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY -| [ "Show" "Obligation" "Tactic" ] -> [ - Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ] -END - -VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY -| [ "Obligations" "of" ident(name) ] -> [ show_obligations (Some name) ] -| [ "Obligations" ] -> [ show_obligations None ] -END - -VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY -| [ "Preterm" "of" ident(name) ] -> [ Feedback.msg_info (show_term (Some name)) ] -| [ "Preterm" ] -> [ Feedback.msg_info (show_term None) ] -END - -open Pp - -(* Declare a printer for the content of Program tactics *) -let () = - let printer _ _ _ = function - | None -> mt () - | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac - in - Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg new file mode 100644 index 0000000000..26f2b08d3a --- /dev/null +++ b/plugins/ltac/g_obligations.mlg @@ -0,0 +1,173 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + snd (get_default_tactic ()) + end in + Obligations.default_tactic := tac + +let with_tac f tac = + let env = Genintern.empty_glob_sign (Global.env ()) in + let tac = match tac with + | None -> None + | Some tac -> + let tac = Genarg.in_gen (Genarg.rawwit wit_ltac) tac in + let _, tac = Genintern.generic_intern env tac in + Some tac + in + f tac + +(* We define new entries for programs, with the use of this module + * Subtac. These entries are named Subtac. + *) + +module Gram = Pcoq.Gram +module Tactic = Pltac + +open Pcoq + +let sigref loc = mkRefC (Libnames.qualid_of_string ~loc "Coq.Init.Specif.sig") + +type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type + +let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = + Genarg.create_arg "withtac" + +let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac) + +} + +GRAMMAR EXTEND Gram + GLOBAL: withtac; + + withtac: + [ [ "with"; t = Tactic.tactic -> { Some t } + | -> { None } ] ] + ; + + Constr.closed_binder: + [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> { + let typ = mkAppC (sigref loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in + [CLocalAssum ([id], default_binder_kind, typ)] } + ] ]; + + END + +{ + +open Obligations + +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 _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) + +} + +VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } +| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> + { obligation (num, Some name, Some t) tac } +| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> + { obligation (num, Some name, None) tac } +| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> + { obligation (num, None, Some t) tac } +| [ "Obligation" integer(num) withtac(tac) ] -> + { obligation (num, None, None) tac } +| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> + { next_obligation (Some name) tac } +| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } +END + +VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF +| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> + { try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) } +| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> + { try_solve_obligation num None (Some (Tacinterp.interp t)) } +END + +VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF +| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> + { try_solve_obligations (Some name) (Some (Tacinterp.interp t)) } +| [ "Solve" "Obligations" "with" tactic(t) ] -> + { try_solve_obligations None (Some (Tacinterp.interp t)) } +| [ "Solve" "Obligations" ] -> + { try_solve_obligations None None } +END + +VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF +| [ "Solve" "All" "Obligations" "with" tactic(t) ] -> + { solve_all_obligations (Some (Tacinterp.interp t)) } +| [ "Solve" "All" "Obligations" ] -> + { solve_all_obligations None } +END + +VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF +| [ "Admit" "Obligations" "of" ident(name) ] -> { admit_obligations (Some name) } +| [ "Admit" "Obligations" ] -> { admit_obligations None } +END + +VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF +| [ "Obligation" "Tactic" ":=" tactic(t) ] -> { + let open Vernacinterp in + set_default_tactic + (Locality.make_section_locality atts.locality) + (Tacintern.glob_tactic t); + } +END + +{ + +open Pp + +} + +VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY +| [ "Show" "Obligation" "Tactic" ] -> { + Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) } +END + +VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY +| [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) } +| [ "Obligations" ] -> { show_obligations None } +END + +VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY +| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_info (show_term (Some name)) } +| [ "Preterm" ] -> { Feedback.msg_info (show_term None) } +END + +{ + +(* Declare a printer for the content of Program tactics *) +let () = + let printer _ _ _ = function + | None -> mt () + | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac + in + Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer + +} diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 deleted file mode 100644 index f1634f1561..0000000000 --- a/plugins/ltac/g_rewrite.ml4 +++ /dev/null @@ -1,297 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ bl ] -END - -type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast -type glob_strategy = (Tacexpr.glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast - -let interp_strategy ist gl s = - let sigma = project gl in - sigma, strategy_of_ast s -let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c) s -let subst_strategy s str = str - -let pr_strategy _ _ _ (s : strategy) = Pp.str "" -let pr_raw_strategy prc prlc _ (s : raw_strategy) = - let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in - Rewrite.pr_strategy prc prr s -let pr_glob_strategy prc prlc _ (s : glob_strategy) = - let prr = Pptactic.pr_red_expr - (Ppconstr.pr_constr_expr, - Ppconstr.pr_lconstr_expr, - Pputils.pr_or_by_notation Libnames.pr_qualid, - Ppconstr.pr_constr_expr) - in - Rewrite.pr_strategy prc prr s - -ARGUMENT EXTEND rewstrategy - PRINTED BY pr_strategy - - INTERPRETED BY interp_strategy - GLOBALIZED BY glob_strategy - SUBSTITUTED BY subst_strategy - - RAW_PRINTED BY pr_raw_strategy - GLOB_PRINTED BY pr_glob_strategy - - [ glob(c) ] -> [ StratConstr (c, true) ] - | [ "<-" constr(c) ] -> [ StratConstr (c, false) ] - | [ "subterms" rewstrategy(h) ] -> [ StratUnary (Subterms, h) ] - | [ "subterm" rewstrategy(h) ] -> [ StratUnary (Subterm, h) ] - | [ "innermost" rewstrategy(h) ] -> [ StratUnary(Innermost, h) ] - | [ "outermost" rewstrategy(h) ] -> [ StratUnary(Outermost, h) ] - | [ "bottomup" rewstrategy(h) ] -> [ StratUnary(Bottomup, h) ] - | [ "topdown" rewstrategy(h) ] -> [ StratUnary(Topdown, h) ] - | [ "id" ] -> [ StratId ] - | [ "fail" ] -> [ StratFail ] - | [ "refl" ] -> [ StratRefl ] - | [ "progress" rewstrategy(h) ] -> [ StratUnary (Progress, h) ] - | [ "try" rewstrategy(h) ] -> [ StratUnary (Try, h) ] - | [ "any" rewstrategy(h) ] -> [ StratUnary (Any, h) ] - | [ "repeat" rewstrategy(h) ] -> [ StratUnary (Repeat, h) ] - | [ rewstrategy(h) ";" rewstrategy(h') ] -> [ StratBinary (Compose, h, h') ] - | [ "(" rewstrategy(h) ")" ] -> [ h ] - | [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ StratBinary (Choice, h, h') ] - | [ "old_hints" preident(h) ] -> [ StratHints (true, h) ] - | [ "hints" preident(h) ] -> [ StratHints (false, h) ] - | [ "terms" constr_list(h) ] -> [ StratTerms h ] - | [ "eval" red_expr(r) ] -> [ StratEval r ] - | [ "fold" constr(c) ] -> [ StratFold c ] -END - -(* By default the strategy for "rewrite_db" is top-down *) - -let db_strat db = StratUnary (Topdown, StratHints (false, db)) -let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db)) - -TACTIC EXTEND rewrite_strat -| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ cl_rewrite_clause_strat s (Some id) ] -| [ "rewrite_strat" rewstrategy(s) ] -> [ cl_rewrite_clause_strat s None ] -| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ cl_rewrite_clause_db db (Some id) ] -| [ "rewrite_db" preident(db) ] -> [ cl_rewrite_clause_db db None ] -END - -let clsubstitute o c = - Proofview.Goal.enter begin fun gl -> - let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in - let hyps = Tacmach.New.pf_ids_of_hyps gl in - Tacticals.New.tclMAP - (fun cl -> - match cl with - | Some id when is_tac id -> Tacticals.New.tclIDTAC - | _ -> cl_rewrite_clause c o AllOccurrences cl) - (None :: List.map (fun id -> Some id) hyps) - end - -TACTIC EXTEND substitute -| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ] -END - - -(* Compatibility with old Setoids *) - -TACTIC EXTEND setoid_rewrite - [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ] - -> [ cl_rewrite_clause c o AllOccurrences None ] - | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] -> - [ cl_rewrite_clause c o AllOccurrences (Some id) ] - | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] -> - [ cl_rewrite_clause c o (occurrences_of occ) None ] - | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] -> - [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ] - | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ)] -> - [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ] -END - -VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF - | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) - "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - [ declare_relation a aeq n (Some lemma1) (Some lemma2) None ] - - | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) - "as" ident(n) ] -> - [ declare_relation a aeq n (Some lemma1) None None ] - | [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> - [ declare_relation a aeq n None None None ] -END - -VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF - [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) - "as" ident(n) ] -> - [ declare_relation a aeq n None (Some lemma2) None ] - | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation a aeq n None (Some lemma2) (Some lemma3) ] -END - -VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF - [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) - "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation a aeq n (Some lemma1) None (Some lemma3) ] - | [ "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 a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ] - | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) - "as" ident(n) ] -> - [ declare_relation a aeq n None None (Some lemma3) ] -END - -type binders_argtype = local_binder_expr list - -let wit_binders = - (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type) - -let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders) - -let () = - let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in - Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer - -open Pcoq - -GEXTEND Gram - GLOBAL: binders; - binders: - [ [ b = Pcoq.Constr.binders -> b ] ]; -END - -VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) - "reflexivity" "proved" "by" constr(lemma1) - "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None ] - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) - "reflexivity" "proved" "by" constr(lemma1) - "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n (Some lemma1) None None ] - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n None None None ] -END - -VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF - [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) - "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n None (Some lemma2) None ] - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) ] -END - -VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF - [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) - "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) ] - | [ "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 ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ] - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) - "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n None None (Some lemma3) ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND AddSetoid1 CLASSIFIED AS SIDEFF - [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ fun ~atts ~st -> let open Vernacinterp in - add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n; - st - ] - | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ fun ~atts ~st -> let open Vernacinterp in - add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n; - st - ] - | [ "Add" "Morphism" constr(m) ":" ident(n) ] - (* This command may or may not open a goal *) - => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ] - -> [ fun ~atts ~st -> let open Vernacinterp in - add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n; - st - ] - | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] - -> [ fun ~atts ~st -> let open Vernacinterp in - add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n; - st - ] - | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) - "with" "signature" lconstr(s) "as" ident(n) ] - => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] - -> [ fun ~atts ~st -> let open Vernacinterp in - add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n; - st - ] -END - -TACTIC EXTEND setoid_symmetry - [ "setoid_symmetry" ] -> [ setoid_symmetry ] - | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ] -END - -TACTIC EXTEND setoid_reflexivity -[ "setoid_reflexivity" ] -> [ setoid_reflexivity ] -END - -TACTIC EXTEND setoid_transitivity - [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ] -| [ "setoid_etransitivity" ] -> [ setoid_transitivity None ] -END - -VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY - [ "Print" "Rewrite" "HintDb" preident(s) ] -> - [ let sigma, env = Pfedit.get_current_context () in - Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) ] -END diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg new file mode 100644 index 0000000000..3e47724c4c --- /dev/null +++ b/plugins/ltac/g_rewrite.mlg @@ -0,0 +1,318 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { bl } +END + +{ + +type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast +type glob_strategy = (Tacexpr.glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast + +let interp_strategy ist gl s = + let sigma = project gl in + sigma, strategy_of_ast s +let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c) s +let subst_strategy s str = str + +let pr_strategy _ _ _ (s : strategy) = Pp.str "" +let pr_raw_strategy prc prlc _ (s : raw_strategy) = + let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in + Rewrite.pr_strategy prc prr s +let pr_glob_strategy prc prlc _ (s : glob_strategy) = + let prr = Pptactic.pr_red_expr + (Ppconstr.pr_constr_expr, + Ppconstr.pr_lconstr_expr, + Pputils.pr_or_by_notation Libnames.pr_qualid, + Ppconstr.pr_constr_expr) + in + Rewrite.pr_strategy prc prr s + +} + +ARGUMENT EXTEND rewstrategy + PRINTED BY { pr_strategy } + + INTERPRETED BY { interp_strategy } + GLOBALIZED BY { glob_strategy } + SUBSTITUTED BY { subst_strategy } + + RAW_PRINTED BY { pr_raw_strategy } + GLOB_PRINTED BY { pr_glob_strategy } + + | [ glob(c) ] -> { StratConstr (c, true) } + | [ "<-" constr(c) ] -> { StratConstr (c, false) } + | [ "subterms" rewstrategy(h) ] -> { StratUnary (Subterms, h) } + | [ "subterm" rewstrategy(h) ] -> { StratUnary (Subterm, h) } + | [ "innermost" rewstrategy(h) ] -> { StratUnary(Innermost, h) } + | [ "outermost" rewstrategy(h) ] -> { StratUnary(Outermost, h) } + | [ "bottomup" rewstrategy(h) ] -> { StratUnary(Bottomup, h) } + | [ "topdown" rewstrategy(h) ] -> { StratUnary(Topdown, h) } + | [ "id" ] -> { StratId } + | [ "fail" ] -> { StratFail } + | [ "refl" ] -> { StratRefl } + | [ "progress" rewstrategy(h) ] -> { StratUnary (Progress, h) } + | [ "try" rewstrategy(h) ] -> { StratUnary (Try, h) } + | [ "any" rewstrategy(h) ] -> { StratUnary (Any, h) } + | [ "repeat" rewstrategy(h) ] -> { StratUnary (Repeat, h) } + | [ rewstrategy(h) ";" rewstrategy(h') ] -> { StratBinary (Compose, h, h') } + | [ "(" rewstrategy(h) ")" ] -> { h } + | [ "choice" rewstrategy(h) rewstrategy(h') ] -> { StratBinary (Choice, h, h') } + | [ "old_hints" preident(h) ] -> { StratHints (true, h) } + | [ "hints" preident(h) ] -> { StratHints (false, h) } + | [ "terms" constr_list(h) ] -> { StratTerms h } + | [ "eval" red_expr(r) ] -> { StratEval r } + | [ "fold" constr(c) ] -> { StratFold c } +END + +(* By default the strategy for "rewrite_db" is top-down *) + +{ + +let db_strat db = StratUnary (Topdown, StratHints (false, db)) +let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db)) + +} + +TACTIC EXTEND rewrite_strat +| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> { cl_rewrite_clause_strat s (Some id) } +| [ "rewrite_strat" rewstrategy(s) ] -> { cl_rewrite_clause_strat s None } +| [ "rewrite_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db db (Some id) } +| [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db db None } +END + +{ + +let clsubstitute o c = + Proofview.Goal.enter begin fun gl -> + let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in + let hyps = Tacmach.New.pf_ids_of_hyps gl in + Tacticals.New.tclMAP + (fun cl -> + match cl with + | Some id when is_tac id -> Tacticals.New.tclIDTAC + | _ -> cl_rewrite_clause c o AllOccurrences cl) + (None :: List.map (fun id -> Some id) hyps) + end + +} + +TACTIC EXTEND substitute +| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> { clsubstitute o c } +END + + +(* Compatibility with old Setoids *) + +TACTIC EXTEND setoid_rewrite + | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ] + -> { cl_rewrite_clause c o AllOccurrences None } + | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] -> + { cl_rewrite_clause c o AllOccurrences (Some id) } + | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] -> + { cl_rewrite_clause c o (occurrences_of occ) None } + | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] -> + { cl_rewrite_clause c o (occurrences_of occ) (Some id) } + | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ)] -> + { cl_rewrite_clause c o (occurrences_of occ) (Some id) } +END + +VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF + | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> + { declare_relation a aeq n (Some lemma1) (Some lemma2) None } + + | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "as" ident(n) ] -> + { declare_relation a aeq n (Some lemma1) None None } + | [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> + { declare_relation a aeq n None None None } +END + +VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF + | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + "as" ident(n) ] -> + { declare_relation a aeq n None (Some lemma2) None } + | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + { declare_relation a aeq n None (Some lemma2) (Some lemma3) } +END + +VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF + | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + { declare_relation a aeq n (Some lemma1) None (Some lemma3) } + | [ "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 a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } + | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + "as" ident(n) ] -> + { declare_relation a aeq n None None (Some lemma3) } +END + +{ + +type binders_argtype = local_binder_expr list + +let wit_binders = + (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type) + +let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders) + +let () = + let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in + Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer + +open Pcoq + +} + +GRAMMAR EXTEND Gram + GLOBAL: binders; + binders: + [ [ b = Pcoq.Constr.binders -> { b } ] ]; +END + +VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + "reflexivity" "proved" "by" constr(lemma1) + "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None } + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + "reflexivity" "proved" "by" constr(lemma1) + "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n (Some lemma1) None None } + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n None None None } +END + +VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n None (Some lemma2) None } + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) } +END + +VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) } + | [ "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 ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n None None (Some lemma3) } +END + +VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF + | [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + { let open Vernacinterp in + add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n; + } + | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + { let open Vernacinterp in + add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n; + } + | [ "Add" "Morphism" constr(m) ":" ident(n) ] + (* This command may or may not open a goal *) + => { Vernacexpr.VtUnknown, Vernacexpr.VtNow } + -> { let open Vernacinterp in + add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n; + } + | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] + => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) } + -> { let open Vernacinterp in + add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n; + } + | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) + "with" "signature" lconstr(s) "as" ident(n) ] + => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) } + -> { let open Vernacinterp in + add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n; + } +END + +TACTIC EXTEND setoid_symmetry + | [ "setoid_symmetry" ] -> { setoid_symmetry } + | [ "setoid_symmetry" "in" hyp(n) ] -> { setoid_symmetry_in n } +END + +TACTIC EXTEND setoid_reflexivity +| [ "setoid_reflexivity" ] -> { setoid_reflexivity } +END + +TACTIC EXTEND setoid_transitivity +| [ "setoid_transitivity" constr(t) ] -> { setoid_transitivity (Some t) } +| [ "setoid_etransitivity" ] -> { setoid_transitivity None } +END + +VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY +| [ "Print" "Rewrite" "HintDb" preident(s) ] -> + { let sigma, env = Pfedit.get_current_context () in + Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) } +END diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 deleted file mode 100644 index 983e1578be..0000000000 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ /dev/null @@ -1,74 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* set_profiling b)) - -let tclRESET_PROFILE = - Proofview.tclLIFT (Proofview.NonLogical.make reset_profile) - -let tclSHOW_PROFILE ~cutoff = - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results ~cutoff)) - -let tclSHOW_PROFILE_TACTIC s = - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results_tactic s)) - -let tclRESTART_TIMER s = - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> restart_timer s)) - -let tclFINISH_TIMING ?(prefix="Timer") (s : string option) = - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> finish_timing ~prefix s)) - -TACTIC EXTEND start_ltac_profiling -| [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] -END - -TACTIC EXTEND stop_ltac_profiling -| [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] -END - -TACTIC EXTEND reset_ltac_profile -| [ "reset" "ltac" "profile" ] -> [ tclRESET_PROFILE ] -END - -TACTIC EXTEND show_ltac_profile -| [ "show" "ltac" "profile" ] -> [ tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff ] -| [ "show" "ltac" "profile" "cutoff" int(n) ] -> [ tclSHOW_PROFILE ~cutoff:(float_of_int n) ] -| [ "show" "ltac" "profile" string(s) ] -> [ tclSHOW_PROFILE_TACTIC s ] -END - -TACTIC EXTEND restart_timer -| [ "restart_timer" string_opt(s) ] -> [ tclRESTART_TIMER s ] -END - -TACTIC EXTEND finish_timing -| [ "finish_timing" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix:"Timer" s ] -| [ "finish_timing" "(" string(prefix) ")" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix s ] -END - -VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF - [ "Reset" "Ltac" "Profile" ] -> [ reset_profile () ] -END - -VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY -| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:!Flags.profile_ltac_cutoff ] -| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ] -END - -VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY - [ "Show" "Ltac" "Profile" string(s) ] -> [ print_results_tactic s ] -END diff --git a/plugins/ltac/profile_ltac_tactics.mlg b/plugins/ltac/profile_ltac_tactics.mlg new file mode 100644 index 0000000000..2713819c7b --- /dev/null +++ b/plugins/ltac/profile_ltac_tactics.mlg @@ -0,0 +1,82 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* set_profiling b)) + +let tclRESET_PROFILE = + Proofview.tclLIFT (Proofview.NonLogical.make reset_profile) + +let tclSHOW_PROFILE ~cutoff = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results ~cutoff)) + +let tclSHOW_PROFILE_TACTIC s = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results_tactic s)) + +let tclRESTART_TIMER s = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> restart_timer s)) + +let tclFINISH_TIMING ?(prefix="Timer") (s : string option) = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> finish_timing ~prefix s)) + +} + +TACTIC EXTEND start_ltac_profiling +| [ "start" "ltac" "profiling" ] -> { tclSET_PROFILING true } +END + +TACTIC EXTEND stop_ltac_profiling +| [ "stop" "ltac" "profiling" ] -> { tclSET_PROFILING false } +END + +TACTIC EXTEND reset_ltac_profile +| [ "reset" "ltac" "profile" ] -> { tclRESET_PROFILE } +END + +TACTIC EXTEND show_ltac_profile +| [ "show" "ltac" "profile" ] -> { tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff } +| [ "show" "ltac" "profile" "cutoff" int(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) } +| [ "show" "ltac" "profile" string(s) ] -> { tclSHOW_PROFILE_TACTIC s } +END + +TACTIC EXTEND restart_timer +| [ "restart_timer" string_opt(s) ] -> { tclRESTART_TIMER s } +END + +TACTIC EXTEND finish_timing +| [ "finish_timing" string_opt(s) ] -> { tclFINISH_TIMING ~prefix:"Timer" s } +| [ "finish_timing" "(" string(prefix) ")" string_opt(s) ] -> { tclFINISH_TIMING ~prefix s } +END + +VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF +| [ "Reset" "Ltac" "Profile" ] -> { reset_profile () } +END + +VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY +| [ "Show" "Ltac" "Profile" ] -> { print_results ~cutoff:!Flags.profile_ltac_cutoff } +| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> { print_results ~cutoff:(float_of_int n) } +END + +VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY +| [ "Show" "Ltac" "Profile" string(s) ] -> { print_results_tactic s } +END -- cgit v1.2.3