From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 30 Oct 2007 19:40:06 +0000 (+0000)
Subject: better implementation of if_
X-Git-Tag: make_still_working~5922
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1212c08483bf6b652d2d013f4ce3bdb60a8388b8;p=helm.git

better implementation of if_
---

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index cf5f22206..d5ec8acfb 100644
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -180,29 +180,26 @@ let seq ~tactics =
         (HExtlib.list_concat ~sep:[ C.Semicolon ]
           (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
 
+(* Tacticals that cannot be implemented on top of tynycals *)
+
+let const_tac res = PET.mk_tactic (fun _ -> res)
+
 let if_ ~start ~continuation ~fail =
-  S.mk_tactic
-    (fun istatus -> 
-      let xostatus = 
-         try 
-	    let res = C.eval (C.Tactical (C.Tactic start)) istatus in
+   let if_ status =
+      let xoutput = 
+         try
+	    let result = PET.apply_tactic start status in
 	    info (lazy ("Tacticals.if_: succedeed!!!"));
-	    Some res
+	    Some result 
 	 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 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 first ~tactics =
   let rec first ~(tactics: tactic list) status =
@@ -219,7 +216,6 @@ let first ~tactics =
   in
   PET.mk_tactic (first ~tactics)
 
-
 let rec do_tactic ~n ~tactic =
  PET.mk_tactic
   (function status ->