X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Ftacticals.ml;h=4a4f150b7bf3e27eb6d7beacdc50df2d84c4d82e;hb=456ea05ac26bf48e4cdc0d745a92de0d14b3ff80;hp=cf5f22206d75faa5463932311a3c3b13625f2544;hpb=18825eb46860edafe9b1082b2ed4c679778a4ce8;p=helm.git

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index cf5f22206..4a4f150b7 100644
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -180,29 +180,43 @@ 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 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 =
@@ -219,7 +233,6 @@ let first ~tactics =
   in
   PET.mk_tactic (first ~tactics)
 
-
 let rec do_tactic ~n ~tactic =
  PET.mk_tactic
   (function status ->
@@ -277,16 +290,18 @@ let solve_tactics ~tactics =
 
 let progress_tactic ~tactic =
   let msg = lazy "Failed to progress" in
-  let progress_tactic (((_,metasenv,_subst,_,_,_),_) as istatus) =
-    let ((_,metasenv',_subst,_,_,_),_) as ostatus =
+  let progress_tactic (((_,metasenv,_subst,_,_,_),g) as istatus) =
+    let ((_,metasenv',_subst,_,_,_),opened) as ostatus =
      PET.apply_tactic tactic istatus
     in
-     (*CSC: Warning
-       If just the index of some metas changes the tactic is recognized
-       as a progressing one. This is wrong. *)
-     if metasenv' = metasenv then
-      raise (PET.Fail msg)
-     else
-      ostatus
+    match opened with
+    | [g1] ->
+        let _,oc,oldty = CicUtil.lookup_meta g metasenv in
+        let _,nc,newty = CicUtil.lookup_meta g1 metasenv' in
+        if oldty = newty && oc = nc then
+          raise (PET.Fail msg)
+        else
+          ostatus
+    | _ -> ostatus
   in
   PET.mk_tactic progress_tactic