From daa7cb065a238c7d4ee394e00315d66d023e5259 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Dec 2015 17:55:25 +0100 Subject: Removing auto from the tactic AST. --- tactics/coretactics.ml4 | 2 -- tactics/eauto.ml4 | 33 ++------------------ tactics/eauto.mli | 6 ---- tactics/g_auto.ml4 | 76 +++++++++++++++++++++++++++++++++++++++++++++++ tactics/hightactics.mllib | 1 + tactics/tacintern.ml | 6 ---- tactics/tacinterp.ml | 36 ---------------------- tactics/tacsubst.ml | 4 --- 8 files changed, 80 insertions(+), 84 deletions(-) create mode 100644 tactics/g_auto.ml4 (limited to 'tactics') diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 1b1fb845e0..6a620deebe 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -221,8 +221,6 @@ let initial_atomic () = "intro", TacIntroMove(None,MoveLast); "intros", TacIntroPattern []; "cofix", TacCofix None; - "trivial", TacTrivial (Off,[],None); - "auto", TacAuto(Off,None,[],None); ] in let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index ffde67e4fb..1943a4f1f2 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -438,37 +438,10 @@ let make_dimension n = function | Some d -> (false,d) open Genarg +open G_auto -(* Hint bases *) - -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 pr_constr_coma_sequence prc _ _ = - prlist_with_sep pr_comma (fun (_,c) -> prc c) - -ARGUMENT EXTEND constr_coma_sequence - TYPED AS open_constr_list - PRINTED BY pr_constr_coma_sequence -| [ open_constr(c) "," constr_coma_sequence(l) ] -> [ c::l ] -| [ open_constr(c) ] -> [ [c] ] -END - -let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using (fun (_,c) -> prc c) - -ARGUMENT EXTEND auto_using - TYPED AS open_constr_list - PRINTED BY pr_auto_using -| [ "using" constr_coma_sequence(l) ] -> [ l ] -| [ ] -> [ [] ] -END +let hintbases = G_auto.hintbases +let wit_hintbases = G_auto.wit_hintbases TACTIC EXTEND eauto | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) diff --git a/tactics/eauto.mli b/tactics/eauto.mli index b55c70fa12..3d02081bfe 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -15,12 +15,6 @@ val hintbases : hint_db_name list option Pcoq.Gram.entry val wit_hintbases : hint_db_name list option Genarg.uniform_genarg_type -val wit_auto_using : - (Tacexpr.open_constr_expr list, - Tacexpr.open_glob_constr list, Evd.open_constr list) - Genarg.genarg_type - - val e_assumption : unit Proofview.tactic val registered_e_assumption : unit Proofview.tactic diff --git a/tactics/g_auto.ml4 b/tactics/g_auto.ml4 new file mode 100644 index 0000000000..7d35cfaab1 --- /dev/null +++ b/tactics/g_auto.ml4 @@ -0,0 +1,76 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [ None ] +| [ "with" ne_preident_list(l) ] -> [ Some l ] +| [ ] -> [ Some [] ] +END + +let pr_constr_coma_sequence prc _ _ = + prlist_with_sep pr_comma (fun (_,c) -> prc c) + +ARGUMENT EXTEND constr_coma_sequence + TYPED AS open_constr_list + PRINTED BY pr_constr_coma_sequence +| [ open_constr(c) "," constr_coma_sequence(l) ] -> [ c::l ] +| [ open_constr(c) ] -> [ [c] ] +END + +let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using (fun (_,c) -> prc c) + +ARGUMENT EXTEND auto_using + TYPED AS open_constr_list + PRINTED BY pr_auto_using +| [ "using" constr_coma_sequence(l) ] -> [ l ] +| [ ] -> [ [] ] +END + +TACTIC EXTEND trivial +| [ "trivial" auto_using(lems) hintbases(db) ] -> + [ Auto.h_trivial lems db ] +END + +TACTIC EXTEND info_trivial +| [ "info_trivial" auto_using(lems) hintbases(db) ] -> + [ Auto.h_trivial ~debug:Info lems db ] +END + +TACTIC EXTEND debug_trivial +| [ "debug" "trivial" auto_using(lems) hintbases(db) ] -> + [ Auto.h_trivial ~debug:Debug lems db ] +END + +TACTIC EXTEND auto +| [ "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> + [ Auto.h_auto n 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 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 lems db ] +END diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib index ff2e1ff6aa..30e97f62d5 100644 --- a/tactics/hightactics.mllib +++ b/tactics/hightactics.mllib @@ -1,6 +1,7 @@ Extraargs Coretactics Extratactics +G_auto Eauto Class_tactics G_class diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 5e725e182d..ecce4a0ff3 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -517,12 +517,6 @@ let rec intern_atomic lf ist x = (clause_app (intern_hyp_location ist) cls),b, (Option.map (intern_intro_pattern_naming_loc lf ist) eqpat)) - (* Automation tactics *) - | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (intern_constr ist) lems,l) - | TacAuto (d,n,lems,l) -> - TacAuto (d,Option.map (intern_int_or_var ist) n, - List.map (intern_constr ist) lems,l) - (* Derived basic tactics *) | TacInductionDestruct (ev,isrec,(l,el)) -> TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats),cls) -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 570ab245b7..8c8861fd99 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1958,42 +1958,6 @@ and interp_atomic ist tac : unit Proofview.tactic = ((sigma,sigma'),c) clp eqpat) sigma') end } - (* Automation tactics *) - | TacTrivial (debug,lems,l) -> - begin if debug == Tacexpr.Info then - msg_warning - (strbrk"The \"info_trivial\" tactic" ++ spc () - ++strbrk"does not print traces anymore." ++ spc() - ++strbrk"Use \"Info 1 trivial\", instead.") - end; - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let lems = interp_auto_lemmas ist env sigma lems in - name_atomic ~env - (TacTrivial(debug,List.map snd lems,l)) - (Auto.h_trivial ~debug - lems - (Option.map (List.map (interp_hint_base ist)) l)) - end } - | TacAuto (debug,n,lems,l) -> - begin if debug == Tacexpr.Info then - msg_warning - (strbrk"The \"info_auto\" tactic" ++ spc () - ++strbrk"does not print traces anymore." ++ spc() - ++strbrk"Use \"Info 1 auto\", instead.") - end; - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let lems = interp_auto_lemmas ist env sigma lems in - name_atomic ~env - (TacAuto(debug,n,List.map snd lems,l)) - (Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n) - lems - (Option.map (List.map (interp_hint_base ist)) l)) - end } - (* Derived basic tactics *) | TacInductionDestruct (isrec,ev,(l,el)) -> (* spiwack: some unknown part of destruct needs the goal to be diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 0c96653626..fdf65292a1 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -154,10 +154,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacLetTac (id,c,clp,b,eqpat) -> TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat) - (* Automation tactics *) - | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (subst_glob_constr subst) lems,l) - | TacAuto (d,n,lems,l) -> TacAuto (d,n,List.map (subst_glob_constr subst) lems,l) - (* Derived basic tactics *) | TacInductionDestruct (isrec,ev,(l,el)) -> let l' = List.map (fun (c,ids,cls) -> -- cgit v1.2.3