source: driver/extracted/iOMonad.mli @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 9.3 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
108val iORel : Monad.monadRel
109
110val pred_io_inject : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO
111
112val iOPred : Monad.injMonadPred
113
114val err_to_io : 'a3 Errors.res -> ('a1, 'a2, 'a3) iO
115
116val dpi1__o__err_to_io__o__inject :
117  ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO Types.sig0
118
119val eject__o__err_to_io__o__inject :
120  'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0
121
122val err_to_io__o__inject : 'a2 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0
123
124val dpi1__o__err_to_io :
125  ('a2 Errors.res, 'a3) Types.dPair -> ('a1, 'a4, 'a2) iO
126
127val eject__o__err_to_io : 'a2 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO
128
129val err_to_io_sig :
130  'a3 Types.sig0 Errors.res -> ('a1, 'a2, 'a3 Types.sig0) iO
131
132val io_inject_0 : ('a1, 'a2, 'a3) iO -> ('a1, 'a2, 'a3 Types.sig0) iO
133
134val io_inject :
135  ('a1, 'a2, 'a3) iO Types.option -> ('a1, 'a2, 'a3 Types.sig0) iO
136
137val io_eject : ('a1, 'a2, 'a3 Types.sig0) iO -> ('a1, 'a2, 'a3) iO
138
139val dpi1__o__io_inject__o__inject :
140  (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
141  Types.sig0) iO Types.sig0
142
143val eject__o__io_inject__o__inject :
144  ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0) iO
145  Types.sig0
146
147val io_inject__o__inject :
148  ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0
149
150val dpi1__o__io_inject :
151  (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2
152  Types.sig0) iO
153
154val eject__o__io_inject :
155  ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2 Types.sig0) iO
156
157val io_inject__o__io_eject__o__inject :
158  ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO Types.sig0
159
160val dpi1__o__err_to_io__o__io_eject__o__inject :
161  ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
162  Types.sig0
163
164val dpi1__o__io_inject__o__io_eject__o__inject :
165  (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
166  Types.sig0
167
168val eject__o__err_to_io__o__io_eject__o__inject :
169  'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0
170
171val eject__o__io_inject__o__io_eject__o__inject :
172  ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0
173
174val err_to_io__o__io_eject__o__inject :
175  'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO Types.sig0
176
177val dpi1__o__io_eject__o__inject :
178  (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
179  Types.sig0
180
181val eject__o__io_eject__o__inject :
182  ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO Types.sig0
183
184val io_eject__o__inject :
185  ('a1, 'a3, 'a2 Types.sig0) iO -> ('a1, 'a3, 'a2) iO Types.sig0
186
187val io_inject__o__io_eject :
188  ('a1, 'a3, 'a2) iO Types.option -> ('a1, 'a3, 'a2) iO
189
190val dpi1__o__err_to_io__o__io_eject :
191  ('a2 Types.sig0 Errors.res, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
192
193val dpi1__o__io_inject__o__io_eject :
194  (('a1, 'a3, 'a2) iO Types.option, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
195
196val eject__o__err_to_io__o__io_eject :
197  'a2 Types.sig0 Errors.res Types.sig0 -> ('a1, 'a3, 'a2) iO
198
199val eject__o__io_inject__o__io_eject :
200  ('a1, 'a3, 'a2) iO Types.option Types.sig0 -> ('a1, 'a3, 'a2) iO
201
202val err_to_io__o__io_eject : 'a2 Types.sig0 Errors.res -> ('a1, 'a3, 'a2) iO
203
204val dpi1__o__io_eject :
205  (('a1, 'a3, 'a2 Types.sig0) iO, 'a4) Types.dPair -> ('a1, 'a3, 'a2) iO
206
207val eject__o__io_eject :
208  ('a1, 'a3, 'a2 Types.sig0) iO Types.sig0 -> ('a1, 'a3, 'a2) iO
209
210val opt_to_io : Errors.errmsg -> 'a3 Types.option -> ('a1, 'a2, 'a3) iO
211
212val bind_res_value :
213  'a3 Errors.res -> ('a3 -> 'a4 Errors.res) -> 'a4 -> ('a3 -> __ -> __ ->
214  'a5) -> 'a5
215
216val bindIO_value :
217  ('a1, 'a2, 'a3) iO -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a4 -> ('a3 -> __ ->
218  __ -> 'a5) -> 'a5
219
220val bindIO_res_interact :
221  'a3 Errors.res -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 -> ('a2 -> ('a1, 'a2,
222  'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5
223
224val bindIO_opt_interact :
225  Errors.errmsg -> 'a3 Types.option -> ('a3 -> ('a1, 'a2, 'a4) iO) -> 'a1 ->
226  ('a2 -> ('a1, 'a2, 'a4) iO) -> ('a3 -> __ -> __ -> 'a5) -> 'a5
227
228val eq_to_rel_io__o__io_eq_from_res__o__inject :
229  'a2 Errors.res -> 'a2 -> __ Types.sig0
230
231val eq_to_rel_io__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
232  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
233
234val jmeq_to_eq__o__io_eq_from_res__o__inject :
235  'a2 Errors.res -> 'a2 -> __ Types.sig0
236
237val jmeq_to_eq__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
238  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
239
240val dpi1__o__io_eq_from_res__o__inject :
241  'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0
242
243val dpi1__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
244  Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
245  Types.sig0
246
247val eject__o__io_eq_from_res__o__inject :
248  'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0
249
250val eject__o__io_eq_from_res__o__opt_eq_from_res__o__inject :
251  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0
252
253val io_eq_from_res__o__opt_eq_from_res__o__inject :
254  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
255
256val io_eq_from_res__o__inject : 'a2 Errors.res -> 'a2 -> __ Types.sig0
257
258val jmeq_to_eq__o__io_monad_eq_from_res__o__inject :
259  'a2 Errors.res -> 'a2 -> __ Types.sig0
260
261val jmeq_to_eq__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
262  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
263
264val dpi1__o__io_monad_eq_from_res__o__inject :
265  'a2 Errors.res -> 'a2 -> (__, 'a4) Types.dPair -> __ Types.sig0
266
267val dpi1__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
268  Errors.errmsg -> 'a1 Types.option -> 'a1 -> (__, 'a4) Types.dPair -> __
269  Types.sig0
270
271val eject__o__io_monad_eq_from_res__o__inject :
272  'a2 Errors.res -> 'a2 -> __ Types.sig0 -> __ Types.sig0
273
274val eject__o__io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
275  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0 -> __ Types.sig0
276
277val io_monad_eq_from_res__o__opt_eq_from_res__o__inject :
278  Errors.errmsg -> 'a1 Types.option -> 'a1 -> __ Types.sig0
279
280val io_monad_eq_from_res__o__inject : 'a2 Errors.res -> 'a2 -> __ Types.sig0
281
282val eq_to_rel_io__o__io_eq_from_opt__o__inject :
283  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
284
285val jmeq_to_eq__o__io_eq_from_opt__o__inject :
286  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
287
288val dpi1__o__io_eq_from_opt__o__inject :
289  Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
290  Types.sig0
291
292val eject__o__io_eq_from_opt__o__inject :
293  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __ Types.sig0
294
295val io_eq_from_opt__o__inject :
296  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
297
298val jmeq_to_eq__o__io_monad_eq_from_opt__o__inject :
299  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
300
301val dpi1__o__io_monad_eq_from_opt__o__inject :
302  Errors.errmsg -> 'a2 Types.option -> 'a2 -> (__, 'a4) Types.dPair -> __
303  Types.sig0
304
305val eject__o__io_monad_eq_from_opt__o__inject :
306  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0 -> __ Types.sig0
307
308val io_monad_eq_from_opt__o__inject :
309  Errors.errmsg -> 'a2 Types.option -> 'a2 -> __ Types.sig0
310
Note: See TracBrowser for help on using the repository browser.