Mercurial > urweb

comparison src/elab_env.sml @ 805:e2780d2f4afc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mutual datatypes through Elaborate
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 May 2009 15:14:17 -0400
parents 8688e01ae469
children 7f871c03e3a1
comparison
equal deleted inserted replaced
804:10fe57e4a8c2 805:e2780d2f4afc
907 907
908 fun sgiSeek (sgi, (sgns, strs, cons)) = 908 fun sgiSeek (sgi, (sgns, strs, cons)) =
909 case sgi of 909 case sgi of
910 SgiConAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) 910 SgiConAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
911 | SgiCon (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x)) 911 | SgiCon (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x))
912 | SgiDatatype (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x)) 912 | SgiDatatype dts => (sgns, strs, foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts)
913 | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x)) 913 | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x))
914 | SgiVal _ => (sgns, strs, cons) 914 | SgiVal _ => (sgns, strs, cons)
915 | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons) 915 | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons)
916 | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons) 916 | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons)
917 | SgiConstraint _ => (sgns, strs, cons) 917 | SgiConstraint _ => (sgns, strs, cons)
927 case f sgi of 927 case f sgi of
928 SOME v => 928 SOME v =>
929 let 929 let
930 val cons = 930 val cons =
931 case sgi of 931 case sgi of
932 SgiDatatype (x, n, _, _) => IM.insert (cons, n, x) 932 SgiDatatype dts => foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts
933 | SgiDatatypeImp (x, n, _, _, _, _, _) => IM.insert (cons, n, x) 933 | SgiDatatypeImp (x, n, _, _, _, _, _) => IM.insert (cons, n, x)
934 | _ => cons 934 | _ => cons
935 in 935 in
936 SOME (v, (sgns, strs, cons)) 936 SOME (v, (sgns, strs, cons))
937 end 937 end
1207 1207
1208 fun sgiBinds env (sgi, loc) = 1208 fun sgiBinds env (sgi, loc) =
1209 case sgi of 1209 case sgi of
1210 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE 1210 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
1211 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 1211 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
1212 | SgiDatatype (x, n, xs, xncs) => 1212 | SgiDatatype dts =>
1213 let 1213 let
1214 val k = (KType, loc) 1214 fun doOne ((x, n, xs, xncs), env) =
1215 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs 1215 let
1216 1216 val k = (KType, loc)
1217 val env = pushCNamedAs env x n k' NONE 1217 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
1218
1219 val env = pushCNamedAs env x n k' NONE
1220 in
1221 foldl (fn ((x', n', to), env) =>
1222 let
1223 val t =
1224 case to of
1225 NONE => (CNamed n, loc)
1226 | SOME t => (TFun (t, (CNamed n, loc)), loc)
1227
1228 val k = (KType, loc)
1229 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
1230 in
1231 pushENamedAs env x' n' t
1232 end)
1233 env xncs
1234 end
1218 in 1235 in
1219 foldl (fn ((x', n', to), env) => 1236 foldl doOne env dts
1220 let
1221 val t =
1222 case to of
1223 NONE => (CNamed n, loc)
1224 | SOME t => (TFun (t, (CNamed n, loc)), loc)
1225
1226 val k = (KType, loc)
1227 val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs
1228 in
1229 pushENamedAs env x' n' t
1230 end)
1231 env xncs
1232 end 1237 end
1233 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => 1238 | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) =>
1234 let 1239 let
1235 val k = (KType, loc) 1240 val k = (KType, loc)
1236 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs 1241 val k' = foldr (fn (_, k') => (KArrow (k, k'), loc)) k xs
1286 fun projectCon env {sgn, str, field} = 1291 fun projectCon env {sgn, str, field} =
1287 case #1 (hnormSgn env sgn) of 1292 case #1 (hnormSgn env sgn) of
1288 SgnConst sgis => 1293 SgnConst sgis =>
1289 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE 1294 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
1290 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE 1295 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
1291 | SgiDatatype (x, _, xs, _) => 1296 | SgiDatatype dts =>
1292 if x = field then 1297 (case List.find (fn (x, _, xs, _) => x = field) dts of
1293 let 1298 SOME (_, _, xs, _) =>
1294 val k = (KType, #2 sgn) 1299 let
1295 val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs 1300 val k = (KType, #2 sgn)
1296 in 1301 val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs
1297 SOME (k', NONE) 1302 in
1298 end 1303 SOME (k', NONE)
1299 else 1304 end
1300 NONE 1305 | NONE => NONE)
1301 | SgiDatatypeImp (x, _, m1, ms, x', xs, _) => 1306 | SgiDatatypeImp (x, _, m1, ms, x', xs, _) =>
1302 if x = field then 1307 if x = field then
1303 let 1308 let
1304 val k = (KType, #2 sgn) 1309 val k = (KType, #2 sgn)
1305 val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs 1310 val k' = foldl (fn (_, k') => (KArrow (k, k'), #2 sgn)) k xs
1323 | _ => NONE 1328 | _ => NONE
1324 1329
1325 fun projectDatatype env {sgn, str, field} = 1330 fun projectDatatype env {sgn, str, field} =
1326 case #1 (hnormSgn env sgn) of 1331 case #1 (hnormSgn env sgn) of
1327 SgnConst sgis => 1332 SgnConst sgis =>
1328 (case sgnSeek (fn SgiDatatype (x, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE 1333 (case sgnSeek (fn SgiDatatype dts =>
1334 (case List.find (fn (x, _, _, _) => x = field) dts of
1335 SOME (_, _, xs, xncs) => SOME (xs, xncs)
1336 | NONE => NONE)
1329 | SgiDatatypeImp (x, _, _, _, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE 1337 | SgiDatatypeImp (x, _, _, _, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE
1330 | _ => NONE) sgis of 1338 | _ => NONE) sgis of
1331 NONE => NONE 1339 NONE => NONE
1332 | SOME ((xs, xncs), subs) => SOME (xs, 1340 | SOME ((xs, xncs), subs) => SOME (xs,
1333 map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs)) 1341 map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
1342 if x <> field then 1350 if x <> field then
1343 NONE 1351 NONE
1344 else 1352 else
1345 SOME (U.classifyDatatype xncs, n', xs, to, (CNamed n, #2 str))) xncs 1353 SOME (U.classifyDatatype xncs, n', xs, to, (CNamed n, #2 str))) xncs
1346 in 1354 in
1347 case sgnSeek (fn SgiDatatype (_, n, xs, xncs) => consider (n, xs, xncs) 1355 case sgnSeek (fn SgiDatatype dts =>
1356 let
1357 fun search dts =
1358 case dts of
1359 [] => NONE
1360 | (_, n, xs, xncs) :: dts =>
1361 case consider (n, xs, xncs) of
1362 NONE => search dts
1363 | v => v
1364 in
1365 search dts
1366 end
1348 | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => consider (n, xs, xncs) 1367 | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => consider (n, xs, xncs)
1349 | _ => NONE) sgis of 1368 | _ => NONE) sgis of
1350 NONE => NONE 1369 NONE => NONE
1351 | SOME ((dk, n, xs, to, t), subs) => SOME (dk, n, xs, Option.map (sgnSubCon (str, subs)) to, 1370 | SOME ((dk, n, xs, to, t), subs) => SOME (dk, n, xs, Option.map (sgnSubCon (str, subs)) to,
1352 sgnSubCon (str, subs) t) 1371 sgnSubCon (str, subs) t)
1380 end) 1399 end)
1381 else 1400 else
1382 NONE) xncs 1401 NONE) xncs
1383 in 1402 in
1384 case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE 1403 case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE
1385 | SgiDatatype (_, n, xs, xncs) => seek (n, xs, xncs) 1404 | SgiDatatype dts =>
1405 let
1406 fun search dts =
1407 case dts of
1408 [] => NONE
1409 | (_, n, xs, xncs) :: dts =>
1410 case seek (n, xs, xncs) of
1411 NONE => search dts
1412 | v => v
1413 in
1414 search dts
1415 end
1386 | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => seek (n, xs, xncs) 1416 | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => seek (n, xs, xncs)
1387 | _ => NONE) sgis of 1417 | _ => NONE) sgis of
1388 NONE => NONE 1418 NONE => NONE
1389 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c) 1419 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)
1390 end 1420 end
1404 in 1434 in
1405 seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc) 1435 seek (sgis, sgns, strs, cons, (sub c1, sub c2) :: acc)
1406 end 1436 end
1407 | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 1437 | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
1408 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 1438 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
1409 | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 1439 | SgiDatatype dts => seek (sgis, sgns, strs,
1440 foldl (fn ((x, n, _, _), cons) => IM.insert (cons, n, x)) cons dts, acc)
1410 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 1441 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
1411 | SgiVal _ => seek (sgis, sgns, strs, cons, acc) 1442 | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
1412 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) 1443 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
1413 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) 1444 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
1414 | SgiClassAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 1445 | SgiClassAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
1429 | EDValRec vis => foldl (fn ((x, t, _), env) => pushERel env x t) env vis 1460 | EDValRec vis => foldl (fn ((x, t, _), env) => pushERel env x t) env vis
1430 1461
1431 fun declBinds env (d, loc) = 1462 fun declBinds env (d, loc) =
1432 case d of 1463 case d of
1433 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 1464 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
1434 | DDatatype (x, n, xs, xncs) => 1465 | DDatatype dts =>
1435 let 1466 let
1436 val k = (KType, loc) 1467 fun doOne ((x, n, xs, xncs), env) =
1437 val nxs = length xs 1468 let
1438 val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) => 1469 val k = (KType, loc)
1439 ((CApp (tb, (CRel (nxs - i - 1), loc)), loc), 1470 val nxs = length xs
1440 (KArrow (k, kb), loc))) 1471 val (tb, kb) = ListUtil.foldli (fn (i, x', (tb, kb)) =>
1441 ((CNamed n, loc), k) xs 1472 ((CApp (tb, (CRel (nxs - i - 1), loc)), loc),
1442 1473 (KArrow (k, kb), loc)))
1443 val env = pushCNamedAs env x n kb NONE 1474 ((CNamed n, loc), k) xs
1444 val env = pushDatatype env n xs xncs 1475
1476 val env = pushCNamedAs env x n kb NONE
1477 val env = pushDatatype env n xs xncs
1478 in
1479 foldl (fn ((x', n', to), env) =>
1480 let
1481 val t =
1482 case to of
1483 NONE => tb
1484 | SOME t => (TFun (t, tb), loc)
1485 val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
1486 in
1487 pushENamedAs env x' n' t
1488 end)
1489 env xncs
1490 end
1445 in 1491 in
1446 foldl (fn ((x', n', to), env) => 1492 foldl doOne env dts
1447 let
1448 val t =
1449 case to of
1450 NONE => tb
1451 | SOME t => (TFun (t, tb), loc)
1452 val t = foldr (fn (x, t) => (TCFun (Implicit, x, k, t), loc)) t xs
1453 in
1454 pushENamedAs env x' n' t
1455 end)
1456 env xncs
1457 end 1493 end
1458 | DDatatypeImp (x, n, m, ms, x', xs, xncs) => 1494 | DDatatypeImp (x, n, m, ms, x', xs, xncs) =>
1459 let 1495 let
1460 val t = (CModProj (m, ms, x'), loc) 1496 val t = (CModProj (m, ms, x'), loc)
1461 val k = (KType, loc) 1497 val k = (KType, loc)