X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fcontinuationals.ml;h=5b1bbce3daf9850c4c1a41ff284dab396d3a5b93;hb=0245778d76e4d7656c1d8a05dc19738f1a953d68;hp=0dc1b75238366a2e8ebda0f6d2c0f768d3050e58;hpb=99db482ebae3e3e4dcc6c4df12027a81bb7a7f76;p=helm.git

diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml
index 0dc1b7523..5b1bbce3d 100644
--- a/helm/ocaml/tactics/continuationals.ml
+++ b/helm/ocaml/tactics/continuationals.ml
@@ -23,23 +23,24 @@
  * http://helm.cs.unibo.it/
  *)
 
+open Printf
+
 exception Error of string 
 
-module L = List
+let fail msg = raise (Error msg)
 
 module type Engine =
 sig
   type goal
-  type conjecture
-  type metasenv = conjecture list
+  type proof
   type tactic
 
-  val goal_of_conjecture: conjecture -> goal
-  val goal_mem: goal -> metasenv -> bool
+  val is_goal_closed: goal -> proof -> bool
+  val goals_of_proof: proof -> goal list
 
   val apply_tactic:
-    tactic -> metasenv -> goal ->
-      metasenv * goal list * goal list
+    tactic -> proof -> goal ->
+      proof * goal list * goal list
 end
 
 (** like List.assoc returning a pair: binding matching the given key,
@@ -54,15 +55,63 @@ let list_assoc_extract key =
   in
   aux []
 
+module type C =
+sig
+  type goal
+  type proof
+  type tactic
+
+  type status
+
+  type tactical =
+    | Tactic of tactic
+    | Skip
+
+  type t =
+    | Dot
+    | Semicolon
+
+    | Branch
+    | Shift of int option
+    | Select of goal list
+    | End
+
+    | Tactical of tactical
+
+  val eval: t -> status -> status
+  val init: proof -> status
+
+  val get_proof: status -> proof
+  val set_proof: proof -> status -> status
+
+  type goal_switch = Open of goal | Closed of goal
+  val get_goals: status -> goal_switch list
+
+  val is_completed: status -> bool
+end
+
 module Make (E:Engine) =
 struct
-  type goal_switch = Open of E.goal | Closed of E.goal
+  type goal = E.goal
+  type proof = E.proof
+  type tactic = E.tactic
+
+  type goal_switch = Open of goal | Closed of goal
   type 'a stack = 'a list
-  type status =
-    E.metasenv * ((int * goal_switch) list * E.goal list * E.goal list) stack
+  type stack_tag = BranchTag | SelectTag | NoTag
+  type stack_entry = 
+    (int * goal_switch) list * goal list * goal list * stack_tag
+  type status = proof * stack_entry stack
+
+  let get_proof = fst
+  let set_proof p (_, s) = p, s
+  let get_goals (_, stack) =
+    match stack with
+    | (goals, _, _, _) :: _ -> List.map snd goals
+    | [] -> assert false
 
   type tactical =
-    | Tactic of E.tactic
+    | Tactic of tactic
     | Skip
 
   type t =
@@ -70,26 +119,27 @@ struct
     | Semicolon
     | Branch
     | Shift of int option
-    | Merge
-    | Select of E.goal list
-    | End_select
+    | Select of goal list
+    | End
     | Tactical of tactical
-    | Qed
 
   let goal_of = function _, Open g -> g | _, Closed g -> g 
   let is_open = function _, Open _ -> true | _, Closed _ -> false 
-  let open_all = L.map (fun p, g -> p, Open g)
+  let open_all = List.map (fun p, g -> p, Open g)
     
   let union a b = a @ b
   
   let complementary part full = (* not really efficient *)
-    L.fold_left (fun acc g -> if L.mem g part then acc else g::acc) full []
+    List.fold_left (fun acc g -> if List.mem g part then acc else g::acc)
+      full []
 
-  let close to_close l =
-    L.map (function p, Open g when L.mem g to_close -> p, Closed g | g -> g) l
+  let close to_close =
+    List.map
+      (function
+      | p, Open g when List.mem g to_close -> p, Closed g
+      | g -> g)
 
-  let stack_map f g h stack =
-    L.map (fun (a,b,c) -> f a, g b, h c) stack
+  let map_stack f g h = List.map (fun (a,b,c,tag) -> f a, g b, h c, tag)
 
   let dummy_pos = ~-1
   let add_dummy_pos g = dummy_pos, g
@@ -103,89 +153,95 @@ struct
     in
     aux 1
 
-  let eval_tactical tactical metasenv switch =
+  let eval_tactical tactical proof switch =
     match tactical, switch with
-    | Tactic tac, Open n -> E.apply_tactic tac metasenv n
-    | Skip, Closed n -> metasenv, [], [n]
-    | Tactic _, Closed _ -> raise (Error "can't apply tactic to a closed goal")
-    | Skip, Open _ -> raise (Error "can't skip an open goal")
+    | Tactic tac, Open n -> E.apply_tactic tac proof n
+    | Skip, Closed n -> proof, [], [n]
+    | Tactic _, Closed _ -> fail "can't apply tactic to a closed goal"
+    | Skip, Open _ -> fail "can't skip an open goal"
 
   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 =
-          L.fold_left 
-            (fun (metasenv, opened, closed) cur_goal ->
-              if L.exists ((=) (goal_of cur_goal)) closed then
-                metasenv, opened, closed 
+    | Tactical t, (proof, (env, todo, left,tag)::tail) ->
+        assert (List.length env > 1);
+        let proof, opened, closed =
+          List.fold_left 
+            (fun (proof, opened, closed) cur_goal ->
+              if List.exists ((=) (goal_of cur_goal)) closed then
+                proof, opened, closed 
               else
-                let metasenv, newopened, newclosed = 
-                  eval_tactical t metasenv (snd cur_goal)
+                let proof, newopened, newclosed = 
+                  eval_tactical t proof (snd cur_goal)
                 in
-                metasenv, 
+                proof, 
                 union (complementary newclosed opened) newopened,
                 union closed newclosed
-            ) (metasenv, [],[]) env
+            ) (proof, [],[]) env
         in
         let pos = ref 0 in
         let stack_opened = List.map (fun g -> incr pos; !pos, g) opened in
-        metasenv, 
+        proof, 
         (open_all stack_opened,
          complementary closed todo,
-         complementary opened left)
-        :: stack_map
+         complementary opened left, tag)
+        :: map_stack
             (close closed) (complementary closed) (complementary opened) tail 
-    | Semicolon, (metasenv, stack) -> metasenv, stack
-    | Dot, (metasenv, (env, todo, left)::tail) ->
+    | Semicolon, (proof, stack) -> proof, stack
+    | Dot, (proof, (env, todo, left, tag)::tail) ->
         let env, left = 
-          match L.filter is_open env, left with 
-          | [], [] -> raise (Error "There is nothig to do for '.'")
-          | g::env,left -> [g], union (L.map goal_of env) left
+          match List.filter is_open env, left with 
+          | [], [] -> fail "There is nothig to do for '.'"
+          | g::env,left -> [g], union (List.map goal_of env) left
           | [], g::left -> [dummy_pos, Open g], left
         in
-        metasenv, (env, todo, left)::tail
-    | Branch, (metasenv, (g1::tl, todo, left)::tail) ->
-        assert (L.length tl >= 1);
-        metasenv, ([g1], [], [])::(tl, todo, left)::tail
-    | Branch, (_, _) -> raise (Error "can't branch on a singleton context")
-    | Shift opt_pos, (metasenv, (leftopen, t, l)::(goals, todo, left)::tail) ->
+        proof, (env, todo, left, tag)::tail
+    | Branch, (proof, (g1::tl, todo, left, tag)::tail) ->
+        assert (List.length tl >= 1);
+        proof, ([g1], [], [], BranchTag)::(tl, todo, left, tag)::tail
+    | Branch, (_, _) -> fail "can't branch on a singleton context"
+    | Shift opt_pos, (proof, (leftopen, t, l,BranchTag)::
+                             (goals, todo, left,tag)::tail) ->
         let next_goal, rem_goals =
           match opt_pos, goals with
           | None, g1 :: tl -> g1, tl
           | Some pos, _ ->
               (try
                 list_assoc_extract pos goals
-              with Not_found ->
-                raise (Error (Printf.sprintf "position %d not found" pos)))
-          | None, [] -> raise (Error "no more goals to shift")
+              with Not_found -> fail (sprintf "position %d not found" pos))
+          | None, [] -> fail "no more goals to shift"
         in
-        let t = union t (union (L.map goal_of (L.filter is_open leftopen)) l) in
-        metasenv, ([next_goal], t, [])::(rem_goals, todo,left)::tail
-    | Shift _, (_, _) -> raise (Error "no more goals to shift")
-    | Merge, (metasenv, (leftopen,t,l)::(not_processed,todo,left)::tail) -> 
-        let env = 
-          (union (open_all (map_dummy_pos t))
-            (union (open_all (map_dummy_pos l))
-              (union not_processed (L.filter is_open leftopen ))))
+        let t =
+          union t (union (List.map goal_of (List.filter is_open leftopen)) l)
         in
-        metasenv, (env,todo,left)::tail
-    | Merge, (_, [_]) -> raise (Error "can't merge here")
-    | Select gl, (metasenv, stack) ->
+        proof, ([next_goal], t, [], BranchTag)::(rem_goals, todo,left,tag)::tail
+    | Shift _, (_, _) -> fail "no more goals to shift"
+    | Select gl, (proof, stack) ->
         List.iter
-          (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) ->
+          (fun g ->
+            if E.is_goal_closed g proof then
+              fail "you can't select a closed goal")
+          gl;
+        (proof, (open_all (map_dummy_pos gl),[],[],SelectTag)::stack)
+    | End, (proof, 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),  [], [] ]
+        | ([], [], [], SelectTag)::tail -> proof, tail
+        | (leftopen,t,l,BranchTag)::(not_processed,todo,left,tag)::tail ->
+            let env = 
+              (union (open_all (map_dummy_pos t))
+                (union (open_all (map_dummy_pos l))
+                  (union not_processed (List.filter is_open leftopen))))
+            in
+            proof, (env,todo,left,tag)::tail
+        | _ -> fail "can't end here")
+
+  let init proof =
+    proof,
+    [ map_open_pos (E.goals_of_proof proof),  [], [], NoTag ]
+
+  let is_completed =
+    function
+    | (_, [[],[],[],NoTag]) -> true
+    | _ -> false
 end