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_abstract.ml

    r2730 r2743  
    150150    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
    151151    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    152 let rec rTLabs_ext_state_rect_Type4 ge h_mk_RTLabs_ext_state x_2285 =
    153   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2285 in
     152let rec rTLabs_ext_state_rect_Type4 ge h_mk_RTLabs_ext_state x_17165 =
     153  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17165 in
    154154  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    155155
     
    157157    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
    158158    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    159 let rec rTLabs_ext_state_rect_Type5 ge h_mk_RTLabs_ext_state x_2287 =
    160   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2287 in
     159let rec rTLabs_ext_state_rect_Type5 ge h_mk_RTLabs_ext_state x_17167 =
     160  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17167 in
    161161  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    162162
     
    164164    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
    165165    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    166 let rec rTLabs_ext_state_rect_Type3 ge h_mk_RTLabs_ext_state x_2289 =
    167   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2289 in
     166let rec rTLabs_ext_state_rect_Type3 ge h_mk_RTLabs_ext_state x_17169 =
     167  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17169 in
    168168  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    169169
     
    171171    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
    172172    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    173 let rec rTLabs_ext_state_rect_Type2 ge h_mk_RTLabs_ext_state x_2291 =
    174   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2291 in
     173let rec rTLabs_ext_state_rect_Type2 ge h_mk_RTLabs_ext_state x_17171 =
     174  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17171 in
    175175  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    176176
     
    178178    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
    179179    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    180 let rec rTLabs_ext_state_rect_Type1 ge h_mk_RTLabs_ext_state x_2293 =
    181   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2293 in
     180let rec rTLabs_ext_state_rect_Type1 ge h_mk_RTLabs_ext_state x_17173 =
     181  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17173 in
    182182  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    183183
     
    185185    RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
    186186    List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1 **)
    187 let rec rTLabs_ext_state_rect_Type0 ge h_mk_RTLabs_ext_state x_2295 =
    188   let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_2295 in
     187let rec rTLabs_ext_state_rect_Type0 ge h_mk_RTLabs_ext_state x_17175 =
     188  let { ras_state = ras_state0; ras_fn_stack = ras_fn_stack0 } = x_17175 in
    189189  h_mk_RTLabs_ext_state ras_state0 ras_fn_stack0 __
    190190
     
    340340    rTLabs_pc -> 'a1 **)
    341341let rec rTLabs_pc_rect_Type4 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    342 | Rapc_state (x_2321, x_2320) -> h_rapc_state x_2321 x_2320
    343 | Rapc_call (x_2323, x_2322) -> h_rapc_call x_2323 x_2322
    344 | Rapc_ret x_2324 -> h_rapc_ret x_2324
     342| Rapc_state (x_17201, x_17200) -> h_rapc_state x_17201 x_17200
     343| Rapc_call (x_17203, x_17202) -> h_rapc_call x_17203 x_17202
     344| Rapc_ret x_17204 -> h_rapc_ret x_17204
    345345| Rapc_fin -> h_rapc_fin
    346346
     
    350350    rTLabs_pc -> 'a1 **)
    351351let rec rTLabs_pc_rect_Type5 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    352 | Rapc_state (x_2331, x_2330) -> h_rapc_state x_2331 x_2330
    353 | Rapc_call (x_2333, x_2332) -> h_rapc_call x_2333 x_2332
    354 | Rapc_ret x_2334 -> h_rapc_ret x_2334
     352| Rapc_state (x_17211, x_17210) -> h_rapc_state x_17211 x_17210
     353| Rapc_call (x_17213, x_17212) -> h_rapc_call x_17213 x_17212
     354| Rapc_ret x_17214 -> h_rapc_ret x_17214
    355355| Rapc_fin -> h_rapc_fin
    356356
     
    360360    rTLabs_pc -> 'a1 **)
    361361let rec rTLabs_pc_rect_Type3 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    362 | Rapc_state (x_2341, x_2340) -> h_rapc_state x_2341 x_2340
    363 | Rapc_call (x_2343, x_2342) -> h_rapc_call x_2343 x_2342
    364 | Rapc_ret x_2344 -> h_rapc_ret x_2344
     362| Rapc_state (x_17221, x_17220) -> h_rapc_state x_17221 x_17220
     363| Rapc_call (x_17223, x_17222) -> h_rapc_call x_17223 x_17222
     364| Rapc_ret x_17224 -> h_rapc_ret x_17224
    365365| Rapc_fin -> h_rapc_fin
    366366
     
    370370    rTLabs_pc -> 'a1 **)
    371371let rec rTLabs_pc_rect_Type2 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    372 | Rapc_state (x_2351, x_2350) -> h_rapc_state x_2351 x_2350
    373 | Rapc_call (x_2353, x_2352) -> h_rapc_call x_2353 x_2352
    374 | Rapc_ret x_2354 -> h_rapc_ret x_2354
     372| Rapc_state (x_17231, x_17230) -> h_rapc_state x_17231 x_17230
     373| Rapc_call (x_17233, x_17232) -> h_rapc_call x_17233 x_17232
     374| Rapc_ret x_17234 -> h_rapc_ret x_17234
    375375| Rapc_fin -> h_rapc_fin
    376376
     
    380380    rTLabs_pc -> 'a1 **)
    381381let rec rTLabs_pc_rect_Type1 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    382 | Rapc_state (x_2361, x_2360) -> h_rapc_state x_2361 x_2360
    383 | Rapc_call (x_2363, x_2362) -> h_rapc_call x_2363 x_2362
    384 | Rapc_ret x_2364 -> h_rapc_ret x_2364
     382| Rapc_state (x_17241, x_17240) -> h_rapc_state x_17241 x_17240
     383| Rapc_call (x_17243, x_17242) -> h_rapc_call x_17243 x_17242
     384| Rapc_ret x_17244 -> h_rapc_ret x_17244
    385385| Rapc_fin -> h_rapc_fin
    386386
     
    390390    rTLabs_pc -> 'a1 **)
    391391let rec rTLabs_pc_rect_Type0 h_rapc_state h_rapc_call h_rapc_ret h_rapc_fin = function
    392 | Rapc_state (x_2371, x_2370) -> h_rapc_state x_2371 x_2370
    393 | Rapc_call (x_2373, x_2372) -> h_rapc_call x_2373 x_2372
    394 | Rapc_ret x_2374 -> h_rapc_ret x_2374
     392| Rapc_state (x_17251, x_17250) -> h_rapc_state x_17251 x_17250
     393| Rapc_call (x_17253, x_17252) -> h_rapc_call x_17253 x_17252
     394| Rapc_ret x_17254 -> h_rapc_ret x_17254
    395395| Rapc_fin -> h_rapc_fin
    396396
Note: See TracChangeset for help on using the changeset viewer.