source: extracted/structuredTraces.mli @ 2716

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

...

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