diff options
| -rw-r--r-- | grammar/q_coqast.ml4 | 2 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 3 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 4 | ||||
| -rw-r--r-- | printing/pptactic.ml | 5 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 8 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 |
9 files changed, 28 insertions, 1 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index b1150d6c0..d0fd618c7 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -453,6 +453,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function <:expr< Tacexpr.TacSolve $mlexpr_of_list mlexpr_of_tactic tl$ >> | Tacexpr.TacTry t -> <:expr< Tacexpr.TacTry $mlexpr_of_tactic t$ >> + | Tacexpr.TacOr (t1,t2) -> + <:expr< Tacexpr.TacOr $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$ >> | Tacexpr.TacOrelse (t1,t2) -> <:expr< Tacexpr.TacOrelse $mlexpr_of_tactic t1$ $mlexpr_of_tactic t2$ >> | Tacexpr.TacDo (n,t) -> diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index df4ed2c41..fece99312 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -214,6 +214,9 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr = | TacComplete of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr | TacSolve of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr list | TacTry of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr + | TacOr of + ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr * + ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr | TacOrelse of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr * ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index e0a1c046a..96f4bc387 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -73,7 +73,9 @@ GEXTEND Gram TacAbstract (tc,Some s) ] (*End of To do*) | "2" RIGHTA - [ ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1) + [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1) + | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> TacOr (ta0,ta1) + | 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" -> diff --git a/printing/pptactic.ml b/printing/pptactic.ml index a77118471..61f758df0 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -886,6 +886,11 @@ let rec pr_tac inherited tac = | TacInfo t -> hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t), linfo + | TacOr (t1,t2) -> + (* arnaud: vérifier qu'il s'agit bien de la syntaxe définitive. *) + hov 1 (pr_tac (lorelse,L) t1 ++ str " +" ++ brk (1,1) ++ + pr_tac (lorelse,E) t2), + lorelse | TacOrelse (t1,t2) -> hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++ pr_tac (lorelse,E) t2), diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 6b06a0534..ddabb5d08 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -687,6 +687,8 @@ and intern_tactic_seq onlytac ist = function | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_pure_tactic ist tac) | TacTimeout (n,tac) -> ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic onlytac ist tac) + | TacOr (tac1,tac2) -> + ist.ltacvars, TacOr (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) | 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 0e54ed84c..abc1daa5b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1137,6 +1137,8 @@ and eval_tactic ist = function | TacTimeout (n,tac) -> Tacticals.New.tclTIMEOUT (interp_int_or_var ist n) (interp_tactic ist tac) | TacTry tac -> Tacticals.New.tclTRY (interp_tactic ist tac) | TacRepeat tac -> Tacticals.New.tclREPEAT (interp_tactic ist tac) + | TacOr (tac1,tac2) -> + Tacticals.New.tclOR (interp_tactic ist tac1) (interp_tactic ist tac2) | 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 deac1d4ff..ba37c1019 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -247,6 +247,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacTry tac -> TacTry (subst_tactic subst tac) | TacInfo tac -> TacInfo (subst_tactic subst tac) | TacRepeat tac -> TacRepeat (subst_tactic subst tac) + | TacOr (tac1,tac2) -> + TacOr (subst_tactic subst tac1,subst_tactic subst tac2) | 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 8156c898e..74c31fa38 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -383,6 +383,14 @@ module New = struct Refiner.catch_failerror e; tclUNIT () with e -> tclZERO e + + (* spiwack: I chose to give the Ltac + the same semantics as + [Proofview.tclOR], however, for consistency with the or-else + tactical, we may consider wrapping the first argument with + [tclPROGRESS]. It strikes me as a bad idea, but consistency can be + considered valuable. *) + let tclOR = Proofview.Notations.(<+>) + let tclORELSE0 t1 t2 = tclINDEPENDENT begin tclORELSE diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index d0dae0993..f7ba178a3 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -183,6 +183,7 @@ module New : sig (meaning that it will jump over [n] error catching tacticals FROM THIS MODULE. *) val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic + val tclOR : unit tactic -> unit tactic -> unit tactic val tclORELSE0 : unit tactic -> unit tactic -> unit tactic val tclORELSE : unit tactic -> unit tactic -> unit tactic |