Changeset 2775 for extracted/toCminor.ml
 Timestamp:
 Mar 5, 2013, 9:52:39 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toCminor.ml
r2773 r2775 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_ 8081 > h_Global x_8081201  Stack x_ 8082 > h_Stack x_8082200  Global x_12912 > h_Global x_12912 201  Stack x_12913 > h_Stack x_12913 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_ 8087 > h_Global x_8087208  Stack x_ 8088 > h_Stack x_8088207  Global x_12918 > h_Global x_12918 208  Stack x_12919 > h_Stack x_12919 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_ 8093 > h_Global x_8093215  Stack x_ 8094 > h_Stack x_8094214  Global x_12924 > h_Global x_12924 215  Stack x_12925 > h_Stack x_12925 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_ 8099 > h_Global x_8099222  Stack x_ 8100 > h_Stack x_8100221  Global x_12930 > h_Global x_12930 222  Stack x_12931 > h_Stack x_12931 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_ 8105 > h_Global x_8105229  Stack x_ 8106 > h_Stack x_8106228  Global x_12936 > h_Global x_12936 229  Stack x_12937 > h_Stack x_12937 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_ 8111 > h_Global x_8111236  Stack x_ 8112 > h_Stack x_8112235  Global x_12942 > h_Global x_12942 236  Stack x_12943 > h_Stack x_12943 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_ 9567 > h_MemDest x_95671223  MemDest x_14398 > h_MemDest x_14398 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_ 9572 > h_MemDest x_95721230  MemDest x_14403 > h_MemDest x_14403 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_ 9577 > h_MemDest x_95771237  MemDest x_14408 > h_MemDest x_14408 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_ 9582 > h_MemDest x_95821244  MemDest x_14413 > h_MemDest x_14413 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_ 9587 > h_MemDest x_95871251  MemDest x_14418 > h_MemDest x_14418 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_ 9592 > h_MemDest x_95921258  MemDest x_14423 > h_MemDest x_14423 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_9627 = 1385 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9627 1384 let rec labgen_rect_Type4 h_mk_labgen x_14458 = 1385 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1386 x_14458 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_9629 = 1393 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9629 1393 let rec labgen_rect_Type5 h_mk_labgen x_14460 = 1394 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1395 x_14460 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_9631 = 1401 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9631 1402 let rec labgen_rect_Type3 h_mk_labgen x_14462 = 1403 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1404 x_14462 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_9633 = 1409 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9633 1411 let rec labgen_rect_Type2 h_mk_labgen x_14464 = 1412 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1413 x_14464 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_9635 = 1417 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9635 1420 let rec labgen_rect_Type1 h_mk_labgen x_14466 = 1421 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1422 x_14466 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_9637 = 1425 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9637 1429 let rec labgen_rect_Type0 h_mk_labgen x_14468 = 1430 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1431 x_14468 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_ 9653=1551 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 9653in1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14484 = 1557 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14484 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_ 9655=1558 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 9655in1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14486 = 1564 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14486 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_ 9657=1565 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 9657in1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14488 = 1571 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14488 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_ 9659=1572 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 9659in1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14490 = 1578 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14490 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_ 9661=1579 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 9661in1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14492 = 1585 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14492 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_ 9663=1586 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 9663in1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14494 = 1592 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14494 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_ 9685, x_9684) > h_ConvertTo x_9685 x_96841676  ConvertTo (x_14516, x_14515) > h_ConvertTo x_14516 x_14515 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_ 9690, x_9689) > h_ConvertTo x_9690 x_96891683  ConvertTo (x_14521, x_14520) > h_ConvertTo x_14521 x_14520 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_ 9695, x_9694) > h_ConvertTo x_9695 x_96941690  ConvertTo (x_14526, x_14525) > h_ConvertTo x_14526 x_14525 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_ 9700, x_9699) > h_ConvertTo x_9700 x_96991697  ConvertTo (x_14531, x_14530) > h_ConvertTo x_14531 x_14530 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_ 9705, x_9704) > h_ConvertTo x_9705 x_97041704  ConvertTo (x_14536, x_14535) > h_ConvertTo x_14536 x_14535 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_ 9710, x_9709) > h_ConvertTo x_9710 x_97091711  ConvertTo (x_14541, x_14540) > h_ConvertTo x_14541 x_14540 1706 1712 1707 1713 (** val convert_flag_inv_rect_Type4 : … … 2026 2032 Obj.magic 2027 2033 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su) 2028 (fun eta 1212>2029 let result = eta 1212in2034 (fun eta2434 > 2035 let result = eta2434 in 2030 2036 (let { Types.fst = fgens1; Types.snd = s0 } = result in 2031 2037 (fun _ >
Note: See TracChangeset
for help on using the changeset viewer.