* 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
+