extracted/structuredTraces.ml

   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 let rec status_class_rect_Type4 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
 107 | Cl_return -> h_cl_return
 108 | Cl_jump -> h_cl_jump
 109 | Cl_call -> h_cl_call
 110 | Cl_tailcall -> h_cl_tailcall
 111 | Cl_other -> h_cl_other
 112
 113 (** val status_class_rect_Type5 :
 114     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
 115 let rec status_class_rect_Type5 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
 116 | Cl_return -> h_cl_return
 117 | Cl_jump -> h_cl_jump
 118 | Cl_call -> h_cl_call
 119 | Cl_tailcall -> h_cl_tailcall
 120 | Cl_other -> h_cl_other
 121
 122 (** val status_class_rect_Type3 :
 123     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
 124 let rec status_class_rect_Type3 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
 125 | Cl_return -> h_cl_return
 126 | Cl_jump -> h_cl_jump
 127 | Cl_call -> h_cl_call
 128 | Cl_tailcall -> h_cl_tailcall
 129 | Cl_other -> h_cl_other
 130
 131 (** val status_class_rect_Type2 :
 132     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
 133 let rec status_class_rect_Type2 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
 134 | Cl_return -> h_cl_return
 135 | Cl_jump -> h_cl_jump
 136 | Cl_call -> h_cl_call
 137 | Cl_tailcall -> h_cl_tailcall
 138 | Cl_other -> h_cl_other
 139
 140 (** val status_class_rect_Type1 :
 141     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
 142 let rec status_class_rect_Type1 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
 143 | Cl_return -> h_cl_return
 144 | Cl_jump -> h_cl_jump
 145 | Cl_call -> h_cl_call
 146 | Cl_tailcall -> h_cl_tailcall
 147 | Cl_other -> h_cl_other
 148
 149 (** val status_class_rect_Type0 :
 150     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> status_class -> 'a1 **)
 151 let rec status_class_rect_Type0 h_cl_return h_cl_jump h_cl_call h_cl_tailcall h_cl_other = function
 152 | Cl_return -> h_cl_return
 153 | Cl_jump -> h_cl_jump
 154 | Cl_call -> h_cl_call
 155 | Cl_tailcall -> h_cl_tailcall
 156 | Cl_other -> h_cl_other
 157
 158 (** val status_class_inv_rect_Type4 :
 159     status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 160     -> (__ -> 'a1) -> 'a1 **)
 161 let status_class_inv_rect_Type4 hterm h1 h2 h3 h4 h5 =
 162   let hcut = status_class_rect_Type4 h1 h2 h3 h4 h5 hterm in hcut __
 163
 164 (** val status_class_inv_rect_Type3 :
 165     status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 166     -> (__ -> 'a1) -> 'a1 **)
 167 let status_class_inv_rect_Type3 hterm h1 h2 h3 h4 h5 =
 168   let hcut = status_class_rect_Type3 h1 h2 h3 h4 h5 hterm in hcut __
 169
 170 (** val status_class_inv_rect_Type2 :
 171     status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 172     -> (__ -> 'a1) -> 'a1 **)
 173 let status_class_inv_rect_Type2 hterm h1 h2 h3 h4 h5 =
 174   let hcut = status_class_rect_Type2 h1 h2 h3 h4 h5 hterm in hcut __
 175
 176 (** val status_class_inv_rect_Type1 :
 177     status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 178     -> (__ -> 'a1) -> 'a1 **)
 179 let status_class_inv_rect_Type1 hterm h1 h2 h3 h4 h5 =
 180   let hcut = status_class_rect_Type1 h1 h2 h3 h4 h5 hterm in hcut __
 181
 182 (** val status_class_inv_rect_Type0 :
 183     status_class -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 184     -> (__ -> 'a1) -> 'a1 **)
 185 let status_class_inv_rect_Type0 hterm h1 h2 h3 h4 h5 =
 186   let hcut = status_class_rect_Type0 h1 h2 h3 h4 h5 hterm in hcut __
 187
 188 (** val status_class_discr : status_class -> status_class -> __ **)
 189 let status_class_discr x y =
 190   Logic.eq_rect_Type2 x
 191     (match x with
 192      | Cl_return -> Obj.magic (fun _ dH -> dH)
 193      | Cl_jump -> Obj.magic (fun _ dH -> dH)
 194      | Cl_call -> Obj.magic (fun _ dH -> dH)
 195      | Cl_tailcall -> Obj.magic (fun _ dH -> dH)
 196      | Cl_other -> Obj.magic (fun _ dH -> dH)) y
 197
 198 (** val status_class_jmdiscr : status_class -> status_class -> __ **)
 199 let status_class_jmdiscr x y =
 200   Logic.eq_rect_Type2 x
 201     (match x with
 202      | Cl_return -> Obj.magic (fun _ dH -> dH)
 203      | Cl_jump -> Obj.magic (fun _ dH -> dH)
 204      | Cl_call -> Obj.magic (fun _ dH -> dH)
 205      | Cl_tailcall -> Obj.magic (fun _ dH -> dH)
 206      | Cl_other -> Obj.magic (fun _ dH -> dH)) y
 207
 208 type abstract_status = { as_pc : Deqsets.deqSet; as_pc_of : (__ -> __);
 209                          as_classify : (__ -> status_class);
 210                          as_label_of_pc : (__ -> CostLabel.costlabel
 211                                           Types.option);
 212                          as_result : (__ -> Integers.int Types.option);
 213                          as_call_ident : (__ Types.sig0 -> AST.ident);
 214                          as_tailcall_ident : (__ Types.sig0 -> AST.ident) }
 215
 216 (** val abstract_status_rect_Type4 :
 217     (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
 218     -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
 219     Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
 220     AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
 221 let rec abstract_status_rect_Type4 h_mk_abstract_status x_22380 =
 222   let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
 223     as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
 224     as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22380
 225   in
 226   h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
 227     as_result0 as_call_ident0 as_tailcall_ident0
 228
 229 (** val abstract_status_rect_Type5 :
 230     (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
 231     -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
 232     Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
 233     AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
 234 let rec abstract_status_rect_Type5 h_mk_abstract_status x_22382 =
 235   let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
 236     as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
 237     as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22382
 238   in
 239   h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
 240     as_result0 as_call_ident0 as_tailcall_ident0
 241
 242 (** val abstract_status_rect_Type3 :
 243     (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
 244     -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
 245     Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
 246     AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
 247 let rec abstract_status_rect_Type3 h_mk_abstract_status x_22384 =
 248   let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
 249     as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
 250     as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22384
 251   in
 252   h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
 253     as_result0 as_call_ident0 as_tailcall_ident0
 254
 255 (** val abstract_status_rect_Type2 :
 256     (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
 257     -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
 258     Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
 259     AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
 260 let rec abstract_status_rect_Type2 h_mk_abstract_status x_22386 =
 261   let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
 262     as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
 263     as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22386
 264   in
 265   h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
 266     as_result0 as_call_ident0 as_tailcall_ident0
 267
 268 (** val abstract_status_rect_Type1 :
 269     (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
 270     -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
 271     Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
 272     AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
 273 let rec abstract_status_rect_Type1 h_mk_abstract_status x_22388 =
 274   let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
 275     as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
 276     as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22388
 277   in
 278   h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
 279     as_result0 as_call_ident0 as_tailcall_ident0
 280
 281 (** val abstract_status_rect_Type0 :
 282     (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class) -> (__
 283     -> CostLabel.costlabel Types.option) -> __ -> (__ -> Integers.int
 284     Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
 285     AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
 286 let rec abstract_status_rect_Type0 h_mk_abstract_status x_22390 =
 287   let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
 288     as_label_of_pc = as_label_of_pc0; as_result = as_result0; as_call_ident =
 289     as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_22390
 290   in
 291   h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
 292     as_result0 as_call_ident0 as_tailcall_ident0
 293
 294 type as_status = __
 295
 296 (** val as_pc : abstract_status -> Deqsets.deqSet **)
 297 let rec as_pc xxx =
 298   xxx.as_pc
 299
 300 (** val as_pc_of : abstract_status -> __ -> __ **)
 301 let rec as_pc_of xxx =
 302   xxx.as_pc_of
 303
 304 (** val as_classify : abstract_status -> __ -> status_class **)
 305 let rec as_classify xxx =
 306   xxx.as_classify
 307
 308 (** val as_label_of_pc :
 309     abstract_status -> __ -> CostLabel.costlabel Types.option **)
 310 let rec as_label_of_pc xxx =
 311   xxx.as_label_of_pc
 312
 313 (** val as_result : abstract_status -> __ -> Integers.int Types.option **)
 314 let rec as_result xxx =
 315   xxx.as_result
 316
 317 (** val as_call_ident : abstract_status -> __ Types.sig0 -> AST.ident **)
 318 let rec as_call_ident xxx =
 319   xxx.as_call_ident
 320
 321 (** val as_tailcall_ident : abstract_status -> __ Types.sig0 -> AST.ident **)
 322 let rec as_tailcall_ident xxx =
 323   xxx.as_tailcall_ident
 324
 325 (** val abstract_status_inv_rect_Type4 :
 326     abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
 327     status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
 328     Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
 329     Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
 330 let abstract_status_inv_rect_Type4 hterm h1 =
 331   let hcut = abstract_status_rect_Type4 h1 hterm in hcut __
 332
 333 (** val abstract_status_inv_rect_Type3 :
 334     abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
 335     status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
 336     Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
 337     Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
 338 let abstract_status_inv_rect_Type3 hterm h1 =
 339   let hcut = abstract_status_rect_Type3 h1 hterm in hcut __
 340
 341 (** val abstract_status_inv_rect_Type2 :
 342     abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
 343     status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
 344     Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
 345     Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
 346 let abstract_status_inv_rect_Type2 hterm h1 =
 347   let hcut = abstract_status_rect_Type2 h1 hterm in hcut __
 348
 349 (** val abstract_status_inv_rect_Type1 :
 350     abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
 351     status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
 352     Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
 353     Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
 354 let abstract_status_inv_rect_Type1 hterm h1 =
 355   let hcut = abstract_status_rect_Type1 h1 hterm in hcut __
 356
 357 (** val abstract_status_inv_rect_Type0 :
 358     abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
 359     status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
 360     Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
 361     Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
 362 let abstract_status_inv_rect_Type0 hterm h1 =
 363   let hcut = abstract_status_rect_Type0 h1 hterm in hcut __
 364
 365 (** val abstract_status_jmdiscr :
 366     abstract_status -> abstract_status -> __ **)
 367 let abstract_status_jmdiscr x y =
 368   Logic.eq_rect_Type2 x
 369     (let { as_pc = a2; as_pc_of = a3; as_classify = a4; as_label_of_pc = a5;
 370        as_result = a7; as_call_ident = a8; as_tailcall_ident = a9 } = x
 371      in
 372     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y
 373
 374 (** val as_label :
 375     abstract_status -> __ -> CostLabel.costlabel Types.option **)
 376 let as_label s s0 =
 377   s.as_label_of_pc (s.as_pc_of s0)
 378
 379 (** val as_costed_exc : abstract_status -> __ -> (__, __) Types.sum **)
 380 let as_costed_exc s s0 =
 381   match as_label s s0 with
 382   | Types.None -> Types.Inr __
 383   | Types.Some c -> Types.Inl __
 384
 385 type as_cost_label = CostLabel.costlabel Types.sig0
 386
 387 type as_cost_labels = as_cost_label List.list
 388
 389 (** val as_cost_get_label :
 390     abstract_status -> as_cost_label -> CostLabel.costlabel **)
 391 let as_cost_get_label s l_sig =
 392   Types.pi1 l_sig
 393
 394 type as_cost_map = as_cost_label -> Nat.nat
 395
 396 (** val as_label_safe : abstract_status -> __ Types.sig0 -> as_cost_label **)
 397 let as_label_safe a_s st_sig =
 398   Option.opt_safe (as_label a_s (Types.pi1 st_sig))
 399
 400 (** val lift_sigma_map_id :
 401     'a2 -> ('a1 -> (__, __) Types.sum) -> ('a1 Types.sig0 -> 'a2) -> 'a1
 402     Types.sig0 -> 'a2 **)
 403 let lift_sigma_map_id dflt dec m a_sig =
 404   match dec (Types.pi1 a_sig) with
 405   | Types.Inl _ -> m (Types.pi1 a_sig)
 406   | Types.Inr _ -> dflt
 407
 408 (** val lift_cost_map_id :
 409     abstract_status -> abstract_status -> (CostLabel.costlabel -> (__, __)
 410     Types.sum) -> as_cost_map -> as_cost_map **)
 411 let lift_cost_map_id s_in s_out =
 412   lift_sigma_map_id Nat.O
 413
 414 type trace_ends_with_ret =
 415 | Ends_with_ret
 416 | Doesnt_end_with_ret
 417
 418 (** val trace_ends_with_ret_rect_Type4 :
 419     'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
 420 let rec trace_ends_with_ret_rect_Type4 h_ends_with_ret h_doesnt_end_with_ret = function
 421 | Ends_with_ret -> h_ends_with_ret
 422 | Doesnt_end_with_ret -> h_doesnt_end_with_ret
 423
 424 (** val trace_ends_with_ret_rect_Type5 :
 425     'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
 426 let rec trace_ends_with_ret_rect_Type5 h_ends_with_ret h_doesnt_end_with_ret = function
 427 | Ends_with_ret -> h_ends_with_ret
 428 | Doesnt_end_with_ret -> h_doesnt_end_with_ret
 429
 430 (** val trace_ends_with_ret_rect_Type3 :
 431     'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
 432 let rec trace_ends_with_ret_rect_Type3 h_ends_with_ret h_doesnt_end_with_ret = function
 433 | Ends_with_ret -> h_ends_with_ret
 434 | Doesnt_end_with_ret -> h_doesnt_end_with_ret
 435
 436 (** val trace_ends_with_ret_rect_Type2 :
 437     'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
 438 let rec trace_ends_with_ret_rect_Type2 h_ends_with_ret h_doesnt_end_with_ret = function
 439 | Ends_with_ret -> h_ends_with_ret
 440 | Doesnt_end_with_ret -> h_doesnt_end_with_ret
 441
 442 (** val trace_ends_with_ret_rect_Type1 :
 443     'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
 444 let rec trace_ends_with_ret_rect_Type1 h_ends_with_ret h_doesnt_end_with_ret = function
 445 | Ends_with_ret -> h_ends_with_ret
 446 | Doesnt_end_with_ret -> h_doesnt_end_with_ret
 447
 448 (** val trace_ends_with_ret_rect_Type0 :
 449     'a1 -> 'a1 -> trace_ends_with_ret -> 'a1 **)
 450 let rec trace_ends_with_ret_rect_Type0 h_ends_with_ret h_doesnt_end_with_ret = function
 451 | Ends_with_ret -> h_ends_with_ret
 452 | Doesnt_end_with_ret -> h_doesnt_end_with_ret
 453
 454 (** val trace_ends_with_ret_inv_rect_Type4 :
 455     trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 456 let trace_ends_with_ret_inv_rect_Type4 hterm h1 h2 =
 457   let hcut = trace_ends_with_ret_rect_Type4 h1 h2 hterm in hcut __
 458
 459 (** val trace_ends_with_ret_inv_rect_Type3 :
 460     trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 461 let trace_ends_with_ret_inv_rect_Type3 hterm h1 h2 =
 462   let hcut = trace_ends_with_ret_rect_Type3 h1 h2 hterm in hcut __
 463
 464 (** val trace_ends_with_ret_inv_rect_Type2 :
 465     trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 466 let trace_ends_with_ret_inv_rect_Type2 hterm h1 h2 =
 467   let hcut = trace_ends_with_ret_rect_Type2 h1 h2 hterm in hcut __
 468
 469 (** val trace_ends_with_ret_inv_rect_Type1 :
 470     trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 471 let trace_ends_with_ret_inv_rect_Type1 hterm h1 h2 =
 472   let hcut = trace_ends_with_ret_rect_Type1 h1 h2 hterm in hcut __
 473
 474 (** val trace_ends_with_ret_inv_rect_Type0 :
 475     trace_ends_with_ret -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 476 let trace_ends_with_ret_inv_rect_Type0 hterm h1 h2 =
 477   let hcut = trace_ends_with_ret_rect_Type0 h1 h2 hterm in hcut __
 478
 479 (** val trace_ends_with_ret_discr :
 480     trace_ends_with_ret -> trace_ends_with_ret -> __ **)
 481 let trace_ends_with_ret_discr x y =
 482   Logic.eq_rect_Type2 x
 483     (match x with
 484      | Ends_with_ret -> Obj.magic (fun _ dH -> dH)
 485      | Doesnt_end_with_ret -> Obj.magic (fun _ dH -> dH)) y
 486
 487 (** val trace_ends_with_ret_jmdiscr :
 488     trace_ends_with_ret -> trace_ends_with_ret -> __ **)
 489 let trace_ends_with_ret_jmdiscr x y =
 490   Logic.eq_rect_Type2 x
 491     (match x with
 492      | Ends_with_ret -> Obj.magic (fun _ dH -> dH)
 493      | Doesnt_end_with_ret -> Obj.magic (fun _ dH -> dH)) y
 494
 495 type trace_label_return =
 496 | Tlr_base of __ * __ * trace_label_label
 497 | Tlr_step of __ * __ * __ * trace_label_label * trace_label_return
 498 and trace_label_label =
 499 | Tll_base of trace_ends_with_ret * __ * __ * trace_any_label
 500 and trace_any_label =
 501 | Tal_base_not_return of __ * __
 502 | Tal_base_return of __ * __
 503 | Tal_base_call of __ * __ * __ * trace_label_return
 504 | Tal_base_tailcall of __ * __ * __ * trace_label_return
 505 | Tal_step_call of trace_ends_with_ret * __ * __ * __ * __
 506    * trace_label_return * trace_any_label
 507 | Tal_step_default of trace_ends_with_ret * __ * __ * __ * trace_any_label
 508
 509 (** val trace_label_return_inv_rect_Type4 :
 510     abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
 511     trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
 512     trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 513 let trace_label_return_inv_rect_Type4 x1 x2 x3 hterm h1 h2 =
 514   let hcut =
 515     match hterm with
 516     | Tlr_base (x, x0, x4) -> h1 x x0 x4
 517     | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
 518   in
 519   hcut __ __ __
 520
 521 (** val trace_label_return_inv_rect_Type3 :
 522     abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
 523     trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
 524     trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 525 let trace_label_return_inv_rect_Type3 x1 x2 x3 hterm h1 h2 =
 526   let hcut =
 527     match hterm with
 528     | Tlr_base (x, x0, x4) -> h1 x x0 x4
 529     | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
 530   in
 531   hcut __ __ __
 532
 533 (** val trace_label_return_inv_rect_Type2 :
 534     abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
 535     trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
 536     trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 537 let trace_label_return_inv_rect_Type2 x1 x2 x3 hterm h1 h2 =
 538   let hcut =
 539     match hterm with
 540     | Tlr_base (x, x0, x4) -> h1 x x0 x4
 541     | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
 542   in
 543   hcut __ __ __
 544
 545 (** val trace_label_return_inv_rect_Type1 :
 546     abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
 547     trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
 548     trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 549 let trace_label_return_inv_rect_Type1 x1 x2 x3 hterm h1 h2 =
 550   let hcut =
 551     match hterm with
 552     | Tlr_base (x, x0, x4) -> h1 x x0 x4
 553     | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
 554   in
 555   hcut __ __ __
 556
 557 (** val trace_label_return_inv_rect_Type0 :
 558     abstract_status -> __ -> __ -> trace_label_return -> (__ -> __ ->
 559     trace_label_label -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
 560     trace_label_label -> trace_label_return -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 561 let trace_label_return_inv_rect_Type0 x1 x2 x3 hterm h1 h2 =
 562   let hcut =
 563     match hterm with
 564     | Tlr_base (x, x0, x4) -> h1 x x0 x4
 565     | Tlr_step (x, x0, x4, x5, x6) -> h2 x x0 x4 x5 x6
 566   in
 567   hcut __ __ __
 568
 569 (** val trace_label_label_inv_rect_Type4 :
 570     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
 571     -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
 572     -> __ -> __ -> 'a1) -> 'a1 **)
 573 let trace_label_label_inv_rect_Type4 x1 x2 x3 x4 hterm h1 =
 574   let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
 575   hcut __ __ __ __
 576
 577 (** val trace_label_label_inv_rect_Type3 :
 578     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
 579     -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
 580     -> __ -> __ -> 'a1) -> 'a1 **)
 581 let trace_label_label_inv_rect_Type3 x1 x2 x3 x4 hterm h1 =
 582   let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
 583   hcut __ __ __ __
 584
 585 (** val trace_label_label_inv_rect_Type2 :
 586     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
 587     -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
 588     -> __ -> __ -> 'a1) -> 'a1 **)
 589 let trace_label_label_inv_rect_Type2 x1 x2 x3 x4 hterm h1 =
 590   let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
 591   hcut __ __ __ __
 592
 593 (** val trace_label_label_inv_rect_Type1 :
 594     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
 595     -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
 596     -> __ -> __ -> 'a1) -> 'a1 **)
 597 let trace_label_label_inv_rect_Type1 x1 x2 x3 x4 hterm h1 =
 598   let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
 599   hcut __ __ __ __
 600
 601 (** val trace_label_label_inv_rect_Type0 :
 602     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
 603     -> (trace_ends_with_ret -> __ -> __ -> trace_any_label -> __ -> __ -> __
 604     -> __ -> __ -> 'a1) -> 'a1 **)
 605 let trace_label_label_inv_rect_Type0 x1 x2 x3 x4 hterm h1 =
 606   let hcut = let Tll_base (x, x0, x5, x6) = hterm in h1 x x0 x5 x6 __ in
 607   hcut __ __ __ __
 608
 609 (** val trace_any_label_inv_rect_Type4 :
 610     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
 611     (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
 612     -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
 613     __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 614     (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
 615     -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
 616     -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
 617     'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
 618     -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 619 let trace_any_label_inv_rect_Type4 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
 620   let hcut =
 621     match hterm with
 622     | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
 623     | Tal_base_return (x, x0) -> h2 x x0 __ __
 624     | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
 625     | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
 626     | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
 627       h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
 628     | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
 629   in
 630   hcut __ __ __ __
 631
 632 (** val trace_any_label_inv_rect_Type3 :
 633     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
 634     (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
 635     -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
 636     __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 637     (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
 638     -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
 639     -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
 640     'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
 641     -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 642 let trace_any_label_inv_rect_Type3 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
 643   let hcut =
 644     match hterm with
 645     | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
 646     | Tal_base_return (x, x0) -> h2 x x0 __ __
 647     | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
 648     | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
 649     | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
 650       h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
 651     | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
 652   in
 653   hcut __ __ __ __
 654
 655 (** val trace_any_label_inv_rect_Type2 :
 656     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
 657     (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
 658     -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
 659     __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 660     (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
 661     -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
 662     -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
 663     'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
 664     -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 665 let trace_any_label_inv_rect_Type2 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
 666   let hcut =
 667     match hterm with
 668     | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
 669     | Tal_base_return (x, x0) -> h2 x x0 __ __
 670     | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
 671     | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
 672     | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
 673       h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
 674     | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
 675   in
 676   hcut __ __ __ __
 677
 678 (** val trace_any_label_inv_rect_Type1 :
 679     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
 680     (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
 681     -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
 682     __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 683     (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
 684     -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
 685     -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
 686     'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
 687     -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 688 let trace_any_label_inv_rect_Type1 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
 689   let hcut =
 690     match hterm with
 691     | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
 692     | Tal_base_return (x, x0) -> h2 x x0 __ __
 693     | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
 694     | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
 695     | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
 696       h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
 697     | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
 698   in
 699   hcut __ __ __ __
 700
 701 (** val trace_any_label_inv_rect_Type0 :
 702     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
 703     (__ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __
 704     -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ ->
 705     __ -> __ -> trace_label_return -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
 706     (__ -> __ -> __ -> __ -> __ -> trace_label_return -> __ -> __ -> __ -> __
 707     -> 'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> __ -> __ -> __
 708     -> trace_label_return -> __ -> trace_any_label -> __ -> __ -> __ -> __ ->
 709     'a1) -> (trace_ends_with_ret -> __ -> __ -> __ -> __ -> trace_any_label
 710     -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 711 let trace_any_label_inv_rect_Type0 x1 x2 x3 x4 hterm h1 h2 h3 h4 h5 h6 =
 712   let hcut =
 713     match hterm with
 714     | Tal_base_not_return (x, x0) -> h1 x x0 __ __ __
 715     | Tal_base_return (x, x0) -> h2 x x0 __ __
 716     | Tal_base_call (x, x0, x5, x6) -> h3 x x0 x5 __ __ __ x6 __
 717     | Tal_base_tailcall (x, x0, x5, x6) -> h4 x x0 x5 __ __ x6
 718     | Tal_step_call (x, x0, x5, x6, x7, x8, x9) ->
 719       h5 x x0 x5 x6 x7 __ __ __ x8 __ x9
 720     | Tal_step_default (x, x0, x5, x6, x7) -> h6 x x0 x5 x6 __ x7 __ __
 721   in
 722   hcut __ __ __ __
 723
 724 (** val trace_label_return_discr :
 725     abstract_status -> __ -> __ -> trace_label_return -> trace_label_return
 726     -> __ **)
 727 let trace_label_return_discr a1 a2 a3 x y =
 728   Logic.eq_rect_Type2 x
 729     (match x with
 730      | Tlr_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
 731      | Tlr_step (a0, a10, a20, a30, a4) ->
 732        Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 733
 734 (** val trace_label_label_discr :
 735     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
 736     -> trace_label_label -> __ **)
 737 let trace_label_label_discr a1 a2 a3 a4 x y =
 738   Logic.eq_rect_Type2 x
 739     (let Tll_base (a0, a10, a20, a30) = x in
 740     Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 741
 742 (** val trace_label_return_jmdiscr :
 743     abstract_status -> __ -> __ -> trace_label_return -> trace_label_return
 744     -> __ **)
 745 let trace_label_return_jmdiscr a1 a2 a3 x y =
 746   Logic.eq_rect_Type2 x
 747     (match x with
 748      | Tlr_base (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
 749      | Tlr_step (a0, a10, a20, a30, a4) ->
 750        Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 751
 752 (** val trace_label_label_jmdiscr :
 753     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
 754     -> trace_label_label -> __ **)
 755 let trace_label_label_jmdiscr a1 a2 a3 a4 x y =
 756   Logic.eq_rect_Type2 x
 757     (let Tll_base (a0, a10, a20, a30) = x in
 758     Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 759
 760 (** val trace_any_label_jmdiscr :
 761     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
 762     trace_any_label -> __ **)
 763 let trace_any_label_jmdiscr a1 a2 a3 a4 x y =
 764   Logic.eq_rect_Type2 x
 765     (match x with
 766      | Tal_base_not_return (a0, a10) ->
 767        Obj.magic (fun _ dH -> dH __ __ __ __ __)
 768      | Tal_base_return (a0, a10) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 769      | Tal_base_call (a0, a10, a20, a6) ->
 770        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
 771      | Tal_base_tailcall (a0, a10, a20, a5) ->
 772        Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
 773      | Tal_step_call (a0, a10, a20, a30, a40, a8, a100) ->
 774        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __)
 775      | Tal_step_default (a0, a10, a20, a30, a5) ->
 776        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)) y
 777
 778 (** val tal_pc_list :
 779     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
 780     __ List.list **)
 781 let rec tal_pc_list s fl st1 st2 = function
 782 | Tal_base_not_return (pre, x) -> List.Cons ((s.as_pc_of pre), List.Nil)
 783 | Tal_base_return (pre, x) -> List.Cons ((s.as_pc_of pre), List.Nil)
 784 | Tal_base_call (pre, x, x0, x4) -> List.Cons ((s.as_pc_of pre), List.Nil)
 785 | Tal_base_tailcall (pre, x, x0, x3) ->
 786   List.Cons ((s.as_pc_of pre), List.Nil)
 787 | Tal_step_call (fl', pre, x, st1', st2', x3, tl) ->
 788   List.Cons ((s.as_pc_of pre), (tal_pc_list s fl' st1' st2' tl))
 789 | Tal_step_default (fl', pre, st1', st2', tl) ->
 790   List.Cons ((s.as_pc_of pre), (tal_pc_list s fl' st1' st2' tl))
 791
 792 (** val as_trace_any_label_length' :
 793     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
 794     Nat.nat **)
 795 let as_trace_any_label_length' s trace_ends_flag start_status final_status the_trace =
 796   List.length
 797     (tal_pc_list s trace_ends_flag start_status final_status the_trace)
 798
 799 (** val tll_hd_label :
 800     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
 801     -> CostLabel.costlabel **)
 802 let tll_hd_label s fl st1 st2 tr =
 803   (let Tll_base (x, st1', x0, x1) = tr in
 804   (fun _ _ _ _ -> Types.pi1 (as_label_safe s st1'))) __ __ __ __
 805
 806 (** val tlr_hd_label :
 807     abstract_status -> __ -> __ -> trace_label_return -> CostLabel.costlabel **)
 808 let tlr_hd_label s st1 st2 = function
 809 | Tlr_base (st1', st2', tll) -> tll_hd_label s Ends_with_ret st1' st2' tll
 810 | Tlr_step (st1', st2', x, tll, x0) ->
 811   tll_hd_label s Doesnt_end_with_ret st1' st2' tll
 812
 813 type trace_any_call =
 814 | Tac_base of __
 815 | Tac_step_call of __ * __ * __ * __ * trace_label_return * trace_any_call
 816 | Tac_step_default of __ * __ * __ * trace_any_call
 817
 818 (** val trace_any_call_rect_Type4 :
 819     abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
 820     -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
 821     -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
 822     __ -> trace_any_call -> 'a1 **)
 823 let rec trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default x_22468 x_22467 = function
 824 | Tac_base status -> h_tac_base status __
 825 | Tac_step_call
 826     (status_pre_fun_call, status_after_fun_call, status_final,
 827      status_start_fun_call, x_22473, x_22471) ->
 828   h_tac_step_call status_pre_fun_call status_after_fun_call status_final
 829     status_start_fun_call __ __ __ x_22473 __ x_22471
 830     (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
 831       h_tac_step_default status_after_fun_call status_final x_22471)
 832 | Tac_step_default (status_pre, status_end, status_init, x_22478) ->
 833   h_tac_step_default status_pre status_end status_init __ x_22478 __ __
 834     (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
 835       h_tac_step_default status_init status_end x_22478)
 836
 837 (** val trace_any_call_rect_Type3 :
 838     abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
 839     -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
 840     -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
 841     __ -> trace_any_call -> 'a1 **)
 842 let rec trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default x_22500 x_22499 = function
 843 | Tac_base status -> h_tac_base status __
 844 | Tac_step_call
 845     (status_pre_fun_call, status_after_fun_call, status_final,
 846      status_start_fun_call, x_22505, x_22503) ->
 847   h_tac_step_call status_pre_fun_call status_after_fun_call status_final
 848     status_start_fun_call __ __ __ x_22505 __ x_22503
 849     (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
 850       h_tac_step_default status_after_fun_call status_final x_22503)
 851 | Tac_step_default (status_pre, status_end, status_init, x_22510) ->
 852   h_tac_step_default status_pre status_end status_init __ x_22510 __ __
 853     (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
 854       h_tac_step_default status_init status_end x_22510)
 855
 856 (** val trace_any_call_rect_Type2 :
 857     abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
 858     -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
 859     -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
 860     __ -> trace_any_call -> 'a1 **)
 861 let rec trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default x_22516 x_22515 = function
 862 | Tac_base status -> h_tac_base status __
 863 | Tac_step_call
 864     (status_pre_fun_call, status_after_fun_call, status_final,
 865      status_start_fun_call, x_22521, x_22519) ->
 866   h_tac_step_call status_pre_fun_call status_after_fun_call status_final
 867     status_start_fun_call __ __ __ x_22521 __ x_22519
 868     (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
 869       h_tac_step_default status_after_fun_call status_final x_22519)
 870 | Tac_step_default (status_pre, status_end, status_init, x_22526) ->
 871   h_tac_step_default status_pre status_end status_init __ x_22526 __ __
 872     (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
 873       h_tac_step_default status_init status_end x_22526)
 874
 875 (** val trace_any_call_rect_Type1 :
 876     abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
 877     -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
 878     -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
 879     __ -> trace_any_call -> 'a1 **)
 880 let rec trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default x_22532 x_22531 = function
 881 | Tac_base status -> h_tac_base status __
 882 | Tac_step_call
 883     (status_pre_fun_call, status_after_fun_call, status_final,
 884      status_start_fun_call, x_22537, x_22535) ->
 885   h_tac_step_call status_pre_fun_call status_after_fun_call status_final
 886     status_start_fun_call __ __ __ x_22537 __ x_22535
 887     (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
 888       h_tac_step_default status_after_fun_call status_final x_22535)
 889 | Tac_step_default (status_pre, status_end, status_init, x_22542) ->
 890   h_tac_step_default status_pre status_end status_init __ x_22542 __ __
 891     (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
 892       h_tac_step_default status_init status_end x_22542)
 893
 894 (** val trace_any_call_rect_Type0 :
 895     abstract_status -> (__ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __
 896     -> __ -> trace_label_return -> __ -> trace_any_call -> 'a1 -> 'a1) -> (__
 897     -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
 898     __ -> trace_any_call -> 'a1 **)
 899 let rec trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default x_22548 x_22547 = function
 900 | Tac_base status -> h_tac_base status __
 901 | Tac_step_call
 902     (status_pre_fun_call, status_after_fun_call, status_final,
 903      status_start_fun_call, x_22553, x_22551) ->
 904   h_tac_step_call status_pre_fun_call status_after_fun_call status_final
 905     status_start_fun_call __ __ __ x_22553 __ x_22551
 906     (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
 907       h_tac_step_default status_after_fun_call status_final x_22551)
 908 | Tac_step_default (status_pre, status_end, status_init, x_22558) ->
 909   h_tac_step_default status_pre status_end status_init __ x_22558 __ __
 910     (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
 911       h_tac_step_default status_init status_end x_22558)
 912
 913 (** val trace_any_call_inv_rect_Type4 :
 914     abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
 915     __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
 916     trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
 917     __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
 918     -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 919 let trace_any_call_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 =
 920   let hcut = trace_any_call_rect_Type4 x1 h1 h2 h3 x2 x3 hterm in
 921   hcut __ __ __
 922
 923 (** val trace_any_call_inv_rect_Type3 :
 924     abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
 925     __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
 926     trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
 927     __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
 928     -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 929 let trace_any_call_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 =
 930   let hcut = trace_any_call_rect_Type3 x1 h1 h2 h3 x2 x3 hterm in
 931   hcut __ __ __
 932
 933 (** val trace_any_call_inv_rect_Type2 :
 934     abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
 935     __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
 936     trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
 937     __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
 938     -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 939 let trace_any_call_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 =
 940   let hcut = trace_any_call_rect_Type2 x1 h1 h2 h3 x2 x3 hterm in
 941   hcut __ __ __
 942
 943 (** val trace_any_call_inv_rect_Type1 :
 944     abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
 945     __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
 946     trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
 947     __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
 948     -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 949 let trace_any_call_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 =
 950   let hcut = trace_any_call_rect_Type1 x1 h1 h2 h3 x2 x3 hterm in
 951   hcut __ __ __
 952
 953 (** val trace_any_call_inv_rect_Type0 :
 954     abstract_status -> __ -> __ -> trace_any_call -> (__ -> __ -> __ -> __ ->
 955     __ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> __ ->
 956     trace_label_return -> __ -> trace_any_call -> (__ -> __ -> __ -> 'a1) ->
 957     __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_any_call -> __
 958     -> __ -> (__ -> __ -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 959 let trace_any_call_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 =
 960   let hcut = trace_any_call_rect_Type0 x1 h1 h2 h3 x2 x3 hterm in
 961   hcut __ __ __
 962
 963 (** val trace_any_call_jmdiscr :
 964     abstract_status -> __ -> __ -> trace_any_call -> trace_any_call -> __ **)
 965 let trace_any_call_jmdiscr a1 a2 a3 x y =
 966   Logic.eq_rect_Type2 x
 967     (match x with
 968      | Tac_base a0 -> Obj.magic (fun _ dH -> dH __ __)
 969      | Tac_step_call (a0, a10, a20, a30, a7, a9) ->
 970        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)
 971      | Tac_step_default (a0, a10, a20, a4) ->
 972        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
 973
 974 type trace_label_call =
 975 | Tlc_base of __ * __ * trace_any_call
 976
 977 (** val trace_label_call_rect_Type4 :
 978     abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
 979     -> trace_label_call -> 'a1 **)
 980 let rec trace_label_call_rect_Type4 s h_tlc_base x_22666 x_22665 = function
 981 | Tlc_base (start_status, end_status, x_22669) ->
 982   h_tlc_base start_status end_status x_22669 __
 983
 984 (** val trace_label_call_rect_Type5 :
 985     abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
 986     -> trace_label_call -> 'a1 **)
 987 let rec trace_label_call_rect_Type5 s h_tlc_base x_22672 x_22671 = function
 988 | Tlc_base (start_status, end_status, x_22675) ->
 989   h_tlc_base start_status end_status x_22675 __
 990
 991 (** val trace_label_call_rect_Type3 :
 992     abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
 993     -> trace_label_call -> 'a1 **)
 994 let rec trace_label_call_rect_Type3 s h_tlc_base x_22678 x_22677 = function
 995 | Tlc_base (start_status, end_status, x_22681) ->
 996   h_tlc_base start_status end_status x_22681 __
 997
 998 (** val trace_label_call_rect_Type2 :
 999     abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1000     -> trace_label_call -> 'a1 **)
1001 let rec trace_label_call_rect_Type2 s h_tlc_base x_22684 x_22683 = function
1002 | Tlc_base (start_status, end_status, x_22687) ->
1003   h_tlc_base start_status end_status x_22687 __
1004
1005 (** val trace_label_call_rect_Type1 :
1006     abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1007     -> trace_label_call -> 'a1 **)
1008 let rec trace_label_call_rect_Type1 s h_tlc_base x_22690 x_22689 = function
1009 | Tlc_base (start_status, end_status, x_22693) ->
1010   h_tlc_base start_status end_status x_22693 __
1011
1012 (** val trace_label_call_rect_Type0 :
1013     abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
1014     -> trace_label_call -> 'a1 **)
1015 let rec trace_label_call_rect_Type0 s h_tlc_base x_22696 x_22695 = function
1016 | Tlc_base (start_status, end_status, x_22699) ->
1017   h_tlc_base start_status end_status x_22699 __
1018
1019 (** val trace_label_call_inv_rect_Type4 :
1020     abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1021     trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1022 let trace_label_call_inv_rect_Type4 x1 x2 x3 hterm h1 =
1023   let hcut = trace_label_call_rect_Type4 x1 h1 x2 x3 hterm in hcut __ __ __
1024
1025 (** val trace_label_call_inv_rect_Type3 :
1026     abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1027     trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1028 let trace_label_call_inv_rect_Type3 x1 x2 x3 hterm h1 =
1029   let hcut = trace_label_call_rect_Type3 x1 h1 x2 x3 hterm in hcut __ __ __
1030
1031 (** val trace_label_call_inv_rect_Type2 :
1032     abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1033     trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1034 let trace_label_call_inv_rect_Type2 x1 x2 x3 hterm h1 =
1035   let hcut = trace_label_call_rect_Type2 x1 h1 x2 x3 hterm in hcut __ __ __
1036
1037 (** val trace_label_call_inv_rect_Type1 :
1038     abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1039     trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1040 let trace_label_call_inv_rect_Type1 x1 x2 x3 hterm h1 =
1041   let hcut = trace_label_call_rect_Type1 x1 h1 x2 x3 hterm in hcut __ __ __
1042
1043 (** val trace_label_call_inv_rect_Type0 :
1044     abstract_status -> __ -> __ -> trace_label_call -> (__ -> __ ->
1045     trace_any_call -> __ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1046 let trace_label_call_inv_rect_Type0 x1 x2 x3 hterm h1 =
1047   let hcut = trace_label_call_rect_Type0 x1 h1 x2 x3 hterm in hcut __ __ __
1048
1049 (** val trace_label_call_discr :
1050     abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __ **)
1051 let trace_label_call_discr a1 a2 a3 x y =
1052   Logic.eq_rect_Type2 x
1053     (let Tlc_base (a0, a10, a20) = x in
1054     Obj.magic (fun _ dH -> dH __ __ __ __)) y
1055
1056 (** val trace_label_call_jmdiscr :
1057     abstract_status -> __ -> __ -> trace_label_call -> trace_label_call -> __ **)
1058 let trace_label_call_jmdiscr a1 a2 a3 x y =
1059   Logic.eq_rect_Type2 x
1060     (let Tlc_base (a0, a10, a20) = x in
1061     Obj.magic (fun _ dH -> dH __ __ __ __)) y
1062
1063 (** val tlc_hd_label :
1064     abstract_status -> __ -> __ -> trace_label_call -> CostLabel.costlabel **)
1065 let tlc_hd_label s st1 st2 tr =
1066   (let Tlc_base (st1', x, x0) = tr in
1067   (fun _ _ _ -> Types.pi1 (as_label_safe s st1'))) __ __ __
1068
1069 type trace_label_diverges = __trace_label_diverges Lazy.t
1070 and __trace_label_diverges =
1071 | Tld_step of __ * __ * trace_label_label * trace_label_diverges
1072 | Tld_base of __ * __ * __ * trace_label_call * trace_label_diverges
1073
1074 (** val trace_label_diverges_inv_rect_Type4 :
1075     abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1076     trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1077     __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1078     __ -> 'a1) -> 'a1 **)
1079 let trace_label_diverges_inv_rect_Type4 x1 x2 hterm h1 h2 =
1080   let hcut =
1081     match Lazy.force
1082     hterm with
1083     | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1084     | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1085   in
1086   hcut __ __
1087
1088 (** val trace_label_diverges_inv_rect_Type3 :
1089     abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1090     trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1091     __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1092     __ -> 'a1) -> 'a1 **)
1093 let trace_label_diverges_inv_rect_Type3 x1 x2 hterm h1 h2 =
1094   let hcut =
1095     match Lazy.force
1096     hterm with
1097     | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1098     | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1099   in
1100   hcut __ __
1101
1102 (** val trace_label_diverges_inv_rect_Type2 :
1103     abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1104     trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1105     __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1106     __ -> 'a1) -> 'a1 **)
1107 let trace_label_diverges_inv_rect_Type2 x1 x2 hterm h1 h2 =
1108   let hcut =
1109     match Lazy.force
1110     hterm with
1111     | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1112     | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1113   in
1114   hcut __ __
1115
1116 (** val trace_label_diverges_inv_rect_Type1 :
1117     abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1118     trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1119     __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1120     __ -> 'a1) -> 'a1 **)
1121 let trace_label_diverges_inv_rect_Type1 x1 x2 hterm h1 h2 =
1122   let hcut =
1123     match Lazy.force
1124     hterm with
1125     | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1126     | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1127   in
1128   hcut __ __
1129
1130 (** val trace_label_diverges_inv_rect_Type0 :
1131     abstract_status -> __ -> trace_label_diverges -> (__ -> __ ->
1132     trace_label_label -> trace_label_diverges -> __ -> __ -> 'a1) -> (__ ->
1133     __ -> __ -> trace_label_call -> __ -> __ -> trace_label_diverges -> __ ->
1134     __ -> 'a1) -> 'a1 **)
1135 let trace_label_diverges_inv_rect_Type0 x1 x2 hterm h1 h2 =
1136   let hcut =
1137     match Lazy.force
1138     hterm with
1139     | Tld_step (x, x0, x3, x4) -> h1 x x0 x3 x4
1140     | Tld_base (x, x0, x3, x4, x5) -> h2 x x0 x3 x4 __ __ x5
1141   in
1142   hcut __ __
1143
1144 (** val trace_label_diverges_jmdiscr :
1145     abstract_status -> __ -> trace_label_diverges -> trace_label_diverges ->
1146     __ **)
1147 let trace_label_diverges_jmdiscr a1 a2 x y =
1148   Logic.eq_rect_Type2 x
1149     (match Lazy.force
1150      x with
1151      | Tld_step (a0, a10, a20, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1152      | Tld_base (a0, a10, a20, a3, a6) ->
1153        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1154
1155 (** val tld_hd_label :
1156     abstract_status -> __ -> trace_label_diverges -> CostLabel.costlabel **)
1157 let tld_hd_label s st tr =
1158   match Lazy.force
1159   tr with
1160   | Tld_step (st', st'', tll, x) ->
1161     tll_hd_label s Doesnt_end_with_ret st' st'' tll
1162   | Tld_base (st', st'', x, tlc, x2) -> tlc_hd_label s st' st'' tlc
1163
1164 type trace_whole_program =
1165 | Twp_terminating of __ * __ * __ * trace_label_return
1166 | Twp_diverges of __ * __ * trace_label_diverges
1167
1168 (** val trace_whole_program_rect_Type4 :
1169     abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1170     __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1171     -> trace_whole_program -> 'a1 **)
1172 let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_22748 = function
1173 | Twp_terminating
1174     (status_initial, status_start_fun, status_final, x_22751) ->
1175   h_twp_terminating status_initial status_start_fun status_final __ __
1176     x_22751 __
1177 | Twp_diverges (status_initial, status_start_fun, x_22754) ->
1178   h_twp_diverges status_initial status_start_fun __ __ x_22754
1179
1180 (** val trace_whole_program_rect_Type5 :
1181     abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1182     __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1183     -> trace_whole_program -> 'a1 **)
1184 let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_22759 = function
1185 | Twp_terminating
1186     (status_initial, status_start_fun, status_final, x_22762) ->
1187   h_twp_terminating status_initial status_start_fun status_final __ __
1188     x_22762 __
1189 | Twp_diverges (status_initial, status_start_fun, x_22765) ->
1190   h_twp_diverges status_initial status_start_fun __ __ x_22765
1191
1192 (** val trace_whole_program_rect_Type3 :
1193     abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1194     __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1195     -> trace_whole_program -> 'a1 **)
1196 let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_22770 = function
1197 | Twp_terminating
1198     (status_initial, status_start_fun, status_final, x_22773) ->
1199   h_twp_terminating status_initial status_start_fun status_final __ __
1200     x_22773 __
1201 | Twp_diverges (status_initial, status_start_fun, x_22776) ->
1202   h_twp_diverges status_initial status_start_fun __ __ x_22776
1203
1204 (** val trace_whole_program_rect_Type2 :
1205     abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1206     __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1207     -> trace_whole_program -> 'a1 **)
1208 let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_22781 = function
1209 | Twp_terminating
1210     (status_initial, status_start_fun, status_final, x_22784) ->
1211   h_twp_terminating status_initial status_start_fun status_final __ __
1212     x_22784 __
1213 | Twp_diverges (status_initial, status_start_fun, x_22787) ->
1214   h_twp_diverges status_initial status_start_fun __ __ x_22787
1215
1216 (** val trace_whole_program_rect_Type1 :
1217     abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1218     __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1219     -> trace_whole_program -> 'a1 **)
1220 let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_22792 = function
1221 | Twp_terminating
1222     (status_initial, status_start_fun, status_final, x_22795) ->
1223   h_twp_terminating status_initial status_start_fun status_final __ __
1224     x_22795 __
1225 | Twp_diverges (status_initial, status_start_fun, x_22798) ->
1226   h_twp_diverges status_initial status_start_fun __ __ x_22798
1227
1228 (** val trace_whole_program_rect_Type0 :
1229     abstract_status -> (__ -> __ -> __ -> __ -> __ -> trace_label_return ->
1230     __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
1231     -> trace_whole_program -> 'a1 **)
1232 let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_22803 = function
1233 | Twp_terminating
1234     (status_initial, status_start_fun, status_final, x_22806) ->
1235   h_twp_terminating status_initial status_start_fun status_final __ __
1236     x_22806 __
1237 | Twp_diverges (status_initial, status_start_fun, x_22809) ->
1238   h_twp_diverges status_initial status_start_fun __ __ x_22809
1239
1240 (** val trace_whole_program_inv_rect_Type4 :
1241     abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1242     __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1243     __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1244 let trace_whole_program_inv_rect_Type4 x1 x2 hterm h1 h2 =
1245   let hcut = trace_whole_program_rect_Type4 x1 h1 h2 x2 hterm in hcut __ __
1246
1247 (** val trace_whole_program_inv_rect_Type3 :
1248     abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1249     __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1250     __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1251 let trace_whole_program_inv_rect_Type3 x1 x2 hterm h1 h2 =
1252   let hcut = trace_whole_program_rect_Type3 x1 h1 h2 x2 hterm in hcut __ __
1253
1254 (** val trace_whole_program_inv_rect_Type2 :
1255     abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1256     __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1257     __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1258 let trace_whole_program_inv_rect_Type2 x1 x2 hterm h1 h2 =
1259   let hcut = trace_whole_program_rect_Type2 x1 h1 h2 x2 hterm in hcut __ __
1260
1261 (** val trace_whole_program_inv_rect_Type1 :
1262     abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1263     __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1264     __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1265 let trace_whole_program_inv_rect_Type1 x1 x2 hterm h1 h2 =
1266   let hcut = trace_whole_program_rect_Type1 x1 h1 h2 x2 hterm in hcut __ __
1267
1268 (** val trace_whole_program_inv_rect_Type0 :
1269     abstract_status -> __ -> trace_whole_program -> (__ -> __ -> __ -> __ ->
1270     __ -> trace_label_return -> __ -> __ -> __ -> 'a1) -> (__ -> __ -> __ ->
1271     __ -> trace_label_diverges -> __ -> __ -> 'a1) -> 'a1 **)
1272 let trace_whole_program_inv_rect_Type0 x1 x2 hterm h1 h2 =
1273   let hcut = trace_whole_program_rect_Type0 x1 h1 h2 x2 hterm in hcut __ __
1274
1275 (** val trace_whole_program_jmdiscr :
1276     abstract_status -> __ -> trace_whole_program -> trace_whole_program -> __ **)
1277 let trace_whole_program_jmdiscr a1 a2 x y =
1278   Logic.eq_rect_Type2 x
1279     (match x with
1280      | Twp_terminating (a0, a10, a20, a5) ->
1281        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)
1282      | Twp_diverges (a0, a10, a4) ->
1283        Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
1284
1285 (** val tal_tl_label :
1286     abstract_status -> __ -> __ -> trace_any_label -> CostLabel.costlabel **)
1287 let tal_tl_label s st1 st2 tr =
1288   Types.pi1 (as_label_safe s st2)
1289
1290 (** val tll_tl_label :
1291     abstract_status -> __ -> __ -> trace_label_label -> CostLabel.costlabel **)
1292 let tll_tl_label s st1 st2 tr =
1293   Types.pi1 (as_label_safe s st2)
1294
1295 type trace_any_any =
1296 | Taa_base of __
1297 | Taa_step of __ * __ * __ * trace_any_any
1298
1299 (** val trace_any_any_rect_Type4 :
1300     abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1301     trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1302 let rec trace_any_any_rect_Type4 s h_taa_base h_taa_step x_23033 x_23032 = function
1303 | Taa_base st -> h_taa_base st
1304 | Taa_step (st1, st2, st3, x_23035) ->
1305   h_taa_step st1 st2 st3 __ __ __ x_23035
1306     (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_23035)
1307
1308 (** val trace_any_any_rect_Type3 :
1309     abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1310     trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1311 let rec trace_any_any_rect_Type3 s h_taa_base h_taa_step x_23051 x_23050 = function
1312 | Taa_base st -> h_taa_base st
1313 | Taa_step (st1, st2, st3, x_23053) ->
1314   h_taa_step st1 st2 st3 __ __ __ x_23053
1315     (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_23053)
1316
1317 (** val trace_any_any_rect_Type2 :
1318     abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1319     trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1320 let rec trace_any_any_rect_Type2 s h_taa_base h_taa_step x_23060 x_23059 = function
1321 | Taa_base st -> h_taa_base st
1322 | Taa_step (st1, st2, st3, x_23062) ->
1323   h_taa_step st1 st2 st3 __ __ __ x_23062
1324     (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_23062)
1325
1326 (** val trace_any_any_rect_Type1 :
1327     abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1328     trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1329 let rec trace_any_any_rect_Type1 s h_taa_base h_taa_step x_23069 x_23068 = function
1330 | Taa_base st -> h_taa_base st
1331 | Taa_step (st1, st2, st3, x_23071) ->
1332   h_taa_step st1 st2 st3 __ __ __ x_23071
1333     (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_23071)
1334
1335 (** val trace_any_any_rect_Type0 :
1336     abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
1337     trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
1338 let rec trace_any_any_rect_Type0 s h_taa_base h_taa_step x_23078 x_23077 = function
1339 | Taa_base st -> h_taa_base st
1340 | Taa_step (st1, st2, st3, x_23080) ->
1341   h_taa_step st1 st2 st3 __ __ __ x_23080
1342     (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_23080)
1343
1344 (** val trace_any_any_inv_rect_Type4 :
1345     abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1346     'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1347     -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1348 let trace_any_any_inv_rect_Type4 x1 x2 x3 hterm h1 h2 =
1349   let hcut = trace_any_any_rect_Type4 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1350
1351 (** val trace_any_any_inv_rect_Type3 :
1352     abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1353     'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1354     -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1355 let trace_any_any_inv_rect_Type3 x1 x2 x3 hterm h1 h2 =
1356   let hcut = trace_any_any_rect_Type3 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1357
1358 (** val trace_any_any_inv_rect_Type2 :
1359     abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1360     'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1361     -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1362 let trace_any_any_inv_rect_Type2 x1 x2 x3 hterm h1 h2 =
1363   let hcut = trace_any_any_rect_Type2 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1364
1365 (** val trace_any_any_inv_rect_Type1 :
1366     abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1367     'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1368     -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1369 let trace_any_any_inv_rect_Type1 x1 x2 x3 hterm h1 h2 =
1370   let hcut = trace_any_any_rect_Type1 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1371
1372 (** val trace_any_any_inv_rect_Type0 :
1373     abstract_status -> __ -> __ -> trace_any_any -> (__ -> __ -> __ -> __ ->
1374     'a1) -> (__ -> __ -> __ -> __ -> __ -> __ -> trace_any_any -> (__ -> __
1375     -> __ -> 'a1) -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1376 let trace_any_any_inv_rect_Type0 x1 x2 x3 hterm h1 h2 =
1377   let hcut = trace_any_any_rect_Type0 x1 h1 h2 x2 x3 hterm in hcut __ __ __
1378
1379 (** val trace_any_any_jmdiscr :
1380     abstract_status -> __ -> __ -> trace_any_any -> trace_any_any -> __ **)
1381 let trace_any_any_jmdiscr a1 a2 a3 x y =
1382   Logic.eq_rect_Type2 x
1383     (match x with
1384      | Taa_base a0 -> Obj.magic (fun _ dH -> dH __)
1385      | Taa_step (a0, a10, a20, a6) ->
1386        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1387
1388 (** val taa_non_empty :
1389     abstract_status -> __ -> __ -> trace_any_any -> Bool.bool **)
1390 let taa_non_empty s st1 st2 = function
1391 | Taa_base x -> Bool.False
1392 | Taa_step (x, x0, x1, x5) -> Bool.True
1393
1394 (** val dpi1__o__taa_to_bool__o__inject :
1395     abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair ->
1396     Bool.bool Types.sig0 **)
1397 let dpi1__o__taa_to_bool__o__inject x1 x2 x3 x5 =
1398   taa_non_empty x1 x2 x3 x5.Types.dpi1
1399
1400 (** val dpi1__o__taa_to_bool__o__bool_to_Prop__o__inject :
1401     abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair -> __
1402     Types.sig0 **)
1403 let dpi1__o__taa_to_bool__o__bool_to_Prop__o__inject x1 x2 x3 x5 =
1404   Util.bool_to_Prop__o__inject (taa_non_empty x1 x2 x3 x5.Types.dpi1)
1405
1406 (** val eject__o__taa_to_bool__o__inject :
1407     abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool
1408     Types.sig0 **)
1409 let eject__o__taa_to_bool__o__inject x1 x2 x3 x5 =
1410   taa_non_empty x1 x2 x3 (Types.pi1 x5)
1411
1412 (** val eject__o__taa_to_bool__o__bool_to_Prop__o__inject :
1413     abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> __ Types.sig0 **)
1414 let eject__o__taa_to_bool__o__bool_to_Prop__o__inject x1 x2 x3 x5 =
1415   Util.bool_to_Prop__o__inject (taa_non_empty x1 x2 x3 (Types.pi1 x5))
1416
1417 (** val taa_to_bool__o__bool_to_Prop__o__inject :
1418     abstract_status -> __ -> __ -> trace_any_any -> __ Types.sig0 **)
1419 let taa_to_bool__o__bool_to_Prop__o__inject x1 x2 x3 x4 =
1420   Util.bool_to_Prop__o__inject (taa_non_empty x1 x2 x3 x4)
1421
1422 (** val taa_to_bool__o__inject :
1423     abstract_status -> __ -> __ -> trace_any_any -> Bool.bool Types.sig0 **)
1424 let taa_to_bool__o__inject x1 x2 x3 x4 =
1425   taa_non_empty x1 x2 x3 x4
1426
1427 (** val dpi1__o__taa_to_bool :
1428     abstract_status -> __ -> __ -> (trace_any_any, 'a1) Types.dPair ->
1429     Bool.bool **)
1430 let dpi1__o__taa_to_bool x0 x1 x2 x4 =
1431   taa_non_empty x0 x1 x2 x4.Types.dpi1
1432
1433 (** val eject__o__taa_to_bool :
1434     abstract_status -> __ -> __ -> trace_any_any Types.sig0 -> Bool.bool **)
1435 let eject__o__taa_to_bool x0 x1 x2 x4 =
1436   taa_non_empty x0 x1 x2 (Types.pi1 x4)
1437
1438 (** val taa_append_tal :
1439     abstract_status -> __ -> trace_ends_with_ret -> __ -> __ -> trace_any_any
1440     -> trace_any_label -> trace_any_label **)
1441 let rec taa_append_tal s st1 fl st2 st3 taa =
1442   (match taa with
1443    | Taa_base st1' -> (fun fl0 st30 tal2 -> tal2)
1444    | Taa_step (st1', st2', st3', tl) ->
1445      (fun fl0 st30 tal2 -> Tal_step_default (fl0, st1', st2', st30,
1446        (taa_append_tal s st2' fl0 st3' st30 tl tal2)))) fl st3
1447
1448 type intensional_event =
1449 | IEVcost of CostLabel.costlabel
1450 | IEVcall of AST.ident
1451 | IEVtailcall of AST.ident * AST.ident
1452 | IEVret of AST.ident
1453
1454 (** val intensional_event_rect_Type4 :
1455     (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1456     AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1457 let rec intensional_event_rect_Type4 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1458 | IEVcost x_23151 -> h_IEVcost x_23151
1459 | IEVcall x_23152 -> h_IEVcall x_23152
1460 | IEVtailcall (x_23154, x_23153) -> h_IEVtailcall x_23154 x_23153
1461 | IEVret x_23155 -> h_IEVret x_23155
1462
1463 (** val intensional_event_rect_Type5 :
1464     (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1465     AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1466 let rec intensional_event_rect_Type5 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1467 | IEVcost x_23161 -> h_IEVcost x_23161
1468 | IEVcall x_23162 -> h_IEVcall x_23162
1469 | IEVtailcall (x_23164, x_23163) -> h_IEVtailcall x_23164 x_23163
1470 | IEVret x_23165 -> h_IEVret x_23165
1471
1472 (** val intensional_event_rect_Type3 :
1473     (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1474     AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1475 let rec intensional_event_rect_Type3 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1476 | IEVcost x_23171 -> h_IEVcost x_23171
1477 | IEVcall x_23172 -> h_IEVcall x_23172
1478 | IEVtailcall (x_23174, x_23173) -> h_IEVtailcall x_23174 x_23173
1479 | IEVret x_23175 -> h_IEVret x_23175
1480
1481 (** val intensional_event_rect_Type2 :
1482     (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1483     AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1484 let rec intensional_event_rect_Type2 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1485 | IEVcost x_23181 -> h_IEVcost x_23181
1486 | IEVcall x_23182 -> h_IEVcall x_23182
1487 | IEVtailcall (x_23184, x_23183) -> h_IEVtailcall x_23184 x_23183
1488 | IEVret x_23185 -> h_IEVret x_23185
1489
1490 (** val intensional_event_rect_Type1 :
1491     (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1492     AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1493 let rec intensional_event_rect_Type1 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1494 | IEVcost x_23191 -> h_IEVcost x_23191
1495 | IEVcall x_23192 -> h_IEVcall x_23192
1496 | IEVtailcall (x_23194, x_23193) -> h_IEVtailcall x_23194 x_23193
1497 | IEVret x_23195 -> h_IEVret x_23195
1498
1499 (** val intensional_event_rect_Type0 :
1500     (CostLabel.costlabel -> 'a1) -> (AST.ident -> 'a1) -> (AST.ident ->
1501     AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
1502 let rec intensional_event_rect_Type0 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
1503 | IEVcost x_23201 -> h_IEVcost x_23201
1504 | IEVcall x_23202 -> h_IEVcall x_23202
1505 | IEVtailcall (x_23204, x_23203) -> h_IEVtailcall x_23204 x_23203
1506 | IEVret x_23205 -> h_IEVret x_23205
1507
1508 (** val intensional_event_inv_rect_Type4 :
1509     intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1510     __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1511     -> 'a1) -> 'a1 **)
1512 let intensional_event_inv_rect_Type4 hterm h1 h2 h3 h4 =
1513   let hcut = intensional_event_rect_Type4 h1 h2 h3 h4 hterm in hcut __
1514
1515 (** val intensional_event_inv_rect_Type3 :
1516     intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1517     __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1518     -> 'a1) -> 'a1 **)
1519 let intensional_event_inv_rect_Type3 hterm h1 h2 h3 h4 =
1520   let hcut = intensional_event_rect_Type3 h1 h2 h3 h4 hterm in hcut __
1521
1522 (** val intensional_event_inv_rect_Type2 :
1523     intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1524     __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1525     -> 'a1) -> 'a1 **)
1526 let intensional_event_inv_rect_Type2 hterm h1 h2 h3 h4 =
1527   let hcut = intensional_event_rect_Type2 h1 h2 h3 h4 hterm in hcut __
1528
1529 (** val intensional_event_inv_rect_Type1 :
1530     intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1531     __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1532     -> 'a1) -> 'a1 **)
1533 let intensional_event_inv_rect_Type1 hterm h1 h2 h3 h4 =
1534   let hcut = intensional_event_rect_Type1 h1 h2 h3 h4 hterm in hcut __
1535
1536 (** val intensional_event_inv_rect_Type0 :
1537     intensional_event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident ->
1538     __ -> 'a1) -> (AST.ident -> AST.ident -> __ -> 'a1) -> (AST.ident -> __
1539     -> 'a1) -> 'a1 **)
1540 let intensional_event_inv_rect_Type0 hterm h1 h2 h3 h4 =
1541   let hcut = intensional_event_rect_Type0 h1 h2 h3 h4 hterm in hcut __
1542
1543 (** val intensional_event_discr :
1544     intensional_event -> intensional_event -> __ **)
1545 let intensional_event_discr x y =
1546   Logic.eq_rect_Type2 x
1547     (match x with
1548      | IEVcost a0 -> Obj.magic (fun _ dH -> dH __)
1549      | IEVcall a0 -> Obj.magic (fun _ dH -> dH __)
1550      | IEVtailcall (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1551      | IEVret a0 -> Obj.magic (fun _ dH -> dH __)) y
1552
1553 (** val intensional_event_jmdiscr :
1554     intensional_event -> intensional_event -> __ **)
1555 let intensional_event_jmdiscr x y =
1556   Logic.eq_rect_Type2 x
1557     (match x with
1558      | IEVcost a0 -> Obj.magic (fun _ dH -> dH __)
1559      | IEVcall a0 -> Obj.magic (fun _ dH -> dH __)
1560      | IEVtailcall (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1561      | IEVret a0 -> Obj.magic (fun _ dH -> dH __)) y
1562
1563 type as_trace = intensional_event List.list Types.sig0
1564
1565 (** val cons_safe :
1566     'a1 Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0 **)
1567 let cons_safe x l =
1568   List.Cons ((Types.pi1 x), (Types.pi1 l))
1569
1570 (** val append_safe :
1571     'a1 List.list Types.sig0 -> 'a1 List.list Types.sig0 -> 'a1 List.list
1572     Types.sig0 **)
1573 let append_safe l1 l2 =
1574   List.append (Types.pi1 l1) (Types.pi1 l2)
1575
1576 (** val nil_safe : 'a1 List.list Types.sig0 **)
1577 let nil_safe =
1578   List.Nil
1579
1580 (** val emittable_cost :
1581     abstract_status -> as_cost_label -> intensional_event Types.sig0 **)
1582 let emittable_cost s l =
1583   IEVcost (Types.pi1 l)
1584
1585 (** val observables_trace_label_label :
1586     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
1587     -> AST.ident -> as_trace **)
1588 let rec observables_trace_label_label s trace_ends_flag start_status final_status the_trace curr =
1589   let Tll_base (ends_flag, initial, final, given_trace) = the_trace in
1590   let label = as_label_safe s initial in
1591   cons_safe (emittable_cost s label)
1592     (observables_trace_any_label s ends_flag initial final given_trace curr)
1593 (** val observables_trace_any_label :
1594     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
1595     AST.ident -> as_trace **)
1596 and observables_trace_any_label s trace_ends_flag start_status final_status the_trace curr =
1597   match the_trace with
1598   | Tal_base_not_return (the_status, x) -> nil_safe
1599   | Tal_base_return (the_status, x) -> cons_safe (IEVret curr) nil_safe
1600   | Tal_base_call (pre_fun_call, start_fun_call, final, call_trace) ->
1601     let id = s.as_call_ident pre_fun_call in
1602     cons_safe (IEVcall id)
1603       (observables_trace_label_return s start_fun_call final call_trace id)
1604   | Tal_base_tailcall (pre_fun_call, start_fun_call, final, call_trace) ->
1605     let id = s.as_tailcall_ident pre_fun_call in
1606     cons_safe (IEVtailcall (curr, id))
1607       (observables_trace_label_return s start_fun_call final call_trace id)
1608   | Tal_step_call
1609       (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
1610        call_trace, final_trace) ->
1611     let id = s.as_call_ident pre_fun_call in
1612     let call_cost_trace =
1613       observables_trace_label_return s start_fun_call after_fun_call
1614         call_trace id
1615     in
1616     let final_cost_trace =
1617       observables_trace_any_label s end_flag after_fun_call final final_trace
1618         curr
1619     in
1620     append_safe (cons_safe (IEVcall id) call_cost_trace) final_cost_trace
1621   | Tal_step_default
1622       (end_flag, status_pre, status_init, status_end, tail_trace) ->
1623     observables_trace_any_label s end_flag status_init status_end tail_trace
1624       curr
1625 (** val observables_trace_label_return :
1626     abstract_status -> __ -> __ -> trace_label_return -> AST.ident ->
1627     as_trace **)
1628 and observables_trace_label_return s start_status final_status the_trace curr =
1629   match the_trace with
1630   | Tlr_base (before, after, trace_to_lift) ->
1631     observables_trace_label_label s Ends_with_ret before after trace_to_lift
1632       curr
1633   | Tlr_step (initial, labelled, final, labelled_trace, ret_trace) ->
1634     let labelled_cost =
1635       observables_trace_label_label s Doesnt_end_with_ret initial labelled
1636         labelled_trace curr
1637     in
1638     let return_cost =
1639       observables_trace_label_return s labelled final ret_trace curr
1640     in
1641     append_safe labelled_cost return_cost
1642
1643 (** val filter_map :
1644     ('a1 -> 'a2 Types.option) -> 'a1 List.list -> 'a2 List.list **)
1645 let rec filter_map f = function
1646 | List.Nil -> List.Nil
1647 | List.Cons (hd, tl) ->
1648   List.append
1649     (match f hd with
1650      | Types.None -> List.Nil
1651      | Types.Some y -> List.Cons (y, List.Nil)) (filter_map f tl)
1652
1653 (** val list_distribute_sig_aux :
1654     'a1 List.list -> 'a1 Types.sig0 List.list **)
1655 let rec list_distribute_sig_aux l =
1656   (match l with
1657    | List.Nil -> (fun _ -> List.Nil)
1658    | List.Cons (hd, tl) ->
1659      (fun _ -> List.Cons (hd, (list_distribute_sig_aux tl)))) __
1660
1661 (** val list_distribute_sig :
1662     'a1 List.list Types.sig0 -> 'a1 Types.sig0 List.list **)
1663 let list_distribute_sig l =
1664   list_distribute_sig_aux (Types.pi1 l)
1665
1666 (** val list_factor_sig :
1667     'a1 Types.sig0 List.list -> 'a1 List.list Types.sig0 **)
1668 let rec list_factor_sig = function
1669 | List.Nil -> nil_safe
1670 | List.Cons (hd, tl) -> cons_safe hd (list_factor_sig tl)
1671
1672 (** val costlabels_of_observables :
1673     abstract_status -> as_trace -> as_cost_label List.list **)
1674 let costlabels_of_observables s l =
1675   filter_map (fun ev ->
1676     (match Types.pi1 ev with
1677      | IEVcost c -> (fun _ -> Types.Some c)
1678      | IEVcall x -> (fun _ -> Types.None)
1679      | IEVtailcall (x, x0) -> (fun _ -> Types.None)
1680      | IEVret x -> (fun _ -> Types.None)) __) (list_distribute_sig l)
1681
1682 (** val flatten_trace_label_return :
1683     abstract_status -> __ -> __ -> trace_label_return -> as_cost_label
1684     List.list **)
1685 let flatten_trace_label_return s st1 st2 tlr =
1686   let dummy = Positive.One in
1687   costlabels_of_observables s
1688     (observables_trace_label_return s st1 st2 tlr dummy)
1689
1690 (** val flatten_trace_label_label :
1691     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
1692     -> as_cost_label List.list **)
1693 let flatten_trace_label_label s flag st1 st2 tll =
1694   let dummy = Positive.One in
1695   costlabels_of_observables s
1696     (observables_trace_label_label s flag st1 st2 tll dummy)
1697
1698 (** val flatten_trace_any_label :
1699     abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
1700     as_cost_label List.list **)
1701 let flatten_trace_any_label s flag st1 st2 tll =
1702   let dummy = Positive.One in
1703   costlabels_of_observables s
1704     (observables_trace_any_label s flag st1 st2 tll dummy)
1705
1706 type trace_any_any_free =
1707 | Taaf_base of __
1708 | Taaf_step of __ * __ * __ * trace_any_any
1709 | Taaf_step_jump of __ * __ * __ * trace_any_any
1710
1711 (** val trace_any_any_free_rect_Type4 :
1712     abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1713     -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1714     'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1715 let rec trace_any_any_free_rect_Type4 s h_taaf_base h_taaf_step h_taaf_step_jump x_23284 x_23283 = function
1716 | Taaf_base s0 -> h_taaf_base s0
1717 | Taaf_step (s1, s2, s3, x_23288) -> h_taaf_step s1 s2 s3 x_23288 __ __
1718 | Taaf_step_jump (s1, s2, s3, x_23292) ->
1719   h_taaf_step_jump s1 s2 s3 x_23292 __ __ __
1720
1721 (** val trace_any_any_free_rect_Type5 :
1722     abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1723     -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1724     'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1725 let rec trace_any_any_free_rect_Type5 s h_taaf_base h_taaf_step h_taaf_step_jump x_23297 x_23296 = function
1726 | Taaf_base s0 -> h_taaf_base s0
1727 | Taaf_step (s1, s2, s3, x_23301) -> h_taaf_step s1 s2 s3 x_23301 __ __
1728 | Taaf_step_jump (s1, s2, s3, x_23305) ->
1729   h_taaf_step_jump s1 s2 s3 x_23305 __ __ __
1730
1731 (** val trace_any_any_free_rect_Type3 :
1732     abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1733     -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1734     'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1735 let rec trace_any_any_free_rect_Type3 s h_taaf_base h_taaf_step h_taaf_step_jump x_23310 x_23309 = function
1736 | Taaf_base s0 -> h_taaf_base s0
1737 | Taaf_step (s1, s2, s3, x_23314) -> h_taaf_step s1 s2 s3 x_23314 __ __
1738 | Taaf_step_jump (s1, s2, s3, x_23318) ->
1739   h_taaf_step_jump s1 s2 s3 x_23318 __ __ __
1740
1741 (** val trace_any_any_free_rect_Type2 :
1742     abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1743     -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1744     'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1745 let rec trace_any_any_free_rect_Type2 s h_taaf_base h_taaf_step h_taaf_step_jump x_23323 x_23322 = function
1746 | Taaf_base s0 -> h_taaf_base s0
1747 | Taaf_step (s1, s2, s3, x_23327) -> h_taaf_step s1 s2 s3 x_23327 __ __
1748 | Taaf_step_jump (s1, s2, s3, x_23331) ->
1749   h_taaf_step_jump s1 s2 s3 x_23331 __ __ __
1750
1751 (** val trace_any_any_free_rect_Type1 :
1752     abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1753     -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1754     'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1755 let rec trace_any_any_free_rect_Type1 s h_taaf_base h_taaf_step h_taaf_step_jump x_23336 x_23335 = function
1756 | Taaf_base s0 -> h_taaf_base s0
1757 | Taaf_step (s1, s2, s3, x_23340) -> h_taaf_step s1 s2 s3 x_23340 __ __
1758 | Taaf_step_jump (s1, s2, s3, x_23344) ->
1759   h_taaf_step_jump s1 s2 s3 x_23344 __ __ __
1760
1761 (** val trace_any_any_free_rect_Type0 :
1762     abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __
1763     -> __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ ->
1764     'a1) -> __ -> __ -> trace_any_any_free -> 'a1 **)
1765 let rec trace_any_any_free_rect_Type0 s h_taaf_base h_taaf_step h_taaf_step_jump x_23349 x_23348 = function
1766 | Taaf_base s0 -> h_taaf_base s0
1767 | Taaf_step (s1, s2, s3, x_23353) -> h_taaf_step s1 s2 s3 x_23353 __ __
1768 | Taaf_step_jump (s1, s2, s3, x_23357) ->
1769   h_taaf_step_jump s1 s2 s3 x_23357 __ __ __
1770
1771 (** val trace_any_any_free_inv_rect_Type4 :
1772     abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1773     __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1774     __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1775     __ -> __ -> 'a1) -> 'a1 **)
1776 let trace_any_any_free_inv_rect_Type4 x1 x2 x3 hterm h1 h2 h3 =
1777   let hcut = trace_any_any_free_rect_Type4 x1 h1 h2 h3 x2 x3 hterm in
1778   hcut __ __ __
1779
1780 (** val trace_any_any_free_inv_rect_Type3 :
1781     abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1782     __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1783     __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1784     __ -> __ -> 'a1) -> 'a1 **)
1785 let trace_any_any_free_inv_rect_Type3 x1 x2 x3 hterm h1 h2 h3 =
1786   let hcut = trace_any_any_free_rect_Type3 x1 h1 h2 h3 x2 x3 hterm in
1787   hcut __ __ __
1788
1789 (** val trace_any_any_free_inv_rect_Type2 :
1790     abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1791     __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1792     __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1793     __ -> __ -> 'a1) -> 'a1 **)
1794 let trace_any_any_free_inv_rect_Type2 x1 x2 x3 hterm h1 h2 h3 =
1795   let hcut = trace_any_any_free_rect_Type2 x1 h1 h2 h3 x2 x3 hterm in
1796   hcut __ __ __
1797
1798 (** val trace_any_any_free_inv_rect_Type1 :
1799     abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1800     __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1801     __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1802     __ -> __ -> 'a1) -> 'a1 **)
1803 let trace_any_any_free_inv_rect_Type1 x1 x2 x3 hterm h1 h2 h3 =
1804   let hcut = trace_any_any_free_rect_Type1 x1 h1 h2 h3 x2 x3 hterm in
1805   hcut __ __ __
1806
1807 (** val trace_any_any_free_inv_rect_Type0 :
1808     abstract_status -> __ -> __ -> trace_any_any_free -> (__ -> __ -> __ ->
1809     __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1810     __ -> 'a1) -> (__ -> __ -> __ -> trace_any_any -> __ -> __ -> __ -> __ ->
1811     __ -> __ -> 'a1) -> 'a1 **)
1812 let trace_any_any_free_inv_rect_Type0 x1 x2 x3 hterm h1 h2 h3 =
1813   let hcut = trace_any_any_free_rect_Type0 x1 h1 h2 h3 x2 x3 hterm in
1814   hcut __ __ __
1815
1816 (** val trace_any_any_free_jmdiscr :
1817     abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any_free
1818     -> __ **)
1819 let trace_any_any_free_jmdiscr a1 a2 a3 x y =
1820   Logic.eq_rect_Type2 x
1821     (match x with
1822      | Taaf_base a0 -> Obj.magic (fun _ dH -> dH __)
1823      | Taaf_step (a0, a10, a20, a30) ->
1824        Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
1825      | Taaf_step_jump (a0, a10, a20, a30) ->
1826        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __)) y
1827
1828 (** val taaf_non_empty :
1829     abstract_status -> __ -> __ -> trace_any_any_free -> Bool.bool **)
1830 let taaf_non_empty s s1 s2 = function
1831 | Taaf_base x -> Bool.False
1832 | Taaf_step (x, x0, x1, x2) -> Bool.True
1833 | Taaf_step_jump (x, x0, x1, x2) -> Bool.True
1834
1835 (** val taa_append_taa :
1836     abstract_status -> __ -> __ -> __ -> trace_any_any -> trace_any_any ->
1837     trace_any_any **)
1838 let rec taa_append_taa s st1 st2 st3 taa =
1839   (match taa with
1840    | Taa_base st1' -> (fun st30 taa2 -> taa2)
1841    | Taa_step (st1', st2', st3', tl) ->
1842      (fun st30 taa2 -> Taa_step (st1', st2', st30,
1843        (taa_append_taa s st2' st3' st30 tl taa2)))) st3
1844
1845 (** val taaf_to_taa :
1846     abstract_status -> __ -> __ -> trace_any_any_free -> trace_any_any **)
1847 let taaf_to_taa s s1 s2 taaf =
1848   (match taaf with
1849    | Taaf_base s0 -> (fun _ -> Taa_base s0)
1850    | Taaf_step (s10, s20, s3, taa) ->
1851      (fun _ ->
1852        taa_append_taa s s10 s20 s3 taa (Taa_step (s20, s3, s3, (Taa_base
1853          s3))))
1854    | Taaf_step_jump (s10, s20, s3, taa) ->
1855      (fun _ -> assert false (* absurd case *))) __
1856
1857 (** val taaf_append_tal :
1858     abstract_status -> __ -> trace_ends_with_ret -> __ -> __ ->
1859     trace_any_any_free -> trace_any_label -> trace_any_label **)
1860 let taaf_append_tal s st1 fl st2 st3 taaf =
1861   taa_append_tal s st1 fl st2 st3 (taaf_to_taa s st1 st2 taaf)
1862
1863 (** val taaf_append_taa :
1864     abstract_status -> __ -> __ -> __ -> trace_any_any_free -> trace_any_any
1865     -> trace_any_any **)
1866 let taaf_append_taa s st1 st2 st3 taaf =
1867   taa_append_taa s st1 st2 st3 (taaf_to_taa s st1 st2 taaf)
1868
1869 (** val taaf_cons :
1870     abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
1871     trace_any_any_free **)
1872 let taaf_cons s s1 s2 s3 tl =
1873   (match tl with
1874    | Taaf_base s20 -> (fun _ _ -> Taaf_step (s1, s1, s20, (Taa_base s1)))
1875    | Taaf_step (s20, s30, s4, taa) ->
1876      (fun _ _ -> Taaf_step (s1, s30, s4, (Taa_step (s1, s20, s30, taa))))
1877    | Taaf_step_jump (s20, s30, s4, taa) ->
1878      (fun _ _ -> Taaf_step_jump (s1, s30, s4, (Taa_step (s1, s20, s30,
1879        taa))))) __ __
1880
1881 (** val taaf_append_taaf :
1882     abstract_status -> __ -> __ -> __ -> trace_any_any_free ->
1883     trace_any_any_free -> trace_any_any_free **)
1884 let taaf_append_taaf s st1 st2 st3 taaf1 taaf2 =
1885   (match taaf2 with
1886    | Taaf_base s1 -> (fun taaf10 _ -> taaf10)
1887    | Taaf_step (s1, s2, s3, taa) ->
1888      (fun taaf10 _ -> Taaf_step (st1, s2, s3,
1889        (taaf_append_taa s st1 s1 s2 taaf10 taa)))
1890    | Taaf_step_jump (s2, s3, s4, taa) ->
1891      (fun taaf10 _ -> Taaf_step_jump (st1, s3, s4,
1892        (taaf_append_taa s st1 s2 s3 taaf10 taa)))) taaf1 __
1893