104 val status_class_rect_Type4 :
105 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
107 val status_class_rect_Type5 :
108 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
110 val status_class_rect_Type3 :
111 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
113 val status_class_rect_Type2 :
114 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
116 val status_class_rect_Type1 :
117 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
119 val status_class_rect_Type0 :
120 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
122 val status_class_inv_rect_Type4 :
123 status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
126 val status_class_inv_rect_Type3 :
127 status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
130 val status_class_inv_rect_Type2 :
131 status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
134 val status_class_inv_rect_Type1 :
135 status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
138 val status_class_inv_rect_Type0 :
139 status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
142 val status_class_discr : status_class -> status_class -> __
144 val status_class_jmdiscr : status_class -> status_class -> __
146 type abstract_status = { as_pc : Deqsets.deqSet; as_pc_of : (__ -> __);
147 as_classify : (__ -> status_class);
148 as_label_of_pc : (__ -> CostLabel.costlabel
150 as_result : (__ -> Integers.int Types.option);
151 as_call_ident : (__ Types.sig0 -> AST.ident);
152 as_tailcall_ident : (__ Types.sig0 -> AST.ident) }
154 val 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
160 val 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
166 val 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
172 val 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
178 val 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
184 val 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
192 val as_pc : abstract_status -> Deqsets.deqSet
194 val as_pc_of : abstract_status -> __ -> __
196 val as_classify : abstract_status -> __ -> status_class
199 abstract_status -> __ -> CostLabel.costlabel Types.option
201 val as_result : abstract_status -> __ -> Integers.int Types.option
203 val as_call_ident : abstract_status -> __ Types.sig0 -> AST.ident
205 val as_tailcall_ident : abstract_status -> __ Types.sig0 -> AST.ident
207 val 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
213 val 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
219 val 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
225 val 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
231 val 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
237 val abstract_status_jmdiscr : abstract_status -> abstract_status -> __
239 val as_label : abstract_status -> __ -> CostLabel.costlabel Types.option
241 val as_costed_exc : abstract_status -> __ -> (__, __) Types.sum
243 type as_cost_label = CostLabel.costlabel Types.sig0
245 type as_cost_labels = as_cost_label List.list
247 val as_cost_get_label :
248 abstract_status -> as_cost_label -> CostLabel.costlabel
250 type as_cost_map = as_cost_label -> Nat.nat
252 val as_label_safe : abstract_status -> __ Types.sig0 -> as_cost_label
254 val lift_sigma_map_id :
255 'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1
258 val lift_cost_map_id :
259 abstract_status -> abstract_status -> (CostLabel.costlabel -> (__, __)
260 Types.sum) -> as_cost_map -> as_cost_map
262 type trace_ends_with_ret =
264 | Doesnt_end_with_ret
266 val trace_ends_with_ret_rect_Type4 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
268 val trace_ends_with_ret_rect_Type5 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
270 val trace_ends_with_ret_rect_Type3 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
272 val trace_ends_with_ret_rect_Type2 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
274 val trace_ends_with_ret_rect_Type1 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
276 val trace_ends_with_ret_rect_Type0 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
278 val trace_ends_with_ret_inv_rect_Type4 :
279 trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
281 val trace_ends_with_ret_inv_rect_Type3 :
282 trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
284 val trace_ends_with_ret_inv_rect_Type2 :
285 trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
287 val trace_ends_with_ret_inv_rect_Type1 :
288 trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
290 val trace_ends_with_ret_inv_rect_Type0 :
291 trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
293 val trace_ends_with_ret_discr :
294 trace_ends_with_ret -> trace_ends_with_ret -> __
296 val trace_ends_with_ret_jmdiscr :
297 trace_ends_with_ret -> trace_ends_with_ret -> __
299 type trace_label_return =
300 | Tlr_base of __ * __ * trace_label_label
301 | Tlr_step of __ * __ * __ * trace_label_label * trace_label_return
302 and trace_label_label =
303 | Tll_base of trace_ends_with_ret * __ * __ * trace_any_label
304 and 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
313 val 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
318 val 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
323 val 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
328 val 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
333 val 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
338 val trace_label_label_inv_rect_Type4 :
339 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
340 (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
343 val trace_label_label_inv_rect_Type3 :
344 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
345 (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
348 val trace_label_label_inv_rect_Type2 :
349 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
350 (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
353 val trace_label_label_inv_rect_Type1 :
354 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
355 (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
358 val trace_label_label_inv_rect_Type0 :
359 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
360 (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __ -> __
363 val 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
374 val 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
385 val 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
396 val 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
407 val 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
418 val trace_label_return_discr :
419 abstract_status -> __ -> __ -> trace_label_return -> trace_label_return ->
422 val trace_label_label_discr :
423 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
424 trace_label_label -> __
426 val trace_label_return_jmdiscr :
427 abstract_status -> __ -> __ -> trace_label_return -> trace_label_return ->
430 val trace_label_label_jmdiscr :
431 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
432 trace_label_label -> __
434 val trace_any_label_jmdiscr :
435 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
436 trace_any_label -> __
439 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label -> __
442 val as_trace_any_label_length' :
443 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
447 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
451 abstract_status -> __ -> __ -> trace_label_return -> CostLabel.costlabel
453 type trace_any_call =
455 | Tac_step_call of __ * __ * __ * __ * trace_label_return * trace_any_call
456 | Tac_step_default of __ * __ * __ * trace_any_call
458 val 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
464 val 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
470 val 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
476 val 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
482 val 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
488 val 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
495 val 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
502 val 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
509 val 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
516 val 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
523 val trace_any_call_jmdiscr :
524 abstract_status -> __ -> __ -> trace_any_call -> trace_any_call -> __
526 type trace_label_call =
527 | Tlc_base of __ * __ * trace_any_call
529 val trace_label_call_rect_Type4 :
530 abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
531 trace_label_call -> 'a1
533 val trace_label_call_rect_Type5 :
534 abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
535 trace_label_call -> 'a1
537 val trace_label_call_rect_Type3 :
538 abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
539 trace_label_call -> 'a1
541 val trace_label_call_rect_Type2 :
542 abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
543 trace_label_call -> 'a1
545 val trace_label_call_rect_Type1 :
546 abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
547 trace_label_call -> 'a1
549 val trace_label_call_rect_Type0 :
550 abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
551 trace_label_call -> 'a1
553 val trace_label_call_inv_rect_Type4 :
554 abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
555 trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
557 val trace_label_call_inv_rect_Type3 :
558 abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
559 trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
561 val trace_label_call_inv_rect_Type2 :
562 abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
563 trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
565 val trace_label_call_inv_rect_Type1 :
566 abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
567 trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
569 val trace_label_call_inv_rect_Type0 :
570 abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
571 trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
573 val trace_label_call_discr :
574 abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __
576 val trace_label_call_jmdiscr :
577 abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __
580 abstract_status -> __ -> __ -> trace_label_call -> CostLabel.costlabel
582 type trace_label_diverges = __trace_label_diverges Lazy.t
583 and __trace_label_diverges =
584 | Tld_step of __ * __ * trace_label_label * trace_label_diverges
585 | Tld_base of __ * __ * __ * trace_label_call * trace_label_diverges
587 val 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 -> __ -> __
593 val 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 -> __ -> __
599 val 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 -> __ -> __
605 val 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 -> __ -> __
611 val 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 -> __ -> __
617 val trace_label_diverges_jmdiscr :
618 abstract_status -> __ -> trace_label_diverges -> trace_label_diverges -> __
621 abstract_status -> __ -> trace_label_diverges -> CostLabel.costlabel
623 type trace_whole_program =
624 | Twp_terminating of __ * __ * __ * trace_label_return
625 | Twp_diverges of __ * __ * trace_label_diverges
627 val trace_whole_program_rect_Type4 :
628 abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
629 -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
630 trace_whole_program -> 'a1
632 val trace_whole_program_rect_Type5 :
633 abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
634 -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
635 trace_whole_program -> 'a1
637 val trace_whole_program_rect_Type3 :
638 abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
639 -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
640 trace_whole_program -> 'a1
642 val trace_whole_program_rect_Type2 :
643 abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
644 -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
645 trace_whole_program -> 'a1
647 val trace_whole_program_rect_Type1 :
648 abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
649 -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
650 trace_whole_program -> 'a1
652 val trace_whole_program_rect_Type0 :
653 abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
654 -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
655 trace_whole_program -> 'a1
657 val trace_whole_program_inv_rect_Type4 :
658 abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
659 -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
660 trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
662 val trace_whole_program_inv_rect_Type3 :
663 abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
664 -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
665 trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
667 val trace_whole_program_inv_rect_Type2 :
668 abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
669 -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
670 trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
672 val trace_whole_program_inv_rect_Type1 :
673 abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
674 -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
675 trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
677 val trace_whole_program_inv_rect_Type0 :
678 abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ -> __
679 -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
680 trace_label_diverges -> __ -> __ -> 'a1) -> 'a1
682 val trace_whole_program_jmdiscr :
683 abstract_status -> __ -> trace_whole_program -> trace_whole_program -> __
686 abstract_status -> __ -> __ -> trace_any_label -> CostLabel.costlabel
689 abstract_status -> __ -> __ -> trace_label_label -> CostLabel.costlabel
693 | Taa_step of __ * __ * __ * trace_any_any
695 val trace_any_any_rect_Type4 :
696 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
697 trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
699 val trace_any_any_rect_Type3 :
700 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
701 trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
703 val trace_any_any_rect_Type2 :
704 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
705 trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
707 val trace_any_any_rect_Type1 :
708 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
709 trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
711 val trace_any_any_rect_Type0 :
712 abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
713 trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
715 val trace_any_any_inv_rect_Type4 :
716 abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
717 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
718 __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
720 val trace_any_any_inv_rect_Type3 :
721 abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
722 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
723 __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
725 val trace_any_any_inv_rect_Type2 :
726 abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
727 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
728 __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
730 val trace_any_any_inv_rect_Type1 :
731 abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
732 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
733 __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
735 val trace_any_any_inv_rect_Type0 :
736 abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
737 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
738 __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
740 val trace_any_any_jmdiscr :
741 abstract_status -> __ -> __ -> trace_any_any -> trace_any_any -> __
743 val taa_non_empty : abstract_status -> __ -> __ -> trace_any_any -> Bool.bool
745 val dpi1__o__taa_to_bool__o__inject :
746 abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair ->
749 val dpi1__o__taa_to_bool__o__bool_to_Prop__o__inject :
750 abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair -> __
753 val eject__o__taa_to_bool__o__inject :
754 abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool
757 val eject__o__taa_to_bool__o__bool_to_Prop__o__inject :
758 abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> __ Types.sig0
760 val taa_to_bool__o__bool_to_Prop__o__inject :
761 abstract_status -> __ -> __ -> trace_any_any -> __ Types.sig0
763 val taa_to_bool__o__inject :
764 abstract_status -> __ -> __ -> trace_any_any -> Bool.bool Types.sig0
766 val dpi1__o__taa_to_bool :
767 abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair ->
770 val eject__o__taa_to_bool :
771 abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool
774 abstract_status -> __ -> trace_ends_with_ret -> __ -> __ -> trace_any_any
775 -> trace_any_label -> trace_any_label
777 type intensional_event =
778 | IEVcost of CostLabel.costlabel
779 | IEVcall of AST.ident
780 | IEVtailcall of AST.ident * AST.ident
781 | IEVret of AST.ident
783 val intensional_event_rect_Type4 :
784 (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
785 AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
787 val intensional_event_rect_Type5 :
788 (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
789 AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
791 val intensional_event_rect_Type3 :
792 (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
793 AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
795 val intensional_event_rect_Type2 :
796 (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
797 AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
799 val intensional_event_rect_Type1 :
800 (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
801 AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
803 val intensional_event_rect_Type0 :
804 (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
805 AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1
807 val intensional_event_inv_rect_Type4 :
808 intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
809 -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
812 val intensional_event_inv_rect_Type3 :
813 intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
814 -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
817 val intensional_event_inv_rect_Type2 :
818 intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
819 -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
822 val intensional_event_inv_rect_Type1 :
823 intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
824 -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
827 val intensional_event_inv_rect_Type0 :
828 intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> __
829 -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __ ->
832 val intensional_event_discr : intensional_event -> intensional_event -> __
834 val intensional_event_jmdiscr : intensional_event -> intensional_event -> __
836 type as_trace = intensional_event List.list Types.sig0
839 'a1 Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0
842 'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list
845 val nil_safe : 'a1 List.list Types.sig0
848 abstract_status -> as_cost_label -> intensional_event Types.sig0
850 val observables_trace_label_return :
851 abstract_status -> __ -> __ -> trace_label_return -> AST.ident -> as_trace
853 val observables_trace_any_label :
854 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
855 AST.ident -> as_trace
857 val observables_trace_label_label :
858 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
859 AST.ident -> as_trace
861 val filter_map : ('a1 -> 'a2 Types.option) -> 'a1 List.list -> 'a2 List.list
863 val list_distribute_sig_aux : 'a1 List.list -> 'a1 Types.sig0 List.list
865 val list_distribute_sig :
866 'a1 List.list Types.sig0 -> 'a1 Types.sig0 List.list
868 val list_factor_sig : 'a1 Types.sig0 List.list -> 'a1 List.list Types.sig0
870 val costlabels_of_observables :
871 abstract_status -> as_trace -> as_cost_label List.list
873 val flatten_trace_label_return :
874 abstract_status -> __ -> __ -> trace_label_return -> as_cost_label
877 val flatten_trace_label_label :
878 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
879 as_cost_label List.list
881 val flatten_trace_any_label :
882 abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
883 as_cost_label List.list
885 type trace_any_any_free =
887 | Taaf_step of __ * __ * __ * trace_any_any
888 | Taaf_step_jump of __ * __ * __ * trace_any_any
890 val 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
895 val 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
900 val 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
905 val 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
910 val 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
915 val 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
920 val trace_any_any_free_inv_rect_Type4 :
921 abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
922 -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
923 -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
926 val trace_any_any_free_inv_rect_Type3 :
927 abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
928 -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
929 -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
932 val trace_any_any_free_inv_rect_Type2 :
933 abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
934 -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
935 -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
938 val trace_any_any_free_inv_rect_Type1 :
939 abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
940 -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
941 -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
944 val trace_any_any_free_inv_rect_Type0 :
945 abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ -> __
946 -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
947 -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ -> __
950 val trace_any_any_free_jmdiscr :
951 abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any_free ->
955 abstract_status -> __ -> __ -> trace_any_any_free -> Bool.bool
958 abstract_status -> __ -> __ -> __ -> trace_any_any -> trace_any_any ->
962 abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any
964 val taaf_append_tal :
965 abstract_status -> __ -> trace_ends_with_ret -> __ -> __ ->
966 trace_any_any_free -> trace_any_label -> trace_any_label
968 val taaf_append_taa :
969 abstract_status -> __ -> __ -> __ -> trace_any_any_free -> trace_any_any ->
973 abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
976 val taaf_append_taaf :
977 abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
978 trace_any_any_free -> trace_any_any_free