source: extracted/structuredTraces.mli @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 28.3 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 Bool
16
17open Jmeq
18
19open BitVectorTrie
20
21open Proper
22
23open PositiveMap
24
25open Deqsets
26
27open ErrorMessages
28
29open PreIdentifiers
30
31open Errors
32
33open Extralib
34
35open Setoids
36
37open Monad
38
39open Option
40
41open Lists
42
43open Positive
44
45open Identifiers
46
47open Exp
48
49open Arithmetic
50
51open Vector
52
53open Div_and_mod
54
55open Russell
56
57open List
58
59open Util
60
61open FoldStuff
62
63open BitVector
64
65open Extranat
66
67open Nat
68
69open Integers
70
71open AST
72
73open CostLabel
74
75open Sets
76
77open Listb
78
79type status_class =
80| Cl_return
81| Cl_jump
82| Cl_call
83| Cl_tailcall
84| Cl_other
85
86val status_class_rect_Type4 :
87  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
88
89val status_class_rect_Type5 :
90  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
91
92val status_class_rect_Type3 :
93  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
94
95val status_class_rect_Type2 :
96  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
97
98val status_class_rect_Type1 :
99  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
100
101val status_class_rect_Type0 :
102  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
103
104val status_class_inv_rect_Type4 :
105  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
106  (__ -> 'a1) -> 'a1
107
108val status_class_inv_rect_Type3 :
109  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
110  (__ -> 'a1) -> 'a1
111
112val status_class_inv_rect_Type2 :
113  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
114  (__ -> 'a1) -> 'a1
115
116val status_class_inv_rect_Type1 :
117  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
118  (__ -> 'a1) -> 'a1
119
120val status_class_inv_rect_Type0 :
121  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
122  (__ -> 'a1) -> 'a1
123
124val status_class_discr : status_class -> status_class -> __
125
126val status_class_jmdiscr : status_class -> status_class -> __
127
128type abstract_status = { as_pc : Deqsets.deqSet; as_pc_of : (__ -> __);
129                         as_classify : (__ -> status_class Types.option);
130                         as_label_of_pc : (__ -> CostLabel.costlabel
131                                          Types.option);
132                         as_call_ident : (__ Types.sig0 -> AST.ident);
133                         as_tailcall_ident : (__ Types.sig0 -> AST.ident) }
134
135val abstract_status_rect_Type4 :
136  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
137  Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
138  (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
139  abstract_status -> 'a1
140
141val abstract_status_rect_Type5 :
142  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
143  Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
144  (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
145  abstract_status -> 'a1
146
147val abstract_status_rect_Type3 :
148  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
149  Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
150  (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
151  abstract_status -> 'a1
152
153val abstract_status_rect_Type2 :
154  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
155  Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
156  (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
157  abstract_status -> 'a1
158
159val abstract_status_rect_Type1 :
160  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
161  Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
162  (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
163  abstract_status -> 'a1
164
165val abstract_status_rect_Type0 :
166  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
167  Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
168  (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
169  abstract_status -> 'a1
170
171type as_status
172
173type as_execute = __
174
175val as_pc : abstract_status -> Deqsets.deqSet
176
177val as_pc_of : abstract_status -> __ -> __
178
179val as_classify : abstract_status -> __ -> status_class Types.option
180
181val as_label_of_pc :
182  abstract_status -> __ -> CostLabel.costlabel Types.option
183
184type as_after_return = __
185
186type as_final = __
187
188val as_call_ident : abstract_status -> __ Types.sig0 -> AST.ident
189
190val as_tailcall_ident : abstract_status -> __ Types.sig0 -> AST.ident
191
192val abstract_status_inv_rect_Type4 :
193  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
194  status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
195  __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) ->
196  __ -> 'a1) -> 'a1
197
198val abstract_status_inv_rect_Type3 :
199  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
200  status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
201  __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) ->
202  __ -> 'a1) -> 'a1
203
204val abstract_status_inv_rect_Type2 :
205  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
206  status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
207  __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) ->
208  __ -> 'a1) -> 'a1
209
210val abstract_status_inv_rect_Type1 :
211  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
212  status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
213  __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) ->
214  __ -> 'a1) -> 'a1
215
216val abstract_status_inv_rect_Type0 :
217  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
218  status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
219  __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) ->
220  __ -> 'a1) -> 'a1
221
222val abstract_status_jmdiscr : abstract_status -> abstract_status -> __
223
224val as_label : abstract_status -> __ -> CostLabel.costlabel Types.option
225
226val as_label_safe : abstract_status -> __ Types.sig0 -> CostLabel.costlabel
227
228val as_costed_exc : abstract_status -> __ -> (__, __) Types.sum
229
230type as_cost_label = CostLabel.costlabel Types.sig0
231
232type as_cost_labels = as_cost_label List.list
233
234val as_cost_get_label :
235  abstract_status -> as_cost_label -> CostLabel.costlabel
236
237val as_cost_get_labels :
238  abstract_status -> as_cost_label PositiveMap.positive_map ->
239  CostLabel.costlabel PositiveMap.positive_map
240
241type as_cost_map = as_cost_label -> Nat.nat
242
243val lift_sigma_map_id :
244  'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1
245  Types.sig0 -> 'a2
246
247val lift_cost_map_id :
248  abstract_status -> abstract_status -> (CostLabel.costlabel -> (__, __)
249  Types.sum) -> as_cost_map -> as_cost_map
250
251type trace_ends_with_ret =
252| Ends_with_ret
253| Doesnt_end_with_ret
254
255val trace_ends_with_ret_rect_Type4 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
256
257val trace_ends_with_ret_rect_Type5 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
258
259val trace_ends_with_ret_rect_Type3 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
260
261val trace_ends_with_ret_rect_Type2 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
262
263val trace_ends_with_ret_rect_Type1 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
264
265val trace_ends_with_ret_rect_Type0 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
266
267val trace_ends_with_ret_inv_rect_Type4 :
268  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
269
270val trace_ends_with_ret_inv_rect_Type3 :
271  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
272
273val trace_ends_with_ret_inv_rect_Type2 :
274  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
275
276val trace_ends_with_ret_inv_rect_Type1 :
277  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
278
279val trace_ends_with_ret_inv_rect_Type0 :
280  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
281
282val trace_ends_with_ret_discr :
283  trace_ends_with_ret -> trace_ends_with_ret -> __
284
285val trace_ends_with_ret_jmdiscr :
286  trace_ends_with_ret -> trace_ends_with_ret -> __
287
288type trace_label_return =
289| Tlr_base of __ * __ * trace_label_label
290| Tlr_step of __ * __ * __ * trace_label_label * trace_label_return
291and trace_label_label =
292| Tll_base of trace_ends_with_ret * __ * __ * trace_any_label
293and trace_any_label =
294| Tal_base_not_return of __ * __
295| Tal_base_return of __ * __
296| Tal_base_call of __ * __ * __ * trace_label_return
297| Tal_base_tailcall of __ * __ * __ * trace_label_return
298| Tal_step_call of trace_ends_with_ret * __ * __ * __ * __
299   * trace_label_return * trace_any_label
300| Tal_step_default of trace_ends_with_ret * __ * __ * __ * trace_any_label
301
302val trace_label_return_inv_rect_Type4 :
303  abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
304  trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
305  trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1
306
307val trace_label_return_inv_rect_Type3 :
308  abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
309  trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
310  trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1
311
312val trace_label_return_inv_rect_Type2 :
313  abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
314  trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
315  trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1
316
317val trace_label_return_inv_rect_Type1 :
318  abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
319  trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
320  trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1
321
322val trace_label_return_inv_rect_Type0 :
323  abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
324  trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
325  trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1
326
327val trace_label_label_inv_rect_Type4 :
328  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
329  (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
330  -> __ -> 'a1) -> 'a1
331
332val trace_label_label_inv_rect_Type3 :
333  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
334  (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
335  -> __ -> 'a1) -> 'a1
336
337val trace_label_label_inv_rect_Type2 :
338  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
339  (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
340  -> __ -> 'a1) -> 'a1
341
342val trace_label_label_inv_rect_Type1 :
343  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
344  (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
345  -> __ -> 'a1) -> 'a1
346
347val trace_label_label_inv_rect_Type0 :
348  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
349  (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
350  -> __ -> 'a1) -> 'a1
351
352val trace_any_label_inv_rect_Type4 :
353  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
354  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ ->
355  __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ ->
356  __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
357  -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> 'a1) ->
358  (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
359  trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ -> 'a1)
360  -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label -> __ ->
361  __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
362
363val trace_any_label_inv_rect_Type3 :
364  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
365  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ ->
366  __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ ->
367  __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
368  -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> 'a1) ->
369  (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
370  trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ -> 'a1)
371  -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label -> __ ->
372  __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
373
374val trace_any_label_inv_rect_Type2 :
375  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
376  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ ->
377  __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ ->
378  __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
379  -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> 'a1) ->
380  (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
381  trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ -> 'a1)
382  -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label -> __ ->
383  __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
384
385val trace_any_label_inv_rect_Type1 :
386  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
387  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ ->
388  __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ ->
389  __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
390  -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> 'a1) ->
391  (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
392  trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ -> 'a1)
393  -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label -> __ ->
394  __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
395
396val trace_any_label_inv_rect_Type0 :
397  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
398  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ ->
399  __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ ->
400  __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
401  -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> 'a1) ->
402  (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
403  trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ -> 'a1)
404  -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label -> __ ->
405  __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
406
407val trace_label_return_discr :
408  abstract_status -> __ -> __ -> trace_label_return -> trace_label_return ->
409  __
410
411val trace_label_label_discr :
412  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
413  trace_label_label -> __
414
415val trace_label_return_jmdiscr :
416  abstract_status -> __ -> __ -> trace_label_return -> trace_label_return ->
417  __
418
419val trace_label_label_jmdiscr :
420  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
421  trace_label_label -> __
422
423val trace_any_label_jmdiscr :
424  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
425  trace_any_label -> __
426
427val tal_pc_list :
428  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label -> __
429  List.list
430
431val as_trace_any_label_length' :
432  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
433  Nat.nat
434
435type tal_unrepeating = __
436
437type tll_unrepeating = __
438
439type tlr_unrepeating = __
440
441val tll_hd_label :
442  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
443  CostLabel.costlabel
444
445val tlr_hd_label :
446  abstract_status -> __ -> __ -> trace_label_return -> CostLabel.costlabel
447
448type trace_any_call =
449| Tac_base of __
450| Tac_step_call of __ * __ * __ * __ * trace_label_return * trace_any_call
451| Tac_step_default of __ * __ * __ * trace_any_call
452
453val trace_any_call_rect_Type4 :
454  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
455  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
456  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
457  -> trace_any_call -> 'a1
458
459val trace_any_call_rect_Type3 :
460  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
461  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
462  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
463  -> trace_any_call -> 'a1
464
465val trace_any_call_rect_Type2 :
466  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
467  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
468  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
469  -> trace_any_call -> 'a1
470
471val trace_any_call_rect_Type1 :
472  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
473  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
474  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
475  -> trace_any_call -> 'a1
476
477val trace_any_call_rect_Type0 :
478  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
479  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
480  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
481  -> trace_any_call -> 'a1
482
483val trace_any_call_inv_rect_Type4 :
484  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
485  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
486  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
487  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
488  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
489
490val trace_any_call_inv_rect_Type3 :
491  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
492  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
493  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
494  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
495  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
496
497val trace_any_call_inv_rect_Type2 :
498  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
499  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
500  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
501  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
502  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
503
504val trace_any_call_inv_rect_Type1 :
505  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
506  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
507  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
508  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
509  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
510
511val trace_any_call_inv_rect_Type0 :
512  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
513  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
514  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
515  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
516  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
517
518val trace_any_call_jmdiscr :
519  abstract_status -> __ -> __ -> trace_any_call -> trace_any_call -> __
520
521type trace_label_call =
522| Tlc_base of __ * __ * trace_any_call
523
524val trace_label_call_rect_Type4 :
525  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
526  trace_label_call -> 'a1
527
528val trace_label_call_rect_Type5 :
529  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
530  trace_label_call -> 'a1
531
532val trace_label_call_rect_Type3 :
533  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
534  trace_label_call -> 'a1
535
536val trace_label_call_rect_Type2 :
537  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
538  trace_label_call -> 'a1
539
540val trace_label_call_rect_Type1 :
541  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
542  trace_label_call -> 'a1
543
544val trace_label_call_rect_Type0 :
545  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
546  trace_label_call -> 'a1
547
548val trace_label_call_inv_rect_Type4 :
549  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
550  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
551
552val trace_label_call_inv_rect_Type3 :
553  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
554  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
555
556val trace_label_call_inv_rect_Type2 :
557  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
558  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
559
560val trace_label_call_inv_rect_Type1 :
561  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
562  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
563
564val trace_label_call_inv_rect_Type0 :
565  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
566  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
567
568val trace_label_call_discr :
569  abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __
570
571val trace_label_call_jmdiscr :
572  abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __
573
574val tlc_hd_label :
575  abstract_status -> __ -> __ -> trace_label_call -> CostLabel.costlabel
576
577type trace_label_diverges = __trace_label_diverges Lazy.t
578and __trace_label_diverges =
579| Tld_step of __ * __ * trace_label_label * trace_label_diverges
580| Tld_base of __ * __ * __ * trace_label_call * trace_label_diverges
581
582val trace_label_diverges_inv_rect_Type4 :
583  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
584  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
585  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
586  -> 'a1) -> 'a1
587
588val trace_label_diverges_inv_rect_Type3 :
589  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
590  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
591  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
592  -> 'a1) -> 'a1
593
594val trace_label_diverges_inv_rect_Type2 :
595  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
596  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
597  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
598  -> 'a1) -> 'a1
599
600val trace_label_diverges_inv_rect_Type1 :
601  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
602  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
603  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
604  -> 'a1) -> 'a1
605
606val trace_label_diverges_inv_rect_Type0 :
607  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
608  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
609  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
610  -> 'a1) -> 'a1
611
612val trace_label_diverges_jmdiscr :
613  abstract_status -> __ -> trace_label_diverges -> trace_label_diverges -> __
614
615val tld_hd_label :
616  abstract_status -> __ -> trace_label_diverges -> CostLabel.costlabel
617
618type trace_whole_program =
619| Twp_terminating of __ * __ * __ * trace_label_return
620| Twp_diverges of __ * __ * trace_label_diverges
621
622val trace_whole_program_rect_Type4 :
623  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
624  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
625  trace_whole_program -> 'a1
626
627val trace_whole_program_rect_Type5 :
628  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
629  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
630  trace_whole_program -> 'a1
631
632val trace_whole_program_rect_Type3 :
633  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
634  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
635  trace_whole_program -> 'a1
636
637val trace_whole_program_rect_Type2 :
638  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
639  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
640  trace_whole_program -> 'a1
641
642val trace_whole_program_rect_Type1 :
643  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
644  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
645  trace_whole_program -> 'a1
646
647val trace_whole_program_rect_Type0 :
648  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
649  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
650  trace_whole_program -> 'a1
651
652val trace_whole_program_inv_rect_Type4 :
653  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
654  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
655  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
656
657val trace_whole_program_inv_rect_Type3 :
658  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
659  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
660  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
661
662val trace_whole_program_inv_rect_Type2 :
663  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
664  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
665  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
666
667val trace_whole_program_inv_rect_Type1 :
668  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
669  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
670  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
671
672val trace_whole_program_inv_rect_Type0 :
673  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
674  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
675  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
676
677val trace_whole_program_jmdiscr :
678  abstract_status -> __ -> trace_whole_program -> trace_whole_program -> __
679
680val tal_tl_label :
681  abstract_status -> __ -> __ -> trace_any_label -> CostLabel.costlabel
682
683val tll_tl_label :
684  abstract_status -> __ -> __ -> trace_label_label -> CostLabel.costlabel
685
686type trace_any_any =
687| Taa_base of __
688| Taa_step of __ * __ * __ * trace_any_any
689
690val trace_any_any_rect_Type4 :
691  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
692  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
693
694val trace_any_any_rect_Type3 :
695  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
696  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
697
698val trace_any_any_rect_Type2 :
699  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
700  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
701
702val trace_any_any_rect_Type1 :
703  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
704  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
705
706val trace_any_any_rect_Type0 :
707  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
708  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
709
710val trace_any_any_inv_rect_Type4 :
711  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
712  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
713  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
714
715val trace_any_any_inv_rect_Type3 :
716  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
717  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
718  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
719
720val trace_any_any_inv_rect_Type2 :
721  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
722  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
723  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
724
725val trace_any_any_inv_rect_Type1 :
726  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
727  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
728  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
729
730val trace_any_any_inv_rect_Type0 :
731  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
732  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
733  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
734
735val trace_any_any_jmdiscr :
736  abstract_status -> __ -> __ -> trace_any_any -> trace_any_any -> __
737
738val taa_non_empty : abstract_status -> __ -> __ -> trace_any_any -> Bool.bool
739
740val taa_append_tal :
741  abstract_status -> __ -> trace_ends_with_ret -> __ -> __ -> trace_any_any
742  -> trace_any_label -> trace_any_label
743
744type tal_collapsable = __
745
746type tal_rel = __
747
748type tll_rel = __
749
750type tlr_rel = __
751
752val flatten_trace_label_return :
753  abstract_status -> __ -> __ -> trace_label_return -> as_cost_label
754  List.list
755
756val flatten_trace_any_label :
757  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
758  as_cost_label List.list
759
760val flatten_trace_label_label :
761  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
762  as_cost_label List.list
763
Note: See TracBrowser for help on using the repository browser.