source: driver/extracted/monad.mli @ 3106

Last change on this file since 3106 was 2775, checked in by sacerdot, 7 years ago

The compiler now computes also the stack cost model.
File size: 9.5 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Relations
14
15open Setoids
16
17type ('a, 'b) pred_transformer = __
18
19type ('a, 'b, 'c, 'd) rel_transformer = __
20
21type monad = { m_return : (__ -> __ -> __);
22               m_bind : (__ -> __ -> __ -> (__ -> __) -> __) }
23
24val monad_rect_Type4 :
25  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
26  monad -> 'a1
27
28val monad_rect_Type5 :
29  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
30  monad -> 'a1
31
32val monad_rect_Type3 :
33  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
34  monad -> 'a1
35
36val monad_rect_Type2 :
37  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
38  monad -> 'a1
39
40val monad_rect_Type1 :
41  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
42  monad -> 'a1
43
44val monad_rect_Type0 :
45  (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1) ->
46  monad -> 'a1
47
48type 'x_772 monad0
49
50val m_return0 : monad -> 'a1 -> __
51
52val m_bind0 : monad -> __ -> ('a1 -> __) -> __
53
54val monad_inv_rect_Type4 :
55  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
56  __ -> 'a1) -> 'a1
57
58val monad_inv_rect_Type3 :
59  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
60  __ -> 'a1) -> 'a1
61
62val monad_inv_rect_Type2 :
63  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
64  __ -> 'a1) -> 'a1
65
66val monad_inv_rect_Type1 :
67  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
68  __ -> 'a1) -> 'a1
69
70val monad_inv_rect_Type0 :
71  monad -> (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) ->
72  __ -> 'a1) -> 'a1
73
74type monadProps =
75  monad
76  (* singleton inductive, whose constructor was mk_MonadProps *)
77
78val monadProps_rect_Type4 :
79  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
80
81val monadProps_rect_Type5 :
82  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
83
84val monadProps_rect_Type3 :
85  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
86
87val monadProps_rect_Type2 :
88  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
89
90val monadProps_rect_Type1 :
91  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
92
93val monadProps_rect_Type0 :
94  (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1
95
96val max_def : monadProps -> monad
97
98val monadProps_inv_rect_Type4 :
99  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
100
101val monadProps_inv_rect_Type3 :
102  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
103
104val monadProps_inv_rect_Type2 :
105  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
106
107val monadProps_inv_rect_Type1 :
108  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
109
110val monadProps_inv_rect_Type0 :
111  monadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
112
113type 'x_772 max_def__o__monad = __
114
115type setoidMonadProps =
116  monad
117  (* singleton inductive, whose constructor was mk_SetoidMonadProps *)
118
119val setoidMonadProps_rect_Type4 :
120  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
121  setoidMonadProps -> 'a1
122
123val setoidMonadProps_rect_Type5 :
124  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
125  setoidMonadProps -> 'a1
126
127val setoidMonadProps_rect_Type3 :
128  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
129  setoidMonadProps -> 'a1
130
131val setoidMonadProps_rect_Type2 :
132  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
133  setoidMonadProps -> 'a1
134
135val setoidMonadProps_rect_Type1 :
136  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
137  setoidMonadProps -> 'a1
138
139val setoidMonadProps_rect_Type0 :
140  (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
141  setoidMonadProps -> 'a1
142
143val smax_def : setoidMonadProps -> monad
144
145val setoidMonadProps_inv_rect_Type4 :
146  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
147  -> __ -> __ -> 'a1) -> 'a1
148
149val setoidMonadProps_inv_rect_Type3 :
150  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
151  -> __ -> __ -> 'a1) -> 'a1
152
153val setoidMonadProps_inv_rect_Type2 :
154  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
155  -> __ -> __ -> 'a1) -> 'a1
156
157val setoidMonadProps_inv_rect_Type1 :
158  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
159  -> __ -> __ -> 'a1) -> 'a1
160
161val setoidMonadProps_inv_rect_Type0 :
162  setoidMonadProps -> (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __
163  -> __ -> __ -> 'a1) -> 'a1
164
165type 'x_772 smax_def__o__monad = __
166
167val setoid_of_monad : setoidMonadProps -> Setoids.setoid
168
169open Bool
170
171open Nat
172
173open List
174
175val m_map : monad -> ('a1 -> 'a2) -> __ -> __
176
177val m_map2 : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __
178
179val m_bind2 : monad -> __ -> ('a1 -> 'a2 -> __) -> __
180
181val m_bind3 : monad -> __ -> ('a1 -> 'a2 -> 'a3 -> __) -> __
182
183val m_join : monad -> __ -> __
184
185val m_sigbind2 : monad -> __ -> ('a1 -> 'a2 -> __ -> __) -> __
186
187val m_list_map : monad -> ('a1 -> __) -> 'a1 List.list -> __
188
189val m_list_map_sigma : monad -> ('a1 -> __) -> 'a1 List.list -> __
190
191val m_bin_op : monad -> ('a1 -> 'a2 -> 'a3) -> __ -> __ -> __
192
193val m_fold : monad -> ('a1 -> 'a2 -> __) -> 'a1 List.list -> 'a2 -> __
194
195val makeMonadProps :
196  (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) -> monadProps
197
198val makeSetoidMonadProps :
199  (__ -> __ -> 'a1) -> (__ -> __ -> 'a1 -> (__ -> 'a1) -> 'a1) ->
200  setoidMonadProps
201
202open Jmeq
203
204open Russell
205
206type monadPred =
207| Mk_MonadPred
208
209val monadPred_rect_Type4 :
210  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
211
212val monadPred_rect_Type5 :
213  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
214
215val monadPred_rect_Type3 :
216  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
217
218val monadPred_rect_Type2 :
219  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
220
221val monadPred_rect_Type1 :
222  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
223
224val monadPred_rect_Type0 :
225  monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadPred -> 'a1
226
227val monadPred_inv_rect_Type4 :
228  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
229
230val monadPred_inv_rect_Type3 :
231  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
232
233val monadPred_inv_rect_Type2 :
234  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
235
236val monadPred_inv_rect_Type1 :
237  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
238
239val monadPred_inv_rect_Type0 :
240  monad -> monadPred -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
241
242val monadPred_jmdiscr : monad -> monadPred -> monadPred -> __
243
244type injMonadPred = { im_pred : monadPred;
245                      mp_inject : (__ -> __ -> __ Types.sig0 -> __) }
246
247val injMonadPred_rect_Type4 :
248  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
249  injMonadPred -> 'a1
250
251val injMonadPred_rect_Type5 :
252  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
253  injMonadPred -> 'a1
254
255val injMonadPred_rect_Type3 :
256  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
257  injMonadPred -> 'a1
258
259val injMonadPred_rect_Type2 :
260  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
261  injMonadPred -> 'a1
262
263val injMonadPred_rect_Type1 :
264  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
265  injMonadPred -> 'a1
266
267val injMonadPred_rect_Type0 :
268  monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
269  injMonadPred -> 'a1
270
271val im_pred : monad -> injMonadPred -> monadPred
272
273val mp_inject0 : monad -> injMonadPred -> __ Types.sig0 -> __
274
275val injMonadPred_inv_rect_Type4 :
276  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
277  __ -> __ -> 'a1) -> 'a1
278
279val injMonadPred_inv_rect_Type3 :
280  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
281  __ -> __ -> 'a1) -> 'a1
282
283val injMonadPred_inv_rect_Type2 :
284  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
285  __ -> __ -> 'a1) -> 'a1
286
287val injMonadPred_inv_rect_Type1 :
288  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
289  __ -> __ -> 'a1) -> 'a1
290
291val injMonadPred_inv_rect_Type0 :
292  monad -> injMonadPred -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) ->
293  __ -> __ -> 'a1) -> 'a1
294
295val injMonadPred_jmdiscr : monad -> injMonadPred -> injMonadPred -> __
296
297type monadRel =
298| Mk_MonadRel
299
300val monadRel_rect_Type4 :
301  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
302
303val monadRel_rect_Type5 :
304  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
305
306val monadRel_rect_Type3 :
307  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
308
309val monadRel_rect_Type2 :
310  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
311
312val monadRel_rect_Type1 :
313  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
314
315val monadRel_rect_Type0 :
316  monad -> monad -> (__ -> __ -> __ -> __ -> 'a1) -> monadRel -> 'a1
317
318val monadRel_inv_rect_Type4 :
319  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
320
321val monadRel_inv_rect_Type3 :
322  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
323
324val monadRel_inv_rect_Type2 :
325  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
326
327val monadRel_inv_rect_Type1 :
328  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
329
330val monadRel_inv_rect_Type0 :
331  monad -> monad -> monadRel -> (__ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
332
333val monadRel_jmdiscr : monad -> monad -> monadRel -> monadRel -> __
334
Note: See TracBrowser for help on using the repository browser.