1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
26 exception Error of string Lazy.t
33 type parameters = (string * string) list
37 type switch = Open of goal | Closed of goal
38 type locator = int * switch
39 type tag = [ `BranchTag | `FocusTag | `NoTag ]
40 type entry = locator list * locator list * locator list * tag * parameters
45 val find_goal: t -> goal (** find "next" goal *)
46 val is_empty: t -> bool (** a singleton empty level *)
47 val of_nmetasenv: (goal * 'a) list -> t
48 val head_switches: t -> switch list (** top level switches *)
49 val head_goals: t -> goal list (** top level goals *)
50 val head_tag: t -> tag (** top level tag *)
51 val shift_goals: t -> goal list (** second level goals *)
52 val open_goals: t -> goal list (** all (Open) goals *)
53 val goal_of_switch: switch -> goal
54 val filter_open : (goal * switch) list -> (goal * switch) list
55 val is_open: goal * switch -> bool
56 val is_fresh: goal * switch -> bool
57 val init_pos: (goal * switch) list -> (goal * switch) list
58 val goal_of_loc: goal * switch -> goal
59 val switch_of_loc: goal * switch -> switch
60 val zero_pos : goal list -> (goal * switch) list
61 val deep_close: goal list -> t -> t
64 val ( @+ ) : 'a list -> 'a list -> 'a list
65 val ( @- ) : 'a list -> 'a list -> 'a list
66 val ( @~- ) : ('a * switch) list -> goal list -> ('a * switch) list
70 (** @param int depth, depth 0 is the top of the stack *)
72 env: ('a -> int -> tag -> locator -> 'a) ->
73 cont:('a -> int -> tag -> locator -> 'a) ->
74 todo:('a -> int -> tag -> locator -> 'a) ->
77 val iter: (** @param depth as above *)
78 env: (int -> tag -> locator -> unit) ->
79 cont:(int -> tag -> locator -> unit) ->
80 todo:(int -> tag -> locator -> unit) ->
83 val map: (** @param depth as above *)
84 env: (int -> tag -> locator list -> locator list) ->
85 cont:(int -> tag -> locator list -> locator list) ->
86 todo:(int -> tag -> locator list -> locator list) ->
92 (** {2 Functorial interface} *)
100 val mk_tactic : (input_status -> output_status) -> tactic
101 val apply_tactic : tactic -> input_status -> output_status
103 val goals : output_status -> goal list * goal list (** opened, closed goals *)
104 val get_stack : input_status -> Stack.t
105 val set_stack : Stack.t -> output_status -> output_status
107 val inject : input_status -> output_status
108 val focus : goal -> output_status -> input_status
134 | Tactical of tactical
136 val eval: t -> input_status -> output_status
139 module Make (S: Status) : C
140 with type tactic = S.tactic
141 and type input_status = S.input_status
142 and type output_status = S.output_status