Ignore:
Timestamp:
Feb 25, 2013, 9:54:49 PM (7 years ago)
Author:
sacerdot
Message:

Exported again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/structuredTraces.ml

    r2717 r2730  
    200200    (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
    201201    abstract_status -> 'a1 **)
    202 let rec abstract_status_rect_Type4 h_mk_abstract_status x_21716 =
     202let rec abstract_status_rect_Type4 h_mk_abstract_status x_1933 =
    203203  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    204204    as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
    205     as_tailcall_ident = as_tailcall_ident0 } = x_21716
     205    as_tailcall_ident = as_tailcall_ident0 } = x_1933
    206206  in
    207207  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    213213    (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
    214214    abstract_status -> 'a1 **)
    215 let rec abstract_status_rect_Type5 h_mk_abstract_status x_21718 =
     215let rec abstract_status_rect_Type5 h_mk_abstract_status x_1935 =
    216216  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    217217    as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
    218     as_tailcall_ident = as_tailcall_ident0 } = x_21718
     218    as_tailcall_ident = as_tailcall_ident0 } = x_1935
    219219  in
    220220  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    226226    (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
    227227    abstract_status -> 'a1 **)
    228 let rec abstract_status_rect_Type3 h_mk_abstract_status x_21720 =
     228let rec abstract_status_rect_Type3 h_mk_abstract_status x_1937 =
    229229  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    230230    as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
    231     as_tailcall_ident = as_tailcall_ident0 } = x_21720
     231    as_tailcall_ident = as_tailcall_ident0 } = x_1937
    232232  in
    233233  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    239239    (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
    240240    abstract_status -> 'a1 **)
    241 let rec abstract_status_rect_Type2 h_mk_abstract_status x_21722 =
     241let rec abstract_status_rect_Type2 h_mk_abstract_status x_1939 =
    242242  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    243243    as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
    244     as_tailcall_ident = as_tailcall_ident0 } = x_21722
     244    as_tailcall_ident = as_tailcall_ident0 } = x_1939
    245245  in
    246246  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    252252    (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
    253253    abstract_status -> 'a1 **)
    254 let rec abstract_status_rect_Type1 h_mk_abstract_status x_21724 =
     254let rec abstract_status_rect_Type1 h_mk_abstract_status x_1941 =
    255255  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    256256    as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
    257     as_tailcall_ident = as_tailcall_ident0 } = x_21724
     257    as_tailcall_ident = as_tailcall_ident0 } = x_1941
    258258  in
    259259  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    265265    (__ Types.sig0 -> AST.ident) -> (__ Types.sig0 -> AST.ident) -> 'a1) ->
    266266    abstract_status -> 'a1 **)
    267 let rec abstract_status_rect_Type0 h_mk_abstract_status x_21726 =
     267let rec abstract_status_rect_Type0 h_mk_abstract_status x_1943 =
    268268  let { as_pc = as_pc0; as_pc_of = as_pc_of0; as_classify = as_classify0;
    269269    as_label_of_pc = as_label_of_pc0; as_call_ident = as_call_ident0;
    270     as_tailcall_ident = as_tailcall_ident0 } = x_21726
     270    as_tailcall_ident = as_tailcall_ident0 } = x_1943
    271271  in
    272272  h_mk_abstract_status __ __ as_pc0 as_pc_of0 as_classify0 as_label_of_pc0 __
     
    816816    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    817817    __ -> 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_21806 x_21805 = function
     818let rec trace_any_call_rect_Type4 s h_tac_base h_tac_step_call h_tac_step_default x_2023 x_2022 = function
    819819| Tac_base status -> h_tac_base status __
    820820| Tac_step_call
    821821    (status_pre_fun_call, status_after_fun_call, status_final,
    822      status_start_fun_call, x_21811, x_21809) ->
     822     status_start_fun_call, x_2028, x_2026) ->
    823823  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    824     status_start_fun_call __ __ __ x_21811 __ x_21809
     824    status_start_fun_call __ __ __ x_2028 __ x_2026
    825825    (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_21809)
    827 | Tac_step_default (status_pre, status_end, status_init, x_21816) ->
    828   h_tac_step_default status_pre status_end status_init __ x_21816 __ __
     826      h_tac_step_default status_after_fun_call status_final x_2026)
     827| Tac_step_default (status_pre, status_end, status_init, x_2033) ->
     828  h_tac_step_default status_pre status_end status_init __ x_2033 __ __
    829829    (trace_any_call_rect_Type4 s h_tac_base h_tac_step_call
    830       h_tac_step_default status_init status_end x_21816)
     830      h_tac_step_default status_init status_end x_2033)
    831831
    832832(** val trace_any_call_rect_Type3 :
     
    835835    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    836836    __ -> 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_21838 x_21837 = function
     837let rec trace_any_call_rect_Type3 s h_tac_base h_tac_step_call h_tac_step_default x_2055 x_2054 = function
    838838| Tac_base status -> h_tac_base status __
    839839| Tac_step_call
    840840    (status_pre_fun_call, status_after_fun_call, status_final,
    841      status_start_fun_call, x_21843, x_21841) ->
     841     status_start_fun_call, x_2060, x_2058) ->
    842842  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    843     status_start_fun_call __ __ __ x_21843 __ x_21841
     843    status_start_fun_call __ __ __ x_2060 __ x_2058
    844844    (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_21841)
    846 | Tac_step_default (status_pre, status_end, status_init, x_21848) ->
    847   h_tac_step_default status_pre status_end status_init __ x_21848 __ __
     845      h_tac_step_default status_after_fun_call status_final x_2058)
     846| Tac_step_default (status_pre, status_end, status_init, x_2065) ->
     847  h_tac_step_default status_pre status_end status_init __ x_2065 __ __
    848848    (trace_any_call_rect_Type3 s h_tac_base h_tac_step_call
    849       h_tac_step_default status_init status_end x_21848)
     849      h_tac_step_default status_init status_end x_2065)
    850850
    851851(** val trace_any_call_rect_Type2 :
     
    854854    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    855855    __ -> 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_21854 x_21853 = function
     856let rec trace_any_call_rect_Type2 s h_tac_base h_tac_step_call h_tac_step_default x_2071 x_2070 = function
    857857| Tac_base status -> h_tac_base status __
    858858| Tac_step_call
    859859    (status_pre_fun_call, status_after_fun_call, status_final,
    860      status_start_fun_call, x_21859, x_21857) ->
     860     status_start_fun_call, x_2076, x_2074) ->
    861861  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    862     status_start_fun_call __ __ __ x_21859 __ x_21857
     862    status_start_fun_call __ __ __ x_2076 __ x_2074
    863863    (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_21857)
    865 | Tac_step_default (status_pre, status_end, status_init, x_21864) ->
    866   h_tac_step_default status_pre status_end status_init __ x_21864 __ __
     864      h_tac_step_default status_after_fun_call status_final x_2074)
     865| Tac_step_default (status_pre, status_end, status_init, x_2081) ->
     866  h_tac_step_default status_pre status_end status_init __ x_2081 __ __
    867867    (trace_any_call_rect_Type2 s h_tac_base h_tac_step_call
    868       h_tac_step_default status_init status_end x_21864)
     868      h_tac_step_default status_init status_end x_2081)
    869869
    870870(** val trace_any_call_rect_Type1 :
     
    873873    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    874874    __ -> 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_21870 x_21869 = function
     875let rec trace_any_call_rect_Type1 s h_tac_base h_tac_step_call h_tac_step_default x_2087 x_2086 = function
    876876| Tac_base status -> h_tac_base status __
    877877| Tac_step_call
    878878    (status_pre_fun_call, status_after_fun_call, status_final,
    879      status_start_fun_call, x_21875, x_21873) ->
     879     status_start_fun_call, x_2092, x_2090) ->
    880880  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    881     status_start_fun_call __ __ __ x_21875 __ x_21873
     881    status_start_fun_call __ __ __ x_2092 __ x_2090
    882882    (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_21873)
    884 | Tac_step_default (status_pre, status_end, status_init, x_21880) ->
    885   h_tac_step_default status_pre status_end status_init __ x_21880 __ __
     883      h_tac_step_default status_after_fun_call status_final x_2090)
     884| Tac_step_default (status_pre, status_end, status_init, x_2097) ->
     885  h_tac_step_default status_pre status_end status_init __ x_2097 __ __
    886886    (trace_any_call_rect_Type1 s h_tac_base h_tac_step_call
    887       h_tac_step_default status_init status_end x_21880)
     887      h_tac_step_default status_init status_end x_2097)
    888888
    889889(** val trace_any_call_rect_Type0 :
     
    892892    -> __ -> __ -> __ -> trace_any_call -> __ -> __ -> 'a1 -> 'a1) -> __ ->
    893893    __ -> 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_21886 x_21885 = function
     894let rec trace_any_call_rect_Type0 s h_tac_base h_tac_step_call h_tac_step_default x_2103 x_2102 = function
    895895| Tac_base status -> h_tac_base status __
    896896| Tac_step_call
    897897    (status_pre_fun_call, status_after_fun_call, status_final,
    898      status_start_fun_call, x_21891, x_21889) ->
     898     status_start_fun_call, x_2108, x_2106) ->
    899899  h_tac_step_call status_pre_fun_call status_after_fun_call status_final
    900     status_start_fun_call __ __ __ x_21891 __ x_21889
     900    status_start_fun_call __ __ __ x_2108 __ x_2106
    901901    (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_21889)
    903 | Tac_step_default (status_pre, status_end, status_init, x_21896) ->
    904   h_tac_step_default status_pre status_end status_init __ x_21896 __ __
     902      h_tac_step_default status_after_fun_call status_final x_2106)
     903| Tac_step_default (status_pre, status_end, status_init, x_2113) ->
     904  h_tac_step_default status_pre status_end status_init __ x_2113 __ __
    905905    (trace_any_call_rect_Type0 s h_tac_base h_tac_step_call
    906       h_tac_step_default status_init status_end x_21896)
     906      h_tac_step_default status_init status_end x_2113)
    907907
    908908(** val trace_any_call_inv_rect_Type4 :
     
    973973    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    974974    -> trace_label_call -> 'a1 **)
    975 let rec trace_label_call_rect_Type4 s h_tlc_base x_22004 x_22003 = function
    976 | Tlc_base (start_status, end_status, x_22007) ->
    977   h_tlc_base start_status end_status x_22007 __
     975let rec trace_label_call_rect_Type4 s h_tlc_base x_2221 x_2220 = function
     976| Tlc_base (start_status, end_status, x_2224) ->
     977  h_tlc_base start_status end_status x_2224 __
    978978
    979979(** val trace_label_call_rect_Type5 :
    980980    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    981981    -> trace_label_call -> 'a1 **)
    982 let rec trace_label_call_rect_Type5 s h_tlc_base x_22010 x_22009 = function
    983 | Tlc_base (start_status, end_status, x_22013) ->
    984   h_tlc_base start_status end_status x_22013 __
     982let rec trace_label_call_rect_Type5 s h_tlc_base x_2227 x_2226 = function
     983| Tlc_base (start_status, end_status, x_2230) ->
     984  h_tlc_base start_status end_status x_2230 __
    985985
    986986(** val trace_label_call_rect_Type3 :
    987987    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    988988    -> trace_label_call -> 'a1 **)
    989 let rec trace_label_call_rect_Type3 s h_tlc_base x_22016 x_22015 = function
    990 | Tlc_base (start_status, end_status, x_22019) ->
    991   h_tlc_base start_status end_status x_22019 __
     989let rec trace_label_call_rect_Type3 s h_tlc_base x_2233 x_2232 = function
     990| Tlc_base (start_status, end_status, x_2236) ->
     991  h_tlc_base start_status end_status x_2236 __
    992992
    993993(** val trace_label_call_rect_Type2 :
    994994    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    995995    -> trace_label_call -> 'a1 **)
    996 let rec trace_label_call_rect_Type2 s h_tlc_base x_22022 x_22021 = function
    997 | Tlc_base (start_status, end_status, x_22025) ->
    998   h_tlc_base start_status end_status x_22025 __
     996let rec trace_label_call_rect_Type2 s h_tlc_base x_2239 x_2238 = function
     997| Tlc_base (start_status, end_status, x_2242) ->
     998  h_tlc_base start_status end_status x_2242 __
    999999
    10001000(** val trace_label_call_rect_Type1 :
    10011001    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    10021002    -> trace_label_call -> 'a1 **)
    1003 let rec trace_label_call_rect_Type1 s h_tlc_base x_22028 x_22027 = function
    1004 | Tlc_base (start_status, end_status, x_22031) ->
    1005   h_tlc_base start_status end_status x_22031 __
     1003let rec trace_label_call_rect_Type1 s h_tlc_base x_2245 x_2244 = function
     1004| Tlc_base (start_status, end_status, x_2248) ->
     1005  h_tlc_base start_status end_status x_2248 __
    10061006
    10071007(** val trace_label_call_rect_Type0 :
    10081008    abstract_status -> (__ -> __ -> trace_any_call -> __ -> 'a1) -> __ -> __
    10091009    -> trace_label_call -> 'a1 **)
    1010 let rec trace_label_call_rect_Type0 s h_tlc_base x_22034 x_22033 = function
    1011 | Tlc_base (start_status, end_status, x_22037) ->
    1012   h_tlc_base start_status end_status x_22037 __
     1010let rec trace_label_call_rect_Type0 s h_tlc_base x_2251 x_2250 = function
     1011| Tlc_base (start_status, end_status, x_2254) ->
     1012  h_tlc_base start_status end_status x_2254 __
    10131013
    10141014(** val trace_label_call_inv_rect_Type4 :
     
    11641164    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    11651165    -> trace_whole_program -> 'a1 **)
    1166 let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_22086 = function
    1167 | Twp_terminating
    1168     (status_initial, status_start_fun, status_final, x_22089) ->
    1169   h_twp_terminating status_initial status_start_fun status_final __ __
    1170     x_22089 __
    1171 | Twp_diverges (status_initial, status_start_fun, x_22092) ->
    1172   h_twp_diverges status_initial status_start_fun __ __ x_22092
     1166let rec trace_whole_program_rect_Type4 s h_twp_terminating h_twp_diverges x_2303 = function
     1167| Twp_terminating (status_initial, status_start_fun, status_final, x_2306) ->
     1168  h_twp_terminating status_initial status_start_fun status_final __ __ x_2306
     1169    __
     1170| Twp_diverges (status_initial, status_start_fun, x_2309) ->
     1171  h_twp_diverges status_initial status_start_fun __ __ x_2309
    11731172
    11741173(** val trace_whole_program_rect_Type5 :
     
    11761175    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    11771176    -> trace_whole_program -> 'a1 **)
    1178 let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_22097 = function
    1179 | Twp_terminating
    1180     (status_initial, status_start_fun, status_final, x_22100) ->
    1181   h_twp_terminating status_initial status_start_fun status_final __ __
    1182     x_22100 __
    1183 | Twp_diverges (status_initial, status_start_fun, x_22103) ->
    1184   h_twp_diverges status_initial status_start_fun __ __ x_22103
     1177let rec trace_whole_program_rect_Type5 s h_twp_terminating h_twp_diverges x_2314 = function
     1178| Twp_terminating (status_initial, status_start_fun, status_final, x_2317) ->
     1179  h_twp_terminating status_initial status_start_fun status_final __ __ x_2317
     1180    __
     1181| Twp_diverges (status_initial, status_start_fun, x_2320) ->
     1182  h_twp_diverges status_initial status_start_fun __ __ x_2320
    11851183
    11861184(** val trace_whole_program_rect_Type3 :
     
    11881186    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    11891187    -> trace_whole_program -> 'a1 **)
    1190 let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_22108 = function
    1191 | Twp_terminating
    1192     (status_initial, status_start_fun, status_final, x_22111) ->
    1193   h_twp_terminating status_initial status_start_fun status_final __ __
    1194     x_22111 __
    1195 | Twp_diverges (status_initial, status_start_fun, x_22114) ->
    1196   h_twp_diverges status_initial status_start_fun __ __ x_22114
     1188let rec trace_whole_program_rect_Type3 s h_twp_terminating h_twp_diverges x_2325 = function
     1189| Twp_terminating (status_initial, status_start_fun, status_final, x_2328) ->
     1190  h_twp_terminating status_initial status_start_fun status_final __ __ x_2328
     1191    __
     1192| Twp_diverges (status_initial, status_start_fun, x_2331) ->
     1193  h_twp_diverges status_initial status_start_fun __ __ x_2331
    11971194
    11981195(** val trace_whole_program_rect_Type2 :
     
    12001197    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    12011198    -> trace_whole_program -> 'a1 **)
    1202 let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_22119 = function
    1203 | Twp_terminating
    1204     (status_initial, status_start_fun, status_final, x_22122) ->
    1205   h_twp_terminating status_initial status_start_fun status_final __ __
    1206     x_22122 __
    1207 | Twp_diverges (status_initial, status_start_fun, x_22125) ->
    1208   h_twp_diverges status_initial status_start_fun __ __ x_22125
     1199let rec trace_whole_program_rect_Type2 s h_twp_terminating h_twp_diverges x_2336 = function
     1200| Twp_terminating (status_initial, status_start_fun, status_final, x_2339) ->
     1201  h_twp_terminating status_initial status_start_fun status_final __ __ x_2339
     1202    __
     1203| Twp_diverges (status_initial, status_start_fun, x_2342) ->
     1204  h_twp_diverges status_initial status_start_fun __ __ x_2342
    12091205
    12101206(** val trace_whole_program_rect_Type1 :
     
    12121208    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    12131209    -> trace_whole_program -> 'a1 **)
    1214 let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_22130 = function
    1215 | Twp_terminating
    1216     (status_initial, status_start_fun, status_final, x_22133) ->
    1217   h_twp_terminating status_initial status_start_fun status_final __ __
    1218     x_22133 __
    1219 | Twp_diverges (status_initial, status_start_fun, x_22136) ->
    1220   h_twp_diverges status_initial status_start_fun __ __ x_22136
     1210let rec trace_whole_program_rect_Type1 s h_twp_terminating h_twp_diverges x_2347 = function
     1211| Twp_terminating (status_initial, status_start_fun, status_final, x_2350) ->
     1212  h_twp_terminating status_initial status_start_fun status_final __ __ x_2350
     1213    __
     1214| Twp_diverges (status_initial, status_start_fun, x_2353) ->
     1215  h_twp_diverges status_initial status_start_fun __ __ x_2353
    12211216
    12221217(** val trace_whole_program_rect_Type0 :
     
    12241219    __ -> 'a1) -> (__ -> __ -> __ -> __ -> trace_label_diverges -> 'a1) -> __
    12251220    -> trace_whole_program -> 'a1 **)
    1226 let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_22141 = function
    1227 | Twp_terminating
    1228     (status_initial, status_start_fun, status_final, x_22144) ->
    1229   h_twp_terminating status_initial status_start_fun status_final __ __
    1230     x_22144 __
    1231 | Twp_diverges (status_initial, status_start_fun, x_22147) ->
    1232   h_twp_diverges status_initial status_start_fun __ __ x_22147
     1221let rec trace_whole_program_rect_Type0 s h_twp_terminating h_twp_diverges x_2358 = function
     1222| Twp_terminating (status_initial, status_start_fun, status_final, x_2361) ->
     1223  h_twp_terminating status_initial status_start_fun status_final __ __ x_2361
     1224    __
     1225| Twp_diverges (status_initial, status_start_fun, x_2364) ->
     1226  h_twp_diverges status_initial status_start_fun __ __ x_2364
    12331227
    12341228(** val trace_whole_program_inv_rect_Type4 :
     
    12941288    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    12951289    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_22371 x_22370 = function
     1290let rec trace_any_any_rect_Type4 s h_taa_base h_taa_step x_2588 x_2587 = function
    12971291| Taa_base st -> h_taa_base st
    1298 | Taa_step (st1, st2, st3, x_22373) ->
    1299   h_taa_step st1 st2 st3 __ __ __ x_22373
    1300     (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_22373)
     1292| Taa_step (st1, st2, st3, x_2590) ->
     1293  h_taa_step st1 st2 st3 __ __ __ x_2590
     1294    (trace_any_any_rect_Type4 s h_taa_base h_taa_step st2 st3 x_2590)
    13011295
    13021296(** val trace_any_any_rect_Type3 :
    13031297    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13041298    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_22389 x_22388 = function
     1299let rec trace_any_any_rect_Type3 s h_taa_base h_taa_step x_2606 x_2605 = function
    13061300| Taa_base st -> h_taa_base st
    1307 | Taa_step (st1, st2, st3, x_22391) ->
    1308   h_taa_step st1 st2 st3 __ __ __ x_22391
    1309     (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_22391)
     1301| Taa_step (st1, st2, st3, x_2608) ->
     1302  h_taa_step st1 st2 st3 __ __ __ x_2608
     1303    (trace_any_any_rect_Type3 s h_taa_base h_taa_step st2 st3 x_2608)
    13101304
    13111305(** val trace_any_any_rect_Type2 :
    13121306    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13131307    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_22398 x_22397 = function
     1308let rec trace_any_any_rect_Type2 s h_taa_base h_taa_step x_2615 x_2614 = function
    13151309| Taa_base st -> h_taa_base st
    1316 | Taa_step (st1, st2, st3, x_22400) ->
    1317   h_taa_step st1 st2 st3 __ __ __ x_22400
    1318     (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_22400)
     1310| Taa_step (st1, st2, st3, x_2617) ->
     1311  h_taa_step st1 st2 st3 __ __ __ x_2617
     1312    (trace_any_any_rect_Type2 s h_taa_base h_taa_step st2 st3 x_2617)
    13191313
    13201314(** val trace_any_any_rect_Type1 :
    13211315    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13221316    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_22407 x_22406 = function
     1317let rec trace_any_any_rect_Type1 s h_taa_base h_taa_step x_2624 x_2623 = function
    13241318| Taa_base st -> h_taa_base st
    1325 | Taa_step (st1, st2, st3, x_22409) ->
    1326   h_taa_step st1 st2 st3 __ __ __ x_22409
    1327     (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_22409)
     1319| Taa_step (st1, st2, st3, x_2626) ->
     1320  h_taa_step st1 st2 st3 __ __ __ x_2626
     1321    (trace_any_any_rect_Type1 s h_taa_base h_taa_step st2 st3 x_2626)
    13281322
    13291323(** val trace_any_any_rect_Type0 :
    13301324    abstract_status -> (__ -> 'a1) -> (__ -> __ -> __ -> __ -> __ -> __ ->
    13311325    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_22416 x_22415 = function
     1326let rec trace_any_any_rect_Type0 s h_taa_base h_taa_step x_2633 x_2632 = function
    13331327| Taa_base st -> h_taa_base st
    1334 | Taa_step (st1, st2, st3, x_22418) ->
    1335   h_taa_step st1 st2 st3 __ __ __ x_22418
    1336     (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_22418)
     1328| Taa_step (st1, st2, st3, x_2635) ->
     1329  h_taa_step st1 st2 st3 __ __ __ x_2635
     1330    (trace_any_any_rect_Type0 s h_taa_base h_taa_step st2 st3 x_2635)
    13371331
    13381332(** val trace_any_any_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.