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