Changeset 2743 for extracted/toCminor.ml


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

    r2730 r2743  
    200200    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    201201let rec var_type_rect_Type4 h_Global h_Stack h_Local = function
    202 | Global x_4448 -> h_Global x_4448
    203 | Stack x_4449 -> h_Stack x_4449
     202| Global x_13003 -> h_Global x_13003
     203| Stack x_13004 -> h_Stack x_13004
    204204| Local -> h_Local
    205205
     
    207207    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    208208let rec var_type_rect_Type5 h_Global h_Stack h_Local = function
    209 | Global x_4454 -> h_Global x_4454
    210 | Stack x_4455 -> h_Stack x_4455
     209| Global x_13009 -> h_Global x_13009
     210| Stack x_13010 -> h_Stack x_13010
    211211| Local -> h_Local
    212212
     
    214214    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    215215let rec var_type_rect_Type3 h_Global h_Stack h_Local = function
    216 | Global x_4460 -> h_Global x_4460
    217 | Stack x_4461 -> h_Stack x_4461
     216| Global x_13015 -> h_Global x_13015
     217| Stack x_13016 -> h_Stack x_13016
    218218| Local -> h_Local
    219219
     
    221221    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    222222let rec var_type_rect_Type2 h_Global h_Stack h_Local = function
    223 | Global x_4466 -> h_Global x_4466
    224 | Stack x_4467 -> h_Stack x_4467
     223| Global x_13021 -> h_Global x_13021
     224| Stack x_13022 -> h_Stack x_13022
    225225| Local -> h_Local
    226226
     
    228228    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    229229let rec var_type_rect_Type1 h_Global h_Stack h_Local = function
    230 | Global x_4472 -> h_Global x_4472
    231 | Stack x_4473 -> h_Stack x_4473
     230| Global x_13027 -> h_Global x_13027
     231| Stack x_13028 -> h_Stack x_13028
    232232| Local -> h_Local
    233233
     
    235235    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    236236let rec var_type_rect_Type0 h_Global h_Stack h_Local = function
    237 | Global x_4478 -> h_Global x_4478
    238 | Stack x_4479 -> h_Stack x_4479
     237| Global x_13033 -> h_Global x_13033
     238| Stack x_13034 -> h_Stack x_13034
    239239| Local -> h_Local
    240240
     
    12231223let rec destination_rect_Type4 vars h_IdDest h_MemDest = function
    12241224| IdDest (id, ty) -> h_IdDest id ty __
    1225 | MemDest x_4526 -> h_MemDest x_4526
     1225| MemDest x_14489 -> h_MemDest x_14489
    12261226
    12271227(** val destination_rect_Type5 :
     
    12301230let rec destination_rect_Type5 vars h_IdDest h_MemDest = function
    12311231| IdDest (id, ty) -> h_IdDest id ty __
    1232 | MemDest x_4531 -> h_MemDest x_4531
     1232| MemDest x_14494 -> h_MemDest x_14494
    12331233
    12341234(** val destination_rect_Type3 :
     
    12371237let rec destination_rect_Type3 vars h_IdDest h_MemDest = function
    12381238| IdDest (id, ty) -> h_IdDest id ty __
    1239 | MemDest x_4536 -> h_MemDest x_4536
     1239| MemDest x_14499 -> h_MemDest x_14499
    12401240
    12411241(** val destination_rect_Type2 :
     
    12441244let rec destination_rect_Type2 vars h_IdDest h_MemDest = function
    12451245| IdDest (id, ty) -> h_IdDest id ty __
    1246 | MemDest x_4541 -> h_MemDest x_4541
     1246| MemDest x_14504 -> h_MemDest x_14504
    12471247
    12481248(** val destination_rect_Type1 :
     
    12511251let rec destination_rect_Type1 vars h_IdDest h_MemDest = function
    12521252| IdDest (id, ty) -> h_IdDest id ty __
    1253 | MemDest x_4546 -> h_MemDest x_4546
     1253| MemDest x_14509 -> h_MemDest x_14509
    12541254
    12551255(** val destination_rect_Type0 :
     
    12581258let rec destination_rect_Type0 vars h_IdDest h_MemDest = function
    12591259| IdDest (id, ty) -> h_IdDest id ty __
    1260 | MemDest x_4551 -> h_MemDest x_4551
     1260| MemDest x_14514 -> h_MemDest x_14514
    12611261
    12621262(** val destination_inv_rect_Type4 :
     
    13861386    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13871387    'a1) -> labgen -> 'a1 **)
    1388 let rec labgen_rect_Type4 h_mk_labgen x_4586 =
    1389   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_4586
     1388let rec labgen_rect_Type4 h_mk_labgen x_14549 =
     1389  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1390    x_14549
    13901391  in
    13911392  h_mk_labgen labuniverse0 label_genlist0 __
     
    13941395    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13951396    'a1) -> labgen -> 'a1 **)
    1396 let rec labgen_rect_Type5 h_mk_labgen x_4588 =
    1397   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_4588
     1397let rec labgen_rect_Type5 h_mk_labgen x_14551 =
     1398  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1399    x_14551
    13981400  in
    13991401  h_mk_labgen labuniverse0 label_genlist0 __
     
    14021404    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14031405    'a1) -> labgen -> 'a1 **)
    1404 let rec labgen_rect_Type3 h_mk_labgen x_4590 =
    1405   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_4590
     1406let rec labgen_rect_Type3 h_mk_labgen x_14553 =
     1407  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1408    x_14553
    14061409  in
    14071410  h_mk_labgen labuniverse0 label_genlist0 __
     
    14101413    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14111414    'a1) -> labgen -> 'a1 **)
    1412 let rec labgen_rect_Type2 h_mk_labgen x_4592 =
    1413   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_4592
     1415let rec labgen_rect_Type2 h_mk_labgen x_14555 =
     1416  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1417    x_14555
    14141418  in
    14151419  h_mk_labgen labuniverse0 label_genlist0 __
     
    14181422    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14191423    'a1) -> labgen -> 'a1 **)
    1420 let rec labgen_rect_Type1 h_mk_labgen x_4594 =
    1421   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_4594
     1424let rec labgen_rect_Type1 h_mk_labgen x_14557 =
     1425  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1426    x_14557
    14221427  in
    14231428  h_mk_labgen labuniverse0 label_genlist0 __
     
    14261431    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14271432    'a1) -> labgen -> 'a1 **)
    1428 let rec labgen_rect_Type0 h_mk_labgen x_4596 =
    1429   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_4596
     1433let rec labgen_rect_Type0 h_mk_labgen x_14559 =
     1434  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1435    x_14559
    14301436  in
    14311437  h_mk_labgen labuniverse0 label_genlist0 __
     
    15521558    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15531559    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1554 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_4612 =
    1555   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_4612 in
     1560let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14575 =
     1561  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14575 in
    15561562  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15571563
     
    15591565    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15601566    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1561 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_4614 =
    1562   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_4614 in
     1567let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14577 =
     1568  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14577 in
    15631569  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15641570
     
    15661572    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15671573    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1568 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_4616 =
    1569   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_4616 in
     1574let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14579 =
     1575  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14579 in
    15701576  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15711577
     
    15731579    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15741580    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1575 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_4618 =
    1576   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_4618 in
     1581let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14581 =
     1582  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14581 in
    15771583  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15781584
     
    15801586    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15811587    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1582 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_4620 =
    1583   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_4620 in
     1588let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14583 =
     1589  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14583 in
    15841590  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15851591
     
    15871593    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15881594    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1589 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_4622 =
    1590   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_4622 in
     1595let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14585 =
     1596  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14585 in
    15911597  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15921598
     
    16721678let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
    16731679| DoNotConvert -> h_DoNotConvert
    1674 | ConvertTo (x_4644, x_4643) -> h_ConvertTo x_4644 x_4643
     1680| ConvertTo (x_14607, x_14606) -> h_ConvertTo x_14607 x_14606
    16751681
    16761682(** val convert_flag_rect_Type5 :
     
    16791685let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
    16801686| DoNotConvert -> h_DoNotConvert
    1681 | ConvertTo (x_4649, x_4648) -> h_ConvertTo x_4649 x_4648
     1687| ConvertTo (x_14612, x_14611) -> h_ConvertTo x_14612 x_14611
    16821688
    16831689(** val convert_flag_rect_Type3 :
     
    16861692let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
    16871693| DoNotConvert -> h_DoNotConvert
    1688 | ConvertTo (x_4654, x_4653) -> h_ConvertTo x_4654 x_4653
     1694| ConvertTo (x_14617, x_14616) -> h_ConvertTo x_14617 x_14616
    16891695
    16901696(** val convert_flag_rect_Type2 :
     
    16931699let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
    16941700| DoNotConvert -> h_DoNotConvert
    1695 | ConvertTo (x_4659, x_4658) -> h_ConvertTo x_4659 x_4658
     1701| ConvertTo (x_14622, x_14621) -> h_ConvertTo x_14622 x_14621
    16961702
    16971703(** val convert_flag_rect_Type1 :
     
    17001706let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
    17011707| DoNotConvert -> h_DoNotConvert
    1702 | ConvertTo (x_4664, x_4663) -> h_ConvertTo x_4664 x_4663
     1708| ConvertTo (x_14627, x_14626) -> h_ConvertTo x_14627 x_14626
    17031709
    17041710(** val convert_flag_rect_Type0 :
     
    17071713let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
    17081714| DoNotConvert -> h_DoNotConvert
    1709 | ConvertTo (x_4669, x_4668) -> h_ConvertTo x_4669 x_4668
     1715| ConvertTo (x_14632, x_14631) -> h_ConvertTo x_14632 x_14631
    17101716
    17111717(** val convert_flag_inv_rect_Type4 :
     
    20302036    Obj.magic
    20312037      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
    2032         (fun eta1293 ->
    2033         let result = eta1293 in
     2038        (fun eta2887 ->
     2039        let result = eta2887 in
    20342040        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20352041        (fun _ ->
Note: See TracChangeset for help on using the changeset viewer.