Mercurial > urweb
comparison src/elaborate.sml @ 1270:9fd0cb0ef6e1
Try harder to place wildified 'con' declarations properly
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 01 Jun 2010 12:50:53 -0400 |
parents | 9f4b9315810d |
children | 74150edf1134 |
comparison
equal
deleted
inserted
replaced
1269:9f4b9315810d | 1270:9fd0cb0ef6e1 |
---|---|
1653 | _ => NONE | 1653 | _ => NONE |
1654 in | 1654 in |
1655 findHead e | 1655 findHead e |
1656 end | 1656 end |
1657 | 1657 |
1658 datatype needed = Needed of {Cons : (L'.kind * L'.con option) SM.map, | 1658 datatype needed = Needed of {Cons : (string option * L'.kind * L'.con option) SM.map, |
1659 Constraints : (E.env * (L'.con * L'.con) * ErrorMsg.span) list, | 1659 Constraints : (E.env * (L'.con * L'.con) * ErrorMsg.span) list, |
1660 Vals : SS.set, | 1660 Vals : SS.set, |
1661 Mods : needed SM.map} | 1661 Mods : (E.env * needed) SM.map} |
1662 | 1662 |
1663 fun ncons (Needed r) = #Cons r | 1663 fun ncons (Needed r) = #Cons r |
1664 fun nconstraints (Needed r) = #Constraints r | 1664 fun nconstraints (Needed r) = #Constraints r |
1665 fun nvals (Needed r) = #Vals r | 1665 fun nvals (Needed r) = #Vals r |
1666 fun nmods (Needed r) = #Mods r | 1666 fun nmods (Needed r) = #Mods r |
2160 foldl (fn ((c1, c2), denv) => | 2160 foldl (fn ((c1, c2), denv) => |
2161 D.assert env denv (c1, c2)) denv (collect true (st, sgn)) | 2161 D.assert env denv (c1, c2)) denv (collect true (st, sgn)) |
2162 end | 2162 end |
2163 | 2163 |
2164 fun elabSgn_item ((sgi, loc), (env, denv, gs)) = | 2164 fun elabSgn_item ((sgi, loc), (env, denv, gs)) = |
2165 case sgi of | 2165 ((*Print.preface ("elabSgi", SourcePrint.p_sgn_item (sgi, loc));*) |
2166 L.SgiConAbs (x, k) => | 2166 case sgi of |
2167 let | 2167 L.SgiConAbs (x, k) => |
2168 val k' = elabKind env k | 2168 let |
2169 | 2169 val k' = elabKind env k |
2170 val (env', n) = E.pushCNamed env x k' NONE | 2170 |
2171 in | 2171 val (env', n) = E.pushCNamed env x k' NONE |
2172 ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs)) | 2172 in |
2173 end | 2173 ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs)) |
2174 | 2174 end |
2175 | L.SgiCon (x, ko, c) => | 2175 |
2176 let | 2176 | L.SgiCon (x, ko, c) => |
2177 val k' = case ko of | 2177 let |
2178 NONE => kunif loc | 2178 val k' = case ko of |
2179 | SOME k => elabKind env k | 2179 NONE => kunif loc |
2180 | 2180 | SOME k => elabKind env k |
2181 val (c', ck, gs') = elabCon (env, denv) c | 2181 |
2182 val (env', n) = E.pushCNamed env x k' (SOME c') | 2182 val (c', ck, gs') = elabCon (env, denv) c |
2183 in | 2183 val (env', n) = E.pushCNamed env x k' (SOME c') |
2184 checkKind env c' ck k'; | 2184 in |
2185 | 2185 checkKind env c' ck k'; |
2186 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) | 2186 |
2187 end | 2187 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) |
2188 | 2188 end |
2189 | L.SgiDatatype dts => | 2189 |
2190 let | 2190 | L.SgiDatatype dts => |
2191 val k = (L'.KType, loc) | 2191 let |
2192 | 2192 val k = (L'.KType, loc) |
2193 val (dts, env) = ListUtil.foldlMap (fn ((x, xs, xcs), env) => | 2193 |
2194 val (dts, env) = ListUtil.foldlMap (fn ((x, xs, xcs), env) => | |
2195 let | |
2196 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs | |
2197 val (env, n) = E.pushCNamed env x k' NONE | |
2198 in | |
2199 ((x, n, xs, xcs), env) | |
2200 end) | |
2201 env dts | |
2202 | |
2203 val (dts, env) = ListUtil.foldlMap | |
2204 (fn ((x, n, xs, xcs), env) => | |
2205 let | |
2206 val t = (L'.CNamed n, loc) | |
2207 val nxs = length xs - 1 | |
2208 val t = ListUtil.foldli (fn (i, _, t) => | |
2209 (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs | |
2210 | |
2211 val (env', denv') = foldl (fn (x, (env', denv')) => | |
2212 (E.pushCRel env' x k, | |
2213 D.enter denv')) (env, denv) xs | |
2214 | |
2215 val (xcs, (used, env, gs)) = | |
2216 ListUtil.foldlMap | |
2217 (fn ((x, to), (used, env, gs)) => | |
2218 let | |
2219 val (to, t, gs') = case to of | |
2220 NONE => (NONE, t, gs) | |
2221 | SOME t' => | |
2222 let | |
2223 val (t', tk, gs') = | |
2224 elabCon (env', denv') t' | |
2225 in | |
2226 checkKind env' t' tk k; | |
2227 (SOME t', | |
2228 (L'.TFun (t', t), loc), | |
2229 gs' @ gs) | |
2230 end | |
2231 val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) | |
2232 t xs | |
2233 | |
2234 val (env, n') = E.pushENamed env x t | |
2235 in | |
2236 if SS.member (used, x) then | |
2237 strError env (DuplicateConstructor (x, loc)) | |
2238 else | |
2239 (); | |
2240 ((x, n', to), (SS.add (used, x), env, gs')) | |
2241 end) | |
2242 (SS.empty, env, []) xcs | |
2243 in | |
2244 ((x, n, xs, xcs), E.pushDatatype env n xs xcs) | |
2245 end) | |
2246 env dts | |
2247 in | |
2248 ([(L'.SgiDatatype dts, loc)], (env, denv, gs)) | |
2249 end | |
2250 | |
2251 | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp" | |
2252 | |
2253 | L.SgiDatatypeImp (x, m1 :: ms, s) => | |
2254 (case E.lookupStr env m1 of | |
2255 NONE => (strError env (UnboundStr (loc, m1)); | |
2256 ([], (env, denv, gs))) | |
2257 | SOME (n, sgn) => | |
2258 let | |
2259 val (str, sgn) = foldl (fn (m, (str, sgn)) => | |
2260 case E.projectStr env {sgn = sgn, str = str, field = m} of | |
2261 NONE => (conError env (UnboundStrInCon (loc, m)); | |
2262 (strerror, sgnerror)) | |
2263 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) | |
2264 ((L'.StrVar n, loc), sgn) ms | |
2265 in | |
2266 case hnormCon env (L'.CModProj (n, ms, s), loc) of | |
2267 (L'.CModProj (n, ms, s), _) => | |
2268 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of | |
2269 NONE => (conError env (UnboundDatatype (loc, s)); | |
2270 ([], (env, denv, []))) | |
2271 | SOME (xs, xncs) => | |
2272 let | |
2273 val k = (L'.KType, loc) | |
2274 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs | |
2275 | |
2276 val t = (L'.CModProj (n, ms, s), loc) | |
2277 val (env, n') = E.pushCNamed env x k' (SOME t) | |
2278 val env = E.pushDatatype env n' xs xncs | |
2279 | |
2280 val t = (L'.CNamed n', loc) | |
2281 val env = foldl (fn ((x, n, to), env) => | |
2194 let | 2282 let |
2195 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs | 2283 val t = case to of |
2196 val (env, n) = E.pushCNamed env x k' NONE | 2284 NONE => t |
2285 | SOME t' => (L'.TFun (t', t), loc) | |
2286 | |
2287 val t = foldr (fn (x, t) => | |
2288 (L'.TCFun (L'.Implicit, x, k, t), loc)) | |
2289 t xs | |
2197 in | 2290 in |
2198 ((x, n, xs, xcs), env) | 2291 E.pushENamedAs env x n t |
2199 end) | 2292 end) env xncs |
2200 env dts | 2293 in |
2201 | 2294 ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, [])) |
2202 val (dts, env) = ListUtil.foldlMap | 2295 end) |
2203 (fn ((x, n, xs, xcs), env) => | 2296 | _ => (strError env (NotDatatype loc); |
2204 let | 2297 ([], (env, denv, []))) |
2205 val t = (L'.CNamed n, loc) | 2298 end) |
2206 val nxs = length xs - 1 | 2299 |
2207 val t = ListUtil.foldli (fn (i, _, t) => | 2300 | L.SgiVal (x, c) => |
2208 (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs | 2301 let |
2209 | 2302 val (c', ck, gs') = elabCon (env, denv) c |
2210 val (env', denv') = foldl (fn (x, (env', denv')) => | 2303 |
2211 (E.pushCRel env' x k, | 2304 val old = c' |
2212 D.enter denv')) (env, denv) xs | 2305 val c' = normClassConstraint env c' |
2213 | 2306 val (env', n) = E.pushENamed env x c' |
2214 val (xcs, (used, env, gs)) = | 2307 in |
2215 ListUtil.foldlMap | 2308 (unifyKinds env ck ktype |
2216 (fn ((x, to), (used, env, gs)) => | 2309 handle KUnify ue => strError env (NotType (loc, ck, ue))); |
2217 let | 2310 |
2218 val (to, t, gs') = case to of | 2311 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) |
2219 NONE => (NONE, t, gs) | 2312 end |
2220 | SOME t' => | 2313 |
2221 let | 2314 | L.SgiTable (x, c, pe, ce) => |
2222 val (t', tk, gs') = | 2315 let |
2223 elabCon (env', denv') t' | 2316 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc) |
2224 in | 2317 |
2225 checkKind env' t' tk k; | 2318 val (c', ck, gs') = elabCon (env, denv) c |
2226 (SOME t', | 2319 val pkey = cunif (loc, cstK) |
2227 (L'.TFun (t', t), loc), | 2320 val visible = cunif (loc, cstK) |
2228 gs' @ gs) | 2321 val (env', ds, uniques) = |
2229 end | 2322 case (#1 pe, #1 ce) of |
2230 val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) | 2323 (L.EVar (["Basis"], "no_primary_key", _), L.EVar (["Basis"], "no_constraint", _)) => |
2231 t xs | 2324 let |
2232 | 2325 val x' = x ^ "_hidden_constraints" |
2233 val (env, n') = E.pushENamed env x t | 2326 val (env', hidden_n) = E.pushCNamed env x' cstK NONE |
2234 in | 2327 val hidden = (L'.CNamed hidden_n, loc) |
2235 if SS.member (used, x) then | 2328 in |
2236 strError env (DuplicateConstructor (x, loc)) | 2329 (env', [(L'.SgiConAbs (x', hidden_n, cstK), loc)], (L'.CConcat (visible, hidden), loc)) |
2237 else | 2330 end |
2238 (); | 2331 | _ => (env, [], visible) |
2239 ((x, n', to), (SS.add (used, x), env, gs')) | 2332 |
2240 end) | 2333 val ct = tableOf () |
2241 (SS.empty, env, []) xcs | 2334 val ct = (L'.CApp (ct, c'), loc) |
2242 in | 2335 val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc) |
2243 ((x, n, xs, xcs), E.pushDatatype env n xs xcs) | 2336 |
2244 end) | 2337 val (pe', pet, gs'') = elabExp (env', denv) pe |
2245 env dts | 2338 val gs'' = List.mapPartial (fn Disjoint x => SOME x |
2246 in | |
2247 ([(L'.SgiDatatype dts, loc)], (env, denv, gs)) | |
2248 end | |
2249 | |
2250 | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp" | |
2251 | |
2252 | L.SgiDatatypeImp (x, m1 :: ms, s) => | |
2253 (case E.lookupStr env m1 of | |
2254 NONE => (strError env (UnboundStr (loc, m1)); | |
2255 ([], (env, denv, gs))) | |
2256 | SOME (n, sgn) => | |
2257 let | |
2258 val (str, sgn) = foldl (fn (m, (str, sgn)) => | |
2259 case E.projectStr env {sgn = sgn, str = str, field = m} of | |
2260 NONE => (conError env (UnboundStrInCon (loc, m)); | |
2261 (strerror, sgnerror)) | |
2262 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) | |
2263 ((L'.StrVar n, loc), sgn) ms | |
2264 in | |
2265 case hnormCon env (L'.CModProj (n, ms, s), loc) of | |
2266 (L'.CModProj (n, ms, s), _) => | |
2267 (case E.projectDatatype env {sgn = sgn, str = str, field = s} of | |
2268 NONE => (conError env (UnboundDatatype (loc, s)); | |
2269 ([], (env, denv, []))) | |
2270 | SOME (xs, xncs) => | |
2271 let | |
2272 val k = (L'.KType, loc) | |
2273 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs | |
2274 | |
2275 val t = (L'.CModProj (n, ms, s), loc) | |
2276 val (env, n') = E.pushCNamed env x k' (SOME t) | |
2277 val env = E.pushDatatype env n' xs xncs | |
2278 | |
2279 val t = (L'.CNamed n', loc) | |
2280 val env = foldl (fn ((x, n, to), env) => | |
2281 let | |
2282 val t = case to of | |
2283 NONE => t | |
2284 | SOME t' => (L'.TFun (t', t), loc) | |
2285 | |
2286 val t = foldr (fn (x, t) => | |
2287 (L'.TCFun (L'.Implicit, x, k, t), loc)) | |
2288 t xs | |
2289 in | |
2290 E.pushENamedAs env x n t | |
2291 end) env xncs | |
2292 in | |
2293 ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, [])) | |
2294 end) | |
2295 | _ => (strError env (NotDatatype loc); | |
2296 ([], (env, denv, []))) | |
2297 end) | |
2298 | |
2299 | L.SgiVal (x, c) => | |
2300 let | |
2301 val (c', ck, gs') = elabCon (env, denv) c | |
2302 | |
2303 val old = c' | |
2304 val c' = normClassConstraint env c' | |
2305 val (env', n) = E.pushENamed env x c' | |
2306 in | |
2307 (unifyKinds env ck ktype | |
2308 handle KUnify ue => strError env (NotType (loc, ck, ue))); | |
2309 | |
2310 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) | |
2311 end | |
2312 | |
2313 | L.SgiTable (x, c, pe, ce) => | |
2314 let | |
2315 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc) | |
2316 | |
2317 val (c', ck, gs') = elabCon (env, denv) c | |
2318 val pkey = cunif (loc, cstK) | |
2319 val visible = cunif (loc, cstK) | |
2320 val (env', ds, uniques) = | |
2321 case (#1 pe, #1 ce) of | |
2322 (L.EVar (["Basis"], "no_primary_key", _), L.EVar (["Basis"], "no_constraint", _)) => | |
2323 let | |
2324 val x' = x ^ "_hidden_constraints" | |
2325 val (env', hidden_n) = E.pushCNamed env x' cstK NONE | |
2326 val hidden = (L'.CNamed hidden_n, loc) | |
2327 in | |
2328 (env', [(L'.SgiConAbs (x', hidden_n, cstK), loc)], (L'.CConcat (visible, hidden), loc)) | |
2329 end | |
2330 | _ => (env, [], visible) | |
2331 | |
2332 val ct = tableOf () | |
2333 val ct = (L'.CApp (ct, c'), loc) | |
2334 val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc) | |
2335 | |
2336 val (pe', pet, gs'') = elabExp (env', denv) pe | |
2337 val gs'' = List.mapPartial (fn Disjoint x => SOME x | |
2338 | _ => NONE) gs'' | 2339 | _ => NONE) gs'' |
2339 | 2340 |
2340 val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc) | 2341 val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc) |
2341 val pst = (L'.CApp (pst, c'), loc) | 2342 val pst = (L'.CApp (pst, c'), loc) |
2342 val pst = (L'.CApp (pst, pkey), loc) | 2343 val pst = (L'.CApp (pst, pkey), loc) |
2343 | 2344 |
2344 val (env', n) = E.pushENamed env' x ct | 2345 val (env', n) = E.pushENamed env' x ct |
2345 | 2346 |
2346 val (ce', cet, gs''') = elabExp (env', denv) ce | 2347 val (ce', cet, gs''') = elabExp (env', denv) ce |
2347 val gs''' = List.mapPartial (fn Disjoint x => SOME x | 2348 val gs''' = List.mapPartial (fn Disjoint x => SOME x |
2348 | _ => NONE) gs''' | 2349 | _ => NONE) gs''' |
2349 | 2350 |
2350 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc) | 2351 val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc) |
2351 val cst = (L'.CApp (cst, c'), loc) | 2352 val cst = (L'.CApp (cst, c'), loc) |
2352 val cst = (L'.CApp (cst, visible), loc) | 2353 val cst = (L'.CApp (cst, visible), loc) |
2353 in | 2354 in |
2354 checkKind env c' ck (L'.KRecord (L'.KType, loc), loc); | 2355 checkKind env c' ck (L'.KRecord (L'.KType, loc), loc); |
2355 checkCon env' pe' pet pst; | 2356 checkCon env' pe' pet pst; |
2356 checkCon env' ce' cet cst; | 2357 checkCon env' ce' cet cst; |
2357 | 2358 |
2358 (ds @ [(L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs)) | 2359 (ds @ [(L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs)) |
2359 end | 2360 end |
2360 | 2361 |
2361 | L.SgiStr (x, sgn) => | 2362 | L.SgiStr (x, sgn) => |
2362 let | 2363 let |
2363 val (sgn', gs') = elabSgn (env, denv) sgn | 2364 val (sgn', gs') = elabSgn (env, denv) sgn |
2364 val (env', n) = E.pushStrNamed env x sgn' | 2365 val (env', n) = E.pushStrNamed env x sgn' |
2365 in | 2366 in |
2366 ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs)) | 2367 ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs)) |
2367 end | 2368 end |
2368 | 2369 |
2369 | L.SgiSgn (x, sgn) => | 2370 | L.SgiSgn (x, sgn) => |
2370 let | 2371 let |
2371 val (sgn', gs') = elabSgn (env, denv) sgn | 2372 val (sgn', gs') = elabSgn (env, denv) sgn |
2372 val (env', n) = E.pushSgnNamed env x sgn' | 2373 val (env', n) = E.pushSgnNamed env x sgn' |
2373 in | 2374 in |
2374 ([(L'.SgiSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs)) | 2375 ([(L'.SgiSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs)) |
2375 end | 2376 end |
2376 | 2377 |
2377 | L.SgiInclude sgn => | 2378 | L.SgiInclude sgn => |
2378 let | 2379 let |
2379 val (sgn', gs') = elabSgn (env, denv) sgn | 2380 val (sgn', gs') = elabSgn (env, denv) sgn |
2380 in | 2381 in |
2381 case #1 (hnormSgn env sgn') of | 2382 case #1 (hnormSgn env sgn') of |
2382 L'.SgnConst sgis => | 2383 L'.SgnConst sgis => |
2383 (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, denv, gs' @ gs)) | 2384 (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, denv, gs' @ gs)) |
2384 | _ => (sgnError env (NotIncludable sgn'); | 2385 | _ => (sgnError env (NotIncludable sgn'); |
2385 ([], (env, denv, []))) | 2386 ([], (env, denv, []))) |
2386 end | 2387 end |
2387 | 2388 |
2388 | L.SgiConstraint (c1, c2) => | 2389 | L.SgiConstraint (c1, c2) => |
2389 let | 2390 let |
2390 val (c1', k1, gs1) = elabCon (env, denv) c1 | 2391 val (c1', k1, gs1) = elabCon (env, denv) c1 |
2391 val (c2', k2, gs2) = elabCon (env, denv) c2 | 2392 val (c2', k2, gs2) = elabCon (env, denv) c2 |
2392 | 2393 |
2393 val denv = D.assert env denv (c1', c2') | 2394 val denv = D.assert env denv (c1', c2') |
2394 in | 2395 in |
2395 checkKind env c1' k1 (L'.KRecord (kunif loc), loc); | 2396 checkKind env c1' k1 (L'.KRecord (kunif loc), loc); |
2396 checkKind env c2' k2 (L'.KRecord (kunif loc), loc); | 2397 checkKind env c2' k2 (L'.KRecord (kunif loc), loc); |
2397 | 2398 |
2398 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2)) | 2399 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2)) |
2399 end | 2400 end |
2400 | 2401 |
2401 | L.SgiClassAbs (x, k) => | 2402 | L.SgiClassAbs (x, k) => |
2402 let | 2403 let |
2403 val k = elabKind env k | 2404 val k = elabKind env k |
2404 val (env, n) = E.pushCNamed env x k NONE | 2405 val (env, n) = E.pushCNamed env x k NONE |
2405 val env = E.pushClass env n | 2406 val env = E.pushClass env n |
2406 in | 2407 in |
2407 ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, [])) | 2408 ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, [])) |
2408 end | 2409 end |
2409 | 2410 |
2410 | L.SgiClass (x, k, c) => | 2411 | L.SgiClass (x, k, c) => |
2411 let | 2412 let |
2412 val k = elabKind env k | 2413 val k = elabKind env k |
2413 val (c', ck, gs) = elabCon (env, denv) c | 2414 val (c', ck, gs) = elabCon (env, denv) c |
2414 val (env, n) = E.pushCNamed env x k (SOME c') | 2415 val (env, n) = E.pushCNamed env x k (SOME c') |
2415 val env = E.pushClass env n | 2416 val env = E.pushClass env n |
2416 in | 2417 in |
2417 checkKind env c' ck k; | 2418 checkKind env c' ck k; |
2418 ([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, [])) | 2419 ([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, [])) |
2419 end | 2420 end) |
2420 | 2421 |
2421 and elabSgn (env, denv) (sgn, loc) = | 2422 and elabSgn (env, denv) (sgn, loc) = |
2422 case sgn of | 2423 case sgn of |
2423 L.SgnConst sgis => | 2424 L.SgnConst sgis => |
2424 let | 2425 let |
3183 case #1 (hnormSgn env sgn) of | 3184 case #1 (hnormSgn env sgn) of |
3184 L'.SgnConst sgis => | 3185 L'.SgnConst sgis => |
3185 (case #1 str of | 3186 (case #1 str of |
3186 L.StrConst ds => | 3187 L.StrConst ds => |
3187 let | 3188 let |
3189 fun cname d = | |
3190 case d of | |
3191 L'.SgiCon (x, _, _, _) => SOME x | |
3192 | L'.SgiConAbs (x, _, _) => SOME x | |
3193 | L'.SgiClass (x, _, _, _) => SOME x | |
3194 | L'.SgiClassAbs (x, _, _) => SOME x | |
3195 | _ => NONE | |
3196 | |
3197 fun dname (d, _) = | |
3198 case d of | |
3199 L.DCon (x, _, _) => SOME x | |
3200 | L.DClass (x, _, _) => SOME x | |
3201 | _ => NONE | |
3202 | |
3188 fun decompileKind (k, loc) = | 3203 fun decompileKind (k, loc) = |
3189 case k of | 3204 case k of |
3190 L'.KType => SOME (L.KType, loc) | 3205 L'.KType => SOME (L.KType, loc) |
3191 | L'.KArrow (k1, k2) => | 3206 | L'.KArrow (k1, k2) => |
3192 (case (decompileKind k1, decompileKind k2) of | 3207 (case (decompileKind k1, decompileKind k2) of |
3257 | L'.CUnif (_, _, _, ref (SOME c)) => decompileCon env c | 3272 | L'.CUnif (_, _, _, ref (SOME c)) => decompileCon env c |
3258 | 3273 |
3259 | _ => NONE | 3274 | _ => NONE |
3260 | 3275 |
3261 fun buildNeeded env sgis = | 3276 fun buildNeeded env sgis = |
3262 #1 (foldl (fn ((sgi, loc), (nd, env')) => | 3277 #1 (foldl (fn ((sgi, loc), (nd, env', lastCon)) => |
3263 (case sgi of | 3278 (case sgi of |
3264 L'.SgiCon (x, _, k, c) => naddCon (nd, x, (k, SOME c)) | 3279 L'.SgiCon (x, _, k, c) => naddCon (nd, x, (lastCon, k, SOME c)) |
3265 | L'.SgiConAbs (x, _, k) => naddCon (nd, x, (k, NONE)) | 3280 | L'.SgiConAbs (x, _, k) => naddCon (nd, x, (lastCon, k, NONE)) |
3266 | L'.SgiConstraint cs => naddConstraint (nd, (env', cs, loc)) | 3281 | L'.SgiConstraint cs => naddConstraint (nd, (env', cs, loc)) |
3267 | L'.SgiVal (x, _, t) => | 3282 | L'.SgiVal (x, _, t) => |
3268 let | 3283 let |
3269 val t = normClassConstraint env' t | 3284 val t = normClassConstraint env' t |
3270 in | 3285 in |
3271 case #1 t of | 3286 case #1 t of |
3272 L'.CApp (f, _) => | 3287 L'.CApp (f, _) => |
3273 if isClassOrFolder env' f then | 3288 if isClassOrFolder env' f then |
3274 naddVal (nd, x) | 3289 naddVal (nd, x) |
3275 else | 3290 else |
3276 nd | 3291 nd |
3277 | _ => nd | 3292 | _ => nd |
3278 end | 3293 end |
3279 | L'.SgiStr (x, _, s) => | 3294 | L'.SgiStr (x, _, s) => |
3280 (case #1 (hnormSgn env s) of | 3295 (case #1 (hnormSgn env' s) of |
3281 L'.SgnConst sgis' => naddMod (nd, x, buildNeeded env sgis') | 3296 L'.SgnConst sgis' => naddMod (nd, x, (env', buildNeeded env' sgis')) |
3282 | _ => nd) | 3297 | _ => nd) |
3283 | _ => nd, | 3298 | _ => nd, |
3284 E.sgiBinds env' (sgi, loc))) | 3299 E.sgiBinds env' (sgi, loc), |
3285 (nempty, env) sgis) | 3300 case cname sgi of |
3301 NONE => lastCon | |
3302 | v => v)) | |
3303 (nempty, env, NONE) sgis) | |
3286 | 3304 |
3287 val nd = buildNeeded env sgis | 3305 val nd = buildNeeded env sgis |
3288 | 3306 |
3289 fun removeUsed (nd, ds) = | 3307 fun removeUsed (nd, ds) = |
3290 foldl (fn ((d, _), nd) => | 3308 foldl (fn ((d, _), nd) => |
3294 | L.DVal (x, _, _) => ndelVal (nd, x) | 3312 | L.DVal (x, _, _) => ndelVal (nd, x) |
3295 | L.DOpen _ => nempty | 3313 | L.DOpen _ => nempty |
3296 | L.DStr (x, _, (L.StrConst ds', _)) => | 3314 | L.DStr (x, _, (L.StrConst ds', _)) => |
3297 (case SM.find (nmods nd, x) of | 3315 (case SM.find (nmods nd, x) of |
3298 NONE => nd | 3316 NONE => nd |
3299 | SOME nd' => naddMod (nd, x, removeUsed (nd', ds'))) | 3317 | SOME (env, nd') => naddMod (nd, x, (env, removeUsed (nd', ds')))) |
3300 | _ => nd) | 3318 | _ => nd) |
3301 nd ds | 3319 nd ds |
3302 | 3320 |
3303 val nd = removeUsed (nd, ds) | 3321 val nd = removeUsed (nd, ds) |
3304 | 3322 |
3305 fun extend (nd, ds) = | 3323 fun extend (env, nd, ds) = |
3306 let | 3324 let |
3307 val ds' = List.mapPartial (fn (env', (c1, c2), loc) => | 3325 val ds' = List.mapPartial (fn (env', (c1, c2), loc) => |
3308 case (decompileCon env' c1, decompileCon env' c2) of | 3326 case (decompileCon env' c1, decompileCon env' c2) of |
3309 (SOME c1, SOME c2) => | 3327 (SOME c1, SOME c2) => |
3310 SOME (L.DConstraint (c1, c2), loc) | 3328 SOME (L.DConstraint (c1, c2), loc) |
3319 val ds'' = map (fn x => (L.DVal (x, NONE, ewild), #2 str)) xs | 3337 val ds'' = map (fn x => (L.DVal (x, NONE, ewild), #2 str)) xs |
3320 in | 3338 in |
3321 ds'' @ ds' | 3339 ds'' @ ds' |
3322 end | 3340 end |
3323 | 3341 |
3324 val ds' = | 3342 val ds = ds @ ds' |
3343 | |
3344 val ds = | |
3325 case SM.listItemsi (ncons nd) of | 3345 case SM.listItemsi (ncons nd) of |
3326 [] => ds' | 3346 [] => ds |
3327 | xs => | 3347 | xs => |
3328 let | 3348 let |
3329 val ds'' = map (fn (x, (k, co)) => | 3349 fun findPlace ((x, (lastCon, k, co)), ds') = |
3330 let | 3350 let |
3331 val k = | 3351 val k = |
3332 case decompileKind k of | 3352 case decompileKind k of |
3333 NONE => (L.KWild, #2 str) | 3353 NONE => (L.KWild, #2 str) |
3334 | SOME k => k | 3354 | SOME k => k |
3335 | 3355 |
3336 val cwild = (L.CWild k, #2 str) | 3356 val cwild = (L.CWild k, #2 str) |
3337 val c = | 3357 val c = |
3338 case co of | 3358 case co of |
3339 NONE => cwild | 3359 NONE => cwild |
3340 | SOME c => | 3360 | SOME c => |
3341 case decompileCon env c of | 3361 case decompileCon env c of |
3342 NONE => cwild | 3362 NONE => cwild |
3343 | SOME c' => c' | 3363 | SOME c' => c' |
3344 in | 3364 |
3345 (L.DCon (x, NONE, c), #2 str) | 3365 val d = (L.DCon (x, NONE, c), #2 str) |
3346 end) xs | 3366 in |
3367 case lastCon of | |
3368 NONE => d :: ds' | |
3369 | _ => | |
3370 let | |
3371 fun seek (ds'', passed) = | |
3372 case ds'' of | |
3373 [] => d :: ds' | |
3374 | d1 :: ds'' => | |
3375 if dname d1 = lastCon then | |
3376 List.revAppend (passed, d1 :: d :: ds'') | |
3377 else | |
3378 seek (ds'', d1 :: passed) | |
3379 in | |
3380 seek (ds', []) | |
3381 end | |
3382 end | |
3347 in | 3383 in |
3348 ds'' @ ds' | 3384 foldl findPlace ds xs |
3349 end | 3385 end |
3350 | |
3351 val ds = map (fn d as (L.DStr (x, s, (L.StrConst ds', loc')), loc) => | |
3352 (case SM.find (nmods nd, x) of | |
3353 NONE => d | |
3354 | SOME nd' => (L.DStr (x, s, (L.StrConst (extend (nd', ds')), loc')), loc)) | |
3355 | d => d) ds | |
3356 in | 3386 in |
3357 ds @ ds' | 3387 map (fn d as (L.DStr (x, s, (L.StrConst ds', loc')), loc) => |
3388 (case SM.find (nmods nd, x) of | |
3389 NONE => d | |
3390 | SOME (env, nd') => | |
3391 (L.DStr (x, s, (L.StrConst (extend (env, nd', ds')), loc')), loc)) | |
3392 | d => d) ds | |
3358 end | 3393 end |
3359 in | 3394 in |
3360 (L.StrConst (extend (nd, ds)), #2 str) | 3395 (L.StrConst (extend (env, nd, ds)), #2 str) |
3361 end | 3396 end |
3362 | _ => str) | 3397 | _ => str) |
3363 | _ => str | 3398 | _ => str |
3364 | 3399 |
3365 and elabDecl (dAll as (d, loc), (env, denv, gs)) = | 3400 and elabDecl (dAll as (d, loc), (env, denv, gs)) = |
4005 case sgn1 of | 4040 case sgn1 of |
4006 (L'.SgnFun (_, _, dom, _), _) => | 4041 (L'.SgnFun (_, _, dom, _), _) => |
4007 wildifyStr env (str2, dom) | 4042 wildifyStr env (str2, dom) |
4008 | _ => str2 | 4043 | _ => str2 |
4009 val (str2', sgn2, gs2) = elabStr (env, denv) str2 | 4044 val (str2', sgn2, gs2) = elabStr (env, denv) str2 |
4010 in | 4045 in |
4011 case #1 (hnormSgn env sgn1) of | 4046 case #1 (hnormSgn env sgn1) of |
4012 L'.SgnError => (strerror, sgnerror, []) | 4047 L'.SgnError => (strerror, sgnerror, []) |
4013 | L'.SgnFun (m, n, dom, ran) => | 4048 | L'.SgnFun (m, n, dom, ran) => |
4014 (subSgn env loc sgn2 dom; | 4049 (subSgn env loc sgn2 dom; |
4015 case #1 (hnormSgn env ran) of | 4050 case #1 (hnormSgn env ran) of |