Changeset 2717 for extracted/toCminor.ml
 Timestamp:
 Feb 23, 2013, 1:16:55 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toCminor.ml
r2649 r2717 1 1 open Preamble 2 2 3 open BitVectorTrie 4 3 5 open CostLabel 4 6 … … 30 32 31 33 open Identifiers 34 35 open Exp 32 36 33 37 open Arithmetic … … 196 200 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 197 201 let rec var_type_rect_Type4 h_Global h_Stack h_Local = function 198  Global x_1 1147 > h_Global x_11147199  Stack x_1 1148 > h_Stack x_11148202  Global x_12977 > h_Global x_12977 203  Stack x_12978 > h_Stack x_12978 200 204  Local > h_Local 201 205 … … 203 207 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 204 208 let rec var_type_rect_Type5 h_Global h_Stack h_Local = function 205  Global x_1 1153 > h_Global x_11153206  Stack x_1 1154 > h_Stack x_11154209  Global x_12983 > h_Global x_12983 210  Stack x_12984 > h_Stack x_12984 207 211  Local > h_Local 208 212 … … 210 214 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 211 215 let rec var_type_rect_Type3 h_Global h_Stack h_Local = function 212  Global x_1 1159 > h_Global x_11159213  Stack x_1 1160 > h_Stack x_11160216  Global x_12989 > h_Global x_12989 217  Stack x_12990 > h_Stack x_12990 214 218  Local > h_Local 215 219 … … 217 221 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 218 222 let rec var_type_rect_Type2 h_Global h_Stack h_Local = function 219  Global x_1 1165 > h_Global x_11165220  Stack x_1 1166 > h_Stack x_11166223  Global x_12995 > h_Global x_12995 224  Stack x_12996 > h_Stack x_12996 221 225  Local > h_Local 222 226 … … 224 228 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 225 229 let rec var_type_rect_Type1 h_Global h_Stack h_Local = function 226  Global x_1 1171 > h_Global x_11171227  Stack x_1 1172 > h_Stack x_11172230  Global x_13001 > h_Global x_13001 231  Stack x_13002 > h_Stack x_13002 228 232  Local > h_Local 229 233 … … 231 235 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 232 236 let rec var_type_rect_Type0 h_Global h_Stack h_Local = function 233  Global x_1 1177 > h_Global x_11177234  Stack x_1 1178 > h_Stack x_11178237  Global x_13007 > h_Global x_13007 238  Stack x_13008 > h_Stack x_13008 235 239  Local > h_Local 236 240 … … 1219 1223 let rec destination_rect_Type4 vars h_IdDest h_MemDest = function 1220 1224  IdDest (id, ty) > h_IdDest id ty __ 1221  MemDest x_1 1225 > h_MemDest x_112251225  MemDest x_14463 > h_MemDest x_14463 1222 1226 1223 1227 (** val destination_rect_Type5 : … … 1226 1230 let rec destination_rect_Type5 vars h_IdDest h_MemDest = function 1227 1231  IdDest (id, ty) > h_IdDest id ty __ 1228  MemDest x_1 1230 > h_MemDest x_112301232  MemDest x_14468 > h_MemDest x_14468 1229 1233 1230 1234 (** val destination_rect_Type3 : … … 1233 1237 let rec destination_rect_Type3 vars h_IdDest h_MemDest = function 1234 1238  IdDest (id, ty) > h_IdDest id ty __ 1235  MemDest x_1 1235 > h_MemDest x_112351239  MemDest x_14473 > h_MemDest x_14473 1236 1240 1237 1241 (** val destination_rect_Type2 : … … 1240 1244 let rec destination_rect_Type2 vars h_IdDest h_MemDest = function 1241 1245  IdDest (id, ty) > h_IdDest id ty __ 1242  MemDest x_1 1240 > h_MemDest x_112401246  MemDest x_14478 > h_MemDest x_14478 1243 1247 1244 1248 (** val destination_rect_Type1 : … … 1247 1251 let rec destination_rect_Type1 vars h_IdDest h_MemDest = function 1248 1252  IdDest (id, ty) > h_IdDest id ty __ 1249  MemDest x_1 1245 > h_MemDest x_112451253  MemDest x_14483 > h_MemDest x_14483 1250 1254 1251 1255 (** val destination_rect_Type0 : … … 1254 1258 let rec destination_rect_Type0 vars h_IdDest h_MemDest = function 1255 1259  IdDest (id, ty) > h_IdDest id ty __ 1256  MemDest x_1 1250 > h_MemDest x_112501260  MemDest x_14488 > h_MemDest x_14488 1257 1261 1258 1262 (** val destination_inv_rect_Type4 : … … 1382 1386 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1383 1387 'a1) > labgen > 'a1 **) 1384 let rec labgen_rect_Type4 h_mk_labgen x_1 1285=1388 let rec labgen_rect_Type4 h_mk_labgen x_14523 = 1385 1389 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1386 x_1 12851390 x_14523 1387 1391 in 1388 1392 h_mk_labgen labuniverse0 label_genlist0 __ … … 1391 1395 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1392 1396 'a1) > labgen > 'a1 **) 1393 let rec labgen_rect_Type5 h_mk_labgen x_1 1287=1397 let rec labgen_rect_Type5 h_mk_labgen x_14525 = 1394 1398 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1395 x_1 12871399 x_14525 1396 1400 in 1397 1401 h_mk_labgen labuniverse0 label_genlist0 __ … … 1400 1404 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1401 1405 'a1) > labgen > 'a1 **) 1402 let rec labgen_rect_Type3 h_mk_labgen x_1 1289=1406 let rec labgen_rect_Type3 h_mk_labgen x_14527 = 1403 1407 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1404 x_1 12891408 x_14527 1405 1409 in 1406 1410 h_mk_labgen labuniverse0 label_genlist0 __ … … 1409 1413 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1410 1414 'a1) > labgen > 'a1 **) 1411 let rec labgen_rect_Type2 h_mk_labgen x_1 1291=1415 let rec labgen_rect_Type2 h_mk_labgen x_14529 = 1412 1416 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1413 x_1 12911417 x_14529 1414 1418 in 1415 1419 h_mk_labgen labuniverse0 label_genlist0 __ … … 1418 1422 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1419 1423 'a1) > labgen > 'a1 **) 1420 let rec labgen_rect_Type1 h_mk_labgen x_1 1293=1424 let rec labgen_rect_Type1 h_mk_labgen x_14531 = 1421 1425 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1422 x_1 12931426 x_14531 1423 1427 in 1424 1428 h_mk_labgen labuniverse0 label_genlist0 __ … … 1427 1431 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1428 1432 'a1) > labgen > 'a1 **) 1429 let rec labgen_rect_Type0 h_mk_labgen x_1 1295=1433 let rec labgen_rect_Type0 h_mk_labgen x_14533 = 1430 1434 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1431 x_1 12951435 x_14533 1432 1436 in 1433 1437 h_mk_labgen labuniverse0 label_genlist0 __ … … 1554 1558 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1555 1559 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_1 1311=1557 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_1 1311in1560 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14549 = 1561 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14549 in 1558 1562 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1559 1563 … … 1561 1565 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1562 1566 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_1 1313=1564 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_1 1313in1567 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14551 = 1568 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14551 in 1565 1569 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1566 1570 … … 1568 1572 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1569 1573 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_1 1315=1571 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_1 1315in1574 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14553 = 1575 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14553 in 1572 1576 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1573 1577 … … 1575 1579 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1576 1580 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_1 1317=1578 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_1 1317in1581 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14555 = 1582 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14555 in 1579 1583 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1580 1584 … … 1582 1586 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1583 1587 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_1 1319=1585 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_1 1319in1588 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14557 = 1589 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14557 in 1586 1590 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1587 1591 … … 1589 1593 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1590 1594 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_1 1321=1592 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_1 1321in1595 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14559 = 1596 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14559 in 1593 1597 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1594 1598 … … 1674 1678 let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function 1675 1679  DoNotConvert > h_DoNotConvert 1676  ConvertTo (x_1 1343, x_11342) > h_ConvertTo x_11343 x_113421680  ConvertTo (x_14581, x_14580) > h_ConvertTo x_14581 x_14580 1677 1681 1678 1682 (** val convert_flag_rect_Type5 : … … 1681 1685 let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function 1682 1686  DoNotConvert > h_DoNotConvert 1683  ConvertTo (x_1 1348, x_11347) > h_ConvertTo x_11348 x_113471687  ConvertTo (x_14586, x_14585) > h_ConvertTo x_14586 x_14585 1684 1688 1685 1689 (** val convert_flag_rect_Type3 : … … 1688 1692 let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function 1689 1693  DoNotConvert > h_DoNotConvert 1690  ConvertTo (x_1 1353, x_11352) > h_ConvertTo x_11353 x_113521694  ConvertTo (x_14591, x_14590) > h_ConvertTo x_14591 x_14590 1691 1695 1692 1696 (** val convert_flag_rect_Type2 : … … 1695 1699 let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function 1696 1700  DoNotConvert > h_DoNotConvert 1697  ConvertTo (x_1 1358, x_11357) > h_ConvertTo x_11358 x_113571701  ConvertTo (x_14596, x_14595) > h_ConvertTo x_14596 x_14595 1698 1702 1699 1703 (** val convert_flag_rect_Type1 : … … 1702 1706 let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function 1703 1707  DoNotConvert > h_DoNotConvert 1704  ConvertTo (x_1 1363, x_11362) > h_ConvertTo x_11363 x_113621708  ConvertTo (x_14601, x_14600) > h_ConvertTo x_14601 x_14600 1705 1709 1706 1710 (** val convert_flag_rect_Type0 : … … 1709 1713 let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function 1710 1714  DoNotConvert > h_DoNotConvert 1711  ConvertTo (x_1 1368, x_11367) > h_ConvertTo x_11368 x_113671715  ConvertTo (x_14606, x_14605) > h_ConvertTo x_14606 x_14605 1712 1716 1713 1717 (** val convert_flag_inv_rect_Type4 : … … 2032 2036 Obj.magic 2033 2037 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su) 2034 (fun eta 1273>2035 let result = eta 1273in2038 (fun eta2862 > 2039 let result = eta2862 in 2036 2040 (let { Types.fst = fgens1; Types.snd = s0 } = result in 2037 2041 (fun _ >
Note: See TracChangeset
for help on using the changeset viewer.