Mercurial > urweb

comparison src/elaborate.sml @ 1302:d008c4c43a0a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Flex kinds for type-level tuples; ::_ notation
author Adam Chlipala <adam@chlipala.net>
date Sun, 10 Oct 2010 13:07:38 -0400
parents 3c334458c84f
children c7b9a33c26c8
comparison
equal deleted inserted replaced
1301:4359e185d3af 1302:d008c4c43a0a
92 | (_, L'.KError) => () 92 | (_, L'.KError) => ()
93 93
94 | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' env k1All k2All 94 | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' env k1All k2All
95 | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' env k1All k2All 95 | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' env k1All k2All
96 96
97 | (L'.KTupleUnif (_, _, ref (SOME k)), _) => unifyKinds' env k k2All
98 | (_, L'.KTupleUnif (_, _, ref (SOME k))) => unifyKinds' env k1All k
99
97 | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) => 100 | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
98 if r1 = r2 then 101 if r1 = r2 then
99 () 102 ()
100 else 103 else
101 r1 := SOME k2All 104 r1 := SOME k2All
108 | (_, L'.KUnif (_, _, r)) => 111 | (_, L'.KUnif (_, _, r)) =>
109 if occursKind r k1All then 112 if occursKind r k1All then
110 err KOccursCheckFailed 113 err KOccursCheckFailed
111 else 114 else
112 r := SOME k1All 115 r := SOME k1All
116
117 | (L'.KTupleUnif (_, nks, r), L'.KTuple ks) =>
118 ((app (fn (n, k) => unifyKinds' env k (List.nth (ks, n-1))) nks;
119 r := SOME k2All)
120 handle Subscript => err KIncompatible)
121 | (L'.KTuple ks, L'.KTupleUnif (_, nks, r)) =>
122 ((app (fn (n, k) => unifyKinds' env (List.nth (ks, n-1)) k) nks;
123 r := SOME k1All)
124 handle Subscript => err KIncompatible)
125 | (L'.KTupleUnif (loc, nks1, r1), L'.KTupleUnif (_, nks2, r2)) =>
126 let
127 val nks = foldl (fn (p as (n, k1), nks) =>
128 case ListUtil.search (fn (n', k2) =>
129 if n' = n then
130 SOME k2
131 else
132 NONE) nks2 of
133 NONE => p :: nks
134 | SOME k2 => (unifyKinds' env k1 k2;
135 nks)) nks2 nks1
136
137 val k = (L'.KTupleUnif (loc, nks, ref NONE), loc)
138 in
139 r1 := SOME k;
140 r2 := SOME k
141 end
113 142
114 | _ => err KIncompatible 143 | _ => err KIncompatible
115 end 144 end
116 145
117 exception KUnify of L'.kind * L'.kind * kunify_error 146 exception KUnify of L'.kind * L'.kind * kunify_error
439 ((L'.CTuple (rev cs'), loc), (L'.KTuple (rev ks), loc), gs) 468 ((L'.CTuple (rev cs'), loc), (L'.KTuple (rev ks), loc), gs)
440 end 469 end
441 | L.CProj (c, n) => 470 | L.CProj (c, n) =>
442 let 471 let
443 val (c', k, gs) = elabCon (env, denv) c 472 val (c', k, gs) = elabCon (env, denv) c
473
474 val k' = kunif loc
444 in 475 in
445 case hnormKind k of 476 if n <= 0 then
446 (L'.KTuple ks, _) => 477 (conError env (ProjBounds (c', n));
447 if n <= 0 orelse n > length ks then 478 (cerror, kerror, []))
448 (conError env (ProjBounds (c', n)); 479 else
449 (cerror, kerror, [])) 480 (checkKind env c' k (L'.KTupleUnif (loc, [(n, k')], ref NONE), loc);
450 else 481 ((L'.CProj (c', n), loc), k', gs))
451 ((L'.CProj (c', n), loc), List.nth (ks, n - 1), gs)
452 | k => (conError env (ProjMismatch (c', k));
453 (cerror, kerror, []))
454 end 482 end
455 483
456 | L.CWild k => 484 | L.CWild k =>
457 let 485 let
458 val k' = elabKind env k 486 val k' = elabKind env k
461 end 489 end
462 490
463 fun kunifsRemain k = 491 fun kunifsRemain k =
464 case k of 492 case k of
465 L'.KUnif (_, _, ref NONE) => true 493 L'.KUnif (_, _, ref NONE) => true
494 | L'.KTupleUnif (_, _, ref NONE) => true
466 | _ => false 495 | _ => false
467 fun cunifsRemain c = 496 fun cunifsRemain c =
468 case c of 497 case c of
469 L'.CUnif (loc, _, _, ref NONE) => SOME loc 498 L'.CUnif (loc, _, _, ref NONE) => SOME loc
470 | _ => NONE 499 | _ => NONE
3227 end 3256 end
3228 3257
3229 | L'.KError => NONE 3258 | L'.KError => NONE
3230 | L'.KUnif (_, _, ref (SOME k)) => decompileKind k 3259 | L'.KUnif (_, _, ref (SOME k)) => decompileKind k
3231 | L'.KUnif _ => NONE 3260 | L'.KUnif _ => NONE
3261 | L'.KTupleUnif (_, _, ref (SOME k)) => decompileKind k
3262 | L'.KTupleUnif _ => NONE
3232 3263
3233 | L'.KRel _ => NONE 3264 | L'.KRel _ => NONE
3234 | L'.KFun _ => NONE 3265 | L'.KFun _ => NONE
3235 3266
3236 fun decompileCon env (c, loc) = 3267 fun decompileCon env (c, loc) =