Mercurial > urweb

comparison src/elaborate.sml @ 76:522f4bd3955e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Broaden unification context
author Adam Chlipala <adamc@hcoop.net>
date Sun, 29 Jun 2008 10:39:43 -0400
parents 88ffb3d61817
children a6d45c6819c9
comparison
equal deleted inserted replaced
75:88ffb3d61817 76:522f4bd3955e
45 case e of 45 case e of
46 L.Explicit => L'.Explicit 46 L.Explicit => L'.Explicit
47 | L.Implicit => L'.Implicit 47 | L.Implicit => L'.Implicit
48 48
49 fun occursKind r = 49 fun occursKind r =
50 U.Kind.exists (fn L'.KUnif (_, r') => r = r' 50 U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
51 | _ => false) 51 | _ => false)
52 52
53 datatype kunify_error = 53 datatype kunify_error =
54 KOccursCheckFailed of L'.kind * L'.kind 54 KOccursCheckFailed of L'.kind * L'.kind
55 | KIncompatible of L'.kind * L'.kind 55 | KIncompatible of L'.kind * L'.kind
80 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2 80 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2
81 81
82 | (L'.KError, _) => () 82 | (L'.KError, _) => ()
83 | (_, L'.KError) => () 83 | (_, L'.KError) => ()
84 84
85 | (L'.KUnif (_, ref (SOME k1All)), _) => unifyKinds' k1All k2All 85 | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All
86 | (_, L'.KUnif (_, ref (SOME k2All))) => unifyKinds' k1All k2All 86 | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' k1All k2All
87 87
88 | (L'.KUnif (_, r1), L'.KUnif (_, r2)) => 88 | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
89 if r1 = r2 then 89 if r1 = r2 then
90 () 90 ()
91 else 91 else
92 r1 := SOME k2All 92 r1 := SOME k2All
93 93
94 | (L'.KUnif (_, r), _) => 94 | (L'.KUnif (_, _, r), _) =>
95 if occursKind r k2All then 95 if occursKind r k2All then
96 err KOccursCheckFailed 96 err KOccursCheckFailed
97 else 97 else
98 r := SOME k2All 98 r := SOME k2All
99 | (_, L'.KUnif (_, r)) => 99 | (_, L'.KUnif (_, _, r)) =>
100 if occursKind r k1All then 100 if occursKind r k1All then
101 err KOccursCheckFailed 101 err KOccursCheckFailed
102 else 102 else
103 r := SOME k1All 103 r := SOME k1All
104 104
157 val count = ref 0 157 val count = ref 0
158 in 158 in
159 159
160 fun resetKunif () = count := 0 160 fun resetKunif () = count := 0
161 161
162 fun kunif () = 162 fun kunif loc =
163 let 163 let
164 val n = !count 164 val n = !count
165 val s = if n <= 26 then 165 val s = if n <= 26 then
166 str (chr (ord #"A" + n)) 166 str (chr (ord #"A" + n))
167 else 167 else
168 "U" ^ Int.toString (n - 26) 168 "U" ^ Int.toString (n - 26)
169 in 169 in
170 count := n + 1; 170 count := n + 1;
171 (L'.KUnif (s, ref NONE), dummy) 171 (L'.KUnif (loc, s, ref NONE), dummy)
172 end 172 end
173 173
174 end 174 end
175 175
176 local 176 local
177 val count = ref 0 177 val count = ref 0
178 in 178 in
179 179
180 fun resetCunif () = count := 0 180 fun resetCunif () = count := 0
181 181
182 fun cunif k = 182 fun cunif (loc, k) =
183 let 183 let
184 val n = !count 184 val n = !count
185 val s = if n <= 26 then 185 val s = if n <= 26 then
186 str (chr (ord #"A" + n)) 186 str (chr (ord #"A" + n))
187 else 187 else
188 "U" ^ Int.toString (n - 26) 188 "U" ^ Int.toString (n - 26)
189 in 189 in
190 count := n + 1; 190 count := n + 1;
191 (L'.CUnif (k, s, ref NONE), dummy) 191 (L'.CUnif (loc, k, s, ref NONE), dummy)
192 end 192 end
193 193
194 end 194 end
195 195
196 fun elabKind (k, loc) = 196 fun elabKind (k, loc) =
197 case k of 197 case k of
198 L.KType => (L'.KType, loc) 198 L.KType => (L'.KType, loc)
199 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) 199 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
200 | L.KName => (L'.KName, loc) 200 | L.KName => (L'.KName, loc)
201 | L.KRecord k => (L'.KRecord (elabKind k), loc) 201 | L.KRecord k => (L'.KRecord (elabKind k), loc)
202 | L.KWild => kunif () 202 | L.KWild => kunif loc
203 203
204 fun foldKind (dom, ran, loc)= 204 fun foldKind (dom, ran, loc)=
205 (L'.KArrow ((L'.KArrow ((L'.KName, loc), 205 (L'.KArrow ((L'.KArrow ((L'.KName, loc),
206 (L'.KArrow (dom, 206 (L'.KArrow (dom,
207 (L'.KArrow (ran, ran), loc)), loc)), loc), 207 (L'.KArrow (ran, ran), loc)), loc)), loc),
280 280
281 | L.CApp (c1, c2) => 281 | L.CApp (c1, c2) =>
282 let 282 let
283 val (c1', k1) = elabCon env c1 283 val (c1', k1) = elabCon env c1
284 val (c2', k2) = elabCon env c2 284 val (c2', k2) = elabCon env c2
285 val dom = kunif () 285 val dom = kunif loc
286 val ran = kunif () 286 val ran = kunif loc
287 in 287 in
288 checkKind env c1' k1 (L'.KArrow (dom, ran), loc); 288 checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
289 checkKind env c2' k2 dom; 289 checkKind env c2' k2 dom;
290 ((L'.CApp (c1', c2'), loc), ran) 290 ((L'.CApp (c1', c2'), loc), ran)
291 end 291 end
292 | L.CAbs (x, ko, t) => 292 | L.CAbs (x, ko, t) =>
293 let 293 let
294 val k' = case ko of 294 val k' = case ko of
295 NONE => kunif () 295 NONE => kunif loc
296 | SOME k => elabKind k 296 | SOME k => elabKind k
297 val env' = E.pushCRel env x k' 297 val env' = E.pushCRel env x k'
298 val (t', tk) = elabCon env' t 298 val (t', tk) = elabCon env' t
299 in 299 in
300 ((L'.CAbs (x, k', t'), loc), 300 ((L'.CAbs (x, k', t'), loc),
304 | L.CName s => 304 | L.CName s =>
305 ((L'.CName s, loc), kname) 305 ((L'.CName s, loc), kname)
306 306
307 | L.CRecord xcs => 307 | L.CRecord xcs =>
308 let 308 let
309 val k = kunif () 309 val k = kunif loc
310 310
311 val xcs' = map (fn (x, c) => 311 val xcs' = map (fn (x, c) =>
312 let 312 let
313 val (x', xk) = elabCon env x 313 val (x', xk) = elabCon env x
314 val (c', ck) = elabCon env c 314 val (c', ck) = elabCon env c
325 end 325 end
326 | L.CConcat (c1, c2) => 326 | L.CConcat (c1, c2) =>
327 let 327 let
328 val (c1', k1) = elabCon env c1 328 val (c1', k1) = elabCon env c1
329 val (c2', k2) = elabCon env c2 329 val (c2', k2) = elabCon env c2
330 val ku = kunif () 330 val ku = kunif loc
331 val k = (L'.KRecord ku, loc) 331 val k = (L'.KRecord ku, loc)
332 in 332 in
333 checkKind env c1' k1 k; 333 checkKind env c1' k1 k;
334 checkKind env c2' k2 k; 334 checkKind env c2' k2 k;
335 ((L'.CConcat (c1', c2'), loc), k) 335 ((L'.CConcat (c1', c2'), loc), k)
336 end 336 end
337 | L.CFold => 337 | L.CFold =>
338 let 338 let
339 val dom = kunif () 339 val dom = kunif loc
340 val ran = kunif () 340 val ran = kunif loc
341 in 341 in
342 ((L'.CFold (dom, ran), loc), 342 ((L'.CFold (dom, ran), loc),
343 foldKind (dom, ran, loc)) 343 foldKind (dom, ran, loc))
344 end 344 end
345 345
346 | L.CWild k => 346 | L.CWild k =>
347 let 347 let
348 val k' = elabKind k 348 val k' = elabKind k
349 in 349 in
350 (cunif k', k') 350 (cunif (loc, k'), k')
351 end 351 end
352 352
353 fun kunifsRemain k = 353 fun kunifsRemain k =
354 case k of 354 case k of
355 L'.KUnif (_, ref NONE) => true 355 L'.KUnif (_, _, ref NONE) => true
356 | _ => false 356 | _ => false
357 fun cunifsRemain c = 357 fun cunifsRemain c =
358 case c of 358 case c of
359 L'.CUnif (_, _, ref NONE) => true 359 L'.CUnif (loc, _, _, ref NONE) => SOME loc
360 | _ => false 360 | _ => NONE
361 361
362 val kunifsInKind = U.Kind.exists kunifsRemain 362 val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
363 val kunifsInCon = U.Con.exists {kind = kunifsRemain, 363 con = fn _ => false,
364 con = fn _ => false} 364 exp = fn _ => false,
365 val kunifsInExp = U.Exp.exists {kind = kunifsRemain, 365 sgn_item = fn _ => false,
366 con = fn _ => false, 366 sgn = fn _ => false,
367 exp = fn _ => false} 367 str = fn _ => false,
368 368 decl = fn _ => false}
369 val cunifsInCon = U.Con.exists {kind = fn _ => false, 369
370 con = cunifsRemain} 370 val cunifsInDecl = U.Decl.search {kind = fn _ => NONE,
371 val cunifsInExp = U.Exp.exists {kind = fn _ => false, 371 con = cunifsRemain,
372 con = cunifsRemain, 372 exp = fn _ => NONE,
373 exp = fn _ => false} 373 sgn_item = fn _ => NONE,
374 sgn = fn _ => NONE,
375 str = fn _ => NONE,
376 decl = fn _ => NONE}
374 377
375 fun occursCon r = 378 fun occursCon r =
376 U.Con.exists {kind = fn _ => false, 379 U.Con.exists {kind = fn _ => false,
377 con = fn L'.CUnif (_, _, r') => r = r' 380 con = fn L'.CUnif (_, _, _, r') => r = r'
378 | _ => false} 381 | _ => false}
379 382
380 datatype cunify_error = 383 datatype cunify_error =
381 CKind of L'.kind * L'.kind * kunify_error 384 CKind of L'.kind * L'.kind * kunify_error
382 | COccursCheckFailed of L'.con * L'.con 385 | COccursCheckFailed of L'.con * L'.con
459 462
460 exception CUnify of L'.con * L'.con * cunify_error 463 exception CUnify of L'.con * L'.con * cunify_error
461 464
462 fun hnormKind (kAll as (k, _)) = 465 fun hnormKind (kAll as (k, _)) =
463 case k of 466 case k of
464 L'.KUnif (_, ref (SOME k)) => hnormKind k 467 L'.KUnif (_, _, ref (SOME k)) => hnormKind k
465 | _ => kAll 468 | _ => kAll
466 469
467 fun kindof env (c, loc) = 470 fun kindof env (c, loc) =
468 case c of 471 case c of
469 L'.TFun _ => ktype 472 L'.TFun _ => ktype
498 | L'.CRecord (k, _) => (L'.KRecord k, loc) 501 | L'.CRecord (k, _) => (L'.KRecord k, loc)
499 | L'.CConcat (c, _) => kindof env c 502 | L'.CConcat (c, _) => kindof env c
500 | L'.CFold (dom, ran) => foldKind (dom, ran, loc) 503 | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
501 504
502 | L'.CError => kerror 505 | L'.CError => kerror
503 | L'.CUnif (k, _, _) => k 506 | L'.CUnif (_, k, _, _) => k
504 507
505 fun unifyRecordCons env (c1, c2) = 508 fun unifyRecordCons env (c1, c2) =
506 let 509 let
507 val k1 = kindof env c1 510 val k1 = kindof env c1
508 val k2 = kindof env c2 511 val k2 = kindof env c2
521 in 524 in
522 {fields = #fields s1 @ #fields s2, 525 {fields = #fields s1 @ #fields s2,
523 unifs = #unifs s1 @ #unifs s2, 526 unifs = #unifs s1 @ #unifs s2,
524 others = #others s1 @ #others s2} 527 others = #others s1 @ #others s2}
525 end 528 end
526 | (L'.CUnif (_, _, ref (SOME c)), _) => recordSummary env c 529 | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary env c
527 | c' as (L'.CUnif (_, _, r), _) => {fields = [], unifs = [(c', r)], others = []} 530 | c' as (L'.CUnif (_, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
528 | c' => {fields = [], unifs = [], others = [c']} 531 | c' => {fields = [], unifs = [], others = [c']}
529 532
530 and consEq env (c1, c2) = 533 and consEq env (c1, c2) =
531 (unifyCons env c1 c2; 534 (unifyCons env c1 c2;
532 true) 535 true)
575 ([], [], _) => ([], [], unifs) 578 ([], [], _) => ([], [], unifs)
576 | (_, _, []) => (fs, others, []) 579 | (_, _, []) => (fs, others, [])
577 | (_, _, (_, r) :: rest) => 580 | (_, _, (_, r) :: rest) =>
578 let 581 let
579 val r' = ref NONE 582 val r' = ref NONE
580 val cr' = (L'.CUnif (k, "recd", r'), dummy) 583 val cr' = (L'.CUnif (dummy, k, "recd", r'), dummy)
581 584
582 val prefix = case (fs, others) of 585 val prefix = case (fs, others) of
583 ([], other :: others) => 586 ([], other :: others) =>
584 List.foldl (fn (other, c) => 587 List.foldl (fn (other, c) =>
585 (L'.CConcat (c, other), dummy)) 588 (L'.CConcat (c, other), dummy))
624 pairOffUnifs (unifs1, unifs2) 627 pairOffUnifs (unifs1, unifs2)
625 end 628 end
626 629
627 and hnormCon env (cAll as (c, loc)) = 630 and hnormCon env (cAll as (c, loc)) =
628 case c of 631 case c of
629 L'.CUnif (_, _, ref (SOME c)) => hnormCon env c 632 L'.CUnif (_, _, _, ref (SOME c)) => hnormCon env c
630 633
631 | L'.CNamed xn => 634 | L'.CNamed xn =>
632 (case E.lookupCNamed env xn of 635 (case E.lookupCNamed env xn of
633 (_, _, SOME c') => hnormCon env c' 636 (_, _, SOME c') => hnormCon env c'
634 | _ => cAll) 637 | _ => cAll)
756 err CIncompatible 759 err CIncompatible
757 760
758 | (L'.CError, _) => () 761 | (L'.CError, _) => ()
759 | (_, L'.CError) => () 762 | (_, L'.CError) => ()
760 763
761 | (L'.CUnif (_, _, ref (SOME c1All)), _) => unifyCons' env c1All c2All 764 | (L'.CUnif (_, _, _, ref (SOME c1All)), _) => unifyCons' env c1All c2All
762 | (_, L'.CUnif (_, _, ref (SOME c2All))) => unifyCons' env c1All c2All 765 | (_, L'.CUnif (_, _, _, ref (SOME c2All))) => unifyCons' env c1All c2All
763 766
764 | (L'.CUnif (k1, _, r1), L'.CUnif (k2, _, r2)) => 767 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
765 if r1 = r2 then 768 if r1 = r2 then
766 () 769 ()
767 else 770 else
768 (unifyKinds k1 k2; 771 (unifyKinds k1 k2;
769 r1 := SOME c2All) 772 r1 := SOME c2All)
770 773
771 | (L'.CUnif (_, _, r), _) => 774 | (L'.CUnif (_, _, _, r), _) =>
772 if occursCon r c2All then 775 if occursCon r c2All then
773 err COccursCheckFailed 776 err COccursCheckFailed
774 else 777 else
775 r := SOME c2All 778 r := SOME c2All
776 | (_, L'.CUnif (_, _, r)) => 779 | (_, L'.CUnif (_, _, _, r)) =>
777 if occursCon r c1All then 780 if occursCon r c1All then
778 err COccursCheckFailed 781 err COccursCheckFailed
779 else 782 else
780 r := SOME c1All 783 r := SOME c1All
781 784
896 let 899 let
897 fun unravel (t, e) = 900 fun unravel (t, e) =
898 case hnormCon env t of 901 case hnormCon env t of
899 (L'.TCFun (L'.Implicit, x, k, t'), _) => 902 (L'.TCFun (L'.Implicit, x, k, t'), _) =>
900 let 903 let
901 val u = cunif k 904 val u = cunif (loc, k)
902 in 905 in
903 unravel (subConInCon (0, u) t', 906 unravel (subConInCon (0, u) t',
904 (L'.ECApp (e, u), loc)) 907 (L'.ECApp (e, u), loc))
905 end 908 end
906 | _ => (e, t) 909 | _ => (e, t)
952 let 955 let
953 val (e1', t1) = elabExp env e1 956 val (e1', t1) = elabExp env e1
954 val (e1', t1) = elabHead env e1' t1 957 val (e1', t1) = elabHead env e1' t1
955 val (e2', t2) = elabExp env e2 958 val (e2', t2) = elabExp env e2
956 959
957 val dom = cunif ktype 960 val dom = cunif (loc, ktype)
958 val ran = cunif ktype 961 val ran = cunif (loc, ktype)
959 val t = (L'.TFun (dom, ran), dummy) 962 val t = (L'.TFun (dom, ran), dummy)
960 in 963 in
961 checkCon env e1' t1 t; 964 checkCon env e1' t1 t;
962 checkCon env e2' t2 dom; 965 checkCon env e2' t2 dom;
963 ((L'.EApp (e1', e2'), loc), ran) 966 ((L'.EApp (e1', e2'), loc), ran)
964 end 967 end
965 | L.EAbs (x, to, e) => 968 | L.EAbs (x, to, e) =>
966 let 969 let
967 val t' = case to of 970 val t' = case to of
968 NONE => cunif ktype 971 NONE => cunif (loc, ktype)
969 | SOME t => 972 | SOME t =>
970 let 973 let
971 val (t', tk) = elabCon env t 974 val (t', tk) = elabCon env t
972 in 975 in
973 checkKind env t' tk ktype; 976 checkKind env t' tk ktype;
1032 | L.EField (e, c) => 1035 | L.EField (e, c) =>
1033 let 1036 let
1034 val (e', et) = elabExp env e 1037 val (e', et) = elabExp env e
1035 val (c', ck) = elabCon env c 1038 val (c', ck) = elabCon env c
1036 1039
1037 val ft = cunif ktype 1040 val ft = cunif (loc, ktype)
1038 val rest = cunif ktype_record 1041 val rest = cunif (loc, ktype_record)
1039 in 1042 in
1040 checkKind env c' ck kname; 1043 checkKind env c' ck kname;
1041 checkCon env e' et (L'.TRecord (L'.CConcat ((L'.CRecord (ktype, [(c', ft)]), loc), rest), loc), loc); 1044 checkCon env e' et (L'.TRecord (L'.CConcat ((L'.CRecord (ktype, [(c', ft)]), loc), rest), loc), loc);
1042 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft) 1045 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft)
1043 end 1046 end
1044 1047
1045 | L.EFold => 1048 | L.EFold =>
1046 let 1049 let
1047 val dom = kunif () 1050 val dom = kunif loc
1048 in 1051 in
1049 ((L'.EFold dom, loc), foldType (dom, loc)) 1052 ((L'.EFold dom, loc), foldType (dom, loc))
1050 end 1053 end
1051 1054
1052 1055
1053 datatype decl_error = 1056 datatype decl_error =
1054 KunifsRemainKind of ErrorMsg.span * L'.kind 1057 KunifsRemain of ErrorMsg.span
1055 | KunifsRemainCon of ErrorMsg.span * L'.con 1058 | CunifsRemain of ErrorMsg.span
1056 | KunifsRemainExp of ErrorMsg.span * L'.exp
1057 | CunifsRemainCon of ErrorMsg.span * L'.con
1058 | CunifsRemainExp of ErrorMsg.span * L'.exp
1059 1059
1060 fun declError env err = 1060 fun declError env err =
1061 case err of 1061 case err of
1062 KunifsRemainKind (loc, k) => 1062 KunifsRemain loc =>
1063 (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in kind"; 1063 ErrorMsg.errorAt loc "Some kind unification variables are undetermined in declaration"
1064 eprefaces' [("Kind", p_kind k)]) 1064 | CunifsRemain loc =>
1065 | KunifsRemainCon (loc, c) => 1065 ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in declaration"
1066 (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in constructor";
1067 eprefaces' [("Constructor", p_con env c)])
1068 | KunifsRemainExp (loc, e) =>
1069 (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in expression";
1070 eprefaces' [("Expression", p_exp env e)])
1071 | CunifsRemainCon (loc, c) =>
1072 (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in constructor";
1073 eprefaces' [("Constructor", p_con env c)])
1074 | CunifsRemainExp (loc, e) =>
1075 (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in expression";
1076 eprefaces' [("Expression", p_exp env e)])
1077 1066
1078 datatype sgn_error = 1067 datatype sgn_error =
1079 UnboundSgn of ErrorMsg.span * string 1068 UnboundSgn of ErrorMsg.span * string
1080 | UnmatchedSgi of L'.sgn_item 1069 | UnmatchedSgi of L'.sgn_item
1081 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error 1070 | SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
1162 kunifyError ue) 1151 kunifyError ue)
1163 1152
1164 val hnormSgn = E.hnormSgn 1153 val hnormSgn = E.hnormSgn
1165 1154
1166 fun elabSgn_item ((sgi, loc), env) = 1155 fun elabSgn_item ((sgi, loc), env) =
1167 let 1156 case sgi of
1168 1157 L.SgiConAbs (x, k) =>
1169 in 1158 let
1170 resetKunif (); 1159 val k' = elabKind k
1171 resetCunif (); 1160
1172 case sgi of 1161 val (env', n) = E.pushCNamed env x k' NONE
1173 L.SgiConAbs (x, k) => 1162 in
1174 let 1163 ([(L'.SgiConAbs (x, n, k'), loc)], env')
1175 val k' = elabKind k 1164 end
1176 1165
1177 val (env', n) = E.pushCNamed env x k' NONE 1166 | L.SgiCon (x, ko, c) =>
1178 in 1167 let
1179 if ErrorMsg.anyErrors () then 1168 val k' = case ko of
1180 () 1169 NONE => kunif loc
1181 else ( 1170 | SOME k => elabKind k
1182 if kunifsInKind k' then 1171
1183 declError env (KunifsRemainKind (loc, k')) 1172 val (c', ck) = elabCon env c
1184 else 1173 val (env', n) = E.pushCNamed env x k' (SOME c')
1185 () 1174 in
1186 ); 1175 checkKind env c' ck k';
1187 1176
1188 ([(L'.SgiConAbs (x, n, k'), loc)], env') 1177 ([(L'.SgiCon (x, n, k', c'), loc)], env')
1189 end 1178 end
1190 1179
1191 | L.SgiCon (x, ko, c) => 1180 | L.SgiVal (x, c) =>
1192 let 1181 let
1193 val k' = case ko of 1182 val (c', ck) = elabCon env c
1194 NONE => kunif () 1183
1195 | SOME k => elabKind k 1184 val (env', n) = E.pushENamed env x c'
1196 1185 in
1197 val (c', ck) = elabCon env c 1186 (unifyKinds ck ktype
1198 val (env', n) = E.pushCNamed env x k' (SOME c') 1187 handle KUnify ue => strError env (NotType (ck, ue)));
1199 in 1188
1200 checkKind env c' ck k'; 1189 ([(L'.SgiVal (x, n, c'), loc)], env')
1201 1190 end
1202 if ErrorMsg.anyErrors () then 1191
1203 () 1192 | L.SgiStr (x, sgn) =>
1204 else ( 1193 let
1205 if kunifsInKind k' then 1194 val sgn' = elabSgn env sgn
1206 declError env (KunifsRemainKind (loc, k')) 1195 val (env', n) = E.pushStrNamed env x sgn'
1207 else 1196 in
1208 (); 1197 ([(L'.SgiStr (x, n, sgn'), loc)], env')
1209 1198 end
1210 if kunifsInCon c' then 1199
1211 declError env (KunifsRemainCon (loc, c')) 1200 | L.SgiSgn (x, sgn) =>
1212 else 1201 let
1213 () 1202 val sgn' = elabSgn env sgn
1214 ); 1203 val (env', n) = E.pushSgnNamed env x sgn'
1215 1204 in
1216 ([(L'.SgiCon (x, n, k', c'), loc)], env') 1205 ([(L'.SgiSgn (x, n, sgn'), loc)], env')
1217 end 1206 end
1218 1207
1219 | L.SgiVal (x, c) => 1208 | L.SgiInclude sgn =>
1220 let 1209 let
1221 val (c', ck) = elabCon env c 1210 val sgn' = elabSgn env sgn
1222 1211 in
1223 val (env', n) = E.pushENamed env x c' 1212 case #1 (hnormSgn env sgn') of
1224 in 1213 L'.SgnConst sgis =>
1225 (unifyKinds ck ktype 1214 (sgis, foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis)
1226 handle KUnify ue => strError env (NotType (ck, ue))); 1215 | _ => (sgnError env (NotIncludable sgn');
1227 1216 ([], env))
1228 if ErrorMsg.anyErrors () then 1217 end
1229 ()
1230 else (
1231 if kunifsInCon c' then
1232 declError env (KunifsRemainCon (loc, c'))
1233 else
1234 ()
1235 );
1236
1237 ([(L'.SgiVal (x, n, c'), loc)], env')
1238 end
1239
1240 | L.SgiStr (x, sgn) =>
1241 let
1242 val sgn' = elabSgn env sgn
1243 val (env', n) = E.pushStrNamed env x sgn'
1244 in
1245 ([(L'.SgiStr (x, n, sgn'), loc)], env')
1246 end
1247
1248 | L.SgiSgn (x, sgn) =>
1249 let
1250 val sgn' = elabSgn env sgn
1251 val (env', n) = E.pushSgnNamed env x sgn'
1252 in
1253 ([(L'.SgiSgn (x, n, sgn'), loc)], env')
1254 end
1255
1256 | L.SgiInclude sgn =>
1257 let
1258 val sgn' = elabSgn env sgn
1259 in
1260 case #1 (hnormSgn env sgn') of
1261 L'.SgnConst sgis =>
1262 (sgis, foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis)
1263 | _ => (sgnError env (NotIncludable sgn');
1264 ([], env))
1265 end
1266
1267 end
1268 1218
1269 and elabSgn env (sgn, loc) = 1219 and elabSgn env (sgn, loc) =
1270 case sgn of 1220 case sgn of
1271 L.SgnConst sgis => 1221 L.SgnConst sgis =>
1272 let 1222 let
1578 1528
1579 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)) 1529 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
1580 1530
1581 1531
1582 fun elabDecl ((d, loc), env) = 1532 fun elabDecl ((d, loc), env) =
1583 let 1533 case d of
1584 1534 L.DCon (x, ko, c) =>
1585 in 1535 let
1586 resetKunif (); 1536 val k' = case ko of
1587 resetCunif (); 1537 NONE => kunif loc
1588 case d of 1538 | SOME k => elabKind k
1589 L.DCon (x, ko, c) => 1539
1540 val (c', ck) = elabCon env c
1541 val (env', n) = E.pushCNamed env x k' (SOME c')
1542 in
1543 checkKind env c' ck k';
1544
1545 ([(L'.DCon (x, n, k', c'), loc)], env')
1546 end
1547 | L.DVal (x, co, e) =>
1548 let
1549 val (c', ck) = case co of
1550 NONE => (cunif (loc, ktype), ktype)
1551 | SOME c => elabCon env c
1552
1553 val (e', et) = elabExp env e
1554 val (env', n) = E.pushENamed env x c'
1555 in
1556 checkCon env e' et c';
1557
1558 ([(L'.DVal (x, n, c', e'), loc)], env')
1559 end
1560
1561 | L.DSgn (x, sgn) =>
1562 let
1563 val sgn' = elabSgn env sgn
1564 val (env', n) = E.pushSgnNamed env x sgn'
1565 in
1566 ([(L'.DSgn (x, n, sgn'), loc)], env')
1567 end
1568
1569 | L.DStr (x, sgno, str) =>
1570 let
1571 val formal = Option.map (elabSgn env) sgno
1572 val (str', actual) = elabStr env str
1573
1574 val sgn' = case formal of
1575 NONE => selfifyAt env {str = str', sgn = actual}
1576 | SOME formal =>
1577 (subSgn env actual formal;
1578 formal)
1579
1580 val (env', n) = E.pushStrNamed env x sgn'
1581 in
1582 case #1 (hnormSgn env sgn') of
1583 L'.SgnFun _ =>
1584 (case #1 str' of
1585 L'.StrFun _ => ()
1586 | _ => strError env (FunctorRebind loc))
1587 | _ => ();
1588
1589 ([(L'.DStr (x, n, sgn', str'), loc)], env')
1590 end
1591
1592 | L.DFfiStr (x, sgn) =>
1593 let
1594 val sgn' = elabSgn env sgn
1595
1596 val (env', n) = E.pushStrNamed env x sgn'
1597 in
1598 ([(L'.DFfiStr (x, n, sgn'), loc)], env')
1599 end
1600
1601 | L.DOpen (m, ms) =>
1602 case E.lookupStr env m of
1603 NONE => (strError env (UnboundStr (loc, m));
1604 ([], env))
1605 | SOME (n, sgn) =>
1590 let 1606 let
1591 val k' = case ko of 1607 val (_, sgn) = foldl (fn (m, (str, sgn)) =>
1592 NONE => kunif () 1608 case E.projectStr env {str = str, sgn = sgn, field = m} of
1593 | SOME k => elabKind k 1609 NONE => (strError env (UnboundStr (loc, m));
1594 1610 (strerror, sgnerror))
1595 val (c', ck) = elabCon env c 1611 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1596 val (env', n) = E.pushCNamed env x k' (SOME c') 1612 ((L'.StrVar n, loc), sgn) ms
1597 in 1613 in
1598 checkKind env c' ck k'; 1614 dopen env {str = n, strs = ms, sgn = sgn}
1599
1600 if ErrorMsg.anyErrors () then
1601 ()
1602 else (
1603 if kunifsInKind k' then
1604 declError env (KunifsRemainKind (loc, k'))
1605 else
1606 ();
1607
1608 if kunifsInCon c' then
1609 declError env (KunifsRemainCon (loc, c'))
1610 else
1611 ()
1612 );
1613
1614 ([(L'.DCon (x, n, k', c'), loc)], env')
1615 end 1615 end
1616 | L.DVal (x, co, e) =>
1617 let
1618 val (c', ck) = case co of
1619 NONE => (cunif ktype, ktype)
1620 | SOME c => elabCon env c
1621
1622 val (e', et) = elabExp env e
1623 val (env', n) = E.pushENamed env x c'
1624 in
1625 checkCon env e' et c';
1626
1627 if ErrorMsg.anyErrors () then
1628 ()
1629 else (
1630 if kunifsInCon c' then
1631 declError env (KunifsRemainCon (loc, c'))
1632 else
1633 ();
1634
1635 if cunifsInCon c' then
1636 declError env (CunifsRemainCon (loc, c'))
1637 else
1638 ();
1639
1640 if kunifsInExp e' then
1641 declError env (KunifsRemainExp (loc, e'))
1642 else
1643 ();
1644
1645 if cunifsInExp e' then
1646 declError env (CunifsRemainExp (loc, e'))
1647 else
1648 ());
1649
1650 ([(L'.DVal (x, n, c', e'), loc)], env')
1651 end
1652
1653 | L.DSgn (x, sgn) =>
1654 let
1655 val sgn' = elabSgn env sgn
1656 val (env', n) = E.pushSgnNamed env x sgn'
1657 in
1658 ([(L'.DSgn (x, n, sgn'), loc)], env')
1659 end
1660
1661 | L.DStr (x, sgno, str) =>
1662 let
1663 val formal = Option.map (elabSgn env) sgno
1664 val (str', actual) = elabStr env str
1665
1666 val sgn' = case formal of
1667 NONE => selfifyAt env {str = str', sgn = actual}
1668 | SOME formal =>
1669 (subSgn env actual formal;
1670 formal)
1671
1672 val (env', n) = E.pushStrNamed env x sgn'
1673 in
1674 case #1 (hnormSgn env sgn') of
1675 L'.SgnFun _ =>
1676 (case #1 str' of
1677 L'.StrFun _ => ()
1678 | _ => strError env (FunctorRebind loc))
1679 | _ => ();
1680
1681 ([(L'.DStr (x, n, sgn', str'), loc)], env')
1682 end
1683
1684 | L.DFfiStr (x, sgn) =>
1685 let
1686 val sgn' = elabSgn env sgn
1687
1688 val (env', n) = E.pushStrNamed env x sgn'
1689 in
1690 ([(L'.DFfiStr (x, n, sgn'), loc)], env')
1691 end
1692
1693 | L.DOpen (m, ms) =>
1694 (case E.lookupStr env m of
1695 NONE => (strError env (UnboundStr (loc, m));
1696 ([], env))
1697 | SOME (n, sgn) =>
1698 let
1699 val (_, sgn) = foldl (fn (m, (str, sgn)) =>
1700 case E.projectStr env {str = str, sgn = sgn, field = m} of
1701 NONE => (strError env (UnboundStr (loc, m));
1702 (strerror, sgnerror))
1703 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1704 ((L'.StrVar n, loc), sgn) ms
1705 in
1706 dopen env {str = n, strs = ms, sgn = sgn}
1707 end)
1708 end
1709 1616
1710 and elabStr env (str, loc) = 1617 and elabStr env (str, loc) =
1711 case str of 1618 case str of
1712 L.StrConst ds => 1619 L.StrConst ds =>
1713 let 1620 let
1842 1749
1843 val () = discoverC int "int" 1750 val () = discoverC int "int"
1844 val () = discoverC float "float" 1751 val () = discoverC float "float"
1845 val () = discoverC string "string" 1752 val () = discoverC string "string"
1846 1753
1847 val (file, _) = ListUtil.foldlMapConcat elabDecl env' file 1754 fun elabDecl' (d, env) =
1755 let
1756 val () = resetKunif ()
1757 val () = resetCunif ()
1758 val (ds, env) = elabDecl (d, env)
1759 in
1760 if ErrorMsg.anyErrors () then
1761 ()
1762 else (
1763 if List.exists kunifsInDecl ds then
1764 declError env (KunifsRemain (#2 d))
1765 else
1766 ();
1767
1768 case ListUtil.search cunifsInDecl ds of
1769 NONE => ()
1770 | SOME loc =>
1771 declError env (CunifsRemain loc)
1772 );
1773
1774 (ds, env)
1775 end
1776
1777 val (file, _) = ListUtil.foldlMapConcat elabDecl' env' file
1848 in 1778 in
1849 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file 1779 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
1850 end 1780 end
1851 1781
1852 end 1782 end