- semantics of tactic subst allmost fixed

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

diff --git a/components/tactics/tacticals.ml b/components/tactics/tacticals.ml
index ceb2d2de88cb28fc8a7554ee87c1167e5c846af8..28bd71b2da5901c199114dde8ce8bacf79aaa17f 100644 (file)
--- a/components/tactics/tacticals.ml
+++ b/components/tactics/tacticals.ml
@@ -38,23 +38,25 @@ let debug_print = fun _ -> ()
   (** debugging print *)
 let info s = debug_print (lazy ("TACTICALS INFO: " ^ (Lazy.force s)))
 
+module PET = ProofEngineTypes
+
 let id_tac = 
  let id_tac (proof,goal) = 
   let _, metasenv, _, _ = proof in
   let _, _, _ = CicUtil.lookup_meta goal metasenv in
   (proof,[goal])
  in 
-  ProofEngineTypes.mk_tactic id_tac
+  PET.mk_tactic id_tac
 
 let fail_tac =
  let fail_tac (proof,goal) =
   let _, metasenv, _, _ = proof in
   let _, _, _ = CicUtil.lookup_meta goal metasenv in
-   raise (ProofEngineTypes.Fail (lazy "fail tactical"))
+   raise (PET.Fail (lazy "fail tactical"))
  in
-  ProofEngineTypes.mk_tactic fail_tac
+  PET.mk_tactic fail_tac
 
-type goal = ProofEngineTypes.goal
+type goal = PET.goal
 
     (** TODO needed until tactics start returning both opened and closed goals
      * First part of the function performs a diff among goals ~before tactic
@@ -97,6 +99,7 @@ sig
   val do_tactic: n: int -> tactic: tactic -> tactic 
   val try_tactic: tactic: tactic -> tactic 
   val solve_tactics: tactics: (string * tactic) list -> tactic
+  val progress_tactic: tactic: tactic -> tactic 
 
   val tactic: tactic -> tactic
   val skip: tactic
@@ -141,7 +144,7 @@ struct
           with
           e ->
             match e with
-            | (ProofEngineTypes.Fail _)
+            | (PET.Fail _)
             | (CicTypeChecker.TypeCheckerFailure _)
             | (CicUnification.UnificationFailure _) ->
                 info (lazy (
@@ -149,7 +152,7 @@ struct
                   Printexc.to_string e));
                   first ~tactics istatus
             | _ -> raise e) (* [e] must not be caught ; let's re-raise it *)
-      | [] -> raise (ProofEngineTypes.Fail (lazy "first: no tactics left"))
+      | [] -> raise (PET.Fail (lazy "first: no tactics left"))
     in
     S.mk_tactic (first ~tactics)
 
@@ -210,7 +213,7 @@ struct
      in
      S.set_goals (opened', closed') output_status
     with 
-     (ProofEngineTypes.Fail _) as e ->
+     (PET.Fail _) as e ->
       info (lazy
         ("Tacticals.repeat_tactic failed after nth time with exception: "
          ^ Printexc.to_string e));
@@ -232,7 +235,7 @@ struct
        in
        S.set_goals (opened', closed') output_status
      with 
-      (ProofEngineTypes.Fail _) as e ->
+      (PET.Fail _) as e ->
        info (lazy
           ("Tacticals.do_tactic failed after nth time with exception: "
            ^ Printexc.to_string e)) ;
@@ -242,17 +245,17 @@ struct
 
   (* This applies tactic and catches its possible failure *)
   let try_tactic ~tactic =
-   let rec try_tactic ~tactic status =
+   let try_tactic status =
     info (lazy "in Tacticals.try_tactic");
     try
      S.apply_tactic tactic status
     with
-     (ProofEngineTypes.Fail _) as e -> 
+     (PET.Fail _) as e -> 
       info (lazy (
         "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e));
       S.apply_tactic S.id_tactic status
    in
-    S.mk_tactic (try_tactic ~tactic)
+    S.mk_tactic try_tactic
 
   (* This tries tactics until one of them doesn't _solve_ the goal *)
   (* TODO: si puo' unificare le 2(due) chiamate ricorsive? *)
@@ -275,18 +278,35 @@ struct
             | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
                    solve_tactics ~tactics:(moretactics) status
          with
-          (ProofEngineTypes.Fail _) as e ->
+          (PET.Fail _) as e ->
            info (lazy (
               "Tacticals.solve_tactics: current tactic failed with exn: "
               ^ Printexc.to_string e));
            solve_tactics ~tactics status
         )
     | [] ->
-        raise (ProofEngineTypes.Fail
+        raise (PET.Fail
           (lazy "solve_tactics cannot solve the goal"))
    in
     S.mk_tactic (solve_tactics ~tactics)
 
+  let progress_tactic ~tactic =
+    let msg = lazy "Failed to progress" in
+    let get_sequent (proof, goal) =
+      let (_, metasenv, _, _) = proof in
+      let _, context, ty = CicUtil.lookup_meta goal metasenv in
+      context, ty
+    in
+    let progress_tactic ist =
+      let before = get_sequent (S.get_status ist) in
+      let ost = S.apply_tactic tactic ist in
+      match S.goals ost with
+        | [goal], _ when before <> get_sequent (S.get_proof ost, goal) ->
+           raise (PET.Fail msg)
+        | _  -> ost
+    in
+    S.mk_tactic progress_tactic
+
   let cont_proxy cont = S.mk_tactic (C.eval cont)
 
   let tactic t = cont_proxy (C.Tactical (C.Tactic t))
@@ -307,17 +327,17 @@ struct
   module Stack = Continuationals.Stack
 
   type input_status =
-    ProofEngineTypes.status (* (proof, goal) *) * Stack.t
+    PET.status (* (proof, goal) *) * Stack.t
 
   type output_status =
-    (ProofEngineTypes.proof * goal list * goal list) * Stack.t
+    (PET.proof * goal list * goal list) * Stack.t
 
-  type tactic = ProofEngineTypes.tactic
+  type tactic = PET.tactic
 
   let id_tactic = id_tac
 
   let mk_tactic f =
-    ProofEngineTypes.mk_tactic
+    PET.mk_tactic
       (fun (proof, goal) as pstatus ->
         let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
         let istatus = pstatus, stack in
@@ -328,14 +348,17 @@ struct
         proof, opened)
 
   let apply_tactic tac ((proof, _) as pstatus, stack) =
-    let proof', opened = ProofEngineTypes.apply_tactic tac pstatus in
+    let proof', opened = PET.apply_tactic tac pstatus in
 (* let _ = prerr_endline ("goal aperti dalla tattica " ^ String.concat "," (List.map string_of_int opened)) in *)
-    let before = ProofEngineTypes.goals_of_proof proof in
-    let after = ProofEngineTypes.goals_of_proof proof' in
+    let before = PET.goals_of_proof proof in
+    let after = PET.goals_of_proof proof' in
     let opened_goals, closed_goals = goals_diff ~before ~after ~opened in
 (* let _ = prerr_endline ("goal ritornati dalla tattica " ^ String.concat "," (List.map string_of_int opened_goals)) in *)
     (proof', opened_goals, closed_goals), stack
 
+  let get_status (status, _) = status
+  let get_proof ((proof, _, _), _) = proof
+
   let goals ((_, opened, closed), _) = opened, closed
   let set_goals (opened, closed) ((proof, _, _), stack) =
     (proof, opened, closed), stack