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/rTLabs_traces.ml

    r2773 r2775  
    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_12748 s x_12747 = function
    299 | Wr_step (s0, tr, s', depth, trace, x_12750) ->
    300   h_wr_step s0 tr s' depth __ trace __ x_12750
     298let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17579 s x_17578 = function
     299| Wr_step (s0, tr, s', depth, trace, x_17581) ->
     300  h_wr_step s0 tr s' depth __ trace __ x_17581
    301301    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    302       s' trace x_12750)
    303 | Wr_call (s0, tr, s', depth, trace, x_12752) ->
    304   h_wr_call s0 tr s' depth __ trace __ x_12752
     302      s' trace x_17581)
     303| Wr_call (s0, tr, s', depth, trace, x_17583) ->
     304  h_wr_call s0 tr s' depth __ trace __ x_17583
    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_12752)
    307 | Wr_ret (s0, tr, s', depth, trace, x_12754) ->
    308   h_wr_ret s0 tr s' depth __ trace __ x_12754
     306      depth) s' trace x_17583)
     307| Wr_ret (s0, tr, s', depth, trace, x_17585) ->
     308  h_wr_ret s0 tr s' depth __ trace __ x_17585
    309309    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    310       s' trace x_12754)
     310      s' trace x_17585)
    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_12776 s x_12775 = function
    326 | Wr_step (s0, tr, s', depth, trace, x_12778) ->
    327   h_wr_step s0 tr s' depth __ trace __ x_12778
     325let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17607 s x_17606 = function
     326| Wr_step (s0, tr, s', depth, trace, x_17609) ->
     327  h_wr_step s0 tr s' depth __ trace __ x_17609
    328328    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    329       s' trace x_12778)
    330 | Wr_call (s0, tr, s', depth, trace, x_12780) ->
    331   h_wr_call s0 tr s' depth __ trace __ x_12780
     329      s' trace x_17609)
     330| Wr_call (s0, tr, s', depth, trace, x_17611) ->
     331  h_wr_call s0 tr s' depth __ trace __ x_17611
    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_12780)
    334 | Wr_ret (s0, tr, s', depth, trace, x_12782) ->
    335   h_wr_ret s0 tr s' depth __ trace __ x_12782
     333      depth) s' trace x_17611)
     334| Wr_ret (s0, tr, s', depth, trace, x_17613) ->
     335  h_wr_ret s0 tr s' depth __ trace __ x_17613
    336336    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    337       s' trace x_12782)
     337      s' trace x_17613)
    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_12790 s x_12789 = function
    353 | Wr_step (s0, tr, s', depth, trace, x_12792) ->
    354   h_wr_step s0 tr s' depth __ trace __ x_12792
     352let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17621 s x_17620 = function
     353| Wr_step (s0, tr, s', depth, trace, x_17623) ->
     354  h_wr_step s0 tr s' depth __ trace __ x_17623
    355355    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    356       s' trace x_12792)
    357 | Wr_call (s0, tr, s', depth, trace, x_12794) ->
    358   h_wr_call s0 tr s' depth __ trace __ x_12794
     356      s' trace x_17623)
     357| Wr_call (s0, tr, s', depth, trace, x_17625) ->
     358  h_wr_call s0 tr s' depth __ trace __ x_17625
    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_12794)
    361 | Wr_ret (s0, tr, s', depth, trace, x_12796) ->
    362   h_wr_ret s0 tr s' depth __ trace __ x_12796
     360      depth) s' trace x_17625)
     361| Wr_ret (s0, tr, s', depth, trace, x_17627) ->
     362  h_wr_ret s0 tr s' depth __ trace __ x_17627
    363363    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    364       s' trace x_12796)
     364      s' trace x_17627)
    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_12804 s x_12803 = function
    380 | Wr_step (s0, tr, s', depth, trace, x_12806) ->
    381   h_wr_step s0 tr s' depth __ trace __ x_12806
     379let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17635 s x_17634 = function
     380| Wr_step (s0, tr, s', depth, trace, x_17637) ->
     381  h_wr_step s0 tr s' depth __ trace __ x_17637
    382382    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    383       s' trace x_12806)
    384 | Wr_call (s0, tr, s', depth, trace, x_12808) ->
    385   h_wr_call s0 tr s' depth __ trace __ x_12808
     383      s' trace x_17637)
     384| Wr_call (s0, tr, s', depth, trace, x_17639) ->
     385  h_wr_call s0 tr s' depth __ trace __ x_17639
    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_12808)
    388 | Wr_ret (s0, tr, s', depth, trace, x_12810) ->
    389   h_wr_ret s0 tr s' depth __ trace __ x_12810
     387      depth) s' trace x_17639)
     388| Wr_ret (s0, tr, s', depth, trace, x_17641) ->
     389  h_wr_ret s0 tr s' depth __ trace __ x_17641
    390390    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    391       s' trace x_12810)
     391      s' trace x_17641)
    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_12818 s x_12817 = function
    407 | Wr_step (s0, tr, s', depth, trace, x_12820) ->
    408   h_wr_step s0 tr s' depth __ trace __ x_12820
     406let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17649 s x_17648 = function
     407| Wr_step (s0, tr, s', depth, trace, x_17651) ->
     408  h_wr_step s0 tr s' depth __ trace __ x_17651
    409409    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    410       s' trace x_12820)
    411 | Wr_call (s0, tr, s', depth, trace, x_12822) ->
    412   h_wr_call s0 tr s' depth __ trace __ x_12822
     410      s' trace x_17651)
     411| Wr_call (s0, tr, s', depth, trace, x_17653) ->
     412  h_wr_call s0 tr s' depth __ trace __ x_17653
    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_12822)
    415 | Wr_ret (s0, tr, s', depth, trace, x_12824) ->
    416   h_wr_ret s0 tr s' depth __ trace __ x_12824
     414      depth) s' trace x_17653)
     415| Wr_ret (s0, tr, s', depth, trace, x_17655) ->
     416  h_wr_ret s0 tr s' depth __ trace __ x_17655
    417417    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    418       s' trace x_12824)
     418      s' trace x_17655)
    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_13359 =
     841let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_18190 =
    842842  let { new_state = new_state0; remainder = remainder0; new_trace =
    843     new_trace0; terminates = terminates0 } = x_13359
     843    new_trace0; terminates = terminates0 } = x_18190
    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_13361 =
     853let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_18192 =
    854854  let { new_state = new_state0; remainder = remainder0; new_trace =
    855     new_trace0; terminates = terminates0 } = x_13361
     855    new_trace0; terminates = terminates0 } = x_18192
    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_13363 =
     865let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_18194 =
    866866  let { new_state = new_state0; remainder = remainder0; new_trace =
    867     new_trace0; terminates = terminates0 } = x_13363
     867    new_trace0; terminates = terminates0 } = x_18194
    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_13365 =
     877let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_18196 =
    878878  let { new_state = new_state0; remainder = remainder0; new_trace =
    879     new_trace0; terminates = terminates0 } = x_13365
     879    new_trace0; terminates = terminates0 } = x_18196
    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_13367 =
     889let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_18198 =
    890890  let { new_state = new_state0; remainder = remainder0; new_trace =
    891     new_trace0; terminates = terminates0 } = x_13367
     891    new_trace0; terminates = terminates0 } = x_18198
    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_13369 =
     901let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_18200 =
    902902  let { new_state = new_state0; remainder = remainder0; new_trace =
    903     new_trace0; terminates = terminates0 } = x_13369
     903    new_trace0; terminates = terminates0 } = x_18200
    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_13387 =
    1002   let { ends = ends0; trace_res = trace_res0 } = x_13387 in
     1001let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_18218 =
     1002  let { ends = ends0; trace_res = trace_res0 } = x_18218 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_13389 =
    1011   let { ends = ends0; trace_res = trace_res0 } = x_13389 in
     1010let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_18220 =
     1011  let { ends = ends0; trace_res = trace_res0 } = x_18220 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_13391 =
    1020   let { ends = ends0; trace_res = trace_res0 } = x_13391 in
     1019let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_18222 =
     1020  let { ends = ends0; trace_res = trace_res0 } = x_18222 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_13393 =
    1029   let { ends = ends0; trace_res = trace_res0 } = x_13393 in
     1028let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_18224 =
     1029  let { ends = ends0; trace_res = trace_res0 } = x_18224 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_13395 =
    1038   let { ends = ends0; trace_res = trace_res0 } = x_13395 in
     1037let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_18226 =
     1038  let { ends = ends0; trace_res = trace_res0 } = x_18226 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_13397 =
    1047   let { ends = ends0; trace_res = trace_res0 } = x_13397 in
     1046let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_18228 =
     1047  let { ends = ends0; trace_res = trace_res0 } = x_18228 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_13732 x_13731 = function
     1560let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_18563 x_18562 = function
    15611561| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1562 | Pft_step (s, tr, s', s'', x_13735) ->
    1563   h_pft_step s tr s' s'' __ x_13735
    1564     (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_13735)
     1562| Pft_step (s, tr, s', s'', x_18566) ->
     1563  h_pft_step s tr s' s'' __ x_18566
     1564    (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_18566)
    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_13748 x_13747 = function
     1572let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_18579 x_18578 = function
    15731573| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1574 | Pft_step (s, tr, s', s'', x_13751) ->
    1575   h_pft_step s tr s' s'' __ x_13751
    1576     (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_13751)
     1574| Pft_step (s, tr, s', s'', x_18582) ->
     1575  h_pft_step s tr s' s'' __ x_18582
     1576    (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_18582)
    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_13756 x_13755 = function
     1584let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_18587 x_18586 = function
    15851585| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1586 | Pft_step (s, tr, s', s'', x_13759) ->
    1587   h_pft_step s tr s' s'' __ x_13759
    1588     (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_13759)
     1586| Pft_step (s, tr, s', s'', x_18590) ->
     1587  h_pft_step s tr s' s'' __ x_18590
     1588    (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_18590)
    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_13764 x_13763 = function
     1596let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_18595 x_18594 = function
    15971597| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1598 | Pft_step (s, tr, s', s'', x_13767) ->
    1599   h_pft_step s tr s' s'' __ x_13767
    1600     (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_13767)
     1598| Pft_step (s, tr, s', s'', x_18598) ->
     1599  h_pft_step s tr s' s'' __ x_18598
     1600    (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_18598)
    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_13772 x_13771 = function
     1608let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_18603 x_18602 = function
    16091609| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1610 | Pft_step (s, tr, s', s'', x_13775) ->
    1611   h_pft_step s tr s' s'' __ x_13775
    1612     (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_13775)
     1610| Pft_step (s, tr, s', s'', x_18606) ->
     1611  h_pft_step s tr s' s'' __ x_18606
     1612    (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_18606)
    16131613
    16141614(** val partial_flat_trace_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.