Changeset 2743 for extracted/toCminor.ml
 Timestamp:
 Feb 27, 2013, 9:27:58 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toCminor.ml
r2730 r2743 200 200 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 201 201 let rec var_type_rect_Type4 h_Global h_Stack h_Local = function 202  Global x_ 4448 > h_Global x_4448203  Stack x_ 4449 > h_Stack x_4449202  Global x_13003 > h_Global x_13003 203  Stack x_13004 > h_Stack x_13004 204 204  Local > h_Local 205 205 … … 207 207 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 208 208 let rec var_type_rect_Type5 h_Global h_Stack h_Local = function 209  Global x_ 4454 > h_Global x_4454210  Stack x_ 4455 > h_Stack x_4455209  Global x_13009 > h_Global x_13009 210  Stack x_13010 > h_Stack x_13010 211 211  Local > h_Local 212 212 … … 214 214 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 215 215 let rec var_type_rect_Type3 h_Global h_Stack h_Local = function 216  Global x_ 4460 > h_Global x_4460217  Stack x_ 4461 > h_Stack x_4461216  Global x_13015 > h_Global x_13015 217  Stack x_13016 > h_Stack x_13016 218 218  Local > h_Local 219 219 … … 221 221 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 222 222 let rec var_type_rect_Type2 h_Global h_Stack h_Local = function 223  Global x_ 4466 > h_Global x_4466224  Stack x_ 4467 > h_Stack x_4467223  Global x_13021 > h_Global x_13021 224  Stack x_13022 > h_Stack x_13022 225 225  Local > h_Local 226 226 … … 228 228 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 229 229 let rec var_type_rect_Type1 h_Global h_Stack h_Local = function 230  Global x_ 4472 > h_Global x_4472231  Stack x_ 4473 > h_Stack x_4473230  Global x_13027 > h_Global x_13027 231  Stack x_13028 > h_Stack x_13028 232 232  Local > h_Local 233 233 … … 235 235 (AST.region > 'a1) > (Nat.nat > 'a1) > 'a1 > var_type > 'a1 **) 236 236 let rec var_type_rect_Type0 h_Global h_Stack h_Local = function 237  Global x_ 4478 > h_Global x_4478238  Stack x_ 4479 > h_Stack x_4479237  Global x_13033 > h_Global x_13033 238  Stack x_13034 > h_Stack x_13034 239 239  Local > h_Local 240 240 … … 1223 1223 let rec destination_rect_Type4 vars h_IdDest h_MemDest = function 1224 1224  IdDest (id, ty) > h_IdDest id ty __ 1225  MemDest x_ 4526 > h_MemDest x_45261225  MemDest x_14489 > h_MemDest x_14489 1226 1226 1227 1227 (** val destination_rect_Type5 : … … 1230 1230 let rec destination_rect_Type5 vars h_IdDest h_MemDest = function 1231 1231  IdDest (id, ty) > h_IdDest id ty __ 1232  MemDest x_ 4531 > h_MemDest x_45311232  MemDest x_14494 > h_MemDest x_14494 1233 1233 1234 1234 (** val destination_rect_Type3 : … … 1237 1237 let rec destination_rect_Type3 vars h_IdDest h_MemDest = function 1238 1238  IdDest (id, ty) > h_IdDest id ty __ 1239  MemDest x_ 4536 > h_MemDest x_45361239  MemDest x_14499 > h_MemDest x_14499 1240 1240 1241 1241 (** val destination_rect_Type2 : … … 1244 1244 let rec destination_rect_Type2 vars h_IdDest h_MemDest = function 1245 1245  IdDest (id, ty) > h_IdDest id ty __ 1246  MemDest x_ 4541 > h_MemDest x_45411246  MemDest x_14504 > h_MemDest x_14504 1247 1247 1248 1248 (** val destination_rect_Type1 : … … 1251 1251 let rec destination_rect_Type1 vars h_IdDest h_MemDest = function 1252 1252  IdDest (id, ty) > h_IdDest id ty __ 1253  MemDest x_ 4546 > h_MemDest x_45461253  MemDest x_14509 > h_MemDest x_14509 1254 1254 1255 1255 (** val destination_rect_Type0 : … … 1258 1258 let rec destination_rect_Type0 vars h_IdDest h_MemDest = function 1259 1259  IdDest (id, ty) > h_IdDest id ty __ 1260  MemDest x_ 4551 > h_MemDest x_45511260  MemDest x_14514 > h_MemDest x_14514 1261 1261 1262 1262 (** val destination_inv_rect_Type4 : … … 1386 1386 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1387 1387 'a1) > labgen > 'a1 **) 1388 let rec labgen_rect_Type4 h_mk_labgen x_4586 = 1389 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_4586 1388 let rec labgen_rect_Type4 h_mk_labgen x_14549 = 1389 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1390 x_14549 1390 1391 in 1391 1392 h_mk_labgen labuniverse0 label_genlist0 __ … … 1394 1395 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1395 1396 'a1) > labgen > 'a1 **) 1396 let rec labgen_rect_Type5 h_mk_labgen x_4588 = 1397 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_4588 1397 let rec labgen_rect_Type5 h_mk_labgen x_14551 = 1398 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1399 x_14551 1398 1400 in 1399 1401 h_mk_labgen labuniverse0 label_genlist0 __ … … 1402 1404 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1403 1405 'a1) > labgen > 'a1 **) 1404 let rec labgen_rect_Type3 h_mk_labgen x_4590 = 1405 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_4590 1406 let rec labgen_rect_Type3 h_mk_labgen x_14553 = 1407 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1408 x_14553 1406 1409 in 1407 1410 h_mk_labgen labuniverse0 label_genlist0 __ … … 1410 1413 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1411 1414 'a1) > labgen > 'a1 **) 1412 let rec labgen_rect_Type2 h_mk_labgen x_4592 = 1413 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_4592 1415 let rec labgen_rect_Type2 h_mk_labgen x_14555 = 1416 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1417 x_14555 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_4594 = 1421 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_4594 1424 let rec labgen_rect_Type1 h_mk_labgen x_14557 = 1425 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1426 x_14557 1422 1427 in 1423 1428 h_mk_labgen labuniverse0 label_genlist0 __ … … 1426 1431 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1427 1432 'a1) > labgen > 'a1 **) 1428 let rec labgen_rect_Type0 h_mk_labgen x_4596 = 1429 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_4596 1433 let rec labgen_rect_Type0 h_mk_labgen x_14559 = 1434 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1435 x_14559 1430 1436 in 1431 1437 h_mk_labgen labuniverse0 label_genlist0 __ … … 1552 1558 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1553 1559 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1554 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_ 4612=1555 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 4612in1560 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14575 = 1561 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14575 in 1556 1562 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1557 1563 … … 1559 1565 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1560 1566 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1561 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_ 4614=1562 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 4614in1567 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14577 = 1568 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14577 in 1563 1569 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1564 1570 … … 1566 1572 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1567 1573 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1568 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_ 4616=1569 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 4616in1574 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14579 = 1575 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14579 in 1570 1576 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1571 1577 … … 1573 1579 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1574 1580 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1575 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_ 4618=1576 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 4618in1581 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14581 = 1582 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14581 in 1577 1583 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1578 1584 … … 1580 1586 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1581 1587 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1582 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_ 4620=1583 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 4620in1588 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14583 = 1589 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14583 in 1584 1590 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1585 1591 … … 1587 1593 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1588 1594 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1589 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_ 4622=1590 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 4622in1595 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14585 = 1596 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14585 in 1591 1597 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1592 1598 … … 1672 1678 let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function 1673 1679  DoNotConvert > h_DoNotConvert 1674  ConvertTo (x_ 4644, x_4643) > h_ConvertTo x_4644 x_46431680  ConvertTo (x_14607, x_14606) > h_ConvertTo x_14607 x_14606 1675 1681 1676 1682 (** val convert_flag_rect_Type5 : … … 1679 1685 let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function 1680 1686  DoNotConvert > h_DoNotConvert 1681  ConvertTo (x_ 4649, x_4648) > h_ConvertTo x_4649 x_46481687  ConvertTo (x_14612, x_14611) > h_ConvertTo x_14612 x_14611 1682 1688 1683 1689 (** val convert_flag_rect_Type3 : … … 1686 1692 let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function 1687 1693  DoNotConvert > h_DoNotConvert 1688  ConvertTo (x_ 4654, x_4653) > h_ConvertTo x_4654 x_46531694  ConvertTo (x_14617, x_14616) > h_ConvertTo x_14617 x_14616 1689 1695 1690 1696 (** val convert_flag_rect_Type2 : … … 1693 1699 let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function 1694 1700  DoNotConvert > h_DoNotConvert 1695  ConvertTo (x_ 4659, x_4658) > h_ConvertTo x_4659 x_46581701  ConvertTo (x_14622, x_14621) > h_ConvertTo x_14622 x_14621 1696 1702 1697 1703 (** val convert_flag_rect_Type1 : … … 1700 1706 let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function 1701 1707  DoNotConvert > h_DoNotConvert 1702  ConvertTo (x_ 4664, x_4663) > h_ConvertTo x_4664 x_46631708  ConvertTo (x_14627, x_14626) > h_ConvertTo x_14627 x_14626 1703 1709 1704 1710 (** val convert_flag_rect_Type0 : … … 1707 1713 let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function 1708 1714  DoNotConvert > h_DoNotConvert 1709  ConvertTo (x_ 4669, x_4668) > h_ConvertTo x_4669 x_46681715  ConvertTo (x_14632, x_14631) > h_ConvertTo x_14632 x_14631 1710 1716 1711 1717 (** val convert_flag_inv_rect_Type4 : … … 2030 2036 Obj.magic 2031 2037 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su) 2032 (fun eta 1293>2033 let result = eta 1293in2038 (fun eta2887 > 2039 let result = eta2887 in 2034 2040 (let { Types.fst = fgens1; Types.snd = s0 } = result in 2035 2041 (fun _ >
Note: See TracChangeset
for help on using the changeset viewer.