extracted/structuredTraces.mli

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Relations
  12
  13 open Bool
  14
  15 open Jmeq
  16
  17 open Proper
  18
  19 open PositiveMap
  20
  21 open Deqsets
  22
  23 open ErrorMessages
  24
  25 open PreIdentifiers
  26
  27 open Errors
  28
  29 open Extralib
  30
  31 open Setoids
  32
  33 open Monad
  34
  35 open Option
  36
  37 open Div_and_mod
  38
  39 open Russell
  40
  41 open Util
  42
  43 open List
  44
  45 open Lists
  46
  47 open Nat
  48
  49 open Positive
  50
  51 open Types
  52
  53 open Identifiers
  54
  55 open CostLabel
  56
  57 open Sets
  58
  59 open Listb
  60
  61 open Integers
  62
  63 open AST
  64
  65 open Division
  66
  67 open Exp
  68
  69 open Arithmetic
  70
  71 open Extranat
  72
  73 open Vector
  74
  75 open FoldStuff
  76
  77 open BitVector
  78
  79 open Z
  80
  81 open BitVectorZ
  82
  83 open Pointers
  84
  85 open Coqlib
  86
  87 open Values
  88
  89 open Events
  90
  91 open IOMonad
  92
  93 open IO
  94
  95 open Hide
  96
  97 type status_class =
  98 | Cl_return
  99 | Cl_jump
 100 | Cl_call
 101 | Cl_tailcall
 102 | Cl_other
 103
 104 val status_class_rect_Type4 :
 105   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
 106
 107 val status_class_rect_Type5 :
 108   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
 109
 110 val status_class_rect_Type3 :
 111   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
 112
 113 val status_class_rect_Type2 :
 114   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
 115
 116 val status_class_rect_Type1 :
 117   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
 118
 119 val status_class_rect_Type0 :
 120   'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1
 121
 122 val status_class_inv_rect_Type4 :
 123   status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 124   (__ -> 'a1) -> 'a1
 125
 126 val status_class_inv_rect_Type3 :
 127   status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 128   (__ -> 'a1) -> 'a1
 129
 130 val status_class_inv_rect_Type2 :
 131   status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 132   (__ -> 'a1) -> 'a1
 133
 134 val status_class_inv_rect_Type1 :
 135   status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 136   (__ -> 'a1) -> 'a1
 137
 138 val status_class_inv_rect_Type0 :
 139   status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) ->
 140   (__ -> 'a1) -> 'a1
 141
 142 val status_class_discr : status_class -> status_class -> __
 143
 144 val status_class_jmdiscr : status_class -> status_class -> __
 145
 146 type 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
 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
 159
 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
 165
 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
 171
 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
 177
 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
 183
 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
 189
 190 type as_status
 191
 192 val as_pc : abstract_status -> Deqsets.deqSet
 193
 194 val as_pc_of : abstract_status -> __ -> __
 195
 196 val as_classify : abstract_status -> __ -> status_class
 197
 198 val as_label_of_pc :
 199   abstract_status -> __ -> CostLabel.costlabel Types.option
 200
 201 val as_result : abstract_status -> __ -> Integers.int Types.option
 202
 203 val as_call_ident : abstract_status -> __ Types.sig0 -> AST.ident
 204
 205 val as_tailcall_ident : abstract_status -> __ Types.sig0 -> AST.ident
 206
 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
 212
 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
 218
 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
 224
 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
 230
 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
 236
 237 val abstract_status_jmdiscr : abstract_status -> abstract_status -> __
 238
 239 val as_label : abstract_status -> __ -> CostLabel.costlabel Types.option
 240
 241 val as_costed_exc : abstract_status -> __ -> (__, __) Types.sum
 242
 243 type as_cost_label = CostLabel.costlabel Types.sig0
 244
 245 type as_cost_labels = as_cost_label List.list
 246
 247 val as_cost_get_label :
 248   abstract_status -> as_cost_label -> CostLabel.costlabel
 249
 250 type as_cost_map = as_cost_label -> Nat.nat
 251
 252 val as_label_safe : abstract_status -> __ Types.sig0 -> as_cost_label
 253
 254 val lift_sigma_map_id :
 255   'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1
 256   Types.sig0 -> 'a2
 257
 258 val lift_cost_map_id :
 259   abstract_status -> abstract_status -> (CostLabel.costlabel -> (__, __)
 260   Types.sum) -> as_cost_map -> as_cost_map
 261
 262 type trace_ends_with_ret =
 263 | Ends_with_ret
 264 | Doesnt_end_with_ret
 265
 266 val trace_ends_with_ret_rect_Type4 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
 267
 268 val trace_ends_with_ret_rect_Type5 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
 269
 270 val trace_ends_with_ret_rect_Type3 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
 271
 272 val trace_ends_with_ret_rect_Type2 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
 273
 274 val trace_ends_with_ret_rect_Type1 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
 275
 276 val trace_ends_with_ret_rect_Type0 : 'a1 -> 'a1 -> trace_ends_with_ret -> 'a1
 277
 278 val trace_ends_with_ret_inv_rect_Type4 :
 279   trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 280
 281 val trace_ends_with_ret_inv_rect_Type3 :
 282   trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 283
 284 val trace_ends_with_ret_inv_rect_Type2 :
 285   trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 286
 287 val trace_ends_with_ret_inv_rect_Type1 :
 288   trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 289
 290 val trace_ends_with_ret_inv_rect_Type0 :
 291   trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 292
 293 val trace_ends_with_ret_discr :
 294   trace_ends_with_ret -> trace_ends_with_ret -> __
 295
 296 val trace_ends_with_ret_jmdiscr :
 297   trace_ends_with_ret -> trace_ends_with_ret -> __
 298
 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
 312
 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
 317
 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
 322
 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
 327
 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
 332
 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
 337
 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 -> __ -> __ -> __ -> __
 341   -> __ -> 'a1) -> 'a1
 342
 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 -> __ -> __ -> __ -> __
 346   -> __ -> 'a1) -> 'a1
 347
 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 -> __ -> __ -> __ -> __
 351   -> __ -> 'a1) -> 'a1
 352
 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 -> __ -> __ -> __ -> __
 356   -> __ -> 'a1) -> 'a1
 357
 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 -> __ -> __ -> __ -> __
 361   -> __ -> 'a1) -> 'a1
 362
 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
 373
 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
 384
 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
 395
 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
 406
 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
 417
 418 val trace_label_return_discr :
 419   abstract_status -> __ -> __ -> trace_label_return -> trace_label_return ->
 420   __
 421
 422 val trace_label_label_discr :
 423   abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
 424   trace_label_label -> __
 425
 426 val trace_label_return_jmdiscr :
 427   abstract_status -> __ -> __ -> trace_label_return -> trace_label_return ->
 428   __
 429
 430 val trace_label_label_jmdiscr :
 431   abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
 432   trace_label_label -> __
 433
 434 val trace_any_label_jmdiscr :
 435   abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
 436   trace_any_label -> __
 437
 438 val tal_pc_list :
 439   abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label -> __
 440   List.list
 441
 442 val as_trace_any_label_length' :
 443   abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
 444   Nat.nat
 445
 446 val tll_hd_label :
 447   abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
 448   CostLabel.costlabel
 449
 450 val tlr_hd_label :
 451   abstract_status -> __ -> __ -> trace_label_return -> CostLabel.costlabel
 452
 453 type 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
 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
 463
 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
 469
 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
 475
 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
 481
 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
 487
 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
 494
 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
 501
 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
 508
 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
 515
 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
 522
 523 val trace_any_call_jmdiscr :
 524   abstract_status -> __ -> __ -> trace_any_call -> trace_any_call -> __
 525
 526 type trace_label_call =
 527 | Tlc_base of __ * __ * trace_any_call
 528
 529 val trace_label_call_rect_Type4 :
 530   abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
 531   trace_label_call -> 'a1
 532
 533 val trace_label_call_rect_Type5 :
 534   abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
 535   trace_label_call -> 'a1
 536
 537 val trace_label_call_rect_Type3 :
 538   abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
 539   trace_label_call -> 'a1
 540
 541 val trace_label_call_rect_Type2 :
 542   abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
 543   trace_label_call -> 'a1
 544
 545 val trace_label_call_rect_Type1 :
 546   abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
 547   trace_label_call -> 'a1
 548
 549 val trace_label_call_rect_Type0 :
 550   abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __ ->
 551   trace_label_call -> 'a1
 552
 553 val trace_label_call_inv_rect_Type4 :
 554   abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
 555   trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 556
 557 val trace_label_call_inv_rect_Type3 :
 558   abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
 559   trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 560
 561 val trace_label_call_inv_rect_Type2 :
 562   abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
 563   trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 564
 565 val trace_label_call_inv_rect_Type1 :
 566   abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
 567   trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 568
 569 val trace_label_call_inv_rect_Type0 :
 570   abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
 571   trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 572
 573 val trace_label_call_discr :
 574   abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __
 575
 576 val trace_label_call_jmdiscr :
 577   abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __
 578
 579 val tlc_hd_label :
 580   abstract_status -> __ -> __ -> trace_label_call -> CostLabel.costlabel
 581
 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
 586
 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 -> __ -> __
 591   -> 'a1) -> 'a1
 592
 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 -> __ -> __
 597   -> 'a1) -> 'a1
 598
 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 -> __ -> __
 603   -> 'a1) -> 'a1
 604
 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 -> __ -> __
 609   -> 'a1) -> 'a1
 610
 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 -> __ -> __
 615   -> 'a1) -> 'a1
 616
 617 val trace_label_diverges_jmdiscr :
 618   abstract_status -> __ -> trace_label_diverges -> trace_label_diverges -> __
 619
 620 val tld_hd_label :
 621   abstract_status -> __ -> trace_label_diverges -> CostLabel.costlabel
 622
 623 type trace_whole_program =
 624 | Twp_terminating of __ * __ * __ * trace_label_return
 625 | Twp_diverges of __ * __ * trace_label_diverges
 626
 627 val trace_whole_program_rect_Type4 :
 628   abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
 629   -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
 630   trace_whole_program -> 'a1
 631
 632 val trace_whole_program_rect_Type5 :
 633   abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
 634   -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
 635   trace_whole_program -> 'a1
 636
 637 val trace_whole_program_rect_Type3 :
 638   abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
 639   -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
 640   trace_whole_program -> 'a1
 641
 642 val trace_whole_program_rect_Type2 :
 643   abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
 644   -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
 645   trace_whole_program -> 'a1
 646
 647 val trace_whole_program_rect_Type1 :
 648   abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
 649   -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
 650   trace_whole_program -> 'a1
 651
 652 val trace_whole_program_rect_Type0 :
 653   abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __
 654   -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __ ->
 655   trace_whole_program -> 'a1
 656
 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
 661
 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
 666
 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
 671
 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
 676
 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
 681
 682 val trace_whole_program_jmdiscr :
 683   abstract_status -> __ -> trace_whole_program -> trace_whole_program -> __
 684
 685 val tal_tl_label :
 686   abstract_status -> __ -> __ -> trace_any_label -> CostLabel.costlabel
 687
 688 val tll_tl_label :
 689   abstract_status -> __ -> __ -> trace_label_label -> CostLabel.costlabel
 690
 691 type trace_any_any =
 692 | Taa_base of __
 693 | Taa_step of __ * __ * __ * trace_any_any
 694
 695 val trace_any_any_rect_Type4 :
 696   abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
 697   trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
 698
 699 val trace_any_any_rect_Type3 :
 700   abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
 701   trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
 702
 703 val trace_any_any_rect_Type2 :
 704   abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
 705   trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
 706
 707 val trace_any_any_rect_Type1 :
 708   abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
 709   trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
 710
 711 val trace_any_any_rect_Type0 :
 712   abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
 713   trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1
 714
 715 val trace_any_any_inv_rect_Type4 :
 716   abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
 717   'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
 718   __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
 719
 720 val trace_any_any_inv_rect_Type3 :
 721   abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
 722   'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
 723   __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
 724
 725 val trace_any_any_inv_rect_Type2 :
 726   abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
 727   'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
 728   __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
 729
 730 val trace_any_any_inv_rect_Type1 :
 731   abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
 732   'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
 733   __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
 734
 735 val trace_any_any_inv_rect_Type0 :
 736   abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
 737   'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __ ->
 738   __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1
 739
 740 val trace_any_any_jmdiscr :
 741   abstract_status -> __ -> __ -> trace_any_any -> trace_any_any -> __
 742
 743 val taa_non_empty : abstract_status -> __ -> __ -> trace_any_any -> Bool.bool
 744
 745 val dpi1__o__taa_to_bool__o__inject :
 746   abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair ->
 747   Bool.bool Types.sig0
 748
 749 val dpi1__o__taa_to_bool__o__bool_to_Prop__o__inject :
 750   abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair -> __
 751   Types.sig0
 752
 753 val eject__o__taa_to_bool__o__inject :
 754   abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool
 755   Types.sig0
 756
 757 val eject__o__taa_to_bool__o__bool_to_Prop__o__inject :
 758   abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> __ Types.sig0
 759
 760 val taa_to_bool__o__bool_to_Prop__o__inject :
 761   abstract_status -> __ -> __ -> trace_any_any -> __ Types.sig0
 762
 763 val taa_to_bool__o__inject :
 764   abstract_status -> __ -> __ -> trace_any_any -> Bool.bool Types.sig0
 765
 766 val dpi1__o__taa_to_bool :
 767   abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair ->
 768   Bool.bool
 769
 770 val eject__o__taa_to_bool :
 771   abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool
 772
 773 val taa_append_tal :
 774   abstract_status -> __ -> trace_ends_with_ret -> __ -> __ -> trace_any_any
 775   -> trace_any_label -> trace_any_label
 776
 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
 782
 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
 786
 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
 790
 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
 794
 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
 798
 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
 802
 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
 806
 807 val 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
 812 val 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
 817 val 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
 822 val 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
 827 val 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
 832 val intensional_event_discr : intensional_event -> intensional_event -> __
 833
 834 val intensional_event_jmdiscr : intensional_event -> intensional_event -> __
 835
 836 type as_trace = intensional_event List.list Types.sig0
 837
 838 val cons_safe :
 839   'a1 Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0
 840
 841 val append_safe :
 842   'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list
 843   Types.sig0
 844
 845 val nil_safe : 'a1 List.list Types.sig0
 846
 847 val emittable_cost :
 848   abstract_status -> as_cost_label -> intensional_event Types.sig0
 849
 850 val observables_trace_label_return :
 851   abstract_status -> __ -> __ -> trace_label_return -> AST.ident -> as_trace
 852
 853 val observables_trace_any_label :
 854   abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
 855   AST.ident -> as_trace
 856
 857 val observables_trace_label_label :
 858   abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
 859   AST.ident -> as_trace
 860
 861 val filter_map : ('a1 -> 'a2 Types.option) -> 'a1 List.list -> 'a2 List.list
 862
 863 val list_distribute_sig_aux : 'a1 List.list -> 'a1 Types.sig0 List.list
 864
 865 val list_distribute_sig :
 866   'a1 List.list Types.sig0 -> 'a1 Types.sig0 List.list
 867
 868 val list_factor_sig : 'a1 Types.sig0 List.list -> 'a1 List.list Types.sig0
 869
 870 val costlabels_of_observables :
 871   abstract_status -> as_trace -> as_cost_label List.list
 872
 873 val flatten_trace_label_return :
 874   abstract_status -> __ -> __ -> trace_label_return -> as_cost_label
 875   List.list
 876
 877 val flatten_trace_label_label :
 878   abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label ->
 879   as_cost_label List.list
 880
 881 val flatten_trace_any_label :
 882   abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
 883   as_cost_label List.list
 884
 885 type trace_any_any_free =
 886 | Taaf_base of __
 887 | Taaf_step of __ * __ * __ * trace_any_any
 888 | Taaf_step_jump of __ * __ * __ * trace_any_any
 889
 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
 894
 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
 899
 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
 904
 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
 909
 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
 914
 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
 919
 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 -> __ -> __ -> __ -> __ -> __
 924   -> __ -> 'a1) -> 'a1
 925
 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 -> __ -> __ -> __ -> __ -> __
 930   -> __ -> 'a1) -> 'a1
 931
 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 -> __ -> __ -> __ -> __ -> __
 936   -> __ -> 'a1) -> 'a1
 937
 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 -> __ -> __ -> __ -> __ -> __
 942   -> __ -> 'a1) -> 'a1
 943
 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 -> __ -> __ -> __ -> __ -> __
 948   -> __ -> 'a1) -> 'a1
 949
 950 val trace_any_any_free_jmdiscr :
 951   abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any_free ->
 952   __
 953
 954 val taaf_non_empty :
 955   abstract_status -> __ -> __ -> trace_any_any_free -> Bool.bool
 956
 957 val taa_append_taa :
 958   abstract_status -> __ -> __ -> __ -> trace_any_any -> trace_any_any ->
 959   trace_any_any
 960
 961 val taaf_to_taa :
 962   abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any
 963
 964 val taaf_append_tal :
 965   abstract_status -> __ -> trace_ends_with_ret -> __ -> __ ->
 966   trace_any_any_free -> trace_any_label -> trace_any_label
 967
 968 val taaf_append_taa :
 969   abstract_status -> __ -> __ -> __ -> trace_any_any_free -> trace_any_any ->
 970   trace_any_any
 971
 972 val taaf_cons :
 973   abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
 974   trace_any_any_free
 975
 976 val taaf_append_taaf :
 977   abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
 978   trace_any_any_free -> trace_any_any_free
 979