Changeset 2890 for extracted/toCminor.ml


Ignore:
Timestamp:
Mar 15, 2013, 11:11:45 PM (7 years ago)
Author:
sacerdot
Message:

Exported again, now the execution is correct up to LIN for a simple program.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/toCminor.ml

    r2882 r2890  
    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_634 -> h_Global x_634
    201 | Stack x_635 -> h_Stack x_635
     200| Global x_13042 -> h_Global x_13042
     201| Stack x_13043 -> h_Stack x_13043
    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_640 -> h_Global x_640
    208 | Stack x_641 -> h_Stack x_641
     207| Global x_13048 -> h_Global x_13048
     208| Stack x_13049 -> h_Stack x_13049
    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_646 -> h_Global x_646
    215 | Stack x_647 -> h_Stack x_647
     214| Global x_13054 -> h_Global x_13054
     215| Stack x_13055 -> h_Stack x_13055
    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_652 -> h_Global x_652
    222 | Stack x_653 -> h_Stack x_653
     221| Global x_13060 -> h_Global x_13060
     222| Stack x_13061 -> h_Stack x_13061
    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_658 -> h_Global x_658
    229 | Stack x_659 -> h_Stack x_659
     228| Global x_13066 -> h_Global x_13066
     229| Stack x_13067 -> h_Stack x_13067
    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_664 -> h_Global x_664
    236 | Stack x_665 -> h_Stack x_665
     235| Global x_13072 -> h_Global x_13072
     236| Stack x_13073 -> h_Stack x_13073
    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_712 -> h_MemDest x_712
     1223| MemDest x_14528 -> h_MemDest x_14528
    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_717 -> h_MemDest x_717
     1230| MemDest x_14533 -> h_MemDest x_14533
    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_722 -> h_MemDest x_722
     1237| MemDest x_14538 -> h_MemDest x_14538
    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_727 -> h_MemDest x_727
     1244| MemDest x_14543 -> h_MemDest x_14543
    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_732 -> h_MemDest x_732
     1251| MemDest x_14548 -> h_MemDest x_14548
    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_737 -> h_MemDest x_737
     1258| MemDest x_14553 -> h_MemDest x_14553
    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_772 =
    1385   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_772
     1384let rec labgen_rect_Type4 h_mk_labgen x_14588 =
     1385  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1386    x_14588
    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_774 =
    1393   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_774
     1393let rec labgen_rect_Type5 h_mk_labgen x_14590 =
     1394  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1395    x_14590
    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_776 =
    1401   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_776
     1402let rec labgen_rect_Type3 h_mk_labgen x_14592 =
     1403  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1404    x_14592
    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_778 =
    1409   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_778
     1411let rec labgen_rect_Type2 h_mk_labgen x_14594 =
     1412  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1413    x_14594
    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_780 =
    1417   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_780
     1420let rec labgen_rect_Type1 h_mk_labgen x_14596 =
     1421  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1422    x_14596
    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_782 =
    1425   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_782
     1429let rec labgen_rect_Type0 h_mk_labgen x_14598 =
     1430  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1431    x_14598
    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_798 =
    1551   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_798 in
     1556let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14614 =
     1557  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14614 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_800 =
    1558   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_800 in
     1563let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14616 =
     1564  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14616 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_802 =
    1565   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_802 in
     1570let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14618 =
     1571  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14618 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_804 =
    1572   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_804 in
     1577let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14620 =
     1578  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14620 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_806 =
    1579   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_806 in
     1584let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14622 =
     1585  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14622 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_808 =
    1586   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_808 in
     1591let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14624 =
     1592  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14624 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_830, x_829) -> h_ConvertTo x_830 x_829
     1676| ConvertTo (x_14646, x_14645) -> h_ConvertTo x_14646 x_14645
    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_835, x_834) -> h_ConvertTo x_835 x_834
     1683| ConvertTo (x_14651, x_14650) -> h_ConvertTo x_14651 x_14650
    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_840, x_839) -> h_ConvertTo x_840 x_839
     1690| ConvertTo (x_14656, x_14655) -> h_ConvertTo x_14656 x_14655
    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_845, x_844) -> h_ConvertTo x_845 x_844
     1697| ConvertTo (x_14661, x_14660) -> h_ConvertTo x_14661 x_14660
    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_850, x_849) -> h_ConvertTo x_850 x_849
     1704| ConvertTo (x_14666, x_14665) -> h_ConvertTo x_14666 x_14665
    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_855, x_854) -> h_ConvertTo x_855 x_854
     1711| ConvertTo (x_14671, x_14670) -> h_ConvertTo x_14671 x_14670
    17061712
    17071713(** val convert_flag_inv_rect_Type4 :
     
    20372043    Obj.magic
    20382044      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
    2039         (fun eta244 ->
    2040         let result = eta244 in
     2045        (fun eta2436 ->
     2046        let result = eta2436 in
    20412047        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20422048        (fun _ ->
Note: See TracChangeset for help on using the changeset viewer.