Ignore:
Timestamp:
Mar 5, 2013, 9:52:39 PM (7 years ago)
Author:
sacerdot
Message:

The compiler now computes also the stack cost model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/structuredTraces.ml

    r2773 r2775  
    219219    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
    220220    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
    221 let rec abstract_status_rect_Type4 h_mk_abstract_status x_11583 =
     221let rec abstract_status_rect_Type4 h_mk_abstract_status x_16414 =
    222222  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    223223    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
     224    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16414
    225225  in
    226226  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    232232    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
    233233    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
    234 let rec abstract_status_rect_Type5 h_mk_abstract_status x_11585 =
     234let rec abstract_status_rect_Type5 h_mk_abstract_status x_16416 =
    235235  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    236236    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
     237    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16416
    238238  in
    239239  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    245245    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
    246246    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
    247 let rec abstract_status_rect_Type3 h_mk_abstract_status x_11587 =
     247let rec abstract_status_rect_Type3 h_mk_abstract_status x_16418 =
    248248  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    249249    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
     250    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16418
    251251  in
    252252  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    258258    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
    259259    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
    260 let rec abstract_status_rect_Type2 h_mk_abstract_status x_11589 =
     260let rec abstract_status_rect_Type2 h_mk_abstract_status x_16420 =
    261261  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    262262    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
     263    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16420
    264264  in
    265265  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    271271    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
    272272    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
    273 let rec abstract_status_rect_Type1 h_mk_abstract_status x_11591 =
     273let rec abstract_status_rect_Type1 h_mk_abstract_status x_16422 =
    274274  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    275275    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
     276    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16422
    277277  in
    278278  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    284284    Types.option) -> (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 ->
    285285    AST.ident) -> 'a1) -> abstract_status -> 'a1 **)
    286 let rec abstract_status_rect_Type0 h_mk_abstract_status x_11593 =
     286let rec abstract_status_rect_Type0 h_mk_abstract_status x_16424 =
    287287  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    288288    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
     289    as_call_ident0; as_tailcall_ident = as_tailcall_ident0 } = x_16424
    290290  in
    291291  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    821821    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    822822    __ -> 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_11671 x_11670 = function
     823let rec trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default x_16502 x_16501 = function
    824824| Tac_base status -> h_tac_base status __
    825825| Tac_step_call
    826826    (status_pre_fun_call, status_after_fun_call, status_final,
    827      status_start_fun_call, x_11676, x_11674) ->
     827     status_start_fun_call, x_16507, x_16505) ->
    828828  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    829     status_start_fun_call __ __ __ x_11676 __ x_11674
     829    status_start_fun_call __ __ __ x_16507 __ x_16505
    830830    (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_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 __ __
     831      h_tac_step_default status_after_fun_call status_final x_16505)
     832| Tac_step_default (status_pre, status_end, status_init, x_16512) ->
     833  h_tac_step_default status_pre status_end status_init __ x_16512 __ __
    834834    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
    835       h_tac_step_default status_init status_end x_11681)
     835      h_tac_step_default status_init status_end x_16512)
    836836
    837837(** val trace_any_call_rect_Type3 :
     
    840840    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    841841    __ -> 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_11703 x_11702 = function
     842let rec trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default x_16534 x_16533 = function
    843843| Tac_base status -> h_tac_base status __
    844844| Tac_step_call
    845845    (status_pre_fun_call, status_after_fun_call, status_final,
    846      status_start_fun_call, x_11708, x_11706) ->
     846     status_start_fun_call, x_16539, x_16537) ->
    847847  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    848     status_start_fun_call __ __ __ x_11708 __ x_11706
     848    status_start_fun_call __ __ __ x_16539 __ x_16537
    849849    (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_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 __ __
     850      h_tac_step_default status_after_fun_call status_final x_16537)
     851| Tac_step_default (status_pre, status_end, status_init, x_16544) ->
     852  h_tac_step_default status_pre status_end status_init __ x_16544 __ __
    853853    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
    854       h_tac_step_default status_init status_end x_11713)
     854      h_tac_step_default status_init status_end x_16544)
    855855
    856856(** val trace_any_call_rect_Type2 :
     
    859859    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    860860    __ -> 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_11719 x_11718 = function
     861let rec trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default x_16550 x_16549 = function
    862862| Tac_base status -> h_tac_base status __
    863863| Tac_step_call
    864864    (status_pre_fun_call, status_after_fun_call, status_final,
    865      status_start_fun_call, x_11724, x_11722) ->
     865     status_start_fun_call, x_16555, x_16553) ->
    866866  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    867     status_start_fun_call __ __ __ x_11724 __ x_11722
     867    status_start_fun_call __ __ __ x_16555 __ x_16553
    868868    (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_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 __ __
     869      h_tac_step_default status_after_fun_call status_final x_16553)
     870| Tac_step_default (status_pre, status_end, status_init, x_16560) ->
     871  h_tac_step_default status_pre status_end status_init __ x_16560 __ __
    872872    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
    873       h_tac_step_default status_init status_end x_11729)
     873      h_tac_step_default status_init status_end x_16560)
    874874
    875875(** val trace_any_call_rect_Type1 :
     
    878878    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    879879    __ -> 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_11735 x_11734 = function
     880let rec trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default x_16566 x_16565 = function
    881881| Tac_base status -> h_tac_base status __
    882882| Tac_step_call
    883883    (status_pre_fun_call, status_after_fun_call, status_final,
    884      status_start_fun_call, x_11740, x_11738) ->
     884     status_start_fun_call, x_16571, x_16569) ->
    885885  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    886     status_start_fun_call __ __ __ x_11740 __ x_11738
     886    status_start_fun_call __ __ __ x_16571 __ x_16569
    887887    (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_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 __ __
     888      h_tac_step_default status_after_fun_call status_final x_16569)
     889| Tac_step_default (status_pre, status_end, status_init, x_16576) ->
     890  h_tac_step_default status_pre status_end status_init __ x_16576 __ __
    891891    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
    892       h_tac_step_default status_init status_end x_11745)
     892      h_tac_step_default status_init status_end x_16576)
    893893
    894894(** val trace_any_call_rect_Type0 :
     
    897897    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    898898    __ -> 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_11751 x_11750 = function
     899let rec trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default x_16582 x_16581 = function
    900900| Tac_base status -> h_tac_base status __
    901901| Tac_step_call
    902902    (status_pre_fun_call, status_after_fun_call, status_final,
    903      status_start_fun_call, x_11756, x_11754) ->
     903     status_start_fun_call, x_16587, x_16585) ->
    904904  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    905     status_start_fun_call __ __ __ x_11756 __ x_11754
     905    status_start_fun_call __ __ __ x_16587 __ x_16585
    906906    (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_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 __ __
     907      h_tac_step_default status_after_fun_call status_final x_16585)
     908| Tac_step_default (status_pre, status_end, status_init, x_16592) ->
     909  h_tac_step_default status_pre status_end status_init __ x_16592 __ __
    910910    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
    911       h_tac_step_default status_init status_end x_11761)
     911      h_tac_step_default status_init status_end x_16592)
    912912
    913913(** val trace_any_call_inv_rect_Type4 :
     
    978978    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    979979    -> trace_label_call -> 'a1 **)
    980 let 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 __
     980let rec trace_label_call_rect_Type4 s h_tlc_base x_16700 x_16699 = function
     981| Tlc_base (start_status, end_status, x_16703) ->
     982  h_tlc_base start_status end_status x_16703 __
    983983
    984984(** val trace_label_call_rect_Type5 :
    985985    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    986986    -> trace_label_call -> 'a1 **)
    987 let 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 __
     987let rec trace_label_call_rect_Type5 s h_tlc_base x_16706 x_16705 = function
     988| Tlc_base (start_status, end_status, x_16709) ->
     989  h_tlc_base start_status end_status x_16709 __
    990990
    991991(** val trace_label_call_rect_Type3 :
    992992    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    993993    -> trace_label_call -> 'a1 **)
    994 let 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 __
     994let rec trace_label_call_rect_Type3 s h_tlc_base x_16712 x_16711 = function
     995| Tlc_base (start_status, end_status, x_16715) ->
     996  h_tlc_base start_status end_status x_16715 __
    997997
    998998(** val trace_label_call_rect_Type2 :
    999999    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    10001000    -> trace_label_call -> 'a1 **)
    1001 let 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 __
     1001let rec trace_label_call_rect_Type2 s h_tlc_base x_16718 x_16717 = function
     1002| Tlc_base (start_status, end_status, x_16721) ->
     1003  h_tlc_base start_status end_status x_16721 __
    10041004
    10051005(** val trace_label_call_rect_Type1 :
    10061006    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    10071007    -> trace_label_call -> 'a1 **)
    1008 let 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 __
     1008let rec trace_label_call_rect_Type1 s h_tlc_base x_16724 x_16723 = function
     1009| Tlc_base (start_status, end_status, x_16727) ->
     1010  h_tlc_base start_status end_status x_16727 __
    10111011
    10121012(** val trace_label_call_rect_Type0 :
    10131013    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    10141014    -> trace_label_call -> 'a1 **)
    1015 let 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 __
     1015let rec trace_label_call_rect_Type0 s h_tlc_base x_16730 x_16729 = function
     1016| Tlc_base (start_status, end_status, x_16733) ->
     1017  h_tlc_base start_status end_status x_16733 __
    10181018
    10191019(** val trace_label_call_inv_rect_Type4 :
     
    11701170    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    11711171    -> trace_whole_program -> 'a1 **)
    1172 let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_11951 = function
     1172let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_16782 = function
    11731173| Twp_terminating
    1174     (status_initial, status_start_fun, status_final, x_11954) ->
     1174    (status_initial, status_start_fun, status_final, x_16785) ->
    11751175  h_twp_terminating status_initial status_start_fun status_final __ __
    1176     x_11954 __
    1177 | Twp_diverges (status_initial, status_start_fun, x_11957) ->
    1178   h_twp_diverges status_initial status_start_fun __ __ x_11957
     1176    x_16785 __
     1177| Twp_diverges (status_initial, status_start_fun, x_16788) ->
     1178  h_twp_diverges status_initial status_start_fun __ __ x_16788
    11791179
    11801180(** val trace_whole_program_rect_Type5 :
     
    11821182    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    11831183    -> trace_whole_program -> 'a1 **)
    1184 let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_11962 = function
     1184let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_16793 = function
    11851185| Twp_terminating
    1186     (status_initial, status_start_fun, status_final, x_11965) ->
     1186    (status_initial, status_start_fun, status_final, x_16796) ->
    11871187  h_twp_terminating status_initial status_start_fun status_final __ __
    1188     x_11965 __
    1189 | Twp_diverges (status_initial, status_start_fun, x_11968) ->
    1190   h_twp_diverges status_initial status_start_fun __ __ x_11968
     1188    x_16796 __
     1189| Twp_diverges (status_initial, status_start_fun, x_16799) ->
     1190  h_twp_diverges status_initial status_start_fun __ __ x_16799
    11911191
    11921192(** val trace_whole_program_rect_Type3 :
     
    11941194    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    11951195    -> trace_whole_program -> 'a1 **)
    1196 let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_11973 = function
     1196let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_16804 = function
    11971197| Twp_terminating
    1198     (status_initial, status_start_fun, status_final, x_11976) ->
     1198    (status_initial, status_start_fun, status_final, x_16807) ->
    11991199  h_twp_terminating status_initial status_start_fun status_final __ __
    1200     x_11976 __
    1201 | Twp_diverges (status_initial, status_start_fun, x_11979) ->
    1202   h_twp_diverges status_initial status_start_fun __ __ x_11979
     1200    x_16807 __
     1201| Twp_diverges (status_initial, status_start_fun, x_16810) ->
     1202  h_twp_diverges status_initial status_start_fun __ __ x_16810
    12031203
    12041204(** val trace_whole_program_rect_Type2 :
     
    12061206    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    12071207    -> trace_whole_program -> 'a1 **)
    1208 let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_11984 = function
     1208let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_16815 = function
    12091209| Twp_terminating
    1210     (status_initial, status_start_fun, status_final, x_11987) ->
     1210    (status_initial, status_start_fun, status_final, x_16818) ->
    12111211  h_twp_terminating status_initial status_start_fun status_final __ __
    1212     x_11987 __
    1213 | Twp_diverges (status_initial, status_start_fun, x_11990) ->
    1214   h_twp_diverges status_initial status_start_fun __ __ x_11990
     1212    x_16818 __
     1213| Twp_diverges (status_initial, status_start_fun, x_16821) ->
     1214  h_twp_diverges status_initial status_start_fun __ __ x_16821
    12151215
    12161216(** val trace_whole_program_rect_Type1 :
     
    12181218    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    12191219    -> trace_whole_program -> 'a1 **)
    1220 let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_11995 = function
     1220let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_16826 = function
    12211221| Twp_terminating
    1222     (status_initial, status_start_fun, status_final, x_11998) ->
     1222    (status_initial, status_start_fun, status_final, x_16829) ->
    12231223  h_twp_terminating status_initial status_start_fun status_final __ __
    1224     x_11998 __
    1225 | Twp_diverges (status_initial, status_start_fun, x_12001) ->
    1226   h_twp_diverges status_initial status_start_fun __ __ x_12001
     1224    x_16829 __
     1225| Twp_diverges (status_initial, status_start_fun, x_16832) ->
     1226  h_twp_diverges status_initial status_start_fun __ __ x_16832
    12271227
    12281228(** val trace_whole_program_rect_Type0 :
     
    12301230    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    12311231    -> trace_whole_program -> 'a1 **)
    1232 let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_12006 = function
     1232let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_16837 = function
    12331233| Twp_terminating
    1234     (status_initial, status_start_fun, status_final, x_12009) ->
     1234    (status_initial, status_start_fun, status_final, x_16840) ->
    12351235  h_twp_terminating status_initial status_start_fun status_final __ __
    1236     x_12009 __
    1237 | Twp_diverges (status_initial, status_start_fun, x_12012) ->
    1238   h_twp_diverges status_initial status_start_fun __ __ x_12012
     1236    x_16840 __
     1237| Twp_diverges (status_initial, status_start_fun, x_16843) ->
     1238  h_twp_diverges status_initial status_start_fun __ __ x_16843
    12391239
    12401240(** val trace_whole_program_inv_rect_Type4 :
     
    13001300    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13011301    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_12236 x_12235 = function
     1302let rec trace_any_any_rect_Type4 s h_taa_base h_taa_step x_17067 x_17066 = function
    13031303| Taa_base st -> h_taa_base st
    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)
     1304| Taa_step (st1, st2, st3, x_17069) ->
     1305  h_taa_step st1 st2 st3 __ __ __ x_17069
     1306    (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_17069)
    13071307
    13081308(** val trace_any_any_rect_Type3 :
    13091309    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13101310    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_12254 x_12253 = function
     1311let rec trace_any_any_rect_Type3 s h_taa_base h_taa_step x_17085 x_17084 = function
    13121312| Taa_base st -> h_taa_base st
    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)
     1313| Taa_step (st1, st2, st3, x_17087) ->
     1314  h_taa_step st1 st2 st3 __ __ __ x_17087
     1315    (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_17087)
    13161316
    13171317(** val trace_any_any_rect_Type2 :
    13181318    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13191319    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_12263 x_12262 = function
     1320let rec trace_any_any_rect_Type2 s h_taa_base h_taa_step x_17094 x_17093 = function
    13211321| Taa_base st -> h_taa_base st
    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)
     1322| Taa_step (st1, st2, st3, x_17096) ->
     1323  h_taa_step st1 st2 st3 __ __ __ x_17096
     1324    (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_17096)
    13251325
    13261326(** val trace_any_any_rect_Type1 :
    13271327    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13281328    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_12272 x_12271 = function
     1329let rec trace_any_any_rect_Type1 s h_taa_base h_taa_step x_17103 x_17102 = function
    13301330| Taa_base st -> h_taa_base st
    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)
     1331| Taa_step (st1, st2, st3, x_17105) ->
     1332  h_taa_step st1 st2 st3 __ __ __ x_17105
     1333    (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_17105)
    13341334
    13351335(** val trace_any_any_rect_Type0 :
    13361336    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13371337    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_12281 x_12280 = function
     1338let rec trace_any_any_rect_Type0 s h_taa_base h_taa_step x_17112 x_17111 = function
    13391339| Taa_base st -> h_taa_base st
    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)
     1340| Taa_step (st1, st2, st3, x_17114) ->
     1341  h_taa_step st1 st2 st3 __ __ __ x_17114
     1342    (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_17114)
    13431343
    13441344(** val trace_any_any_inv_rect_Type4 :
     
    14561456    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
    14571457let 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
     1458| IEVcost x_17185 -> h_IEVcost x_17185
     1459| IEVcall x_17186 -> h_IEVcall x_17186
     1460| IEVtailcall (x_17188, x_17187) -> h_IEVtailcall x_17188 x_17187
     1461| IEVret x_17189 -> h_IEVret x_17189
    14621462
    14631463(** val intensional_event_rect_Type5 :
     
    14651465    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
    14661466let 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
     1467| IEVcost x_17195 -> h_IEVcost x_17195
     1468| IEVcall x_17196 -> h_IEVcall x_17196
     1469| IEVtailcall (x_17198, x_17197) -> h_IEVtailcall x_17198 x_17197
     1470| IEVret x_17199 -> h_IEVret x_17199
    14711471
    14721472(** val intensional_event_rect_Type3 :
     
    14741474    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
    14751475let 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
     1476| IEVcost x_17205 -> h_IEVcost x_17205
     1477| IEVcall x_17206 -> h_IEVcall x_17206
     1478| IEVtailcall (x_17208, x_17207) -> h_IEVtailcall x_17208 x_17207
     1479| IEVret x_17209 -> h_IEVret x_17209
    14801480
    14811481(** val intensional_event_rect_Type2 :
     
    14831483    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
    14841484let 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
     1485| IEVcost x_17215 -> h_IEVcost x_17215
     1486| IEVcall x_17216 -> h_IEVcall x_17216
     1487| IEVtailcall (x_17218, x_17217) -> h_IEVtailcall x_17218 x_17217
     1488| IEVret x_17219 -> h_IEVret x_17219
    14891489
    14901490(** val intensional_event_rect_Type1 :
     
    14921492    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
    14931493let 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
     1494| IEVcost x_17225 -> h_IEVcost x_17225
     1495| IEVcall x_17226 -> h_IEVcall x_17226
     1496| IEVtailcall (x_17228, x_17227) -> h_IEVtailcall x_17228 x_17227
     1497| IEVret x_17229 -> h_IEVret x_17229
    14981498
    14991499(** val intensional_event_rect_Type0 :
     
    15011501    AST.ident -> 'a1) -> (AST.ident -> 'a1) -> intensional_event -> 'a1 **)
    15021502let 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
     1503| IEVcost x_17235 -> h_IEVcost x_17235
     1504| IEVcall x_17236 -> h_IEVcall x_17236
     1505| IEVtailcall (x_17238, x_17237) -> h_IEVtailcall x_17238 x_17237
     1506| IEVret x_17239 -> h_IEVret x_17239
    15071507
    15081508(** val intensional_event_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.