Changeset 2960 for extracted/toCminor.ml
 Timestamp:
 Mar 26, 2013, 4:51:40 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/toCminor.ml
r2951 r2960 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_13 081 > h_Global x_13081201  Stack x_13 082 > h_Stack x_13082200  Global x_138 > h_Global x_138 201  Stack x_139 > h_Stack x_139 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 3087 > h_Global x_13087208  Stack x_1 3088 > h_Stack x_13088207  Global x_144 > h_Global x_144 208  Stack x_145 > h_Stack x_145 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 3093 > h_Global x_13093215  Stack x_1 3094 > h_Stack x_13094214  Global x_150 > h_Global x_150 215  Stack x_151 > h_Stack x_151 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 3099 > h_Global x_13099222  Stack x_1 3100 > h_Stack x_13100221  Global x_156 > h_Global x_156 222  Stack x_157 > h_Stack x_157 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 3105 > h_Global x_13105229  Stack x_1 3106 > h_Stack x_13106228  Global x_162 > h_Global x_162 229  Stack x_163 > h_Stack x_163 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 3111 > h_Global x_13111236  Stack x_1 3112 > h_Stack x_13112235  Global x_168 > h_Global x_168 236  Stack x_169 > h_Stack x_169 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_ 14567 > h_MemDest x_145671223  MemDest x_216 > h_MemDest x_216 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_ 14572 > h_MemDest x_145721230  MemDest x_221 > h_MemDest x_221 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_ 14577 > h_MemDest x_145771237  MemDest x_226 > h_MemDest x_226 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_ 14582 > h_MemDest x_145821244  MemDest x_231 > h_MemDest x_231 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_ 14587 > h_MemDest x_145871251  MemDest x_236 > h_MemDest x_236 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_ 14592 > h_MemDest x_145921258  MemDest x_241 > h_MemDest x_241 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_14627 = 1385 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1386 x_14627 1384 let rec labgen_rect_Type4 h_mk_labgen x_276 = 1385 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_276 1387 1386 in 1388 1387 h_mk_labgen labuniverse0 label_genlist0 __ … … 1391 1390 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1392 1391 'a1) > labgen > 'a1 **) 1393 let rec labgen_rect_Type5 h_mk_labgen x_14629 = 1394 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1395 x_14629 1392 let rec labgen_rect_Type5 h_mk_labgen x_278 = 1393 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_278 1396 1394 in 1397 1395 h_mk_labgen labuniverse0 label_genlist0 __ … … 1400 1398 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1401 1399 'a1) > labgen > 'a1 **) 1402 let rec labgen_rect_Type3 h_mk_labgen x_14631 = 1403 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1404 x_14631 1400 let rec labgen_rect_Type3 h_mk_labgen x_280 = 1401 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_280 1405 1402 in 1406 1403 h_mk_labgen labuniverse0 label_genlist0 __ … … 1409 1406 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1410 1407 'a1) > labgen > 'a1 **) 1411 let rec labgen_rect_Type2 h_mk_labgen x_14633 = 1412 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1413 x_14633 1408 let rec labgen_rect_Type2 h_mk_labgen x_282 = 1409 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_282 1414 1410 in 1415 1411 h_mk_labgen labuniverse0 label_genlist0 __ … … 1418 1414 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1419 1415 'a1) > labgen > 'a1 **) 1420 let rec labgen_rect_Type1 h_mk_labgen x_14635 = 1421 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1422 x_14635 1416 let rec labgen_rect_Type1 h_mk_labgen x_284 = 1417 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_284 1423 1418 in 1424 1419 h_mk_labgen labuniverse0 label_genlist0 __ … … 1427 1422 (Identifiers.universe > PreIdentifiers.identifier List.list > __ > 1428 1423 'a1) > labgen > 'a1 **) 1429 let rec labgen_rect_Type0 h_mk_labgen x_14637 = 1430 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = 1431 x_14637 1424 let rec labgen_rect_Type0 h_mk_labgen x_286 = 1425 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_286 1432 1426 in 1433 1427 h_mk_labgen labuniverse0 label_genlist0 __ … … 1554 1548 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1555 1549 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1556 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_ 14653=1557 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14653in1550 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_302 = 1551 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_302 in 1558 1552 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1559 1553 … … 1561 1555 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1562 1556 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1563 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_ 14655=1564 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14655in1557 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_304 = 1558 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_304 in 1565 1559 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1566 1560 … … 1568 1562 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1569 1563 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1570 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_ 14657=1571 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14657in1564 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_306 = 1565 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_306 in 1572 1566 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1573 1567 … … 1575 1569 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1576 1570 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1577 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_ 14659=1578 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14659in1571 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_308 = 1572 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_308 in 1579 1573 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1580 1574 … … 1582 1576 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1583 1577 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1584 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_ 14661=1585 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14661in1578 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_310 = 1579 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_310 in 1586 1580 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1587 1581 … … 1589 1583 var_types > (Identifiers.universe > (AST.ident, Csyntax.type0) 1590 1584 Types.prod List.list > __ > __ > 'a1) > tmpgen > 'a1 **) 1591 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_ 14663=1592 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_ 14663in1585 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_312 = 1586 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_312 in 1593 1587 h_mk_tmpgen tmp_universe0 tmp_env0 __ __ 1594 1588 … … 1674 1668 let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function 1675 1669  DoNotConvert > h_DoNotConvert 1676  ConvertTo (x_ 14685, x_14684) > h_ConvertTo x_14685 x_146841670  ConvertTo (x_334, x_333) > h_ConvertTo x_334 x_333 1677 1671 1678 1672 (** val convert_flag_rect_Type5 : … … 1681 1675 let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function 1682 1676  DoNotConvert > h_DoNotConvert 1683  ConvertTo (x_ 14690, x_14689) > h_ConvertTo x_14690 x_146891677  ConvertTo (x_339, x_338) > h_ConvertTo x_339 x_338 1684 1678 1685 1679 (** val convert_flag_rect_Type3 : … … 1688 1682 let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function 1689 1683  DoNotConvert > h_DoNotConvert 1690  ConvertTo (x_ 14695, x_14694) > h_ConvertTo x_14695 x_146941684  ConvertTo (x_344, x_343) > h_ConvertTo x_344 x_343 1691 1685 1692 1686 (** val convert_flag_rect_Type2 : … … 1695 1689 let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function 1696 1690  DoNotConvert > h_DoNotConvert 1697  ConvertTo (x_ 14700, x_14699) > h_ConvertTo x_14700 x_146991691  ConvertTo (x_349, x_348) > h_ConvertTo x_349 x_348 1698 1692 1699 1693 (** val convert_flag_rect_Type1 : … … 1702 1696 let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function 1703 1697  DoNotConvert > h_DoNotConvert 1704  ConvertTo (x_ 14705, x_14704) > h_ConvertTo x_14705 x_147041698  ConvertTo (x_354, x_353) > h_ConvertTo x_354 x_353 1705 1699 1706 1700 (** val convert_flag_rect_Type0 : … … 1709 1703 let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function 1710 1704  DoNotConvert > h_DoNotConvert 1711  ConvertTo (x_ 14710, x_14709) > h_ConvertTo x_14710 x_147091705  ConvertTo (x_359, x_358) > h_ConvertTo x_359 x_358 1712 1706 1713 1707 (** val convert_flag_inv_rect_Type4 : … … 2032 2026 (Cminor_syntax.St_cost (l, s1')) }))) 2033 2027 2034 (** val alloc_params :2028 (** val alloc_params_main : 2035 2029 var_types > lenv > Csyntax.statement > tmpgen > convert_flag > 2036 2030 AST.typ Types.option > (AST.ident, Csyntax.type0) Types.prod List.list … … 2038 2032 Types.sig0 > ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) 2039 2033 Types.prod Types.sig0 Errors.res **) 2040 let alloc_params vars lbls statement uv ul rettyp params s =2034 let alloc_params_main vars lbls statement uv ul rettyp params s = 2041 2035 Util.foldl (fun su it > 2042 2036 let { Types.fst = id; Types.snd = ty } = it in 2043 2037 Obj.magic 2044 2038 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su) 2045 (fun eta 2436>2046 let result = eta 2436in2039 (fun eta650 > 2040 let result = eta650 in 2047 2041 (let { Types.fst = fgens1; Types.snd = s0 } = result in 2048 2042 (fun _ > … … 2062 2056  Local > (fun _ > Errors.OK result)) __)))) __))) (Errors.OK 2063 2057 s) params 2058 2059 (** val alloc_params : 2060 var_types > lenv > Csyntax.statement > tmpgen > convert_flag > 2061 AST.typ Types.option > (AST.ident, Csyntax.type0) Types.prod List.list 2062 > ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod 2063 Types.sig0 > ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) 2064 Types.prod Types.sig0 Errors.res **) 2065 let alloc_params vars lbls statement uv ul rettyp params su = 2066 (let { Types.fst = tl; Types.snd = s0 } = Types.pi1 su in 2067 (match s0 with 2068  Cminor_syntax.St_skip > 2069 (fun _ > alloc_params_main vars lbls statement uv ul rettyp params su) 2070  Cminor_syntax.St_assign (x, x0, x1) > 2071 (fun _ > alloc_params_main vars lbls statement uv ul rettyp params su) 2072  Cminor_syntax.St_store (x, x0, x1) > 2073 (fun _ > alloc_params_main vars lbls statement uv ul rettyp params su) 2074  Cminor_syntax.St_call (x, x0, x1) > 2075 (fun _ > alloc_params_main vars lbls statement uv ul rettyp params su) 2076  Cminor_syntax.St_seq (x, x0) > 2077 (fun _ > alloc_params_main vars lbls statement uv ul rettyp params su) 2078  Cminor_syntax.St_ifthenelse (x, x0, x1, x2, x3) > 2079 (fun _ > alloc_params_main vars lbls statement uv ul rettyp params su) 2080  Cminor_syntax.St_return x > 2081 (fun _ > alloc_params_main vars lbls statement uv ul rettyp params su) 2082  Cminor_syntax.St_label (x, x0) > 2083 (fun _ > alloc_params_main vars lbls statement uv ul rettyp params su) 2084  Cminor_syntax.St_goto x > 2085 (fun _ > alloc_params_main vars lbls statement uv ul rettyp params su) 2086  Cminor_syntax.St_cost (cl, s') > 2087 (fun _ > 2088 Obj.magic 2089 (Monad.m_bind0 (Monad.max_def Errors.res0) 2090 (Obj.magic 2091 (alloc_params_main vars lbls statement uv ul rettyp params 2092 { Types.fst = tl; Types.snd = s' })) (fun tls > 2093 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = 2094 (Types.pi1 tls).Types.fst; Types.snd = (Cminor_syntax.St_cost 2095 (cl, (Types.pi1 tls).Types.snd)) }))))) __ 2064 2096 2065 2097 (** val populate_lenv :
Note: See TracChangeset
for help on using the changeset viewer.