ocaml 3.09 transition

[helm.git] / helm / ocaml / tactics / continuationals.mli

diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli
index 4b2632e56c232d77aa6126e1adfee6c789ef5084..d40202d4b37e2a92f1ba878a0581fdbf50501bcb 100644 (file)
--- a/helm/ocaml/tactics/continuationals.mli
+++ b/helm/ocaml/tactics/continuationals.mli
@@ -23,44 +23,104 @@
  * 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 conjecture
-  type metasenv = conjecture list
+  type input_status
+  type output_status
+
   type tactic
 
-  val goal_of_conjecture: conjecture -> goal
-  val is_goal_in_metasenv: metasenv -> goal -> bool
+  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 -> metasenv -> goal ->
-      metasenv * goal list * goal list
+  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.metasenv * ((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 =
     | Dot
     | 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
 
-  val eval: t -> status -> 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
+