X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Ftacticals.ml;h=f647ebccaa9d199181761b2233c59f00ace13f1d;hb=ea8ddf1f729c60d4eee6c659b179d9b77b6ec241;hp=06f96a573c28f367c244a649080c4fc136c7e981;hpb=f438e9b0c8e43a66c56b17adeb8793042d0aade1;p=helm.git

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index 06f96a573..f647ebcca 100644
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -182,6 +182,42 @@ let seq ~tactics =
 
 (* Tacticals that cannot be implemented on top of tynycals *)
 
+let const_tac res = PET.mk_tactic (fun _ -> res)
+
+let if_ ~start ~continuation ~fail =
+   let if_ status =
+      let xoutput = 
+         try
+	    let result = PET.apply_tactic start status in
+	    info (lazy ("Tacticals.if_: succedeed!!!"));
+	    Some result 
+	 with PET.Fail _ -> None
+      in
+      let tactic = match xoutput with
+         | Some res -> then_ ~start:(const_tac res) ~continuation
+	 | None     -> fail
+      in 
+      PET.apply_tactic tactic status
+   in
+   PET.mk_tactic if_
+
+let ifs ~start ~continuations ~fail =
+   let ifs status =
+      let xoutput = 
+         try
+	    let result = PET.apply_tactic start status in
+	    info (lazy ("Tacticals.ifs: succedeed!!!"));
+	    Some result 
+	 with PET.Fail _ -> None
+      in
+      let tactic = match xoutput with
+         | Some res -> thens ~start:(const_tac res) ~continuations
+	 | None     -> fail
+      in 
+      PET.apply_tactic tactic status
+   in
+   PET.mk_tactic ifs
+
 let first ~tactics =
   let rec first ~(tactics: tactic list) status =
     info (lazy "in Tacticals.first");
@@ -197,7 +233,6 @@ let first ~tactics =
   in
   PET.mk_tactic (first ~tactics)
 
-
 let rec do_tactic ~n ~tactic =
  PET.mk_tactic
   (function status ->