Mercurial > urweb

comparison src/elaborate.sml @ 157:adc4e42e3adc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Basic datatype importing works
author Adam Chlipala <adamc@hcoop.net>
date Thu, 24 Jul 2008 15:49:30 -0400
parents 34ccd7d2bea8
children b4b70de488e9
comparison
equal deleted inserted replaced
156:34ccd7d2bea8 157:adc4e42e3adc
114 unifyKinds' k1 k2 114 unifyKinds' k1 k2
115 handle KUnify' err => raise KUnify (k1, k2, err) 115 handle KUnify' err => raise KUnify (k1, k2, err)
116 116
117 datatype con_error = 117 datatype con_error =
118 UnboundCon of ErrorMsg.span * string 118 UnboundCon of ErrorMsg.span * string
119 | UnboundDatatype of ErrorMsg.span * string
119 | UnboundStrInCon of ErrorMsg.span * string 120 | UnboundStrInCon of ErrorMsg.span * string
120 | WrongKind of L'.con * L'.kind * L'.kind * kunify_error 121 | WrongKind of L'.con * L'.kind * L'.kind * kunify_error
121 | DuplicateField of ErrorMsg.span * string 122 | DuplicateField of ErrorMsg.span * string
122 123
123 fun conError env err = 124 fun conError env err =
124 case err of 125 case err of
125 UnboundCon (loc, s) => 126 UnboundCon (loc, s) =>
126 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s) 127 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
128 | UnboundDatatype (loc, s) =>
129 ErrorMsg.errorAt loc ("Unbound datatype " ^ s)
127 | UnboundStrInCon (loc, s) => 130 | UnboundStrInCon (loc, s) =>
128 ErrorMsg.errorAt loc ("Unbound structure " ^ s) 131 ErrorMsg.errorAt loc ("Unbound structure " ^ s)
129 | WrongKind (c, k1, k2, kerr) => 132 | WrongKind (c, k1, k2, kerr) =>
130 (ErrorMsg.errorAt (#2 c) "Wrong kind"; 133 (ErrorMsg.errorAt (#2 c) "Wrong kind";
131 eprefaces' [("Constructor", p_con env c), 134 eprefaces' [("Constructor", p_con env c),
1281 checkKind env c' ck k'; 1284 checkKind env c' ck k';
1282 1285
1283 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) 1286 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs))
1284 end 1287 end
1285 1288
1286 | L.SgiDatatype _ => raise Fail "Elaborate SgiDatatype" 1289 | L.SgiDatatype (x, xcs) =>
1290 let
1291 val k = (L'.KType, loc)
1292 val (env, n) = E.pushCNamed env x k NONE
1293 val t = (L'.CNamed n, loc)
1294
1295 val (xcs, (used, env, gs)) =
1296 ListUtil.foldlMap
1297 (fn ((x, to), (used, env, gs)) =>
1298 let
1299 val (to, t, gs') = case to of
1300 NONE => (NONE, t, gs)
1301 | SOME t' =>
1302 let
1303 val (t', tk, gs') = elabCon (env, denv) t'
1304 in
1305 checkKind env t' tk k;
1306 (SOME t', (L'.TFun (t', t), loc), gs' @ gs)
1307 end
1308
1309 val (env, n') = E.pushENamed env x t
1310 in
1311 if SS.member (used, x) then
1312 strError env (DuplicateConstructor (x, loc))
1313 else
1314 ();
1315 ((x, n', to), (SS.add (used, x), env, gs'))
1316 end)
1317 (SS.empty, env, []) xcs
1318 in
1319 ([(L'.SgiDatatype (x, n, xcs), loc)], (env, denv, gs))
1320 end
1287 1321
1288 | L.SgiDatatypeImp _ => raise Fail "Elaborate SgiDatatypeImp" 1322 | L.SgiDatatypeImp _ => raise Fail "Elaborate SgiDatatypeImp"
1289 1323
1290 | L.SgiVal (x, c) => 1324 | L.SgiVal (x, c) =>
1291 let 1325 let
1853 (SS.empty, env, []) xcs 1887 (SS.empty, env, []) xcs
1854 in 1888 in
1855 ([(L'.DDatatype (x, n, xcs), loc)], (env, denv, gs)) 1889 ([(L'.DDatatype (x, n, xcs), loc)], (env, denv, gs))
1856 end 1890 end
1857 1891
1858 | L.DDatatypeImp _ => raise Fail "Elaborate DDatatypeImp" 1892 | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp"
1893
1894 | L.DDatatypeImp (x, m1 :: ms, s) =>
1895 (case E.lookupStr env m1 of
1896 NONE => (expError env (UnboundStrInExp (loc, m1));
1897 ([], (env, denv, gs)))
1898 | SOME (n, sgn) =>
1899 let
1900 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
1901 case E.projectStr env {sgn = sgn, str = str, field = m} of
1902 NONE => (conError env (UnboundStrInCon (loc, m));
1903 (strerror, sgnerror))
1904 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1905 ((L'.StrVar n, loc), sgn) ms
1906 in
1907 case E.projectDatatype env {sgn = sgn, str = str, field = s} of
1908 NONE => (conError env (UnboundDatatype (loc, s));
1909 ([], (env, denv, gs)))
1910 | SOME xncs =>
1911 let
1912 val k = (L'.KType, loc)
1913 val t = (L'.CModProj (n, ms, s), loc)
1914 val (env, n') = E.pushCNamed env x k (SOME t)
1915 val env = E.pushDatatype env n' xncs
1916
1917 val t = (L'.CNamed n', loc)
1918 val env = foldl (fn ((x, n, to), env) =>
1919 let
1920 val t = case to of
1921 NONE => t
1922 | SOME t' => (L'.TFun (t', t), loc)
1923 in
1924 E.pushENamedAs env x n t
1925 end) env xncs
1926 in
1927 ([(L'.DDatatypeImp (x, n', n, ms, s), loc)], (env, denv, []))
1928 end
1929 end)
1930
1859 | L.DVal (x, co, e) => 1931 | L.DVal (x, co, e) =>
1860 let 1932 let
1861 val (c', _, gs1) = case co of 1933 val (c', _, gs1) = case co of
1862 NONE => (cunif (loc, ktype), ktype, []) 1934 NONE => (cunif (loc, ktype), ktype, [])
1863 | SOME c => elabCon (env, denv) c 1935 | SOME c => elabCon (env, denv) c