X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fcontinuationals.mli;h=d40202d4b37e2a92f1ba878a0581fdbf50501bcb;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=109dbaf99790e71ee2682ead2547e218aa62aa28;hpb=8b55faddb06e3c4b0a13839210bb49170939b33e;p=helm.git

diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli
index 109dbaf99..d40202d4b 100644
--- a/helm/ocaml/tactics/continuationals.mli
+++ b/helm/ocaml/tactics/continuationals.mli
@@ -25,28 +25,80 @@
 
 exception Error of string Lazy.t
 
-module type Engine =
+type goal = ProofEngineTypes.goal
+
+(** {2 Goal stack} *)
+
+module Stack:
 sig
-  type goal
-  type proof
+  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 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 apply_tactic:
-    tactic -> proof -> goal ->
-      proof * goal list * goal list (** new proof, opened goals, closed goals *)
+  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 inject : input_status -> output_status
+  val focus : goal -> output_status -> input_status
 end
 
 module type C =
 sig
-  type goal
-  type proof
+  type input_status
+  type output_status
   type tactic
 
-  type status
-
   type tactical =
     | Tactic of tactic
     | Skip
@@ -56,28 +108,19 @@ sig
     | Semicolon
 
     | Branch
-    | Shift of int option
-    | Select of goal list
-    | End
+    | Shift
+    | Pos of int
+    | Merge
+    | Focus of goal list
+    | Unfocus
 
     | Tactical of tactical
 
-  val eval: t -> status -> 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
+  val eval: t -> input_status -> output_status
 end
 
-module Make (E:Engine) : C
-  with type goal = E.goal
-   and type proof = E.proof
-   and type tactic = E.tactic
+module Make (S: Status) : C
+  with type tactic = S.tactic
+   and type input_status = S.input_status
+   and type output_status = S.output_status