diff options
| -rw-r--r-- | intf/tacexpr.mli | 4 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 3 | ||||
| -rw-r--r-- | printing/pptactic.ml | 6 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 6 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 5 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 5 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 15 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 6 |
8 files changed, 46 insertions, 4 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index efe62f569c..0c2b754788 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -251,6 +251,10 @@ and 'a gen_tactic_expr = 'a gen_tactic_expr | TacExactlyOnce of 'a gen_tactic_expr + | TacIfThenCatch of + 'a gen_tactic_expr * + 'a gen_tactic_expr * + 'a gen_tactic_expr | TacOrelse of 'a gen_tactic_expr * 'a gen_tactic_expr diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index de8d332b8b..b2b1d5adea 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -84,6 +84,9 @@ GEXTEND Gram | "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 diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 412c1050b4..d43b94ec4b 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1190,6 +1190,12 @@ module Make keyword "exactly_once" ++ spc () ++ pr_tac (ltactical,E) t), ltactical + | TacIfThenCatch (t,tt,te) -> + hov 1 ( + str"tryif" ++ spc() ++ pr_tac (ltactical,E) t ++ brk(1,1) ++ + str"then" ++ spc() ++ pr_tac (ltactical,E) tt ++ brk(1,1) ++ + str"else" ++ spc() ++ pr_tac (ltactical,E) te ++ brk(1,1)), + ltactical | TacOrelse (t1,t2) -> hov 1 ( pr_tac (lorelse,L) t1 ++ spc () diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 7d609e1a53..c0e18c1f28 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -654,6 +654,12 @@ and intern_tactic_seq onlytac ist = function ist.ltacvars, TacOnce (intern_pure_tactic ist tac) | TacExactlyOnce tac -> ist.ltacvars, TacExactlyOnce (intern_pure_tactic ist tac) + | TacIfThenCatch (tac,tact,tace) -> + ist.ltacvars, + TacIfThenCatch ( + intern_pure_tactic ist tac, + intern_pure_tactic ist tact, + intern_pure_tactic ist tace) | TacOrelse (tac1,tac2) -> ist.ltacvars, TacOrelse (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_pure_tactic ist) l) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e774316a66..fc31c3a994 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1169,6 +1169,11 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Tacticals.New.tclONCE (interp_tactic ist tac) | TacExactlyOnce tac -> Tacticals.New.tclEXACTLY_ONCE (interp_tactic ist tac) + | TacIfThenCatch (t,tt,te) -> + Tacticals.New.tclIFCATCH + (interp_tactic ist t) + (fun () -> interp_tactic ist tt) + (fun () -> interp_tactic ist te) | TacOrelse (tac1,tac2) -> Tacticals.New.tclORELSE (interp_tactic ist tac1) (interp_tactic ist tac2) | TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 5a02a53f3e..ca6a40a80f 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -244,6 +244,11 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with TacOnce (subst_tactic subst tac) | TacExactlyOnce tac -> TacExactlyOnce (subst_tactic subst tac) + | TacIfThenCatch (tac,tact,tace) -> + TacIfThenCatch ( + subst_tactic subst tac, + subst_tactic subst tact, + subst_tactic subst tace) | TacOrelse (tac1,tac2) -> TacOrelse (subst_tactic subst tac1,subst_tactic subst tac2) | TacFirst l -> TacFirst (List.map (subst_tactic subst) l) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bb7a3f2e32..82ec155595 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -339,6 +339,13 @@ module New = struct let tclEXACTLY_ONCE t = Proofview.tclEXACTLY_ONCE (Refiner.FailError(0,lazy (assert false))) t + let tclIFCATCH t tt te = + tclINDEPENDENT begin + Proofview.tclIFCATCH t + tt + (fun e -> catch_failerror e <*> te ()) + end + let tclORELSE0 t1 t2 = tclINDEPENDENT begin tclORELSE @@ -401,12 +408,12 @@ module New = struct let tclIFTHENELSE t1 t2 t3 = tclINDEPENDENT begin - tclIFCATCH t1 + Proofview.tclIFCATCH t1 (fun () -> t2) (fun e -> Proofview.tclORELSE t3 (fun e' -> tclZERO e)) end let tclIFTHENSVELSE t1 a t3 = - tclIFCATCH t1 + Proofview.tclIFCATCH t1 (fun () -> tclDISPATCH (Array.to_list a)) (fun _ -> t3) let tclIFTHENTRYELSEMUST t1 t2 = @@ -434,14 +441,14 @@ module New = struct let rec tclREPEAT0 t = tclINDEPENDENT begin - tclIFCATCH t + Proofview.tclIFCATCH t (fun () -> tclCHECKINTERRUPT <*> tclREPEAT0 t) (fun e -> catch_failerror e <*> tclUNIT ()) end let tclREPEAT t = tclREPEAT0 (tclPROGRESS t) let rec tclREPEAT_MAIN0 t = - tclIFCATCH t + Proofview.tclIFCATCH t (fun () -> tclTRYFOCUS 1 1 (tclREPEAT_MAIN0 t)) (fun e -> catch_failerror e <*> tclUNIT ()) let tclREPEAT_MAIN t = diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 35a3205896..fbdc6d94e1 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -176,6 +176,12 @@ module New : sig val tclONCE : unit tactic -> unit tactic val tclEXACTLY_ONCE : unit tactic -> unit tactic + + val tclIFCATCH : + unit tactic -> + (unit -> unit tactic) -> + (unit -> unit tactic) -> unit tactic + val tclORELSE0 : unit tactic -> unit tactic -> unit tactic val tclORELSE : unit tactic -> unit tactic -> unit tactic |