Mercurial > urweb
comparison src/elaborate.sml @ 805:e2780d2f4afc
Mutual datatypes through Elaborate
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 16 May 2009 15:14:17 -0400 |
parents | 9330ba3a2799 |
children | cb30dd2ba353 |
comparison
equal
deleted
inserted
replaced
804:10fe57e4a8c2 | 805:e2780d2f4afc |
---|---|
1969 checkKind env c' ck k'; | 1969 checkKind env c' ck k'; |
1970 | 1970 |
1971 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) | 1971 ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) |
1972 end | 1972 end |
1973 | 1973 |
1974 | L.SgiDatatype (x, xs, xcs) => | 1974 | L.SgiDatatype dts => |
1975 let | 1975 let |
1976 val k = (L'.KType, loc) | 1976 val k = (L'.KType, loc) |
1977 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs | 1977 |
1978 val (env, n) = E.pushCNamed env x k' NONE | 1978 val (dts, env) = ListUtil.foldlMap (fn ((x, xs, xcs), env) => |
1979 val t = (L'.CNamed n, loc) | 1979 let |
1980 val nxs = length xs - 1 | 1980 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs |
1981 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs | 1981 val (env, n) = E.pushCNamed env x k' NONE |
1982 | 1982 in |
1983 val (env', denv') = foldl (fn (x, (env', denv')) => | 1983 ((x, n, xs, xcs), env) |
1984 (E.pushCRel env' x k, | 1984 end) |
1985 D.enter denv')) (env, denv) xs | 1985 env dts |
1986 | 1986 |
1987 val (xcs, (used, env, gs)) = | 1987 val (dts, env) = ListUtil.foldlMap |
1988 ListUtil.foldlMap | 1988 (fn ((x, n, xs, xcs), env) => |
1989 (fn ((x, to), (used, env, gs)) => | 1989 let |
1990 let | 1990 val t = (L'.CNamed n, loc) |
1991 val (to, t, gs') = case to of | 1991 val nxs = length xs - 1 |
1992 NONE => (NONE, t, gs) | 1992 val t = ListUtil.foldli (fn (i, _, t) => |
1993 | SOME t' => | 1993 (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs |
1994 let | 1994 |
1995 val (t', tk, gs') = elabCon (env', denv') t' | 1995 val (env', denv') = foldl (fn (x, (env', denv')) => |
1996 in | 1996 (E.pushCRel env' x k, |
1997 checkKind env' t' tk k; | 1997 D.enter denv')) (env, denv) xs |
1998 (SOME t', (L'.TFun (t', t), loc), gs' @ gs) | 1998 |
1999 end | 1999 val (xcs, (used, env, gs)) = |
2000 val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs | 2000 ListUtil.foldlMap |
2001 | 2001 (fn ((x, to), (used, env, gs)) => |
2002 val (env, n') = E.pushENamed env x t | 2002 let |
2003 in | 2003 val (to, t, gs') = case to of |
2004 if SS.member (used, x) then | 2004 NONE => (NONE, t, gs) |
2005 strError env (DuplicateConstructor (x, loc)) | 2005 | SOME t' => |
2006 else | 2006 let |
2007 (); | 2007 val (t', tk, gs') = |
2008 ((x, n', to), (SS.add (used, x), env, gs')) | 2008 elabCon (env', denv') t' |
2009 end) | 2009 in |
2010 (SS.empty, env, []) xcs | 2010 checkKind env' t' tk k; |
2011 | 2011 (SOME t', |
2012 val env = E.pushDatatype env n xs xcs | 2012 (L'.TFun (t', t), loc), |
2013 gs' @ gs) | |
2014 end | |
2015 val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) | |
2016 t xs | |
2017 | |
2018 val (env, n') = E.pushENamed env x t | |
2019 in | |
2020 if SS.member (used, x) then | |
2021 strError env (DuplicateConstructor (x, loc)) | |
2022 else | |
2023 (); | |
2024 ((x, n', to), (SS.add (used, x), env, gs')) | |
2025 end) | |
2026 (SS.empty, env, []) xcs | |
2027 in | |
2028 ((x, n, xs, xcs), E.pushDatatype env n xs xcs) | |
2029 end) | |
2030 env dts | |
2013 in | 2031 in |
2014 ([(L'.SgiDatatype (x, n, xs, xcs), loc)], (env, denv, gs)) | 2032 ([(L'.SgiDatatype dts, loc)], (env, denv, gs)) |
2015 end | 2033 end |
2016 | 2034 |
2017 | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp" | 2035 | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp" |
2018 | 2036 |
2019 | L.SgiDatatypeImp (x, m1 :: ms, s) => | 2037 | L.SgiDatatypeImp (x, m1 :: ms, s) => |
2197 (if SS.member (cons, x) then | 2215 (if SS.member (cons, x) then |
2198 sgnError env (DuplicateCon (loc, x)) | 2216 sgnError env (DuplicateCon (loc, x)) |
2199 else | 2217 else |
2200 (); | 2218 (); |
2201 (SS.add (cons, x), vals, sgns, strs)) | 2219 (SS.add (cons, x), vals, sgns, strs)) |
2202 | L'.SgiDatatype (x, _, _, xncs) => | 2220 | L'.SgiDatatype dts => |
2203 let | 2221 let |
2204 val vals = foldl (fn ((x, _, _), vals) => | 2222 val (cons, vals) = |
2205 (if SS.member (vals, x) then | 2223 let |
2206 sgnError env (DuplicateVal (loc, x)) | 2224 fun doOne ((x, _, _, xncs), (cons, vals)) = |
2207 else | 2225 let |
2208 (); | 2226 val vals = foldl (fn ((x, _, _), vals) => |
2209 SS.add (vals, x))) | 2227 (if SS.member (vals, x) then |
2210 vals xncs | 2228 sgnError env (DuplicateVal (loc, x)) |
2229 else | |
2230 (); | |
2231 SS.add (vals, x))) | |
2232 vals xncs | |
2233 in | |
2234 if SS.member (cons, x) then | |
2235 sgnError env (DuplicateCon (loc, x)) | |
2236 else | |
2237 (); | |
2238 (SS.add (cons, x), vals) | |
2239 end | |
2240 in | |
2241 foldl doOne (cons, vals) dts | |
2242 end | |
2211 in | 2243 in |
2212 if SS.member (cons, x) then | 2244 (cons, vals, sgns, strs) |
2213 sgnError env (DuplicateCon (loc, x)) | |
2214 else | |
2215 (); | |
2216 (SS.add (cons, x), vals, sgns, strs) | |
2217 end | 2245 end |
2218 | L'.SgiDatatypeImp (x, _, _, _, _, _, _) => | 2246 | L'.SgiDatatypeImp (x, _, _, _, _, _, _) => |
2219 (if SS.member (cons, x) then | 2247 (if SS.member (cons, x) then |
2220 sgnError env (DuplicateCon (loc, x)) | 2248 sgnError env (DuplicateCon (loc, x)) |
2221 else | 2249 else |
2316 case #1 (hnormSgn env sgn) of | 2344 case #1 (hnormSgn env sgn) of |
2317 L'.SgnError => sgn | 2345 L'.SgnError => sgn |
2318 | L'.SgnVar _ => sgn | 2346 | L'.SgnVar _ => sgn |
2319 | 2347 |
2320 | L'.SgnConst sgis => | 2348 | L'.SgnConst sgis => |
2321 (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) => | 2349 (L'.SgnConst (ListUtil.mapConcat (fn (L'.SgiConAbs (x, n, k), loc) => |
2322 (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) | 2350 [(L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] |
2323 | (L'.SgiDatatype (x, n, xs, xncs), loc) => | 2351 | (L'.SgiDatatype dts, loc) => |
2324 (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc) | 2352 map (fn (x, n, xs, xncs) => (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts |
2325 | (L'.SgiClassAbs (x, n, k), loc) => | 2353 | (L'.SgiClassAbs (x, n, k), loc) => |
2326 (L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) | 2354 [(L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] |
2327 | (L'.SgiStr (x, n, sgn), loc) => | 2355 | (L'.SgiStr (x, n, sgn), loc) => |
2328 (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) | 2356 [(L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)] |
2329 | x => x) sgis), #2 sgn) | 2357 | x => [x]) sgis), #2 sgn) |
2330 | L'.SgnFun _ => sgn | 2358 | L'.SgnFun _ => sgn |
2331 | L'.SgnWhere _ => sgn | 2359 | L'.SgnWhere _ => sgn |
2332 | L'.SgnProj (m, ms, x) => | 2360 | L'.SgnProj (m, ms, x) => |
2333 case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) | 2361 case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) |
2334 (L'.StrVar m, #2 sgn) ms, | 2362 (L'.StrVar m, #2 sgn) ms, |
2358 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) | 2386 val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) |
2359 (L'.StrVar str, #2 sgn) strs | 2387 (L'.StrVar str, #2 sgn) strs |
2360 in | 2388 in |
2361 case #1 (hnormSgn env sgn) of | 2389 case #1 (hnormSgn env sgn) of |
2362 L'.SgnConst sgis => | 2390 L'.SgnConst sgis => |
2363 ListUtil.foldlMap (fn ((sgi, loc), env') => | 2391 ListUtil.foldlMapConcat |
2364 let | 2392 (fn ((sgi, loc), env') => |
2365 val d = | 2393 let |
2366 case sgi of | 2394 val d = |
2367 L'.SgiConAbs (x, n, k) => | 2395 case sgi of |
2368 let | 2396 L'.SgiConAbs (x, n, k) => |
2369 val c = (L'.CModProj (str, strs, x), loc) | 2397 let |
2370 in | 2398 val c = (L'.CModProj (str, strs, x), loc) |
2371 (L'.DCon (x, n, k, c), loc) | 2399 in |
2372 end | 2400 [(L'.DCon (x, n, k, c), loc)] |
2373 | L'.SgiCon (x, n, k, c) => | 2401 end |
2374 (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) | 2402 | L'.SgiCon (x, n, k, c) => |
2375 | L'.SgiDatatype (x, n, xs, xncs) => | 2403 [(L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] |
2376 (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc) | 2404 | L'.SgiDatatype dts => |
2377 | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => | 2405 map (fn (x, n, xs, xncs) => (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts |
2378 (L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) | 2406 | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => |
2379 | L'.SgiVal (x, n, t) => | 2407 [(L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)] |
2380 (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc) | 2408 | L'.SgiVal (x, n, t) => |
2381 | L'.SgiStr (x, n, sgn) => | 2409 [(L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)] |
2382 (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc) | 2410 | L'.SgiStr (x, n, sgn) => |
2383 | L'.SgiSgn (x, n, sgn) => | 2411 [(L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)] |
2384 (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc) | 2412 | L'.SgiSgn (x, n, sgn) => |
2385 | L'.SgiConstraint (c1, c2) => | 2413 [(L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)] |
2386 (L'.DConstraint (c1, c2), loc) | 2414 | L'.SgiConstraint (c1, c2) => |
2387 | L'.SgiClassAbs (x, n, k) => | 2415 [(L'.DConstraint (c1, c2), loc)] |
2388 let | 2416 | L'.SgiClassAbs (x, n, k) => |
2389 val c = (L'.CModProj (str, strs, x), loc) | 2417 let |
2390 in | 2418 val c = (L'.CModProj (str, strs, x), loc) |
2391 (L'.DCon (x, n, k, c), loc) | 2419 in |
2392 end | 2420 [(L'.DCon (x, n, k, c), loc)] |
2393 | L'.SgiClass (x, n, k, _) => | 2421 end |
2394 let | 2422 | L'.SgiClass (x, n, k, _) => |
2395 val c = (L'.CModProj (str, strs, x), loc) | 2423 let |
2396 in | 2424 val c = (L'.CModProj (str, strs, x), loc) |
2397 (L'.DCon (x, n, k, c), loc) | 2425 in |
2398 end | 2426 [(L'.DCon (x, n, k, c), loc)] |
2399 in | 2427 end |
2400 (d, E.declBinds env' d) | 2428 in |
2401 end) | 2429 (d, foldl (fn (d, env') => E.declBinds env' d) env' d) |
2402 env sgis | 2430 end) |
2431 env sgis | |
2403 | _ => (strError env (UnOpenable sgn); | 2432 | _ => (strError env (UnOpenable sgn); |
2404 ([], env)) | 2433 ([], env)) |
2405 end | 2434 end |
2406 | 2435 |
2407 and sgiOfDecl (d, loc) = | 2436 and sgiOfDecl (d, loc) = |
2443 | 2472 |
2444 fun folder (sgi2All as (sgi, loc), env) = | 2473 fun folder (sgi2All as (sgi, loc), env) = |
2445 let | 2474 let |
2446 (*val () = prefaces "folder" [("sgis1", p_sgn env (L'.SgnConst sgis1, loc2))]*) | 2475 (*val () = prefaces "folder" [("sgis1", p_sgn env (L'.SgnConst sgis1, loc2))]*) |
2447 | 2476 |
2448 fun seek p = | 2477 fun seek' f p = |
2449 let | 2478 let |
2450 fun seek env ls = | 2479 fun seek env ls = |
2451 case ls of | 2480 case ls of |
2452 [] => (sgnError env (UnmatchedSgi sgi2All); | 2481 [] => f env |
2453 env) | |
2454 | h :: t => | 2482 | h :: t => |
2455 case p (env, h) of | 2483 case p (env, h) of |
2456 NONE => | 2484 NONE => |
2457 let | 2485 let |
2458 val env = case #1 h of | 2486 val env = case #1 h of |
2472 end | 2500 end |
2473 | SOME envs => envs | 2501 | SOME envs => envs |
2474 in | 2502 in |
2475 seek env sgis1 | 2503 seek env sgis1 |
2476 end | 2504 end |
2505 | |
2506 val seek = seek' (fn env => (sgnError env (UnmatchedSgi sgi2All); | |
2507 env)) | |
2477 in | 2508 in |
2478 case sgi of | 2509 case sgi of |
2479 L'.SgiConAbs (x, n2, k2) => | 2510 L'.SgiConAbs (x, n2, k2) => |
2480 seek (fn (env, sgi1All as (sgi1, _)) => | 2511 seek (fn (env, sgi1All as (sgi1, _)) => |
2481 let | 2512 let |
2496 NONE | 2527 NONE |
2497 in | 2528 in |
2498 case sgi1 of | 2529 case sgi1 of |
2499 L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE) | 2530 L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE) |
2500 | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1) | 2531 | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1) |
2501 | L'.SgiDatatype (x', n1, xs, _) => | 2532 | L'.SgiDatatype dts => |
2502 let | 2533 let |
2503 val k = (L'.KType, loc) | 2534 val k = (L'.KType, loc) |
2504 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs | 2535 |
2536 fun search dts = | |
2537 case dts of | |
2538 [] => NONE | |
2539 | (x', n1, xs, _) :: dts => | |
2540 let | |
2541 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs | |
2542 in | |
2543 case found (x', n1, k', NONE) of | |
2544 NONE => search dts | |
2545 | x => x | |
2546 end | |
2505 in | 2547 in |
2506 found (x', n1, k', NONE) | 2548 search dts |
2507 end | 2549 end |
2508 | L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) => | 2550 | L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) => |
2509 let | 2551 let |
2510 val k = (L'.KType, loc) | 2552 val k = (L'.KType, loc) |
2511 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs | 2553 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs |
2547 L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1) | 2589 L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1) |
2548 | L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1) | 2590 | L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1) |
2549 | _ => NONE | 2591 | _ => NONE |
2550 end) | 2592 end) |
2551 | 2593 |
2552 | L'.SgiDatatype (x, n2, xs2, xncs2) => | 2594 | L'.SgiDatatype dts2 => |
2553 seek (fn (env, sgi1All as (sgi1, _)) => | 2595 let |
2554 let | 2596 fun found' (sgi1All, (x1, n1, xs1, xncs1), (x2, n2, xs2, xncs2), env) = |
2555 fun found (n1, xs1, xncs1) = | 2597 if x1 <> x2 then |
2556 let | 2598 NONE |
2557 fun mismatched ue = | 2599 else |
2558 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue)); | 2600 let |
2559 SOME env) | 2601 fun mismatched ue = |
2560 | 2602 (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue)); |
2561 val k = (L'.KType, loc) | 2603 SOME env) |
2562 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1 | 2604 |
2563 | 2605 val k = (L'.KType, loc) |
2564 fun good () = | 2606 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1 |
2565 let | 2607 |
2566 val env = E.sgiBinds env sgi1All | 2608 fun good () = |
2567 val env = if n1 = n2 then | 2609 let |
2568 env | 2610 val env = E.sgiBinds env sgi1All |
2569 else | 2611 val env = if n1 = n2 then |
2570 E.pushCNamedAs env x n2 k' | 2612 env |
2571 (SOME (L'.CNamed n1, loc)) | 2613 else |
2572 in | 2614 E.pushCNamedAs env x1 n2 k' |
2573 SOME env | 2615 (SOME (L'.CNamed n1, loc)) |
2574 end | 2616 in |
2575 | 2617 SOME env |
2576 val env = E.pushCNamedAs env x n1 k' NONE | 2618 end |
2577 val env = if n1 = n2 then | 2619 |
2578 env | 2620 val env = E.pushCNamedAs env x1 n1 k' NONE |
2579 else | 2621 val env = if n1 = n2 then |
2580 E.pushCNamedAs env x n2 k' (SOME (L'.CNamed n1, loc)) | 2622 env |
2581 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1 | 2623 else |
2582 fun xncBad ((x1, _, t1), (x2, _, t2)) = | 2624 E.pushCNamedAs env x1 n2 k' (SOME (L'.CNamed n1, loc)) |
2583 String.compare (x1, x2) <> EQUAL | 2625 val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1 |
2584 orelse case (t1, t2) of | 2626 fun xncBad ((x1, _, t1), (x2, _, t2)) = |
2585 (NONE, NONE) => false | 2627 String.compare (x1, x2) <> EQUAL |
2586 | (SOME t1, SOME t2) => | 2628 orelse case (t1, t2) of |
2587 (unifyCons env t1 t2; false) | 2629 (NONE, NONE) => false |
2588 | _ => true | 2630 | (SOME t1, SOME t2) => |
2589 in | 2631 (unifyCons env t1 t2; false) |
2590 (if xs1 <> xs2 | 2632 | _ => true |
2591 orelse length xncs1 <> length xncs2 | 2633 in |
2592 orelse ListPair.exists xncBad (xncs1, xncs2) then | 2634 (if xs1 <> xs2 |
2593 mismatched NONE | 2635 orelse length xncs1 <> length xncs2 |
2594 else | 2636 orelse ListPair.exists xncBad (xncs1, xncs2) then |
2595 good ()) | 2637 mismatched NONE |
2596 handle CUnify ue => mismatched (SOME ue) | |
2597 end | |
2598 in | |
2599 case sgi1 of | |
2600 L'.SgiDatatype (x', n1, xs, xncs1) => | |
2601 if x' = x then | |
2602 found (n1, xs, xncs1) | |
2603 else | 2638 else |
2604 NONE | 2639 good ()) |
2605 | L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) => | 2640 handle CUnify ue => mismatched (SOME ue) |
2606 if x' = x then | 2641 end |
2607 found (n1, xs, xncs1) | 2642 in |
2608 else | 2643 seek' |
2609 NONE | 2644 (fn _ => |
2610 | _ => NONE | 2645 let |
2611 end) | 2646 fun seekOne (dt2, env) = |
2647 seek (fn (env, sgi1All as (sgi1, _)) => | |
2648 case sgi1 of | |
2649 L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) => | |
2650 found' (sgi1All, (x', n1, xs, xncs1), dt2, env) | |
2651 | _ => NONE) | |
2652 | |
2653 fun seekAll (dts, env) = | |
2654 case dts of | |
2655 [] => env | |
2656 | dt :: dts => seekAll (dts, seekOne (dt, env)) | |
2657 in | |
2658 seekAll (dts2, env) | |
2659 end) | |
2660 (fn (env, sgi1All as (sgi1, _)) => | |
2661 let | |
2662 fun found dts1 = | |
2663 let | |
2664 fun iter (dts1, dts2, env) = | |
2665 case (dts1, dts2) of | |
2666 ([], []) => SOME env | |
2667 | (dt1 :: dts1, dt2 :: dts2) => | |
2668 (case found' (sgi1All, dt1, dt2, env) of | |
2669 NONE => NONE | |
2670 | SOME env => iter (dts1, dts2, env)) | |
2671 | _ => NONE | |
2672 in | |
2673 iter (dts1, dts2, env) | |
2674 end | |
2675 in | |
2676 case sgi1 of | |
2677 L'.SgiDatatype dts1 => found dts1 | |
2678 | _ => NONE | |
2679 end) | |
2680 end | |
2612 | 2681 |
2613 | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) => | 2682 | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) => |
2614 seek (fn (env, sgi1All as (sgi1, _)) => | 2683 seek (fn (env, sgi1All as (sgi1, _)) => |
2615 case sgi1 of | 2684 case sgi1 of |
2616 L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) => | 2685 L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) => |
3031 in | 3100 in |
3032 checkKind env c' ck k'; | 3101 checkKind env c' ck k'; |
3033 | 3102 |
3034 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs)) | 3103 ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs)) |
3035 end | 3104 end |
3036 | L.DDatatype (x, xs, xcs) => | 3105 | L.DDatatype dts => |
3037 let | 3106 let |
3038 val positive = List.all (fn (_, to) => | |
3039 case to of | |
3040 NONE => true | |
3041 | SOME t => positive x t) xcs | |
3042 | |
3043 val k = (L'.KType, loc) | 3107 val k = (L'.KType, loc) |
3044 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs | 3108 |
3045 val (env, n) = E.pushCNamed env x k' NONE | 3109 val (dts, env) = ListUtil.foldlMap |
3046 val t = (L'.CNamed n, loc) | 3110 (fn ((x, xs, xcs), env) => |
3047 val nxs = length xs - 1 | 3111 let |
3048 val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs | 3112 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs |
3049 | 3113 val (env, n) = E.pushCNamed env x k' NONE |
3050 val (env', denv') = foldl (fn (x, (env', denv')) => | 3114 in |
3051 (E.pushCRel env' x k, | 3115 ((x, n, xs, xcs), env) |
3052 D.enter denv')) (env, denv) xs | 3116 end) |
3053 | 3117 env dts |
3054 val (xcs, (used, env, gs')) = | 3118 |
3055 ListUtil.foldlMap | 3119 val (dts, (env, gs')) = ListUtil.foldlMap |
3056 (fn ((x, to), (used, env, gs)) => | 3120 (fn ((x, n, xs, xcs), (env, gs')) => |
3057 let | 3121 let |
3058 val (to, t, gs') = case to of | 3122 val t = (L'.CNamed n, loc) |
3059 NONE => (NONE, t, gs) | 3123 val nxs = length xs - 1 |
3060 | SOME t' => | 3124 val t = ListUtil.foldli |
3061 let | 3125 (fn (i, _, t) => |
3062 val (t', tk, gs') = elabCon (env', denv') t' | 3126 (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs |
3063 in | 3127 |
3064 checkKind env' t' tk k; | 3128 val (env', denv') = foldl (fn (x, (env', denv')) => |
3065 (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs) | 3129 (E.pushCRel env' x k, |
3066 end | 3130 D.enter denv')) (env, denv) xs |
3067 val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs | 3131 |
3068 | 3132 val (xcs, (used, env, gs')) = |
3069 val (env, n') = E.pushENamed env x t | 3133 ListUtil.foldlMap |
3070 in | 3134 (fn ((x, to), (used, env, gs)) => |
3071 if SS.member (used, x) then | 3135 let |
3072 strError env (DuplicateConstructor (x, loc)) | 3136 val (to, t, gs') = case to of |
3073 else | 3137 NONE => (NONE, t, gs) |
3074 (); | 3138 | SOME t' => |
3075 ((x, n', to), (SS.add (used, x), env, gs')) | 3139 let |
3076 end) | 3140 val (t', tk, gs') = elabCon (env', denv') t' |
3077 (SS.empty, env, []) xcs | 3141 in |
3078 | 3142 checkKind env' t' tk k; |
3079 val env = E.pushDatatype env n xs xcs | 3143 (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs) |
3080 val d' = (L'.DDatatype (x, n, xs, xcs), loc) | 3144 end |
3145 val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs | |
3146 | |
3147 val (env, n') = E.pushENamed env x t | |
3148 in | |
3149 if SS.member (used, x) then | |
3150 strError env (DuplicateConstructor (x, loc)) | |
3151 else | |
3152 (); | |
3153 ((x, n', to), (SS.add (used, x), env, gs')) | |
3154 end) | |
3155 (SS.empty, env, gs') xcs | |
3156 in | |
3157 ((x, n, xs, xcs), (E.pushDatatype env n xs xcs, gs')) | |
3158 end) | |
3159 (env, []) dts | |
3081 in | 3160 in |
3082 (*if positive then | 3161 ([(L'.DDatatype dts, loc)], (env, denv, gs' @ gs)) |
3083 () | |
3084 else | |
3085 declError env (Nonpositive d');*) | |
3086 | |
3087 ([d'], (env, denv, gs' @ gs)) | |
3088 end | 3162 end |
3089 | 3163 |
3090 | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp" | 3164 | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp" |
3091 | 3165 |
3092 | L.DDatatypeImp (x, m1 :: ms, s) => | 3166 | L.DDatatypeImp (x, m1 :: ms, s) => |
3482 else | 3556 else |
3483 (SS.add (cons, x), x) | 3557 (SS.add (cons, x), x) |
3484 in | 3558 in |
3485 ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs) | 3559 ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs) |
3486 end | 3560 end |
3487 | L'.SgiDatatype (x, n, xs, xncs) => | 3561 | L'.SgiDatatype dts => |
3488 let | 3562 let |
3489 val (cons, x) = | 3563 fun doOne ((x, n, xs, xncs), (cons, vals)) = |
3490 if SS.member (cons, x) then | 3564 let |
3491 (cons, "?" ^ x) | 3565 val (cons, x) = |
3492 else | 3566 if SS.member (cons, x) then |
3493 (SS.add (cons, x), x) | 3567 (cons, "?" ^ x) |
3494 | |
3495 val (xncs, vals) = | |
3496 ListUtil.foldlMap | |
3497 (fn ((x, n, t), vals) => | |
3498 if SS.member (vals, x) then | |
3499 (("?" ^ x, n, t), vals) | |
3500 else | 3568 else |
3501 ((x, n, t), SS.add (vals, x))) | 3569 (SS.add (cons, x), x) |
3502 vals xncs | 3570 |
3571 val (xncs, vals) = | |
3572 ListUtil.foldlMap | |
3573 (fn ((x, n, t), vals) => | |
3574 if SS.member (vals, x) then | |
3575 (("?" ^ x, n, t), vals) | |
3576 else | |
3577 ((x, n, t), SS.add (vals, x))) | |
3578 vals xncs | |
3579 in | |
3580 ((x, n, xs, xncs), (cons, vals)) | |
3581 end | |
3582 | |
3583 val (dts, (cons, vals)) = ListUtil.foldlMap doOne (cons, vals) dts | |
3503 in | 3584 in |
3504 ((L'.SgiDatatype (x, n, xs, xncs), loc) :: sgis, cons, vals, sgns, strs) | 3585 ((L'.SgiDatatype dts, loc) :: sgis, cons, vals, sgns, strs) |
3505 end | 3586 end |
3506 | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => | 3587 | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => |
3507 let | 3588 let |
3508 val (cons, x) = | 3589 val (cons, x) = |
3509 if SS.member (cons, x) then | 3590 if SS.member (cons, x) then |