Changeset 2827 for extracted/toCminor.ml
 Timestamp:
 Mar 8, 2013, 9:07:28 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toCminor.ml
r2797 r2827 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 2925 > h_Global x_12925201  Stack x_1 2926 > h_Stack x_12926200  Global x_13042 > h_Global x_13042 201  Stack x_13043 > h_Stack x_13043 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 2931 > h_Global x_12931208  Stack x_1 2932 > h_Stack x_12932207  Global x_13048 > h_Global x_13048 208  Stack x_13049 > h_Stack x_13049 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 2937 > h_Global x_12937215  Stack x_1 2938 > h_Stack x_12938214  Global x_13054 > h_Global x_13054 215  Stack x_13055 > h_Stack x_13055 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 2943 > h_Global x_12943222  Stack x_1 2944 > h_Stack x_12944221  Global x_13060 > h_Global x_13060 222  Stack x_13061 > h_Stack x_13061 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 2949 > h_Global x_12949229  Stack x_1 2950 > h_Stack x_12950228  Global x_13066 > h_Global x_13066 229  Stack x_13067 > h_Stack x_13067 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 2955 > h_Global x_12955236  Stack x_1 2956 > h_Stack x_12956235  Global x_13072 > h_Global x_13072 236  Stack x_13073 > h_Stack x_13073 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_14 411 > h_MemDest x_144111223  MemDest x_14528 > h_MemDest x_14528 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_14 416 > h_MemDest x_144161230  MemDest x_14533 > h_MemDest x_14533 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_14 421 > h_MemDest x_144211237  MemDest x_14538 > h_MemDest x_14538 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_14 426 > h_MemDest x_144261244  MemDest x_14543 > h_MemDest x_14543 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_14 431 > h_MemDest x_144311251  MemDest x_14548 > h_MemDest x_14548 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_14 436 > h_MemDest x_144361258  MemDest x_14553 > h_MemDest x_14553 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 471=1384 let rec labgen_rect_Type4 h_mk_labgen x_14588 = 1385 1385 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1386 x_14 4711386 x_14588 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 473=1393 let rec labgen_rect_Type5 h_mk_labgen x_14590 = 1394 1394 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1395 x_14 4731395 x_14590 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 475=1402 let rec labgen_rect_Type3 h_mk_labgen x_14592 = 1403 1403 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1404 x_14 4751404 x_14592 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 477=1411 let rec labgen_rect_Type2 h_mk_labgen x_14594 = 1412 1412 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1413 x_14 4771413 x_14594 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 479=1420 let rec labgen_rect_Type1 h_mk_labgen x_14596 = 1421 1421 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1422 x_14 4791422 x_14596 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 481=1429 let rec labgen_rect_Type0 h_mk_labgen x_14598 = 1430 1430 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1431 x_14 4811431 x_14598 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_14 497=1557 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14 497in1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14614 = 1557 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14614 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_14 499=1564 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14 499in1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14616 = 1564 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14616 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_14 501=1571 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14 501in1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14618 = 1571 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14618 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_14 503=1578 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14 503in1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14620 = 1578 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14620 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_14 505=1585 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14 505in1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14622 = 1585 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14622 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_14 507=1592 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14 507in1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14624 = 1592 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14624 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_14 529, x_14528) > h_ConvertTo x_14529 x_145281676  ConvertTo (x_14646, x_14645) > h_ConvertTo x_14646 x_14645 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_14 534, x_14533) > h_ConvertTo x_14534 x_145331683  ConvertTo (x_14651, x_14650) > h_ConvertTo x_14651 x_14650 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_14 539, x_14538) > h_ConvertTo x_14539 x_145381690  ConvertTo (x_14656, x_14655) > h_ConvertTo x_14656 x_14655 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 544, x_14543) > h_ConvertTo x_14544 x_145431697  ConvertTo (x_14661, x_14660) > h_ConvertTo x_14661 x_14660 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 549, x_14548) > h_ConvertTo x_14549 x_145481704  ConvertTo (x_14666, x_14665) > h_ConvertTo x_14666 x_14665 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 554, x_14553) > h_ConvertTo x_14554 x_145531711  ConvertTo (x_14671, x_14670) > h_ConvertTo x_14671 x_14670 1712 1712 1713 1713 (** val convert_flag_inv_rect_Type4 : … … 1786 1786 ((Csyntax.typ_of_type ty), id, (Types.pi1 e2'0))) })) 1787 1787  MemDest e1' > 1788 Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd = 1789 ul }; Types.snd = (Cminor_syntax.St_store 1790 ((Csyntax.typ_of_type (Csyntax.typeof e2)), (Types.pi1 e1'), 1791 (Types.pi1 e2'))) })))) 1788 (match TypeComparison.type_eq_dec (Csyntax.typeof e1) 1789 (Csyntax.typeof e2) with 1790  Types.Inl _ > 1791 Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd = 1792 ul }; Types.snd = (Cminor_syntax.St_store 1793 ((Csyntax.typ_of_type (Csyntax.typeof e2)), (Types.pi1 e1'), 1794 (Types.pi1 e2'))) }) 1795  Types.Inr _ > 1796 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))))) 1792 1797  Csyntax.Scall (ret, ef, args) > 1793 1798 Obj.magic … … 1821 1826 in 1822 1827 (fun _ > 1823 Obj.magic (Errors.OK { Types.fst = { Types.fst = uv1; 1828 (let { Types.fst = tmp2; Types.snd = uv2 } = 1829 alloc_tmp vars (Csyntax.Tpointer (Csyntax.typeof e1)) uv1 1830 in 1831 (fun _ > 1832 Obj.magic (Errors.OK { Types.fst = { Types.fst = uv2; 1824 1833 Types.snd = ul }; Types.snd = (Cminor_syntax.St_seq 1825 ((Cminor_syntax.St_call ((Types.Some { Types.fst = tmp; 1826 Types.snd = (Csyntax.typ_of_type (Csyntax.typeof e1)) }), 1834 ((Cminor_syntax.St_store (AST.ASTptr, (Cminor_syntax.Id 1835 (AST.ASTptr, tmp2)), (Types.pi1 e1'))), 1836 (Cminor_syntax.St_seq ((Cminor_syntax.St_call ((Types.Some 1837 { Types.fst = tmp; Types.snd = 1838 (Csyntax.typ_of_type (Csyntax.typeof e1)) }), 1827 1839 (Types.pi1 ef'0), (Types.pi1 args'))), 1828 1840 (Cminor_syntax.St_store 1829 1841 ((Csyntax.typ_of_type (Csyntax.typeof e1)), 1830 1842 (Types.pi1 e1'), (Cminor_syntax.Id 1831 ((Csyntax.typ_of_type (Csyntax.typeof e1)), tmp)))))) })))1832 __)) )))1843 ((Csyntax.typ_of_type (Csyntax.typeof e1)), tmp)))))))) }))) 1844 __)) __))))) 1833 1845  Csyntax.Ssequence (s1, s2) > 1834 1846 Obj.magic … … 2032 2044 Obj.magic 2033 2045 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su) 2034 (fun eta243 4>2035 let result = eta243 4in2046 (fun eta2436 > 2047 let result = eta2436 in 2036 2048 (let { Types.fst = fgens1; Types.snd = s0 } = result in 2037 2049 (fun _ >
Note: See TracChangeset
for help on using the changeset viewer.