source: driver/extracted/structuredTraces.mli @ 3106

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

Extracted again.

File size: 36.5 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Relations
12
13open Bool
14
15open Jmeq
16
17open Proper
18
19open PositiveMap
20
21open Deqsets
22
23open ErrorMessages
24
25open PreIdentifiers
26
27open Errors
28
29open Extralib
30
31open Setoids
32
33open Monad
34
35open Option
36
37open Div_and_mod
38
39open Russell
40
41open Util
42
43open List
44
45open Lists
46
47open Nat
48
49open Positive
50
51open Types
52
53open Identifiers
54
55open CostLabel
56
57open Sets
58
59open Listb
60
61open Integers
62
63open AST
64
65open Division
66
67open Exp
68
69open Arithmetic
70
71open Extranat
72
73open Vector
74
75open FoldStuff
76
77open BitVector
78
79open Z
80
81open BitVectorZ
82
83open Pointers
84
85open Coqlib
86
87open Values
88
89open Events
90
91open IOMonad
92
93open IO
94
95open Hide
96
97type status_class =
98| Cl_return
99| Cl_jump
100| Cl_call
101| Cl_tailcall
102| Cl_other
103
104val status_class_rect_Type4 :
105  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
106
107val status_class_rect_Type5 :
108  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
109
110val status_class_rect_Type3 :
111  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
112
113val status_class_rect_Type2 :
114  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
115
116val status_class_rect_Type1 :
117  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
118
119val status_class_rect_Type0 :
120  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
121
122val status_class_inv_rect_Type4 :
123  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
124  (__ -> 'a1) -> 'a1
125
126val status_class_inv_rect_Type3 :
127  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
128  (__ -> 'a1) -> 'a1
129
130val status_class_inv_rect_Type2 :
131  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
132  (__ -> 'a1) -> 'a1
133
134val status_class_inv_rect_Type1 :
135  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
136  (__ -> 'a1) -> 'a1
137
138val status_class_inv_rect_Type0 :
139  status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
140  (__ -> 'a1) -> 'a1
141
142val status_class_discr : status_class -> status_class -> __
143
144val status_class_jmdiscr : status_class -> status_class -> __
145
146type abstract_status = { as_pc : Deqsets.deqSet; as_pc_of : (__ -> __);
147                         as_classify : (__ -> status_class);
148                         as_label_of_pc : (__ -> CostLabel.costlabel
149                                          Types.option);
150                         as_result : (__ -> Integers.int Types.option);
151                         as_call_ident : (__ Types.sig0 -> AST.ident);
152                         as_tailcall_ident : (__ Types.sig0 -> AST.ident) }
153
154val abstract_status_rect_Type4 :
155  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__ ->
156  CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
157  Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
158  AST.ident) -> 'a1) -> abstract_status -> 'a1
159
160val abstract_status_rect_Type5 :
161  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__ ->
162  CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
163  Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
164  AST.ident) -> 'a1) -> abstract_status -> 'a1
165
166val abstract_status_rect_Type3 :
167  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__ ->
168  CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
169  Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
170  AST.ident) -> 'a1) -> abstract_status -> 'a1
171
172val abstract_status_rect_Type2 :
173  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__ ->
174  CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
175  Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
176  AST.ident) -> 'a1) -> abstract_status -> 'a1
177
178val abstract_status_rect_Type1 :
179  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__ ->
180  CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
181  Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
182  AST.ident) -> 'a1) -> abstract_status -> 'a1
183
184val abstract_status_rect_Type0 :
185  (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__ ->
186  CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
187  Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
188  AST.ident) -> 'a1) -> abstract_status -> 'a1
189
190type as_status
191
192val as_pc : abstract_status -> Deqsets.deqSet
193
194val as_pc_of : abstract_status -> __ -> __
195
196val as_classify : abstract_status -> __ -> status_class
197
198val as_label_of_pc :
199  abstract_status -> __ -> CostLabel.costlabel Types.option
200
201val as_result : abstract_status -> __ -> Integers.int Types.option
202
203val as_call_ident : abstract_status -> __ Types.sig0 -> AST.ident
204
205val as_tailcall_ident : abstract_status -> __ Types.sig0 -> AST.ident
206
207val abstract_status_inv_rect_Type4 :
208  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
209  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
210  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
211  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1
212
213val abstract_status_inv_rect_Type3 :
214  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
215  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
216  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
217  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1
218
219val abstract_status_inv_rect_Type2 :
220  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
221  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
222  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
223  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1
224
225val abstract_status_inv_rect_Type1 :
226  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
227  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
228  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
229  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1
230
231val abstract_status_inv_rect_Type0 :
232  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
233  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
234  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
235  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1
236
237val abstract_status_jmdiscr : abstract_status -> abstract_status -> __
238
239val as_label : abstract_status -> __ -> CostLabel.costlabel Types.option
240
241val as_costed_exc : abstract_status -> __ -> (__, __) Types.sum
242
243type as_cost_label = CostLabel.costlabel Types.sig0
244
245type as_cost_labels = as_cost_label List.list
246
247val as_cost_get_label :
248  abstract_status -> as_cost_label -> CostLabel.costlabel
249
250type as_cost_map = as_cost_label -> Nat.nat
251
252val as_label_safe : abstract_status -> __ Types.sig0 -> as_cost_label
253
254val lift_sigma_map_id :
255  'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1
256  Types.sig0 -> 'a2
257
258val lift_cost_map_id :
259  abstract_status -> abstract_status -> (CostLabel.costlabel -> (__, __)
260  Types.sum) -> as_cost_map -> as_cost_map
261
262type trace_ends_with_ret =
263| Ends_with_ret
264| Doesnt_end_with_ret
265
266val trace_ends_with_ret_rect_Type4 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
267
268val trace_ends_with_ret_rect_Type5 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
269
270val trace_ends_with_ret_rect_Type3 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
271
272val trace_ends_with_ret_rect_Type2 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
273
274val trace_ends_with_ret_rect_Type1 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
275
276val trace_ends_with_ret_rect_Type0 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
277
278val trace_ends_with_ret_inv_rect_Type4 :
279  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
280
281val trace_ends_with_ret_inv_rect_Type3 :
282  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
283
284val trace_ends_with_ret_inv_rect_Type2 :
285  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
286
287val trace_ends_with_ret_inv_rect_Type1 :
288  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
289
290val trace_ends_with_ret_inv_rect_Type0 :
291  trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
292
293val trace_ends_with_ret_discr :
294  trace_ends_with_ret -> trace_ends_with_ret -> __
295
296val trace_ends_with_ret_jmdiscr :
297  trace_ends_with_ret -> trace_ends_with_ret -> __
298
299type trace_label_return =
300| Tlr_base of __ * __ * trace_label_label
301| Tlr_step of __ * __ * __ * trace_label_label * trace_label_return
302and trace_label_label =
303| Tll_base of trace_ends_with_ret * __ * __ * trace_any_label
304and trace_any_label =
305| Tal_base_not_return of __ * __
306| Tal_base_return of __ * __
307| Tal_base_call of __ * __ * __ * trace_label_return
308| Tal_base_tailcall of __ * __ * __ * trace_label_return
309| Tal_step_call of trace_ends_with_ret * __ * __ * __ * __
310   * trace_label_return * trace_any_label
311| Tal_step_default of trace_ends_with_ret * __ * __ * __ * trace_any_label
312
313val trace_label_return_inv_rect_Type4 :
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_Type3 :
319  abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
320  trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
321  trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1
322
323val trace_label_return_inv_rect_Type2 :
324  abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
325  trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
326  trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1
327
328val trace_label_return_inv_rect_Type1 :
329  abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
330  trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
331  trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1
332
333val trace_label_return_inv_rect_Type0 :
334  abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
335  trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
336  trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1
337
338val trace_label_label_inv_rect_Type4 :
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_Type3 :
344  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
345  (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
346  -> __ -> 'a1) -> 'a1
347
348val trace_label_label_inv_rect_Type2 :
349  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
350  (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
351  -> __ -> 'a1) -> 'a1
352
353val trace_label_label_inv_rect_Type1 :
354  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
355  (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
356  -> __ -> 'a1) -> 'a1
357
358val trace_label_label_inv_rect_Type0 :
359  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
360  (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
361  -> __ -> 'a1) -> 'a1
362
363val trace_any_label_inv_rect_Type4 :
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_Type3 :
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_Type2 :
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_Type1 :
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_any_label_inv_rect_Type0 :
408  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
409  (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ ->
410  __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ ->
411  __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
412  -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> 'a1) ->
413  (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __ ->
414  trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ -> 'a1)
415  -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label -> __ ->
416  __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
417
418val trace_label_return_discr :
419  abstract_status -> __ -> __ -> trace_label_return -> trace_label_return ->
420  __
421
422val trace_label_label_discr :
423  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
424  trace_label_label -> __
425
426val trace_label_return_jmdiscr :
427  abstract_status -> __ -> __ -> trace_label_return -> trace_label_return ->
428  __
429
430val trace_label_label_jmdiscr :
431  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
432  trace_label_label -> __
433
434val trace_any_label_jmdiscr :
435  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
436  trace_any_label -> __
437
438val tal_pc_list :
439  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label -> __
440  List.list
441
442val as_trace_any_label_length' :
443  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
444  Nat.nat
445
446val tll_hd_label :
447  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
448  CostLabel.costlabel
449
450val tlr_hd_label :
451  abstract_status -> __ -> __ -> trace_label_return -> CostLabel.costlabel
452
453type trace_any_call =
454| Tac_base of __
455| Tac_step_call of __ * __ * __ * __ * trace_label_return * trace_any_call
456| Tac_step_default of __ * __ * __ * trace_any_call
457
458val trace_any_call_rect_Type4 :
459  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
460  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
461  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
462  -> trace_any_call -> 'a1
463
464val trace_any_call_rect_Type3 :
465  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
466  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
467  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
468  -> trace_any_call -> 'a1
469
470val trace_any_call_rect_Type2 :
471  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
472  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
473  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
474  -> trace_any_call -> 'a1
475
476val trace_any_call_rect_Type1 :
477  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
478  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
479  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
480  -> trace_any_call -> 'a1
481
482val trace_any_call_rect_Type0 :
483  abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
484  -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
485  -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ -> __
486  -> trace_any_call -> 'a1
487
488val trace_any_call_inv_rect_Type4 :
489  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
490  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
491  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
492  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
493  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
494
495val trace_any_call_inv_rect_Type3 :
496  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
497  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
498  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
499  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
500  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
501
502val trace_any_call_inv_rect_Type2 :
503  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
504  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
505  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
506  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
507  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
508
509val trace_any_call_inv_rect_Type1 :
510  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
511  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
512  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
513  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
514  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
515
516val trace_any_call_inv_rect_Type0 :
517  abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
518  __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ -> trace_label_return
519  -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
520  'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> (__ -> __ ->
521  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
522
523val trace_any_call_jmdiscr :
524  abstract_status -> __ -> __ -> trace_any_call -> trace_any_call -> __
525
526type trace_label_call =
527| Tlc_base of __ * __ * trace_any_call
528
529val trace_label_call_rect_Type4 :
530  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
531  trace_label_call -> 'a1
532
533val trace_label_call_rect_Type5 :
534  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
535  trace_label_call -> 'a1
536
537val trace_label_call_rect_Type3 :
538  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
539  trace_label_call -> 'a1
540
541val trace_label_call_rect_Type2 :
542  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
543  trace_label_call -> 'a1
544
545val trace_label_call_rect_Type1 :
546  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
547  trace_label_call -> 'a1
548
549val trace_label_call_rect_Type0 :
550  abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
551  trace_label_call -> 'a1
552
553val trace_label_call_inv_rect_Type4 :
554  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
555  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
556
557val trace_label_call_inv_rect_Type3 :
558  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
559  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
560
561val trace_label_call_inv_rect_Type2 :
562  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
563  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
564
565val trace_label_call_inv_rect_Type1 :
566  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
567  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
568
569val trace_label_call_inv_rect_Type0 :
570  abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
571  trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
572
573val trace_label_call_discr :
574  abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __
575
576val trace_label_call_jmdiscr :
577  abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __
578
579val tlc_hd_label :
580  abstract_status -> __ -> __ -> trace_label_call -> CostLabel.costlabel
581
582type trace_label_diverges = __trace_label_diverges Lazy.t
583and __trace_label_diverges =
584| Tld_step of __ * __ * trace_label_label * trace_label_diverges
585| Tld_base of __ * __ * __ * trace_label_call * trace_label_diverges
586
587val trace_label_diverges_inv_rect_Type4 :
588  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
589  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
590  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
591  -> 'a1) -> 'a1
592
593val trace_label_diverges_inv_rect_Type3 :
594  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
595  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
596  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
597  -> 'a1) -> 'a1
598
599val trace_label_diverges_inv_rect_Type2 :
600  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
601  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
602  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
603  -> 'a1) -> 'a1
604
605val trace_label_diverges_inv_rect_Type1 :
606  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
607  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
608  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
609  -> 'a1) -> 'a1
610
611val trace_label_diverges_inv_rect_Type0 :
612  abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
613  trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ -> __
614  -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ -> __
615  -> 'a1) -> 'a1
616
617val trace_label_diverges_jmdiscr :
618  abstract_status -> __ -> trace_label_diverges -> trace_label_diverges -> __
619
620val tld_hd_label :
621  abstract_status -> __ -> trace_label_diverges -> CostLabel.costlabel
622
623type trace_whole_program =
624| Twp_terminating of __ * __ * __ * trace_label_return
625| Twp_diverges of __ * __ * trace_label_diverges
626
627val trace_whole_program_rect_Type4 :
628  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
629  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
630  trace_whole_program -> 'a1
631
632val trace_whole_program_rect_Type5 :
633  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
634  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
635  trace_whole_program -> 'a1
636
637val trace_whole_program_rect_Type3 :
638  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
639  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
640  trace_whole_program -> 'a1
641
642val trace_whole_program_rect_Type2 :
643  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
644  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
645  trace_whole_program -> 'a1
646
647val trace_whole_program_rect_Type1 :
648  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
649  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
650  trace_whole_program -> 'a1
651
652val trace_whole_program_rect_Type0 :
653  abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
654  -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
655  trace_whole_program -> 'a1
656
657val trace_whole_program_inv_rect_Type4 :
658  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
659  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
660  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
661
662val trace_whole_program_inv_rect_Type3 :
663  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
664  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
665  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
666
667val trace_whole_program_inv_rect_Type2 :
668  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
669  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
670  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
671
672val trace_whole_program_inv_rect_Type1 :
673  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
674  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
675  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
676
677val trace_whole_program_inv_rect_Type0 :
678  abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
679  -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
680  trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
681
682val trace_whole_program_jmdiscr :
683  abstract_status -> __ -> trace_whole_program -> trace_whole_program -> __
684
685val tal_tl_label :
686  abstract_status -> __ -> __ -> trace_any_label -> CostLabel.costlabel
687
688val tll_tl_label :
689  abstract_status -> __ -> __ -> trace_label_label -> CostLabel.costlabel
690
691type trace_any_any =
692| Taa_base of __
693| Taa_step of __ * __ * __ * trace_any_any
694
695val trace_any_any_rect_Type4 :
696  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
697  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
698
699val trace_any_any_rect_Type3 :
700  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
701  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
702
703val trace_any_any_rect_Type2 :
704  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
705  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
706
707val trace_any_any_rect_Type1 :
708  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
709  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
710
711val trace_any_any_rect_Type0 :
712  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
713  trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
714
715val trace_any_any_inv_rect_Type4 :
716  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
717  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
718  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
719
720val trace_any_any_inv_rect_Type3 :
721  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
722  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
723  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
724
725val trace_any_any_inv_rect_Type2 :
726  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
727  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
728  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
729
730val trace_any_any_inv_rect_Type1 :
731  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
732  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
733  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
734
735val trace_any_any_inv_rect_Type0 :
736  abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
737  'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
738  __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
739
740val trace_any_any_jmdiscr :
741  abstract_status -> __ -> __ -> trace_any_any -> trace_any_any -> __
742
743val taa_non_empty : abstract_status -> __ -> __ -> trace_any_any -> Bool.bool
744
745val dpi1__o__taa_to_bool__o__inject :
746  abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair ->
747  Bool.bool Types.sig0
748
749val dpi1__o__taa_to_bool__o__bool_to_Prop__o__inject :
750  abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair -> __
751  Types.sig0
752
753val eject__o__taa_to_bool__o__inject :
754  abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool
755  Types.sig0
756
757val eject__o__taa_to_bool__o__bool_to_Prop__o__inject :
758  abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> __ Types.sig0
759
760val taa_to_bool__o__bool_to_Prop__o__inject :
761  abstract_status -> __ -> __ -> trace_any_any -> __ Types.sig0
762
763val taa_to_bool__o__inject :
764  abstract_status -> __ -> __ -> trace_any_any -> Bool.bool Types.sig0
765
766val dpi1__o__taa_to_bool :
767  abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair ->
768  Bool.bool
769
770val eject__o__taa_to_bool :
771  abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool
772
773val taa_append_tal :
774  abstract_status -> __ -> trace_ends_with_ret -> __ -> __ -> trace_any_any
775  -> trace_any_label -> trace_any_label
776
777type intensional_event =
778| IEVcost of CostLabel.costlabel
779| IEVcall of AST.ident
780| IEVtailcall of AST.ident * AST.ident
781| IEVret of AST.ident
782
783val intensional_event_rect_Type4 :
784  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
785  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
786
787val intensional_event_rect_Type5 :
788  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
789  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
790
791val intensional_event_rect_Type3 :
792  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
793  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
794
795val intensional_event_rect_Type2 :
796  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
797  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
798
799val intensional_event_rect_Type1 :
800  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
801  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
802
803val intensional_event_rect_Type0 :
804  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
805  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
806
807val intensional_event_inv_rect_Type4 :
808  intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
809  -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
810  'a1) -> 'a1
811
812val intensional_event_inv_rect_Type3 :
813  intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
814  -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
815  'a1) -> 'a1
816
817val intensional_event_inv_rect_Type2 :
818  intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
819  -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
820  'a1) -> 'a1
821
822val intensional_event_inv_rect_Type1 :
823  intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
824  -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
825  'a1) -> 'a1
826
827val intensional_event_inv_rect_Type0 :
828  intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
829  -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
830  'a1) -> 'a1
831
832val intensional_event_discr : intensional_event -> intensional_event -> __
833
834val intensional_event_jmdiscr : intensional_event -> intensional_event -> __
835
836type as_trace = intensional_event List.list Types.sig0
837
838val cons_safe :
839  'a1 Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0
840
841val append_safe :
842  'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list
843  Types.sig0
844
845val nil_safe : 'a1 List.list Types.sig0
846
847val emittable_cost :
848  abstract_status -> as_cost_label -> intensional_event Types.sig0
849
850val observables_trace_label_return :
851  abstract_status -> __ -> __ -> trace_label_return -> AST.ident -> as_trace
852
853val observables_trace_any_label :
854  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
855  AST.ident -> as_trace
856
857val observables_trace_label_label :
858  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
859  AST.ident -> as_trace
860
861val filter_map : ('a1 -> 'a2 Types.option) -> 'a1 List.list -> 'a2 List.list
862
863val list_distribute_sig_aux : 'a1 List.list -> 'a1 Types.sig0 List.list
864
865val list_distribute_sig :
866  'a1 List.list Types.sig0 -> 'a1 Types.sig0 List.list
867
868val list_factor_sig : 'a1 Types.sig0 List.list -> 'a1 List.list Types.sig0
869
870val costlabels_of_observables :
871  abstract_status -> as_trace -> as_cost_label List.list
872
873val flatten_trace_label_return :
874  abstract_status -> __ -> __ -> trace_label_return -> as_cost_label
875  List.list
876
877val flatten_trace_label_label :
878  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
879  as_cost_label List.list
880
881val flatten_trace_any_label :
882  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
883  as_cost_label List.list
884
885type trace_any_any_free =
886| Taaf_base of __
887| Taaf_step of __ * __ * __ * trace_any_any
888| Taaf_step_jump of __ * __ * __ * trace_any_any
889
890val trace_any_any_free_rect_Type4 :
891  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ ->
892  __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) ->
893  __ -> __ -> trace_any_any_free -> 'a1
894
895val trace_any_any_free_rect_Type5 :
896  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ ->
897  __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) ->
898  __ -> __ -> trace_any_any_free -> 'a1
899
900val trace_any_any_free_rect_Type3 :
901  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ ->
902  __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) ->
903  __ -> __ -> trace_any_any_free -> 'a1
904
905val trace_any_any_free_rect_Type2 :
906  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ ->
907  __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) ->
908  __ -> __ -> trace_any_any_free -> 'a1
909
910val trace_any_any_free_rect_Type1 :
911  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ ->
912  __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) ->
913  __ -> __ -> trace_any_any_free -> 'a1
914
915val trace_any_any_free_rect_Type0 :
916  abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ ->
917  __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> 'a1) ->
918  __ -> __ -> trace_any_any_free -> 'a1
919
920val trace_any_any_free_inv_rect_Type4 :
921  abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
922  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
923  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
924  -> __ -> 'a1) -> 'a1
925
926val trace_any_any_free_inv_rect_Type3 :
927  abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
928  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
929  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
930  -> __ -> 'a1) -> 'a1
931
932val trace_any_any_free_inv_rect_Type2 :
933  abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
934  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
935  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
936  -> __ -> 'a1) -> 'a1
937
938val trace_any_any_free_inv_rect_Type1 :
939  abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
940  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
941  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
942  -> __ -> 'a1) -> 'a1
943
944val trace_any_any_free_inv_rect_Type0 :
945  abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
946  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
947  -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
948  -> __ -> 'a1) -> 'a1
949
950val trace_any_any_free_jmdiscr :
951  abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any_free ->
952  __
953
954val taaf_non_empty :
955  abstract_status -> __ -> __ -> trace_any_any_free -> Bool.bool
956
957val taa_append_taa :
958  abstract_status -> __ -> __ -> __ -> trace_any_any -> trace_any_any ->
959  trace_any_any
960
961val taaf_to_taa :
962  abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any
963
964val taaf_append_tal :
965  abstract_status -> __ -> trace_ends_with_ret -> __ -> __ ->
966  trace_any_any_free -> trace_any_label -> trace_any_label
967
968val taaf_append_taa :
969  abstract_status -> __ -> __ -> __ -> trace_any_any_free -> trace_any_any ->
970  trace_any_any
971
972val taaf_cons :
973  abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
974  trace_any_any_free
975
976val taaf_append_taaf :
977  abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
978  trace_any_any_free -> trace_any_any_free
979
Note: See TracBrowser for help on using the repository browser.