X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Ftacticals.ml;h=34ecb2d99d1c68f6f18a58cca383cb396358f663;hb=57c7d6ef239b4c2b070721715887684adf41159c;hp=63b8e12b59a362ddafa4deb855bf215ecf6db5be;hpb=c175c78b4fd9d0bac50669e9954acf68d50014e7;p=helm.git

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index 63b8e12b5..34ecb2d99 100644
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -42,7 +42,7 @@ module PET = ProofEngineTypes
 
 let id_tac = 
  let id_tac (proof,goal) = 
-  let _, metasenv, _, _, _ = proof in
+  let _, metasenv, _, _, _, _ = proof in
   let _, _, _ = CicUtil.lookup_meta goal metasenv in
   (proof,[goal])
  in 
@@ -50,7 +50,7 @@ let id_tac =
 
 let fail_tac =
  let fail_tac (proof,goal) =
-  let _, metasenv, _, _, _ = proof in
+  let _, metasenv, _, _ , _, _ = proof in
   let _, _, _ = CicUtil.lookup_meta goal metasenv in
    raise (PET.Fail (lazy "fail tactical"))
  in
@@ -113,7 +113,7 @@ struct
      back to obtain the result of the tactic *)
   let mk_tactic f =
     PET.mk_tactic
-      (fun (proof, goal) as pstatus ->
+      (fun ((proof, goal) as pstatus) ->
         let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
         let istatus = pstatus, stack in
         let (proof, _, _), stack = f istatus in
@@ -182,23 +182,57 @@ 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: (string * tactic) list) status =
+  let rec first ~(tactics: tactic list) status =
     info (lazy "in Tacticals.first");
     match tactics with
       [] -> raise (PET.Fail (lazy "first: no tactics left"))
-    | (descr, tac)::tactics ->
-        info (lazy ("Tacticals.first IS TRYING " ^ descr));
+    | tac::tactics ->
         try
          let res = PET.apply_tactic tac status in
-          info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
+          info (lazy ("Tacticals.first: succedeed!!!"));
           res
         with 
          PET.Fail _ -> first ~tactics status
   in
   PET.mk_tactic (first ~tactics)
 
-
 let rec do_tactic ~n ~tactic =
  PET.mk_tactic
   (function status ->
@@ -230,18 +264,16 @@ let rec repeat_tactic ~tactic =
 
 (* This tries tactics until one of them solves the goal *)
 let solve_tactics ~tactics =
- let rec solve_tactics ~(tactics: (string * tactic) list) status =
+ let rec solve_tactics ~(tactics: tactic list) status =
   info (lazy "in Tacticals.solve_tactics");
   match tactics with
-  | (descr, currenttactic)::moretactics ->
-      info (lazy ("Tacticals.solve_tactics is trying " ^ descr));
+  | currenttactic::moretactics ->
       (try
         let (proof, opened) as output_status =
          PET.apply_tactic currenttactic status 
         in
         match opened with 
-          | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^ 
-                   " solved the goal!!!"));
+          | [] -> info (lazy ("Tacticals.solve_tactics: solved the goal!!!"));
                   output_status
           | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
                  raise (PET.Fail (lazy "Goal not solved"))
@@ -258,16 +290,18 @@ let solve_tactics ~tactics =
 
 let progress_tactic ~tactic =
   let msg = lazy "Failed to progress" in
-  let progress_tactic (((_,metasenv,_,_,_),_) as istatus) =
-    let ((_,metasenv',_,_,_),_) as ostatus =
+  let progress_tactic (((_,metasenv,_,_,_,_),g) as istatus) =
+    let ((_,metasenv',_,_,_,_),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