From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 10 Oct 2005 08:07:19 +0000 (+0000)
Subject: - added stack frame tagging
X-Git-Tag: V_0_7_2_3~228
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3337e1349c79b52dcadb2b072539ca0c881d70c9;p=helm.git

- added stack frame tagging
- unified "End" for Branch and Select
---

diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml
index 5f72547c2..5b1bbce3d 100644
--- a/helm/ocaml/tactics/continuationals.ml
+++ b/helm/ocaml/tactics/continuationals.ml
@@ -55,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.proof * ((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 =
@@ -71,11 +119,9 @@ 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 
@@ -93,7 +139,7 @@ struct
       | p, Open g when List.mem g to_close -> p, Closed g
       | g -> g)
 
-  let map_stack f g h = List.map (fun (a,b,c) -> f a, g b, h c)
+  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
@@ -117,7 +163,7 @@ struct
   let eval continuational status =
     match continuational, status with
     | _, (_, []) -> assert false
-    | Tactical t, (proof, (env, todo, left)::tail) ->
+    | Tactical t, (proof, (env, todo, left,tag)::tail) ->
         assert (List.length env > 1);
         let proof, opened, closed =
           List.fold_left 
@@ -138,23 +184,24 @@ struct
         proof, 
         (open_all stack_opened,
          complementary closed todo,
-         complementary opened left)
+         complementary opened left, tag)
         :: map_stack
             (close closed) (complementary closed) (complementary opened) tail 
     | Semicolon, (proof, stack) -> proof, stack
-    | Dot, (proof, (env, todo, left)::tail) ->
+    | Dot, (proof, (env, todo, left, tag)::tail) ->
         let 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
-        proof, (env, todo, left)::tail
-    | Branch, (proof, (g1::tl, todo, left)::tail) ->
+        proof, (env, todo, left, tag)::tail
+    | Branch, (proof, (g1::tl, todo, left, tag)::tail) ->
         assert (List.length tl >= 1);
-        proof, ([g1], [], [])::(tl, todo, left)::tail
+        proof, ([g1], [], [], BranchTag)::(tl, todo, left, tag)::tail
     | Branch, (_, _) -> fail "can't branch on a singleton context"
-    | Shift opt_pos, (proof, (leftopen, t, l)::(goals, todo, left)::tail) ->
+    | 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
@@ -167,32 +214,34 @@ struct
         let t =
           union t (union (List.map goal_of (List.filter is_open leftopen)) l)
         in
-        proof, ([next_goal], t, [])::(rem_goals, todo,left)::tail
+        proof, ([next_goal], t, [], BranchTag)::(rem_goals, todo,left,tag)::tail
     | Shift _, (_, _) -> fail "no more goals to shift"
-    | Merge, (proof, (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 (List.filter is_open leftopen))))
-        in
-        proof, (env,todo,left)::tail
-    | Merge, (_, [_]) -> fail "can't merge here"
     | Select gl, (proof, stack) ->
         List.iter
           (fun g ->
-            if not (E.is_goal_closed g proof) then
+            if E.is_goal_closed g proof then
               fail "you can't select a closed goal")
           gl;
-        (proof, (open_all (map_dummy_pos gl),[],[])::stack)
-    | End_select, (proof, stack) ->
+        (proof, (open_all (map_dummy_pos gl),[],[],SelectTag)::stack)
+    | End, (proof, stack) ->
         (match stack with 
-        | ([], [], [])::tail -> proof, tail
-        | _ -> fail "select left some goals open")
-    | Qed, (proof, [[], [], []]) -> status
-    | Qed, _ -> fail "can't qed an unfinished proof"
+        | ([], [], [], 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),  [], [] ]
+    [ map_open_pos (E.goals_of_proof proof),  [], [], NoTag ]
+
+  let is_completed =
+    function
+    | (_, [[],[],[],NoTag]) -> true
+    | _ -> false
 end
 
diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli
index 65a579b67..e89e2e51d 100644
--- a/helm/ocaml/tactics/continuationals.mli
+++ b/helm/ocaml/tactics/continuationals.mli
@@ -39,15 +39,16 @@ sig
       proof * goal list * goal list (** new proof, opened goals, closed goals *)
 end
 
-module Make (E:Engine) :
+module type C =
 sig
-  type goal_switch = Open of E.goal | Closed of E.goal
-  type 'a stack = 'a list
-  type status =
-    E.proof * ((int * goal_switch) list * E.goal list * E.goal list) stack
+  type goal
+  type proof
+  type tactic
+
+  type status
 
   type tactical =
-    | Tactic of E.tactic
+    | Tactic of tactic
     | Skip
 
   type t =
@@ -56,16 +57,27 @@ sig
 
     | Branch
     | Shift of int option
-    | Merge
-
-    | Select of E.goal list
-    | End_select
+    | Select of goal list
+    | End
 
     | Tactical of tactical
 
-    | Qed
-
   val eval: t -> status -> status
-  val init: E.proof -> status
+  val init: proof -> status
+
+  (** {2 Status accessors} *)
+
+  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) : C
+  with type goal = E.goal
+   and type proof = E.proof
+   and type tactic = E.tactic
+