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

    r2730 r2743  
    9999    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    100100    'a2) trans_system -> 'a3 **)
    101 let rec trans_system_rect_Type4 h_mk_trans_system x_8529 =
    102   let { is_final = is_final0; step = step0 } = x_8529 in
     101let rec trans_system_rect_Type4 h_mk_trans_system x_5873 =
     102  let { is_final = is_final0; step = step0 } = x_5873 in
    103103  h_mk_trans_system __ __ is_final0 step0
    104104
     
    107107    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    108108    'a2) trans_system -> 'a3 **)
    109 let rec trans_system_rect_Type5 h_mk_trans_system x_8531 =
    110   let { is_final = is_final0; step = step0 } = x_8531 in
     109let rec trans_system_rect_Type5 h_mk_trans_system x_5875 =
     110  let { is_final = is_final0; step = step0 } = x_5875 in
    111111  h_mk_trans_system __ __ is_final0 step0
    112112
     
    115115    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    116116    'a2) trans_system -> 'a3 **)
    117 let rec trans_system_rect_Type3 h_mk_trans_system x_8533 =
    118   let { is_final = is_final0; step = step0 } = x_8533 in
     117let rec trans_system_rect_Type3 h_mk_trans_system x_5877 =
     118  let { is_final = is_final0; step = step0 } = x_5877 in
    119119  h_mk_trans_system __ __ is_final0 step0
    120120
     
    123123    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    124124    'a2) trans_system -> 'a3 **)
    125 let rec trans_system_rect_Type2 h_mk_trans_system x_8535 =
    126   let { is_final = is_final0; step = step0 } = x_8535 in
     125let rec trans_system_rect_Type2 h_mk_trans_system x_5879 =
     126  let { is_final = is_final0; step = step0 } = x_5879 in
    127127  h_mk_trans_system __ __ is_final0 step0
    128128
     
    131131    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    132132    'a2) trans_system -> 'a3 **)
    133 let rec trans_system_rect_Type1 h_mk_trans_system x_8537 =
    134   let { is_final = is_final0; step = step0 } = x_8537 in
     133let rec trans_system_rect_Type1 h_mk_trans_system x_5881 =
     134  let { is_final = is_final0; step = step0 } = x_5881 in
    135135  h_mk_trans_system __ __ is_final0 step0
    136136
     
    139139    ('a1, 'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1,
    140140    'a2) trans_system -> 'a3 **)
    141 let rec trans_system_rect_Type0 h_mk_trans_system x_8539 =
    142   let { is_final = is_final0; step = step0 } = x_8539 in
     141let rec trans_system_rect_Type0 h_mk_trans_system x_5883 =
     142  let { is_final = is_final0; step = step0 } = x_5883 in
    143143  h_mk_trans_system __ __ is_final0 step0
    144144
    145 type ('a,'b) global = __
    146 
    147 type ('a,'b) state = __
     145type ('x, 'x0) global = __
     146
     147type ('x, 'x0) state = __
    148148
    149149(** val is_final :
     
    227227    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    228228    await_value_stuff -> 'a1 **)
    229 let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_8701 =
    230   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8701
     229let rec await_value_stuff_rect_Type4 h_mk_await_value_stuff x_6045 =
     230  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6045
    231231  in
    232232  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
     
    235235    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    236236    await_value_stuff -> 'a1 **)
    237 let rec await_value_stuff_rect_Type5 h_mk_await_value_stuff x_8703 =
    238   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8703
     237let rec await_value_stuff_rect_Type5 h_mk_await_value_stuff x_6047 =
     238  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6047
    239239  in
    240240  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
     
    243243    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    244244    await_value_stuff -> 'a1 **)
    245 let rec await_value_stuff_rect_Type3 h_mk_await_value_stuff x_8705 =
    246   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8705
     245let rec await_value_stuff_rect_Type3 h_mk_await_value_stuff x_6049 =
     246  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6049
    247247  in
    248248  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
     
    251251    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    252252    await_value_stuff -> 'a1 **)
    253 let rec await_value_stuff_rect_Type2 h_mk_await_value_stuff x_8707 =
    254   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8707
     253let rec await_value_stuff_rect_Type2 h_mk_await_value_stuff x_6051 =
     254  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6051
    255255  in
    256256  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
     
    259259    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    260260    await_value_stuff -> 'a1 **)
    261 let rec await_value_stuff_rect_Type1 h_mk_await_value_stuff x_8709 =
    262   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8709
     261let rec await_value_stuff_rect_Type1 h_mk_await_value_stuff x_6053 =
     262  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6053
    263263  in
    264264  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
     
    267267    (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
    268268    await_value_stuff -> 'a1 **)
    269 let rec await_value_stuff_rect_Type0 h_mk_await_value_stuff x_8711 =
    270   let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_8711
     269let rec await_value_stuff_rect_Type0 h_mk_await_value_stuff x_6055 =
     270  let { avs_exec = avs_exec0; avs_g = avs_g0; avs_inv = avs_inv0 } = x_6055
    271271  in
    272272  h_mk_await_value_stuff __ __ avs_exec0 avs_g0 avs_inv0
     
    456456    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    457457    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
    458 let rec fullexec_rect_Type4 h_mk_fullexec x_8729 =
     458let rec fullexec_rect_Type4 h_mk_fullexec x_6073 =
    459459  let { es1 = es2; make_global = make_global0; make_initial_state =
    460     make_initial_state0 } = x_8729
     460    make_initial_state0 } = x_6073
    461461  in
    462462  h_mk_fullexec __ es2 make_global0 make_initial_state0
     
    465465    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    466466    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
    467 let rec fullexec_rect_Type5 h_mk_fullexec x_8731 =
     467let rec fullexec_rect_Type5 h_mk_fullexec x_6075 =
    468468  let { es1 = es2; make_global = make_global0; make_initial_state =
    469     make_initial_state0 } = x_8731
     469    make_initial_state0 } = x_6075
    470470  in
    471471  h_mk_fullexec __ es2 make_global0 make_initial_state0
     
    474474    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    475475    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
    476 let rec fullexec_rect_Type3 h_mk_fullexec x_8733 =
     476let rec fullexec_rect_Type3 h_mk_fullexec x_6077 =
    477477  let { es1 = es2; make_global = make_global0; make_initial_state =
    478     make_initial_state0 } = x_8733
     478    make_initial_state0 } = x_6077
    479479  in
    480480  h_mk_fullexec __ es2 make_global0 make_initial_state0
     
    483483    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    484484    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
    485 let rec fullexec_rect_Type2 h_mk_fullexec x_8735 =
     485let rec fullexec_rect_Type2 h_mk_fullexec x_6079 =
    486486  let { es1 = es2; make_global = make_global0; make_initial_state =
    487     make_initial_state0 } = x_8735
     487    make_initial_state0 } = x_6079
    488488  in
    489489  h_mk_fullexec __ es2 make_global0 make_initial_state0
     
    492492    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    493493    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
    494 let rec fullexec_rect_Type1 h_mk_fullexec x_8737 =
     494let rec fullexec_rect_Type1 h_mk_fullexec x_6081 =
    495495  let { es1 = es2; make_global = make_global0; make_initial_state =
    496     make_initial_state0 } = x_8737
     496    make_initial_state0 } = x_6081
    497497  in
    498498  h_mk_fullexec __ es2 make_global0 make_initial_state0
     
    501501    (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
    502502    'a3) -> ('a1, 'a2) fullexec -> 'a3 **)
    503 let rec fullexec_rect_Type0 h_mk_fullexec x_8739 =
     503let rec fullexec_rect_Type0 h_mk_fullexec x_6083 =
    504504  let { es1 = es2; make_global = make_global0; make_initial_state =
    505     make_initial_state0 } = x_8739
     505    make_initial_state0 } = x_6083
    506506  in
    507507  h_mk_fullexec __ es2 make_global0 make_initial_state0
    508508
    509 type ('a,'b) program0 = __
     509type ('x, 'x0) program0 = __
    510510
    511511(** val es1 : ('a1, 'a2) fullexec -> ('a1, 'a2) trans_system **)
Note: See TracChangeset for help on using the changeset viewer.