From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 25 Oct 2005 16:39:45 +0000 (+0000)
Subject: Semantic change: applying a tactic to the empty goal list is now an error.
X-Git-Tag: V_0_7_2_3~184
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=097b7147a9daf37360fa51828e0f14843b5bd881;p=helm.git

Semantic change: applying a tactic to the empty goal list is now an error.
---

diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml
index 345502d5b..b720b6b70 100644
--- a/helm/ocaml/tactics/continuationals.ml
+++ b/helm/ocaml/tactics/continuationals.ml
@@ -25,7 +25,7 @@
 
 open Printf
 
-let debug = true
+let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
 
 exception Error of string lazy_t
@@ -268,6 +268,7 @@ struct
       match cmd, stack with
       | _, [] -> assert false
       | Tactical tac, (g, t, k, tag) :: s ->
+          if g = [] then fail (lazy "can't apply a tactic to zero goals");
           debug_print (lazy ("context length " ^string_of_int (List.length g)));
           let rec aux s go gc =
             function
diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 827d58bbc..8281c9452 100644
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -159,54 +159,17 @@ struct
               (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) continuations))
           @ [ C.Merge ]))
 
-(*   let thens ~start ~continuations =
-   let thens ~start ~continuations status =
-   let output_status = S.apply_tactic start status in
-   let new_goals = S.goals output_status in
-    try
-     let output_status,goals =
-      List.fold_left2
-       (fun (output_status,goals) goal tactic ->
-         let status = S.focus goal output_status in
-         let output_status' = S.apply_tactic tactic status in
-         let new_goals' = S.goals output_status' in
-          (output_status',goals@new_goals')
-       ) (output_status,[]) new_goals continuations
-     in
-      S.set_goals output_status goals
-    with
-     Invalid_argument _ -> 
-      let debug = Printf.sprintf "thens: expected %i new goals, found %i"
-       (List.length continuations) (List.length new_goals)
-      in
-      raise (Fail debug)
-   in
-    S.mk_tactic (thens ~start ~continuations ) *)
-
   let then_ ~start ~continuation =
     S.mk_tactic
       (fun istatus ->
-        fold_eval istatus
-          [ C.Tactical (C.Tactic start);
-            C.Semicolon;
-            C.Tactical (C.Tactic continuation) ])
-
-(*   let then_ ~start ~continuation =
-   let then_ ~start ~continuation status =
-   let output_status = S.apply_tactic start status in
-   let new_goals = S.goals output_status in
-    let output_status,goals =
-     List.fold_left
-      (fun (output_status,goals) goal ->
-        let status = S.focus goal output_status in
-        let output_status' = S.apply_tactic continuation status in
-        let new_goals' = S.goals output_status' in
-         (output_status',goals@new_goals')
-      ) (output_status,[]) new_goals
-    in
-     S.set_goals output_status goals
-   in
-    S.mk_tactic (then_ ~start ~continuation) *)
+        let ostatus = C.eval (C.Tactical (C.Tactic start)) istatus in
+        let opened,closed = S.goals ostatus in
+         match opened with
+            [] -> ostatus
+          | _ ->
+            fold_eval (S.focus ~-1 ostatus)
+              [ C.Semicolon;
+                C.Tactical (C.Tactic continuation) ])
 
   let seq ~tactics =
     S.mk_tactic
@@ -215,12 +178,6 @@ struct
           (HExtlib.list_concat ~sep:[ C.Semicolon ]
             (List.map (fun t -> [ C.Tactical (C.Tactic t) ]) tactics)))
 
-(*   let rec seq ~tactics =
-    match tactics with
-    | [] -> assert false
-    | [tac] -> tac
-    | hd :: tl -> then_ ~start:hd ~continuation:(seq ~tactics:tl) *)
-
   (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno
    * applicato la tattica *)
 
@@ -243,18 +200,6 @@ struct
    let rec repeat_tactic ~tactic status =
     info (lazy "in repeat_tactic");
     try
-(*      let rec step output_status opened closed =
-       match opened with
-       | [] -> output_status, [], closed
-       | head :: tail -> 
-           let status = S.focus head output_status in
-           let output_status' = repeat_tactic ~tactic status in
-           let opened', closed' = S.goals output_status' in
-           let output_status'', opened'', closed'' =
-             step output_status' tail []
-           in
-           output_status'', opened' @ opened'', closed' @ closed''
-     in *)
      let output_status = S.apply_tactic tactic status in
      let opened, closed = S.goals output_status in
      let output_status, opened', closed' =
@@ -279,16 +224,6 @@ struct
      try 
       let output_status = S.apply_tactic tactic status in
       let opened, closed = S.goals output_status in
-(*       let rec step output_status goallist =
-       match goallist with
-          [] -> output_status, []
-        | head::tail -> 
-           let status = S.focus head output_status in
-           let output_status' = do_tactic ~n:(n-1) ~tactic status in
-           let goallist' = S.goals output_status' in 
-           let (output_status'', goallist'') = step output_status' tail in
-            output_status'', goallist'@goallist''
-      in *)
        let output_status, opened', closed' =
          step (do_tactic ~n:(n-1) ~tactic) output_status opened closed
        in