Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (7 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLabs_traces.ml

    r2730 r2743  
    135135open Executions
    136136
    137 open Listb
     137open Listb_extra
    138138
    139139type ('o, 'i) flat_trace = ('o, 'i) __flat_trace Lazy.t
     
    297297    RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
    298298    will_return -> 'a1 **)
    299 let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2558 s x_2557 = function
    300 | Wr_step (s0, tr, s', depth, trace0, x_2560) ->
    301   h_wr_step s0 tr s' depth __ trace0 __ x_2560
     299let rec will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17438 s x_17437 = function
     300| Wr_step (s0, tr, s', depth, trace0, x_17440) ->
     301  h_wr_step s0 tr s' depth __ trace0 __ x_17440
    302302    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    303       s' trace0 x_2560)
    304 | Wr_call (s0, tr, s', depth, trace0, x_2562) ->
    305   h_wr_call s0 tr s' depth __ trace0 __ x_2562
     303      s' trace0 x_17440)
     304| Wr_call (s0, tr, s', depth, trace0, x_17442) ->
     305  h_wr_call s0 tr s' depth __ trace0 __ x_17442
    306306    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    307       depth) s' trace0 x_2562)
    308 | Wr_ret (s0, tr, s', depth, trace0, x_2564) ->
    309   h_wr_ret s0 tr s' depth __ trace0 __ x_2564
     307      depth) s' trace0 x_17442)
     308| Wr_ret (s0, tr, s', depth, trace0, x_17444) ->
     309  h_wr_ret s0 tr s' depth __ trace0 __ x_17444
    310310    (will_return_rect_Type4 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    311       s' trace0 x_2564)
     311      s' trace0 x_17444)
    312312| Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
    313313
     
    325325    RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
    326326    will_return -> 'a1 **)
    327 let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2586 s x_2585 = function
    328 | Wr_step (s0, tr, s', depth, trace0, x_2588) ->
    329   h_wr_step s0 tr s' depth __ trace0 __ x_2588
     327let rec will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17466 s x_17465 = function
     328| Wr_step (s0, tr, s', depth, trace0, x_17468) ->
     329  h_wr_step s0 tr s' depth __ trace0 __ x_17468
    330330    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    331       s' trace0 x_2588)
    332 | Wr_call (s0, tr, s', depth, trace0, x_2590) ->
    333   h_wr_call s0 tr s' depth __ trace0 __ x_2590
     331      s' trace0 x_17468)
     332| Wr_call (s0, tr, s', depth, trace0, x_17470) ->
     333  h_wr_call s0 tr s' depth __ trace0 __ x_17470
    334334    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    335       depth) s' trace0 x_2590)
    336 | Wr_ret (s0, tr, s', depth, trace0, x_2592) ->
    337   h_wr_ret s0 tr s' depth __ trace0 __ x_2592
     335      depth) s' trace0 x_17470)
     336| Wr_ret (s0, tr, s', depth, trace0, x_17472) ->
     337  h_wr_ret s0 tr s' depth __ trace0 __ x_17472
    338338    (will_return_rect_Type3 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    339       s' trace0 x_2592)
     339      s' trace0 x_17472)
    340340| Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
    341341
     
    353353    RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
    354354    will_return -> 'a1 **)
    355 let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2600 s x_2599 = function
    356 | Wr_step (s0, tr, s', depth, trace0, x_2602) ->
    357   h_wr_step s0 tr s' depth __ trace0 __ x_2602
     355let rec will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17480 s x_17479 = function
     356| Wr_step (s0, tr, s', depth, trace0, x_17482) ->
     357  h_wr_step s0 tr s' depth __ trace0 __ x_17482
    358358    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    359       s' trace0 x_2602)
    360 | Wr_call (s0, tr, s', depth, trace0, x_2604) ->
    361   h_wr_call s0 tr s' depth __ trace0 __ x_2604
     359      s' trace0 x_17482)
     360| Wr_call (s0, tr, s', depth, trace0, x_17484) ->
     361  h_wr_call s0 tr s' depth __ trace0 __ x_17484
    362362    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    363       depth) s' trace0 x_2604)
    364 | Wr_ret (s0, tr, s', depth, trace0, x_2606) ->
    365   h_wr_ret s0 tr s' depth __ trace0 __ x_2606
     363      depth) s' trace0 x_17484)
     364| Wr_ret (s0, tr, s', depth, trace0, x_17486) ->
     365  h_wr_ret s0 tr s' depth __ trace0 __ x_17486
    366366    (will_return_rect_Type2 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    367       s' trace0 x_2606)
     367      s' trace0 x_17486)
    368368| Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
    369369
     
    381381    RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
    382382    will_return -> 'a1 **)
    383 let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2614 s x_2613 = function
    384 | Wr_step (s0, tr, s', depth, trace0, x_2616) ->
    385   h_wr_step s0 tr s' depth __ trace0 __ x_2616
     383let rec will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17494 s x_17493 = function
     384| Wr_step (s0, tr, s', depth, trace0, x_17496) ->
     385  h_wr_step s0 tr s' depth __ trace0 __ x_17496
    386386    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    387       s' trace0 x_2616)
    388 | Wr_call (s0, tr, s', depth, trace0, x_2618) ->
    389   h_wr_call s0 tr s' depth __ trace0 __ x_2618
     387      s' trace0 x_17496)
     388| Wr_call (s0, tr, s', depth, trace0, x_17498) ->
     389  h_wr_call s0 tr s' depth __ trace0 __ x_17498
    390390    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    391       depth) s' trace0 x_2618)
    392 | Wr_ret (s0, tr, s', depth, trace0, x_2620) ->
    393   h_wr_ret s0 tr s' depth __ trace0 __ x_2620
     391      depth) s' trace0 x_17498)
     392| Wr_ret (s0, tr, s', depth, trace0, x_17500) ->
     393  h_wr_ret s0 tr s' depth __ trace0 __ x_17500
    394394    (will_return_rect_Type1 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    395       s' trace0 x_2620)
     395      s' trace0 x_17500)
    396396| Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
    397397
     
    409409    RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
    410410    will_return -> 'a1 **)
    411 let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_2628 s x_2627 = function
    412 | Wr_step (s0, tr, s', depth, trace0, x_2630) ->
    413   h_wr_step s0 tr s' depth __ trace0 __ x_2630
     411let rec will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base x_17508 s x_17507 = function
     412| Wr_step (s0, tr, s', depth, trace0, x_17510) ->
     413  h_wr_step s0 tr s' depth __ trace0 __ x_17510
    414414    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    415       s' trace0 x_2630)
    416 | Wr_call (s0, tr, s', depth, trace0, x_2632) ->
    417   h_wr_call s0 tr s' depth __ trace0 __ x_2632
     415      s' trace0 x_17510)
     416| Wr_call (s0, tr, s', depth, trace0, x_17512) ->
     417  h_wr_call s0 tr s' depth __ trace0 __ x_17512
    418418    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base (Nat.S
    419       depth) s' trace0 x_2632)
    420 | Wr_ret (s0, tr, s', depth, trace0, x_2634) ->
    421   h_wr_ret s0 tr s' depth __ trace0 __ x_2634
     419      depth) s' trace0 x_17512)
     420| Wr_ret (s0, tr, s', depth, trace0, x_17514) ->
     421  h_wr_ret s0 tr s' depth __ trace0 __ x_17514
    422422    (will_return_rect_Type0 ge h_wr_step h_wr_call h_wr_ret h_wr_base depth
    423       s' trace0 x_2634)
     423      s' trace0 x_17514)
    424424| Wr_base (s0, tr, s', trace0) -> h_wr_base s0 tr s' __ trace0 __
    425425
     
    851851    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    852852    trace_result -> 'a2 **)
    853 let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_3169 =
     853let rec trace_result_rect_Type4 ge depth ends start full original_terminates limit h_mk_trace_result x_18049 =
    854854  let { new_state = new_state0; remainder = remainder0; new_trace =
    855     new_trace0; terminates = terminates0 } = x_3169
     855    new_trace0; terminates = terminates0 } = x_18049
    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_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_3171 =
     865let rec trace_result_rect_Type5 ge depth ends start full original_terminates limit h_mk_trace_result x_18051 =
    866866  let { new_state = new_state0; remainder = remainder0; new_trace =
    867     new_trace0; terminates = terminates0 } = x_3171
     867    new_trace0; terminates = terminates0 } = x_18051
    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_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_3173 =
     877let rec trace_result_rect_Type3 ge depth ends start full original_terminates limit h_mk_trace_result x_18053 =
    878878  let { new_state = new_state0; remainder = remainder0; new_trace =
    879     new_trace0; terminates = terminates0 } = x_3173
     879    new_trace0; terminates = terminates0 } = x_18053
    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_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_3175 =
     889let rec trace_result_rect_Type2 ge depth ends start full original_terminates limit h_mk_trace_result x_18055 =
    890890  let { new_state = new_state0; remainder = remainder0; new_trace =
    891     new_trace0; terminates = terminates0 } = x_3175
     891    new_trace0; terminates = terminates0 } = x_18055
    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_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_3177 =
     901let rec trace_result_rect_Type1 ge depth ends start full original_terminates limit h_mk_trace_result x_18057 =
    902902  let { new_state = new_state0; remainder = remainder0; new_trace =
    903     new_trace0; terminates = terminates0 } = x_3177
     903    new_trace0; terminates = terminates0 } = x_18057
    904904  in
    905905  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    911911    (IO.io_out, IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1
    912912    trace_result -> 'a2 **)
    913 let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_3179 =
     913let rec trace_result_rect_Type0 ge depth ends start full original_terminates limit h_mk_trace_result x_18059 =
    914914  let { new_state = new_state0; remainder = remainder0; new_trace =
    915     new_trace0; terminates = terminates0 } = x_3179
     915    new_trace0; terminates = terminates0 } = x_18059
    916916  in
    917917  h_mk_trace_result new_state0 remainder0 __ new_trace0 __ terminates0
     
    10111011    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10121012    sub_trace_result -> 'a2 **)
    1013 let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_3197 =
    1014   let { ends = ends0; trace_res = trace_res0 } = x_3197 in
     1013let rec sub_trace_result_rect_Type4 ge depth start full original_terminates limit h_mk_sub_trace_result x_18077 =
     1014  let { ends = ends0; trace_res = trace_res0 } = x_18077 in
    10151015  h_mk_sub_trace_result ends0 trace_res0
    10161016
     
    10201020    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10211021    sub_trace_result -> 'a2 **)
    1022 let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_3199 =
    1023   let { ends = ends0; trace_res = trace_res0 } = x_3199 in
     1022let rec sub_trace_result_rect_Type5 ge depth start full original_terminates limit h_mk_sub_trace_result x_18079 =
     1023  let { ends = ends0; trace_res = trace_res0 } = x_18079 in
    10241024  h_mk_sub_trace_result ends0 trace_res0
    10251025
     
    10291029    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10301030    sub_trace_result -> 'a2 **)
    1031 let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_3201 =
    1032   let { ends = ends0; trace_res = trace_res0 } = x_3201 in
     1031let rec sub_trace_result_rect_Type3 ge depth start full original_terminates limit h_mk_sub_trace_result x_18081 =
     1032  let { ends = ends0; trace_res = trace_res0 } = x_18081 in
    10331033  h_mk_sub_trace_result ends0 trace_res0
    10341034
     
    10381038    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10391039    sub_trace_result -> 'a2 **)
    1040 let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_3203 =
    1041   let { ends = ends0; trace_res = trace_res0 } = x_3203 in
     1040let rec sub_trace_result_rect_Type2 ge depth start full original_terminates limit h_mk_sub_trace_result x_18083 =
     1041  let { ends = ends0; trace_res = trace_res0 } = x_18083 in
    10421042  h_mk_sub_trace_result ends0 trace_res0
    10431043
     
    10471047    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10481048    sub_trace_result -> 'a2 **)
    1049 let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_3205 =
    1050   let { ends = ends0; trace_res = trace_res0 } = x_3205 in
     1049let rec sub_trace_result_rect_Type1 ge depth start full original_terminates limit h_mk_sub_trace_result x_18085 =
     1050  let { ends = ends0; trace_res = trace_res0 } = x_18085 in
    10511051  h_mk_sub_trace_result ends0 trace_res0
    10521052
     
    10561056    (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
    10571057    sub_trace_result -> 'a2 **)
    1058 let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_3207 =
    1059   let { ends = ends0; trace_res = trace_res0 } = x_3207 in
     1058let rec sub_trace_result_rect_Type0 ge depth start full original_terminates limit h_mk_sub_trace_result x_18087 =
     1059  let { ends = ends0; trace_res = trace_res0 } = x_18087 in
    10601060  h_mk_sub_trace_result ends0 trace_res0
    10611061
     
    15731573    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
    15741574    partial_flat_trace -> 'a3 **)
    1575 let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_3542 x_3541 = function
     1575let rec partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step x_18422 x_18421 = function
    15761576| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1577 | Pft_step (s, tr, s', s'', x_3545) ->
    1578   h_pft_step s tr s' s'' __ x_3545
    1579     (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_3545)
     1577| Pft_step (s, tr, s', s'', x_18425) ->
     1578  h_pft_step s tr s' s'' __ x_18425
     1579    (partial_flat_trace_rect_Type4 ge h_pft_base h_pft_step s' s'' x_18425)
    15801580
    15811581(** val partial_flat_trace_rect_Type3 :
     
    15861586    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
    15871587    partial_flat_trace -> 'a3 **)
    1588 let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_3558 x_3557 = function
     1588let rec partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step x_18438 x_18437 = function
    15891589| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1590 | Pft_step (s, tr, s', s'', x_3561) ->
    1591   h_pft_step s tr s' s'' __ x_3561
    1592     (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_3561)
     1590| Pft_step (s, tr, s', s'', x_18441) ->
     1591  h_pft_step s tr s' s'' __ x_18441
     1592    (partial_flat_trace_rect_Type3 ge h_pft_base h_pft_step s' s'' x_18441)
    15931593
    15941594(** val partial_flat_trace_rect_Type2 :
     
    15991599    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
    16001600    partial_flat_trace -> 'a3 **)
    1601 let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_3566 x_3565 = function
     1601let rec partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step x_18446 x_18445 = function
    16021602| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1603 | Pft_step (s, tr, s', s'', x_3569) ->
    1604   h_pft_step s tr s' s'' __ x_3569
    1605     (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_3569)
     1603| Pft_step (s, tr, s', s'', x_18449) ->
     1604  h_pft_step s tr s' s'' __ x_18449
     1605    (partial_flat_trace_rect_Type2 ge h_pft_base h_pft_step s' s'' x_18449)
    16061606
    16071607(** val partial_flat_trace_rect_Type1 :
     
    16121612    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
    16131613    partial_flat_trace -> 'a3 **)
    1614 let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_3574 x_3573 = function
     1614let rec partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step x_18454 x_18453 = function
    16151615| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1616 | Pft_step (s, tr, s', s'', x_3577) ->
    1617   h_pft_step s tr s' s'' __ x_3577
    1618     (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_3577)
     1616| Pft_step (s, tr, s', s'', x_18457) ->
     1617  h_pft_step s tr s' s'' __ x_18457
     1618    (partial_flat_trace_rect_Type1 ge h_pft_base h_pft_step s' s'' x_18457)
    16191619
    16201620(** val partial_flat_trace_rect_Type0 :
     
    16251625    RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> ('a1, 'a2)
    16261626    partial_flat_trace -> 'a3 **)
    1627 let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_3582 x_3581 = function
     1627let rec partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step x_18462 x_18461 = function
    16281628| Pft_base (s, tr, s') -> h_pft_base s tr s' __
    1629 | Pft_step (s, tr, s', s'', x_3585) ->
    1630   h_pft_step s tr s' s'' __ x_3585
    1631     (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_3585)
     1629| Pft_step (s, tr, s', s'', x_18465) ->
     1630  h_pft_step s tr s' s'' __ x_18465
     1631    (partial_flat_trace_rect_Type0 ge h_pft_base h_pft_step s' s'' x_18465)
    16321632
    16331633(** val partial_flat_trace_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.