Mercurial > urweb

comparison src/elaborate.sml @ 623:588b9d16b00a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:10:25 -0500
parents d64533157f40
children 12b73f3c108e
comparison
equal deleted inserted replaced
622:d64533157f40 623:588b9d16b00a
59 U.Kind.exists (fn L'.KUnif (_, _, r') => r = r' 59 U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
60 | _ => false) 60 | _ => false)
61 61
62 exception KUnify' of kunify_error 62 exception KUnify' of kunify_error
63 63
64 fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) = 64 fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) =
65 let 65 let
66 fun err f = raise KUnify' (f (k1All, k2All)) 66 fun err f = raise KUnify' (f (k1All, k2All))
67 in 67 in
68 case (k1, k2) of 68 case (k1, k2) of
69 (L'.KType, L'.KType) => () 69 (L'.KType, L'.KType) => ()
70 | (L'.KUnit, L'.KUnit) => () 70 | (L'.KUnit, L'.KUnit) => ()
71 71
72 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) => 72 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
73 (unifyKinds' d1 d2; 73 (unifyKinds' env d1 d2;
74 unifyKinds' r1 r2) 74 unifyKinds' env r1 r2)
75 | (L'.KName, L'.KName) => () 75 | (L'.KName, L'.KName) => ()
76 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2 76 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' env k1 k2
77 | (L'.KTuple ks1, L'.KTuple ks2) => 77 | (L'.KTuple ks1, L'.KTuple ks2) =>
78 ((ListPair.appEq (fn (k1, k2) => unifyKinds' k1 k2) (ks1, ks2)) 78 ((ListPair.appEq (fn (k1, k2) => unifyKinds' env k1 k2) (ks1, ks2))
79 handle ListPair.UnequalLengths => err KIncompatible) 79 handle ListPair.UnequalLengths => err KIncompatible)
80
81 | (L'.KRel n1, L'.KRel n2) =>
82 if n1 = n2 then
83 ()
84 else
85 err KIncompatible
86 | (L'.KFun (x, k1), L'.KFun (_, k2)) =>
87 unifyKinds' (E.pushKRel env x) k1 k2
80 88
81 | (L'.KError, _) => () 89 | (L'.KError, _) => ()
82 | (_, L'.KError) => () 90 | (_, L'.KError) => ()
83 91
84 | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All 92 | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' env k1All k2All
85 | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' k1All k2All 93 | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' env k1All k2All
86 94
87 | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) => 95 | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
88 if r1 = r2 then 96 if r1 = r2 then
89 () 97 ()
90 else 98 else
104 | _ => err KIncompatible 112 | _ => err KIncompatible
105 end 113 end
106 114
107 exception KUnify of L'.kind * L'.kind * kunify_error 115 exception KUnify of L'.kind * L'.kind * kunify_error
108 116
109 fun unifyKinds k1 k2 = 117 fun unifyKinds env k1 k2 =
110 unifyKinds' k1 k2 118 unifyKinds' env k1 k2
111 handle KUnify' err => raise KUnify (k1, k2, err) 119 handle KUnify' err => raise KUnify (k1, k2, err)
112 120
113 fun checkKind env c k1 k2 = 121 fun checkKind env c k1 k2 =
114 unifyKinds k1 k2 122 unifyKinds env k1 k2
115 handle KUnify (k1, k2, err) => 123 handle KUnify (k1, k2, err) =>
116 conError env (WrongKind (c, k1, k2, err)) 124 conError env (WrongKind (c, k1, k2, err))
117 125
118 val dummy = ErrorMsg.dummySpan 126 val dummy = ErrorMsg.dummySpan
119 127
170 (L'.CUnif (loc, k, s, ref NONE), dummy) 178 (L'.CUnif (loc, k, s, ref NONE), dummy)
171 end 179 end
172 180
173 end 181 end
174 182
175 fun elabKind (k, loc) = 183 fun elabKind env (k, loc) =
176 case k of 184 case k of
177 L.KType => (L'.KType, loc) 185 L.KType => (L'.KType, loc)
178 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) 186 | L.KArrow (k1, k2) => (L'.KArrow (elabKind env k1, elabKind env k2), loc)
179 | L.KName => (L'.KName, loc) 187 | L.KName => (L'.KName, loc)
180 | L.KRecord k => (L'.KRecord (elabKind k), loc) 188 | L.KRecord k => (L'.KRecord (elabKind env k), loc)
181 | L.KUnit => (L'.KUnit, loc) 189 | L.KUnit => (L'.KUnit, loc)
182 | L.KTuple ks => (L'.KTuple (map elabKind ks), loc) 190 | L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc)
183 | L.KWild => kunif loc 191 | L.KWild => kunif loc
192
193 | L.KVar s => (case E.lookupK env s of
194 NONE =>
195 (kindError env (UnboundKind (loc, s));
196 kerror)
197 | SOME n => (L'.KRel n, loc))
198 | L.KFun (x, k) => (L'.KFun (x, elabKind (E.pushKRel env x) k), loc)
184 199
185 fun mapKind (dom, ran, loc)= 200 fun mapKind (dom, ran, loc)=
186 (L'.KArrow ((L'.KArrow (dom, ran), loc), 201 (L'.KArrow ((L'.KArrow (dom, ran), loc),
187 (L'.KArrow ((L'.KRecord dom, loc), 202 (L'.KArrow ((L'.KRecord dom, loc),
188 (L'.KRecord ran, loc)), loc)), loc) 203 (L'.KRecord ran, loc)), loc)), loc)
190 fun hnormKind (kAll as (k, _)) = 205 fun hnormKind (kAll as (k, _)) =
191 case k of 206 case k of
192 L'.KUnif (_, _, ref (SOME k)) => hnormKind k 207 L'.KUnif (_, _, ref (SOME k)) => hnormKind k
193 | _ => kAll 208 | _ => kAll
194 209
210 open ElabOps
211 val hnormCon = D.hnormCon
212
213 fun elabConHead (c as (_, loc)) k =
214 let
215 fun unravel (k, c) =
216 case hnormKind k of
217 (L'.KFun (x, k'), _) =>
218 let
219 val u = kunif loc
220
221 val k'' = subKindInKind (0, u) k'
222 in
223 unravel (k'', (L'.CKApp (c, u), loc))
224 end
225 | _ => (c, k)
226 in
227 unravel (k, c)
228 end
229
195 fun elabCon (env, denv) (c, loc) = 230 fun elabCon (env, denv) (c, loc) =
196 case c of 231 case c of
197 L.CAnnot (c, k) => 232 L.CAnnot (c, k) =>
198 let 233 let
199 val k' = elabKind k 234 val k' = elabKind env k
200 val (c', ck, gs) = elabCon (env, denv) c 235 val (c', ck, gs) = elabCon (env, denv) c
201 in 236 in
202 checkKind env c' ck k'; 237 checkKind env c' ck k';
203 (c', k', gs) 238 (c', k', gs)
204 end 239 end
213 ((L'.TFun (t1', t2'), loc), ktype, gs1 @ gs2) 248 ((L'.TFun (t1', t2'), loc), ktype, gs1 @ gs2)
214 end 249 end
215 | L.TCFun (e, x, k, t) => 250 | L.TCFun (e, x, k, t) =>
216 let 251 let
217 val e' = elabExplicitness e 252 val e' = elabExplicitness e
218 val k' = elabKind k 253 val k' = elabKind env k
219 val env' = E.pushCRel env x k' 254 val env' = E.pushCRel env x k'
220 val (t', tk, gs) = elabCon (env', D.enter denv) t 255 val (t', tk, gs) = elabCon (env', D.enter denv) t
221 in 256 in
222 checkKind env t' tk ktype; 257 checkKind env t' tk ktype;
223 ((L'.TCFun (e', x, k', t'), loc), ktype, gs) 258 ((L'.TCFun (e', x, k', t'), loc), ktype, gs)
259 end
260 | L.TKFun (x, t) =>
261 let
262 val env' = E.pushKRel env x
263 val (t', tk, gs) = elabCon (env', denv) t
264 in
265 checkKind env t' tk ktype;
266 ((L'.TKFun (x, t'), loc), ktype, gs)
224 end 267 end
225 | L.CDisjoint (c1, c2, c) => 268 | L.CDisjoint (c1, c2, c) =>
226 let 269 let
227 val (c1', k1, gs1) = elabCon (env, denv) c1 270 val (c1', k1, gs1) = elabCon (env, denv) c1
228 val (c2', k2, gs2) = elabCon (env, denv) c2 271 val (c2', k2, gs2) = elabCon (env, denv) c2
251 (case E.lookupC env s of 294 (case E.lookupC env s of
252 E.NotBound => 295 E.NotBound =>
253 (conError env (UnboundCon (loc, s)); 296 (conError env (UnboundCon (loc, s));
254 (cerror, kerror, [])) 297 (cerror, kerror, []))
255 | E.Rel (n, k) => 298 | E.Rel (n, k) =>
256 ((L'.CRel n, loc), k, []) 299 let
300 val (c, k) = elabConHead (L'.CRel n, loc) k
301 in
302 (c, k, [])
303 end
257 | E.Named (n, k) => 304 | E.Named (n, k) =>
258 ((L'.CNamed n, loc), k, [])) 305 let
306 val (c, k) = elabConHead (L'.CNamed n, loc) k
307 in
308 (c, k, [])
309 end)
259 | L.CVar (m1 :: ms, s) => 310 | L.CVar (m1 :: ms, s) =>
260 (case E.lookupStr env m1 of 311 (case E.lookupStr env m1 of
261 NONE => (conError env (UnboundStrInCon (loc, m1)); 312 NONE => (conError env (UnboundStrInCon (loc, m1));
262 (cerror, kerror, [])) 313 (cerror, kerror, []))
263 | SOME (n, sgn) => 314 | SOME (n, sgn) =>
290 end 341 end
291 | L.CAbs (x, ko, t) => 342 | L.CAbs (x, ko, t) =>
292 let 343 let
293 val k' = case ko of 344 val k' = case ko of
294 NONE => kunif loc 345 NONE => kunif loc
295 | SOME k => elabKind k 346 | SOME k => elabKind env k
296 val env' = E.pushCRel env x k' 347 val env' = E.pushCRel env x k'
297 val (t', tk, gs) = elabCon (env', D.enter denv) t 348 val (t', tk, gs) = elabCon (env', D.enter denv) t
298 in 349 in
299 ((L'.CAbs (x, k', t'), loc), 350 ((L'.CAbs (x, k', t'), loc),
300 (L'.KArrow (k', tk), loc), 351 (L'.KArrow (k', tk), loc),
352 gs)
353 end
354 | L.CKAbs (x, t) =>
355 let
356 val env' = E.pushKRel env x
357 val (t', tk, gs) = elabCon (env', denv) t
358 in
359 ((L'.CKAbs (x, t'), loc),
360 (L'.KFun (x, tk), loc),
301 gs) 361 gs)
302 end 362 end
303 363
304 | L.CName s => 364 | L.CName s =>
305 ((L'.CName s, loc), kname, []) 365 ((L'.CName s, loc), kname, [])
390 (cerror, kerror, [])) 450 (cerror, kerror, []))
391 end 451 end
392 452
393 | L.CWild k => 453 | L.CWild k =>
394 let 454 let
395 val k' = elabKind k 455 val k' = elabKind env k
396 in 456 in
397 (cunif (loc, k'), k', []) 457 (cunif (loc, k'), k', [])
398 end 458 end
399 459
400 fun kunifsRemain k = 460 fun kunifsRemain k =
428 | _ => false} 488 | _ => false}
429 489
430 exception CUnify' of cunify_error 490 exception CUnify' of cunify_error
431 491
432 exception SynUnif = E.SynUnif 492 exception SynUnif = E.SynUnif
433
434 open ElabOps
435 493
436 type record_summary = { 494 type record_summary = {
437 fields : (L'.con * L'.con) list, 495 fields : (L'.con * L'.con) list,
438 unifs : (L'.con * L'.con option ref) list, 496 unifs : (L'.con * L'.con option ref) list,
439 others : L'.con list 497 others : L'.con list
497 | k => raise CUnify' (CKindof (k, c, "tuple"))) 555 | k => raise CUnify' (CKindof (k, c, "tuple")))
498 556
499 | L'.CError => kerror 557 | L'.CError => kerror
500 | L'.CUnif (_, k, _, _) => k 558 | L'.CUnif (_, k, _, _) => k
501 559
502 val hnormCon = D.hnormCon 560 | L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc)
561 | L'.CKApp (c, k) =>
562 (case hnormKind (kindof env c) of
563 (L'.KFun (_, k'), _) => subKindInKind (0, k) k'
564 | k => raise CUnify' (CKindof (k, c, "kapp")))
565 | L'.TKFun _ => ktype
503 566
504 fun deConstraintCon (env, denv) c = 567 fun deConstraintCon (env, denv) c =
505 let 568 let
506 val (c, gs) = hnormCon (env, denv) c 569 val (c, gs) = hnormCon (env, denv) c
507 in 570 in
562 | k => raise CUnify' (CKindof (k, c, "tuple")))*) 625 | k => raise CUnify' (CKindof (k, c, "tuple")))*)
563 626
564 | L'.CError => false 627 | L'.CError => false
565 | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit 628 | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit
566 629
630 | L'.CKAbs _ => false
631 | L'.CKApp _ => false
632 | L'.TKFun _ => false
633
567 fun unifyRecordCons (env, denv) (c1, c2) = 634 fun unifyRecordCons (env, denv) (c1, c2) =
568 let 635 let
569 fun rkindof c = 636 fun rkindof c =
570 case hnormKind (kindof env c) of 637 case hnormKind (kindof env c) of
571 (L'.KRecord k, _) => k 638 (L'.KRecord k, _) => k
576 val k2 = rkindof c2 643 val k2 = rkindof c2
577 644
578 val (r1, gs1) = recordSummary (env, denv) c1 645 val (r1, gs1) = recordSummary (env, denv) c1
579 val (r2, gs2) = recordSummary (env, denv) c2 646 val (r2, gs2) = recordSummary (env, denv) c2
580 in 647 in
581 unifyKinds k1 k2; 648 unifyKinds env k1 k2;
582 unifySummaries (env, denv) (k1, r1, r2); 649 unifySummaries (env, denv) (k1, r1, r2);
583 gs1 @ gs2 650 gs1 @ gs2
584 end 651 end
585 652
586 and recordSummary (env, denv) c = 653 and recordSummary (env, denv) c =
846 val old2 = c2*) 913 val old2 = c2*)
847 val (c1, gs1) = hnormCon (env, denv) c1 914 val (c1, gs1) = hnormCon (env, denv) c1
848 val (c2, gs2) = hnormCon (env, denv) c2 915 val (c2, gs2) = hnormCon (env, denv) c2
849 in 916 in
850 let 917 let
918 (*val () = prefaces "unifyCons'" [("old1", p_con env old1),
919 ("old2", p_con env old2),
920 ("c1", p_con env c1),
921 ("c2", p_con env c2)]*)
922
851 val gs3 = unifyCons'' (env, denv) c1 c2 923 val gs3 = unifyCons'' (env, denv) c1 c2
852 in 924 in
853 (*prefaces "unifyCons'" [("c1", p_con env old1),
854 ("c2", p_con env old2),
855 ("t", PD.string (LargeReal.toString (Time.toReal
856 (Time.- (Time.now (), befor)))))];*)
857 gs1 @ gs2 @ gs3 925 gs1 @ gs2 @ gs3
858 end 926 end
859 handle ex => guessMap (env, denv) (c1, c2, gs1 @ gs2, ex) 927 handle ex => guessMap (env, denv) (c1, c2, gs1 @ gs2, ex)
860 end 928 end
861 929
876 @ unifyCons' (env, denv) r1 r2 944 @ unifyCons' (env, denv) r1 r2
877 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => 945 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
878 if expl1 <> expl2 then 946 if expl1 <> expl2 then
879 err CExplicitness 947 err CExplicitness
880 else 948 else
881 (unifyKinds d1 d2; 949 (unifyKinds env d1 d2;
882 let 950 let
883 val denv' = D.enter denv 951 val denv' = D.enter denv
884 (*val befor = Time.now ()*) 952 (*val befor = Time.now ()*)
885 val env' = E.pushCRel env x1 d1 953 val env' = E.pushCRel env x1 d1
886 in 954 in
904 972
905 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) => 973 | (L'.CApp (d1, r1), L'.CApp (d2, r2)) =>
906 (unifyCons' (env, denv) d1 d2; 974 (unifyCons' (env, denv) d1 d2;
907 unifyCons' (env, denv) r1 r2) 975 unifyCons' (env, denv) r1 r2)
908 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => 976 | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) =>
909 (unifyKinds k1 k2; 977 (unifyKinds env k1 k2;
910 unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2) 978 unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2)
911 979
912 | (L'.CName n1, L'.CName n2) => 980 | (L'.CName n1, L'.CName n2) =>
913 if n1 = n2 then 981 if n1 = n2 then
914 [] 982 []
952 if n1 = n2 then 1020 if n1 = n2 then
953 unifyCons' (env, denv) c1 c2 1021 unifyCons' (env, denv) c1 c2
954 else 1022 else
955 err CIncompatible 1023 err CIncompatible
956 1024
1025 | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
1026 (unifyKinds env dom1 dom2;
1027 unifyKinds env ran1 ran2;
1028 [])
1029
1030 | (L'.CKAbs (x, c1), L'.CKAbs (_, c2)) =>
1031 unifyCons' (E.pushKRel env x, denv) c1 c2
1032 | (L'.CKApp (c1, k1), L'.CKApp (c2, k2)) =>
1033 (unifyKinds env k1 k2;
1034 unifyCons' (env, denv) c1 c2)
1035 | (L'.TKFun (x, c1), L'.TKFun (_, c2)) =>
1036 unifyCons' (E.pushKRel env x, denv) c1 c2
1037
957 | (L'.CError, _) => [] 1038 | (L'.CError, _) => []
958 | (_, L'.CError) => [] 1039 | (_, L'.CError) => []
959 1040
960 | (L'.CRecord _, _) => isRecord () 1041 | (L'.CRecord _, _) => isRecord ()
961 | (_, L'.CRecord _) => isRecord () 1042 | (_, L'.CRecord _) => isRecord ()
964 1045
965 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => 1046 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
966 if r1 = r2 then 1047 if r1 = r2 then
967 [] 1048 []
968 else 1049 else
969 (unifyKinds k1 k2; 1050 (unifyKinds env k1 k2;
970 r1 := SOME c2All; 1051 r1 := SOME c2All;
971 []) 1052 [])
972 1053
973 | (L'.CUnif (_, _, _, r), _) => 1054 | (L'.CUnif (_, _, _, r), _) =>
974 if occursCon r c2All then 1055 if occursCon r c2All then
981 err COccursCheckFailed 1062 err COccursCheckFailed
982 else 1063 else
983 (r := SOME c1All; 1064 (r := SOME c1All;
984 []) 1065 [])
985 1066
986 | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) =>
987 (unifyKinds dom1 dom2;
988 unifyKinds ran1 ran2;
989 [])
990
991 | _ => err CIncompatible 1067 | _ => err CIncompatible
992 end 1068 end
993 1069
994 and unifyCons (env, denv) c1 c2 = 1070 and unifyCons (env, denv) c1 c2 =
995 unifyCons' (env, denv) c1 c2 1071 unifyCons' (env, denv) c1 c2
1011 fun primType env p = 1087 fun primType env p =
1012 case p of 1088 case p of
1013 P.Int _ => !int 1089 P.Int _ => !int
1014 | P.Float _ => !float 1090 | P.Float _ => !float
1015 | P.String _ => !string 1091 | P.String _ => !string
1016 1092
1017 fun recCons (k, nm, v, rest, loc) =
1018 (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc),
1019 rest), loc)
1020
1021 fun foldType (dom, loc) =
1022 (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc),
1023 (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc),
1024 (L'.TCFun (L'.Explicit, "v", dom,
1025 (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
1026 (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
1027 (L'.CDisjoint (L'.Instantiate,
1028 (L'.CRecord
1029 ((L'.KUnit, loc),
1030 [((L'.CRel 2, loc),
1031 (L'.CUnit, loc))]), loc),
1032 (L'.CRel 0, loc),
1033 (L'.CApp ((L'.CRel 3, loc),
1034 recCons (dom,
1035 (L'.CRel 2, loc),
1036 (L'.CRel 1, loc),
1037 (L'.CRel 0, loc),
1038 loc)), loc)),
1039 loc)), loc)),
1040 loc)), loc)), loc),
1041 (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc),
1042 (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc),
1043 (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)),
1044 loc)), loc)), loc)
1045
1046 datatype constraint = 1093 datatype constraint =
1047 Disjoint of D.goal 1094 Disjoint of D.goal
1048 | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span 1095 | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span
1049 1096
1050 val enD = map Disjoint 1097 val enD = map Disjoint
1054 fun unravel (t, e) = 1101 fun unravel (t, e) =
1055 let 1102 let
1056 val (t, gs) = hnormCon (env, denv) t 1103 val (t, gs) = hnormCon (env, denv) t
1057 in 1104 in
1058 case t of 1105 case t of
1059 (L'.TCFun (L'.Implicit, x, k, t'), _) => 1106 (L'.TKFun (x, t'), _) =>
1107 let
1108 val u = kunif loc
1109
1110 val t'' = subKindInCon (0, u) t'
1111 val (e, t, gs') = unravel (t'', (L'.EKApp (e, u), loc))
1112 in
1113 (e, t, enD gs @ gs')
1114 end
1115 | (L'.TCFun (L'.Implicit, x, k, t'), _) =>
1060 let 1116 let
1061 val u = cunif (loc, k) 1117 val u = cunif (loc, k)
1062 1118
1063 val t'' = subConInCon (0, u) t' 1119 val t'' = subConInCon (0, u) t'
1064 val (e, t, gs') = unravel (t'', (L'.ECApp (e, u), loc)) 1120 val (e, t, gs') = unravel (t'', (L'.ECApp (e, u), loc))
1573 (eerror, cerror, [])) 1629 (eerror, cerror, []))
1574 end 1630 end
1575 | L.ECAbs (expl, x, k, e) => 1631 | L.ECAbs (expl, x, k, e) =>
1576 let 1632 let
1577 val expl' = elabExplicitness expl 1633 val expl' = elabExplicitness expl
1578 val k' = elabKind k 1634 val k' = elabKind env k
1579 1635
1580 val env' = E.pushCRel env x k' 1636 val env' = E.pushCRel env x k'
1581 val (e', et, gs) = elabExp (env', D.enter denv) e 1637 val (e', et, gs) = elabExp (env', D.enter denv) e
1582 in 1638 in
1583 ((L'.ECAbs (expl', x, k', e'), loc), 1639 ((L'.ECAbs (expl', x, k', e'), loc),
1584 (L'.TCFun (expl', x, k', et), loc), 1640 (L'.TCFun (expl', x, k', et), loc),
1641 gs)
1642 end
1643 | L.EKAbs (x, e) =>
1644 let
1645 val env' = E.pushKRel env x
1646 val (e', et, gs) = elabExp (env', denv) e
1647 in
1648 ((L'.EKAbs (x, e'), loc),
1649 (L'.TKFun (x, et), loc),
1585 gs) 1650 gs)
1586 end 1651 end
1587 1652
1588 | L.EDisjoint (c1, c2, e) => 1653 | L.EDisjoint (c1, c2, e) =>
1589 let 1654 let
1708 in 1773 in
1709 ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc), 1774 ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc),
1710 gs1 @ enD gs2 @ enD gs3 @ enD gs4) 1775 gs1 @ enD gs2 @ enD gs3 @ enD gs4)
1711 end 1776 end
1712 1777
1713 | L.EFold =>
1714 let
1715 val dom = kunif loc
1716 in
1717 ((L'.EFold dom, loc), foldType (dom, loc), [])
1718 end
1719
1720 | L.ECase (e, pes) => 1778 | L.ECase (e, pes) =>
1721 let 1779 let
1722 val (e', et, gs1) = elabExp (env, denv) e 1780 val (e', et, gs1) = elabExp (env, denv) e
1723 val result = cunif (loc, (L'.KType, loc)) 1781 val result = cunif (loc, (L'.KType, loc))
1724 val (pes', gs) = ListUtil.foldlMap 1782 val (pes', gs) = ListUtil.foldlMap
1779 let 1837 let
1780 fun allowable (e, _) = 1838 fun allowable (e, _) =
1781 case e of 1839 case e of
1782 L.EAbs _ => true 1840 L.EAbs _ => true
1783 | L.ECAbs (_, _, _, e) => allowable e 1841 | L.ECAbs (_, _, _, e) => allowable e
1842 | L.EKAbs (_, e) => allowable e
1784 | L.EDisjoint (_, _, e) => allowable e 1843 | L.EDisjoint (_, _, e) => allowable e
1785 | _ => false 1844 | _ => false
1786 1845
1787 val (vis, gs) = ListUtil.foldlMap 1846 val (vis, gs) = ListUtil.foldlMap
1788 (fn ((x, co, e), gs) => 1847 (fn ((x, co, e), gs) =>
1857 1916
1858 fun elabSgn_item ((sgi, loc), (env, denv, gs)) = 1917 fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
1859 case sgi of 1918 case sgi of
1860 L.SgiConAbs (x, k) => 1919 L.SgiConAbs (x, k) =>
1861 let 1920 let
1862 val k' = elabKind k 1921 val k' = elabKind env k
1863 1922
1864 val (env', n) = E.pushCNamed env x k' NONE 1923 val (env', n) = E.pushCNamed env x k' NONE
1865 in 1924 in
1866 ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs)) 1925 ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs))
1867 end 1926 end
1868 1927
1869 | L.SgiCon (x, ko, c) => 1928 | L.SgiCon (x, ko, c) =>
1870 let 1929 let
1871 val k' = case ko of 1930 val k' = case ko of
1872 NONE => kunif loc 1931 NONE => kunif loc
1873 | SOME k => elabKind k 1932 | SOME k => elabKind env k
1874 1933
1875 val (c', ck, gs') = elabCon (env, denv) c 1934 val (c', ck, gs') = elabCon (env, denv) c
1876 val (env', n) = E.pushCNamed env x k' (SOME c') 1935 val (env', n) = E.pushCNamed env x k' (SOME c')
1877 in 1936 in
1878 checkKind env c' ck k'; 1937 checkKind env c' ck k';
1977 val (c', ck, gs') = elabCon (env, denv) c 2036 val (c', ck, gs') = elabCon (env, denv) c
1978 2037
1979 val (env', n) = E.pushENamed env x c' 2038 val (env', n) = E.pushENamed env x c'
1980 val c' = normClassConstraint env c' 2039 val c' = normClassConstraint env c'
1981 in 2040 in
1982 (unifyKinds ck ktype 2041 (unifyKinds env ck ktype
1983 handle KUnify ue => strError env (NotType (ck, ue))); 2042 handle KUnify ue => strError env (NotType (ck, ue)));
1984 2043
1985 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) 2044 ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs))
1986 end 2045 end
1987 2046
2025 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3)) 2084 ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3))
2026 end 2085 end
2027 2086
2028 | L.SgiClassAbs (x, k) => 2087 | L.SgiClassAbs (x, k) =>
2029 let 2088 let
2030 val k = elabKind k 2089 val k = elabKind env k
2031 val k' = (L'.KArrow (k, (L'.KType, loc)), loc) 2090 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
2032 val (env, n) = E.pushCNamed env x k' NONE 2091 val (env, n) = E.pushCNamed env x k' NONE
2033 val env = E.pushClass env n 2092 val env = E.pushClass env n
2034 in 2093 in
2035 ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, [])) 2094 ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, []))
2036 end 2095 end
2037 2096
2038 | L.SgiClass (x, k, c) => 2097 | L.SgiClass (x, k, c) =>
2039 let 2098 let
2040 val k = elabKind k 2099 val k = elabKind env k
2041 val k' = (L'.KArrow (k, (L'.KType, loc)), loc) 2100 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
2042 val (c', ck, gs) = elabCon (env, denv) c 2101 val (c', ck, gs) = elabCon (env, denv) c
2043 val (env, n) = E.pushCNamed env x k' (SOME c') 2102 val (env, n) = E.pushCNamed env x k' (SOME c')
2044 val env = E.pushClass env n 2103 val env = E.pushClass env n
2045 in 2104 in
2147 case #1 (hnormSgn env sgn') of 2206 case #1 (hnormSgn env sgn') of
2148 L'.SgnError => (sgnerror, []) 2207 L'.SgnError => (sgnerror, [])
2149 | L'.SgnConst sgis => 2208 | L'.SgnConst sgis =>
2150 if List.exists (fn (L'.SgiConAbs (x', _, k), _) => 2209 if List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
2151 x' = x andalso 2210 x' = x andalso
2152 (unifyKinds k ck 2211 (unifyKinds env k ck
2153 handle KUnify x => sgnError env (WhereWrongKind x); 2212 handle KUnify x => sgnError env (WhereWrongKind x);
2154 true) 2213 true)
2155 | _ => false) sgis then 2214 | _ => false) sgis then
2156 ((L'.SgnWhere (sgn', x, c'), loc), ds1 @ ds2) 2215 ((L'.SgnWhere (sgn', x, c'), loc), ds1 @ ds2)
2157 else 2216 else
2353 seek (fn (env, sgi1All as (sgi1, _)) => 2412 seek (fn (env, sgi1All as (sgi1, _)) =>
2354 let 2413 let
2355 fun found (x', n1, k1, co1) = 2414 fun found (x', n1, k1, co1) =
2356 if x = x' then 2415 if x = x' then
2357 let 2416 let
2358 val () = unifyKinds k1 k2 2417 val () = unifyKinds env k1 k2
2359 handle KUnify (k1, k2, err) => 2418 handle KUnify (k1, k2, err) =>
2360 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) 2419 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
2361 val env = E.pushCNamedAs env x n1 k1 co1 2420 val env = E.pushCNamedAs env x n1 k1 co1
2362 in 2421 in
2363 SOME (if n1 = n2 then 2422 SOME (if n1 = n2 then
2604 seek (fn (env, sgi1All as (sgi1, _)) => 2663 seek (fn (env, sgi1All as (sgi1, _)) =>
2605 let 2664 let
2606 fun found (x', n1, k1, co) = 2665 fun found (x', n1, k1, co) =
2607 if x = x' then 2666 if x = x' then
2608 let 2667 let
2609 val () = unifyKinds k1 k2 2668 val () = unifyKinds env k1 k2
2610 handle KUnify (k1, k2, err) => 2669 handle KUnify (k1, k2, err) =>
2611 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) 2670 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
2612 2671
2613 val k = (L'.KArrow (k1, (L'.KType, loc)), loc) 2672 val k = (L'.KArrow (k1, (L'.KType, loc)), loc)
2614 val env = E.pushCNamedAs env x n1 k co 2673 val env = E.pushCNamedAs env x n1 k co
2633 val k = (L'.KArrow (k2, (L'.KType, loc)), loc) 2692 val k = (L'.KArrow (k2, (L'.KType, loc)), loc)
2634 2693
2635 fun found (x', n1, k1, c1) = 2694 fun found (x', n1, k1, c1) =
2636 if x = x' then 2695 if x = x' then
2637 let 2696 let
2638 val () = unifyKinds k1 k2 2697 val () = unifyKinds env k1 k2
2639 handle KUnify (k1, k2, err) => 2698 handle KUnify (k1, k2, err) =>
2640 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) 2699 sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err))
2641 2700
2642 fun good () = 2701 fun good () =
2643 let 2702 let
2700 | CVar _ => true 2759 | CVar _ => true
2701 | CApp (c1, c2) => none c1 andalso none c2 2760 | CApp (c1, c2) => none c1 andalso none c2
2702 | CAbs _ => false 2761 | CAbs _ => false
2703 | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 2762 | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
2704 2763
2764 | CKAbs _ => false
2765 | TKFun _ => false
2766
2705 | CName _ => true 2767 | CName _ => true
2706 2768
2707 | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs 2769 | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs
2708 | CConcat (c1, c2) => none c1 andalso none c2 2770 | CConcat (c1, c2) => none c1 andalso none c2
2709 | CMap => true 2771 | CMap => true
2725 2787
2726 | CVar _ => true 2788 | CVar _ => true
2727 | CApp (c1, c2) => pos c1 andalso none c2 2789 | CApp (c1, c2) => pos c1 andalso none c2
2728 | CAbs _ => false 2790 | CAbs _ => false
2729 | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 2791 | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3
2792
2793 | CKAbs _ => false
2794 | TKFun _ => false
2730 2795
2731 | CName _ => true 2796 | CName _ => true
2732 2797
2733 | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs 2798 | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs
2734 | CConcat (c1, c2) => pos c1 andalso pos c2 2799 | CConcat (c1, c2) => pos c1 andalso pos c2
2774 end 2839 end
2775 2840
2776 | L'.KError => NONE 2841 | L'.KError => NONE
2777 | L'.KUnif (_, _, ref (SOME k)) => decompileKind k 2842 | L'.KUnif (_, _, ref (SOME k)) => decompileKind k
2778 | L'.KUnif _ => NONE 2843 | L'.KUnif _ => NONE
2844
2845 | L'.KRel _ => NONE
2846 | L'.KFun _ => NONE
2779 2847
2780 fun decompileCon env (c, loc) = 2848 fun decompileCon env (c, loc) =
2781 case c of 2849 case c of
2782 L'.CRel i => 2850 L'.CRel i =>
2783 let 2851 let
2912 case d of 2980 case d of
2913 L.DCon (x, ko, c) => 2981 L.DCon (x, ko, c) =>
2914 let 2982 let
2915 val k' = case ko of 2983 val k' = case ko of
2916 NONE => kunif loc 2984 NONE => kunif loc
2917 | SOME k => elabKind k 2985 | SOME k => elabKind env k
2918 2986
2919 val (c', ck, gs') = elabCon (env, denv) c 2987 val (c', ck, gs') = elabCon (env, denv) c
2920 val (env', n) = E.pushCNamed env x k' (SOME c') 2988 val (env', n) = E.pushCNamed env x k' (SOME c')
2921 in 2989 in
2922 checkKind env c' ck k'; 2990 checkKind env c' ck k';
3045 let 3113 let
3046 fun allowable (e, _) = 3114 fun allowable (e, _) =
3047 case e of 3115 case e of
3048 L.EAbs _ => true 3116 L.EAbs _ => true
3049 | L.ECAbs (_, _, _, e) => allowable e 3117 | L.ECAbs (_, _, _, e) => allowable e
3118 | L.EKAbs (_, e) => allowable e
3050 | L.EDisjoint (_, _, e) => allowable e 3119 | L.EDisjoint (_, _, e) => allowable e
3051 | _ => false 3120 | _ => false
3052 3121
3053 val (vis, gs) = ListUtil.foldlMap 3122 val (vis, gs) = ListUtil.foldlMap
3054 (fn ((x, co, e), gs) => 3123 (fn ((x, co, e), gs) =>
3262 ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs)) 3331 ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs))
3263 end 3332 end
3264 3333
3265 | L.DClass (x, k, c) => 3334 | L.DClass (x, k, c) =>
3266 let 3335 let
3267 val k = elabKind k 3336 val k = elabKind env k
3268 val k' = (L'.KArrow (k, (L'.KType, loc)), loc) 3337 val k' = (L'.KArrow (k, (L'.KType, loc)), loc)
3269 val (c', ck, gs') = elabCon (env, denv) c 3338 val (c', ck, gs') = elabCon (env, denv) c
3270 val (env, n) = E.pushCNamed env x k' (SOME c') 3339 val (env, n) = E.pushCNamed env x k' (SOME c')
3271 val env = E.pushClass env n 3340 val env = E.pushClass env n
3272 in 3341 in