Ignore:
Timestamp:
Mar 12, 2013, 5:53:56 PM (7 years ago)
Author:
sacerdot
Message:

Pretty printing of the LTL program.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLabs_traces.ml

    r2827 r2854  
    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_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
     298let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2230 s x_2229 = function
     299| Wr_step (s0, tr, s', depth, trace, x_2232) ->
     300  h_wr_step s0 tr s' depth __ trace __ x_2232
    301301    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    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
     302      s' trace x_2232)
     303| Wr_call (s0, tr, s', depth, trace, x_2234) ->
     304  h_wr_call s0 tr s' depth __ trace __ x_2234
    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_17713)
    307 | Wr_ret (s0, tr, s', depth, trace, x_17715) ->
    308   h_wr_ret s0 tr s' depth __ trace __ x_17715
     306      depth) s' trace x_2234)
     307| Wr_ret (s0, tr, s', depth, trace, x_2236) ->
     308  h_wr_ret s0 tr s' depth __ trace __ x_2236
    309309    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    310       s' trace x_17715)
     310      s' trace x_2236)
    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_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
     325let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2258 s x_2257 = function
     326| Wr_step (s0, tr, s', depth, trace, x_2260) ->
     327  h_wr_step s0 tr s' depth __ trace __ x_2260
    328328    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    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
     329      s' trace x_2260)
     330| Wr_call (s0, tr, s', depth, trace, x_2262) ->
     331  h_wr_call s0 tr s' depth __ trace __ x_2262
    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_17741)
    334 | Wr_ret (s0, tr, s', depth, trace, x_17743) ->
    335   h_wr_ret s0 tr s' depth __ trace __ x_17743
     333      depth) s' trace x_2262)
     334| Wr_ret (s0, tr, s', depth, trace, x_2264) ->
     335  h_wr_ret s0 tr s' depth __ trace __ x_2264
    336336    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    337       s' trace x_17743)
     337      s' trace x_2264)
    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_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
     352let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2272 s x_2271 = function
     353| Wr_step (s0, tr, s', depth, trace, x_2274) ->
     354  h_wr_step s0 tr s' depth __ trace __ x_2274
    355355    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    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
     356      s' trace x_2274)
     357| Wr_call (s0, tr, s', depth, trace, x_2276) ->
     358  h_wr_call s0 tr s' depth __ trace __ x_2276
    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_17755)
    361 | Wr_ret (s0, tr, s', depth, trace, x_17757) ->
    362   h_wr_ret s0 tr s' depth __ trace __ x_17757
     360      depth) s' trace x_2276)
     361| Wr_ret (s0, tr, s', depth, trace, x_2278) ->
     362  h_wr_ret s0 tr s' depth __ trace __ x_2278
    363363    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    364       s' trace x_17757)
     364      s' trace x_2278)
    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_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
     379let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2286 s x_2285 = function
     380| Wr_step (s0, tr, s', depth, trace, x_2288) ->
     381  h_wr_step s0 tr s' depth __ trace __ x_2288
    382382    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    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
     383      s' trace x_2288)
     384| Wr_call (s0, tr, s', depth, trace, x_2290) ->
     385  h_wr_call s0 tr s' depth __ trace __ x_2290
    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_17769)
    388 | Wr_ret (s0, tr, s', depth, trace, x_17771) ->
    389   h_wr_ret s0 tr s' depth __ trace __ x_17771
     387      depth) s' trace x_2290)
     388| Wr_ret (s0, tr, s', depth, trace, x_2292) ->
     389  h_wr_ret s0 tr s' depth __ trace __ x_2292
    390390    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    391       s' trace x_17771)
     391      s' trace x_2292)
    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_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
     406let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2300 s x_2299 = function
     407| Wr_step (s0, tr, s', depth, trace, x_2302) ->
     408  h_wr_step s0 tr s' depth __ trace __ x_2302
    409409    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    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
     410      s' trace x_2302)
     411| Wr_call (s0, tr, s', depth, trace, x_2304) ->
     412  h_wr_call s0 tr s' depth __ trace __ x_2304
    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_17783)
    415 | Wr_ret (s0, tr, s', depth, trace, x_17785) ->
    416   h_wr_ret s0 tr s' depth __ trace __ x_17785
     414      depth) s' trace x_2304)
     415| Wr_ret (s0, tr, s', depth, trace, x_2306) ->
     416  h_wr_ret s0 tr s' depth __ trace __ x_2306
    417417    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    418       s' trace x_17785)
     418      s' trace x_2306)
    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_18320 =
     841let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_2841 =
    842842  let { new_state = new_state0; remainder = remainder0; new_trace =
    843     new_trace0; terminates = terminates0 } = x_18320
     843    new_trace0; terminates = terminates0 } = x_2841
    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_18322 =
     853let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_2843 =
    854854  let { new_state = new_state0; remainder = remainder0; new_trace =
    855     new_trace0; terminates = terminates0 } = x_18322
     855    new_trace0; terminates = terminates0 } = x_2843
    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_18324 =
     865let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_2845 =
    866866  let { new_state = new_state0; remainder = remainder0; new_trace =
    867     new_trace0; terminates = terminates0 } = x_18324
     867    new_trace0; terminates = terminates0 } = x_2845
    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_18326 =
     877let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_2847 =
    878878  let { new_state = new_state0; remainder = remainder0; new_trace =
    879     new_trace0; terminates = terminates0 } = x_18326
     879    new_trace0; terminates = terminates0 } = x_2847
    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_18328 =
     889let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_2849 =
    890890  let { new_state = new_state0; remainder = remainder0; new_trace =
    891     new_trace0; terminates = terminates0 } = x_18328
     891    new_trace0; terminates = terminates0 } = x_2849
    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_18330 =
     901let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_2851 =
    902902  let { new_state = new_state0; remainder = remainder0; new_trace =
    903     new_trace0; terminates = terminates0 } = x_18330
     903    new_trace0; terminates = terminates0 } = x_2851
    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_18348 =
    1002   let { ends = ends0; trace_res = trace_res0 } = x_18348 in
     1001let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_2869 =
     1002  let { ends = ends0; trace_res = trace_res0 } = x_2869 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_18350 =
    1011   let { ends = ends0; trace_res = trace_res0 } = x_18350 in
     1010let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_2871 =
     1011  let { ends = ends0; trace_res = trace_res0 } = x_2871 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_18352 =
    1020   let { ends = ends0; trace_res = trace_res0 } = x_18352 in
     1019let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_2873 =
     1020  let { ends = ends0; trace_res = trace_res0 } = x_2873 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_18354 =
    1029   let { ends = ends0; trace_res = trace_res0 } = x_18354 in
     1028let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_2875 =
     1029  let { ends = ends0; trace_res = trace_res0 } = x_2875 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_18356 =
    1038   let { ends = ends0; trace_res = trace_res0 } = x_18356 in
     1037let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_2877 =
     1038  let { ends = ends0; trace_res = trace_res0 } = x_2877 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_18358 =
    1047   let { ends = ends0; trace_res = trace_res0 } = x_18358 in
     1046let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_2879 =
     1047  let { ends = ends0; trace_res = trace_res0 } = x_2879 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_18693 x_18692 = function
     1560let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_3214 x_3213 = function
    15611561| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    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)
     1562| Pft_step (s, tr, s', s'', x_3217) ->
     1563  h_pft_step s tr s' s'' __ x_3217
     1564    (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_3217)
    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_18709 x_18708 = function
     1572let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_3230 x_3229 = function
    15731573| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    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)
     1574| Pft_step (s, tr, s', s'', x_3233) ->
     1575  h_pft_step s tr s' s'' __ x_3233
     1576    (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_3233)
    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_18717 x_18716 = function
     1584let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_3238 x_3237 = function
    15851585| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    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)
     1586| Pft_step (s, tr, s', s'', x_3241) ->
     1587  h_pft_step s tr s' s'' __ x_3241
     1588    (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_3241)
    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_18725 x_18724 = function
     1596let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_3246 x_3245 = function
    15971597| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    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)
     1598| Pft_step (s, tr, s', s'', x_3249) ->
     1599  h_pft_step s tr s' s'' __ x_3249
     1600    (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_3249)
    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_18733 x_18732 = function
     1608let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_3254 x_3253 = function
    16091609| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    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)
     1610| Pft_step (s, tr, s', s'', x_3257) ->
     1611  h_pft_step s tr s' s'' __ x_3257
     1612    (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_3257)
    16131613
    16141614(** val partial_flat_trace_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.