source: extracted/iOMonad.mli @ 2755

Last change on this file since 2755 was 2743, checked in by sacerdot, 7 years ago

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 9.4 KB
Line 
1open Preamble
2
3open Div_and_mod
4
5open Jmeq
6
7open Russell
8
9open Util
10
11open Bool
12
13open Relations
14
15open Nat
16
17open List
18
19open Hints_declaration
20
21open Core_notation
22
23open Pts
24
25open Logic
26
27open Types
28
29open Extralib
30
31open ErrorMessages
32
33open Option
34
35open Setoids
36
37open Monad
38
39open Positive
40
41open PreIdentifiers
42
43open Errors
44
45type ('output, 'input, 't) iO =
46| Interact of 'output * ('input -> ('output, 'input, 't) iO)
47| Value of 't
48| Wrong of Errors.errmsg
49
50val iO_rect_Type4 :
51  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
52  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
53
54val iO_rect_Type3 :
55  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
56  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
57
58val iO_rect_Type2 :
59  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
60  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
61
62val iO_rect_Type1 :
63  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
64  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
65
66val iO_rect_Type0 :
67  ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> 'a4) -> 'a4) -> ('a3 -> 'a4)
68  -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4
69
70val iO_inv_rect_Type4 :
71  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
72  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
73  'a4
74
75val iO_inv_rect_Type3 :
76  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
77  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
78  'a4
79
80val iO_inv_rect_Type2 :
81  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
82  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
83  'a4
84
85val iO_inv_rect_Type1 :
86  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
87  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
88  'a4
89
90val iO_inv_rect_Type0 :
91  ('a1, 'a2, 'a3) iO -> ('a1 -> ('a2 -> ('a1, 'a2, 'a3) iO) -> ('a2 -> __ ->
92  'a4) -> __ -> 'a4) -> ('a3 -> __ -> 'a4) -> (Errors.errmsg -> __ -> 'a4) ->
93  'a4
94
95val iO_discr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __
96
97val iO_jmdiscr : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3) iO -> __
98
99open Proper
100
101val bindIO :
102  ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> ('a1, 'a2, 'a4) iO
103
104val iOMonad : Monad.monadProps
105
106val bindIO2 : __ -> ('a3 -> 'a4 -> __) -> __
107
108type ('a,'b,'c,'d) rel_io = __
109
110val iORel : Monad.monadRel
111
112type ('a,'b,'c) pred_io = __
113
114val pred_io_inject : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO
115
116val iOPred : Monad.injMonadPred
117
118val err_to_io : 'a3 Errors.res -> ('a1, 'a2, 'a3) iO
119
120val dpi1__o__err_to_io__o__inject :
121  ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO Types.sig0
122
123val eject__o__err_to_io__o__inject :
124  'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0
125
126val err_to_io__o__inject : 'a2 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0
127
128val dpi1__o__err_to_io :
129  ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO
130
131val eject__o__err_to_io : 'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO
132
133val err_to_io_sig :
134  'a3 Types.sig0 Errors.res -> ('a1, 'a2, 'a3 Types.sig0) iO
135
136type ('a,'b,'c) p_io = __
137
138type ('a,'b,'c) p_io' = __
139
140val io_inject_0 : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO
141
142val io_inject :
143  ('a1, 'a2, 'a3) iO Types.option -> ('a1, 'a2, 'a3 Types.sig0) iO
144
145val io_eject : ('a1, 'a2, 'a3 Types.sig0) iO -> ('a1, 'a2, 'a3) iO
146
147val dpi1__o__io_inject__o__inject :
148  (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
149  Types.sig0) iO Types.sig0
150
151val eject__o__io_inject__o__inject :
152  ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0) iO
153  Types.sig0
154
155val io_inject__o__inject :
156  ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0
157
158val dpi1__o__io_inject :
159  (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
160  Types.sig0) iO
161
162val eject__o__io_inject :
163  ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0) iO
164
165val io_inject__o__io_eject__o__inject :
166  ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO Types.sig0
167
168val dpi1__o__err_to_io__o__io_eject__o__inject :
169  ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
170  Types.sig0
171
172val dpi1__o__io_inject__o__io_eject__o__inject :
173  (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
174  Types.sig0
175
176val eject__o__err_to_io__o__io_eject__o__inject :
177  'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0
178
179val eject__o__io_inject__o__io_eject__o__inject :
180  ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0
181
182val err_to_io__o__io_eject__o__inject :
183  'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0
184
185val dpi1__o__io_eject__o__inject :
186  (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
187  Types.sig0
188
189val eject__o__io_eject__o__inject :
190  ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0
191
192val io_eject__o__inject :
193  ('a1, 'a3, 'a2 Types.sig0) iO -> ('a1, 'a3, 'a2) iO Types.sig0
194
195val io_inject__o__io_eject :
196  ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO
197
198val dpi1__o__err_to_io__o__io_eject :
199  ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
200
201val dpi1__o__io_inject__o__io_eject :
202  (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
203
204val eject__o__err_to_io__o__io_eject :
205  'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO
206
207val eject__o__io_inject__o__io_eject :
208  ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO
209
210val err_to_io__o__io_eject : 'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO
211
212val dpi1__o__io_eject :
213  (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
214
215val eject__o__io_eject :
216  ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO
217
218val opt_to_io : Errors.errmsg -> 'a3 Types.option -> ('a1, 'a2, 'a3) iO
219
220val bind_res_value :
221  'a3 Errors.res -> ('a3 -> 'a4 Errors.res) -> 'a4 -> ('a3 -> __ -> __ ->
222  'a5) -> 'a5
223
224val bindIO_value :
225  ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a4 -> ('a3 -> __ ->
226  __ -> 'a5) -> 'a5
227
228val bindIO_res_interact :
229  'a3 Errors.res -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 -> ('a2 -> ('a1, 'a2,
230  'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5
231
232val bindIO_opt_interact :
233  Errors.errmsg -> 'a3 Types.option -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 ->
234  ('a2 -> ('a1, 'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5
235
236val eq_to_rel_io__o__io_eq_from_res__o__inject :
237  'a2 Errors.res -> 'a2 -> __ Types.sig0
238
239val eq_to_rel_io__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
240  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
241
242val jmeq_to_eq__o__io_eq_from_res__o__inject :
243  'a2 Errors.res -> 'a2 -> __ Types.sig0
244
245val jmeq_to_eq__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
246  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
247
248val dpi1__o__io_eq_from_res__o__inject :
249  'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0
250
251val dpi1__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
252  Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
253  Types.sig0
254
255val eject__o__io_eq_from_res__o__inject :
256  'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0
257
258val eject__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
259  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0
260
261val io_eq_from_res__o__opt_eq_from_res__o__inject :
262  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
263
264val io_eq_from_res__o__inject : 'a2 Errors.res -> 'a2 -> __ Types.sig0
265
266val jmeq_to_eq__o__io_monad_eq_from_res__o__inject :
267  'a2 Errors.res -> 'a2 -> __ Types.sig0
268
269val jmeq_to_eq__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
270  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
271
272val dpi1__o__io_monad_eq_from_res__o__inject :
273  'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0
274
275val dpi1__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
276  Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
277  Types.sig0
278
279val eject__o__io_monad_eq_from_res__o__inject :
280  'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0
281
282val eject__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
283  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0
284
285val io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
286  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
287
288val io_monad_eq_from_res__o__inject : 'a2 Errors.res -> 'a2 -> __ Types.sig0
289
290val eq_to_rel_io__o__io_eq_from_opt__o__inject :
291  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
292
293val jmeq_to_eq__o__io_eq_from_opt__o__inject :
294  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
295
296val dpi1__o__io_eq_from_opt__o__inject :
297  Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
298  Types.sig0
299
300val eject__o__io_eq_from_opt__o__inject :
301  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __ Types.sig0
302
303val io_eq_from_opt__o__inject :
304  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
305
306val jmeq_to_eq__o__io_monad_eq_from_opt__o__inject :
307  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
308
309val dpi1__o__io_monad_eq_from_opt__o__inject :
310  Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
311  Types.sig0
312
313val eject__o__io_monad_eq_from_opt__o__inject :
314  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __ Types.sig0
315
316val io_monad_eq_from_opt__o__inject :
317  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
318
Note: See TracBrowser for help on using the repository browser.