]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/ng_tactics/continuationals.mli
Fixed indentation, which is semantic in Haskell.
[helm.git] / matitaB / components / ng_tactics / continuationals.mli
1 (* Copyright (C) 2005, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 exception Error of string Lazy.t
27
28 type goal = int
29
30 (** {2 Goal stack} *)
31
32 module Stack:
33 sig
34   type switch = Open of goal | Closed of goal
35   type locator = int * switch
36   type tag = [ `BranchTag | `FocusTag | `NoTag ]
37   type entry = locator list * locator list * locator list * tag
38   type t = entry list
39
40   val empty: t
41
42   val find_goal: t -> goal            (** find "next" goal *)
43   val is_empty: t -> bool             (** a singleton empty level *)
44   val of_nmetasenv: (goal * 'a) list -> t
45   val head_switches: t -> switch list (** top level switches *)
46   val head_goals: t -> goal list      (** top level goals *)
47   val head_tag: t -> tag              (** top level tag *)
48   val shift_goals: t -> goal list     (** second level goals *)
49   val open_goals: t -> goal list      (** all (Open) goals *)
50   val goal_of_switch: switch -> goal
51   val filter_open : (goal * switch) list -> (goal * switch) list
52   val is_open: goal * switch -> bool
53   val is_fresh: goal * switch -> bool
54   val init_pos: (goal * switch) list -> (goal * switch) list 
55   val goal_of_loc: goal * switch -> goal
56   val switch_of_loc: goal * switch -> switch
57   val zero_pos : goal list -> (goal * switch) list
58   val deep_close: goal list -> t -> t
59
60
61   val ( @+ ) : 'a list -> 'a list -> 'a list
62   val ( @- ) : 'a list -> 'a list -> 'a list
63   val ( @~- ) : ('a * switch) list -> goal list -> ('a * switch) list
64
65
66
67   (** @param int depth, depth 0 is the top of the stack *)
68   val fold:
69     env: ('a -> int -> tag -> locator -> 'a) ->
70     cont:('a -> int -> tag -> locator -> 'a) ->
71     todo:('a -> int -> tag -> locator -> 'a) ->
72       'a  -> t -> 'a
73
74   val iter: (** @param depth as above *)
75     env: (int -> tag -> locator -> unit) ->
76     cont:(int -> tag -> locator -> unit) ->
77     todo:(int -> tag -> locator -> unit) ->
78       t -> unit
79
80   val map:  (** @param depth as above *)
81     env: (int -> tag -> locator list -> locator list) ->
82     cont:(int -> tag -> locator list -> locator list) ->
83     todo:(int -> tag -> locator list -> locator list) ->
84       t -> t
85
86   val pp: t -> string
87 end
88
89 (** {2 Functorial interface} *)
90
91 module type Status =
92 sig
93   type input_status
94   type output_status
95
96   type tactic
97   val mk_tactic : (input_status -> output_status) -> tactic
98   val apply_tactic : tactic -> input_status -> output_status
99
100   val goals : output_status -> goal list * goal list (** opened, closed goals *)
101   val get_stack : input_status -> Stack.t
102   val set_stack : Stack.t -> output_status -> output_status
103
104   val inject : input_status -> output_status
105   val focus : goal -> output_status -> input_status
106 end
107
108 module type C =
109 sig
110   type input_status
111   type output_status
112   type tactic
113
114   type tactical =
115     | Tactic of tactic
116     | Skip
117
118   type t =
119     | Dot
120     | Semicolon
121
122     | Branch
123     | Shift
124     | Pos of int list
125     | Wildcard
126     | Merge
127
128     | Focus of goal list
129     | Unfocus
130
131     | Tactical of tactical
132
133   val eval: t -> input_status -> output_status
134 end
135
136 module Make (S: Status) : C
137   with type tactic = S.tactic
138    and type input_status = S.input_status
139    and type output_status = S.output_status
140