Changeset 2997 for extracted/toCminor.ml


Ignore:
Timestamp:
Mar 28, 2013, 10:27:41 AM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/toCminor.ml

    r2960 r2997  
    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_138 -> h_Global x_138
    201 | Stack x_139 -> h_Stack x_139
     200| Global x_12720 -> h_Global x_12720
     201| Stack x_12721 -> h_Stack x_12721
    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_144 -> h_Global x_144
    208 | Stack x_145 -> h_Stack x_145
     207| Global x_12726 -> h_Global x_12726
     208| Stack x_12727 -> h_Stack x_12727
    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_150 -> h_Global x_150
    215 | Stack x_151 -> h_Stack x_151
     214| Global x_12732 -> h_Global x_12732
     215| Stack x_12733 -> h_Stack x_12733
    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_156 -> h_Global x_156
    222 | Stack x_157 -> h_Stack x_157
     221| Global x_12738 -> h_Global x_12738
     222| Stack x_12739 -> h_Stack x_12739
    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_162 -> h_Global x_162
    229 | Stack x_163 -> h_Stack x_163
     228| Global x_12744 -> h_Global x_12744
     229| Stack x_12745 -> h_Stack x_12745
    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_168 -> h_Global x_168
    236 | Stack x_169 -> h_Stack x_169
     235| Global x_12750 -> h_Global x_12750
     236| Stack x_12751 -> h_Stack x_12751
    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_216 -> h_MemDest x_216
     1223| MemDest x_12798 -> h_MemDest x_12798
    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_221 -> h_MemDest x_221
     1230| MemDest x_12803 -> h_MemDest x_12803
    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_226 -> h_MemDest x_226
     1237| MemDest x_12808 -> h_MemDest x_12808
    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_231 -> h_MemDest x_231
     1244| MemDest x_12813 -> h_MemDest x_12813
    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_236 -> h_MemDest x_236
     1251| MemDest x_12818 -> h_MemDest x_12818
    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_241 -> h_MemDest x_241
     1258| MemDest x_12823 -> h_MemDest x_12823
    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_276 =
    1385   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_276
     1384let rec labgen_rect_Type4 h_mk_labgen x_12858 =
     1385  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1386    x_12858
    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_278 =
    1393   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_278
     1393let rec labgen_rect_Type5 h_mk_labgen x_12860 =
     1394  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1395    x_12860
    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_280 =
    1401   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_280
     1402let rec labgen_rect_Type3 h_mk_labgen x_12862 =
     1403  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1404    x_12862
    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_282 =
    1409   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_282
     1411let rec labgen_rect_Type2 h_mk_labgen x_12864 =
     1412  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1413    x_12864
    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_284 =
    1417   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_284
     1420let rec labgen_rect_Type1 h_mk_labgen x_12866 =
     1421  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1422    x_12866
    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_286 =
    1425   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_286
     1429let rec labgen_rect_Type0 h_mk_labgen x_12868 =
     1430  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
     1431    x_12868
    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_302 =
    1551   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_302 in
     1556let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_12884 =
     1557  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12884 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_304 =
    1558   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_304 in
     1563let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_12886 =
     1564  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12886 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_306 =
    1565   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_306 in
     1570let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_12888 =
     1571  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12888 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_308 =
    1572   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_308 in
     1577let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_12890 =
     1578  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12890 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_310 =
    1579   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_310 in
     1584let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_12892 =
     1585  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12892 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_312 =
    1586   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_312 in
     1591let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_12894 =
     1592  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12894 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_334, x_333) -> h_ConvertTo x_334 x_333
     1676| ConvertTo (x_12916, x_12915) -> h_ConvertTo x_12916 x_12915
    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_339, x_338) -> h_ConvertTo x_339 x_338
     1683| ConvertTo (x_12921, x_12920) -> h_ConvertTo x_12921 x_12920
    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_344, x_343) -> h_ConvertTo x_344 x_343
     1690| ConvertTo (x_12926, x_12925) -> h_ConvertTo x_12926 x_12925
    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_349, x_348) -> h_ConvertTo x_349 x_348
     1697| ConvertTo (x_12931, x_12930) -> h_ConvertTo x_12931 x_12930
    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_354, x_353) -> h_ConvertTo x_354 x_353
     1704| ConvertTo (x_12936, x_12935) -> h_ConvertTo x_12936 x_12935
    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_359, x_358) -> h_ConvertTo x_359 x_358
     1711| ConvertTo (x_12941, x_12940) -> h_ConvertTo x_12941 x_12940
    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 eta650 ->
    2040         let result = eta650 in
     2045        (fun eta29042 ->
     2046        let result = eta29042 in
    20412047        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20422048        (fun _ ->
Note: See TracChangeset for help on using the changeset viewer.