Mercurial > urweb

comparison src/elaborate.sml @ 805:e2780d2f4afc

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