Changeset 2882 for extracted/toCminor.ml


Ignore:
Timestamp:
Mar 15, 2013, 5:52:58 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/toCminor.ml

    r2827 r2882  
    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_634 -> h_Global x_634
     201| Stack x_635 -> h_Stack x_635
    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_640 -> h_Global x_640
     208| Stack x_641 -> h_Stack x_641
    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_646 -> h_Global x_646
     215| Stack x_647 -> h_Stack x_647
    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_652 -> h_Global x_652
     222| Stack x_653 -> h_Stack x_653
    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_658 -> h_Global x_658
     229| Stack x_659 -> h_Stack x_659
    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_664 -> h_Global x_664
     236| Stack x_665 -> h_Stack x_665
    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_712 -> h_MemDest x_712
    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_717 -> h_MemDest x_717
    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_722 -> h_MemDest x_722
    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_727 -> h_MemDest x_727
    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_732 -> h_MemDest x_732
    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_737 -> h_MemDest x_737
    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 =
    1385   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1386     x_14588
     1384let rec labgen_rect_Type4 h_mk_labgen x_772 =
     1385  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_772
    13871386  in
    13881387  h_mk_labgen labuniverse0 label_genlist0 __
     
    13911390    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13921391    'a1) -> labgen -> 'a1 **)
    1393 let rec labgen_rect_Type5 h_mk_labgen x_14590 =
    1394   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1395     x_14590
     1392let rec labgen_rect_Type5 h_mk_labgen x_774 =
     1393  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_774
    13961394  in
    13971395  h_mk_labgen labuniverse0 label_genlist0 __
     
    14001398    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14011399    'a1) -> labgen -> 'a1 **)
    1402 let rec labgen_rect_Type3 h_mk_labgen x_14592 =
    1403   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1404     x_14592
     1400let rec labgen_rect_Type3 h_mk_labgen x_776 =
     1401  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_776
    14051402  in
    14061403  h_mk_labgen labuniverse0 label_genlist0 __
     
    14091406    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14101407    'a1) -> labgen -> 'a1 **)
    1411 let rec labgen_rect_Type2 h_mk_labgen x_14594 =
    1412   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1413     x_14594
     1408let rec labgen_rect_Type2 h_mk_labgen x_778 =
     1409  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_778
    14141410  in
    14151411  h_mk_labgen labuniverse0 label_genlist0 __
     
    14181414    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14191415    'a1) -> labgen -> 'a1 **)
    1420 let rec labgen_rect_Type1 h_mk_labgen x_14596 =
    1421   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1422     x_14596
     1416let rec labgen_rect_Type1 h_mk_labgen x_780 =
     1417  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_780
    14231418  in
    14241419  h_mk_labgen labuniverse0 label_genlist0 __
     
    14271422    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14281423    'a1) -> labgen -> 'a1 **)
    1429 let rec labgen_rect_Type0 h_mk_labgen x_14598 =
    1430   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1431     x_14598
     1424let rec labgen_rect_Type0 h_mk_labgen x_782 =
     1425  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_782
    14321426  in
    14331427  h_mk_labgen labuniverse0 label_genlist0 __
     
    15541548    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15551549    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
     1550let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_798 =
     1551  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_798 in
    15581552  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15591553
     
    15611555    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15621556    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
     1557let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_800 =
     1558  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_800 in
    15651559  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15661560
     
    15681562    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15691563    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
     1564let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_802 =
     1565  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_802 in
    15721566  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15731567
     
    15751569    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15761570    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
     1571let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_804 =
     1572  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_804 in
    15791573  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15801574
     
    15821576    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15831577    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
     1578let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_806 =
     1579  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_806 in
    15861580  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15871581
     
    15891583    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15901584    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
     1585let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_808 =
     1586  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_808 in
    15931587  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15941588
     
    16741668let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
    16751669| DoNotConvert -> h_DoNotConvert
    1676 | ConvertTo (x_14646, x_14645) -> h_ConvertTo x_14646 x_14645
     1670| ConvertTo (x_830, x_829) -> h_ConvertTo x_830 x_829
    16771671
    16781672(** val convert_flag_rect_Type5 :
     
    16811675let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
    16821676| DoNotConvert -> h_DoNotConvert
    1683 | ConvertTo (x_14651, x_14650) -> h_ConvertTo x_14651 x_14650
     1677| ConvertTo (x_835, x_834) -> h_ConvertTo x_835 x_834
    16841678
    16851679(** val convert_flag_rect_Type3 :
     
    16881682let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
    16891683| DoNotConvert -> h_DoNotConvert
    1690 | ConvertTo (x_14656, x_14655) -> h_ConvertTo x_14656 x_14655
     1684| ConvertTo (x_840, x_839) -> h_ConvertTo x_840 x_839
    16911685
    16921686(** val convert_flag_rect_Type2 :
     
    16951689let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
    16961690| DoNotConvert -> h_DoNotConvert
    1697 | ConvertTo (x_14661, x_14660) -> h_ConvertTo x_14661 x_14660
     1691| ConvertTo (x_845, x_844) -> h_ConvertTo x_845 x_844
    16981692
    16991693(** val convert_flag_rect_Type1 :
     
    17021696let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
    17031697| DoNotConvert -> h_DoNotConvert
    1704 | ConvertTo (x_14666, x_14665) -> h_ConvertTo x_14666 x_14665
     1698| ConvertTo (x_850, x_849) -> h_ConvertTo x_850 x_849
    17051699
    17061700(** val convert_flag_rect_Type0 :
     
    17091703let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
    17101704| DoNotConvert -> h_DoNotConvert
    1711 | ConvertTo (x_14671, x_14670) -> h_ConvertTo x_14671 x_14670
     1705| ConvertTo (x_855, x_854) -> h_ConvertTo x_855 x_854
    17121706
    17131707(** val convert_flag_inv_rect_Type4 :
     
    18321826                Obj.magic (Errors.OK { Types.fst = { Types.fst = uv2;
    18331827                  Types.snd = ul }; Types.snd = (Cminor_syntax.St_seq
    1834                   ((Cminor_syntax.St_store (AST.ASTptr, (Cminor_syntax.Id
    1835                   (AST.ASTptr, tmp2)), (Types.pi1 e1'))),
    1836                   (Cminor_syntax.St_seq ((Cminor_syntax.St_call ((Types.Some
    1837                   { Types.fst = tmp; Types.snd =
    1838                   (Csyntax.typ_of_type (Csyntax.typeof e1)) }),
     1828                  ((Cminor_syntax.St_assign (AST.ASTptr, tmp2,
     1829                  (Types.pi1 e1'))), (Cminor_syntax.St_seq
     1830                  ((Cminor_syntax.St_call ((Types.Some { Types.fst = tmp;
     1831                  Types.snd = (Csyntax.typ_of_type (Csyntax.typeof e1)) }),
    18391832                  (Types.pi1 ef'0), (Types.pi1 args'))),
    18401833                  (Cminor_syntax.St_store
    18411834                  ((Csyntax.typ_of_type (Csyntax.typeof e1)),
    1842                   (Types.pi1 e1'), (Cminor_syntax.Id
     1835                  (Cminor_syntax.Id (AST.ASTptr, tmp2)), (Cminor_syntax.Id
    18431836                  ((Csyntax.typ_of_type (Csyntax.typeof e1)), tmp)))))))) })))
    18441837                  __)) __)))))
     
    20442037    Obj.magic
    20452038      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
    2046         (fun eta2436 ->
    2047         let result = eta2436 in
     2039        (fun eta244 ->
     2040        let result = eta244 in
    20482041        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20492042        (fun _ ->
Note: See TracChangeset for help on using the changeset viewer.