Changeset 2775 for extracted/toCminor.ml


Ignore:
Timestamp:
Mar 5, 2013, 9:52:39 PM (7 years ago)
Author:
sacerdot
Message:

The compiler now computes also the stack cost model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/toCminor.ml

    r2773 r2775  
    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_8081 -> h_Global x_8081
    201 | Stack x_8082 -> h_Stack x_8082
     200| Global x_12912 -> h_Global x_12912
     201| Stack x_12913 -> h_Stack x_12913
    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_8087 -> h_Global x_8087
    208 | Stack x_8088 -> h_Stack x_8088
     207| Global x_12918 -> h_Global x_12918
     208| Stack x_12919 -> h_Stack x_12919
    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_8093 -> h_Global x_8093
    215 | Stack x_8094 -> h_Stack x_8094
     214| Global x_12924 -> h_Global x_12924
     215| Stack x_12925 -> h_Stack x_12925
    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_8099 -> h_Global x_8099
    222 | Stack x_8100 -> h_Stack x_8100
     221| Global x_12930 -> h_Global x_12930
     222| Stack x_12931 -> h_Stack x_12931
    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_8105 -> h_Global x_8105
    229 | Stack x_8106 -> h_Stack x_8106
     228| Global x_12936 -> h_Global x_12936
     229| Stack x_12937 -> h_Stack x_12937
    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_8111 -> h_Global x_8111
    236 | Stack x_8112 -> h_Stack x_8112
     235| Global x_12942 -> h_Global x_12942
     236| Stack x_12943 -> h_Stack x_12943
    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_9567 -> h_MemDest x_9567
     1223| MemDest x_14398 -> h_MemDest x_14398
    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_9572 -> h_MemDest x_9572
     1230| MemDest x_14403 -> h_MemDest x_14403
    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_9577 -> h_MemDest x_9577
     1237| MemDest x_14408 -> h_MemDest x_14408
    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_9582 -> h_MemDest x_9582
     1244| MemDest x_14413 -> h_MemDest x_14413
    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_9587 -> h_MemDest x_9587
     1251| MemDest x_14418 -> h_MemDest x_14418
    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_9592 -> h_MemDest x_9592
     1258| MemDest x_14423 -> h_MemDest x_14423
    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_9627 =
    1385   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9627
     1384let rec labgen_rect_Type4 h_mk_labgen x_14458 =
     1385  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1386    x_14458
    13861387  in
    13871388  h_mk_labgen labuniverse0 label_genlist0 __
     
    13901391    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13911392    'a1) -> labgen -> 'a1 **)
    1392 let rec labgen_rect_Type5 h_mk_labgen x_9629 =
    1393   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9629
     1393let rec labgen_rect_Type5 h_mk_labgen x_14460 =
     1394  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1395    x_14460
    13941396  in
    13951397  h_mk_labgen labuniverse0 label_genlist0 __
     
    13981400    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13991401    'a1) -> labgen -> 'a1 **)
    1400 let rec labgen_rect_Type3 h_mk_labgen x_9631 =
    1401   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9631
     1402let rec labgen_rect_Type3 h_mk_labgen x_14462 =
     1403  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1404    x_14462
    14021405  in
    14031406  h_mk_labgen labuniverse0 label_genlist0 __
     
    14061409    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14071410    'a1) -> labgen -> 'a1 **)
    1408 let rec labgen_rect_Type2 h_mk_labgen x_9633 =
    1409   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9633
     1411let rec labgen_rect_Type2 h_mk_labgen x_14464 =
     1412  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1413    x_14464
    14101414  in
    14111415  h_mk_labgen labuniverse0 label_genlist0 __
     
    14141418    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14151419    'a1) -> labgen -> 'a1 **)
    1416 let rec labgen_rect_Type1 h_mk_labgen x_9635 =
    1417   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9635
     1420let rec labgen_rect_Type1 h_mk_labgen x_14466 =
     1421  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1422    x_14466
    14181423  in
    14191424  h_mk_labgen labuniverse0 label_genlist0 __
     
    14221427    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14231428    'a1) -> labgen -> 'a1 **)
    1424 let rec labgen_rect_Type0 h_mk_labgen x_9637 =
    1425   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9637
     1429let rec labgen_rect_Type0 h_mk_labgen x_14468 =
     1430  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1431    x_14468
    14261432  in
    14271433  h_mk_labgen labuniverse0 label_genlist0 __
     
    15481554    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15491555    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1550 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_9653 =
    1551   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9653 in
     1556let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14484 =
     1557  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14484 in
    15521558  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15531559
     
    15551561    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15561562    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1557 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_9655 =
    1558   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9655 in
     1563let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14486 =
     1564  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14486 in
    15591565  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15601566
     
    15621568    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15631569    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1564 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_9657 =
    1565   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9657 in
     1570let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14488 =
     1571  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14488 in
    15661572  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15671573
     
    15691575    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15701576    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1571 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_9659 =
    1572   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9659 in
     1577let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14490 =
     1578  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14490 in
    15731579  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15741580
     
    15761582    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15771583    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1578 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_9661 =
    1579   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9661 in
     1584let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14492 =
     1585  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14492 in
    15801586  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15811587
     
    15831589    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15841590    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1585 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_9663 =
    1586   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9663 in
     1591let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14494 =
     1592  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14494 in
    15871593  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15881594
     
    16681674let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
    16691675| DoNotConvert -> h_DoNotConvert
    1670 | ConvertTo (x_9685, x_9684) -> h_ConvertTo x_9685 x_9684
     1676| ConvertTo (x_14516, x_14515) -> h_ConvertTo x_14516 x_14515
    16711677
    16721678(** val convert_flag_rect_Type5 :
     
    16751681let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
    16761682| DoNotConvert -> h_DoNotConvert
    1677 | ConvertTo (x_9690, x_9689) -> h_ConvertTo x_9690 x_9689
     1683| ConvertTo (x_14521, x_14520) -> h_ConvertTo x_14521 x_14520
    16781684
    16791685(** val convert_flag_rect_Type3 :
     
    16821688let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
    16831689| DoNotConvert -> h_DoNotConvert
    1684 | ConvertTo (x_9695, x_9694) -> h_ConvertTo x_9695 x_9694
     1690| ConvertTo (x_14526, x_14525) -> h_ConvertTo x_14526 x_14525
    16851691
    16861692(** val convert_flag_rect_Type2 :
     
    16891695let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
    16901696| DoNotConvert -> h_DoNotConvert
    1691 | ConvertTo (x_9700, x_9699) -> h_ConvertTo x_9700 x_9699
     1697| ConvertTo (x_14531, x_14530) -> h_ConvertTo x_14531 x_14530
    16921698
    16931699(** val convert_flag_rect_Type1 :
     
    16961702let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
    16971703| DoNotConvert -> h_DoNotConvert
    1698 | ConvertTo (x_9705, x_9704) -> h_ConvertTo x_9705 x_9704
     1704| ConvertTo (x_14536, x_14535) -> h_ConvertTo x_14536 x_14535
    16991705
    17001706(** val convert_flag_rect_Type0 :
     
    17031709let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
    17041710| DoNotConvert -> h_DoNotConvert
    1705 | ConvertTo (x_9710, x_9709) -> h_ConvertTo x_9710 x_9709
     1711| ConvertTo (x_14541, x_14540) -> h_ConvertTo x_14541 x_14540
    17061712
    17071713(** val convert_flag_inv_rect_Type4 :
     
    20262032    Obj.magic
    20272033      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
    2028         (fun eta1212 ->
    2029         let result = eta1212 in
     2034        (fun eta2434 ->
     2035        let result = eta2434 in
    20302036        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20312037        (fun _ ->
Note: See TracChangeset for help on using the changeset viewer.