Mercurial > urweb

comparison src/elaborate.sml @ 345:b85e6ba56618

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge CDisjoint and TDisjoint
author Adam Chlipala <adamc@hcoop.net>
date Sat, 04 Oct 2008 15:50:28 -0400
parents 389399d65331
children b88f4297167f
comparison
equal deleted inserted replaced
344:3c0feecd057d 345:b85e6ba56618
223 val (t', tk, gs) = elabCon (env', D.enter denv) t 223 val (t', tk, gs) = elabCon (env', D.enter denv) t
224 in 224 in
225 checkKind env t' tk ktype; 225 checkKind env t' tk ktype;
226 ((L'.TCFun (e', x, k', t'), loc), ktype, gs) 226 ((L'.TCFun (e', x, k', t'), loc), ktype, gs)
227 end 227 end
228 | L.TDisjoint (c1, c2, c) => 228 | L.CDisjoint (c1, c2, c) =>
229 let 229 let
230 val (c1', k1, gs1) = elabCon (env, denv) c1 230 val (c1', k1, gs1) = elabCon (env, denv) c1
231 val (c2', k2, gs2) = elabCon (env, denv) c2 231 val (c2', k2, gs2) = elabCon (env, denv) c2
232 232
233 val ku1 = kunif loc 233 val ku1 = kunif loc
237 val (c', k, gs4) = elabCon (env, denv') c 237 val (c', k, gs4) = elabCon (env, denv') c
238 in 238 in
239 checkKind env c1' k1 (L'.KRecord ku1, loc); 239 checkKind env c1' k1 (L'.KRecord ku1, loc);
240 checkKind env c2' k2 (L'.KRecord ku2, loc); 240 checkKind env c2' k2 (L'.KRecord ku2, loc);
241 241
242 ((L'.TDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4) 242 ((L'.CDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
243 end 243 end
244 | L.TRecord c => 244 | L.TRecord c =>
245 let 245 let
246 val (c', ck, gs) = elabCon (env, denv) c 246 val (c', ck, gs) = elabCon (env, denv) c
247 val k = (L'.KRecord ktype, loc) 247 val k = (L'.KRecord ktype, loc)
302 ((L'.CAbs (x, k', t'), loc), 302 ((L'.CAbs (x, k', t'), loc),
303 (L'.KArrow (k', tk), loc), 303 (L'.KArrow (k', tk), loc),
304 gs) 304 gs)
305 end 305 end
306 306
307 | L.CDisjoint (c1, c2, c) =>
308 let
309 val (c1', k1, gs1) = elabCon (env, denv) c1
310 val (c2', k2, gs2) = elabCon (env, denv) c2
311
312 val ku1 = kunif loc
313 val ku2 = kunif loc
314
315 val (denv', gs3) = D.assert env denv (c1', c2')
316 val (c', k, gs4) = elabCon (env, denv') c
317 in
318 checkKind env c1' k1 (L'.KRecord ku1, loc);
319 checkKind env c2' k2 (L'.KRecord ku2, loc);
320
321 ((L'.CDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
322 end
323
324 | L.CName s => 307 | L.CName s =>
325 ((L'.CName s, loc), kname, []) 308 ((L'.CName s, loc), kname, [])
326 309
327 | L.CRecord xcs => 310 | L.CRecord xcs =>
328 let 311 let
474 457
475 fun kindof env (c, loc) = 458 fun kindof env (c, loc) =
476 case c of 459 case c of
477 L'.TFun _ => ktype 460 L'.TFun _ => ktype
478 | L'.TCFun _ => ktype 461 | L'.TCFun _ => ktype
479 | L'.TDisjoint _ => ktype
480 | L'.TRecord _ => ktype 462 | L'.TRecord _ => ktype
481 463
482 | L'.CRel xn => #2 (E.lookupCRel env xn) 464 | L'.CRel xn => #2 (E.lookupCRel env xn)
483 | L'.CNamed xn => #2 (E.lookupCNamed env xn) 465 | L'.CNamed xn => #2 (E.lookupCNamed env xn)
484 | L'.CModProj (n, ms, x) => 466 | L'.CModProj (n, ms, x) =>
499 (case hnormKind (kindof env c) of 481 (case hnormKind (kindof env c) of
500 (L'.KArrow (_, k), _) => k 482 (L'.KArrow (_, k), _) => k
501 | (L'.KError, _) => kerror 483 | (L'.KError, _) => kerror
502 | k => raise CUnify' (CKindof (k, c))) 484 | k => raise CUnify' (CKindof (k, c)))
503 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc) 485 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
504 | L'.CDisjoint (_, _, c) => kindof env c 486 | L'.CDisjoint (_, _, _, c) => kindof env c
505 487
506 | L'.CName _ => kname 488 | L'.CName _ => kname
507 489
508 | L'.CRecord (k, _) => (L'.KRecord k, loc) 490 | L'.CRecord (k, _) => (L'.KRecord k, loc)
509 | L'.CConcat (c, _) => kindof env c 491 | L'.CConcat (c, _) => kindof env c
539 in 521 in
540 case #1 c of 522 case #1 c of
541 L'.CRecord (_, []) => (Nil, gs) 523 L'.CRecord (_, []) => (Nil, gs)
542 | L'.CRecord (_, _ :: _) => (Cons, gs) 524 | L'.CRecord (_, _ :: _) => (Cons, gs)
543 | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs) 525 | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs)
544 | L'.CDisjoint (_, _, c) => 526 | L'.CDisjoint (_, _, _, c) =>
545 let 527 let
546 val (s, gs') = summarizeCon (env, denv) c 528 val (s, gs') = summarizeCon (env, denv) c
547 in 529 in
548 (s, gs @ gs') 530 (s, gs @ gs')
549 end 531 end
822 | _ => raise ex 804 | _ => raise ex
823 end 805 end
824 806
825 and unifyCons' (env, denv) c1 c2 = 807 and unifyCons' (env, denv) c1 c2 =
826 case (#1 c1, #1 c2) of 808 case (#1 c1, #1 c2) of
827 (L'.TDisjoint (_, x1, y1, t1), L'.TDisjoint (_, x2, y2, t2)) => 809 (L'.CDisjoint (_, x1, y1, t1), L'.CDisjoint (_, x2, y2, t2)) =>
828 let 810 let
829 val gs1 = unifyCons' (env, denv) x1 x2 811 val gs1 = unifyCons' (env, denv) x1 x2
830 val gs2 = unifyCons' (env, denv) y1 y2 812 val gs2 = unifyCons' (env, denv) y1 y2
831 val (denv', gs3) = D.assert env denv (x1, y1) 813 val (denv', gs3) = D.assert env denv (x1, y1)
832 val gs4 = unifyCons' (env, denv') t1 t2 814 val gs4 = unifyCons' (env, denv') t1 t2
981 (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc), 963 (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc),
982 (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc), 964 (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc),
983 (L'.TCFun (L'.Explicit, "v", dom, 965 (L'.TCFun (L'.Explicit, "v", dom,
984 (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc), 966 (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
985 (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc), 967 (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
986 (L'.TDisjoint (L'.Instantiate, 968 (L'.CDisjoint (L'.Instantiate,
987 (L'.CRecord 969 (L'.CRecord
988 ((L'.KUnit, loc), 970 ((L'.KUnit, loc),
989 [((L'.CRel 2, loc), 971 [((L'.CRel 2, loc),
990 (L'.CUnit, loc))]), loc), 972 (L'.CUnit, loc))]), loc),
991 (L'.CRel 0, loc), 973 (L'.CRel 0, loc),
1522 val (e', t, gs4) = elabExp (env, denv') e 1504 val (e', t, gs4) = elabExp (env, denv') e
1523 in 1505 in
1524 checkKind env c1' k1 (L'.KRecord ku1, loc); 1506 checkKind env c1' k1 (L'.KRecord ku1, loc);
1525 checkKind env c2' k2 (L'.KRecord ku2, loc); 1507 checkKind env c2' k2 (L'.KRecord ku2, loc);
1526 1508
1527 (e', (L'.TDisjoint (L'.LeaveAlone, c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4) 1509 (e', (L'.CDisjoint (L'.LeaveAlone, c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4)
1528 end 1510 end
1529 1511
1530 | L.ERecord xes => 1512 | L.ERecord xes =>
1531 let 1513 let
1532 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) => 1514 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
2570 case c of 2552 case c of
2571 CAnnot (c, _) => none c 2553 CAnnot (c, _) => none c
2572 2554
2573 | TFun (c1, c2) => none c1 andalso none c2 2555 | TFun (c1, c2) => none c1 andalso none c2
2574 | TCFun (_, _, _, c) => none c 2556 | TCFun (_, _, _, c) => none c
2575 | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
2576 | TRecord c => none c 2557 | TRecord c => none c
2577 2558
2578 | CVar ([], x) => x <> self 2559 | CVar ([], x) => x <> self
2579 | CVar _ => true 2560 | CVar _ => true
2580 | CApp (c1, c2) => none c1 andalso none c2 2561 | CApp (c1, c2) => none c1 andalso none c2
2598 case c of 2579 case c of
2599 CAnnot (c, _) => pos c 2580 CAnnot (c, _) => pos c
2600 2581
2601 | TFun (c1, c2) => none c1 andalso pos c2 2582 | TFun (c1, c2) => none c1 andalso pos c2
2602 | TCFun (_, _, _, c) => pos c 2583 | TCFun (_, _, _, c) => pos c
2603 | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
2604 | TRecord c => pos c 2584 | TRecord c => pos c
2605 2585
2606 | CVar _ => true 2586 | CVar _ => true
2607 | CApp (c1, c2) => pos c1 andalso none c2 2587 | CApp (c1, c2) => pos c1 andalso none c2
2608 | CAbs _ => false 2588 | CAbs _ => false
2719 val makeInstantiable = 2699 val makeInstantiable =
2720 let 2700 let
2721 fun kind k = k 2701 fun kind k = k
2722 fun con c = 2702 fun con c =
2723 case c of 2703 case c of
2724 L'.TDisjoint (L'.LeaveAlone, c1, c2, c) => L'.TDisjoint (L'.Instantiate, c1, c2, c) 2704 L'.CDisjoint (L'.LeaveAlone, c1, c2, c) => L'.CDisjoint (L'.Instantiate, c1, c2, c)
2725 | _ => c 2705 | _ => c
2726 in 2706 in
2727 U.Con.map {kind = kind, con = con} 2707 U.Con.map {kind = kind, con = con}
2728 end 2708 end
2729 2709