Changeset 2997 for extracted/toCminor.ml
 Timestamp:
 Mar 28, 2013, 10:27:41 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toCminor.ml
r2960 r2997 198 198 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 199 199 let rec var_type_rect_Type4 h_Global h_Stack h_Local = function 200  Global x_1 38 > h_Global x_138201  Stack x_1 39 > h_Stack x_139200  Global x_12720 > h_Global x_12720 201  Stack x_12721 > h_Stack x_12721 202 202  Local > h_Local 203 203 … … 205 205 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 206 206 let rec var_type_rect_Type5 h_Global h_Stack h_Local = function 207  Global x_1 44 > h_Global x_144208  Stack x_1 45 > h_Stack x_145207  Global x_12726 > h_Global x_12726 208  Stack x_12727 > h_Stack x_12727 209 209  Local > h_Local 210 210 … … 212 212 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 213 213 let rec var_type_rect_Type3 h_Global h_Stack h_Local = function 214  Global x_1 50 > h_Global x_150215  Stack x_1 51 > h_Stack x_151214  Global x_12732 > h_Global x_12732 215  Stack x_12733 > h_Stack x_12733 216 216  Local > h_Local 217 217 … … 219 219 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 220 220 let rec var_type_rect_Type2 h_Global h_Stack h_Local = function 221  Global x_1 56 > h_Global x_156222  Stack x_1 57 > h_Stack x_157221  Global x_12738 > h_Global x_12738 222  Stack x_12739 > h_Stack x_12739 223 223  Local > h_Local 224 224 … … 226 226 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 227 227 let rec var_type_rect_Type1 h_Global h_Stack h_Local = function 228  Global x_1 62 > h_Global x_162229  Stack x_1 63 > h_Stack x_163228  Global x_12744 > h_Global x_12744 229  Stack x_12745 > h_Stack x_12745 230 230  Local > h_Local 231 231 … … 233 233 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 234 234 let rec var_type_rect_Type0 h_Global h_Stack h_Local = function 235  Global x_1 68 > h_Global x_168236  Stack x_1 69 > h_Stack x_169235  Global x_12750 > h_Global x_12750 236  Stack x_12751 > h_Stack x_12751 237 237  Local > h_Local 238 238 … … 1221 1221 let rec destination_rect_Type4 vars h_IdDest h_MemDest = function 1222 1222  IdDest (id, ty) > h_IdDest id ty __ 1223  MemDest x_ 216 > h_MemDest x_2161223  MemDest x_12798 > h_MemDest x_12798 1224 1224 1225 1225 (** val destination_rect_Type5 : … … 1228 1228 let rec destination_rect_Type5 vars h_IdDest h_MemDest = function 1229 1229  IdDest (id, ty) > h_IdDest id ty __ 1230  MemDest x_ 221 > h_MemDest x_2211230  MemDest x_12803 > h_MemDest x_12803 1231 1231 1232 1232 (** val destination_rect_Type3 : … … 1235 1235 let rec destination_rect_Type3 vars h_IdDest h_MemDest = function 1236 1236  IdDest (id, ty) > h_IdDest id ty __ 1237  MemDest x_ 226 > h_MemDest x_2261237  MemDest x_12808 > h_MemDest x_12808 1238 1238 1239 1239 (** val destination_rect_Type2 : … … 1242 1242 let rec destination_rect_Type2 vars h_IdDest h_MemDest = function 1243 1243  IdDest (id, ty) > h_IdDest id ty __ 1244  MemDest x_ 231 > h_MemDest x_2311244  MemDest x_12813 > h_MemDest x_12813 1245 1245 1246 1246 (** val destination_rect_Type1 : … … 1249 1249 let rec destination_rect_Type1 vars h_IdDest h_MemDest = function 1250 1250  IdDest (id, ty) > h_IdDest id ty __ 1251  MemDest x_ 236 > h_MemDest x_2361251  MemDest x_12818 > h_MemDest x_12818 1252 1252 1253 1253 (** val destination_rect_Type0 : … … 1256 1256 let rec destination_rect_Type0 vars h_IdDest h_MemDest = function 1257 1257  IdDest (id, ty) > h_IdDest id ty __ 1258  MemDest x_ 241 > h_MemDest x_2411258  MemDest x_12823 > h_MemDest x_12823 1259 1259 1260 1260 (** val destination_inv_rect_Type4 : … … 1382 1382 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1383 1383 'a1) > labgen > 'a1 **) 1384 let rec labgen_rect_Type4 h_mk_labgen x_276 = 1385 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_276 1384 let rec labgen_rect_Type4 h_mk_labgen x_12858 = 1385 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1386 x_12858 1386 1387 in 1387 1388 h_mk_labgen labuniverse0 label_genlist0 __ … … 1390 1391 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1391 1392 'a1) > labgen > 'a1 **) 1392 let rec labgen_rect_Type5 h_mk_labgen x_278 = 1393 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_278 1393 let rec labgen_rect_Type5 h_mk_labgen x_12860 = 1394 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1395 x_12860 1394 1396 in 1395 1397 h_mk_labgen labuniverse0 label_genlist0 __ … … 1398 1400 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1399 1401 'a1) > labgen > 'a1 **) 1400 let rec labgen_rect_Type3 h_mk_labgen x_280 = 1401 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_280 1402 let rec labgen_rect_Type3 h_mk_labgen x_12862 = 1403 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1404 x_12862 1402 1405 in 1403 1406 h_mk_labgen labuniverse0 label_genlist0 __ … … 1406 1409 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1407 1410 'a1) > labgen > 'a1 **) 1408 let rec labgen_rect_Type2 h_mk_labgen x_282 = 1409 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_282 1411 let rec labgen_rect_Type2 h_mk_labgen x_12864 = 1412 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1413 x_12864 1410 1414 in 1411 1415 h_mk_labgen labuniverse0 label_genlist0 __ … … 1414 1418 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1415 1419 'a1) > labgen > 'a1 **) 1416 let rec labgen_rect_Type1 h_mk_labgen x_284 = 1417 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_284 1420 let rec labgen_rect_Type1 h_mk_labgen x_12866 = 1421 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1422 x_12866 1418 1423 in 1419 1424 h_mk_labgen labuniverse0 label_genlist0 __ … … 1422 1427 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1423 1428 'a1) > labgen > 'a1 **) 1424 let rec labgen_rect_Type0 h_mk_labgen x_286 = 1425 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_286 1429 let rec labgen_rect_Type0 h_mk_labgen x_12868 = 1430 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1431 x_12868 1426 1432 in 1427 1433 h_mk_labgen labuniverse0 label_genlist0 __ … … 1548 1554 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1549 1555 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_ 302in1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_12884 = 1557 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12884 in 1552 1558 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1553 1559 … … 1555 1561 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1556 1562 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_ 304in1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_12886 = 1564 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12886 in 1559 1565 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1560 1566 … … 1562 1568 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1563 1569 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_ 306in1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_12888 = 1571 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12888 in 1566 1572 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1567 1573 … … 1569 1575 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1570 1576 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_ 308in1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_12890 = 1578 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12890 in 1573 1579 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1574 1580 … … 1576 1582 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1577 1583 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_ 310in1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_12892 = 1585 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12892 in 1580 1586 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1581 1587 … … 1583 1589 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1584 1590 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_ 312in1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_12894 = 1592 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_12894 in 1587 1593 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1588 1594 … … 1668 1674 let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function 1669 1675  DoNotConvert > h_DoNotConvert 1670  ConvertTo (x_ 334, x_333) > h_ConvertTo x_334 x_3331676  ConvertTo (x_12916, x_12915) > h_ConvertTo x_12916 x_12915 1671 1677 1672 1678 (** val convert_flag_rect_Type5 : … … 1675 1681 let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function 1676 1682  DoNotConvert > h_DoNotConvert 1677  ConvertTo (x_ 339, x_338) > h_ConvertTo x_339 x_3381683  ConvertTo (x_12921, x_12920) > h_ConvertTo x_12921 x_12920 1678 1684 1679 1685 (** val convert_flag_rect_Type3 : … … 1682 1688 let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function 1683 1689  DoNotConvert > h_DoNotConvert 1684  ConvertTo (x_ 344, x_343) > h_ConvertTo x_344 x_3431690  ConvertTo (x_12926, x_12925) > h_ConvertTo x_12926 x_12925 1685 1691 1686 1692 (** val convert_flag_rect_Type2 : … … 1689 1695 let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function 1690 1696  DoNotConvert > h_DoNotConvert 1691  ConvertTo (x_ 349, x_348) > h_ConvertTo x_349 x_3481697  ConvertTo (x_12931, x_12930) > h_ConvertTo x_12931 x_12930 1692 1698 1693 1699 (** val convert_flag_rect_Type1 : … … 1696 1702 let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function 1697 1703  DoNotConvert > h_DoNotConvert 1698  ConvertTo (x_ 354, x_353) > h_ConvertTo x_354 x_3531704  ConvertTo (x_12936, x_12935) > h_ConvertTo x_12936 x_12935 1699 1705 1700 1706 (** val convert_flag_rect_Type0 : … … 1703 1709 let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function 1704 1710  DoNotConvert > h_DoNotConvert 1705  ConvertTo (x_ 359, x_358) > h_ConvertTo x_359 x_3581711  ConvertTo (x_12941, x_12940) > h_ConvertTo x_12941 x_12940 1706 1712 1707 1713 (** val convert_flag_inv_rect_Type4 : … … 2037 2043 Obj.magic 2038 2044 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su) 2039 (fun eta 650>2040 let result = eta 650in2045 (fun eta29042 > 2046 let result = eta29042 in 2041 2047 (let { Types.fst = fgens1; Types.snd = s0 } = result in 2042 2048 (fun _ >
Note: See TracChangeset
for help on using the changeset viewer.