Mercurial > urweb

comparison src/elaborate.sml @ 711:7292bcb7c02d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Made type class system very general; demo compiles
author Adam Chlipala <adamc@hcoop.net>
date Thu, 09 Apr 2009 12:31:56 -0400
parents 71409a4ccb67
children 915ec60592d4
comparison
equal deleted inserted replaced
710:71409a4ccb67 711:7292bcb7c02d
2019 2019
2020 | L.SgiVal (x, c) => 2020 | L.SgiVal (x, c) =>
2021 let 2021 let
2022 val (c', ck, gs') = elabCon (env, denv) c 2022 val (c', ck, gs') = elabCon (env, denv) c
2023 2023
2024 val c' = normClassConstraint env c'
2024 val (env', n) = E.pushENamed env x c' 2025 val (env', n) = E.pushENamed env x c'
2025 val c' = normClassConstraint env c'
2026 in 2026 in
2027 (unifyKinds env ck ktype 2027 (unifyKinds env ck ktype
2028 handle KUnify ue => strError env (NotType (loc, ck, ue))); 2028 handle KUnify ue => strError env (NotType (loc, ck, ue)));
2029 2029
2030 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) 2030 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
2113 end 2113 end
2114 2114
2115 | L.SgiClassAbs (x, k) => 2115 | L.SgiClassAbs (x, k) =>
2116 let 2116 let
2117 val k = elabKind env k 2117 val k = elabKind env k
2118 val k' = (L'.KArrow (k, (L'.KType, loc)), loc) 2118 val (env, n) = E.pushCNamed env x k NONE
2119 val (env, n) = E.pushCNamed env x k' NONE
2120 val env = E.pushClass env n 2119 val env = E.pushClass env n
2121 in 2120 in
2122 ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, [])) 2121 ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, []))
2123 end 2122 end
2124 2123
2125 | L.SgiClass (x, k, c) => 2124 | L.SgiClass (x, k, c) =>
2126 let 2125 let
2127 val k = elabKind env k 2126 val k = elabKind env k
2128 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
2129 val (c', ck, gs) = elabCon (env, denv) c 2127 val (c', ck, gs) = elabCon (env, denv) c
2130 val (env, n) = E.pushCNamed env x k' (SOME c') 2128 val (env, n) = E.pushCNamed env x k (SOME c')
2131 val env = E.pushClass env n 2129 val env = E.pushClass env n
2132 in 2130 in
2133 checkKind env c' ck k'; 2131 checkKind env c' ck k;
2134 ([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, [])) 2132 ([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, []))
2135 end 2133 end
2136 2134
2137 and elabSgn (env, denv) (sgn, loc) = 2135 and elabSgn (env, denv) (sgn, loc) =
2138 case sgn of 2136 case sgn of
2339 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc) 2337 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
2340 | L'.SgiConstraint (c1, c2) => 2338 | L'.SgiConstraint (c1, c2) =>
2341 (L'.DConstraint (c1, c2), loc) 2339 (L'.DConstraint (c1, c2), loc)
2342 | L'.SgiClassAbs (x, n, k) => 2340 | L'.SgiClassAbs (x, n, k) =>
2343 let 2341 let
2344 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
2345 val c = (L'.CModProj (str, strs, x), loc) 2342 val c = (L'.CModProj (str, strs, x), loc)
2346 in 2343 in
2347 (L'.DCon (x, n, k', c), loc) 2344 (L'.DCon (x, n, k, c), loc)
2348 end 2345 end
2349 | L'.SgiClass (x, n, k, _) => 2346 | L'.SgiClass (x, n, k, _) =>
2350 let 2347 let
2351 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
2352 val c = (L'.CModProj (str, strs, x), loc) 2348 val c = (L'.CModProj (str, strs, x), loc)
2353 in 2349 in
2354 (L'.DCon (x, n, k', c), loc) 2350 (L'.DCon (x, n, k, c), loc)
2355 end 2351 end
2356 in 2352 in
2357 (d, E.declBinds env' d) 2353 (d, E.declBinds env' d)
2358 end) 2354 end)
2359 env sgis 2355 env sgis
2464 val k = (L'.KType, loc) 2460 val k = (L'.KType, loc)
2465 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs 2461 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
2466 in 2462 in
2467 found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc)) 2463 found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc))
2468 end 2464 end
2469 | L'.SgiClassAbs (x', n1, k) => found (x', n1, 2465 | L'.SgiClassAbs (x', n1, k) => found (x', n1, k, NONE)
2470 (L'.KArrow (k, 2466 | L'.SgiClass (x', n1, k, c) => found (x', n1, k, SOME c)
2471 (L'.KType, loc)), loc),
2472 NONE)
2473 | L'.SgiClass (x', n1, k, c) => found (x', n1,
2474 (L'.KArrow (k,
2475 (L'.KType, loc)), loc),
2476 SOME c)
2477 | _ => NONE 2467 | _ => NONE
2478 end) 2468 end)
2479 2469
2480 | L'.SgiCon (x, n2, k2, c2) => 2470 | L'.SgiCon (x, n2, k2, c2) =>
2481 seek (fn (env, sgi1All as (sgi1, _)) => 2471 seek (fn (env, sgi1All as (sgi1, _)) =>
2503 else 2493 else
2504 NONE 2494 NONE
2505 in 2495 in
2506 case sgi1 of 2496 case sgi1 of
2507 L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1) 2497 L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1)
2508 | L'.SgiClass (x', n1, k1, c1) => 2498 | L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1)
2509 found (x', n1, (L'.KArrow (k1, (L'.KType, loc)), loc), c1)
2510 | _ => NONE 2499 | _ => NONE
2511 end) 2500 end)
2512 2501
2513 | L'.SgiDatatype (x, n2, xs2, xncs2) => 2502 | L'.SgiDatatype (x, n2, xs2, xncs2) =>
2514 seek (fn (env, sgi1All as (sgi1, _)) => 2503 seek (fn (env, sgi1All as (sgi1, _)) =>
2675 let 2664 let
2676 val () = unifyKinds env k1 k2 2665 val () = unifyKinds env k1 k2
2677 handle KUnify (k1, k2, err) => 2666 handle KUnify (k1, k2, err) =>
2678 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) 2667 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
2679 2668
2680 val k = (L'.KArrow (k1, (L'.KType, loc)), loc) 2669 val env = E.pushCNamedAs env x n1 k1 co
2681 val env = E.pushCNamedAs env x n1 k co
2682 in 2670 in
2683 SOME (if n1 = n2 then 2671 SOME (if n1 = n2 then
2684 env 2672 env
2685 else 2673 else
2686 E.pushCNamedAs env x n2 k (SOME (L'.CNamed n1, loc2))) 2674 E.pushCNamedAs env x n2 k1 (SOME (L'.CNamed n1, loc2)))
2687 end 2675 end
2688 else 2676 else
2689 NONE 2677 NONE
2690 in 2678 in
2691 case sgi1 of 2679 case sgi1 of
2694 | _ => NONE 2682 | _ => NONE
2695 end) 2683 end)
2696 | L'.SgiClass (x, n2, k2, c2) => 2684 | L'.SgiClass (x, n2, k2, c2) =>
2697 seek (fn (env, sgi1All as (sgi1, _)) => 2685 seek (fn (env, sgi1All as (sgi1, _)) =>
2698 let 2686 let
2699 val k = (L'.KArrow (k2, (L'.KType, loc)), loc)
2700
2701 fun found (x', n1, k1, c1) = 2687 fun found (x', n1, k1, c1) =
2702 if x = x' then 2688 if x = x' then
2703 let 2689 let
2704 val () = unifyKinds env k1 k2 2690 val () = unifyKinds env k1 k2
2705 handle KUnify (k1, k2, err) => 2691 handle KUnify (k1, k2, err) =>
2706 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) 2692 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
2707 2693
2708 fun good () = 2694 fun good () =
2709 let 2695 let
2710 val env = E.pushCNamedAs env x n2 k (SOME c2) 2696 val env = E.pushCNamedAs env x n2 k2 (SOME c2)
2711 val env = if n1 = n2 then 2697 val env = if n1 = n2 then
2712 env 2698 env
2713 else 2699 else
2714 E.pushCNamedAs env x n1 k (SOME c1) 2700 E.pushCNamedAs env x n1 k2 (SOME c1)
2715 in 2701 in
2716 SOME env 2702 SOME env
2717 end 2703 end
2718 in 2704 in
2719 (unifyCons env c1 c2; 2705 (unifyCons env c1 c2;
3359 end 3345 end
3360 3346
3361 | L.DClass (x, k, c) => 3347 | L.DClass (x, k, c) =>
3362 let 3348 let
3363 val k = elabKind env k 3349 val k = elabKind env k
3364 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
3365 val (c', ck, gs') = elabCon (env, denv) c 3350 val (c', ck, gs') = elabCon (env, denv) c
3366 val (env, n) = E.pushCNamed env x k' (SOME c') 3351 val (env, n) = E.pushCNamed env x k (SOME c')
3367 val env = E.pushClass env n 3352 val env = E.pushClass env n
3368 in 3353 in
3369 checkKind env c' ck k'; 3354 checkKind env c' ck k;
3370 ([(L'.DClass (x, n, k, c'), loc)], (env, denv, enD gs' @ gs)) 3355 ([(L'.DClass (x, n, k, c'), loc)], (env, denv, enD gs' @ gs))
3371 end 3356 end
3372 3357
3373 | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs)) 3358 | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs))
3374 3359