ocaml 3.09 transition

[helm.git] / helm / ocaml / tactics / continuationals.ml

diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml
index 345502d5b766ed828e383e8dbbc8bebff9622099..fd965dddd62a6b7886a092ba8c63431c3d89819c 100644 (file)
--- 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
@@ -37,11 +37,11 @@ module Stack =
 struct
   type switch = Open of goal | Closed of goal
   type locator = int * switch
-  type tag = BranchTag | FocusTag | NoTag
+  type tag = [ `BranchTag | `FocusTag | `NoTag ]
   type entry = locator list * locator list * locator list * tag
   type t = entry list
 
-  let empty = [ [], [], [], NoTag ]
+  let empty = [ [], [], [], `NoTag ]
 
   let fold ~env ~cont ~todo init stack =
     let rec aux acc depth =
@@ -108,12 +108,12 @@ struct
   let is_empty =
     function
     | [] -> assert false
-    | [ [], [], [], NoTag ] -> true
+    | [ [], [], [], `NoTag ] -> true
     | _ -> false
 
   let of_metasenv metasenv =
     let goals = List.map (fun (g, _, _) -> g) metasenv in
-    [ zero_pos goals, [], [], NoTag ]
+    [ zero_pos goals, [], [], `NoTag ]
 
   let head_switches =
     function
@@ -159,7 +159,7 @@ struct
     in
     let pp_loc (i, s) = string_of_int i ^ pp_switch s in
     let pp_env env = sprintf "[%s]" (String.concat ";" (List.map pp_loc env)) in
-    let pp_tag = function BranchTag -> "B" | FocusTag -> "F" | NoTag -> "N" in
+    let pp_tag = function `BranchTag -> "B" | `FocusTag -> "F" | `NoTag -> "N" in
     let pp_stack_entry (env, todo, cont, tag) =
       sprintf "(%s, %s, %s, %s)" (pp_env env) (pp_env todo) (pp_env cont)
         (pp_tag tag)
@@ -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
@@ -309,28 +310,28 @@ struct
           | [] | [ _ ] -> fail (lazy "too few goals to branch");
           | loc :: loc_tl ->
               new_stack
-                (([ loc ], [], [], BranchTag) :: (loc_tl, t, k, tag) :: s))
-      | Shift, (g, t, k, BranchTag) :: (g', t', k', tag) :: s ->
+                (([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s))
+      | Shift, (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
           (match g' with
           | [] -> fail (lazy "no more goals to shift")
           | loc :: loc_tl ->
               new_stack
-                (([ loc ], t @+ filter_open g, [], BranchTag)
+                (([ loc ], t @+ filter_open g, [],`BranchTag)
                 :: (loc_tl, t', k', tag) :: s))
       | Shift, _ -> fail (lazy "can't shift goals here")
-      | Pos i, ([ loc ], [], [], BranchTag) :: (g', t', k', tag) :: s
+      | Pos i, ([ loc ], [], [],`BranchTag) :: (g', t', k', tag) :: s
         when is_fresh loc ->
           let loc_i, g' = extract_pos i g' in
           new_stack
-            (([ loc_i ], [], [], BranchTag)
+            (([ loc_i ], [], [],`BranchTag)
              :: ([ loc ] @+ g', t', k', tag) :: s)
-      | Pos i, (g, t, k, BranchTag) :: (g', t', k', tag) :: s ->
+      | Pos i, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
           let loc_i, g' = extract_pos i g' in
           new_stack
-            (([ loc_i ], [], [], BranchTag)
+            (([ loc_i ], [], [],`BranchTag)
              :: (g', t' @+ filter_open g, k', tag) :: s)
       | Pos _, _ -> fail (lazy "can't use relative positioning here")
-      | Merge, (g, t, k, BranchTag) :: (g', t', k', tag) :: s ->
+      | Merge, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
           new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
       | Merge, _ -> fail (lazy "can't merge goals here")
       | Focus [], _ -> assert false
@@ -344,8 +345,8 @@ struct
               if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
                 fail (lazy (sprintf "goal %d not found (or closed)" g)))
             gs;
-          new_stack ((zero_pos gs, [], [], FocusTag) :: deep_close gs s)
-      | Unfocus, ([], [], [], FocusTag) :: s -> new_stack s
+          new_stack ((zero_pos gs, [], [], `FocusTag) :: deep_close gs s)
+      | Unfocus, ([], [], [], `FocusTag) :: s -> new_stack s
       | Unfocus, _ -> fail (lazy "can't unfocus, some goals are still open")
     in
     debug_print (lazy (sprintf "EVAL CONT %s -> %s" (pp_t cmd) (pp stack)));