source: extracted/structuredTraces.mli @ 2968

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

Extracted again.

File size: 36.5 KB
RevLine 
[2601]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
[2649]23open ErrorMessages
24
[2601]25open PreIdentifiers
26
27open Errors
28
29open Extralib
30
31open Setoids
32
33open Monad
34
35open Option
36
[2773]37open Div_and_mod
38
39open Russell
40
41open Util
42
43open List
44
[2601]45open Lists
46
[2773]47open Nat
48
[2601]49open Positive
50
[2773]51open Types
52
[2601]53open Identifiers
54
[2773]55open CostLabel
[2717]56
[2773]57open Sets
[2601]58
[2773]59open Listb
[2601]60
[2773]61open Integers
[2601]62
[2773]63open AST
[2601]64
[2773]65open Division
[2601]66
[2773]67open Exp
[2601]68
[2773]69open Arithmetic
70
71open Extranat
72
73open Vector
74
[2601]75open FoldStuff
76
77open BitVector
78
[2773]79open Z
[2601]80
[2773]81open BitVectorZ
[2601]82
[2773]83open Pointers
[2601]84
[2773]85open Coqlib
[2601]86
[2773]87open Values
[2601]88
[2773]89open Events
[2601]90
[2773]91open IOMonad
[2601]92
[2773]93open IO
94
95open Hide
96
[2601]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 : (__ -> __);
[2773]147                         as_classify : (__ -> status_class);
[2601]148                         as_label_of_pc : (__ -> CostLabel.costlabel
149                                          Types.option);
[2773]150                         as_result : (__ -> Integers.int Types.option);
[2601]151                         as_call_ident : (__ Types.sig0 -> AST.ident);
152                         as_tailcall_ident : (__ Types.sig0 -> AST.ident) }
153
154val abstract_status_rect_Type4 :
[2773]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
[2601]159
160val abstract_status_rect_Type5 :
[2773]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
[2601]165
166val abstract_status_rect_Type3 :
[2773]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
[2601]171
172val abstract_status_rect_Type2 :
[2773]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
[2601]177
178val abstract_status_rect_Type1 :
[2773]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
[2601]183
184val abstract_status_rect_Type0 :
[2773]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
[2601]189
190type as_status
191
192val as_pc : abstract_status -> Deqsets.deqSet
193
194val as_pc_of : abstract_status -> __ -> __
195
[2773]196val as_classify : abstract_status -> __ -> status_class
[2601]197
198val as_label_of_pc :
199  abstract_status -> __ -> CostLabel.costlabel Types.option
200
[2773]201val as_result : abstract_status -> __ -> Integers.int Types.option
[2601]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 -> (__ -> __) -> (__ ->
[2773]209  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
210  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
211  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1
[2601]212
213val abstract_status_inv_rect_Type3 :
214  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
[2773]215  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
216  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
217  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1
[2601]218
219val abstract_status_inv_rect_Type2 :
220  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
[2773]221  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
222  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
223  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1
[2601]224
225val abstract_status_inv_rect_Type1 :
226  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
[2773]227  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
228  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
229  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1
[2601]230
231val abstract_status_inv_rect_Type0 :
232  abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
[2773]233  status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
234  Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
235  Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1
[2601]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
[2773]252val as_label_safe : abstract_status -> __ Types.sig0 -> as_cost_label
253
[2601]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
[2743]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
[2601]773val taa_append_tal :
774  abstract_status -> __ -> trace_ends_with_ret -> __ -> __ -> trace_any_any
775  -> trace_any_label -> trace_any_label
776
[2773]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
[2601]782
[2773]783val intensional_event_rect_Type4 :
784  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
785  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
[2601]786
[2773]787val intensional_event_rect_Type5 :
788  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
789  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
[2601]790
[2773]791val intensional_event_rect_Type3 :
792  (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
793  AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
[2601]794
[2773]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
[2601]873val flatten_trace_label_return :
874  abstract_status -> __ -> __ -> trace_label_return -> as_cost_label
875  List.list
876
[2773]877val flatten_trace_label_label :
878  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
879  as_cost_label List.list
880
[2601]881val flatten_trace_any_label :
882  abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
883  as_cost_label List.list
884
[2873]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.