Mercurial > urweb

comparison src/elaborate.sml @ 158:b4b70de488e9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More datatype module stuff
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Jul 2008 16:36:41 -0400
parents adc4e42e3adc
children 1e382d10e832
comparison
equal deleted inserted replaced
157:adc4e42e3adc 158:b4b70de488e9
1235 | NotFunctor of L'.sgn 1235 | NotFunctor of L'.sgn
1236 | FunctorRebind of ErrorMsg.span 1236 | FunctorRebind of ErrorMsg.span
1237 | UnOpenable of L'.sgn 1237 | UnOpenable of L'.sgn
1238 | NotType of L'.kind * (L'.kind * L'.kind * kunify_error) 1238 | NotType of L'.kind * (L'.kind * L'.kind * kunify_error)
1239 | DuplicateConstructor of string * ErrorMsg.span 1239 | DuplicateConstructor of string * ErrorMsg.span
1240 | NotDatatype of ErrorMsg.span
1240 1241
1241 fun strError env err = 1242 fun strError env err =
1242 case err of 1243 case err of
1243 UnboundStr (loc, s) => 1244 UnboundStr (loc, s) =>
1244 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s) 1245 ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
1256 ("Subkind 1", p_kind k1), 1257 ("Subkind 1", p_kind k1),
1257 ("Subkind 2", p_kind k2)]; 1258 ("Subkind 2", p_kind k2)];
1258 kunifyError ue) 1259 kunifyError ue)
1259 | DuplicateConstructor (x, loc) => 1260 | DuplicateConstructor (x, loc) =>
1260 ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x) 1261 ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
1262 | NotDatatype loc =>
1263 ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
1261 1264
1262 val hnormSgn = E.hnormSgn 1265 val hnormSgn = E.hnormSgn
1263 1266
1264 fun elabSgn_item ((sgi, loc), (env, denv, gs)) = 1267 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
1265 case sgi of 1268 case sgi of
1317 (SS.empty, env, []) xcs 1320 (SS.empty, env, []) xcs
1318 in 1321 in
1319 ([(L'.SgiDatatype (x, n, xcs), loc)], (env, denv, gs)) 1322 ([(L'.SgiDatatype (x, n, xcs), loc)], (env, denv, gs))
1320 end 1323 end
1321 1324
1322 | L.SgiDatatypeImp _ => raise Fail "Elaborate SgiDatatypeImp" 1325 | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp"
1326
1327 | L.SgiDatatypeImp (x, m1 :: ms, s) =>
1328 (case E.lookupStr env m1 of
1329 NONE => (strError env (UnboundStr (loc, m1));
1330 ([], (env, denv, gs)))
1331 | SOME (n, sgn) =>
1332 let
1333 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
1334 case E.projectStr env {sgn = sgn, str = str, field = m} of
1335 NONE => (conError env (UnboundStrInCon (loc, m));
1336 (strerror, sgnerror))
1337 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1338 ((L'.StrVar n, loc), sgn) ms
1339 in
1340 case E.projectDatatype env {sgn = sgn, str = str, field = s} of
1341 NONE => (conError env (UnboundDatatype (loc, s));
1342 ([], (env, denv, gs)))
1343 | SOME xncs =>
1344 let
1345 val k = (L'.KType, loc)
1346 val t = (L'.CModProj (n, ms, s), loc)
1347 val (env, n') = E.pushCNamed env x k (SOME t)
1348 val env = E.pushDatatype env n' xncs
1349
1350 val t = (L'.CNamed n', loc)
1351 val env = foldl (fn ((x, n, to), env) =>
1352 let
1353 val t = case to of
1354 NONE => t
1355 | SOME t' => (L'.TFun (t', t), loc)
1356 in
1357 E.pushENamedAs env x n t
1358 end) env xncs
1359 in
1360 ([(L'.SgiDatatypeImp (x, n', n, ms, s), loc)], (env, denv, []))
1361 end
1362 end)
1323 1363
1324 | L.SgiVal (x, c) => 1364 | L.SgiVal (x, c) =>
1325 let 1365 let
1326 val (c', ck, gs') = elabCon (env, denv) c 1366 val (c', ck, gs') = elabCon (env, denv) c
1327 1367
1499 | L'.SgnVar _ => sgn 1539 | L'.SgnVar _ => sgn
1500 1540
1501 | L'.SgnConst sgis => 1541 | L'.SgnConst sgis =>
1502 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) => 1542 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
1503 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) 1543 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
1544 | (L'.SgiDatatype (x, n, xncs), loc) =>
1545 (L'.SgiDatatypeImp (x, n, str, strs, x), loc)
1504 | (L'.SgiStr (x, n, sgn), loc) => 1546 | (L'.SgiStr (x, n, sgn), loc) =>
1505 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) 1547 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
1506 | x => x) sgis), #2 sgn) 1548 | x => x) sgis), #2 sgn)
1507 | L'.SgnFun _ => sgn 1549 | L'.SgnFun _ => sgn
1508 | L'.SgnWhere _ => sgn 1550 | L'.SgnWhere _ => sgn
1743 NONE) 1785 NONE)
1744 handle CUnify ue => mismatched (SOME ue) 1786 handle CUnify ue => mismatched (SOME ue)
1745 end 1787 end
1746 | _ => NONE) 1788 | _ => NONE)
1747 1789
1748 | L'.SgiDatatypeImp _ => raise Fail "SgiDatatypeImp in subsgn" 1790 | L'.SgiDatatypeImp (x, n2, m11, ms1, s1) =>
1791 seek (fn sgi1All as (sgi1, _) =>
1792 case sgi1 of
1793 L'.SgiDatatypeImp (x', n1, m12, ms2, s2) =>
1794 if x = x' then
1795 let
1796 val k = (L'.KType, loc)
1797 val t1 = (L'.CModProj (m11, ms1, s1), loc)
1798 val t2 = (L'.CModProj (m12, ms2, s2), loc)
1799
1800 fun good () =
1801 let
1802 val env = E.pushCNamedAs env x n1 k (SOME t1)
1803 val env = E.pushCNamedAs env x n2 k (SOME t2)
1804 in
1805 SOME (env, denv)
1806 end
1807 in
1808 (case unifyCons (env, denv) t1 t2 of
1809 [] => good ()
1810 | _ => NONE)
1811 handle CUnify (c1, c2, err) =>
1812 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
1813 good ())
1814 end
1815 else
1816 NONE
1817
1818 | _ => NONE)
1749 1819
1750 | L'.SgiVal (x, n2, c2) => 1820 | L'.SgiVal (x, n2, c2) =>
1751 seek (fn sgi1All as (sgi1, _) => 1821 seek (fn sgi1All as (sgi1, _) =>
1752 case sgi1 of 1822 case sgi1 of
1753 L'.SgiVal (x', n1, c1) => 1823 L'.SgiVal (x', n1, c1) =>
1902 NONE => (conError env (UnboundStrInCon (loc, m)); 1972 NONE => (conError env (UnboundStrInCon (loc, m));
1903 (strerror, sgnerror)) 1973 (strerror, sgnerror))
1904 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) 1974 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1905 ((L'.StrVar n, loc), sgn) ms 1975 ((L'.StrVar n, loc), sgn) ms
1906 in 1976 in
1907 case E.projectDatatype env {sgn = sgn, str = str, field = s} of 1977 case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
1908 NONE => (conError env (UnboundDatatype (loc, s)); 1978 ((L'.CModProj (n, ms, s), _), gs) =>
1909 ([], (env, denv, gs))) 1979 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
1910 | SOME xncs => 1980 NONE => (conError env (UnboundDatatype (loc, s));
1911 let 1981 ([], (env, denv, gs)))
1912 val k = (L'.KType, loc) 1982 | SOME xncs =>
1913 val t = (L'.CModProj (n, ms, s), loc) 1983 let
1914 val (env, n') = E.pushCNamed env x k (SOME t) 1984 val k = (L'.KType, loc)
1915 val env = E.pushDatatype env n' xncs 1985 val t = (L'.CModProj (n, ms, s), loc)
1916 1986 val (env, n') = E.pushCNamed env x k (SOME t)
1917 val t = (L'.CNamed n', loc) 1987 val env = E.pushDatatype env n' xncs
1918 val env = foldl (fn ((x, n, to), env) => 1988
1919 let 1989 val t = (L'.CNamed n', loc)
1920 val t = case to of 1990 val env = foldl (fn ((x, n, to), env) =>
1921 NONE => t 1991 let
1922 | SOME t' => (L'.TFun (t', t), loc) 1992 val t = case to of
1923 in 1993 NONE => t
1924 E.pushENamedAs env x n t 1994 | SOME t' => (L'.TFun (t', t), loc)
1925 end) env xncs 1995 in
1926 in 1996 E.pushENamedAs env x n t
1927 ([(L'.DDatatypeImp (x, n', n, ms, s), loc)], (env, denv, [])) 1997 end) env xncs
1928 end 1998 in
1999 ([(L'.DDatatypeImp (x, n', n, ms, s), loc)], (env, denv, gs))
2000 end)
2001 | _ => (strError env (NotDatatype loc);
2002 ([], (env, denv, [])))
1929 end) 2003 end)
1930 2004
1931 | L.DVal (x, co, e) => 2005 | L.DVal (x, co, e) =>
1932 let 2006 let
1933 val (c', _, gs1) = case co of 2007 val (c', _, gs1) = case co of
2033 | _ => str) 2107 | _ => str)
2034 | _ => str 2108 | _ => str
2035 2109
2036 val (str', actual, gs2) = elabStr (env, denv) str 2110 val (str', actual, gs2) = elabStr (env, denv) str
2037 in 2111 in
2038 subSgn (env, denv) actual formal; 2112 subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal;
2039 (str', formal, gs1 @ gs2) 2113 (str', formal, gs1 @ gs2)
2040 end 2114 end
2041 2115
2042 val (env', n) = E.pushStrNamed env x sgn' 2116 val (env', n) = E.pushStrNamed env x sgn'
2043 in 2117 in