- better naming

- uniform handling of empty stack assertion failure
- added Qed and init

diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml
index f5a7477204e7b6c7bcee9f9bd4f4d9f883f8e15b..0dc1b75238366a2e8ebda0f6d2c0f768d3050e58 100644 (file)
--- a/helm/ocaml/tactics/continuationals.ml
+++ b/helm/ocaml/tactics/continuationals.ml
@@ -35,7 +35,7 @@ sig
   type tactic
 
   val goal_of_conjecture: conjecture -> goal
-  val is_goal_in_metasenv: metasenv -> goal -> bool
+  val goal_mem: goal -> metasenv -> bool
 
   val apply_tactic:
     tactic -> metasenv -> goal ->
@@ -74,6 +74,7 @@ struct
     | Select of E.goal list
     | End_select
     | Tactical of tactical
+    | Qed
 
   let goal_of = function _, Open g -> g | _, Closed g -> g 
   let is_open = function _, Open _ -> true | _, Closed _ -> false 
@@ -94,6 +95,14 @@ struct
   let add_dummy_pos g = dummy_pos, g
   let map_dummy_pos = List.map add_dummy_pos
 
+  let map_open_pos =
+    let rec aux pos =
+      function
+      | [] -> []
+      | g :: tl -> (pos, Open g) :: aux (pos + 1) tl
+    in
+    aux 1
+
   let eval_tactical tactical metasenv switch =
     match tactical, switch with
     | Tactic tac, Open n -> E.apply_tactic tac metasenv n
@@ -101,8 +110,9 @@ struct
     | Tactic _, Closed _ -> raise (Error "can't apply tactic to a closed goal")
     | Skip, Open _ -> raise (Error "can't skip an open goal")
 
-  let eval continuational (status: status) = 
+  let eval continuational status =
     match continuational, status with
+    | _, (_, []) -> assert false
     | Tactical t, (metasenv, (env, todo, left)::tail) ->
         assert (L.length env > 1);
         let metasenv, opened, closed =
@@ -127,7 +137,6 @@ struct
          complementary opened left)
         :: stack_map
             (close closed) (complementary closed) (complementary opened) tail 
-    | Tactical _, (_, []) -> assert false
     | Semicolon, (metasenv, stack) -> metasenv, stack
     | Dot, (metasenv, (env, todo, left)::tail) ->
         let env, left = 
@@ -137,7 +146,6 @@ struct
           | [], g::left -> [dummy_pos, Open g], left
         in
         metasenv, (env, todo, left)::tail
-    | Dot, (_, []) -> assert false
     | Branch, (metasenv, (g1::tl, todo, left)::tail) ->
         assert (L.length tl >= 1);
         metasenv, ([g1], [], [])::(tl, todo, left)::tail
@@ -163,16 +171,21 @@ struct
               (union not_processed (L.filter is_open leftopen ))))
         in
         metasenv, (env,todo,left)::tail
-    | Merge, (_, [])
     | Merge, (_, [_]) -> raise (Error "can't merge here")
     | Select gl, (metasenv, stack) ->
         List.iter
-          (fun g -> if not (E.is_goal_in_metasenv metasenv g) then 
+          (fun g -> if not (E.goal_mem g metasenv) then 
             raise (Error "you can't select a closed goal")) gl;
         (metasenv, (open_all (map_dummy_pos gl),[],[])::stack)
     | End_select, (metasenv, stack) ->
         (match stack with 
         | ([], [], [])::tail -> metasenv, tail
         | _ -> raise (Error "select left some goals open"))
+    | Qed, (metasenv, [[], [], []]) -> status
+    | Qed, _ -> raise (Error "can't qed an unfinished proof")
+
+  let init metasenv =
+    metasenv,
+    [ map_open_pos (List.map E.goal_of_conjecture metasenv),  [], [] ]
 end
 

diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli
index 4b2632e56c232d77aa6126e1adfee6c789ef5084..bebea704561e44955650521708e9d2b254f34ac7 100644 (file)
--- a/helm/ocaml/tactics/continuationals.mli
+++ b/helm/ocaml/tactics/continuationals.mli
@@ -33,7 +33,7 @@ sig
   type tactic
 
   val goal_of_conjecture: conjecture -> goal
-  val is_goal_in_metasenv: metasenv -> goal -> bool
+  val goal_mem: goal -> metasenv -> bool
 
   val apply_tactic:
     tactic -> metasenv -> goal ->
@@ -54,13 +54,19 @@ sig
   type t =
     | Dot
     | Semicolon
+
     | Branch
     | Shift of int option
     | Merge
+
     | Select of E.goal list
     | End_select
+
     | Tactical of tactical
 
+    | Qed
+
   val eval: t -> status -> status
+  val init: E.metasenv -> status
 end