Changeset 2951 for extracted/toCminor.ml


Ignore:
Timestamp:
Mar 25, 2013, 11:30:01 PM (7 years ago)
Author:
sacerdot
Message:

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/toCminor.ml

    r2890 r2951  
    198198    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    199199let rec var_type_rect_Type4 h_Global h_Stack h_Local = function
    200 | Global x_13042 -> h_Global x_13042
    201 | Stack x_13043 -> h_Stack x_13043
     200| Global x_13081 -> h_Global x_13081
     201| Stack x_13082 -> h_Stack x_13082
    202202| Local -> h_Local
    203203
     
    205205    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    206206let rec var_type_rect_Type5 h_Global h_Stack h_Local = function
    207 | Global x_13048 -> h_Global x_13048
    208 | Stack x_13049 -> h_Stack x_13049
     207| Global x_13087 -> h_Global x_13087
     208| Stack x_13088 -> h_Stack x_13088
    209209| Local -> h_Local
    210210
     
    212212    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    213213let rec var_type_rect_Type3 h_Global h_Stack h_Local = function
    214 | Global x_13054 -> h_Global x_13054
    215 | Stack x_13055 -> h_Stack x_13055
     214| Global x_13093 -> h_Global x_13093
     215| Stack x_13094 -> h_Stack x_13094
    216216| Local -> h_Local
    217217
     
    219219    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    220220let rec var_type_rect_Type2 h_Global h_Stack h_Local = function
    221 | Global x_13060 -> h_Global x_13060
    222 | Stack x_13061 -> h_Stack x_13061
     221| Global x_13099 -> h_Global x_13099
     222| Stack x_13100 -> h_Stack x_13100
    223223| Local -> h_Local
    224224
     
    226226    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    227227let rec var_type_rect_Type1 h_Global h_Stack h_Local = function
    228 | Global x_13066 -> h_Global x_13066
    229 | Stack x_13067 -> h_Stack x_13067
     228| Global x_13105 -> h_Global x_13105
     229| Stack x_13106 -> h_Stack x_13106
    230230| Local -> h_Local
    231231
     
    233233    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    234234let rec var_type_rect_Type0 h_Global h_Stack h_Local = function
    235 | Global x_13072 -> h_Global x_13072
    236 | Stack x_13073 -> h_Stack x_13073
     235| Global x_13111 -> h_Global x_13111
     236| Stack x_13112 -> h_Stack x_13112
    237237| Local -> h_Local
    238238
     
    12211221let rec destination_rect_Type4 vars h_IdDest h_MemDest = function
    12221222| IdDest (id, ty) -> h_IdDest id ty __
    1223 | MemDest x_14528 -> h_MemDest x_14528
     1223| MemDest x_14567 -> h_MemDest x_14567
    12241224
    12251225(** val destination_rect_Type5 :
     
    12281228let rec destination_rect_Type5 vars h_IdDest h_MemDest = function
    12291229| IdDest (id, ty) -> h_IdDest id ty __
    1230 | MemDest x_14533 -> h_MemDest x_14533
     1230| MemDest x_14572 -> h_MemDest x_14572
    12311231
    12321232(** val destination_rect_Type3 :
     
    12351235let rec destination_rect_Type3 vars h_IdDest h_MemDest = function
    12361236| IdDest (id, ty) -> h_IdDest id ty __
    1237 | MemDest x_14538 -> h_MemDest x_14538
     1237| MemDest x_14577 -> h_MemDest x_14577
    12381238
    12391239(** val destination_rect_Type2 :
     
    12421242let rec destination_rect_Type2 vars h_IdDest h_MemDest = function
    12431243| IdDest (id, ty) -> h_IdDest id ty __
    1244 | MemDest x_14543 -> h_MemDest x_14543
     1244| MemDest x_14582 -> h_MemDest x_14582
    12451245
    12461246(** val destination_rect_Type1 :
     
    12491249let rec destination_rect_Type1 vars h_IdDest h_MemDest = function
    12501250| IdDest (id, ty) -> h_IdDest id ty __
    1251 | MemDest x_14548 -> h_MemDest x_14548
     1251| MemDest x_14587 -> h_MemDest x_14587
    12521252
    12531253(** val destination_rect_Type0 :
     
    12561256let rec destination_rect_Type0 vars h_IdDest h_MemDest = function
    12571257| IdDest (id, ty) -> h_IdDest id ty __
    1258 | MemDest x_14553 -> h_MemDest x_14553
     1258| MemDest x_14592 -> h_MemDest x_14592
    12591259
    12601260(** val destination_inv_rect_Type4 :
     
    13821382    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13831383    'a1) -> labgen -> 'a1 **)
    1384 let rec labgen_rect_Type4 h_mk_labgen x_14588 =
     1384let rec labgen_rect_Type4 h_mk_labgen x_14627 =
    13851385  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1386     x_14588
     1386    x_14627
    13871387  in
    13881388  h_mk_labgen labuniverse0 label_genlist0 __
     
    13911391    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13921392    'a1) -> labgen -> 'a1 **)
    1393 let rec labgen_rect_Type5 h_mk_labgen x_14590 =
     1393let rec labgen_rect_Type5 h_mk_labgen x_14629 =
    13941394  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1395     x_14590
     1395    x_14629
    13961396  in
    13971397  h_mk_labgen labuniverse0 label_genlist0 __
     
    14001400    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14011401    'a1) -> labgen -> 'a1 **)
    1402 let rec labgen_rect_Type3 h_mk_labgen x_14592 =
     1402let rec labgen_rect_Type3 h_mk_labgen x_14631 =
    14031403  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1404     x_14592
     1404    x_14631
    14051405  in
    14061406  h_mk_labgen labuniverse0 label_genlist0 __
     
    14091409    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14101410    'a1) -> labgen -> 'a1 **)
    1411 let rec labgen_rect_Type2 h_mk_labgen x_14594 =
     1411let rec labgen_rect_Type2 h_mk_labgen x_14633 =
    14121412  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1413     x_14594
     1413    x_14633
    14141414  in
    14151415  h_mk_labgen labuniverse0 label_genlist0 __
     
    14181418    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14191419    'a1) -> labgen -> 'a1 **)
    1420 let rec labgen_rect_Type1 h_mk_labgen x_14596 =
     1420let rec labgen_rect_Type1 h_mk_labgen x_14635 =
    14211421  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1422     x_14596
     1422    x_14635
    14231423  in
    14241424  h_mk_labgen labuniverse0 label_genlist0 __
     
    14271427    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14281428    'a1) -> labgen -> 'a1 **)
    1429 let rec labgen_rect_Type0 h_mk_labgen x_14598 =
     1429let rec labgen_rect_Type0 h_mk_labgen x_14637 =
    14301430  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1431     x_14598
     1431    x_14637
    14321432  in
    14331433  h_mk_labgen labuniverse0 label_genlist0 __
     
    15541554    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15551555    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14614 =
    1557   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14614 in
     1556let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14653 =
     1557  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14653 in
    15581558  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15591559
     
    15611561    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15621562    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14616 =
    1564   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14616 in
     1563let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14655 =
     1564  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14655 in
    15651565  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15661566
     
    15681568    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15691569    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14618 =
    1571   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14618 in
     1570let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14657 =
     1571  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14657 in
    15721572  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15731573
     
    15751575    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15761576    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14620 =
    1578   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14620 in
     1577let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14659 =
     1578  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14659 in
    15791579  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15801580
     
    15821582    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15831583    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14622 =
    1585   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14622 in
     1584let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14661 =
     1585  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14661 in
    15861586  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15871587
     
    15891589    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15901590    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14624 =
    1592   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14624 in
     1591let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14663 =
     1592  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14663 in
    15931593  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15941594
     
    16741674let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
    16751675| DoNotConvert -> h_DoNotConvert
    1676 | ConvertTo (x_14646, x_14645) -> h_ConvertTo x_14646 x_14645
     1676| ConvertTo (x_14685, x_14684) -> h_ConvertTo x_14685 x_14684
    16771677
    16781678(** val convert_flag_rect_Type5 :
     
    16811681let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
    16821682| DoNotConvert -> h_DoNotConvert
    1683 | ConvertTo (x_14651, x_14650) -> h_ConvertTo x_14651 x_14650
     1683| ConvertTo (x_14690, x_14689) -> h_ConvertTo x_14690 x_14689
    16841684
    16851685(** val convert_flag_rect_Type3 :
     
    16881688let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
    16891689| DoNotConvert -> h_DoNotConvert
    1690 | ConvertTo (x_14656, x_14655) -> h_ConvertTo x_14656 x_14655
     1690| ConvertTo (x_14695, x_14694) -> h_ConvertTo x_14695 x_14694
    16911691
    16921692(** val convert_flag_rect_Type2 :
     
    16951695let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
    16961696| DoNotConvert -> h_DoNotConvert
    1697 | ConvertTo (x_14661, x_14660) -> h_ConvertTo x_14661 x_14660
     1697| ConvertTo (x_14700, x_14699) -> h_ConvertTo x_14700 x_14699
    16981698
    16991699(** val convert_flag_rect_Type1 :
     
    17021702let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
    17031703| DoNotConvert -> h_DoNotConvert
    1704 | ConvertTo (x_14666, x_14665) -> h_ConvertTo x_14666 x_14665
     1704| ConvertTo (x_14705, x_14704) -> h_ConvertTo x_14705 x_14704
    17051705
    17061706(** val convert_flag_rect_Type0 :
     
    17091709let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
    17101710| DoNotConvert -> h_DoNotConvert
    1711 | ConvertTo (x_14671, x_14670) -> h_ConvertTo x_14671 x_14670
     1711| ConvertTo (x_14710, x_14709) -> h_ConvertTo x_14710 x_14709
    17121712
    17131713(** val convert_flag_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.