Changeset 2951 for extracted/toCminor.ml
 Timestamp:
 Mar 25, 2013, 11:30:01 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toCminor.ml
r2890 r2951 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_130 42 > h_Global x_13042201  Stack x_130 43 > h_Stack x_13043200  Global x_13081 > h_Global x_13081 201  Stack x_13082 > h_Stack x_13082 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_130 48 > h_Global x_13048208  Stack x_130 49 > h_Stack x_13049207  Global x_13087 > h_Global x_13087 208  Stack x_13088 > h_Stack x_13088 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_130 54 > h_Global x_13054215  Stack x_130 55 > h_Stack x_13055214  Global x_13093 > h_Global x_13093 215  Stack x_13094 > h_Stack x_13094 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_130 60 > h_Global x_13060222  Stack x_13 061 > h_Stack x_13061221  Global x_13099 > h_Global x_13099 222  Stack x_13100 > h_Stack x_13100 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_13 066 > h_Global x_13066229  Stack x_13 067 > h_Stack x_13067228  Global x_13105 > h_Global x_13105 229  Stack x_13106 > h_Stack x_13106 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_13 072 > h_Global x_13072236  Stack x_13 073 > h_Stack x_13073235  Global x_13111 > h_Global x_13111 236  Stack x_13112 > h_Stack x_13112 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_145 28 > h_MemDest x_145281223  MemDest x_14567 > h_MemDest x_14567 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_145 33 > h_MemDest x_145331230  MemDest x_14572 > h_MemDest x_14572 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_145 38 > h_MemDest x_145381237  MemDest x_14577 > h_MemDest x_14577 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_145 43 > h_MemDest x_145431244  MemDest x_14582 > h_MemDest x_14582 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_145 48 > h_MemDest x_145481251  MemDest x_14587 > h_MemDest x_14587 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_145 53 > h_MemDest x_145531258  MemDest x_14592 > h_MemDest x_14592 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_14 588=1384 let rec labgen_rect_Type4 h_mk_labgen x_14627 = 1385 1385 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1386 x_14 5881386 x_14627 1387 1387 in 1388 1388 h_mk_labgen labuniverse0 label_genlist0 __ … … 1391 1391 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1392 1392 'a1) > labgen > 'a1 **) 1393 let rec labgen_rect_Type5 h_mk_labgen x_14 590=1393 let rec labgen_rect_Type5 h_mk_labgen x_14629 = 1394 1394 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1395 x_14 5901395 x_14629 1396 1396 in 1397 1397 h_mk_labgen labuniverse0 label_genlist0 __ … … 1400 1400 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1401 1401 'a1) > labgen > 'a1 **) 1402 let rec labgen_rect_Type3 h_mk_labgen x_14 592=1402 let rec labgen_rect_Type3 h_mk_labgen x_14631 = 1403 1403 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1404 x_14 5921404 x_14631 1405 1405 in 1406 1406 h_mk_labgen labuniverse0 label_genlist0 __ … … 1409 1409 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1410 1410 'a1) > labgen > 'a1 **) 1411 let rec labgen_rect_Type2 h_mk_labgen x_14 594=1411 let rec labgen_rect_Type2 h_mk_labgen x_14633 = 1412 1412 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1413 x_14 5941413 x_14633 1414 1414 in 1415 1415 h_mk_labgen labuniverse0 label_genlist0 __ … … 1418 1418 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1419 1419 'a1) > labgen > 'a1 **) 1420 let rec labgen_rect_Type1 h_mk_labgen x_14 596=1420 let rec labgen_rect_Type1 h_mk_labgen x_14635 = 1421 1421 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1422 x_14 5961422 x_14635 1423 1423 in 1424 1424 h_mk_labgen labuniverse0 label_genlist0 __ … … 1427 1427 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1428 1428 'a1) > labgen > 'a1 **) 1429 let rec labgen_rect_Type0 h_mk_labgen x_14 598=1429 let rec labgen_rect_Type0 h_mk_labgen x_14637 = 1430 1430 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1431 x_14 5981431 x_14637 1432 1432 in 1433 1433 h_mk_labgen labuniverse0 label_genlist0 __ … … 1554 1554 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1555 1555 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_146 14=1557 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_146 14in1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14653 = 1557 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14653 in 1558 1558 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1559 1559 … … 1561 1561 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1562 1562 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_146 16=1564 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_146 16in1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14655 = 1564 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14655 in 1565 1565 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1566 1566 … … 1568 1568 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1569 1569 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_146 18=1571 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_146 18in1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14657 = 1571 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14657 in 1572 1572 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1573 1573 … … 1575 1575 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1576 1576 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_146 20=1578 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_146 20in1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14659 = 1578 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14659 in 1579 1579 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1580 1580 … … 1582 1582 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1583 1583 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_146 22=1585 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_146 22in1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14661 = 1585 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14661 in 1586 1586 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1587 1587 … … 1589 1589 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1590 1590 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_146 24=1592 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_146 24in1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14663 = 1592 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14663 in 1593 1593 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1594 1594 … … 1674 1674 let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function 1675 1675  DoNotConvert > h_DoNotConvert 1676  ConvertTo (x_146 46, x_14645) > h_ConvertTo x_14646 x_146451676  ConvertTo (x_14685, x_14684) > h_ConvertTo x_14685 x_14684 1677 1677 1678 1678 (** val convert_flag_rect_Type5 : … … 1681 1681 let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function 1682 1682  DoNotConvert > h_DoNotConvert 1683  ConvertTo (x_146 51, x_14650) > h_ConvertTo x_14651 x_146501683  ConvertTo (x_14690, x_14689) > h_ConvertTo x_14690 x_14689 1684 1684 1685 1685 (** val convert_flag_rect_Type3 : … … 1688 1688 let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function 1689 1689  DoNotConvert > h_DoNotConvert 1690  ConvertTo (x_146 56, x_14655) > h_ConvertTo x_14656 x_146551690  ConvertTo (x_14695, x_14694) > h_ConvertTo x_14695 x_14694 1691 1691 1692 1692 (** val convert_flag_rect_Type2 : … … 1695 1695 let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function 1696 1696  DoNotConvert > h_DoNotConvert 1697  ConvertTo (x_14 661, x_14660) > h_ConvertTo x_14661 x_146601697  ConvertTo (x_14700, x_14699) > h_ConvertTo x_14700 x_14699 1698 1698 1699 1699 (** val convert_flag_rect_Type1 : … … 1702 1702 let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function 1703 1703  DoNotConvert > h_DoNotConvert 1704  ConvertTo (x_14 666, x_14665) > h_ConvertTo x_14666 x_146651704  ConvertTo (x_14705, x_14704) > h_ConvertTo x_14705 x_14704 1705 1705 1706 1706 (** val convert_flag_rect_Type0 : … … 1709 1709 let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function 1710 1710  DoNotConvert > h_DoNotConvert 1711  ConvertTo (x_14 671, x_14670) > h_ConvertTo x_14671 x_146701711  ConvertTo (x_14710, x_14709) > h_ConvertTo x_14710 x_14709 1712 1712 1713 1713 (** val convert_flag_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.