Mercurial > urweb

comparison src/elaborate.sml @ 83:0a1baddd8ab2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Threading disjointness conditions through Elaborate
author Adam Chlipala <adamc@hcoop.net>
date Tue, 01 Jul 2008 11:39:14 -0400
parents b4f2a258e52c
children e86370850c30
comparison
equal deleted inserted replaced
82:b4f2a258e52c 83:0a1baddd8ab2
211 (L'.KArrow (ran, ran), loc)), loc)), loc), 211 (L'.KArrow (ran, ran), loc)), loc)), loc),
212 (L'.KArrow (ran, 212 (L'.KArrow (ran,
213 (L'.KArrow ((L'.KRecord dom, loc), 213 (L'.KArrow ((L'.KRecord dom, loc),
214 ran), loc)), loc)), loc) 214 ran), loc)), loc)), loc)
215 215
216 fun elabCon env (c, loc) = 216 fun elabCon (env, denv) (c, loc) =
217 case c of 217 case c of
218 L.CAnnot (c, k) => 218 L.CAnnot (c, k) =>
219 let 219 let
220 val k' = elabKind k 220 val k' = elabKind k
221 val (c', ck) = elabCon env c 221 val (c', ck, gs) = elabCon (env, denv) c
222 in 222 in
223 checkKind env c' ck k'; 223 checkKind env c' ck k';
224 (c', k') 224 (c', k', gs)
225 end 225 end
226 226
227 | L.TFun (t1, t2) => 227 | L.TFun (t1, t2) =>
228 let 228 let
229 val (t1', k1) = elabCon env t1 229 val (t1', k1, gs1) = elabCon (env, denv) t1
230 val (t2', k2) = elabCon env t2 230 val (t2', k2, gs2) = elabCon (env, denv) t2
231 in 231 in
232 checkKind env t1' k1 ktype; 232 checkKind env t1' k1 ktype;
233 checkKind env t2' k2 ktype; 233 checkKind env t2' k2 ktype;
234 ((L'.TFun (t1', t2'), loc), ktype) 234 ((L'.TFun (t1', t2'), loc), ktype, gs1 @ gs2)
235 end 235 end
236 | L.TCFun (e, x, k, t) => 236 | L.TCFun (e, x, k, t) =>
237 let 237 let
238 val e' = elabExplicitness e 238 val e' = elabExplicitness e
239 val k' = elabKind k 239 val k' = elabKind k
240 val env' = E.pushCRel env x k' 240 val env' = E.pushCRel env x k'
241 val (t', tk) = elabCon env' t 241 val (t', tk, gs) = elabCon (env', D.enter denv) t
242 in 242 in
243 checkKind env t' tk ktype; 243 checkKind env t' tk ktype;
244 ((L'.TCFun (e', x, k', t'), loc), ktype) 244 ((L'.TCFun (e', x, k', t'), loc), ktype, gs)
245 end 245 end
246 | L.TRecord c => 246 | L.TRecord c =>
247 let 247 let
248 val (c', ck) = elabCon env c 248 val (c', ck, gs) = elabCon (env, denv) c
249 val k = (L'.KRecord ktype, loc) 249 val k = (L'.KRecord ktype, loc)
250 in 250 in
251 checkKind env c' ck k; 251 checkKind env c' ck k;
252 ((L'.TRecord c', loc), ktype) 252 ((L'.TRecord c', loc), ktype, gs)
253 end 253 end
254 254
255 | L.CVar ([], s) => 255 | L.CVar ([], s) =>
256 (case E.lookupC env s of 256 (case E.lookupC env s of
257 E.NotBound => 257 E.NotBound =>
258 (conError env (UnboundCon (loc, s)); 258 (conError env (UnboundCon (loc, s));
259 (cerror, kerror)) 259 (cerror, kerror, []))
260 | E.Rel (n, k) => 260 | E.Rel (n, k) =>
261 ((L'.CRel n, loc), k) 261 ((L'.CRel n, loc), k, [])
262 | E.Named (n, k) => 262 | E.Named (n, k) =>
263 ((L'.CNamed n, loc), k)) 263 ((L'.CNamed n, loc), k, []))
264 | L.CVar (m1 :: ms, s) => 264 | L.CVar (m1 :: ms, s) =>
265 (case E.lookupStr env m1 of 265 (case E.lookupStr env m1 of
266 NONE => (conError env (UnboundStrInCon (loc, m1)); 266 NONE => (conError env (UnboundStrInCon (loc, m1));
267 (cerror, kerror)) 267 (cerror, kerror, []))
268 | SOME (n, sgn) => 268 | SOME (n, sgn) =>
269 let 269 let
270 val (str, sgn) = foldl (fn (m, (str, sgn)) => 270 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
271 case E.projectStr env {sgn = sgn, str = str, field = m} of 271 case E.projectStr env {sgn = sgn, str = str, field = m} of
272 NONE => (conError env (UnboundStrInCon (loc, m)); 272 NONE => (conError env (UnboundStrInCon (loc, m));
277 val k = case E.projectCon env {sgn = sgn, str = str, field = s} of 277 val k = case E.projectCon env {sgn = sgn, str = str, field = s} of
278 NONE => (conError env (UnboundCon (loc, s)); 278 NONE => (conError env (UnboundCon (loc, s));
279 kerror) 279 kerror)
280 | SOME (k, _) => k 280 | SOME (k, _) => k
281 in 281 in
282 ((L'.CModProj (n, ms, s), loc), k) 282 ((L'.CModProj (n, ms, s), loc), k, [])
283 end) 283 end)
284 284
285 | L.CApp (c1, c2) => 285 | L.CApp (c1, c2) =>
286 let 286 let
287 val (c1', k1) = elabCon env c1 287 val (c1', k1, gs1) = elabCon (env, denv) c1
288 val (c2', k2) = elabCon env c2 288 val (c2', k2, gs2) = elabCon (env, denv) c2
289 val dom = kunif loc 289 val dom = kunif loc
290 val ran = kunif loc 290 val ran = kunif loc
291 in 291 in
292 checkKind env c1' k1 (L'.KArrow (dom, ran), loc); 292 checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
293 checkKind env c2' k2 dom; 293 checkKind env c2' k2 dom;
294 ((L'.CApp (c1', c2'), loc), ran) 294 ((L'.CApp (c1', c2'), loc), ran, gs1 @ gs2)
295 end 295 end
296 | L.CAbs (x, ko, t) => 296 | L.CAbs (x, ko, t) =>
297 let 297 let
298 val k' = case ko of 298 val k' = case ko of
299 NONE => kunif loc 299 NONE => kunif loc
300 | SOME k => elabKind k 300 | SOME k => elabKind k
301 val env' = E.pushCRel env x k' 301 val env' = E.pushCRel env x k'
302 val (t', tk) = elabCon env' t 302 val (t', tk, gs) = elabCon (env', D.enter denv) t
303 in 303 in
304 ((L'.CAbs (x, k', t'), loc), 304 ((L'.CAbs (x, k', t'), loc),
305 (L'.KArrow (k', tk), loc)) 305 (L'.KArrow (k', tk), loc),
306 gs)
306 end 307 end
307 308
308 | L.CName s => 309 | L.CName s =>
309 ((L'.CName s, loc), kname) 310 ((L'.CName s, loc), kname, [])
310 311
311 | L.CRecord xcs => 312 | L.CRecord xcs =>
312 let 313 let
313 val k = kunif loc 314 val k = kunif loc
314 315
315 val xcs' = map (fn (x, c) => 316 val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) =>
316 let 317 let
317 val (x', xk) = elabCon env x 318 val (x', xk, gs1) = elabCon (env, denv) x
318 val (c', ck) = elabCon env c 319 val (c', ck, gs2) = elabCon (env, denv) c
319 in 320 in
320 checkKind env x' xk kname; 321 checkKind env x' xk kname;
321 checkKind env c' ck k; 322 checkKind env c' ck k;
322 (x', c') 323 ((x', c'), gs1 @ gs2 @ gs)
323 end) xcs 324 end) [] xcs
324 325
325 val rc = (L'.CRecord (k, xcs'), loc) 326 val rc = (L'.CRecord (k, xcs'), loc)
326 (* Add duplicate field checking later. *) 327 (* Add duplicate field checking later. *)
327 in 328
328 (rc, (L'.KRecord k, loc)) 329 fun prove (xcs, ds) =
330 case xcs of
331 [] => ds
332 | xc :: rest =>
333 let
334 val r1 = (L'.CRecord (k, [xc]), loc)
335 val ds = foldl (fn (xc', ds) =>
336 let
337 val r2 = (L'.CRecord (k, [xc']), loc)
338 in
339 map (fn cs => (loc, env, denv, cs)) (D.prove env denv (r1, r2, loc))
340 @ ds
341 end)
342 ds rest
343 in
344 prove (rest, ds)
345 end
346 in
347 (rc, (L'.KRecord k, loc), prove (xcs', gs))
329 end 348 end
330 | L.CConcat (c1, c2) => 349 | L.CConcat (c1, c2) =>
331 let 350 let
332 val (c1', k1) = elabCon env c1 351 val (c1', k1, gs1) = elabCon (env, denv) c1
333 val (c2', k2) = elabCon env c2 352 val (c2', k2, gs2) = elabCon (env, denv) c2
334 val ku = kunif loc 353 val ku = kunif loc
335 val k = (L'.KRecord ku, loc) 354 val k = (L'.KRecord ku, loc)
336 in 355 in
337 case D.prove env D.empty (c1', c2', loc) of
338 [] => ()
339 | _ => raise Fail "Can't prove disjointness";
340
341 checkKind env c1' k1 k; 356 checkKind env c1' k1 k;
342 checkKind env c2' k2 k; 357 checkKind env c2' k2 k;
343 ((L'.CConcat (c1', c2'), loc), k) 358 ((L'.CConcat (c1', c2'), loc), k,
359 map (fn cs => (loc, env, denv, cs)) (D.prove env denv (c1', c2', loc)) @ gs1 @ gs2)
344 end 360 end
345 | L.CFold => 361 | L.CFold =>
346 let 362 let
347 val dom = kunif loc 363 val dom = kunif loc
348 val ran = kunif loc 364 val ran = kunif loc
349 in 365 in
350 ((L'.CFold (dom, ran), loc), 366 ((L'.CFold (dom, ran), loc),
351 foldKind (dom, ran, loc)) 367 foldKind (dom, ran, loc),
352 end 368 [])
353 369 end
354 | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc)) 370
371 | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), [])
355 372
356 | L.CWild k => 373 | L.CWild k =>
357 let 374 let
358 val k' = elabKind k 375 val k' = elabKind k
359 in 376 in
360 (cunif (loc, k'), k') 377 (cunif (loc, k'), k', [])
361 end 378 end
362 379
363 fun kunifsRemain k = 380 fun kunifsRemain k =
364 case k of 381 case k of
365 L'.KUnif (_, _, ref NONE) => true 382 L'.KUnif (_, _, ref NONE) => true
822 | _ => (e, t) 839 | _ => (e, t)
823 in 840 in
824 unravel (t, e) 841 unravel (t, e)
825 end 842 end
826 843
827 fun elabExp env (e, loc) = 844 fun elabExp (env, denv) (e, loc) =
828 case e of 845 case e of
829 L.EAnnot (e, t) => 846 L.EAnnot (e, t) =>
830 let 847 let
831 val (e', et) = elabExp env e 848 val (e', et, gs1) = elabExp (env, denv) e
832 val (t', _) = elabCon env t 849 val (t', _, gs2) = elabCon (env, denv) t
833 in 850 in
834 checkCon env e' et t'; 851 checkCon env e' et t';
835 (e', t') 852 (e', t', gs1 @ gs2)
836 end 853 end
837 854
838 | L.EPrim p => ((L'.EPrim p, loc), primType env p) 855 | L.EPrim p => ((L'.EPrim p, loc), primType env p, [])
839 | L.EVar ([], s) => 856 | L.EVar ([], s) =>
840 (case E.lookupE env s of 857 (case E.lookupE env s of
841 E.NotBound => 858 E.NotBound =>
842 (expError env (UnboundExp (loc, s)); 859 (expError env (UnboundExp (loc, s));
843 (eerror, cerror)) 860 (eerror, cerror, []))
844 | E.Rel (n, t) => ((L'.ERel n, loc), t) 861 | E.Rel (n, t) => ((L'.ERel n, loc), t, [])
845 | E.Named (n, t) => ((L'.ENamed n, loc), t)) 862 | E.Named (n, t) => ((L'.ENamed n, loc), t, []))
846 | L.EVar (m1 :: ms, s) => 863 | L.EVar (m1 :: ms, s) =>
847 (case E.lookupStr env m1 of 864 (case E.lookupStr env m1 of
848 NONE => (expError env (UnboundStrInExp (loc, m1)); 865 NONE => (expError env (UnboundStrInExp (loc, m1));
849 (eerror, cerror)) 866 (eerror, cerror, []))
850 | SOME (n, sgn) => 867 | SOME (n, sgn) =>
851 let 868 let
852 val (str, sgn) = foldl (fn (m, (str, sgn)) => 869 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
853 case E.projectStr env {sgn = sgn, str = str, field = m} of 870 case E.projectStr env {sgn = sgn, str = str, field = m} of
854 NONE => (conError env (UnboundStrInCon (loc, m)); 871 NONE => (conError env (UnboundStrInCon (loc, m));
859 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of 876 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
860 NONE => (expError env (UnboundExp (loc, s)); 877 NONE => (expError env (UnboundExp (loc, s));
861 cerror) 878 cerror)
862 | SOME t => t 879 | SOME t => t
863 in 880 in
864 ((L'.EModProj (n, ms, s), loc), t) 881 ((L'.EModProj (n, ms, s), loc), t, [])
865 end) 882 end)
866 883
867 | L.EApp (e1, e2) => 884 | L.EApp (e1, e2) =>
868 let 885 let
869 val (e1', t1) = elabExp env e1 886 val (e1', t1, gs1) = elabExp (env, denv) e1
870 val (e1', t1) = elabHead env e1' t1 887 val (e1', t1) = elabHead env e1' t1
871 val (e2', t2) = elabExp env e2 888 val (e2', t2, gs2) = elabExp (env, denv) e2
872 889
873 val dom = cunif (loc, ktype) 890 val dom = cunif (loc, ktype)
874 val ran = cunif (loc, ktype) 891 val ran = cunif (loc, ktype)
875 val t = (L'.TFun (dom, ran), dummy) 892 val t = (L'.TFun (dom, ran), dummy)
876 in 893 in
877 checkCon env e1' t1 t; 894 checkCon env e1' t1 t;
878 checkCon env e2' t2 dom; 895 checkCon env e2' t2 dom;
879 ((L'.EApp (e1', e2'), loc), ran) 896 ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2)
880 end 897 end
881 | L.EAbs (x, to, e) => 898 | L.EAbs (x, to, e) =>
882 let 899 let
883 val t' = case to of 900 val (t', gs1) = case to of
884 NONE => cunif (loc, ktype) 901 NONE => (cunif (loc, ktype), [])
885 | SOME t => 902 | SOME t =>
886 let 903 let
887 val (t', tk) = elabCon env t 904 val (t', tk, gs) = elabCon (env, denv) t
888 in 905 in
889 checkKind env t' tk ktype; 906 checkKind env t' tk ktype;
890 t' 907 (t', gs)
891 end 908 end
892 val (e', et) = elabExp (E.pushERel env x t') e 909 val (e', et, gs2) = elabExp (E.pushERel env x t', denv) e
893 in 910 in
894 ((L'.EAbs (x, t', et, e'), loc), 911 ((L'.EAbs (x, t', et, e'), loc),
895 (L'.TFun (t', et), loc)) 912 (L'.TFun (t', et), loc),
913 gs1 @ gs2)
896 end 914 end
897 | L.ECApp (e, c) => 915 | L.ECApp (e, c) =>
898 let 916 let
899 val (e', et) = elabExp env e 917 val (e', et, gs1) = elabExp (env, denv) e
900 val (e', et) = elabHead env e' et 918 val (e', et) = elabHead env e' et
901 val (c', ck) = elabCon env c 919 val (c', ck, gs2) = elabCon (env, denv) c
902 in 920 in
903 case #1 (hnormCon env et) of 921 case #1 (hnormCon env et) of
904 L'.CError => (eerror, cerror) 922 L'.CError => (eerror, cerror, [])
905 | L'.TCFun (_, _, k, eb) => 923 | L'.TCFun (_, _, k, eb) =>
906 let 924 let
907 val () = checkKind env c' ck k 925 val () = checkKind env c' ck k
908 val eb' = subConInCon (0, c') eb 926 val eb' = subConInCon (0, c') eb
909 handle SynUnif => (expError env (Unif ("substitution", eb)); 927 handle SynUnif => (expError env (Unif ("substitution", eb));
910 cerror) 928 cerror)
911 in 929 in
912 ((L'.ECApp (e', c'), loc), eb') 930 ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2)
913 end 931 end
914 932
915 | L'.CUnif _ => 933 | L'.CUnif _ =>
916 (expError env (Unif ("application", et)); 934 (expError env (Unif ("application", et));
917 (eerror, cerror)) 935 (eerror, cerror, []))
918 936
919 | _ => 937 | _ =>
920 (expError env (WrongForm ("constructor function", e', et)); 938 (expError env (WrongForm ("constructor function", e', et));
921 (eerror, cerror)) 939 (eerror, cerror, []))
922 end 940 end
923 | L.ECAbs (expl, x, k, e) => 941 | L.ECAbs (expl, x, k, e) =>
924 let 942 let
925 val expl' = elabExplicitness expl 943 val expl' = elabExplicitness expl
926 val k' = elabKind k 944 val k' = elabKind k
927 val (e', et) = elabExp (E.pushCRel env x k') e 945 val (e', et, gs) = elabExp (E.pushCRel env x k', D.enter denv) e
928 in 946 in
929 ((L'.ECAbs (expl', x, k', e'), loc), 947 ((L'.ECAbs (expl', x, k', e'), loc),
930 (L'.TCFun (expl', x, k', et), loc)) 948 (L'.TCFun (expl', x, k', et), loc),
949 gs)
931 end 950 end
932 951
933 | L.ERecord xes => 952 | L.ERecord xes =>
934 let 953 let
935 val xes' = map (fn (x, e) => 954 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
936 let 955 let
937 val (x', xk) = elabCon env x 956 val (x', xk, gs1) = elabCon (env, denv) x
938 val (e', et) = elabExp env e 957 val (e', et, gs2) = elabExp (env, denv) e
939 in 958 in
940 checkKind env x' xk kname; 959 checkKind env x' xk kname;
941 (x', e', et) 960 ((x', e', et), gs1 @ gs2 @ gs)
942 end) xes 961 end)
962 [] xes
943 in 963 in
944 ((L'.ERecord xes', loc), 964 ((L'.ERecord xes', loc),
945 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc)) 965 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
966 gs)
946 end 967 end
947 968
948 | L.EField (e, c) => 969 | L.EField (e, c) =>
949 let 970 let
950 val (e', et) = elabExp env e 971 val (e', et, gs1) = elabExp (env, denv) e
951 val (c', ck) = elabCon env c 972 val (c', ck, gs2) = elabCon (env, denv) c
952 973
953 val ft = cunif (loc, ktype) 974 val ft = cunif (loc, ktype)
954 val rest = cunif (loc, ktype_record) 975 val rest = cunif (loc, ktype_record)
955 in 976 in
956 checkKind env c' ck kname; 977 checkKind env c' ck kname;
957 checkCon env e' et (L'.TRecord (L'.CConcat ((L'.CRecord (ktype, [(c', ft)]), loc), rest), loc), loc); 978 checkCon env e' et (L'.TRecord (L'.CConcat ((L'.CRecord (ktype, [(c', ft)]), loc), rest), loc), loc);
958 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft) 979 ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2)
959 end 980 end
960 981
961 | L.EFold => 982 | L.EFold =>
962 let 983 let
963 val dom = kunif loc 984 val dom = kunif loc
964 in 985 in
965 ((L'.EFold dom, loc), foldType (dom, loc)) 986 ((L'.EFold dom, loc), foldType (dom, loc), [])
966 end 987 end
967 988
968 989
969 datatype decl_error = 990 datatype decl_error =
970 KunifsRemain of ErrorMsg.span 991 KunifsRemain of ErrorMsg.span
1063 ("Subkind 2", p_kind k2)]; 1084 ("Subkind 2", p_kind k2)];
1064 kunifyError ue) 1085 kunifyError ue)
1065 1086
1066 val hnormSgn = E.hnormSgn 1087 val hnormSgn = E.hnormSgn
1067 1088
1068 fun elabSgn_item ((sgi, loc), env) = 1089 fun elabSgn_item denv ((sgi, loc), (env, gs)) =
1069 case sgi of 1090 case sgi of
1070 L.SgiConAbs (x, k) => 1091 L.SgiConAbs (x, k) =>
1071 let 1092 let
1072 val k' = elabKind k 1093 val k' = elabKind k
1073 1094
1074 val (env', n) = E.pushCNamed env x k' NONE 1095 val (env', n) = E.pushCNamed env x k' NONE
1075 in 1096 in
1076 ([(L'.SgiConAbs (x, n, k'), loc)], env') 1097 ([(L'.SgiConAbs (x, n, k'), loc)], (env', gs))
1077 end 1098 end
1078 1099
1079 | L.SgiCon (x, ko, c) => 1100 | L.SgiCon (x, ko, c) =>
1080 let 1101 let
1081 val k' = case ko of 1102 val k' = case ko of
1082 NONE => kunif loc 1103 NONE => kunif loc
1083 | SOME k => elabKind k 1104 | SOME k => elabKind k
1084 1105
1085 val (c', ck) = elabCon env c 1106 val (c', ck, gs') = elabCon (env, denv) c
1086 val (env', n) = E.pushCNamed env x k' (SOME c') 1107 val (env', n) = E.pushCNamed env x k' (SOME c')
1087 in 1108 in
1088 checkKind env c' ck k'; 1109 checkKind env c' ck k';
1089 1110
1090 ([(L'.SgiCon (x, n, k', c'), loc)], env') 1111 ([(L'.SgiCon (x, n, k', c'), loc)], (env', gs' @ gs))
1091 end 1112 end
1092 1113
1093 | L.SgiVal (x, c) => 1114 | L.SgiVal (x, c) =>
1094 let 1115 let
1095 val (c', ck) = elabCon env c 1116 val (c', ck, gs') = elabCon (env, denv) c
1096 1117
1097 val (env', n) = E.pushENamed env x c' 1118 val (env', n) = E.pushENamed env x c'
1098 in 1119 in
1099 (unifyKinds ck ktype 1120 (unifyKinds ck ktype
1100 handle KUnify ue => strError env (NotType (ck, ue))); 1121 handle KUnify ue => strError env (NotType (ck, ue)));
1101 1122
1102 ([(L'.SgiVal (x, n, c'), loc)], env') 1123 ([(L'.SgiVal (x, n, c'), loc)], (env', gs' @ gs))
1103 end 1124 end
1104 1125
1105 | L.SgiStr (x, sgn) => 1126 | L.SgiStr (x, sgn) =>
1106 let 1127 let
1107 val sgn' = elabSgn env sgn 1128 val (sgn', gs') = elabSgn (env, denv) sgn
1108 val (env', n) = E.pushStrNamed env x sgn' 1129 val (env', n) = E.pushStrNamed env x sgn'
1109 in 1130 in
1110 ([(L'.SgiStr (x, n, sgn'), loc)], env') 1131 ([(L'.SgiStr (x, n, sgn'), loc)], (env', gs' @ gs))
1111 end 1132 end
1112 1133
1113 | L.SgiSgn (x, sgn) => 1134 | L.SgiSgn (x, sgn) =>
1114 let 1135 let
1115 val sgn' = elabSgn env sgn 1136 val (sgn', gs') = elabSgn (env, denv) sgn
1116 val (env', n) = E.pushSgnNamed env x sgn' 1137 val (env', n) = E.pushSgnNamed env x sgn'
1117 in 1138 in
1118 ([(L'.SgiSgn (x, n, sgn'), loc)], env') 1139 ([(L'.SgiSgn (x, n, sgn'), loc)], (env', gs' @ gs))
1119 end 1140 end
1120 1141
1121 | L.SgiInclude sgn => 1142 | L.SgiInclude sgn =>
1122 let 1143 let
1123 val sgn' = elabSgn env sgn 1144 val (sgn', gs') = elabSgn (env, denv) sgn
1124 in 1145 in
1125 case #1 (hnormSgn env sgn') of 1146 case #1 (hnormSgn env sgn') of
1126 L'.SgnConst sgis => 1147 L'.SgnConst sgis =>
1127 (sgis, foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis) 1148 (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, gs' @ gs))
1128 | _ => (sgnError env (NotIncludable sgn'); 1149 | _ => (sgnError env (NotIncludable sgn');
1129 ([], env)) 1150 ([], (env, [])))
1130 end 1151 end
1131 1152
1132 and elabSgn env (sgn, loc) = 1153 and elabSgn (env, denv) (sgn, loc) =
1133 case sgn of 1154 case sgn of
1134 L.SgnConst sgis => 1155 L.SgnConst sgis =>
1135 let 1156 let
1136 val (sgis', _) = ListUtil.foldlMapConcat elabSgn_item env sgis 1157 val (sgis', (_, gs)) = ListUtil.foldlMapConcat (elabSgn_item denv) (env, []) sgis
1137 1158
1138 val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) => 1159 val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) =>
1139 case sgi of 1160 case sgi of
1140 L'.SgiConAbs (x, _, _) => 1161 L'.SgiConAbs (x, _, _) =>
1141 (if SS.member (cons, x) then 1162 (if SS.member (cons, x) then
1167 else 1188 else
1168 (); 1189 ();
1169 (cons, vals, sgns, SS.add (strs, x)))) 1190 (cons, vals, sgns, SS.add (strs, x))))
1170 (SS.empty, SS.empty, SS.empty, SS.empty) sgis' 1191 (SS.empty, SS.empty, SS.empty, SS.empty) sgis'
1171 in 1192 in
1172 (L'.SgnConst sgis', loc) 1193 ((L'.SgnConst sgis', loc), gs)
1173 end 1194 end
1174 | L.SgnVar x => 1195 | L.SgnVar x =>
1175 (case E.lookupSgn env x of 1196 (case E.lookupSgn env x of
1176 NONE => 1197 NONE =>
1177 (sgnError env (UnboundSgn (loc, x)); 1198 (sgnError env (UnboundSgn (loc, x));
1178 (L'.SgnError, loc)) 1199 ((L'.SgnError, loc), []))
1179 | SOME (n, sgis) => (L'.SgnVar n, loc)) 1200 | SOME (n, sgis) => ((L'.SgnVar n, loc), []))
1180 | L.SgnFun (m, dom, ran) => 1201 | L.SgnFun (m, dom, ran) =>
1181 let 1202 let
1182 val dom' = elabSgn env dom 1203 val (dom', gs1) = elabSgn (env, denv) dom
1183 val (env', n) = E.pushStrNamed env m dom' 1204 val (env', n) = E.pushStrNamed env m dom'
1184 val ran' = elabSgn env' ran 1205 val (ran', gs2) = elabSgn (env', denv) ran
1185 in 1206 in
1186 (L'.SgnFun (m, n, dom', ran'), loc) 1207 ((L'.SgnFun (m, n, dom', ran'), loc), gs1 @ gs2)
1187 end 1208 end
1188 | L.SgnWhere (sgn, x, c) => 1209 | L.SgnWhere (sgn, x, c) =>
1189 let 1210 let
1190 val sgn' = elabSgn env sgn 1211 val (sgn', ds1) = elabSgn (env, denv) sgn
1191 val (c', ck) = elabCon env c 1212 val (c', ck, ds2) = elabCon (env, denv) c
1192 in 1213 in
1193 case #1 (hnormSgn env sgn') of 1214 case #1 (hnormSgn env sgn') of
1194 L'.SgnError => sgnerror 1215 L'.SgnError => (sgnerror, [])
1195 | L'.SgnConst sgis => 1216 | L'.SgnConst sgis =>
1196 if List.exists (fn (L'.SgiConAbs (x', _, k), _) => 1217 if List.exists (fn (L'.SgiConAbs (x', _, k), _) =>
1197 x' = x andalso 1218 x' = x andalso
1198 (unifyKinds k ck 1219 (unifyKinds k ck
1199 handle KUnify x => sgnError env (WhereWrongKind x); 1220 handle KUnify x => sgnError env (WhereWrongKind x);
1200 true) 1221 true)
1201 | _ => false) sgis then 1222 | _ => false) sgis then
1202 (L'.SgnWhere (sgn', x, c'), loc) 1223 ((L'.SgnWhere (sgn', x, c'), loc), ds1 @ ds2)
1203 else 1224 else
1204 (sgnError env (UnWhereable (sgn', x)); 1225 (sgnError env (UnWhereable (sgn', x));
1205 sgnerror) 1226 (sgnerror, []))
1206 | _ => (sgnError env (UnWhereable (sgn', x)); 1227 | _ => (sgnError env (UnWhereable (sgn', x));
1207 sgnerror) 1228 (sgnerror, []))
1208 end 1229 end
1209 | L.SgnProj (m, ms, x) => 1230 | L.SgnProj (m, ms, x) =>
1210 (case E.lookupStr env m of 1231 (case E.lookupStr env m of
1211 NONE => (strError env (UnboundStr (loc, m)); 1232 NONE => (strError env (UnboundStr (loc, m));
1212 sgnerror) 1233 (sgnerror, []))
1213 | SOME (n, sgn) => 1234 | SOME (n, sgn) =>
1214 let 1235 let
1215 val (str, sgn) = foldl (fn (m, (str, sgn)) => 1236 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
1216 case E.projectStr env {sgn = sgn, str = str, field = m} of 1237 case E.projectStr env {sgn = sgn, str = str, field = m} of
1217 NONE => (strError env (UnboundStr (loc, m)); 1238 NONE => (strError env (UnboundStr (loc, m));
1219 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) 1240 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1220 ((L'.StrVar n, loc), sgn) ms 1241 ((L'.StrVar n, loc), sgn) ms
1221 in 1242 in
1222 case E.projectSgn env {sgn = sgn, str = str, field = x} of 1243 case E.projectSgn env {sgn = sgn, str = str, field = x} of
1223 NONE => (sgnError env (UnboundSgn (loc, x)); 1244 NONE => (sgnError env (UnboundSgn (loc, x));
1224 sgnerror) 1245 (sgnerror, []))
1225 | SOME _ => (L'.SgnProj (n, ms, x), loc) 1246 | SOME _ => ((L'.SgnProj (n, ms, x), loc), [])
1226 end) 1247 end)
1227 1248
1228 1249
1229 fun selfify env {str, strs, sgn} = 1250 fun selfify env {str, strs, sgn} =
1230 case #1 (hnormSgn env sgn) of 1251 case #1 (hnormSgn env sgn) of
1440 end 1461 end
1441 1462
1442 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)) 1463 | _ => sgnError env (SgnWrongForm (sgn1, sgn2))
1443 1464
1444 1465
1445 fun elabDecl ((d, loc), env) = 1466 fun elabDecl denv ((d, loc), (env, gs)) =
1446 case d of 1467 case d of
1447 L.DCon (x, ko, c) => 1468 L.DCon (x, ko, c) =>
1448 let 1469 let
1449 val k' = case ko of 1470 val k' = case ko of
1450 NONE => kunif loc 1471 NONE => kunif loc
1451 | SOME k => elabKind k 1472 | SOME k => elabKind k
1452 1473
1453 val (c', ck) = elabCon env c 1474 val (c', ck, gs') = elabCon (env, denv) c
1454 val (env', n) = E.pushCNamed env x k' (SOME c') 1475 val (env', n) = E.pushCNamed env x k' (SOME c')
1455 in 1476 in
1456 checkKind env c' ck k'; 1477 checkKind env c' ck k';
1457 1478
1458 ([(L'.DCon (x, n, k', c'), loc)], env') 1479 ([(L'.DCon (x, n, k', c'), loc)], (env', gs' @ gs))
1459 end 1480 end
1460 | L.DVal (x, co, e) => 1481 | L.DVal (x, co, e) =>
1461 let 1482 let
1462 val (c', ck) = case co of 1483 val (c', ck, gs1) = case co of
1463 NONE => (cunif (loc, ktype), ktype) 1484 NONE => (cunif (loc, ktype), ktype, [])
1464 | SOME c => elabCon env c 1485 | SOME c => elabCon (env, denv) c
1465 1486
1466 val (e', et) = elabExp env e 1487 val (e', et, gs2) = elabExp (env, denv) e
1467 val (env', n) = E.pushENamed env x c' 1488 val (env', n) = E.pushENamed env x c'
1468 in 1489 in
1469 checkCon env e' et c'; 1490 checkCon env e' et c';
1470 1491
1471 ([(L'.DVal (x, n, c', e'), loc)], env') 1492 ([(L'.DVal (x, n, c', e'), loc)], (env', gs1 @ gs2 @ gs))
1472 end 1493 end
1473 1494
1474 | L.DSgn (x, sgn) => 1495 | L.DSgn (x, sgn) =>
1475 let 1496 let
1476 val sgn' = elabSgn env sgn 1497 val (sgn', gs') = elabSgn (env, denv) sgn
1477 val (env', n) = E.pushSgnNamed env x sgn' 1498 val (env', n) = E.pushSgnNamed env x sgn'
1478 in 1499 in
1479 ([(L'.DSgn (x, n, sgn'), loc)], env') 1500 ([(L'.DSgn (x, n, sgn'), loc)], (env', gs' @ gs))
1480 end 1501 end
1481 1502
1482 | L.DStr (x, sgno, str) => 1503 | L.DStr (x, sgno, str) =>
1483 let 1504 let
1484 val formal = Option.map (elabSgn env) sgno 1505 val formal = Option.map (elabSgn (env, denv)) sgno
1485 1506
1486 val (str', sgn') = 1507 val (str', sgn', gs') =
1487 case formal of 1508 case formal of
1488 NONE => 1509 NONE =>
1489 let 1510 let
1490 val (str', actual) = elabStr env str 1511 val (str', actual, ds) = elabStr (env, denv) str
1491 in 1512 in
1492 (str', selfifyAt env {str = str', sgn = actual}) 1513 (str', selfifyAt env {str = str', sgn = actual}, ds)
1493 end 1514 end
1494 | SOME formal => 1515 | SOME (formal, gs1) =>
1495 let 1516 let
1496 val str = 1517 val str =
1497 case #1 (hnormSgn env formal) of 1518 case #1 (hnormSgn env formal) of
1498 L'.SgnConst sgis => 1519 L'.SgnConst sgis =>
1499 (case #1 str of 1520 (case #1 str of
1525 end 1546 end
1526 end 1547 end
1527 | _ => str) 1548 | _ => str)
1528 | _ => str 1549 | _ => str
1529 1550
1530 val (str', actual) = elabStr env str 1551 val (str', actual, gs2) = elabStr (env, denv) str
1531 in 1552 in
1532 subSgn env actual formal; 1553 subSgn env actual formal;
1533 (str', formal) 1554 (str', formal, gs1 @ gs2)
1534 end 1555 end
1535 1556
1536 val (env', n) = E.pushStrNamed env x sgn' 1557 val (env', n) = E.pushStrNamed env x sgn'
1537 in 1558 in
1538 case #1 (hnormSgn env sgn') of 1559 case #1 (hnormSgn env sgn') of
1540 (case #1 str' of 1561 (case #1 str' of
1541 L'.StrFun _ => () 1562 L'.StrFun _ => ()
1542 | _ => strError env (FunctorRebind loc)) 1563 | _ => strError env (FunctorRebind loc))
1543 | _ => (); 1564 | _ => ();
1544 1565
1545 ([(L'.DStr (x, n, sgn', str'), loc)], env') 1566 ([(L'.DStr (x, n, sgn', str'), loc)], (env', gs' @ gs))
1546 end 1567 end
1547 1568
1548 | L.DFfiStr (x, sgn) => 1569 | L.DFfiStr (x, sgn) =>
1549 let 1570 let
1550 val sgn' = elabSgn env sgn 1571 val (sgn', gs') = elabSgn (env, denv) sgn
1551 1572
1552 val (env', n) = E.pushStrNamed env x sgn' 1573 val (env', n) = E.pushStrNamed env x sgn'
1553 in 1574 in
1554 ([(L'.DFfiStr (x, n, sgn'), loc)], env') 1575 ([(L'.DFfiStr (x, n, sgn'), loc)], (env', gs' @ gs))
1555 end 1576 end
1556 1577
1557 | L.DOpen (m, ms) => 1578 | L.DOpen (m, ms) =>
1558 case E.lookupStr env m of 1579 case E.lookupStr env m of
1559 NONE => (strError env (UnboundStr (loc, m)); 1580 NONE => (strError env (UnboundStr (loc, m));
1560 ([], env)) 1581 ([], (env, [])))
1561 | SOME (n, sgn) => 1582 | SOME (n, sgn) =>
1562 let 1583 let
1563 val (_, sgn) = foldl (fn (m, (str, sgn)) => 1584 val (_, sgn) = foldl (fn (m, (str, sgn)) =>
1564 case E.projectStr env {str = str, sgn = sgn, field = m} of 1585 case E.projectStr env {str = str, sgn = sgn, field = m} of
1565 NONE => (strError env (UnboundStr (loc, m)); 1586 NONE => (strError env (UnboundStr (loc, m));
1566 (strerror, sgnerror)) 1587 (strerror, sgnerror))
1567 | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) 1588 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
1568 ((L'.StrVar n, loc), sgn) ms 1589 ((L'.StrVar n, loc), sgn) ms
1590
1591 val (ds, env') = dopen env {str = n, strs = ms, sgn = sgn}
1569 in 1592 in
1570 dopen env {str = n, strs = ms, sgn = sgn} 1593 (ds, (env', []))
1571 end 1594 end
1572 1595
1573 and elabStr env (str, loc) = 1596 and elabStr (env, denv) (str, loc) =
1574 case str of 1597 case str of
1575 L.StrConst ds => 1598 L.StrConst ds =>
1576 let 1599 let
1577 val (ds', env') = ListUtil.foldlMapConcat elabDecl env ds 1600 val (ds', (env', gs)) = ListUtil.foldlMapConcat (elabDecl denv) (env, []) ds
1578 val sgis = map sgiOfDecl ds' 1601 val sgis = map sgiOfDecl ds'
1579 1602
1580 val (sgis, _, _, _, _) = 1603 val (sgis, _, _, _, _) =
1581 foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) => 1604 foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) =>
1582 case sgi of 1605 case sgi of
1632 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) 1655 ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs)
1633 end) 1656 end)
1634 1657
1635 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis 1658 ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis
1636 in 1659 in
1637 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc)) 1660 ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs)
1638 end 1661 end
1639 | L.StrVar x => 1662 | L.StrVar x =>
1640 (case E.lookupStr env x of 1663 (case E.lookupStr env x of
1641 NONE => 1664 NONE =>
1642 (strError env (UnboundStr (loc, x)); 1665 (strError env (UnboundStr (loc, x));
1643 (strerror, sgnerror)) 1666 (strerror, sgnerror, []))
1644 | SOME (n, sgn) => ((L'.StrVar n, loc), sgn)) 1667 | SOME (n, sgn) => ((L'.StrVar n, loc), sgn, []))
1645 | L.StrProj (str, x) => 1668 | L.StrProj (str, x) =>
1646 let 1669 let
1647 val (str', sgn) = elabStr env str 1670 val (str', sgn, gs) = elabStr (env, denv) str
1648 in 1671 in
1649 case E.projectStr env {str = str', sgn = sgn, field = x} of 1672 case E.projectStr env {str = str', sgn = sgn, field = x} of
1650 NONE => (strError env (UnboundStr (loc, x)); 1673 NONE => (strError env (UnboundStr (loc, x));
1651 (strerror, sgnerror)) 1674 (strerror, sgnerror, []))
1652 | SOME sgn => ((L'.StrProj (str', x), loc), sgn) 1675 | SOME sgn => ((L'.StrProj (str', x), loc), sgn, gs)
1653 end 1676 end
1654 | L.StrFun (m, dom, ranO, str) => 1677 | L.StrFun (m, dom, ranO, str) =>
1655 let 1678 let
1656 val dom' = elabSgn env dom 1679 val (dom', gs1) = elabSgn (env, denv) dom
1657 val (env', n) = E.pushStrNamed env m dom' 1680 val (env', n) = E.pushStrNamed env m dom'
1658 val (str', actual) = elabStr env' str 1681 val (str', actual, gs2) = elabStr (env', denv) str
1659 1682
1660 val formal = 1683 val (formal, gs3) =
1661 case ranO of 1684 case ranO of
1662 NONE => actual 1685 NONE => (actual, [])
1663 | SOME ran => 1686 | SOME ran =>
1664 let 1687 let
1665 val ran' = elabSgn env' ran 1688 val (ran', gs) = elabSgn (env', denv) ran
1666 in 1689 in
1667 subSgn env' actual ran'; 1690 subSgn env' actual ran';
1668 ran' 1691 (ran', gs)
1669 end 1692 end
1670 in 1693 in
1671 ((L'.StrFun (m, n, dom', formal, str'), loc), 1694 ((L'.StrFun (m, n, dom', formal, str'), loc),
1672 (L'.SgnFun (m, n, dom', formal), loc)) 1695 (L'.SgnFun (m, n, dom', formal), loc),
1696 gs1 @ gs2 @ gs3)
1673 end 1697 end
1674 | L.StrApp (str1, str2) => 1698 | L.StrApp (str1, str2) =>
1675 let 1699 let
1676 val (str1', sgn1) = elabStr env str1 1700 val (str1', sgn1, gs1) = elabStr (env, denv) str1
1677 val (str2', sgn2) = elabStr env str2 1701 val (str2', sgn2, gs2) = elabStr (env, denv) str2
1678 in 1702 in
1679 case #1 (hnormSgn env sgn1) of 1703 case #1 (hnormSgn env sgn1) of
1680 L'.SgnError => (strerror, sgnerror) 1704 L'.SgnError => (strerror, sgnerror, [])
1681 | L'.SgnFun (m, n, dom, ran) => 1705 | L'.SgnFun (m, n, dom, ran) =>
1682 (subSgn env sgn2 dom; 1706 (subSgn env sgn2 dom;
1683 case #1 (hnormSgn env ran) of 1707 case #1 (hnormSgn env ran) of
1684 L'.SgnError => (strerror, sgnerror) 1708 L'.SgnError => (strerror, sgnerror, [])
1685 | L'.SgnConst sgis => 1709 | L'.SgnConst sgis =>
1686 ((L'.StrApp (str1', str2'), loc), 1710 ((L'.StrApp (str1', str2'), loc),
1687 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc)) 1711 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc),
1712 gs1 @ gs2)
1688 | _ => raise Fail "Unable to hnormSgn in functor application") 1713 | _ => raise Fail "Unable to hnormSgn in functor application")
1689 | _ => (strError env (NotFunctor sgn1); 1714 | _ => (strError env (NotFunctor sgn1);
1690 (strerror, sgnerror)) 1715 (strerror, sgnerror, []))
1691 end 1716 end
1692 1717
1693 fun elabFile basis env file = 1718 fun elabFile basis env file =
1694 let 1719 let
1695 val sgn = elabSgn env (L.SgnConst basis, ErrorMsg.dummySpan) 1720 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan)
1721 val () = case gs of
1722 [] => ()
1723 | _ => raise Fail "Unresolved disjointness constraints in Basis"
1724
1696 val (env', basis_n) = E.pushStrNamed env "Basis" sgn 1725 val (env', basis_n) = E.pushStrNamed env "Basis" sgn
1697 1726
1698 val (ds, env') = dopen env' {str = basis_n, strs = [], sgn = sgn} 1727 val (ds, env') = dopen env' {str = basis_n, strs = [], sgn = sgn}
1699 1728
1700 fun discoverC r x = 1729 fun discoverC r x =
1705 1734
1706 val () = discoverC int "int" 1735 val () = discoverC int "int"
1707 val () = discoverC float "float" 1736 val () = discoverC float "float"
1708 val () = discoverC string "string" 1737 val () = discoverC string "string"
1709 1738
1710 fun elabDecl' (d, env) = 1739 fun elabDecl' (d, (env, gs)) =
1711 let 1740 let
1712 val () = resetKunif () 1741 val () = resetKunif ()
1713 val () = resetCunif () 1742 val () = resetCunif ()
1714 val (ds, env) = elabDecl (d, env) 1743 val (ds, (env, gs)) = elabDecl D.empty (d, (env, gs))
1715 in 1744 in
1716 if ErrorMsg.anyErrors () then 1745 if ErrorMsg.anyErrors () then
1717 () 1746 ()
1718 else ( 1747 else (
1719 if List.exists kunifsInDecl ds then 1748 if List.exists kunifsInDecl ds then
1725 NONE => () 1754 NONE => ()
1726 | SOME loc => 1755 | SOME loc =>
1727 declError env (CunifsRemain loc) 1756 declError env (CunifsRemain loc)
1728 ); 1757 );
1729 1758
1730 (ds, env) 1759 (ds, (env, gs))
1731 end 1760 end
1732 1761
1733 val (file, _) = ListUtil.foldlMapConcat elabDecl' env' file 1762 val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file
1734 in 1763 in
1764 app (fn (loc, env, denv, (c1, c2)) =>
1765 case D.prove env denv (c1, c2, loc) of
1766 [] => ()
1767 | _ =>
1768 (ErrorMsg.errorAt loc "Remaining constraint";
1769 eprefaces' [("Con 1", p_con env c1),
1770 ("Con 2", p_con env c2)])) gs;
1771
1735 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file 1772 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
1736 end 1773 end
1737 1774
1738 end 1775 end