X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fcontinuationals.mli;h=d40202d4b37e2a92f1ba878a0581fdbf50501bcb;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=65a579b67792d608c548ae9d602d97689878e8d5;hpb=8508b9dd5fa37b169b36e8143df8bf5e9206b127;p=helm.git

diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli
index 65a579b67..d40202d4b 100644
--- a/helm/ocaml/tactics/continuationals.mli
+++ b/helm/ocaml/tactics/continuationals.mli
@@ -23,31 +23,84 @@
  * http://helm.cs.unibo.it/
  *)
 
-exception Error of string
+exception Error of string Lazy.t
 
-module type Engine =
+type goal = ProofEngineTypes.goal
+
+(** {2 Goal stack} *)
+
+module Stack:
+sig
+  type switch = Open of goal | Closed of goal
+  type locator = int * switch
+  type tag = [ `BranchTag | `FocusTag | `NoTag ]
+  type entry = locator list * locator list * locator list * tag
+  type t = entry list
+
+  val empty: t
+
+  val find_goal: t -> goal            (** find "next" goal *)
+  val is_empty: t -> bool             (** a singleton empty level *)
+  val of_metasenv: Cic.metasenv -> t
+  val head_switches: t -> switch list (** top level switches *)
+  val head_goals: t -> goal list      (** top level goals *)
+  val head_tag: t -> tag              (** top level tag *)
+  val shift_goals: t -> goal list     (** second level goals *)
+  val open_goals: t -> goal list      (** all (Open) goals *)
+  val goal_of_switch: switch -> goal
+
+  (** @param int depth, depth 0 is the top of the stack *)
+  val fold:
+    env: ('a -> int -> tag -> locator -> 'a) ->
+    cont:('a -> int -> tag -> locator -> 'a) ->
+    todo:('a -> int -> tag -> locator -> 'a) ->
+      'a  -> t -> 'a
+
+  val iter: (** @param depth as above *)
+    env: (int -> tag -> locator -> unit) ->
+    cont:(int -> tag -> locator -> unit) ->
+    todo:(int -> tag -> locator -> unit) ->
+      t -> unit
+
+  val map:  (** @param depth as above *)
+    env: (int -> tag -> locator list -> locator list) ->
+    cont:(int -> tag -> locator list -> locator list) ->
+    todo:(int -> tag -> locator list -> locator list) ->
+      t -> t
+
+  val pp: t -> string
+end
+
+(** {2 Functorial interface} *)
+
+module type Status =
 sig
-  type goal
-  type proof
+  type input_status
+  type output_status
+
   type tactic
 
-  val is_goal_closed: goal -> proof -> bool
-  val goals_of_proof: proof -> goal list
+  val id_tactic : tactic
+  val mk_tactic : (input_status -> output_status) -> tactic
+  val apply_tactic : tactic -> input_status -> output_status
+
+  val goals : output_status -> goal list * goal list (** opened, closed goals *)
+  val set_goals: goal list * goal list -> output_status -> output_status
+  val get_stack : input_status -> Stack.t
+  val set_stack : Stack.t -> output_status -> output_status
 
-  val apply_tactic:
-    tactic -> proof -> goal ->
-      proof * goal list * goal list (** new proof, opened goals, closed goals *)
+  val inject : input_status -> output_status
+  val focus : goal -> output_status -> input_status
 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 input_status
+  type output_status
+  type tactic
 
   type tactical =
-    | Tactic of E.tactic
+    | Tactic of tactic
     | Skip
 
   type t =
@@ -55,17 +108,19 @@ sig
     | Semicolon
 
     | Branch
-    | Shift of int option
+    | Shift
+    | Pos of int
     | Merge
-
-    | Select of E.goal list
-    | End_select
+    | Focus of goal list
+    | Unfocus
 
     | Tactical of tactical
 
-    | Qed
-
-  val eval: t -> status -> status
-  val init: E.proof -> status
+  val eval: t -> input_status -> output_status
 end
 
+module Make (S: Status) : C
+  with type tactic = S.tactic
+   and type input_status = S.input_status
+   and type output_status = S.output_status
+