Changeset 3001 for extracted/toCminor.ml


Ignore:
Timestamp:
Mar 28, 2013, 1:02:48 PM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/toCminor.ml

    r2997 r3001  
    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_12720 -> h_Global x_12720
    201 | Stack x_12721 -> h_Stack x_12721
     200| Global x_9647 -> h_Global x_9647
     201| Stack x_9648 -> h_Stack x_9648
    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_12726 -> h_Global x_12726
    208 | Stack x_12727 -> h_Stack x_12727
     207| Global x_9653 -> h_Global x_9653
     208| Stack x_9654 -> h_Stack x_9654
    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_12732 -> h_Global x_12732
    215 | Stack x_12733 -> h_Stack x_12733
     214| Global x_9659 -> h_Global x_9659
     215| Stack x_9660 -> h_Stack x_9660
    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_12738 -> h_Global x_12738
    222 | Stack x_12739 -> h_Stack x_12739
     221| Global x_9665 -> h_Global x_9665
     222| Stack x_9666 -> h_Stack x_9666
    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_12744 -> h_Global x_12744
    229 | Stack x_12745 -> h_Stack x_12745
     228| Global x_9671 -> h_Global x_9671
     229| Stack x_9672 -> h_Stack x_9672
    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_12750 -> h_Global x_12750
    236 | Stack x_12751 -> h_Stack x_12751
     235| Global x_9677 -> h_Global x_9677
     236| Stack x_9678 -> h_Stack x_9678
    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_12798 -> h_MemDest x_12798
     1223| MemDest x_9725 -> h_MemDest x_9725
    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_12803 -> h_MemDest x_12803
     1230| MemDest x_9730 -> h_MemDest x_9730
    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_12808 -> h_MemDest x_12808
     1237| MemDest x_9735 -> h_MemDest x_9735
    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_12813 -> h_MemDest x_12813
     1244| MemDest x_9740 -> h_MemDest x_9740
    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_12818 -> h_MemDest x_12818
     1251| MemDest x_9745 -> h_MemDest x_9745
    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_12823 -> h_MemDest x_12823
     1258| MemDest x_9750 -> h_MemDest x_9750
    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_12858 =
    1385   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1386     x_12858
     1384let rec labgen_rect_Type4 h_mk_labgen x_9785 =
     1385  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9785
    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_12860 =
    1394   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1395     x_12860
     1392let rec labgen_rect_Type5 h_mk_labgen x_9787 =
     1393  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9787
    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_12862 =
    1403   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1404     x_12862
     1400let rec labgen_rect_Type3 h_mk_labgen x_9789 =
     1401  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9789
    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_12864 =
    1412   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1413     x_12864
     1408let rec labgen_rect_Type2 h_mk_labgen x_9791 =
     1409  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9791
    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_12866 =
    1421   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1422     x_12866
     1416let rec labgen_rect_Type1 h_mk_labgen x_9793 =
     1417  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9793
    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_12868 =
    1430   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1431     x_12868
     1424let rec labgen_rect_Type0 h_mk_labgen x_9795 =
     1425  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9795
    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_12884 =
    1557   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12884 in
     1550let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_9811 =
     1551  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9811 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_12886 =
    1564   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12886 in
     1557let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_9813 =
     1558  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9813 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_12888 =
    1571   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12888 in
     1564let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_9815 =
     1565  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9815 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_12890 =
    1578   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12890 in
     1571let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_9817 =
     1572  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9817 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_12892 =
    1585   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12892 in
     1578let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_9819 =
     1579  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9819 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_12894 =
    1592   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12894 in
     1585let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_9821 =
     1586  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9821 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_12916, x_12915) -> h_ConvertTo x_12916 x_12915
     1670| ConvertTo (x_9843, x_9842) -> h_ConvertTo x_9843 x_9842
    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_12921, x_12920) -> h_ConvertTo x_12921 x_12920
     1677| ConvertTo (x_9848, x_9847) -> h_ConvertTo x_9848 x_9847
    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_12926, x_12925) -> h_ConvertTo x_12926 x_12925
     1684| ConvertTo (x_9853, x_9852) -> h_ConvertTo x_9853 x_9852
    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_12931, x_12930) -> h_ConvertTo x_12931 x_12930
     1691| ConvertTo (x_9858, x_9857) -> h_ConvertTo x_9858 x_9857
    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_12936, x_12935) -> h_ConvertTo x_12936 x_12935
     1698| ConvertTo (x_9863, x_9862) -> h_ConvertTo x_9863 x_9862
    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_12941, x_12940) -> h_ConvertTo x_12941 x_12940
     1705| ConvertTo (x_9868, x_9867) -> h_ConvertTo x_9868 x_9867
    17121706
    17131707(** val convert_flag_inv_rect_Type4 :
     
    20432037    Obj.magic
    20442038      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
    2045         (fun eta29042 ->
    2046         let result = eta29042 in
     2039        (fun eta28663 ->
     2040        let result = eta28663 in
    20472041        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20482042        (fun _ ->
     
    22212215    List.map (fun idf -> { Types.fst = { Types.fst = idf.Types.fst;
    22222216      Types.snd = AST.Code }; Types.snd =
    2223       (Csyntax.type_of_fundef idf.Types.snd) }) p.AST.prog_funct
     2217      (Csyntax.type_of_fundef idf.Types.snd) }) (AST.prog_funct p)
    22242218  in
    22252219  let var_globals =
    22262220    List.map (fun v -> { Types.fst = { Types.fst = v.Types.fst.Types.fst;
    22272221      Types.snd = v.Types.fst.Types.snd }; Types.snd =
    2228       v.Types.snd.Types.snd }) p.AST.prog_vars
     2222      v.Types.snd.Types.snd }) (AST.prog_vars p)
    22292223  in
    22302224  let globals = List.append fun_globals var_globals in
     
    22382232              (fun f ->
    22392233              Obj.magic (Errors.OK { Types.fst = x.Types.fst; Types.snd =
    2240                 f })))) p.AST.prog_funct)) (fun fns ->
     2234                f })))) (AST.prog_funct p))) (fun fns ->
    22412235      Obj.magic (Errors.OK { AST.prog_vars =
    22422236        (List.map (fun v -> { Types.fst = v.Types.fst; Types.snd =
    2243           v.Types.snd.Types.fst }) p.AST.prog_vars); AST.prog_funct = fns;
    2244         AST.prog_main = p.AST.prog_main })))
    2245 
     2237          v.Types.snd.Types.fst }) (AST.prog_vars p)); AST.prog_funct = fns;
     2238        AST.prog_main = (AST.prog_main p) })))
     2239
Note: See TracChangeset for help on using the changeset viewer.