Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/structuredTraces.ml

    r2743 r2773  
    99open Logic
    1010
     11open Relations
     12
     13open Bool
     14
     15open Jmeq
     16
     17open Proper
     18
     19open PositiveMap
     20
     21open Deqsets
     22
     23open ErrorMessages
     24
     25open PreIdentifiers
     26
     27open Errors
     28
     29open Extralib
     30
     31open Setoids
     32
     33open Monad
     34
     35open Option
     36
     37open Div_and_mod
     38
     39open Russell
     40
     41open Util
     42
     43open List
     44
     45open Lists
     46
     47open Nat
     48
     49open Positive
     50
    1151open Types
    1252
    13 open Relations
    14 
    15 open Bool
    16 
    17 open Jmeq
    18 
    19 open BitVectorTrie
    20 
    21 open Proper
    22 
    23 open PositiveMap
    24 
    25 open Deqsets
    26 
    27 open ErrorMessages
    28 
    29 open PreIdentifiers
    30 
    31 open Errors
    32 
    33 open Extralib
    34 
    35 open Setoids
    36 
    37 open Monad
    38 
    39 open Option
    40 
    41 open Lists
    42 
    43 open Positive
    44 
    4553open Identifiers
    4654
     55open CostLabel
     56
     57open Sets
     58
     59open Listb
     60
     61open Integers
     62
     63open AST
     64
     65open Division
     66
    4767open Exp
    4868
    4969open Arithmetic
    5070
     71open Extranat
     72
    5173open Vector
    5274
    53 open Div_and_mod
    54 
    55 open Russell
    56 
    57 open List
    58 
    59 open Util
    60 
    6175open FoldStuff
    6276
    6377open BitVector
    6478
    65 open Extranat
    66 
    67 open Nat
    68 
    69 open Integers
    70 
    71 open AST
    72 
    73 open CostLabel
    74 
    75 open Sets
    76 
    77 open Listb
     79open Z
     80
     81open BitVectorZ
     82
     83open Pointers
     84
     85open Coqlib
     86
     87open Values
     88
     89open Events
     90
     91open IOMonad
     92
     93open IO
     94
     95open Hide
    7896
    7997type status_class =
     
    189207
    190208type abstract_status = { as_pc : Deqsets.deqSet; as_pc_of : (__ -> __);
    191                          as_classify : (__ -> status_class Types.option);
     209                         as_classify : (__ -> status_class);
    192210                         as_label_of_pc : (__ -> CostLabel.costlabel
    193211                                          Types.option);
     212                         as_result : (__ -> Integers.int Types.option);
    194213                         as_call_ident : (__ Types.sig0 -> AST.ident);
    195214                         as_tailcall_ident : (__ Types.sig0 -> AST.ident) }
    196215
    197216(** val abstract_status_rect_Type4 :
    198     (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
    199     Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
    200     (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
    201     abstract_status -> 'a1 **)
    202 let rec abstract_status_rect_Type4 h_mk_abstract_status x_16401 =
     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 **)
     221let rec abstract_status_rect_Type4 h_mk_abstract_status x_11583 =
    203222  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    204     as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
    205     as_tailcall_ident = as_tailcall_ident0 } = x_16401
     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_11583
    206225  in
    207226  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
    208     __ as_call_ident0 as_tailcall_ident0
     227    as_result0 as_call_ident0 as_tailcall_ident0
    209228
    210229(** val abstract_status_rect_Type5 :
    211     (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
    212     Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
    213     (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
    214     abstract_status -> 'a1 **)
    215 let rec abstract_status_rect_Type5 h_mk_abstract_status x_16403 =
     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 **)
     234let rec abstract_status_rect_Type5 h_mk_abstract_status x_11585 =
    216235  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    217     as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
    218     as_tailcall_ident = as_tailcall_ident0 } = x_16403
     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_11585
    219238  in
    220239  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
    221     __ as_call_ident0 as_tailcall_ident0
     240    as_result0 as_call_ident0 as_tailcall_ident0
    222241
    223242(** val abstract_status_rect_Type3 :
    224     (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
    225     Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
    226     (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
    227     abstract_status -> 'a1 **)
    228 let rec abstract_status_rect_Type3 h_mk_abstract_status x_16405 =
     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 **)
     247let rec abstract_status_rect_Type3 h_mk_abstract_status x_11587 =
    229248  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    230     as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
    231     as_tailcall_ident = as_tailcall_ident0 } = x_16405
     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_11587
    232251  in
    233252  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
    234     __ as_call_ident0 as_tailcall_ident0
     253    as_result0 as_call_ident0 as_tailcall_ident0
    235254
    236255(** val abstract_status_rect_Type2 :
    237     (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
    238     Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
    239     (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
    240     abstract_status -> 'a1 **)
    241 let rec abstract_status_rect_Type2 h_mk_abstract_status x_16407 =
     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 **)
     260let rec abstract_status_rect_Type2 h_mk_abstract_status x_11589 =
    242261  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    243     as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
    244     as_tailcall_ident = as_tailcall_ident0 } = x_16407
     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_11589
    245264  in
    246265  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
    247     __ as_call_ident0 as_tailcall_ident0
     266    as_result0 as_call_ident0 as_tailcall_ident0
    248267
    249268(** val abstract_status_rect_Type1 :
    250     (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
    251     Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
    252     (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
    253     abstract_status -> 'a1 **)
    254 let rec abstract_status_rect_Type1 h_mk_abstract_status x_16409 =
     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 **)
     273let rec abstract_status_rect_Type1 h_mk_abstract_status x_11591 =
    255274  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    256     as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
    257     as_tailcall_ident = as_tailcall_ident0 } = x_16409
     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_11591
    258277  in
    259278  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
    260     __ as_call_ident0 as_tailcall_ident0
     279    as_result0 as_call_ident0 as_tailcall_ident0
    261280
    262281(** val abstract_status_rect_Type0 :
    263     (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ -> status_class
    264     Types.option) -> (__ -> CostLabel.costlabel Types.option) -> __ -> __ ->
    265     (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
    266     abstract_status -> 'a1 **)
    267 let rec abstract_status_rect_Type0 h_mk_abstract_status x_16411 =
     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 **)
     286let rec abstract_status_rect_Type0 h_mk_abstract_status x_11593 =
    268287  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    269     as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
    270     as_tailcall_ident = as_tailcall_ident0 } = x_16411
     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_11593
    271290  in
    272291  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
    273     __ as_call_ident0 as_tailcall_ident0
     292    as_result0 as_call_ident0 as_tailcall_ident0
    274293
    275294type as_status = __
    276 
    277 type as_execute = __
    278295
    279296(** val as_pc : abstract_status -> Deqsets.deqSet **)
     
    285302  xxx.as_pc_of
    286303
    287 (** val as_classify : abstract_status -> __ -> status_class Types.option **)
     304(** val as_classify : abstract_status -> __ -> status_class **)
    288305let rec as_classify xxx =
    289306  xxx.as_classify
     
    294311  xxx.as_label_of_pc
    295312
    296 type as_after_return = __
    297 
    298 type as_final = __
     313(** val as_result : abstract_status -> __ -> Integers.int Types.option **)
     314let rec as_result xxx =
     315  xxx.as_result
    299316
    300317(** val as_call_ident : abstract_status -> __ Types.sig0 -> AST.ident **)
     
    308325(** val abstract_status_inv_rect_Type4 :
    309326    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
    310     status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
    311     __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident)
    312     -> __ -> 'a1) -> 'a1 **)
     327    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
     328    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
     329    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
    313330let abstract_status_inv_rect_Type4 hterm h1 =
    314331  let hcut = abstract_status_rect_Type4 h1 hterm in hcut __
     
    316333(** val abstract_status_inv_rect_Type3 :
    317334    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
    318     status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
    319     __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident)
    320     -> __ -> 'a1) -> 'a1 **)
     335    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
     336    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
     337    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
    321338let abstract_status_inv_rect_Type3 hterm h1 =
    322339  let hcut = abstract_status_rect_Type3 h1 hterm in hcut __
     
    324341(** val abstract_status_inv_rect_Type2 :
    325342    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
    326     status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
    327     __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident)
    328     -> __ -> 'a1) -> 'a1 **)
     343    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
     344    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
     345    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
    329346let abstract_status_inv_rect_Type2 hterm h1 =
    330347  let hcut = abstract_status_rect_Type2 h1 hterm in hcut __
     
    332349(** val abstract_status_inv_rect_Type1 :
    333350    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
    334     status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
    335     __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident)
    336     -> __ -> 'a1) -> 'a1 **)
     351    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
     352    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
     353    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
    337354let abstract_status_inv_rect_Type1 hterm h1 =
    338355  let hcut = abstract_status_rect_Type1 h1 hterm in hcut __
     
    340357(** val abstract_status_inv_rect_Type0 :
    341358    abstract_status -> (__ -> __ -> Deqsets.deqSet -> (__ -> __) -> (__ ->
    342     status_class Types.option) -> (__ -> CostLabel.costlabel Types.option) ->
    343     __ -> __ -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident)
    344     -> __ -> 'a1) -> 'a1 **)
     359    status_class) -> (__ -> CostLabel.costlabel Types.option) -> __ -> (__ ->
     360    Integers.int Types.option) -> (__ Types.sig0 -> AST.ident) -> (__
     361    Types.sig0 -> AST.ident) -> __ -> 'a1) -> 'a1 **)
    345362let abstract_status_inv_rect_Type0 hterm h1 =
    346363  let hcut = abstract_status_rect_Type0 h1 hterm in hcut __
     
    351368  Logic.eq_rect_Type2 x
    352369    (let { as_pc = a2; as_pc_of = a3; as_classify = a4; as_label_of_pc = a5;
    353        as_call_ident = a8; as_tailcall_ident = a9 } = x
     370       as_result = a7; as_call_ident = a8; as_tailcall_ident = a9 } = x
    354371     in
    355372    Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y
     
    359376let as_label s s0 =
    360377  s.as_label_of_pc (s.as_pc_of s0)
    361 
    362 (** val as_label_safe :
    363     abstract_status -> __ Types.sig0 -> CostLabel.costlabel **)
    364 let as_label_safe a_s st_sig =
    365   Option.opt_safe (as_label a_s (Types.pi1 st_sig))
    366378
    367379(** val as_costed_exc : abstract_status -> __ -> (__, __) Types.sum **)
     
    380392  Types.pi1 l_sig
    381393
    382 (** val as_cost_get_labels :
    383     abstract_status -> as_cost_label PositiveMap.positive_map ->
    384     CostLabel.costlabel PositiveMap.positive_map **)
    385 let as_cost_get_labels s =
    386   PositiveMap.map0 (as_cost_get_label s)
    387 
    388394type as_cost_map = as_cost_label -> Nat.nat
     395
     396(** val as_label_safe : abstract_status -> __ Types.sig0 -> as_cost_label **)
     397let as_label_safe a_s st_sig =
     398  Option.opt_safe (as_label a_s (Types.pi1 st_sig))
    389399
    390400(** val lift_sigma_map_id :
     
    787797    (tal_pc_list s trace_ends_flag start_status final_status the_trace)
    788798
    789 type tal_unrepeating = __
    790 
    791 type tll_unrepeating = __
    792 
    793 type tlr_unrepeating = __
    794 
    795799(** val tll_hd_label :
    796800    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
    797801    -> CostLabel.costlabel **)
    798 let tll_hd_label s fl st1 st2 = function
    799 | Tll_base (x, st1', x0, x1) -> as_label_safe s st1'
     802let 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'))) __ __ __ __
    800805
    801806(** val tlr_hd_label :
     
    816821    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    817822    __ -> trace_any_call -> 'a1 **)
    818 let rec trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default x_16491 x_16490 = function
     823let rec trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default x_11671 x_11670 = function
    819824| Tac_base status -> h_tac_base status __
    820825| Tac_step_call
    821826    (status_pre_fun_call, status_after_fun_call, status_final,
    822      status_start_fun_call, x_16496, x_16494) ->
     827     status_start_fun_call, x_11676, x_11674) ->
    823828  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    824     status_start_fun_call __ __ __ x_16496 __ x_16494
     829    status_start_fun_call __ __ __ x_11676 __ x_11674
    825830    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
    826       h_tac_step_default status_after_fun_call status_final x_16494)
    827 | Tac_step_default (status_pre, status_end, status_init, x_16501) ->
    828   h_tac_step_default status_pre status_end status_init __ x_16501 __ __
     831      h_tac_step_default status_after_fun_call status_final x_11674)
     832| Tac_step_default (status_pre, status_end, status_init, x_11681) ->
     833  h_tac_step_default status_pre status_end status_init __ x_11681 __ __
    829834    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
    830       h_tac_step_default status_init status_end x_16501)
     835      h_tac_step_default status_init status_end x_11681)
    831836
    832837(** val trace_any_call_rect_Type3 :
     
    835840    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    836841    __ -> trace_any_call -> 'a1 **)
    837 let rec trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default x_16523 x_16522 = function
     842let rec trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default x_11703 x_11702 = function
    838843| Tac_base status -> h_tac_base status __
    839844| Tac_step_call
    840845    (status_pre_fun_call, status_after_fun_call, status_final,
    841      status_start_fun_call, x_16528, x_16526) ->
     846     status_start_fun_call, x_11708, x_11706) ->
    842847  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    843     status_start_fun_call __ __ __ x_16528 __ x_16526
     848    status_start_fun_call __ __ __ x_11708 __ x_11706
    844849    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
    845       h_tac_step_default status_after_fun_call status_final x_16526)
    846 | Tac_step_default (status_pre, status_end, status_init, x_16533) ->
    847   h_tac_step_default status_pre status_end status_init __ x_16533 __ __
     850      h_tac_step_default status_after_fun_call status_final x_11706)
     851| Tac_step_default (status_pre, status_end, status_init, x_11713) ->
     852  h_tac_step_default status_pre status_end status_init __ x_11713 __ __
    848853    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
    849       h_tac_step_default status_init status_end x_16533)
     854      h_tac_step_default status_init status_end x_11713)
    850855
    851856(** val trace_any_call_rect_Type2 :
     
    854859    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    855860    __ -> trace_any_call -> 'a1 **)
    856 let rec trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default x_16539 x_16538 = function
     861let rec trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default x_11719 x_11718 = function
    857862| Tac_base status -> h_tac_base status __
    858863| Tac_step_call
    859864    (status_pre_fun_call, status_after_fun_call, status_final,
    860      status_start_fun_call, x_16544, x_16542) ->
     865     status_start_fun_call, x_11724, x_11722) ->
    861866  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    862     status_start_fun_call __ __ __ x_16544 __ x_16542
     867    status_start_fun_call __ __ __ x_11724 __ x_11722
    863868    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
    864       h_tac_step_default status_after_fun_call status_final x_16542)
    865 | Tac_step_default (status_pre, status_end, status_init, x_16549) ->
    866   h_tac_step_default status_pre status_end status_init __ x_16549 __ __
     869      h_tac_step_default status_after_fun_call status_final x_11722)
     870| Tac_step_default (status_pre, status_end, status_init, x_11729) ->
     871  h_tac_step_default status_pre status_end status_init __ x_11729 __ __
    867872    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
    868       h_tac_step_default status_init status_end x_16549)
     873      h_tac_step_default status_init status_end x_11729)
    869874
    870875(** val trace_any_call_rect_Type1 :
     
    873878    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    874879    __ -> trace_any_call -> 'a1 **)
    875 let rec trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default x_16555 x_16554 = function
     880let rec trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default x_11735 x_11734 = function
    876881| Tac_base status -> h_tac_base status __
    877882| Tac_step_call
    878883    (status_pre_fun_call, status_after_fun_call, status_final,
    879      status_start_fun_call, x_16560, x_16558) ->
     884     status_start_fun_call, x_11740, x_11738) ->
    880885  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    881     status_start_fun_call __ __ __ x_16560 __ x_16558
     886    status_start_fun_call __ __ __ x_11740 __ x_11738
    882887    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
    883       h_tac_step_default status_after_fun_call status_final x_16558)
    884 | Tac_step_default (status_pre, status_end, status_init, x_16565) ->
    885   h_tac_step_default status_pre status_end status_init __ x_16565 __ __
     888      h_tac_step_default status_after_fun_call status_final x_11738)
     889| Tac_step_default (status_pre, status_end, status_init, x_11745) ->
     890  h_tac_step_default status_pre status_end status_init __ x_11745 __ __
    886891    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
    887       h_tac_step_default status_init status_end x_16565)
     892      h_tac_step_default status_init status_end x_11745)
    888893
    889894(** val trace_any_call_rect_Type0 :
     
    892897    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    893898    __ -> trace_any_call -> 'a1 **)
    894 let rec trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default x_16571 x_16570 = function
     899let rec trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default x_11751 x_11750 = function
    895900| Tac_base status -> h_tac_base status __
    896901| Tac_step_call
    897902    (status_pre_fun_call, status_after_fun_call, status_final,
    898      status_start_fun_call, x_16576, x_16574) ->
     903     status_start_fun_call, x_11756, x_11754) ->
    899904  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    900     status_start_fun_call __ __ __ x_16576 __ x_16574
     905    status_start_fun_call __ __ __ x_11756 __ x_11754
    901906    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
    902       h_tac_step_default status_after_fun_call status_final x_16574)
    903 | Tac_step_default (status_pre, status_end, status_init, x_16581) ->
    904   h_tac_step_default status_pre status_end status_init __ x_16581 __ __
     907      h_tac_step_default status_after_fun_call status_final x_11754)
     908| Tac_step_default (status_pre, status_end, status_init, x_11761) ->
     909  h_tac_step_default status_pre status_end status_init __ x_11761 __ __
    905910    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
    906       h_tac_step_default status_init status_end x_16581)
     911      h_tac_step_default status_init status_end x_11761)
    907912
    908913(** val trace_any_call_inv_rect_Type4 :
     
    973978    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    974979    -> trace_label_call -> 'a1 **)
    975 let rec trace_label_call_rect_Type4 s h_tlc_base x_16689 x_16688 = function
    976 | Tlc_base (start_status, end_status, x_16692) ->
    977   h_tlc_base start_status end_status x_16692 __
     980let rec trace_label_call_rect_Type4 s h_tlc_base x_11869 x_11868 = function
     981| Tlc_base (start_status, end_status, x_11872) ->
     982  h_tlc_base start_status end_status x_11872 __
    978983
    979984(** val trace_label_call_rect_Type5 :
    980985    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    981986    -> trace_label_call -> 'a1 **)
    982 let rec trace_label_call_rect_Type5 s h_tlc_base x_16695 x_16694 = function
    983 | Tlc_base (start_status, end_status, x_16698) ->
    984   h_tlc_base start_status end_status x_16698 __
     987let rec trace_label_call_rect_Type5 s h_tlc_base x_11875 x_11874 = function
     988| Tlc_base (start_status, end_status, x_11878) ->
     989  h_tlc_base start_status end_status x_11878 __
    985990
    986991(** val trace_label_call_rect_Type3 :
    987992    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    988993    -> trace_label_call -> 'a1 **)
    989 let rec trace_label_call_rect_Type3 s h_tlc_base x_16701 x_16700 = function
    990 | Tlc_base (start_status, end_status, x_16704) ->
    991   h_tlc_base start_status end_status x_16704 __
     994let rec trace_label_call_rect_Type3 s h_tlc_base x_11881 x_11880 = function
     995| Tlc_base (start_status, end_status, x_11884) ->
     996  h_tlc_base start_status end_status x_11884 __
    992997
    993998(** val trace_label_call_rect_Type2 :
    994999    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    9951000    -> trace_label_call -> 'a1 **)
    996 let rec trace_label_call_rect_Type2 s h_tlc_base x_16707 x_16706 = function
    997 | Tlc_base (start_status, end_status, x_16710) ->
    998   h_tlc_base start_status end_status x_16710 __
     1001let rec trace_label_call_rect_Type2 s h_tlc_base x_11887 x_11886 = function
     1002| Tlc_base (start_status, end_status, x_11890) ->
     1003  h_tlc_base start_status end_status x_11890 __
    9991004
    10001005(** val trace_label_call_rect_Type1 :
    10011006    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    10021007    -> trace_label_call -> 'a1 **)
    1003 let rec trace_label_call_rect_Type1 s h_tlc_base x_16713 x_16712 = function
    1004 | Tlc_base (start_status, end_status, x_16716) ->
    1005   h_tlc_base start_status end_status x_16716 __
     1008let rec trace_label_call_rect_Type1 s h_tlc_base x_11893 x_11892 = function
     1009| Tlc_base (start_status, end_status, x_11896) ->
     1010  h_tlc_base start_status end_status x_11896 __
    10061011
    10071012(** val trace_label_call_rect_Type0 :
    10081013    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    10091014    -> trace_label_call -> 'a1 **)
    1010 let rec trace_label_call_rect_Type0 s h_tlc_base x_16719 x_16718 = function
    1011 | Tlc_base (start_status, end_status, x_16722) ->
    1012   h_tlc_base start_status end_status x_16722 __
     1015let rec trace_label_call_rect_Type0 s h_tlc_base x_11899 x_11898 = function
     1016| Tlc_base (start_status, end_status, x_11902) ->
     1017  h_tlc_base start_status end_status x_11902 __
    10131018
    10141019(** val trace_label_call_inv_rect_Type4 :
     
    10581063(** val tlc_hd_label :
    10591064    abstract_status -> __ -> __ -> trace_label_call -> CostLabel.costlabel **)
    1060 let tlc_hd_label s st1 st2 = function
    1061 | Tlc_base (st1', x, x0) -> as_label_safe s st1'
     1065let 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'))) __ __ __
    10621068
    10631069type trace_label_diverges = __trace_label_diverges Lazy.t
     
    11641170    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    11651171    -> trace_whole_program -> 'a1 **)
    1166 let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_16771 = function
     1172let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_11951 = function
    11671173| Twp_terminating
    1168     (status_initial, status_start_fun, status_final, x_16774) ->
     1174    (status_initial, status_start_fun, status_final, x_11954) ->
    11691175  h_twp_terminating status_initial status_start_fun status_final __ __
    1170     x_16774 __
    1171 | Twp_diverges (status_initial, status_start_fun, x_16777) ->
    1172   h_twp_diverges status_initial status_start_fun __ __ x_16777
     1176    x_11954 __
     1177| Twp_diverges (status_initial, status_start_fun, x_11957) ->
     1178  h_twp_diverges status_initial status_start_fun __ __ x_11957
    11731179
    11741180(** val trace_whole_program_rect_Type5 :
     
    11761182    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    11771183    -> trace_whole_program -> 'a1 **)
    1178 let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_16782 = function
     1184let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_11962 = function
    11791185| Twp_terminating
    1180     (status_initial, status_start_fun, status_final, x_16785) ->
     1186    (status_initial, status_start_fun, status_final, x_11965) ->
    11811187  h_twp_terminating status_initial status_start_fun status_final __ __
    1182     x_16785 __
    1183 | Twp_diverges (status_initial, status_start_fun, x_16788) ->
    1184   h_twp_diverges status_initial status_start_fun __ __ x_16788
     1188    x_11965 __
     1189| Twp_diverges (status_initial, status_start_fun, x_11968) ->
     1190  h_twp_diverges status_initial status_start_fun __ __ x_11968
    11851191
    11861192(** val trace_whole_program_rect_Type3 :
     
    11881194    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    11891195    -> trace_whole_program -> 'a1 **)
    1190 let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_16793 = function
     1196let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_11973 = function
    11911197| Twp_terminating
    1192     (status_initial, status_start_fun, status_final, x_16796) ->
     1198    (status_initial, status_start_fun, status_final, x_11976) ->
    11931199  h_twp_terminating status_initial status_start_fun status_final __ __
    1194     x_16796 __
    1195 | Twp_diverges (status_initial, status_start_fun, x_16799) ->
    1196   h_twp_diverges status_initial status_start_fun __ __ x_16799
     1200    x_11976 __
     1201| Twp_diverges (status_initial, status_start_fun, x_11979) ->
     1202  h_twp_diverges status_initial status_start_fun __ __ x_11979
    11971203
    11981204(** val trace_whole_program_rect_Type2 :
     
    12001206    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    12011207    -> trace_whole_program -> 'a1 **)
    1202 let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_16804 = function
     1208let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_11984 = function
    12031209| Twp_terminating
    1204     (status_initial, status_start_fun, status_final, x_16807) ->
     1210    (status_initial, status_start_fun, status_final, x_11987) ->
    12051211  h_twp_terminating status_initial status_start_fun status_final __ __
    1206     x_16807 __
    1207 | Twp_diverges (status_initial, status_start_fun, x_16810) ->
    1208   h_twp_diverges status_initial status_start_fun __ __ x_16810
     1212    x_11987 __
     1213| Twp_diverges (status_initial, status_start_fun, x_11990) ->
     1214  h_twp_diverges status_initial status_start_fun __ __ x_11990
    12091215
    12101216(** val trace_whole_program_rect_Type1 :
     
    12121218    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    12131219    -> trace_whole_program -> 'a1 **)
    1214 let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_16815 = function
     1220let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_11995 = function
    12151221| Twp_terminating
    1216     (status_initial, status_start_fun, status_final, x_16818) ->
     1222    (status_initial, status_start_fun, status_final, x_11998) ->
    12171223  h_twp_terminating status_initial status_start_fun status_final __ __
    1218     x_16818 __
    1219 | Twp_diverges (status_initial, status_start_fun, x_16821) ->
    1220   h_twp_diverges status_initial status_start_fun __ __ x_16821
     1224    x_11998 __
     1225| Twp_diverges (status_initial, status_start_fun, x_12001) ->
     1226  h_twp_diverges status_initial status_start_fun __ __ x_12001
    12211227
    12221228(** val trace_whole_program_rect_Type0 :
     
    12241230    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    12251231    -> trace_whole_program -> 'a1 **)
    1226 let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_16826 = function
     1232let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_12006 = function
    12271233| Twp_terminating
    1228     (status_initial, status_start_fun, status_final, x_16829) ->
     1234    (status_initial, status_start_fun, status_final, x_12009) ->
    12291235  h_twp_terminating status_initial status_start_fun status_final __ __
    1230     x_16829 __
    1231 | Twp_diverges (status_initial, status_start_fun, x_16832) ->
    1232   h_twp_diverges status_initial status_start_fun __ __ x_16832
     1236    x_12009 __
     1237| Twp_diverges (status_initial, status_start_fun, x_12012) ->
     1238  h_twp_diverges status_initial status_start_fun __ __ x_12012
    12331239
    12341240(** val trace_whole_program_inv_rect_Type4 :
     
    12801286    abstract_status -> __ -> __ -> trace_any_label -> CostLabel.costlabel **)
    12811287let tal_tl_label s st1 st2 tr =
    1282   as_label_safe s st2
     1288  Types.pi1 (as_label_safe s st2)
    12831289
    12841290(** val tll_tl_label :
    12851291    abstract_status -> __ -> __ -> trace_label_label -> CostLabel.costlabel **)
    12861292let tll_tl_label s st1 st2 tr =
    1287   as_label_safe s st2
     1293  Types.pi1 (as_label_safe s st2)
    12881294
    12891295type trace_any_any =
     
    12941300    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    12951301    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
    1296 let rec trace_any_any_rect_Type4 s h_taa_base h_taa_step x_17056 x_17055 = function
     1302let rec trace_any_any_rect_Type4 s h_taa_base h_taa_step x_12236 x_12235 = function
    12971303| Taa_base st -> h_taa_base st
    1298 | Taa_step (st1, st2, st3, x_17058) ->
    1299   h_taa_step st1 st2 st3 __ __ __ x_17058
    1300     (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_17058)
     1304| Taa_step (st1, st2, st3, x_12238) ->
     1305  h_taa_step st1 st2 st3 __ __ __ x_12238
     1306    (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_12238)
    13011307
    13021308(** val trace_any_any_rect_Type3 :
    13031309    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13041310    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
    1305 let rec trace_any_any_rect_Type3 s h_taa_base h_taa_step x_17074 x_17073 = function
     1311let rec trace_any_any_rect_Type3 s h_taa_base h_taa_step x_12254 x_12253 = function
    13061312| Taa_base st -> h_taa_base st
    1307 | Taa_step (st1, st2, st3, x_17076) ->
    1308   h_taa_step st1 st2 st3 __ __ __ x_17076
    1309     (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_17076)
     1313| Taa_step (st1, st2, st3, x_12256) ->
     1314  h_taa_step st1 st2 st3 __ __ __ x_12256
     1315    (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_12256)
    13101316
    13111317(** val trace_any_any_rect_Type2 :
    13121318    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13131319    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
    1314 let rec trace_any_any_rect_Type2 s h_taa_base h_taa_step x_17083 x_17082 = function
     1320let rec trace_any_any_rect_Type2 s h_taa_base h_taa_step x_12263 x_12262 = function
    13151321| Taa_base st -> h_taa_base st
    1316 | Taa_step (st1, st2, st3, x_17085) ->
    1317   h_taa_step st1 st2 st3 __ __ __ x_17085
    1318     (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_17085)
     1322| Taa_step (st1, st2, st3, x_12265) ->
     1323  h_taa_step st1 st2 st3 __ __ __ x_12265
     1324    (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_12265)
    13191325
    13201326(** val trace_any_any_rect_Type1 :
    13211327    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13221328    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
    1323 let rec trace_any_any_rect_Type1 s h_taa_base h_taa_step x_17092 x_17091 = function
     1329let rec trace_any_any_rect_Type1 s h_taa_base h_taa_step x_12272 x_12271 = function
    13241330| Taa_base st -> h_taa_base st
    1325 | Taa_step (st1, st2, st3, x_17094) ->
    1326   h_taa_step st1 st2 st3 __ __ __ x_17094
    1327     (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_17094)
     1331| Taa_step (st1, st2, st3, x_12274) ->
     1332  h_taa_step st1 st2 st3 __ __ __ x_12274
     1333    (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_12274)
    13281334
    13291335(** val trace_any_any_rect_Type0 :
    13301336    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13311337    trace_any_any -> 'a1 -> 'a1) -> __ -> __ -> trace_any_any -> 'a1 **)
    1332 let rec trace_any_any_rect_Type0 s h_taa_base h_taa_step x_17101 x_17100 = function
     1338let rec trace_any_any_rect_Type0 s h_taa_base h_taa_step x_12281 x_12280 = function
    13331339| Taa_base st -> h_taa_base st
    1334 | Taa_step (st1, st2, st3, x_17103) ->
    1335   h_taa_step st1 st2 st3 __ __ __ x_17103
    1336     (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_17103)
     1340| Taa_step (st1, st2, st3, x_12283) ->
     1341  h_taa_step st1 st2 st3 __ __ __ x_12283
     1342    (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_12283)
    13371343
    13381344(** val trace_any_any_inv_rect_Type4 :
     
    14401446       (taa_append_tal s st2' fl0 st3' st30 tl tal2)))) fl st3
    14411447
    1442 type tal_collapsable = __
    1443 
    1444 type tal_rel = __
    1445 
    1446 type tll_rel = __
    1447 
    1448 type tlr_rel = __
     1448type 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 **)
     1457let rec intensional_event_rect_Type4 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
     1458| IEVcost x_12354 -> h_IEVcost x_12354
     1459| IEVcall x_12355 -> h_IEVcall x_12355
     1460| IEVtailcall (x_12357, x_12356) -> h_IEVtailcall x_12357 x_12356
     1461| IEVret x_12358 -> h_IEVret x_12358
     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 **)
     1466let rec intensional_event_rect_Type5 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
     1467| IEVcost x_12364 -> h_IEVcost x_12364
     1468| IEVcall x_12365 -> h_IEVcall x_12365
     1469| IEVtailcall (x_12367, x_12366) -> h_IEVtailcall x_12367 x_12366
     1470| IEVret x_12368 -> h_IEVret x_12368
     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 **)
     1475let rec intensional_event_rect_Type3 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
     1476| IEVcost x_12374 -> h_IEVcost x_12374
     1477| IEVcall x_12375 -> h_IEVcall x_12375
     1478| IEVtailcall (x_12377, x_12376) -> h_IEVtailcall x_12377 x_12376
     1479| IEVret x_12378 -> h_IEVret x_12378
     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 **)
     1484let rec intensional_event_rect_Type2 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
     1485| IEVcost x_12384 -> h_IEVcost x_12384
     1486| IEVcall x_12385 -> h_IEVcall x_12385
     1487| IEVtailcall (x_12387, x_12386) -> h_IEVtailcall x_12387 x_12386
     1488| IEVret x_12388 -> h_IEVret x_12388
     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 **)
     1493let rec intensional_event_rect_Type1 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
     1494| IEVcost x_12394 -> h_IEVcost x_12394
     1495| IEVcall x_12395 -> h_IEVcall x_12395
     1496| IEVtailcall (x_12397, x_12396) -> h_IEVtailcall x_12397 x_12396
     1497| IEVret x_12398 -> h_IEVret x_12398
     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 **)
     1502let rec intensional_event_rect_Type0 h_IEVcost h_IEVcall h_IEVtailcall h_IEVret = function
     1503| IEVcost x_12404 -> h_IEVcost x_12404
     1504| IEVcall x_12405 -> h_IEVcall x_12405
     1505| IEVtailcall (x_12407, x_12406) -> h_IEVtailcall x_12407 x_12406
     1506| IEVret x_12408 -> h_IEVret x_12408
     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 **)
     1512let 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 **)
     1519let 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 **)
     1526let 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 **)
     1533let 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 **)
     1540let 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 -> __ **)
     1545let 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 -> __ **)
     1555let 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
     1563type 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 **)
     1567let 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 **)
     1573let append_safe l1 l2 =
     1574  List.append (Types.pi1 l1) (Types.pi1 l2)
     1575
     1576(** val nil_safe : 'a1 List.list Types.sig0 **)
     1577let nil_safe =
     1578  List.Nil
     1579
     1580(** val emittable_cost :
     1581    abstract_status -> as_cost_label -> intensional_event Types.sig0 **)
     1582let 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 **)
     1588let 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 **)
     1596and 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 **)
     1628and 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 **)
     1645let 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 **)
     1655let 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 **)
     1663let 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 **)
     1668let 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 **)
     1674let 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 **)
     1685let 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)
    14491689
    14501690(** val flatten_trace_label_label :
    14511691    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_label_label
    14521692    -> as_cost_label List.list **)
    1453 let rec flatten_trace_label_label s trace_ends_flag start_status final_status = function
    1454 | Tll_base (ends_flag, initial, final, given_trace) ->
    1455   let label =
    1456     (match as_label s initial with
    1457      | Types.None -> (fun _ -> assert false (* absurd case *))
    1458      | Types.Some l -> (fun _ -> l)) __
    1459   in
    1460   List.Cons (label,
    1461   (flatten_trace_any_label s ends_flag initial final given_trace))
     1693let 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
    14621698(** val flatten_trace_any_label :
    14631699    abstract_status -> trace_ends_with_ret -> __ -> __ -> trace_any_label ->
    14641700    as_cost_label List.list **)
    1465 and flatten_trace_any_label s trace_ends_flag start_status final_status = function
    1466 | Tal_base_not_return (the_status, x) -> List.Nil
    1467 | Tal_base_return (the_status, x) -> List.Nil
    1468 | Tal_base_call (pre_fun_call, start_fun_call, final, call_trace) ->
    1469   flatten_trace_label_return s start_fun_call final call_trace
    1470 | Tal_base_tailcall (pre_fun_call, start_fun_call, final, call_trace) ->
    1471   flatten_trace_label_return s start_fun_call final call_trace
    1472 | Tal_step_call
    1473     (end_flag, pre_fun_call, start_fun_call, after_fun_call, final,
    1474      call_trace, final_trace) ->
    1475   let call_cost_trace =
    1476     flatten_trace_label_return s start_fun_call after_fun_call call_trace
    1477   in
    1478   let final_cost_trace =
    1479     flatten_trace_any_label s end_flag after_fun_call final final_trace
    1480   in
    1481   List.append call_cost_trace final_cost_trace
    1482 | Tal_step_default
    1483     (end_flag, status_pre, status_init, status_end, tail_trace) ->
    1484   flatten_trace_any_label s end_flag status_init status_end tail_trace
    1485 (** val flatten_trace_label_return :
    1486     abstract_status -> __ -> __ -> trace_label_return -> as_cost_label
    1487     List.list **)
    1488 and flatten_trace_label_return s start_status final_status = function
    1489 | Tlr_base (before, after, trace_to_lift) ->
    1490   flatten_trace_label_label s Ends_with_ret before after trace_to_lift
    1491 | Tlr_step (initial, labelled, final, labelled_trace, ret_trace) ->
    1492   let labelled_cost =
    1493     flatten_trace_label_label s Doesnt_end_with_ret initial labelled
    1494       labelled_trace
    1495   in
    1496   let return_cost = flatten_trace_label_return s labelled final ret_trace in
    1497   List.append labelled_cost return_cost
    1498 
     1701let 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
Note: See TracChangeset for help on using the changeset viewer.