- tacticals: new tactical ifs added: uses thens where if_ uses then_

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

diff --git a/components/tactics/tacticals.ml b/components/tactics/tacticals.ml
index 3e9c1db2cbb59f2db82f313b5b934f6058ea8657..f647ebccaa9d199181761b2233c59f00ace13f1d 100644 (file)
--- a/components/tactics/tacticals.ml
+++ b/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, _subst, _, _, _ = 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, _subst, _ , _, _ = 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,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 ->
@@ -255,8 +290,8 @@ 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,_subst,_,_,_),_) as istatus) =
+    let ((_,metasenv',_subst,_,_,_),_) as ostatus =
      PET.apply_tactic tactic istatus
     in
      (*CSC: Warning