Mercurial > urweb

comparison src/elaborate.sml @ 210:f4033abd6ab1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Inferring sql_type's
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 Aug 2008 12:35:46 -0400
parents 1487c712eb12
children e86411f647c6
comparison
equal deleted inserted replaced
209:1487c712eb12 210:f4033abd6ab1
44 val compare = String.compare 44 val compare = String.compare
45 end 45 end
46 46
47 structure SS = BinarySetFn(SK) 47 structure SS = BinarySetFn(SK)
48 structure SM = BinaryMapFn(SK) 48 structure SM = BinaryMapFn(SK)
49
50 val basis_r = ref 0
49 51
50 fun elabExplicitness e = 52 fun elabExplicitness e =
51 case e of 53 case e of
52 L.Explicit => L'.Explicit 54 L.Explicit => L'.Explicit
53 | L.Implicit => L'.Implicit 55 | L.Implicit => L'.Implicit
860 end 862 end
861 end 863 end
862 864
863 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = 865 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
864 let 866 let
865 fun err f = (prefaces "unifyCons'' fails" [("c1All", p_con env c1All), 867 fun err f = raise CUnify' (f (c1All, c2All))
866 ("c2All", p_con env c2All)];
867 raise CUnify' (f (c1All, c2All)))
868 868
869 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All) 869 fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All)
870 in 870 in
871 (*eprefaces "unifyCons''" [("c1All", p_con env c1All), 871 (*eprefaces "unifyCons''" [("c1All", p_con env c1All),
872 ("c2All", p_con env c2All)];*) 872 ("c2All", p_con env c2All)];*)
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 989
989 fun expError env err = 990 fun expError env err =
990 case err of 991 case err of
991 UnboundExp (loc, s) => 992 UnboundExp (loc, s) =>
992 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s) 993 ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
1025 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument" 1026 ErrorMsg.errorAt loc "Constructor expects argument but is used with no argument"
1026 | Inexhaustive loc => 1027 | Inexhaustive loc =>
1027 ErrorMsg.errorAt loc "Inexhaustive 'case'" 1028 ErrorMsg.errorAt loc "Inexhaustive 'case'"
1028 | DuplicatePatField (loc, s) => 1029 | DuplicatePatField (loc, s) =>
1029 ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern") 1030 ErrorMsg.errorAt loc ("Duplicate record field " ^ s ^ " in pattern")
1030 1031 | SqlInfer (loc, c) =>
1032 (ErrorMsg.errorAt loc "Can't infer SQL-ness of type";
1033 eprefaces' [("Type", p_con env c)])
1034
1031 fun checkCon (env, denv) e c1 c2 = 1035 fun checkCon (env, denv) e c1 c2 =
1032 unifyCons (env, denv) c1 c2 1036 unifyCons (env, denv) c1 c2
1033 handle CUnify (c1, c2, err) => 1037 handle CUnify (c1, c2, err) =>
1034 (expError env (Unify (e, c1, c2, err)); 1038 (expError env (Unify (e, c1, c2, err));
1035 []) 1039 [])
1412 cerror) 1416 cerror)
1413 | SOME t => t 1417 | SOME t => t
1414 in 1418 in
1415 ((L'.EModProj (n, ms, s), loc), t, []) 1419 ((L'.EModProj (n, ms, s), loc), t, [])
1416 end) 1420 end)
1421
1422 | L.EApp (e1, (L.ESqlInfer, _)) =>
1423 let
1424 val (e1', t1, gs1) = elabExp (env, denv) e1
1425 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
1426 val (t1, gs3) = hnormCon (env, denv) t1
1427 in
1428 case t1 of
1429 (L'.TFun ((L'.CApp ((L'.CModProj (basis, [], "sql_type"), _),
1430 t), _), ran), _) =>
1431 if basis <> !basis_r then
1432 raise Fail "Bad use of ESqlInfer [1]"
1433 else
1434 let
1435 val (t, gs4) = hnormCon (env, denv) t
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
1465 | L.ESqlInfer => raise Fail "Bad use of ESqlInfer [3]"
1417 1466
1418 | L.EApp (e1, e2) => 1467 | L.EApp (e1, e2) =>
1419 let 1468 let
1420 val (e1', t1, gs1) = elabExp (env, denv) e1 1469 val (e1', t1, gs1) = elabExp (env, denv) e1
1421 val (e1', t1, gs2) = elabHead (env, denv) e1' t1 1470 val (e1', t1, gs2) = elabHead (env, denv) e1' t1
1734 | NotDatatype loc => 1783 | NotDatatype loc =>
1735 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype" 1784 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
1736 1785
1737 val hnormSgn = E.hnormSgn 1786 val hnormSgn = E.hnormSgn
1738 1787
1739 fun tableOf' env = 1788 fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan)
1740 case E.lookupStr env "Basis" of
1741 NONE => raise Fail "Elaborate.tableOf: Can't find Basis"
1742 | SOME (n, _) => n
1743
1744 fun tableOf env = (L'.CModProj (tableOf' env, [], "sql_table"), ErrorMsg.dummySpan)
1745 1789
1746 fun elabSgn_item ((sgi, loc), (env, denv, gs)) = 1790 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
1747 case sgi of 1791 case sgi of
1748 L.SgiConAbs (x, k) => 1792 L.SgiConAbs (x, k) =>
1749 let 1793 let
1909 end 1953 end
1910 1954
1911 | L.SgiTable (x, c) => 1955 | L.SgiTable (x, c) =>
1912 let 1956 let
1913 val (c', k, gs) = elabCon (env, denv) c 1957 val (c', k, gs) = elabCon (env, denv) c
1914 val (env, n) = E.pushENamed env x (L'.CApp (tableOf env, c'), loc) 1958 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
1915 in 1959 in
1916 checkKind env c' k (L'.KRecord (L'.KType, loc), loc); 1960 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
1917 ([(L'.SgiTable (tableOf' env, x, n, c'), loc)], (env, denv, gs)) 1961 ([(L'.SgiTable (!basis_r, x, n, c'), loc)], (env, denv, gs))
1918 end 1962 end
1919 1963
1920 and elabSgn (env, denv) (sgn, loc) = 1964 and elabSgn (env, denv) (sgn, loc) =
1921 case sgn of 1965 case sgn of
1922 L.SgnConst sgis => 1966 L.SgnConst sgis =>
2112 | L'.SgiSgn (x, n, sgn) => 2156 | L'.SgiSgn (x, n, sgn) =>
2113 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc) 2157 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)
2114 | L'.SgiConstraint (c1, c2) => 2158 | L'.SgiConstraint (c1, c2) =>
2115 (L'.DConstraint (c1, c2), loc) 2159 (L'.DConstraint (c1, c2), loc)
2116 | L'.SgiTable (_, x, n, c) => 2160 | L'.SgiTable (_, x, n, c) =>
2117 (L'.DVal (x, n, (L'.CApp (tableOf env, c), loc), 2161 (L'.DVal (x, n, (L'.CApp (tableOf (), c), loc),
2118 (L'.EModProj (str, strs, x), loc)), loc) 2162 (L'.EModProj (str, strs, x), loc)), loc)
2119 in 2163 in
2120 (d, (E.declBinds env' d, denv')) 2164 (d, (E.declBinds env' d, denv'))
2121 end) 2165 end)
2122 (env, denv) sgis 2166 (env, denv) sgis
2361 SOME (env, denv)) 2405 SOME (env, denv))
2362 else 2406 else
2363 NONE 2407 NONE
2364 | L'.SgiTable (_, x', n1, c1) => 2408 | L'.SgiTable (_, x', n1, c1) =>
2365 if x = x' then 2409 if x = x' then
2366 (case unifyCons (env, denv) (L'.CApp (tableOf env, c1), loc) c2 of 2410 (case unifyCons (env, denv) (L'.CApp (tableOf (), c1), loc) c2 of
2367 [] => SOME (env, denv) 2411 [] => SOME (env, denv)
2368 | _ => NONE) 2412 | _ => NONE)
2369 handle CUnify (c1, c2, err) => 2413 handle CUnify (c1, c2, err) =>
2370 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); 2414 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
2371 SOME (env, denv)) 2415 SOME (env, denv))
2797 end 2841 end
2798 2842
2799 | L.DTable (x, c) => 2843 | L.DTable (x, c) =>
2800 let 2844 let
2801 val (c', k, gs') = elabCon (env, denv) c 2845 val (c', k, gs') = elabCon (env, denv) c
2802 val (env, n) = E.pushENamed env x (L'.CApp (tableOf env, c'), loc) 2846 val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc)
2803 in 2847 in
2804 checkKind env c' k (L'.KRecord (L'.KType, loc), loc); 2848 checkKind env c' k (L'.KRecord (L'.KType, loc), loc);
2805 ([(L'.DTable (tableOf' env, x, n, c'), loc)], (env, denv, gs' @ gs)) 2849 ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, gs' @ gs))
2806 end 2850 end
2807 2851
2808 and elabStr (env, denv) (str, loc) = 2852 and elabStr (env, denv) (str, loc) =
2809 case str of 2853 case str of
2810 L.StrConst ds => 2854 L.StrConst ds =>
2977 [("c1", p_con env c1), 3021 [("c1", p_con env c1),
2978 ("c2", p_con env c2)]) gs; 3022 ("c2", p_con env c2)]) gs;
2979 raise Fail "Unresolved disjointness constraints in Basis") 3023 raise Fail "Unresolved disjointness constraints in Basis")
2980 3024
2981 val (env', basis_n) = E.pushStrNamed env "Basis" sgn 3025 val (env', basis_n) = E.pushStrNamed env "Basis" sgn
3026 val () = basis_r := basis_n
2982 3027
2983 val (ds, (env', _)) = dopen (env', D.empty) {str = basis_n, strs = [], sgn = sgn} 3028 val (ds, (env', _)) = dopen (env', D.empty) {str = basis_n, strs = [], sgn = sgn}
2984 3029
2985 fun discoverC r x = 3030 fun discoverC r x =
2986 case E.lookupC env' x of 3031 case E.lookupC env' x of