diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/coretactics.ml4 | 70 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 14 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 71 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 12 |
4 files changed, 69 insertions, 98 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 63fb67e146..74d98176a4 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -15,6 +15,7 @@ open Misctypes open Genredexpr open Proofview.Notations +open Sigma.Notations DECLARE PLUGIN "coretactics" @@ -140,10 +141,19 @@ END TACTIC EXTEND symmetry [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ] +| [ "symmetry" clause(cl) ] -> [ Tactics.intros_symmetry cl ] END (** Split *) +let rec delayed_list = function +| [] -> { Tacexpr.delayed = fun _ sigma -> Sigma.here [] sigma } +| x :: l -> + { Tacexpr.delayed = fun env sigma -> + let Sigma (x, sigma, p) = x.Tacexpr.delayed env sigma in + let Sigma (l, sigma, q) = (delayed_list l).Tacexpr.delayed env sigma in + Sigma (x :: l, sigma, p +> q) } + TACTIC EXTEND split [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ] END @@ -164,12 +174,35 @@ TACTIC EXTEND esplit_with ] END +TACTIC EXTEND exists + [ "exists" ] -> [ Tactics.split_with_bindings false [NoBindings] ] +| [ "exists" ne_bindings_list_sep(bll, ",") ] -> [ + Tacticals.New.tclDELAYEDWITHHOLES false (delayed_list bll) (fun bll -> Tactics.split_with_bindings false bll) + ] +END + +TACTIC EXTEND eexists + [ "eexists" ] -> [ Tactics.split_with_bindings true [NoBindings] ] +| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> [ + Tacticals.New.tclDELAYEDWITHHOLES true (delayed_list bll) (fun bll -> Tactics.split_with_bindings true bll) + ] +END + (** Intro *) TACTIC EXTEND intros_until [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ] END +(** Move *) + +TACTIC EXTEND move + [ "move" hyp(id) "at" "top" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveFirst) ] +| [ "move" hyp(id) "at" "bottom" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveLast) ] +| [ "move" hyp(id) "after" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveAfter h)) ] +| [ "move" hyp(id) "before" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveBefore h)) ] +END + (** Revert *) TACTIC EXTEND revert @@ -192,6 +225,42 @@ TACTIC EXTEND admit [ "admit" ] -> [ Proofview.give_up ] END +(* Fix *) + +TACTIC EXTEND fix + [ "fix" natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix None n) ] +| [ "fix" ident(id) natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix (Some id) n) ] +END + +(* Cofix *) + +TACTIC EXTEND cofix + [ "cofix" ] -> [ Proofview.V82.tactic (Tactics.cofix None) ] +| [ "cofix" ident(id) ] -> [ Proofview.V82.tactic (Tactics.cofix (Some id)) ] +END + +(* Clear *) + +TACTIC EXTEND clear + [ "clear" hyp_list(ids) ] -> [ + if List.is_empty ids then Tactics.keep [] + else Proofview.V82.tactic (Tactics.clear ids) + ] +| [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ] +END + +(* Clearbody *) + +TACTIC EXTEND clearbody + [ "clearbody" ne_hyp_list(ids) ] -> [ Tactics.clear_body ids ] +END + +(* Generalize dependent *) + +TACTIC EXTEND generalize_dependent + [ "generalize" "dependent" constr(c) ] -> [ Proofview.V82.tactic (Tactics.generalize_dep c) ] +END + (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) open Tacexpr @@ -210,7 +279,6 @@ let initial_atomic () = "compute", TacReduce(Cbv Redops.all_flags,nocl); "intro", TacIntroMove(None,MoveLast); "intros", TacIntroPattern []; - "cofix", TacCofix None; ] in let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index cbb9db65c1..a069fd7557 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -491,11 +491,9 @@ let rec intern_atomic lf ist x = TacElim (ev,intern_constr_with_bindings_arg ist cb, Option.map (intern_constr_with_bindings ist) cbo) | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings_arg ist cb) - | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n) | TacMutualFix (id,n,l) -> let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in TacMutualFix (intern_ident lf ist id, n, List.map f l) - | TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt) | TacMutualCofix (id,l) -> let f (id,c) = (intern_ident lf ist id,intern_type ist c) in TacMutualCofix (intern_ident lf ist id, List.map f l) @@ -507,7 +505,6 @@ let rec intern_atomic lf ist x = TacGeneralize (List.map (fun (c,na) -> intern_constr_with_occurrences ist c, intern_name lf ist na) cl) - | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c) | TacLetTac (na,c,cls,b,eqpat) -> let na = intern_name lf ist na in TacLetTac (na,intern_constr ist c, @@ -527,18 +524,11 @@ let rec intern_atomic lf ist x = let h2 = intern_quantified_hypothesis ist h2 in TacDoubleInduction (h1,h2) (* Context management *) - | TacClear (b,l) -> TacClear (b,List.map (intern_hyp ist) l) - | TacClearBody l -> TacClearBody (List.map (intern_hyp ist) l) - | TacMove (id1,id2) -> - TacMove (intern_hyp ist id1,intern_move_location ist id2) | TacRename l -> TacRename (List.map (fun (id1,id2) -> intern_hyp ist id1, intern_hyp ist id2) l) - (* Constructors *) - | TacSplit (ev,bll) -> TacSplit (ev,List.map (intern_bindings ist) bll) - (* Conversion *) | TacReduce (r,cl) -> dump_glob_red_expr r; @@ -560,10 +550,6 @@ let rec intern_atomic lf ist x = TacChange (Some (intern_typed_pattern ist p),intern_constr ist c, clause_app (intern_hyp_location ist) cl) - (* Equivalence relations *) - | TacSymmetry idopt -> - TacSymmetry (clause_app (intern_hyp_location ist) idopt) - (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> TacRewrite diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d5a1215b87..1a8a95158a 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1749,15 +1749,6 @@ and interp_atomic ist tac : unit Proofview.tactic = in Tacticals.New.tclWITHHOLES ev named_tac sigma end } - | TacFix (idopt,n) -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let idopt = Option.map (interp_ident ist env sigma) idopt in - name_atomic ~env - (TacFix(idopt,n)) - (Proofview.V82.tactic (Tactics.fix idopt n)) - end } | TacMutualFix (id,n,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin @@ -1773,15 +1764,6 @@ and interp_atomic ist tac : unit Proofview.tactic = Sigma.Unsafe.of_pair (tac, sigma) end } end - | TacCofix idopt -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let idopt = Option.map (interp_ident ist env sigma) idopt in - name_atomic ~env - (TacCofix (idopt)) - (Proofview.V82.tactic (Tactics.cofix idopt)) - end } | TacMutualCofix (id,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin @@ -1821,12 +1803,6 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacGeneralize cl) (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma end } - | TacGeneralizeDep c -> - (new_interp_constr ist c) (fun c -> - name_atomic (* spiwack: probably needs a goal environment *) - (TacGeneralizeDep c) - (Proofview.V82.tactic (Tactics.generalize_dep c)) - ) | TacLetTac (na,c,clp,b,eqpat) -> Proofview.V82.nf_evar_goals <*> Proofview.Goal.nf_enter { enter = begin fun gl -> @@ -1899,31 +1875,6 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacDoubleInduction (h1,h2)) (Elim.h_double_induction h1 h2) (* Context management *) - | TacClear (b,l) -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = pf_env gl in - let sigma = project gl in - let l = interp_hyp_list ist env sigma l in - if b then name_atomic ~env (TacClear (b, l)) (Tactics.keep l) - else - (* spiwack: until the tactic is in the monad *) - let tac = Proofview.V82.tactic (fun gl -> Tactics.clear l gl) in - Proofview.Trace.name_tactic (fun () -> Pp.str"<clear>") tac - end } - | TacClearBody l -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = pf_env gl in - let sigma = project gl in - let l = interp_hyp_list ist env sigma l in - name_atomic ~env - (TacClearBody l) - (Tactics.clear_body l) - end } - | TacMove (id1,id2) -> - Proofview.Goal.enter { enter = begin fun gl -> - Proofview.V82.tactic (Tactics.move_hyp (interp_hyp ist (pf_env gl) (project gl) id1) - (interp_move_location ist (pf_env gl) (project gl) id2)) - end } | TacRename l -> Proofview.Goal.enter { enter = begin fun gl -> let env = pf_env gl in @@ -1938,18 +1889,6 @@ and interp_atomic ist tac : unit Proofview.tactic = (Tactics.rename_hyp l) end } - (* Constructors *) - | TacSplit (ev,bll) -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in - let named_tac = - let tac = Tactics.split_with_bindings ev bll in - name_atomic ~env (TacSplit (ev, bll)) tac - in - Tacticals.New.tclWITHHOLES ev named_tac sigma - end } (* Conversion *) | TacReduce (r,cl) -> (* spiwack: until the tactic is in the monad *) @@ -2018,16 +1957,6 @@ and interp_atomic ist tac : unit Proofview.tactic = end } end - (* Equivalence relations *) - | TacSymmetry c -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let cl = interp_clause ist env sigma c in - name_atomic ~env - (TacSymmetry cl) - (Tactics.intros_symmetry cl) - end } (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 4a5fa9828e..3f103a290d 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -146,17 +146,14 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with TacElim (ev,subst_glob_with_bindings_arg subst cb, Option.map (subst_glob_with_bindings subst) cbo) | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings_arg subst cb) - | TacFix (idopt,n) as x -> x | TacMutualFix (id,n,l) -> TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l) - | TacCofix idopt as x -> x | TacMutualCofix (id,l) -> TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l) | TacAssert (b,otac,na,c) -> TacAssert (b,Option.map (subst_tactic subst) otac,na,subst_glob_constr subst c) | TacGeneralize cl -> TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl) - | TacGeneralizeDep c -> TacGeneralizeDep (subst_glob_constr subst c) | TacLetTac (id,c,clp,b,eqpat) -> TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat) @@ -169,23 +166,14 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacDoubleInduction (h1,h2) as x -> x (* Context management *) - | TacClear _ as x -> x - | TacClearBody l as x -> x - | TacMove (id1,id2) as x -> x | TacRename l as x -> x - (* Constructors *) - | TacSplit (ev,bll) -> TacSplit (ev,List.map (subst_bindings subst) bll) - (* Conversion *) | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl) | TacChange (op,c,cl) -> TacChange (Option.map (subst_glob_constr_or_pattern subst) op, subst_glob_constr subst c, cl) - (* Equivalence relations *) - | TacSymmetry _ as x -> x - (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> TacRewrite (ev, |