Mercurial > urweb

comparison src/elaborate.sml @ 211:e86411f647c6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial type class support
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 Aug 2008 14:32:18 -0400
parents f4033abd6ab1
children 0343557355fc
comparison
equal deleted inserted replaced
210:f4033abd6ab1 211:e86411f647c6
983 | UnboundConstructor of ErrorMsg.span * string list * string 983 | UnboundConstructor of ErrorMsg.span * string list * string
984 | PatHasArg of ErrorMsg.span 984 | PatHasArg of ErrorMsg.span
985 | PatHasNoArg of ErrorMsg.span 985 | PatHasNoArg of ErrorMsg.span
986 | Inexhaustive of ErrorMsg.span 986 | Inexhaustive of ErrorMsg.span
987 | DuplicatePatField of ErrorMsg.span * string 987 | DuplicatePatField of ErrorMsg.span * string
988 | SqlInfer of ErrorMsg.span * L'.con 988 | Unresolvable of ErrorMsg.span * L'.con
989 | OutOfContext of ErrorMsg.span
989 990
990 fun expError env err = 991 fun expError env err =
991 case err of 992 case err of
992 UnboundExp (loc, s) => 993 UnboundExp (loc, s) =>
993 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s) 994 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
1026 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument" 1027 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
1027 | Inexhaustive loc => 1028 | Inexhaustive loc =>
1028 ErrorMsg.errorAt loc "Inexhaustive 'case'" 1029 ErrorMsg.errorAt loc "Inexhaustive 'case'"
1029 | DuplicatePatField (loc, s) => 1030 | DuplicatePatField (loc, s) =>
1030 ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern") 1031 ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
1031 | SqlInfer (loc, c) => 1032 | OutOfContext loc =>
1032 (ErrorMsg.errorAt loc "Can't infer SQL-ness of type"; 1033 ErrorMsg.errorAt loc "Type class wildcard occurs out of context"
1033 eprefaces' [("Type", p_con env c)]) 1034 | Unresolvable (loc, c) =>
1035 (ErrorMsg.errorAt loc "Can't resolve type class instance";
1036 eprefaces' [("Class constraint", p_con env c)])
1034 1037
1035 fun checkCon (env, denv) e c1 c2 = 1038 fun checkCon (env, denv) e c1 c2 =
1036 unifyCons (env, denv) c1 c2 1039 unifyCons (env, denv) c1 c2
1037 handle CUnify (c1, c2, err) => 1040 handle CUnify (c1, c2, err) =>
1038 (expError env (Unify (e, c1, c2, err)); 1041 (expError env (Unify (e, c1, c2, err));
1417 | SOME t => t 1420 | SOME t => t
1418 in 1421 in
1419 ((L'.EModProj (n, ms, s), loc), t, []) 1422 ((L'.EModProj (n, ms, s), loc), t, [])
1420 end) 1423 end)
1421 1424
1422 | L.EApp (e1, (L.ESqlInfer, _)) => 1425 | L.EApp (e1, (L.EWild, _)) =>
1423 let 1426 let
1424 val (e1', t1, gs1) = elabExp (env, denv) e1 1427 val (e1', t1, gs1) = elabExp (env, denv) e1
1425 val (e1', t1, gs2) = elabHead (env, denv) e1' t1 1428 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
1426 val (t1, gs3) = hnormCon (env, denv) t1 1429 val (t1, gs3) = hnormCon (env, denv) t1
1427 in 1430 in
1428 case t1 of 1431 case t1 of
1429 (L'.TFun ((L'.CApp ((L'.CModProj (basis, [], "sql_type"), _), 1432 (L'.TFun (dom, ran), _) =>
1430 t), _), ran), _) => 1433 (case E.resolveClass env dom of
1431 if basis <> !basis_r then 1434 NONE => (expError env (Unresolvable (loc, dom));
1432 raise Fail "Bad use of ESqlInfer [1]" 1435 (eerror, cerror, []))
1433 else 1436 | SOME pf => ((L'.EApp (e1', pf), loc), ran, gs1 @ gs2 @ gs3))
1434 let 1437 | _ => (expError env (OutOfContext loc);
1435 val (t, gs4) = hnormCon (env, denv) t 1438 (eerror, cerror, []))
1436
1437 fun error () = expError env (SqlInfer (loc, t))
1438 in
1439 case t of
1440 (L'.CModProj (basis, [], x), _) =>
1441 (if basis <> !basis_r then
1442 error ()
1443 else
1444 case x of
1445 "bool" => ()
1446 | "int" => ()
1447 | "float" => ()
1448 | "string" => ()
1449 | _ => error ();
1450 ((L'.EApp (e1', (L'.EModProj (basis, [], "sql_" ^ x), loc)), loc),
1451 ran, gs1 @ gs2 @ gs3 @ gs4))
1452 | (L'.CUnif (_, (L'.KType, _), _, r), _) =>
1453 let
1454 val t = (L'.CModProj (basis, [], "int"), loc)
1455 in
1456 r := SOME t;
1457 ((L'.EApp (e1', (L'.EModProj (basis, [], "sql_int"), loc)), loc),
1458 ran, gs1 @ gs2 @ gs3 @ gs4)
1459 end
1460 | _ => (error ();
1461 (eerror, cerror, []))
1462 end
1463 | _ => raise Fail "Bad use of ESqlInfer [2]"
1464 end 1439 end
1465 | L.ESqlInfer => raise Fail "Bad use of ESqlInfer [3]" 1440 | L.EWild => (expError env (OutOfContext loc);
1441 (eerror, cerror, []))
1466 1442
1467 | L.EApp (e1, e2) => 1443 | L.EApp (e1, e2) =>
1468 let 1444 let
1469 val (e1', t1, gs1) = elabExp (env, denv) e1 1445 val (e1', t1, gs1) = elabExp (env, denv) e1
1470 val (e1', t1, gs2) = elabHead (env, denv) e1' t1 1446 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
1957 val (c', k, gs) = elabCon (env, denv) c 1933 val (c', k, gs) = elabCon (env, denv) c
1958 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc) 1934 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
1959 in 1935 in
1960 checkKind env c' k (L'.KRecord (L'.KType, loc), loc); 1936 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
1961 ([(L'.SgiTable (!basis_r, x, n, c'), loc)], (env, denv, gs)) 1937 ([(L'.SgiTable (!basis_r, x, n, c'), loc)], (env, denv, gs))
1938 end
1939
1940 | L.SgiClassAbs x =>
1941 let
1942 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
1943 val (env, n) = E.pushCNamed env x k NONE
1944 val env = E.pushClass env n
1945 in
1946 ([(L'.SgiClassAbs (x, n), loc)], (env, denv, []))
1947 end
1948
1949 | L.SgiClass (x, c) =>
1950 let
1951 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
1952 val (c', ck, gs) = elabCon (env, denv) c
1953 val (env, n) = E.pushCNamed env x k (SOME c')
1954 val env = E.pushClass env n
1955 in
1956 checkKind env c' ck k;
1957 ([(L'.SgiClass (x, n, c'), loc)], (env, denv, []))
1962 end 1958 end
1963 1959
1964 and elabSgn (env, denv) (sgn, loc) = 1960 and elabSgn (env, denv) (sgn, loc) =
1965 case sgn of 1961 case sgn of
1966 L.SgnConst sgis => 1962 L.SgnConst sgis =>
2025 | L'.SgiTable (_, x, _, _) => 2021 | L'.SgiTable (_, x, _, _) =>
2026 (if SS.member (vals, x) then 2022 (if SS.member (vals, x) then
2027 sgnError env (DuplicateVal (loc, x)) 2023 sgnError env (DuplicateVal (loc, x))
2028 else 2024 else
2029 (); 2025 ();
2030 (cons, SS.add (vals, x), sgns, strs))) 2026 (cons, SS.add (vals, x), sgns, strs))
2027 | L'.SgiClassAbs (x, _) =>
2028 (if SS.member (cons, x) then
2029 sgnError env (DuplicateCon (loc, x))
2030 else
2031 ();
2032 (SS.add (cons, x), vals, sgns, strs))
2033 | L'.SgiClass (x, _, _) =>
2034 (if SS.member (cons, x) then
2035 sgnError env (DuplicateCon (loc, x))
2036 else
2037 ();
2038 (SS.add (cons, x), vals, sgns, strs)))
2031 (SS.empty, SS.empty, SS.empty, SS.empty) sgis' 2039 (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
2032 in 2040 in
2033 ((L'.SgnConst sgis', loc), gs) 2041 ((L'.SgnConst sgis', loc), gs)
2034 end 2042 end
2035 | L.SgnVar x => 2043 | L.SgnVar x =>
2158 | L'.SgiConstraint (c1, c2) => 2166 | L'.SgiConstraint (c1, c2) =>
2159 (L'.DConstraint (c1, c2), loc) 2167 (L'.DConstraint (c1, c2), loc)
2160 | L'.SgiTable (_, x, n, c) => 2168 | L'.SgiTable (_, x, n, c) =>
2161 (L'.DVal (x, n, (L'.CApp (tableOf (), c), loc), 2169 (L'.DVal (x, n, (L'.CApp (tableOf (), c), loc),
2162 (L'.EModProj (str, strs, x), loc)), loc) 2170 (L'.EModProj (str, strs, x), loc)), loc)
2171 | L'.SgiClassAbs (x, n) =>
2172 let
2173 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
2174 val c = (L'.CModProj (str, strs, x), loc)
2175 in
2176 (L'.DCon (x, n, k, c), loc)
2177 end
2178 | L'.SgiClass (x, n, _) =>
2179 let
2180 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
2181 val c = (L'.CModProj (str, strs, x), loc)
2182 in
2183 (L'.DCon (x, n, k, c), loc)
2184 end
2163 in 2185 in
2164 (d, (E.declBinds env' d, denv')) 2186 (d, (E.declBinds env' d, denv'))
2165 end) 2187 end)
2166 (env, denv) sgis 2188 (env, denv) sgis
2167 | _ => (strError env (UnOpenable sgn); 2189 | _ => (strError env (UnOpenable sgn);
2281 val k = (L'.KType, loc) 2303 val k = (L'.KType, loc)
2282 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs 2304 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
2283 in 2305 in
2284 found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc)) 2306 found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc))
2285 end 2307 end
2308 | L'.SgiClassAbs (x', n1) => found (x', n1,
2309 (L'.KArrow ((L'.KType, loc),
2310 (L'.KType, loc)), loc),
2311 NONE)
2312 | L'.SgiClass (x', n1, c) => found (x', n1,
2313 (L'.KArrow ((L'.KType, loc),
2314 (L'.KType, loc)), loc),
2315 SOME c)
2286 | _ => NONE 2316 | _ => NONE
2287 end) 2317 end)
2288 2318
2289 | L'.SgiCon (x, n2, k2, c2) => 2319 | L'.SgiCon (x, n2, k2, c2) =>
2290 seek (fn sgi1All as (sgi1, _) => 2320 seek (fn sgi1All as (sgi1, _) =>
2291 case sgi1 of 2321 let
2292 L'.SgiCon (x', n1, k1, c1) => 2322 fun found (x', n1, k1, c1) =
2293 if x = x' then 2323 if x = x' then
2294 let 2324 let
2295 fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2), denv) 2325 fun good () = SOME (E.pushCNamedAs env x n2 k2 (SOME c2), denv)
2296 in 2326 in
2297 (case unifyCons (env, denv) c1 c2 of 2327 (case unifyCons (env, denv) c1 c2 of
2298 [] => good () 2328 [] => good ()
2299 | _ => NONE) 2329 | _ => NONE)
2300 handle CUnify (c1, c2, err) => 2330 handle CUnify (c1, c2, err) =>
2301 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2331 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2302 good ()) 2332 good ())
2303 end 2333 end
2304 else 2334 else
2305 NONE 2335 NONE
2306 | _ => NONE) 2336 in
2337 case sgi1 of
2338 L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1)
2339 | L'.SgiClass (x', n1, c1) =>
2340 found (x', n1, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), c1)
2341 | _ => NONE
2342 end)
2307 2343
2308 | L'.SgiDatatype (x, n2, xs2, xncs2) => 2344 | L'.SgiDatatype (x, n2, xs2, xncs2) =>
2309 seek (fn sgi1All as (sgi1, _) => 2345 seek (fn sgi1All as (sgi1, _) =>
2310 let 2346 let
2311 fun found (n1, xs1, xncs1) = 2347 fun found (n1, xs1, xncs1) =
2489 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2525 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2490 SOME (env, denv)) 2526 SOME (env, denv))
2491 else 2527 else
2492 NONE 2528 NONE
2493 | _ => NONE) 2529 | _ => NONE)
2530
2531 | L'.SgiClassAbs (x, n2) =>
2532 seek (fn sgi1All as (sgi1, _) =>
2533 let
2534 fun found (x', n1, co) =
2535 if x = x' then
2536 let
2537 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
2538 val env = E.pushCNamedAs env x n1 k co
2539 in
2540 SOME (if n1 = n2 then
2541 env
2542 else
2543 E.pushCNamedAs env x n2 k (SOME (L'.CNamed n1, loc2)),
2544 denv)
2545 end
2546 else
2547 NONE
2548 in
2549 case sgi1 of
2550 L'.SgiClassAbs (x', n1) => found (x', n1, NONE)
2551 | L'.SgiClass (x', n1, c) => found (x', n1, SOME c)
2552 | _ => NONE
2553 end)
2554 | L'.SgiClass (x, n2, c2) =>
2555 seek (fn sgi1All as (sgi1, _) =>
2556 let
2557 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
2558
2559 fun found (x', n1, c1) =
2560 if x = x' then
2561 let
2562 fun good () = SOME (E.pushCNamedAs env x n2 k (SOME c2), denv)
2563 in
2564 (case unifyCons (env, denv) c1 c2 of
2565 [] => good ()
2566 | _ => NONE)
2567 handle CUnify (c1, c2, err) =>
2568 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2569 good ())
2570 end
2571 else
2572 NONE
2573 in
2574 case sgi1 of
2575 L'.SgiClass (x', n1, c1) => found (x', n1, c1)
2576 | _ => NONE
2577 end)
2494 end 2578 end
2495 in 2579 in
2496 ignore (foldl folder (env, denv) sgis2) 2580 ignore (foldl folder (env, denv) sgis2)
2497 end 2581 end
2498 2582
2845 val (c', k, gs') = elabCon (env, denv) c 2929 val (c', k, gs') = elabCon (env, denv) c
2846 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc) 2930 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
2847 in 2931 in
2848 checkKind env c' k (L'.KRecord (L'.KType, loc), loc); 2932 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
2849 ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, gs' @ gs)) 2933 ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, gs' @ gs))
2934 end
2935
2936 | L.DClass (x, c) =>
2937 let
2938 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
2939 val (c', ck, gs) = elabCon (env, denv) c
2940 val (env, n) = E.pushCNamed env x k (SOME c')
2941 val env = E.pushClass env n
2942 in
2943 checkKind env c' ck k;
2944 ([(L'.DCon (x, n, k, c'), loc)], (env, denv, []))
2850 end 2945 end
2851 2946
2852 and elabStr (env, denv) (str, loc) = 2947 and elabStr (env, denv) (str, loc) =
2853 case str of 2948 case str of
2854 L.StrConst ds => 2949 L.StrConst ds =>
2947 (vals, "?" ^ x) 3042 (vals, "?" ^ x)
2948 else 3043 else
2949 (SS.add (vals, x), x) 3044 (SS.add (vals, x), x)
2950 in 3045 in
2951 ((L'.SgiTable (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs) 3046 ((L'.SgiTable (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs)
3047 end
3048 | L'.SgiClassAbs (x, n) =>
3049 let
3050 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
3051
3052 val (cons, x) =
3053 if SS.member (cons, x) then
3054 (cons, "?" ^ x)
3055 else
3056 (SS.add (cons, x), x)
3057 in
3058 ((L'.SgiClassAbs (x, n), loc) :: sgis, cons, vals, sgns, strs)
3059 end
3060 | L'.SgiClass (x, n, c) =>
3061 let
3062 val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc)
3063
3064 val (cons, x) =
3065 if SS.member (cons, x) then
3066 (cons, "?" ^ x)
3067 else
3068 (SS.add (cons, x), x)
3069 in
3070 ((L'.SgiClass (x, n, c), loc) :: sgis, cons, vals, sgns, strs)
2952 end) 3071 end)
2953 3072
2954 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis 3073 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
2955 in 3074 in
2956 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs) 3075 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs)