Mercurial > urweb

comparison src/elaborate.sml @ 1639:6c00d8af6239

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add a new scoping check for unification variables, to fix a type inference bug
author Adam Chlipala <adam@chlipala.net>
date Sun, 18 Dec 2011 11:29:13 -0500
parents 07eed8386f07
children dc986eb6113c
comparison
equal deleted inserted replaced
1638:3bf727a08db8 1639:6c00d8af6239
61 61
62 fun occursKind r = 62 fun occursKind r =
63 U.Kind.exists (fn L'.KUnif (_, _, r') => r = r' 63 U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
64 | _ => false) 64 | _ => false)
65 65
66 fun validateCon env c =
67 (U.Con.appB {kind = fn env' => fn k => case k of
68 L'.KRel n => ignore (E.lookupKRel env' n)
69 | L'.KUnif (_, _, r as ref (L'.KUnknown f)) =>
70 r := L'.KUnknown (fn k => f k andalso validateKind env' k)
71 | _ => (),
72 con = fn env' => fn c => case c of
73 L'.CRel n => ignore (E.lookupCRel env' n)
74 | L'.CNamed n => ignore (E.lookupCNamed env' n)
75 | L'.CModProj (n, _, _) => ignore (E.lookupStrNamed env' n)
76 | L'.CUnif (_, _, _, _, r as ref (L'.Unknown f)) =>
77 r := L'.Unknown (fn c => f c andalso validateCon env' c)
78 | _ => (),
79 bind = fn (env', b) => case b of
80 U.Con.RelK x => E.pushKRel env' x
81 | U.Con.RelC (x, k) => E.pushCRel env' x k
82 | U.Con.NamedC (x, n, k, co) => E.pushCNamedAs env x n k co}
83 env c;
84 true)
85 handle _ => false
86
87 and validateKind env k = validateCon env (L'.CRecord (k, []), ErrorMsg.dummySpan)
88
66 exception KUnify' of kunify_error 89 exception KUnify' of kunify_error
67 90
68 fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) = 91 fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) =
69 let 92 let
70 fun err f = raise KUnify' (f (k1All, k2All)) 93 fun err f = raise KUnify' (f (k1All, k2All))
91 unifyKinds' (E.pushKRel env x) k1 k2 114 unifyKinds' (E.pushKRel env x) k1 k2
92 115
93 | (L'.KError, _) => () 116 | (L'.KError, _) => ()
94 | (_, L'.KError) => () 117 | (_, L'.KError) => ()
95 118
96 | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' env k1All k2All 119 | (L'.KUnif (_, _, ref (L'.KKnown k1All)), _) => unifyKinds' env k1All k2All
97 | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' env k1All k2All 120 | (_, L'.KUnif (_, _, ref (L'.KKnown k2All))) => unifyKinds' env k1All k2All
98 121
99 | (L'.KTupleUnif (_, _, ref (SOME k)), _) => unifyKinds' env k k2All 122 | (L'.KTupleUnif (_, _, ref (L'.KKnown k)), _) => unifyKinds' env k k2All
100 | (_, L'.KTupleUnif (_, _, ref (SOME k))) => unifyKinds' env k1All k 123 | (_, L'.KTupleUnif (_, _, ref (L'.KKnown k))) => unifyKinds' env k1All k
101 124
102 | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) => 125 | (L'.KUnif (_, _, r1 as ref (L'.KUnknown f1)), L'.KUnif (_, _, r2 as ref (L'.KUnknown f2))) =>
103 if r1 = r2 then 126 if r1 = r2 then
104 () 127 ()
105 else 128 else
106 r1 := SOME k2All 129 (r1 := L'.KKnown k2All;
107 130 r2 := L'.KUnknown (fn x => f1 x andalso f2 x))
108 | (L'.KUnif (_, _, r), _) => 131
132 | (L'.KUnif (_, _, r as ref (L'.KUnknown f)), _) =>
109 if occursKind r k2All then 133 if occursKind r k2All then
110 err KOccursCheckFailed 134 err KOccursCheckFailed
135 else if not (f k2All) then
136 err KScope
111 else 137 else
112 r := SOME k2All 138 r := L'.KKnown k2All
113 | (_, L'.KUnif (_, _, r)) => 139 | (_, L'.KUnif (_, _, r as ref (L'.KUnknown f))) =>
114 if occursKind r k1All then 140 if occursKind r k1All then
115 err KOccursCheckFailed 141 err KOccursCheckFailed
142 else if not (f k1All) then
143 err KScope
116 else 144 else
117 r := SOME k1All 145 r := L'.KKnown k1All
118 146
119 | (L'.KTupleUnif (_, nks, r), L'.KTuple ks) => 147 | (L'.KTupleUnif (_, nks, r as ref (L'.KUnknown f)), L'.KTuple ks) =>
120 ((app (fn (n, k) => unifyKinds' env k (List.nth (ks, n-1))) nks; 148 if not (f k2All) then
121 r := SOME k2All) 149 err KScope
122 handle Subscript => err KIncompatible) 150 else
123 | (L'.KTuple ks, L'.KTupleUnif (_, nks, r)) => 151 ((app (fn (n, k) => unifyKinds' env k (List.nth (ks, n-1))) nks;
124 ((app (fn (n, k) => unifyKinds' env (List.nth (ks, n-1)) k) nks; 152 r := L'.KKnown k2All)
125 r := SOME k1All) 153 handle Subscript => err KIncompatible)
126 handle Subscript => err KIncompatible) 154 | (L'.KTuple ks, L'.KTupleUnif (_, nks, r as ref (L'.KUnknown f))) =>
127 | (L'.KTupleUnif (loc, nks1, r1), L'.KTupleUnif (_, nks2, r2)) => 155 if not (f k2All) then
156 err KScope
157 else
158 ((app (fn (n, k) => unifyKinds' env (List.nth (ks, n-1)) k) nks;
159 r := L'.KKnown k1All)
160 handle Subscript => err KIncompatible)
161 | (L'.KTupleUnif (loc, nks1, r1 as ref (L'.KUnknown f1)), L'.KTupleUnif (_, nks2, r2 as ref (L'.KUnknown f2))) =>
128 let 162 let
129 val nks = foldl (fn (p as (n, k1), nks) => 163 val nks = foldl (fn (p as (n, k1), nks) =>
130 case ListUtil.search (fn (n', k2) => 164 case ListUtil.search (fn (n', k2) =>
131 if n' = n then 165 if n' = n then
132 SOME k2 166 SOME k2
134 NONE) nks2 of 168 NONE) nks2 of
135 NONE => p :: nks 169 NONE => p :: nks
136 | SOME k2 => (unifyKinds' env k1 k2; 170 | SOME k2 => (unifyKinds' env k1 k2;
137 nks)) nks2 nks1 171 nks)) nks2 nks1
138 172
139 val k = (L'.KTupleUnif (loc, nks, ref NONE), loc) 173 val k = (L'.KTupleUnif (loc, nks, ref (L'.KUnknown (fn x => f1 x andalso f2 x))), loc)
140 in 174 in
141 r1 := SOME k; 175 r1 := L'.KKnown k;
142 r2 := SOME k 176 r2 := L'.KKnown k
143 end 177 end
144 178
145 | _ => err KIncompatible 179 | _ => err KIncompatible
146 end 180 end
147 181
172 val float = ref cerror 206 val float = ref cerror
173 val string = ref cerror 207 val string = ref cerror
174 val char = ref cerror 208 val char = ref cerror
175 val table = ref cerror 209 val table = ref cerror
176 210
211
177 local 212 local
178 val count = ref 0 213 val count = ref 0
179 in 214 in
180 215
181 fun resetKunif () = count := 0 216 fun resetKunif () = count := 0
182 217
183 fun kunif loc = 218 fun kunif' f loc =
184 let 219 let
185 val n = !count 220 val n = !count
186 val s = if n <= 26 then 221 val s = if n <= 26 then
187 str (chr (ord #"A" + n)) 222 str (chr (ord #"A" + n))
188 else 223 else
189 "U" ^ Int.toString (n - 26) 224 "U" ^ Int.toString (n - 26)
190 in 225 in
191 count := n + 1; 226 count := n + 1;
192 (L'.KUnif (loc, s, ref NONE), loc) 227 (L'.KUnif (loc, s, ref (L'.KUnknown f)), loc)
193 end 228 end
229
230 fun kunif env = kunif' (validateKind env)
194 231
195 end 232 end
196 233
197 local 234 local
198 val count = ref 0 235 val count = ref 0
199 in 236 in
200 237
201 fun resetCunif () = count := 0 238 fun resetCunif () = count := 0
202 239
203 fun cunif (loc, k) = 240 fun cunif' f (loc, k) =
204 let 241 let
205 val n = !count 242 val n = !count
206 val s = if n < 26 then 243 val s = if n < 26 then
207 str (chr (ord #"A" + n)) 244 str (chr (ord #"A" + n))
208 else 245 else
209 "U" ^ Int.toString (n - 26) 246 "U" ^ Int.toString (n - 26)
210 in 247 in
211 count := n + 1; 248 count := n + 1;
212 (L'.CUnif (0, loc, k, s, ref NONE), loc) 249 (L'.CUnif (0, loc, k, s, ref (L'.Unknown f)), loc)
213 end 250 end
251
252 fun cunif env = cunif' (validateCon env)
214 253
215 end 254 end
216 255
217 fun elabKind env (k, loc) = 256 fun elabKind env (k, loc) =
218 case k of 257 case k of
220 | L.KArrow (k1, k2) => (L'.KArrow (elabKind env k1, elabKind env k2), loc) 259 | L.KArrow (k1, k2) => (L'.KArrow (elabKind env k1, elabKind env k2), loc)
221 | L.KName => (L'.KName, loc) 260 | L.KName => (L'.KName, loc)
222 | L.KRecord k => (L'.KRecord (elabKind env k), loc) 261 | L.KRecord k => (L'.KRecord (elabKind env k), loc)
223 | L.KUnit => (L'.KUnit, loc) 262 | L.KUnit => (L'.KUnit, loc)
224 | L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc) 263 | L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc)
225 | L.KWild => kunif loc 264 | L.KWild => kunif env loc
226 265
227 | L.KVar s => (case E.lookupK env s of 266 | L.KVar s => (case E.lookupK env s of
228 NONE => 267 NONE =>
229 (kindError env (UnboundKind (loc, s)); 268 (kindError env (UnboundKind (loc, s));
230 kerror) 269 kerror)
236 (L'.KArrow ((L'.KRecord dom, loc), 275 (L'.KArrow ((L'.KRecord dom, loc),
237 (L'.KRecord ran, loc)), loc)), loc) 276 (L'.KRecord ran, loc)), loc)), loc)
238 277
239 fun hnormKind (kAll as (k, _)) = 278 fun hnormKind (kAll as (k, _)) =
240 case k of 279 case k of
241 L'.KUnif (_, _, ref (SOME k)) => hnormKind k 280 L'.KUnif (_, _, ref (L'.KKnown k)) => hnormKind k
242 | _ => kAll 281 | _ => kAll
243 282
244 open ElabOps 283 open ElabOps
245 284
246 fun elabConHead (c as (_, loc)) k = 285 fun elabConHead env (c as (_, loc)) k =
247 let 286 let
248 fun unravel (k, c) = 287 fun unravel (k, c) =
249 case hnormKind k of 288 case hnormKind k of
250 (L'.KFun (x, k'), _) => 289 (L'.KFun (x, k'), _) =>
251 let 290 let
252 val u = kunif loc 291 val u = kunif env loc
253 292
254 val k'' = subKindInKind (0, u) k' 293 val k'' = subKindInKind (0, u) k'
255 in 294 in
256 unravel (k'', (L'.CKApp (c, u), loc)) 295 unravel (k'', (L'.CKApp (c, u), loc))
257 end 296 end
301 | L.TDisjoint (c1, c2, c) => 340 | L.TDisjoint (c1, c2, c) =>
302 let 341 let
303 val (c1', k1, gs1) = elabCon (env, denv) c1 342 val (c1', k1, gs1) = elabCon (env, denv) c1
304 val (c2', k2, gs2) = elabCon (env, denv) c2 343 val (c2', k2, gs2) = elabCon (env, denv) c2
305 344
306 val ku1 = kunif loc 345 val ku1 = kunif env loc
307 val ku2 = kunif loc 346 val ku2 = kunif env loc
308 347
309 val denv' = D.assert env denv (c1', c2') 348 val denv' = D.assert env denv (c1', c2')
310 val (c', k, gs4) = elabCon (env, denv') c 349 val (c', k, gs4) = elabCon (env, denv') c
311 in 350 in
312 checkKind env c1' k1 (L'.KRecord ku1, loc); 351 checkKind env c1' k1 (L'.KRecord ku1, loc);
329 E.NotBound => 368 E.NotBound =>
330 (conError env (UnboundCon (loc, s)); 369 (conError env (UnboundCon (loc, s));
331 (cerror, kerror, [])) 370 (cerror, kerror, []))
332 | E.Rel (n, k) => 371 | E.Rel (n, k) =>
333 let 372 let
334 val (c, k) = elabConHead (L'.CRel n, loc) k 373 val (c, k) = elabConHead env (L'.CRel n, loc) k
335 in 374 in
336 (c, k, []) 375 (c, k, [])
337 end 376 end
338 | E.Named (n, k) => 377 | E.Named (n, k) =>
339 let 378 let
340 val (c, k) = elabConHead (L'.CNamed n, loc) k 379 val (c, k) = elabConHead env (L'.CNamed n, loc) k
341 in 380 in
342 (c, k, []) 381 (c, k, [])
343 end) 382 end)
344 | L.CVar (m1 :: ms, s) => 383 | L.CVar (m1 :: ms, s) =>
345 (case E.lookupStr env m1 of 384 (case E.lookupStr env m1 of
356 395
357 val k = case E.projectCon env {sgn = sgn, str = str, field = s} of 396 val k = case E.projectCon env {sgn = sgn, str = str, field = s} of
358 NONE => (conError env (UnboundCon (loc, s)); 397 NONE => (conError env (UnboundCon (loc, s));
359 kerror) 398 kerror)
360 | SOME (k, _) => k 399 | SOME (k, _) => k
361 val (c, k) = elabConHead (L'.CModProj (n, ms, s), loc) k 400 val (c, k) = elabConHead env (L'.CModProj (n, ms, s), loc) k
362 in 401 in
363 (c, k, []) 402 (c, k, [])
364 end) 403 end)
365 404
366 | L.CApp (c1, c2) => 405 | L.CApp (c1, c2) =>
367 let 406 let
368 val (c1', k1, gs1) = elabCon (env, denv) c1 407 val (c1', k1, gs1) = elabCon (env, denv) c1
369 val (c2', k2, gs2) = elabCon (env, denv) c2 408 val (c2', k2, gs2) = elabCon (env, denv) c2
370 val dom = kunif loc 409 val dom = kunif env loc
371 val ran = kunif loc 410 val ran = kunif env loc
372 in 411 in
373 checkKind env c1' k1 (L'.KArrow (dom, ran), loc); 412 checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
374 checkKind env c2' k2 dom; 413 checkKind env c2' k2 dom;
375 ((L'.CApp (c1', c2'), loc), ran, gs1 @ gs2) 414 ((L'.CApp (c1', c2'), loc), ran, gs1 @ gs2)
376 end 415 end
377 | L.CAbs (x, ko, t) => 416 | L.CAbs (x, ko, t) =>
378 let 417 let
379 val k' = case ko of 418 val k' = case ko of
380 NONE => kunif loc 419 NONE => kunif env loc
381 | SOME k => elabKind env k 420 | SOME k => elabKind env k
382 val env' = E.pushCRel env x k' 421 val env' = E.pushCRel env x k'
383 val (t', tk, gs) = elabCon (env', D.enter denv) t 422 val (t', tk, gs) = elabCon (env', D.enter denv) t
384 in 423 in
385 ((L'.CAbs (x, k', t'), loc), 424 ((L'.CAbs (x, k', t'), loc),
399 | L.CName s => 438 | L.CName s =>
400 ((L'.CName s, loc), kname, []) 439 ((L'.CName s, loc), kname, [])
401 440
402 | L.CRecord xcs => 441 | L.CRecord xcs =>
403 let 442 let
404 val k = kunif loc 443 val k = kunif env loc
405 444
406 val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) => 445 val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) =>
407 let 446 let
408 val (x', xk, gs1) = elabCon (env, denv) x 447 val (x', xk, gs1) = elabCon (env, denv) x
409 val (c', ck, gs2) = elabCon (env, denv) c 448 val (c', ck, gs2) = elabCon (env, denv) c
437 end 476 end
438 | L.CConcat (c1, c2) => 477 | L.CConcat (c1, c2) =>
439 let 478 let
440 val (c1', k1, gs1) = elabCon (env, denv) c1 479 val (c1', k1, gs1) = elabCon (env, denv) c1
441 val (c2', k2, gs2) = elabCon (env, denv) c2 480 val (c2', k2, gs2) = elabCon (env, denv) c2
442 val ku = kunif loc 481 val ku = kunif env loc
443 val k = (L'.KRecord ku, loc) 482 val k = (L'.KRecord ku, loc)
444 in 483 in
445 checkKind env c1' k1 k; 484 checkKind env c1' k1 k;
446 checkKind env c2' k2 k; 485 checkKind env c2' k2 k;
447 ((L'.CConcat (c1', c2'), loc), k, 486 ((L'.CConcat (c1', c2'), loc), k,
448 D.prove env denv (c1', c2', loc) @ gs1 @ gs2) 487 D.prove env denv (c1', c2', loc) @ gs1 @ gs2)
449 end 488 end
450 | L.CMap => 489 | L.CMap =>
451 let 490 let
452 val dom = kunif loc 491 val dom = kunif env loc
453 val ran = kunif loc 492 val ran = kunif env loc
454 in 493 in
455 ((L'.CMap (dom, ran), loc), 494 ((L'.CMap (dom, ran), loc),
456 mapKind (dom, ran, loc), 495 mapKind (dom, ran, loc),
457 []) 496 [])
458 end 497 end
472 end 511 end
473 | L.CProj (c, n) => 512 | L.CProj (c, n) =>
474 let 513 let
475 val (c', k, gs) = elabCon (env, denv) c 514 val (c', k, gs) = elabCon (env, denv) c
476 515
477 val k' = kunif loc 516 val k' = kunif env loc
478 in 517 in
479 if n <= 0 then 518 if n <= 0 then
480 (conError env (ProjBounds (c', n)); 519 (conError env (ProjBounds (c', n));
481 (cerror, kerror, [])) 520 (cerror, kerror, []))
482 else 521 else
483 (checkKind env c' k (L'.KTupleUnif (loc, [(n, k')], ref NONE), loc); 522 (checkKind env c' k (L'.KTupleUnif (loc, [(n, k')], ref (L'.KUnknown (validateKind env))), loc);
484 ((L'.CProj (c', n), loc), k', gs)) 523 ((L'.CProj (c', n), loc), k', gs))
485 end 524 end
486 525
487 | L.CWild k => 526 | L.CWild k =>
488 let 527 let
489 val k' = elabKind env k 528 val k' = elabKind env k
490 in 529 in
491 (cunif (loc, k'), k', []) 530 (cunif env (loc, k'), k', [])
492 end 531 end
493 532
494 fun kunifsRemain k = 533 fun kunifsRemain k =
495 case k of 534 case k of
496 L'.KUnif (_, _, ref NONE) => true 535 L'.KUnif (_, _, ref (L'.KUnknown _)) => true
497 | L'.KTupleUnif (_, _, ref NONE) => true 536 | L'.KTupleUnif (_, _, ref (L'.KUnknown _)) => true
498 | _ => false 537 | _ => false
499 fun cunifsRemain c = 538 fun cunifsRemain c =
500 case c of 539 case c of
501 L'.CUnif (_, loc, k, _, r as ref NONE) => 540 L'.CUnif (_, loc, k, _, r as ref (L'.Unknown _)) =>
502 (case #1 (hnormKind k) of 541 (case #1 (hnormKind k) of
503 L'.KUnit => (r := SOME (L'.CUnit, loc); false) 542 L'.KUnit => (r := L'.Known (L'.CUnit, loc); false)
504 | _ => true) 543 | _ => true)
505 | _ => false 544 | _ => false
506 545
507 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain, 546 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
508 con = fn _ => false, 547 con = fn _ => false,
527 566
528 exception CUnify' of cunify_error 567 exception CUnify' of cunify_error
529 568
530 type record_summary = { 569 type record_summary = {
531 fields : (L'.con * L'.con) list, 570 fields : (L'.con * L'.con) list,
532 unifs : (L'.con * L'.con option ref) list, 571 unifs : (L'.con * L'.cunif ref) list,
533 others : L'.con list 572 others : L'.con list
534 } 573 }
535 574
536 fun summaryToCon {fields, unifs, others} = 575 fun summaryToCon {fields, unifs, others} =
537 let 576 let
596 | L'.CProj (c, n) => 635 | L'.CProj (c, n) =>
597 (case hnormKind (kindof env c) of 636 (case hnormKind (kindof env c) of
598 (L'.KTuple ks, _) => List.nth (ks, n - 1) 637 (L'.KTuple ks, _) => List.nth (ks, n - 1)
599 | (L'.KUnif (_, _, r), _) => 638 | (L'.KUnif (_, _, r), _) =>
600 let 639 let
601 val ku = kunif loc 640 val ku = kunif env loc
602 val k = (L'.KTupleUnif (loc, [(n, ku)], ref NONE), loc) 641 val k = (L'.KTupleUnif (loc, [(n, ku)], r), loc)
603 in 642 in
604 r := SOME k; 643 r := L'.KKnown k;
605 k 644 k
606 end 645 end
607 | (L'.KTupleUnif (_, nks, r), _) => 646 | (L'.KTupleUnif (_, nks, r), _) =>
608 (case ListUtil.search (fn (n', k) => if n' = n then SOME k else NONE) nks of 647 (case ListUtil.search (fn (n', k) => if n' = n then SOME k else NONE) nks of
609 SOME k => k 648 SOME k => k
610 | NONE => 649 | NONE =>
611 let 650 let
612 val ku = kunif loc 651 val ku = kunif env loc
613 val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), ref NONE), loc) 652 val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), r), loc)
614 in 653 in
615 r := SOME k; 654 r := L'.KKnown k;
616 k 655 k
617 end) 656 end)
618 | k => raise CUnify' (CKindof (k, c, "tuple"))) 657 | k => raise CUnify' (CKindof (k, c, "tuple")))
619 658
620 | L'.CError => kerror 659 | L'.CError => kerror
711 let 750 let
712 fun rkindof c = 751 fun rkindof c =
713 case hnormKind (kindof env c) of 752 case hnormKind (kindof env c) of
714 (L'.KRecord k, _) => k 753 (L'.KRecord k, _) => k
715 | (L'.KError, _) => kerror 754 | (L'.KError, _) => kerror
716 | (L'.KUnif (_, _, r), _) => 755 | (L'.KUnif (_, _, r as ref (L'.KUnknown f)), _) =>
717 let 756 let
718 val k = kunif (#2 c) 757 val k = kunif' f (#2 c)
719 in 758 in
720 r := SOME (L'.KRecord k, #2 c); 759 r := L'.KKnown (L'.KRecord k, #2 c);
721 k 760 k
722 end 761 end
723 | k => raise CUnify' (CKindof (k, c, "record")) 762 | k => raise CUnify' (CKindof (k, c, "record"))
724 763
725 val k1 = rkindof c1 764 val k1 = rkindof c1
749 in 788 in
750 {fields = #fields s1 @ #fields s2, 789 {fields = #fields s1 @ #fields s2,
751 unifs = #unifs s1 @ #unifs s2, 790 unifs = #unifs s1 @ #unifs s2,
752 others = #others s1 @ #others s2} 791 others = #others s1 @ #others s2}
753 end 792 end
754 | (L'.CUnif (nl, _, _, _, ref (SOME c)), _) => recordSummary env (E.mliftConInCon nl c) 793 | (L'.CUnif (nl, _, _, _, ref (L'.Known c)), _) => recordSummary env (E.mliftConInCon nl c)
755 | c' as (L'.CUnif (0, _, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []} 794 | c' as (L'.CUnif (0, _, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
756 | c' => {fields = [], unifs = [], others = [c']} 795 | c' => {fields = [], unifs = [], others = [c']}
757 in 796 in
758 sum 797 sum
759 end 798 end
843 882
844 val empties = ([], [], [], [], [], []) 883 val empties = ([], [], [], [], [], [])
845 884
846 val (unifs1, fs1, others1, unifs2, fs2, others2) = 885 val (unifs1, fs1, others1, unifs2, fs2, others2) =
847 case (unifs1, fs1, others1, unifs2, fs2, others2) of 886 case (unifs1, fs1, others1, unifs2, fs2, others2) of
848 orig as ([(_, r)], [], [], _, _, _) => 887 orig as ([(_, r as ref (L'.Unknown f))], [], [], _, _, _) =>
849 let 888 let
850 val c = unsummarize {fields = fs2, others = others2, unifs = unifs2} 889 val c = unsummarize {fields = fs2, others = others2, unifs = unifs2}
851 in 890 in
852 if occursCon r c then 891 if occursCon r c orelse not (f c) then
853 orig 892 orig
854 else 893 else
855 (r := SOME c; 894 (r := L'.Known c;
856 empties) 895 empties)
857 end 896 end
858 | orig as (_, _, _, [(_, r)], [], []) => 897 | orig as (_, _, _, [(_, r as ref (L'.Unknown f))], [], []) =>
859 let 898 let
860 val c = unsummarize {fields = fs1, others = others1, unifs = unifs1} 899 val c = unsummarize {fields = fs1, others = others1, unifs = unifs1}
861 in 900 in
862 if occursCon r c then 901 if occursCon r c orelse not (f c) then
863 orig 902 orig
864 else 903 else
865 (r := SOME c; 904 (r := L'.Known c;
866 empties) 905 empties)
867 end 906 end
868 | orig as ([(_, r1 as ref NONE)], _, [], [(_, r2 as ref NONE)], _, []) => 907 | orig as ([(_, r1 as ref (L'.Unknown f1))], _, [], [(_, r2 as ref (L'.Unknown f2))], _, []) =>
869 if List.all (fn (x1, _) => List.all (fn (x2, _) => consNeq env (x1, x2)) fs2) fs1 then 908 if List.all (fn (x1, _) => List.all (fn (x2, _) => consNeq env (x1, x2)) fs2) fs1 then
870 let 909 let
871 val kr = (L'.KRecord k, loc) 910 val kr = (L'.KRecord k, loc)
872 val u = cunif (loc, kr) 911 val u = cunif env (loc, kr)
912
913 val c1 = (L'.CConcat ((L'.CRecord (k, fs2), loc), u), loc)
914 val c2 = (L'.CConcat ((L'.CRecord (k, fs1), loc), u), loc)
873 in 915 in
874 r1 := SOME (L'.CConcat ((L'.CRecord (k, fs2), loc), u), loc); 916 if not (f1 c1) orelse not (f2 c2) then
875 r2 := SOME (L'.CConcat ((L'.CRecord (k, fs1), loc), u), loc); 917 orig
876 empties 918 else
919 (r1 := L'.Known c1;
920 r2 := L'.Known c2;
921 empties)
877 end 922 end
878 else 923 else
879 orig 924 orig
880 | orig => orig 925 | orig => orig
881 926
948 else 993 else
949 failure () 994 failure ()
950 in 995 in
951 (case (unifs1, fs1, others1, unifs2, fs2, others2) of 996 (case (unifs1, fs1, others1, unifs2, fs2, others2) of
952 (_, [], [], [], [], []) => 997 (_, [], [], [], [], []) =>
953 app (fn (_, r) => r := SOME empty) unifs1 998 app (fn (_, r) => r := L'.Known empty) unifs1
954 | ([], [], [], _, [], []) => 999 | ([], [], [], _, [], []) =>
955 app (fn (_, r) => r := SOME empty) unifs2 1000 app (fn (_, r) => r := L'.Known empty) unifs2
956 | (_, _, _, [], [], [cr as (L'.CUnif (nl, _, _, _, r), _)]) => 1001 | (_, _, _, [], [], [cr as (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _)]) =>
957 let 1002 let
958 val c = summaryToCon {fields = fs1, unifs = unifs1, others = others1} 1003 val c = summaryToCon {fields = fs1, unifs = unifs1, others = others1}
959 in 1004 in
960 if occursCon r c then 1005 if occursCon r c then
961 (reducedSummaries := NONE; 1006 (reducedSummaries := NONE;
962 raise CUnify' (COccursCheckFailed (cr, c))) 1007 raise CUnify' (COccursCheckFailed (cr, c)))
963 else 1008 else
964 (r := SOME (squish nl c)) 1009 let
1010 val sq = squish nl c
1011 in
1012 if not (f sq) then
1013 default ()
1014 else
1015 r := L'.Known sq
1016 end
965 handle CantSquish => default () 1017 handle CantSquish => default ()
966 end 1018 end
967 | ([], [], [cr as (L'.CUnif (nl, _, _, _, r), _)], _, _, _) => 1019 | ([], [], [cr as (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _)], _, _, _) =>
968 let 1020 let
969 val c = summaryToCon {fields = fs2, unifs = unifs2, others = others2} 1021 val c = summaryToCon {fields = fs2, unifs = unifs2, others = others2}
970 in 1022 in
971 if occursCon r c then 1023 if occursCon r c then
972 (reducedSummaries := NONE; 1024 (reducedSummaries := NONE;
973 raise CUnify' (COccursCheckFailed (cr, c))) 1025 raise CUnify' (COccursCheckFailed (cr, c)))
974 else 1026 else
975 (r := SOME (squish nl c)) 1027 let
1028 val sq = squish nl c
1029 in
1030 if not (f sq) then
1031 default ()
1032 else
1033 r := L'.Known sq
1034 end
976 handle CantSquish => default () 1035 handle CantSquish => default ()
977 end 1036 end
978 | _ => default ()) 1037 | _ => default ())
979 1038
980 (*before eprefaces "Summaries'" [("#1", p_summary env (normalizeRecordSummary env s1)), 1039 (*before eprefaces "Summaries'" [("#1", p_summary env (normalizeRecordSummary env s1)),
990 L'.CRecord (_, []) => unifyCons env loc r (L'.CRecord (dom, []), loc) 1049 L'.CRecord (_, []) => unifyCons env loc r (L'.CRecord (dom, []), loc)
991 | L'.CRecord (_, [(x, v)]) => 1050 | L'.CRecord (_, [(x, v)]) =>
992 let 1051 let
993 val v' = case dom of 1052 val v' = case dom of
994 (L'.KUnit, _) => (L'.CUnit, loc) 1053 (L'.KUnit, _) => (L'.CUnit, loc)
995 | _ => cunif (loc, dom) 1054 | _ => cunif env (loc, dom)
996 in 1055 in
997 unifyCons env loc v (L'.CApp (f, v'), loc); 1056 unifyCons env loc v (L'.CApp (f, v'), loc);
998 unifyCons env loc r (L'.CRecord (dom, [(x, v')]), loc) 1057 unifyCons env loc r (L'.CRecord (dom, [(x, v')]), loc)
999 end 1058 end
1000 | L'.CRecord (_, (x, v) :: rest) => 1059 | L'.CRecord (_, (x, v) :: rest) =>
1001 let 1060 let
1002 val r1 = cunif (loc, (L'.KRecord dom, loc)) 1061 val r1 = cunif env (loc, (L'.KRecord dom, loc))
1003 val r2 = cunif (loc, (L'.KRecord dom, loc)) 1062 val r2 = cunif env (loc, (L'.KRecord dom, loc))
1004 in 1063 in
1005 unfold (r1, (L'.CRecord (ran, [(x, v)]), loc)); 1064 unfold (r1, (L'.CRecord (ran, [(x, v)]), loc));
1006 unfold (r2, (L'.CRecord (ran, rest), loc)); 1065 unfold (r2, (L'.CRecord (ran, rest), loc));
1007 unifyCons env loc r (L'.CConcat (r1, r2), loc) 1066 unifyCons env loc r (L'.CConcat (r1, r2), loc)
1008 end 1067 end
1009 | L'.CConcat (c1', c2') => 1068 | L'.CConcat (c1', c2') =>
1010 let 1069 let
1011 val r1 = cunif (loc, (L'.KRecord dom, loc)) 1070 val r1 = cunif env (loc, (L'.KRecord dom, loc))
1012 val r2 = cunif (loc, (L'.KRecord dom, loc)) 1071 val r2 = cunif env (loc, (L'.KRecord dom, loc))
1013 in 1072 in
1014 unfold (r1, c1'); 1073 unfold (r1, c1');
1015 unfold (r2, c2'); 1074 unfold (r2, c2');
1016 unifyCons env loc r (L'.CConcat (r1, r2), loc) 1075 unifyCons env loc r (L'.CConcat (r1, r2), loc)
1017 end 1076 end
1018 | L'.CUnif (0, _, _, _, ur) => 1077 | L'.CUnif (0, _, _, _, ur as ref (L'.Unknown rf)) =>
1019 ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc) 1078 let
1079 val c' = (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc)
1080 in
1081 if not (rf c') then
1082 cunifyError env (CScope (c, c'))
1083 else
1084 ur := L'.Known c'
1085 end
1020 | _ => raise ex 1086 | _ => raise ex
1021 in 1087 in
1022 unfold (r, c) 1088 unfold (r, c)
1023 end 1089 end
1024 handle _ => raise ex 1090 handle _ => raise ex
1061 unifyCons' env loc c1 c2 1127 unifyCons' env loc c1 c2
1062 else 1128 else
1063 onFail () 1129 onFail ()
1064 in 1130 in
1065 case #1 (hnormCon env c2) of 1131 case #1 (hnormCon env c2) of
1066 L'.CUnif (0, _, k, _, r) => 1132 L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) =>
1067 (case #1 (hnormKind k) of 1133 (case #1 (hnormKind k) of
1068 L'.KTuple ks => 1134 L'.KTuple ks =>
1069 let 1135 let
1070 val loc = #2 c2 1136 val loc = #2 c2
1071 val us = map (fn k => cunif (loc, k)) ks 1137 val us = map (fn k => cunif' f (loc, k)) ks
1072 in 1138 in
1073 r := SOME (L'.CTuple us, loc); 1139 r := L'.Known (L'.CTuple us, loc);
1074 unifyCons' env loc c1All (List.nth (us, n2 - 1)) 1140 unifyCons' env loc c1All (List.nth (us, n2 - 1))
1075 end 1141 end
1076 | _ => tryNormal ()) 1142 | _ => tryNormal ())
1077 | _ => tryNormal () 1143 | _ => tryNormal ()
1078 end 1144 end
1079 | _ => onFail () 1145 | _ => onFail ()
1080 in 1146 in
1081 case #1 (hnormCon env c1) of 1147 case #1 (hnormCon env c1) of
1082 L'.CUnif (0, _, k, _, r) => 1148 L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) =>
1083 (case #1 (hnormKind k) of 1149 (case #1 (hnormKind k) of
1084 L'.KTuple ks => 1150 L'.KTuple ks =>
1085 let 1151 let
1086 val loc = #2 c1 1152 val loc = #2 c1
1087 val us = map (fn k => cunif (loc, k)) ks 1153 val us = map (fn k => cunif' f (loc, k)) ks
1088 in 1154 in
1089 r := SOME (L'.CTuple us, loc); 1155 r := L'.Known (L'.CTuple us, loc);
1090 unifyCons' env loc (List.nth (us, n1 - 1)) c2All 1156 unifyCons' env loc (List.nth (us, n1 - 1)) c2All
1091 end 1157 end
1092 | _ => trySnd ()) 1158 | _ => trySnd ())
1093 | _ => trySnd () 1159 | _ => trySnd ()
1094 end 1160 end
1095 1161
1096 fun projSpecial2 (c2, n2, onFail) = 1162 fun projSpecial2 (c2, n2, onFail) =
1097 case #1 (hnormCon env c2) of 1163 case #1 (hnormCon env c2) of
1098 L'.CUnif (0, _, k, _, r) => 1164 L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) =>
1099 (case #1 (hnormKind k) of 1165 (case #1 (hnormKind k) of
1100 L'.KTuple ks => 1166 L'.KTuple ks =>
1101 let 1167 let
1102 val loc = #2 c2 1168 val loc = #2 c2
1103 val us = map (fn k => cunif (loc, k)) ks 1169 val us = map (fn k => cunif' f (loc, k)) ks
1104 in 1170 in
1105 r := SOME (L'.CTuple us, loc); 1171 r := L'.Known (L'.CTuple us, loc);
1106 unifyCons' env loc c1All (List.nth (us, n2 - 1)) 1172 unifyCons' env loc c1All (List.nth (us, n2 - 1))
1107 end 1173 end
1108 | _ => onFail ()) 1174 | _ => onFail ())
1109 | _ => onFail () 1175 | _ => onFail ()
1110 1176
1121 1187
1122 case (c1, c2) of 1188 case (c1, c2) of
1123 (L'.CError, _) => () 1189 (L'.CError, _) => ()
1124 | (_, L'.CError) => () 1190 | (_, L'.CError) => ()
1125 1191
1126 | (L'.CUnif (nl1, loc1, k1, _, r1), L'.CUnif (nl2, loc2, k2, _, r2)) => 1192 | (L'.CUnif (nl1, loc1, k1, _, r1 as ref (L'.Unknown f1)), L'.CUnif (nl2, loc2, k2, _, r2 as ref (L'.Unknown f2))) =>
1127 if r1 = r2 andalso nl1 = nl2 then 1193 if r1 = r2 andalso nl1 = nl2 then
1128 () 1194 ()
1129 else if nl1 = 0 then 1195 else if nl1 = 0 then
1130 (unifyKinds env k1 k2; 1196 (unifyKinds env k1 k2;
1131 r1 := SOME c2All) 1197 if f1 c2All then
1198 r1 := L'.Known c2All
1199 else
1200 err CScope)
1132 else if nl2 = 0 then 1201 else if nl2 = 0 then
1133 (unifyKinds env k1 k2; 1202 (unifyKinds env k1 k2;
1134 r2 := SOME c1All) 1203 if f2 c1All then
1204 r2 := L'.Known c1All
1205 else
1206 err CScope)
1135 else 1207 else
1136 err (fn _ => TooLifty (loc1, loc2)) 1208 err (fn _ => TooLifty (loc1, loc2))
1137 1209
1138 | (L'.CUnif (0, _, _, _, r), _) => 1210 | (L'.CUnif (0, _, _, _, r as ref (L'.Unknown f)), _) =>
1211 if occursCon r c2All then
1212 err COccursCheckFailed
1213 else if f c2All then
1214 r := L'.Known c2All
1215 else
1216 err CScope
1217 | (_, L'.CUnif (0, _, _, _, r as ref (L'.Unknown f))) =>
1218 if occursCon r c1All then
1219 err COccursCheckFailed
1220 else if f c1All then
1221 r := L'.Known c1All
1222 else
1223 err CScope
1224
1225 | (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _) =>
1139 if occursCon r c2All then 1226 if occursCon r c2All then
1140 err COccursCheckFailed 1227 err COccursCheckFailed
1141 else 1228 else
1142 r := SOME c2All 1229 (let
1143 | (_, L'.CUnif (0, _, _, _, r)) => 1230 val sq = squish nl c2All
1231 in
1232 if f sq then
1233 r := L'.Known sq
1234 else
1235 err CScope
1236 end
1237 handle CantSquish => err (fn _ => TooDeep))
1238 | (_, L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f))) =>
1144 if occursCon r c1All then 1239 if occursCon r c1All then
1145 err COccursCheckFailed 1240 err COccursCheckFailed
1146 else 1241 else
1147 r := SOME c1All 1242 (let
1148 1243 val sq = squish nl c1All
1149 | (L'.CUnif (nl, _, _, _, r), _) => 1244 in
1150 if occursCon r c2All then 1245 if f sq then
1151 err COccursCheckFailed 1246 r := L'.Known sq
1152 else 1247 else
1153 (r := SOME (squish nl c2All) 1248 err CScope
1154 handle CantSquish => err (fn _ => TooDeep)) 1249 end
1155 | (_, L'.CUnif (nl, _, _, _, r)) =>
1156 if occursCon r c1All then
1157 err COccursCheckFailed
1158 else
1159 (r := SOME (squish nl c1All)
1160 handle CantSquish => err (fn _ => TooDeep)) 1250 handle CantSquish => err (fn _ => TooDeep))
1161 1251
1162 | (L'.CRecord _, _) => isRecord () 1252 | (L'.CRecord _, _) => isRecord ()
1163 | (_, L'.CRecord _) => isRecord () 1253 | (_, L'.CRecord _) => isRecord ()
1164 | (L'.CConcat _, _) => isRecord () 1254 | (L'.CConcat _, _) => isRecord ()
1167 1257
1168 | (L'.CUnit, L'.CUnit) => () 1258 | (L'.CUnit, L'.CUnit) => ()
1169 1259
1170 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => 1260 | (L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
1171 (unifyCons' env loc d1 d2; 1261 (unifyCons' env loc d1 d2;
1172 unifyCons' env loc r1 r2) 1262 unifyCons' env loc r1 r2)
1173 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => 1263 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
1174 if expl1 <> expl2 then 1264 if expl1 <> expl2 then
1175 err CExplicitness 1265 err CExplicitness
1176 else 1266 else
1177 (unifyKinds env d1 d2; 1267 (unifyKinds env d1 d2;
1293 let 1383 let
1294 fun unravelKind (t, e) = 1384 fun unravelKind (t, e) =
1295 case hnormCon env t of 1385 case hnormCon env t of
1296 (L'.TKFun (x, t'), _) => 1386 (L'.TKFun (x, t'), _) =>
1297 let 1387 let
1298 val u = kunif loc 1388 val u = kunif env loc
1299 1389
1300 val t'' = subKindInCon (0, u) t' 1390 val t'' = subKindInCon (0, u) t'
1301 in 1391 in
1302 unravelKind (t'', (L'.EKApp (e, u), loc)) 1392 unravelKind (t'', (L'.EKApp (e, u), loc))
1303 end 1393 end
1305 1395
1306 fun unravel (t, e) = 1396 fun unravel (t, e) =
1307 case hnormCon env t of 1397 case hnormCon env t of
1308 (L'.TKFun (x, t'), _) => 1398 (L'.TKFun (x, t'), _) =>
1309 let 1399 let
1310 val u = kunif loc 1400 val u = kunif env loc
1311 1401
1312 val t'' = subKindInCon (0, u) t' 1402 val t'' = subKindInCon (0, u) t'
1313 in 1403 in
1314 unravel (t'', (L'.EKApp (e, u), loc)) 1404 unravel (t'', (L'.EKApp (e, u), loc))
1315 end 1405 end
1316 | (L'.TCFun (L'.Implicit, x, k, t'), _) => 1406 | (L'.TCFun (L'.Implicit, x, k, t'), _) =>
1317 let 1407 let
1318 val u = cunif (loc, k) 1408 val u = cunif env (loc, k)
1319 1409
1320 val t'' = subConInCon env (0, u) t' 1410 val t'' = subConInCon env (0, u) t'
1321 in 1411 in
1322 unravel (t'', (L'.ECApp (e, u), loc)) 1412 unravel (t'', (L'.ECApp (e, u), loc))
1323 end 1413 end
1391 | (SOME _, NONE) => (expError env (PatHasArg loc); 1481 | (SOME _, NONE) => (expError env (PatHasArg loc);
1392 rerror) 1482 rerror)
1393 | (NONE, NONE) => 1483 | (NONE, NONE) =>
1394 let 1484 let
1395 val k = (L'.KType, loc) 1485 val k = (L'.KType, loc)
1396 val unifs = map (fn _ => cunif (loc, k)) xs 1486 val unifs = map (fn _ => cunif env (loc, k)) xs
1397 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs 1487 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
1398 in 1488 in
1399 (((L'.PCon (dk, pc, unifs, NONE), loc), dn), 1489 (((L'.PCon (dk, pc, unifs, NONE), loc), dn),
1400 (env, bound)) 1490 (env, bound))
1401 end 1491 end
1402 | (SOME p, SOME t) => 1492 | (SOME p, SOME t) =>
1403 let 1493 let
1404 val ((p', pt), (env, bound)) = elabPat (p, (env, bound)) 1494 val ((p', pt), (env, bound)) = elabPat (p, (env, bound))
1405 1495
1406 val k = (L'.KType, loc) 1496 val k = (L'.KType, loc)
1407 val unifs = map (fn _ => cunif (loc, k)) xs 1497 val unifs = map (fn _ => cunif env (loc, k)) xs
1408 val nxs = length unifs - 1 1498 val nxs = length unifs - 1
1409 val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i, 1499 val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i,
1410 E.mliftConInCon (nxs - i) u) t) t unifs 1500 E.mliftConInCon (nxs - i) u) t) t unifs
1411 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs 1501 val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs
1412 in 1502 in
1414 (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn), 1504 (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn),
1415 (env, bound)) 1505 (env, bound))
1416 end 1506 end
1417 in 1507 in
1418 case p of 1508 case p of
1419 L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))), 1509 L.PWild => (((L'.PWild, loc), cunif env (loc, (L'.KType, loc))),
1420 (env, bound)) 1510 (env, bound))
1421 | L.PVar x => 1511 | L.PVar x =>
1422 let 1512 let
1423 val t = if SS.member (bound, x) then 1513 val t = if SS.member (bound, x) then
1424 (expError env (DuplicatePatternVariable (loc, x)); 1514 (expError env (DuplicatePatternVariable (loc, x));
1425 terror) 1515 terror)
1426 else 1516 else
1427 cunif (loc, (L'.KType, loc)) 1517 cunif env (loc, (L'.KType, loc))
1428 in 1518 in
1429 (((L'.PVar (x, t), loc), t), 1519 (((L'.PVar (x, t), loc), t),
1430 (E.pushERel env x t, SS.add (bound, x))) 1520 (E.pushERel env x t, SS.add (bound, x)))
1431 end 1521 end
1432 | L.PPrim p => (((L'.PPrim p, loc), primType env p), 1522 | L.PPrim p => (((L'.PPrim p, loc), primType env p),
1471 1561
1472 val k = (L'.KType, loc) 1562 val k = (L'.KType, loc)
1473 val c = (L'.CRecord (k, map (fn (x, _, t) => ((L'.CName x, loc), t)) xpts), loc) 1563 val c = (L'.CRecord (k, map (fn (x, _, t) => ((L'.CName x, loc), t)) xpts), loc)
1474 val c = 1564 val c =
1475 if flex then 1565 if flex then
1476 (L'.CConcat (c, cunif (loc, (L'.KRecord k, loc))), loc) 1566 (L'.CConcat (c, cunif env (loc, (L'.KRecord k, loc))), loc)
1477 else 1567 else
1478 c 1568 c
1479 in 1569 in
1480 (((L'.PRecord xpts, loc), 1570 (((L'.PRecord xpts, loc),
1481 (L'.TRecord c, loc)), 1571 (L'.TRecord c, loc)),
1776 val c2 = normClassConstraint env c2 1866 val c2 = normClassConstraint env c2
1777 in 1867 in
1778 (L'.TFun (c1, c2), loc) 1868 (L'.TFun (c1, c2), loc)
1779 end 1869 end
1780 | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc) 1870 | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc)
1781 | L'.CUnif (nl, _, _, _, ref (SOME c)) => normClassConstraint env (E.mliftConInCon nl c) 1871 | L'.CUnif (nl, _, _, _, ref (L'.Known c)) => normClassConstraint env (E.mliftConInCon nl c)
1782 | _ => unmodCon env (c, loc) 1872 | _ => unmodCon env (c, loc)
1783 1873
1784 fun findHead e e' = 1874 fun findHead e e' =
1785 let 1875 let
1786 fun findHead (e, _) = 1876 fun findHead (e, _) =
1885 Mods = #Mods r} 1975 Mods = #Mods r}
1886 end 1976 end
1887 1977
1888 fun chaseUnifs c = 1978 fun chaseUnifs c =
1889 case #1 c of 1979 case #1 c of
1890 L'.CUnif (_, _, _, _, ref (SOME c)) => chaseUnifs c 1980 L'.CUnif (_, _, _, _, ref (L'.Known c)) => chaseUnifs c
1891 | _ => c 1981 | _ => c
1892 1982
1893 fun elabExp (env, denv) (eAll as (e, loc)) = 1983 fun elabExp (env, denv) (eAll as (e, loc)) =
1894 let 1984 let
1895 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*) 1985 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*)
1935 end) 2025 end)
1936 2026
1937 | L.EWild => 2027 | L.EWild =>
1938 let 2028 let
1939 val r = ref NONE 2029 val r = ref NONE
1940 val c = cunif (loc, (L'.KType, loc)) 2030 val c = cunif env (loc, (L'.KType, loc))
1941 in 2031 in
1942 ((L'.EUnif r, loc), c, [TypeClass (env, c, r, loc)]) 2032 ((L'.EUnif r, loc), c, [TypeClass (env, c, r, loc)])
1943 end 2033 end
1944 2034
1945 | L.EApp (e1, e2) => 2035 | L.EApp (e1, e2) =>
1946 let 2036 let
1947 val (e1', t1, gs1) = elabExp (env, denv) e1 2037 val (e1', t1, gs1) = elabExp (env, denv) e1
1948 2038
1949 val (e2', t2, gs2) = elabExp (env, denv) e2 2039 val (e2', t2, gs2) = elabExp (env, denv) e2
1950 2040
1951 val dom = cunif (loc, ktype) 2041 val dom = cunif env (loc, ktype)
1952 val ran = cunif (loc, ktype) 2042 val ran = cunif env (loc, ktype)
1953 val t = (L'.TFun (dom, ran), loc) 2043 val t = (L'.TFun (dom, ran), loc)
1954 2044
1955 val () = checkCon env e1' t1 t 2045 val () = checkCon env e1' t1 t
1956 val () = checkCon env e2' t2 dom 2046 val () = checkCon env e2' t2 dom
1957 2047
1964 (ef, et, gs1 @ gs2 @ gs3) 2054 (ef, et, gs1 @ gs2 @ gs3)
1965 end 2055 end
1966 | L.EAbs (x, to, e) => 2056 | L.EAbs (x, to, e) =>
1967 let 2057 let
1968 val (t', gs1) = case to of 2058 val (t', gs1) = case to of
1969 NONE => (cunif (loc, ktype), []) 2059 NONE => (cunif env (loc, ktype), [])
1970 | SOME t => 2060 | SOME t =>
1971 let 2061 let
1972 val (t', tk, gs) = elabCon (env, denv) t 2062 val (t', tk, gs) = elabCon (env, denv) t
1973 in 2063 in
1974 checkKind env t' tk ktype; 2064 checkKind env t' tk ktype;
2040 | L.EDisjoint (c1, c2, e) => 2130 | L.EDisjoint (c1, c2, e) =>
2041 let 2131 let
2042 val (c1', k1, gs1) = elabCon (env, denv) c1 2132 val (c1', k1, gs1) = elabCon (env, denv) c1
2043 val (c2', k2, gs2) = elabCon (env, denv) c2 2133 val (c2', k2, gs2) = elabCon (env, denv) c2
2044 2134
2045 val ku1 = kunif loc 2135 val ku1 = kunif env loc
2046 val ku2 = kunif loc 2136 val ku2 = kunif env loc
2047 2137
2048 val denv' = D.assert env denv (c1', c2') 2138 val denv' = D.assert env denv (c1', c2')
2049 val (e', t, gs3) = elabExp (env, denv') e 2139 val (e', t, gs3) = elabExp (env, denv') e
2050 in 2140 in
2051 checkKind env c1' k1 (L'.KRecord ku1, loc); 2141 checkKind env c1' k1 (L'.KRecord ku1, loc);
2055 end 2145 end
2056 | L.EDisjointApp e => 2146 | L.EDisjointApp e =>
2057 let 2147 let
2058 val (e', t, gs1) = elabExp (env, denv) e 2148 val (e', t, gs1) = elabExp (env, denv) e
2059 2149
2060 val k1 = kunif loc 2150 val k1 = kunif env loc
2061 val c1 = cunif (loc, (L'.KRecord k1, loc)) 2151 val c1 = cunif env (loc, (L'.KRecord k1, loc))
2062 val k2 = kunif loc 2152 val k2 = kunif env loc
2063 val c2 = cunif (loc, (L'.KRecord k2, loc)) 2153 val c2 = cunif env (loc, (L'.KRecord k2, loc))
2064 val t' = cunif (loc, ktype) 2154 val t' = cunif env (loc, ktype)
2065 val () = checkCon env e' t (L'.TDisjoint (c1, c2, t'), loc) 2155 val () = checkCon env e' t (L'.TDisjoint (c1, c2, t'), loc)
2066 val gs2 = D.prove env denv (c1, c2, loc) 2156 val gs2 = D.prove env denv (c1, c2, loc)
2067 in 2157 in
2068 (e', (#1 (chaseUnifs t'), loc), enD gs2 @ gs1) 2158 (e', (#1 (chaseUnifs t'), loc), enD gs2 @ gs1)
2069 end 2159 end
2113 | L.EField (e, c) => 2203 | L.EField (e, c) =>
2114 let 2204 let
2115 val (e', et, gs1) = elabExp (env, denv) e 2205 val (e', et, gs1) = elabExp (env, denv) e
2116 val (c', ck, gs2) = elabCon (env, denv) c 2206 val (c', ck, gs2) = elabCon (env, denv) c
2117 2207
2118 val ft = cunif (loc, ktype) 2208 val ft = cunif env (loc, ktype)
2119 val rest = cunif (loc, ktype_record) 2209 val rest = cunif env (loc, ktype_record)
2120 val first = (L'.CRecord (ktype, [(c', ft)]), loc) 2210 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
2121 val () = checkCon env e' et 2211 val () = checkCon env e' et
2122 (L'.TRecord (L'.CConcat (first, rest), loc), loc); 2212 (L'.TRecord (L'.CConcat (first, rest), loc), loc);
2123 val gs3 = D.prove env denv (first, rest, loc) 2213 val gs3 = D.prove env denv (first, rest, loc)
2124 in 2214 in
2128 | L.EConcat (e1, e2) => 2218 | L.EConcat (e1, e2) =>
2129 let 2219 let
2130 val (e1', e1t, gs1) = elabExp (env, denv) e1 2220 val (e1', e1t, gs1) = elabExp (env, denv) e1
2131 val (e2', e2t, gs2) = elabExp (env, denv) e2 2221 val (e2', e2t, gs2) = elabExp (env, denv) e2
2132 2222
2133 val r1 = cunif (loc, ktype_record) 2223 val r1 = cunif env (loc, ktype_record)
2134 val r2 = cunif (loc, ktype_record) 2224 val r2 = cunif env (loc, ktype_record)
2135 2225
2136 val () = checkCon env e1' e1t (L'.TRecord r1, loc) 2226 val () = checkCon env e1' e1t (L'.TRecord r1, loc)
2137 val () = checkCon env e2' e2t (L'.TRecord r2, loc) 2227 val () = checkCon env e2' e2t (L'.TRecord r2, loc)
2138 2228
2139 val gs3 = D.prove env denv (r1, r2, loc) 2229 val gs3 = D.prove env denv (r1, r2, loc)
2145 | L.ECut (e, c) => 2235 | L.ECut (e, c) =>
2146 let 2236 let
2147 val (e', et, gs1) = elabExp (env, denv) e 2237 val (e', et, gs1) = elabExp (env, denv) e
2148 val (c', ck, gs2) = elabCon (env, denv) c 2238 val (c', ck, gs2) = elabCon (env, denv) c
2149 2239
2150 val ft = cunif (loc, ktype) 2240 val ft = cunif env (loc, ktype)
2151 val rest = cunif (loc, ktype_record) 2241 val rest = cunif env (loc, ktype_record)
2152 val first = (L'.CRecord (ktype, [(c', ft)]), loc) 2242 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
2153 2243
2154 val () = checkCon env e' et 2244 val () = checkCon env e' et
2155 (L'.TRecord (L'.CConcat (first, rest), loc), loc) 2245 (L'.TRecord (L'.CConcat (first, rest), loc), loc)
2156 2246
2163 | L.ECutMulti (e, c) => 2253 | L.ECutMulti (e, c) =>
2164 let 2254 let
2165 val (e', et, gs1) = elabExp (env, denv) e 2255 val (e', et, gs1) = elabExp (env, denv) e
2166 val (c', ck, gs2) = elabCon (env, denv) c 2256 val (c', ck, gs2) = elabCon (env, denv) c
2167 2257
2168 val rest = cunif (loc, ktype_record) 2258 val rest = cunif env (loc, ktype_record)
2169 2259
2170 val () = checkCon env e' et 2260 val () = checkCon env e' et
2171 (L'.TRecord (L'.CConcat (c', rest), loc), loc) 2261 (L'.TRecord (L'.CConcat (c', rest), loc), loc)
2172 2262
2173 val gs3 = D.prove env denv (c', rest, loc) 2263 val gs3 = D.prove env denv (c', rest, loc)
2178 end 2268 end
2179 2269
2180 | L.ECase (e, pes) => 2270 | L.ECase (e, pes) =>
2181 let 2271 let
2182 val (e', et, gs1) = elabExp (env, denv) e 2272 val (e', et, gs1) = elabExp (env, denv) e
2183 val result = cunif (loc, (L'.KType, loc)) 2273 val result = cunif env (loc, (L'.KType, loc))
2184 val (pes', gs) = ListUtil.foldlMap 2274 val (pes', gs) = ListUtil.foldlMap
2185 (fn ((p, e), gs) => 2275 (fn ((p, e), gs) =>
2186 let 2276 let
2187 val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty)) 2277 val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty))
2188 2278
2253 2343
2254 val (vis, gs) = ListUtil.foldlMap 2344 val (vis, gs) = ListUtil.foldlMap
2255 (fn ((x, co, e), gs) => 2345 (fn ((x, co, e), gs) =>
2256 let 2346 let
2257 val (c', _, gs1) = case co of 2347 val (c', _, gs1) = case co of
2258 NONE => (cunif (loc, ktype), ktype, []) 2348 NONE => (cunif env (loc, ktype), ktype, [])
2259 | SOME c => elabCon (env, denv) c 2349 | SOME c => elabCon (env, denv) c
2260 in 2350 in
2261 ((x, c', e), enD gs1 @ gs) 2351 ((x, c', e), enD gs1 @ gs)
2262 end) gs vis 2352 end) gs vis
2263 2353
2337 end 2427 end
2338 2428
2339 | L.SgiCon (x, ko, c) => 2429 | L.SgiCon (x, ko, c) =>
2340 let 2430 let
2341 val k' = case ko of 2431 val k' = case ko of
2342 NONE => kunif loc 2432 NONE => kunif env loc
2343 | SOME k => elabKind env k 2433 | SOME k => elabKind env k
2344 2434
2345 val (c', ck, gs') = elabCon (env, denv) c 2435 val (c', ck, gs') = elabCon (env, denv) c
2346 val (env', n) = E.pushCNamed env x k' (SOME c') 2436 val (env', n) = E.pushCNamed env x k' (SOME c')
2347 in 2437 in
2477 | L.SgiTable (x, c, pe, ce) => 2567 | L.SgiTable (x, c, pe, ce) =>
2478 let 2568 let
2479 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc) 2569 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
2480 2570
2481 val (c', ck, gs') = elabCon (env, denv) c 2571 val (c', ck, gs') = elabCon (env, denv) c
2482 val pkey = cunif (loc, cstK) 2572 val pkey = cunif env (loc, cstK)
2483 val visible = cunif (loc, cstK) 2573 val visible = cunif env (loc, cstK)
2484 val (env', ds, uniques) = 2574 val (env', ds, uniques) =
2485 case (#1 pe, #1 ce) of 2575 case (#1 pe, #1 ce) of
2486 (L.EVar (["Basis"], "no_primary_key", _), L.EVar (["Basis"], "no_constraint", _)) => 2576 (L.EVar (["Basis"], "no_primary_key", _), L.EVar (["Basis"], "no_constraint", _)) =>
2487 let 2577 let
2488 val x' = x ^ "_hidden_constraints" 2578 val x' = x ^ "_hidden_constraints"
2554 val (c1', k1, gs1) = elabCon (env, denv) c1 2644 val (c1', k1, gs1) = elabCon (env, denv) c1
2555 val (c2', k2, gs2) = elabCon (env, denv) c2 2645 val (c2', k2, gs2) = elabCon (env, denv) c2
2556 2646
2557 val denv = D.assert env denv (c1', c2') 2647 val denv = D.assert env denv (c1', c2')
2558 in 2648 in
2559 checkKind env c1' k1 (L'.KRecord (kunif loc), loc); 2649 checkKind env c1' k1 (L'.KRecord (kunif env loc), loc);
2560 checkKind env c2' k2 (L'.KRecord (kunif loc), loc); 2650 checkKind env c2' k2 (L'.KRecord (kunif env loc), loc);
2561 2651
2562 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2)) 2652 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2))
2563 end 2653 end
2564 2654
2565 | L.SgiClassAbs (x, k) => 2655 | L.SgiClassAbs (x, k) =>
3419 else 3509 else
3420 NONE 3510 NONE
3421 end 3511 end
3422 3512
3423 | L'.KError => NONE 3513 | L'.KError => NONE
3424 | L'.KUnif (_, _, ref (SOME k)) => decompileKind k 3514 | L'.KUnif (_, _, ref (L'.KKnown k)) => decompileKind k
3425 | L'.KUnif _ => NONE 3515 | L'.KUnif _ => NONE
3426 | L'.KTupleUnif (_, _, ref (SOME k)) => decompileKind k 3516 | L'.KTupleUnif (_, _, ref (L'.KKnown k)) => decompileKind k
3427 | L'.KTupleUnif _ => NONE 3517 | L'.KTupleUnif _ => NONE
3428 3518
3429 | L'.KRel _ => NONE 3519 | L'.KRel _ => NONE
3430 | L'.KFun _ => NONE 3520 | L'.KFun _ => NONE
3431 3521
3470 | L'.CConcat (c1, c2) => 3560 | L'.CConcat (c1, c2) =>
3471 (case (decompileCon env c1, decompileCon env c2) of 3561 (case (decompileCon env c1, decompileCon env c2) of
3472 (SOME c1, SOME c2) => SOME (L.CConcat (c1, c2), loc) 3562 (SOME c1, SOME c2) => SOME (L.CConcat (c1, c2), loc)
3473 | _ => NONE) 3563 | _ => NONE)
3474 | L'.CUnit => SOME (L.CUnit, loc) 3564 | L'.CUnit => SOME (L.CUnit, loc)
3475 | L'.CUnif (nl, _, _, _, ref (SOME c)) => decompileCon env (E.mliftConInCon nl c) 3565 | L'.CUnif (nl, _, _, _, ref (L'.Known c)) => decompileCon env (E.mliftConInCon nl c)
3476 3566
3477 | L'.CApp (f, x) => 3567 | L'.CApp (f, x) =>
3478 (case (decompileCon env f, decompileCon env x) of 3568 (case (decompileCon env f, decompileCon env x) of
3479 (SOME f, SOME x) => SOME (L.CApp (f, x), loc) 3569 (SOME f, SOME x) => SOME (L.CApp (f, x), loc)
3480 | _ => NONE) 3570 | _ => NONE)
3597 val r = 3687 val r =
3598 case d of 3688 case d of
3599 L.DCon (x, ko, c) => 3689 L.DCon (x, ko, c) =>
3600 let 3690 let
3601 val k' = case ko of 3691 val k' = case ko of
3602 NONE => kunif loc 3692 NONE => kunif env loc
3603 | SOME k => elabKind env k 3693 | SOME k => elabKind env k
3604 3694
3605 val (c', ck, gs') = elabCon (env, denv) c 3695 val (c', ck, gs') = elabCon (env, denv) c
3606 val (env', n) = E.pushCNamed env x k' (SOME c') 3696 val (env', n) = E.pushCNamed env x k' (SOME c')
3607 in 3697 in
3721 end) 3811 end)
3722 3812
3723 | L.DVal (x, co, e) => 3813 | L.DVal (x, co, e) =>
3724 let 3814 let
3725 val (c', _, gs1) = case co of 3815 val (c', _, gs1) = case co of
3726 NONE => (cunif (loc, ktype), ktype, []) 3816 NONE => (cunif env (loc, ktype), ktype, [])
3727 | SOME c => elabCon (env, denv) c 3817 | SOME c => elabCon (env, denv) c
3728 3818
3729 val (e', et, gs2) = elabExp (env, denv) e 3819 val (e', et, gs2) = elabExp (env, denv) e
3730 3820
3731 val () = checkCon env e' et c' 3821 val () = checkCon env e' et c'
3749 3839
3750 val (vis, gs) = ListUtil.foldlMap 3840 val (vis, gs) = ListUtil.foldlMap
3751 (fn ((x, co, e), gs) => 3841 (fn ((x, co, e), gs) =>
3752 let 3842 let
3753 val (c', _, gs1) = case co of 3843 val (c', _, gs1) = case co of
3754 NONE => (cunif (loc, ktype), ktype, []) 3844 NONE => (cunif env (loc, ktype), ktype, [])
3755 | SOME c => elabCon (env, denv) c 3845 | SOME c => elabCon (env, denv) c
3756 val c' = normClassConstraint env c' 3846 val c' = normClassConstraint env c'
3757 in 3847 in
3758 ((x, c', e), enD gs1 @ gs) 3848 ((x, c', e), enD gs1 @ gs)
3759 end) gs vis 3849 end) gs vis
3866 val (c2', k2, gs2) = elabCon (env, denv) c2 3956 val (c2', k2, gs2) = elabCon (env, denv) c2
3867 val gs3 = D.prove env denv (c1', c2', loc) 3957 val gs3 = D.prove env denv (c1', c2', loc)
3868 3958
3869 val denv' = D.assert env denv (c1', c2') 3959 val denv' = D.assert env denv (c1', c2')
3870 in 3960 in
3871 checkKind env c1' k1 (L'.KRecord (kunif loc), loc); 3961 checkKind env c1' k1 (L'.KRecord (kunif env loc), loc);
3872 checkKind env c2' k2 (L'.KRecord (kunif loc), loc); 3962 checkKind env c2' k2 (L'.KRecord (kunif env loc), loc);
3873 3963
3874 ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ gs)) 3964 ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ gs))
3875 end 3965 end
3876 3966
3877 | L.DOpenConstraints (m, ms) => 3967 | L.DOpenConstraints (m, ms) =>
3957 | L.DTable (x, c, pe, ce) => 4047 | L.DTable (x, c, pe, ce) =>
3958 let 4048 let
3959 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc) 4049 val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc)
3960 4050
3961 val (c', k, gs') = elabCon (env, denv) c 4051 val (c', k, gs') = elabCon (env, denv) c
3962 val pkey = cunif (loc, cstK) 4052 val pkey = cunif env (loc, cstK)
3963 val uniques = cunif (loc, cstK) 4053 val uniques = cunif env (loc, cstK)
3964 4054
3965 val ct = tableOf () 4055 val ct = tableOf ()
3966 val ct = (L'.CApp (ct, c'), loc) 4056 val ct = (L'.CApp (ct, c'), loc)
3967 val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc) 4057 val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc)
3968 4058
3993 | L.DView (x, e) => 4083 | L.DView (x, e) =>
3994 let 4084 let
3995 val (e', t, gs') = elabExp (env, denv) e 4085 val (e', t, gs') = elabExp (env, denv) e
3996 4086
3997 val k = (L'.KRecord (L'.KType, loc), loc) 4087 val k = (L'.KRecord (L'.KType, loc), loc)
3998 val fs = cunif (loc, k) 4088 val fs = cunif env (loc, k)
3999 val ts = cunif (loc, (L'.KRecord k, loc)) 4089 val ts = cunif env (loc, (L'.KRecord k, loc))
4000 val tf = (L'.CApp ((L'.CMap (k, k), loc), 4090 val tf = (L'.CApp ((L'.CMap (k, k), loc),
4001 (L'.CAbs ("_", k, (L'.CRecord ((L'.KType, loc), []), loc)), loc)), loc) 4091 (L'.CAbs ("_", k, (L'.CRecord ((L'.KType, loc), []), loc)), loc)), loc)
4002 val ts = (L'.CApp (tf, ts), loc) 4092 val ts = (L'.CApp (tf, ts), loc)
4003 4093
4004 val cv = viewOf () 4094 val cv = viewOf ()
4046 | L.DTask (e1, e2) => 4136 | L.DTask (e1, e2) =>
4047 let 4137 let
4048 val (e1', t1, gs1) = elabExp (env, denv) e1 4138 val (e1', t1, gs1) = elabExp (env, denv) e1
4049 val (e2', t2, gs2) = elabExp (env, denv) e2 4139 val (e2', t2, gs2) = elabExp (env, denv) e2
4050 4140
4051 val targ = cunif (loc, (L'.KType, loc)) 4141 val targ = cunif env (loc, (L'.KType, loc))
4052 4142
4053 val t1' = (L'.CModProj (!basis_r, [], "task_kind"), loc) 4143 val t1' = (L'.CModProj (!basis_r, [], "task_kind"), loc)
4054 val t1' = (L'.CApp (t1', targ), loc) 4144 val t1' = (L'.CApp (t1', targ), loc)
4055 4145
4056 val t2' = (L'.CApp ((L'.CModProj (!basis_r, [], "transaction"), loc), 4146 val t2' = (L'.CApp ((L'.CModProj (!basis_r, [], "transaction"), loc),