- destruct: core of subst tactic implemented,

[helm.git] / components / tactics / tacticals.ml

diff --git a/components/tactics/tacticals.ml b/components/tactics/tacticals.ml
index 06f96a573c28f367c244a649080c4fc136c7e981..cf5f22206d75faa5463932311a3c3b13625f2544 100644 (file)
--- a/components/tactics/tacticals.ml
+++ b/components/tactics/tacticals.ml
@@ -180,6 +180,28 @@ let seq ~tactics =
         (HExtlib.list_concat ~sep:[ C.Semicolon ]
           (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
 
+let if_ ~start ~continuation ~fail =
+  S.mk_tactic
+    (fun istatus -> 
+      let xostatus = 
+         try 
+           let res = C.eval (C.Tactical (C.Tactic start)) istatus in
+           info (lazy ("Tacticals.if_: succedeed!!!"));
+           Some res
+        with PET.Fail _ -> None
+      in
+      match xostatus with
+         | Some ostatus ->
+            let opened,closed = S.goals ostatus in
+            begin match opened with
+                | [] -> ostatus
+                | _ ->
+                   fold_eval (S.focus ~-1 ostatus)
+                      [ C.Semicolon; C.Tactical (C.Tactic continuation) ]
+            end
+        | None -> C.eval (C.Tactical (C.Tactic fail)) istatus
+    )
+
 (* Tacticals that cannot be implemented on top of tynycals *)
 
 let first ~tactics =