Mercurial > urweb

comparison src/elaborate.sml @ 563:44958d74c43f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial conversion to arbitrary-kind classes
author Adam Chlipala <adamc@hcoop.net>
date Fri, 19 Dec 2008 10:03:31 -0500
parents 685d232bd1a5
children 803b2f3bb86b
comparison
equal deleted inserted replaced
562:6daa59a55c43 563:44958d74c43f
2057 checkKind env c2' k2 (L'.KRecord (kunif loc), loc); 2057 checkKind env c2' k2 (L'.KRecord (kunif loc), loc);
2058 2058
2059 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3)) 2059 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3))
2060 end 2060 end
2061 2061
2062 | L.SgiClassAbs x => 2062 | L.SgiClassAbs (x, k) =>
2063 let 2063 let
2064 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 2064 val k = elabKind k
2065 val (env, n) = E.pushCNamed env x k NONE 2065 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
2066 val (env, n) = E.pushCNamed env x k' NONE
2066 val env = E.pushClass env n 2067 val env = E.pushClass env n
2067 in 2068 in
2068 ([(L'.SgiClassAbs (x, n), loc)], (env, denv, [])) 2069 ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, []))
2069 end 2070 end
2070 2071
2071 | L.SgiClass (x, c) => 2072 | L.SgiClass (x, k, c) =>
2072 let 2073 let
2073 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 2074 val k = elabKind k
2075 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
2074 val (c', ck, gs) = elabCon (env, denv) c 2076 val (c', ck, gs) = elabCon (env, denv) c
2075 val (env, n) = E.pushCNamed env x k (SOME c') 2077 val (env, n) = E.pushCNamed env x k' (SOME c')
2076 val env = E.pushClass env n 2078 val env = E.pushClass env n
2077 in 2079 in
2078 checkKind env c' ck k; 2080 checkKind env c' ck k';
2079 ([(L'.SgiClass (x, n, c'), loc)], (env, denv, [])) 2081 ([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, []))
2080 end 2082 end
2081 2083
2082 and elabSgn (env, denv) (sgn, loc) = 2084 and elabSgn (env, denv) (sgn, loc) =
2083 case sgn of 2085 case sgn of
2084 L.SgnConst sgis => 2086 L.SgnConst sgis =>
2138 sgnError env (DuplicateStr (loc, x)) 2140 sgnError env (DuplicateStr (loc, x))
2139 else 2141 else
2140 (); 2142 ();
2141 (cons, vals, sgns, SS.add (strs, x))) 2143 (cons, vals, sgns, SS.add (strs, x)))
2142 | L'.SgiConstraint _ => (cons, vals, sgns, strs) 2144 | L'.SgiConstraint _ => (cons, vals, sgns, strs)
2143 | L'.SgiClassAbs (x, _) => 2145 | L'.SgiClassAbs (x, _, _) =>
2144 (if SS.member (cons, x) then 2146 (if SS.member (cons, x) then
2145 sgnError env (DuplicateCon (loc, x)) 2147 sgnError env (DuplicateCon (loc, x))
2146 else 2148 else
2147 (); 2149 ();
2148 (SS.add (cons, x), vals, sgns, strs)) 2150 (SS.add (cons, x), vals, sgns, strs))
2149 | L'.SgiClass (x, _, _) => 2151 | L'.SgiClass (x, _, _, _) =>
2150 (if SS.member (cons, x) then 2152 (if SS.member (cons, x) then
2151 sgnError env (DuplicateCon (loc, x)) 2153 sgnError env (DuplicateCon (loc, x))
2152 else 2154 else
2153 (); 2155 ();
2154 (SS.add (cons, x), vals, sgns, strs))) 2156 (SS.add (cons, x), vals, sgns, strs)))
2220 | L'.SgnConst sgis => 2222 | L'.SgnConst sgis =>
2221 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) => 2223 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
2222 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) 2224 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
2223 | (L'.SgiDatatype (x, n, xs, xncs), loc) => 2225 | (L'.SgiDatatype (x, n, xs, xncs), loc) =>
2224 (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc) 2226 (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)
2225 | (L'.SgiClassAbs (x, n), loc) => 2227 | (L'.SgiClassAbs (x, n, k), loc) =>
2226 (L'.SgiClass (x, n, (L'.CModProj (str, strs, x), loc)), loc) 2228 (L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
2227 | (L'.SgiStr (x, n, sgn), loc) => 2229 | (L'.SgiStr (x, n, sgn), loc) =>
2228 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) 2230 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
2229 | x => x) sgis), #2 sgn) 2231 | x => x) sgis), #2 sgn)
2230 | L'.SgnFun _ => sgn 2232 | L'.SgnFun _ => sgn
2231 | L'.SgnWhere _ => sgn 2233 | L'.SgnWhere _ => sgn
2282 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc) 2284 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)
2283 | L'.SgiSgn (x, n, sgn) => 2285 | L'.SgiSgn (x, n, sgn) =>
2284 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc) 2286 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
2285 | L'.SgiConstraint (c1, c2) => 2287 | L'.SgiConstraint (c1, c2) =>
2286 (L'.DConstraint (c1, c2), loc) 2288 (L'.DConstraint (c1, c2), loc)
2287 | L'.SgiClassAbs (x, n) => 2289 | L'.SgiClassAbs (x, n, k) =>
2288 let 2290 let
2289 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 2291 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
2290 val c = (L'.CModProj (str, strs, x), loc) 2292 val c = (L'.CModProj (str, strs, x), loc)
2291 in 2293 in
2292 (L'.DCon (x, n, k, c), loc) 2294 (L'.DCon (x, n, k', c), loc)
2293 end 2295 end
2294 | L'.SgiClass (x, n, _) => 2296 | L'.SgiClass (x, n, k, _) =>
2295 let 2297 let
2296 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 2298 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
2297 val c = (L'.CModProj (str, strs, x), loc) 2299 val c = (L'.CModProj (str, strs, x), loc)
2298 in 2300 in
2299 (L'.DCon (x, n, k, c), loc) 2301 (L'.DCon (x, n, k', c), loc)
2300 end 2302 end
2301 in 2303 in
2302 (d, (E.declBinds env' d, denv')) 2304 (d, (E.declBinds env' d, denv'))
2303 end) 2305 end)
2304 (env, denv) sgis 2306 (env, denv) sgis
2318 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] 2320 | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)]
2319 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] 2321 | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)]
2320 | L'.DExport _ => [] 2322 | L'.DExport _ => []
2321 | L'.DTable (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), loc)), loc)] 2323 | L'.DTable (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), loc)), loc)]
2322 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)] 2324 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
2323 | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)] 2325 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
2324 | L'.DDatabase _ => [] 2326 | L'.DDatabase _ => []
2325 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] 2327 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
2326 2328
2327 fun sgiBindsD (env, denv) (sgi, _) = 2329 fun sgiBindsD (env, denv) (sgi, _) =
2328 case sgi of 2330 case sgi of
2416 val k = (L'.KType, loc) 2418 val k = (L'.KType, loc)
2417 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs 2419 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
2418 in 2420 in
2419 found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc)) 2421 found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc))
2420 end 2422 end
2421 | L'.SgiClassAbs (x', n1) => found (x', n1, 2423 | L'.SgiClassAbs (x', n1, k) => found (x', n1,
2422 (L'.KArrow ((L'.KType, loc), 2424 (L'.KArrow (k,
2423 (L'.KType, loc)), loc), 2425 (L'.KType, loc)), loc),
2424 NONE) 2426 NONE)
2425 | L'.SgiClass (x', n1, c) => found (x', n1, 2427 | L'.SgiClass (x', n1, k, c) => found (x', n1,
2426 (L'.KArrow ((L'.KType, loc), 2428 (L'.KArrow (k,
2427 (L'.KType, loc)), loc), 2429 (L'.KType, loc)), loc),
2428 SOME c) 2430 SOME c)
2429 | _ => NONE 2431 | _ => NONE
2430 end) 2432 end)
2431 2433
2432 | L'.SgiCon (x, n2, k2, c2) => 2434 | L'.SgiCon (x, n2, k2, c2) =>
2433 seek (fn (env, sgi1All as (sgi1, _)) => 2435 seek (fn (env, sgi1All as (sgi1, _)) =>
2456 else 2458 else
2457 NONE 2459 NONE
2458 in 2460 in
2459 case sgi1 of 2461 case sgi1 of
2460 L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1) 2462 L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1)
2461 | L'.SgiClass (x', n1, c1) => 2463 | L'.SgiClass (x', n1, k1, c1) =>
2462 found (x', n1, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), c1) 2464 found (x', n1, (L'.KArrow (k1, (L'.KType, loc)), loc), c1)
2463 | _ => NONE 2465 | _ => NONE
2464 end) 2466 end)
2465 2467
2466 | L'.SgiDatatype (x, n2, xs2, xncs2) => 2468 | L'.SgiDatatype (x, n2, xs2, xncs2) =>
2467 seek (fn (env, sgi1All as (sgi1, _)) => 2469 seek (fn (env, sgi1All as (sgi1, _)) =>
2630 end 2632 end
2631 else 2633 else
2632 NONE 2634 NONE
2633 | _ => NONE) 2635 | _ => NONE)
2634 2636
2635 | L'.SgiClassAbs (x, n2) => 2637 | L'.SgiClassAbs (x, n2, k2) =>
2636 seek (fn (env, sgi1All as (sgi1, _)) => 2638 seek (fn (env, sgi1All as (sgi1, _)) =>
2637 let 2639 let
2638 fun found (x', n1, co) = 2640 fun found (x', n1, k1, co) =
2639 if x = x' then 2641 if x = x' then
2640 let 2642 let
2641 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 2643 val () = unifyKinds k1 k2
2644 handle KUnify (k1, k2, err) =>
2645 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
2646
2647 val k = (L'.KArrow (k1, (L'.KType, loc)), loc)
2642 val env = E.pushCNamedAs env x n1 k co 2648 val env = E.pushCNamedAs env x n1 k co
2643 in 2649 in
2644 SOME (if n1 = n2 then 2650 SOME (if n1 = n2 then
2645 env 2651 env
2646 else 2652 else
2649 end 2655 end
2650 else 2656 else
2651 NONE 2657 NONE
2652 in 2658 in
2653 case sgi1 of 2659 case sgi1 of
2654 L'.SgiClassAbs (x', n1) => found (x', n1, NONE) 2660 L'.SgiClassAbs (x', n1, k1) => found (x', n1, k1, NONE)
2655 | L'.SgiClass (x', n1, c) => found (x', n1, SOME c) 2661 | L'.SgiClass (x', n1, k1, c) => found (x', n1, k1, SOME c)
2656 | _ => NONE 2662 | _ => NONE
2657 end) 2663 end)
2658 | L'.SgiClass (x, n2, c2) => 2664 | L'.SgiClass (x, n2, k2, c2) =>
2659 seek (fn (env, sgi1All as (sgi1, _)) => 2665 seek (fn (env, sgi1All as (sgi1, _)) =>
2660 let 2666 let
2661 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 2667 val k = (L'.KArrow (k2, (L'.KType, loc)), loc)
2662 2668
2663 fun found (x', n1, c1) = 2669 fun found (x', n1, k1, c1) =
2664 if x = x' then 2670 if x = x' then
2665 let 2671 let
2672 val () = unifyKinds k1 k2
2673 handle KUnify (k1, k2, err) =>
2674 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
2675
2666 fun good () = 2676 fun good () =
2667 let 2677 let
2668 val env = E.pushCNamedAs env x n2 k (SOME c2) 2678 val env = E.pushCNamedAs env x n2 k (SOME c2)
2669 val env = if n1 = n2 then 2679 val env = if n1 = n2 then
2670 env 2680 env
2683 end 2693 end
2684 else 2694 else
2685 NONE 2695 NONE
2686 in 2696 in
2687 case sgi1 of 2697 case sgi1 of
2688 L'.SgiClass (x', n1, c1) => found (x', n1, c1) 2698 L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1)
2689 | _ => NONE 2699 | _ => NONE
2690 end) 2700 end)
2691 end 2701 end
2692 in 2702 in
2693 ignore (foldl folder (env, denv) sgis2) 2703 ignore (foldl folder (env, denv) sgis2)
2876 val (neededC, neededV) = foldl (fn ((d, _), needed as (neededC, neededV)) => 2886 val (neededC, neededV) = foldl (fn ((d, _), needed as (neededC, neededV)) =>
2877 case d of 2887 case d of
2878 L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV) 2888 L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
2879 handle NotFound => 2889 handle NotFound =>
2880 needed) 2890 needed)
2881 | L.DClass (x, _) => ((#1 (SM.remove (neededC, x)), neededV) 2891 | L.DClass (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV)
2882 handle NotFound => needed) 2892 handle NotFound => needed)
2883 | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x)) 2893 | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x))
2884 handle NotFound => needed) 2894 handle NotFound => needed)
2885 | L.DOpen _ => (SM.empty, SS.empty) 2895 | L.DOpen _ => (SM.empty, SS.empty)
2886 | _ => needed) 2896 | _ => needed)
2887 (neededC, neededV) ds 2897 (neededC, neededV) ds
3284 val (env, n) = E.pushENamed env x (sequenceOf ()) 3294 val (env, n) = E.pushENamed env x (sequenceOf ())
3285 in 3295 in
3286 ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs)) 3296 ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs))
3287 end 3297 end
3288 3298
3289 | L.DClass (x, c) => 3299 | L.DClass (x, k, c) =>
3290 let 3300 let
3291 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) 3301 val k = elabKind k
3302 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
3292 val (c', ck, gs') = elabCon (env, denv) c 3303 val (c', ck, gs') = elabCon (env, denv) c
3293 val (env, n) = E.pushCNamed env x k (SOME c') 3304 val (env, n) = E.pushCNamed env x k' (SOME c')
3294 val env = E.pushClass env n 3305 val env = E.pushClass env n
3295 in 3306 in
3296 checkKind env c' ck k; 3307 checkKind env c' ck k';
3297 ([(L'.DClass (x, n, c'), loc)], (env, denv, enD gs' @ gs)) 3308 ([(L'.DClass (x, n, k, c'), loc)], (env, denv, enD gs' @ gs))
3298 end 3309 end
3299 3310
3300 | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs)) 3311 | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs))
3301 3312
3302 | L.DCookie (x, c) => 3313 | L.DCookie (x, c) =>
3406 (SS.add (strs, x), x) 3417 (SS.add (strs, x), x)
3407 in 3418 in
3408 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) 3419 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
3409 end 3420 end
3410 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs) 3421 | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs)
3411 | L'.SgiClassAbs (x, n) => 3422 | L'.SgiClassAbs (x, n, k) =>
3412 let 3423 let
3413 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
3414
3415 val (cons, x) = 3424 val (cons, x) =
3416 if SS.member (cons, x) then 3425 if SS.member (cons, x) then
3417 (cons, "?" ^ x) 3426 (cons, "?" ^ x)
3418 else 3427 else
3419 (SS.add (cons, x), x) 3428 (SS.add (cons, x), x)
3420 in 3429 in
3421 ((L'.SgiClassAbs (x, n), loc) :: sgis, cons, vals, sgns, strs) 3430 ((L'.SgiClassAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs)
3422 end 3431 end
3423 | L'.SgiClass (x, n, c) => 3432 | L'.SgiClass (x, n, k, c) =>
3424 let 3433 let
3425 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
3426
3427 val (cons, x) = 3434 val (cons, x) =
3428 if SS.member (cons, x) then 3435 if SS.member (cons, x) then
3429 (cons, "?" ^ x) 3436 (cons, "?" ^ x)
3430 else 3437 else
3431 (SS.add (cons, x), x) 3438 (SS.add (cons, x), x)
3432 in 3439 in
3433 ((L'.SgiClass (x, n, c), loc) :: sgis, cons, vals, sgns, strs) 3440 ((L'.SgiClass (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs)
3434 end) 3441 end)
3435 3442
3436 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis 3443 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
3437 in 3444 in
3438 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs) 3445 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs)