Ignore:
Timestamp:
Mar 8, 2013, 9:07:28 PM (7 years ago)
Author:
sacerdot
Message:

Everything extracted again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLabs_traces.ml

    r2797 r2827  
    296296    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    297297    flat_trace -> will_return -> 'a1 **)
    298 let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17592 s x_17591 = function
    299 | Wr_step (s0, tr, s', depth, trace, x_17594) ->
    300   h_wr_step s0 tr s' depth __ trace __ x_17594
     298let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17709 s x_17708 = function
     299| Wr_step (s0, tr, s', depth, trace, x_17711) ->
     300  h_wr_step s0 tr s' depth __ trace __ x_17711
    301301    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    302       s' trace x_17594)
    303 | Wr_call (s0, tr, s', depth, trace, x_17596) ->
    304   h_wr_call s0 tr s' depth __ trace __ x_17596
     302      s' trace x_17711)
     303| Wr_call (s0, tr, s', depth, trace, x_17713) ->
     304  h_wr_call s0 tr s' depth __ trace __ x_17713
    305305    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    306       depth) s' trace x_17596)
    307 | Wr_ret (s0, tr, s', depth, trace, x_17598) ->
    308   h_wr_ret s0 tr s' depth __ trace __ x_17598
     306      depth) s' trace x_17713)
     307| Wr_ret (s0, tr, s', depth, trace, x_17715) ->
     308  h_wr_ret s0 tr s' depth __ trace __ x_17715
    309309    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    310       s' trace x_17598)
     310      s' trace x_17715)
    311311| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    312312
     
    323323    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    324324    flat_trace -> will_return -> 'a1 **)
    325 let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17620 s x_17619 = function
    326 | Wr_step (s0, tr, s', depth, trace, x_17622) ->
    327   h_wr_step s0 tr s' depth __ trace __ x_17622
     325let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17737 s x_17736 = function
     326| Wr_step (s0, tr, s', depth, trace, x_17739) ->
     327  h_wr_step s0 tr s' depth __ trace __ x_17739
    328328    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    329       s' trace x_17622)
    330 | Wr_call (s0, tr, s', depth, trace, x_17624) ->
    331   h_wr_call s0 tr s' depth __ trace __ x_17624
     329      s' trace x_17739)
     330| Wr_call (s0, tr, s', depth, trace, x_17741) ->
     331  h_wr_call s0 tr s' depth __ trace __ x_17741
    332332    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    333       depth) s' trace x_17624)
    334 | Wr_ret (s0, tr, s', depth, trace, x_17626) ->
    335   h_wr_ret s0 tr s' depth __ trace __ x_17626
     333      depth) s' trace x_17741)
     334| Wr_ret (s0, tr, s', depth, trace, x_17743) ->
     335  h_wr_ret s0 tr s' depth __ trace __ x_17743
    336336    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    337       s' trace x_17626)
     337      s' trace x_17743)
    338338| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    339339
     
    350350    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    351351    flat_trace -> will_return -> 'a1 **)
    352 let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17634 s x_17633 = function
    353 | Wr_step (s0, tr, s', depth, trace, x_17636) ->
    354   h_wr_step s0 tr s' depth __ trace __ x_17636
     352let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17751 s x_17750 = function
     353| Wr_step (s0, tr, s', depth, trace, x_17753) ->
     354  h_wr_step s0 tr s' depth __ trace __ x_17753
    355355    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    356       s' trace x_17636)
    357 | Wr_call (s0, tr, s', depth, trace, x_17638) ->
    358   h_wr_call s0 tr s' depth __ trace __ x_17638
     356      s' trace x_17753)
     357| Wr_call (s0, tr, s', depth, trace, x_17755) ->
     358  h_wr_call s0 tr s' depth __ trace __ x_17755
    359359    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    360       depth) s' trace x_17638)
    361 | Wr_ret (s0, tr, s', depth, trace, x_17640) ->
    362   h_wr_ret s0 tr s' depth __ trace __ x_17640
     360      depth) s' trace x_17755)
     361| Wr_ret (s0, tr, s', depth, trace, x_17757) ->
     362  h_wr_ret s0 tr s' depth __ trace __ x_17757
    363363    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    364       s' trace x_17640)
     364      s' trace x_17757)
    365365| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    366366
     
    377377    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    378378    flat_trace -> will_return -> 'a1 **)
    379 let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17648 s x_17647 = function
    380 | Wr_step (s0, tr, s', depth, trace, x_17650) ->
    381   h_wr_step s0 tr s' depth __ trace __ x_17650
     379let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17765 s x_17764 = function
     380| Wr_step (s0, tr, s', depth, trace, x_17767) ->
     381  h_wr_step s0 tr s' depth __ trace __ x_17767
    382382    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    383       s' trace x_17650)
    384 | Wr_call (s0, tr, s', depth, trace, x_17652) ->
    385   h_wr_call s0 tr s' depth __ trace __ x_17652
     383      s' trace x_17767)
     384| Wr_call (s0, tr, s', depth, trace, x_17769) ->
     385  h_wr_call s0 tr s' depth __ trace __ x_17769
    386386    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    387       depth) s' trace x_17652)
    388 | Wr_ret (s0, tr, s', depth, trace, x_17654) ->
    389   h_wr_ret s0 tr s' depth __ trace __ x_17654
     387      depth) s' trace x_17769)
     388| Wr_ret (s0, tr, s', depth, trace, x_17771) ->
     389  h_wr_ret s0 tr s' depth __ trace __ x_17771
    390390    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    391       s' trace x_17654)
     391      s' trace x_17771)
    392392| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    393393
     
    404404    'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    405405    flat_trace -> will_return -> 'a1 **)
    406 let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17662 s x_17661 = function
    407 | Wr_step (s0, tr, s', depth, trace, x_17664) ->
    408   h_wr_step s0 tr s' depth __ trace __ x_17664
     406let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17779 s x_17778 = function
     407| Wr_step (s0, tr, s', depth, trace, x_17781) ->
     408  h_wr_step s0 tr s' depth __ trace __ x_17781
    409409    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    410       s' trace x_17664)
    411 | Wr_call (s0, tr, s', depth, trace, x_17666) ->
    412   h_wr_call s0 tr s' depth __ trace __ x_17666
     410      s' trace x_17781)
     411| Wr_call (s0, tr, s', depth, trace, x_17783) ->
     412  h_wr_call s0 tr s' depth __ trace __ x_17783
    413413    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    414       depth) s' trace x_17666)
    415 | Wr_ret (s0, tr, s', depth, trace, x_17668) ->
    416   h_wr_ret s0 tr s' depth __ trace __ x_17668
     414      depth) s' trace x_17783)
     415| Wr_ret (s0, tr, s', depth, trace, x_17785) ->
     416  h_wr_ret s0 tr s' depth __ trace __ x_17785
    417417    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    418       s' trace x_17668)
     418      s' trace x_17785)
    419419| Wr_base (s0, tr, s', trace) -> h_wr_base s0 tr s' __ trace __
    420420
     
    839839    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    840840    trace_result -> 'a2 **)
    841 let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_18203 =
     841let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_18320 =
    842842  let { new_state = new_state0; remainder = remainder0; new_trace =
    843     new_trace0; terminates = terminates0 } = x_18203
     843    new_trace0; terminates = terminates0 } = x_18320
    844844  in
    845845  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    851851    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    852852    trace_result -> 'a2 **)
    853 let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_18205 =
     853let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_18322 =
    854854  let { new_state = new_state0; remainder = remainder0; new_trace =
    855     new_trace0; terminates = terminates0 } = x_18205
     855    new_trace0; terminates = terminates0 } = x_18322
    856856  in
    857857  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    863863    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    864864    trace_result -> 'a2 **)
    865 let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_18207 =
     865let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_18324 =
    866866  let { new_state = new_state0; remainder = remainder0; new_trace =
    867     new_trace0; terminates = terminates0 } = x_18207
     867    new_trace0; terminates = terminates0 } = x_18324
    868868  in
    869869  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    875875    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    876876    trace_result -> 'a2 **)
    877 let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_18209 =
     877let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_18326 =
    878878  let { new_state = new_state0; remainder = remainder0; new_trace =
    879     new_trace0; terminates = terminates0 } = x_18209
     879    new_trace0; terminates = terminates0 } = x_18326
    880880  in
    881881  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    887887    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    888888    trace_result -> 'a2 **)
    889 let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_18211 =
     889let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_18328 =
    890890  let { new_state = new_state0; remainder = remainder0; new_trace =
    891     new_trace0; terminates = terminates0 } = x_18211
     891    new_trace0; terminates = terminates0 } = x_18328
    892892  in
    893893  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    899899    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    900900    trace_result -> 'a2 **)
    901 let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_18213 =
     901let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_18330 =
    902902  let { new_state = new_state0; remainder = remainder0; new_trace =
    903     new_trace0; terminates = terminates0 } = x_18213
     903    new_trace0; terminates = terminates0 } = x_18330
    904904  in
    905905  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    999999    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10001000    sub_trace_result -> 'a2 **)
    1001 let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_18231 =
    1002   let { ends = ends0; trace_res = trace_res0 } = x_18231 in
     1001let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_18348 =
     1002  let { ends = ends0; trace_res = trace_res0 } = x_18348 in
    10031003  h_mk_sub_trace_result ends0 trace_res0
    10041004
     
    10081008    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10091009    sub_trace_result -> 'a2 **)
    1010 let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_18233 =
    1011   let { ends = ends0; trace_res = trace_res0 } = x_18233 in
     1010let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_18350 =
     1011  let { ends = ends0; trace_res = trace_res0 } = x_18350 in
    10121012  h_mk_sub_trace_result ends0 trace_res0
    10131013
     
    10171017    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10181018    sub_trace_result -> 'a2 **)
    1019 let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_18235 =
    1020   let { ends = ends0; trace_res = trace_res0 } = x_18235 in
     1019let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_18352 =
     1020  let { ends = ends0; trace_res = trace_res0 } = x_18352 in
    10211021  h_mk_sub_trace_result ends0 trace_res0
    10221022
     
    10261026    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10271027    sub_trace_result -> 'a2 **)
    1028 let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_18237 =
    1029   let { ends = ends0; trace_res = trace_res0 } = x_18237 in
     1028let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_18354 =
     1029  let { ends = ends0; trace_res = trace_res0 } = x_18354 in
    10301030  h_mk_sub_trace_result ends0 trace_res0
    10311031
     
    10351035    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10361036    sub_trace_result -> 'a2 **)
    1037 let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_18239 =
    1038   let { ends = ends0; trace_res = trace_res0 } = x_18239 in
     1037let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_18356 =
     1038  let { ends = ends0; trace_res = trace_res0 } = x_18356 in
    10391039  h_mk_sub_trace_result ends0 trace_res0
    10401040
     
    10441044    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10451045    sub_trace_result -> 'a2 **)
    1046 let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_18241 =
    1047   let { ends = ends0; trace_res = trace_res0 } = x_18241 in
     1046let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_18358 =
     1047  let { ends = ends0; trace_res = trace_res0 } = x_18358 in
    10481048  h_mk_sub_trace_result ends0 trace_res0
    10491049
     
    15581558    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15591559    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1560 let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_18576 x_18575 = function
     1560let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_18693 x_18692 = function
    15611561| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1562 | Pft_step (s, tr, s', s'', x_18579) ->
    1563   h_pft_step s tr s' s'' __ x_18579
    1564     (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_18579)
     1562| Pft_step (s, tr, s', s'', x_18696) ->
     1563  h_pft_step s tr s' s'' __ x_18696
     1564    (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_18696)
    15651565
    15661566(** val partial_flat_trace_rect_Type3 :
     
    15701570    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15711571    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1572 let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_18592 x_18591 = function
     1572let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_18709 x_18708 = function
    15731573| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1574 | Pft_step (s, tr, s', s'', x_18595) ->
    1575   h_pft_step s tr s' s'' __ x_18595
    1576     (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_18595)
     1574| Pft_step (s, tr, s', s'', x_18712) ->
     1575  h_pft_step s tr s' s'' __ x_18712
     1576    (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_18712)
    15771577
    15781578(** val partial_flat_trace_rect_Type2 :
     
    15821582    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15831583    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1584 let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_18600 x_18599 = function
     1584let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_18717 x_18716 = function
    15851585| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1586 | Pft_step (s, tr, s', s'', x_18603) ->
    1587   h_pft_step s tr s' s'' __ x_18603
    1588     (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_18603)
     1586| Pft_step (s, tr, s', s'', x_18720) ->
     1587  h_pft_step s tr s' s'' __ x_18720
     1588    (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_18720)
    15891589
    15901590(** val partial_flat_trace_rect_Type1 :
     
    15941594    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    15951595    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1596 let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_18608 x_18607 = function
     1596let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_18725 x_18724 = function
    15971597| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1598 | Pft_step (s, tr, s', s'', x_18611) ->
    1599   h_pft_step s tr s' s'' __ x_18611
    1600     (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_18611)
     1598| Pft_step (s, tr, s', s'', x_18728) ->
     1599  h_pft_step s tr s' s'' __ x_18728
     1600    (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_18728)
    16011601
    16021602(** val partial_flat_trace_rect_Type0 :
     
    16061606    ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
    16071607    RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3 **)
    1608 let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_18616 x_18615 = function
     1608let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_18733 x_18732 = function
    16091609| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1610 | Pft_step (s, tr, s', s'', x_18619) ->
    1611   h_pft_step s tr s' s'' __ x_18619
    1612     (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_18619)
     1610| Pft_step (s, tr, s', s'', x_18736) ->
     1611  h_pft_step s tr s' s'' __ x_18736
     1612    (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_18736)
    16131613
    16141614(** val partial_flat_trace_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.