Mercurial > urweb

comparison src/elaborate.sml @ 1270:9fd0cb0ef6e1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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