diff options
| -rw-r--r-- | intf/tacexpr.mli | 2 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 1 | ||||
| -rw-r--r-- | printing/pptactic.ml | 4 | ||||
| -rw-r--r-- | proofs/proofview.ml | 22 | ||||
| -rw-r--r-- | proofs/proofview.mli | 7 | ||||
| -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 | 2 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 |
10 files changed, 45 insertions, 0 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 839294c0a1..0ddf58b74a 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -219,6 +219,8 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr = ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr | TacOnce of ('t,'p,'c,'i,'r,'n,'l) gen_tactic_expr + | TacExactlyOnce of + ('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 033de89df3..d075a77904 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -67,6 +67,7 @@ GEXTEND Gram | 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) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f0d713be48..c5a8a380d6 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -895,6 +895,10 @@ let rec pr_tac inherited tac = (* arnaud: vérifier qu'il s'agit bien de la syntaxe définitive. *) hov 1 (str "once" ++ spc () ++ pr_tac (ltactical,E) t), ltactical + | TacExactlyOnce t -> + (* arnaud: vérifier qu'il s'agit bien de la syntaxe définitive. *) + hov 1 (str "exactly_once" ++ spc () ++ pr_tac (ltactical,E) t), + ltactical | TacOrelse (t1,t2) -> hov 1 (pr_tac (lorelse,L) t1 ++ str " ||" ++ brk (1,1) ++ pr_tac (lorelse,E) t2), diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 823082aced..bb1d5758d6 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -253,6 +253,28 @@ let tclONCE t = | Nil e -> tclZERO e | Cons (x,_) -> tclUNIT x +exception MoreThanOneSuccess +let _ = Errors.register_handler begin function + | MoreThanOneSuccess -> Errors.error "This tactic has more than one success." + | _ -> raise Errors.Unhandled +end + +(* [tclONCE e t] succeeds as [t] if [t] has exactly one + success. Otherwise it fails. It may behave differently than [t] as + there may be extra non-logical effects used to discover that [t] + does not have a second success. Moreover the second success may be + conditional on the error recieved: [e] is used. *) +let tclEXACTLY_ONCE e t = + (* spiwack: convenience notations, waiting for ocaml 3.12 *) + let (>>=) = Proof.bind in + Proof.split t >>= function + | Nil e -> tclZERO e + | Cons (x,k) -> + Proof.split (k e) >>= function + | Nil _ -> tclUNIT x + | _ -> tclZERO MoreThanOneSuccess + + (* Focuses a tactic at a range of subgoals, found by their indices. *) (* arnaud: bug if 0 goals ! *) let tclFOCUS i j t = diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 0504efea57..5b25c003d6 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -160,6 +160,13 @@ val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (exn -> 'b tactic) -> 'b tact success. *) val tclONCE : 'a tactic -> 'a tactic +(* [tclONCE e t] succeeds as [t] if [t] has exactly one + success. Otherwise it fails. It may behave differently than [t] as + there may be extra non-logical effects used to discover that [t] + does not have a second success. Moreover the second success may be + conditional on the error recieved: [e] is used. *) +val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic + (* Focuses a tactic at a range of subgoals, found by their indices. *) val tclFOCUS : int -> int -> 'a tactic -> 'a tactic diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 2f41ff2aea..42ea649ecd 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -691,6 +691,8 @@ and intern_tactic_seq onlytac ist = function ist.ltacvars, TacOr (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2) | TacOnce tac -> ist.ltacvars, TacOnce (intern_pure_tactic ist tac) + | TacExactlyOnce tac -> + ist.ltacvars, TacExactlyOnce (intern_pure_tactic ist tac) | 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 2c64b669c5..edb9ab66d3 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1141,6 +1141,8 @@ and eval_tactic ist = function Tacticals.New.tclOR (interp_tactic ist tac1) (interp_tactic ist tac2) | TacOnce tac -> Tacticals.New.tclONCE (interp_tactic ist tac) + | TacExactlyOnce tac -> + Tacticals.New.tclEXACTLY_ONCE (interp_tactic ist tac) | 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 44327abef2..7c968865ac 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -251,6 +251,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with TacOr (subst_tactic subst tac1,subst_tactic subst tac2) | TacOnce tac -> TacOnce (subst_tactic subst tac) + | TacExactlyOnce tac -> + TacExactlyOnce (subst_tactic subst tac) | 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 1b8cf531bc..f25bae9bb8 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -400,6 +400,8 @@ module New = struct let tclONCE = Proofview.tclONCE + let tclEXACTLY_ONCE t = Proofview.tclEXACTLY_ONCE (Refiner.FailError(0,lazy (assert false))) t + let tclORELSE0 t1 t2 = tclINDEPENDENT begin tclORELSE diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 722cb8b135..efeb4a7478 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -185,6 +185,7 @@ module New : sig val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic val tclOR : unit tactic -> unit tactic -> unit tactic val tclONCE : unit tactic -> unit tactic + val tclEXACTLY_ONCE : unit tactic -> unit tactic val tclORELSE0 : unit tactic -> unit tactic -> unit tactic val tclORELSE : unit tactic -> unit tactic -> unit tactic |