Mercurial > urweb

comparison src/elaborate.sml @ 207:cc68da3801bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Non-star SELECT
author Adam Chlipala <adamc@hcoop.net>
date Thu, 14 Aug 2008 18:35:08 -0400
parents cb8493759a7b
children 1487c712eb12
comparison
equal deleted inserted replaced
206:cb8493759a7b 207:cc68da3801bc
84 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) => 84 | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) =>
85 (unifyKinds' d1 d2; 85 (unifyKinds' d1 d2;
86 unifyKinds' r1 r2) 86 unifyKinds' r1 r2)
87 | (L'.KName, L'.KName) => () 87 | (L'.KName, L'.KName) => ()
88 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2 88 | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2
89 | (L'.KTuple ks1, L'.KTuple ks2) =>
90 ((ListPair.appEq (fn (k1, k2) => unifyKinds' k1 k2) (ks1, ks2))
91 handle ListPair.UnequalLengths => err KIncompatible)
89 92
90 | (L'.KError, _) => () 93 | (L'.KError, _) => ()
91 | (_, L'.KError) => () 94 | (_, L'.KError) => ()
92 95
93 | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All 96 | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All
123 UnboundCon of ErrorMsg.span * string 126 UnboundCon of ErrorMsg.span * string
124 | UnboundDatatype of ErrorMsg.span * string 127 | UnboundDatatype of ErrorMsg.span * string
125 | UnboundStrInCon of ErrorMsg.span * string 128 | UnboundStrInCon of ErrorMsg.span * string
126 | WrongKind of L'.con * L'.kind * L'.kind * kunify_error 129 | WrongKind of L'.con * L'.kind * L'.kind * kunify_error
127 | DuplicateField of ErrorMsg.span * string 130 | DuplicateField of ErrorMsg.span * string
131 | ProjBounds of L'.con * int
132 | ProjMismatch of L'.con * L'.kind
128 133
129 fun conError env err = 134 fun conError env err =
130 case err of 135 case err of
131 UnboundCon (loc, s) => 136 UnboundCon (loc, s) =>
132 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s) 137 ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
140 ("Have kind", p_kind k1), 145 ("Have kind", p_kind k1),
141 ("Need kind", p_kind k2)]; 146 ("Need kind", p_kind k2)];
142 kunifyError kerr) 147 kunifyError kerr)
143 | DuplicateField (loc, s) => 148 | DuplicateField (loc, s) =>
144 ErrorMsg.errorAt loc ("Duplicate record field " ^ s) 149 ErrorMsg.errorAt loc ("Duplicate record field " ^ s)
150 | ProjBounds (c, n) =>
151 (ErrorMsg.errorAt (#2 c) "Out of bounds constructor projection";
152 eprefaces' [("Constructor", p_con env c),
153 ("Index", Print.PD.string (Int.toString n))])
154 | ProjMismatch (c, k) =>
155 (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor";
156 eprefaces' [("Constructor", p_con env c),
157 ("Kind", p_kind k)])
145 158
146 fun checkKind env c k1 k2 = 159 fun checkKind env c k1 k2 =
147 unifyKinds k1 k2 160 unifyKinds k1 k2
148 handle KUnify (k1, k2, err) => 161 handle KUnify (k1, k2, err) =>
149 conError env (WrongKind (c, k1, k2, err)) 162 conError env (WrongKind (c, k1, k2, err))
210 L.KType => (L'.KType, loc) 223 L.KType => (L'.KType, loc)
211 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) 224 | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
212 | L.KName => (L'.KName, loc) 225 | L.KName => (L'.KName, loc)
213 | L.KRecord k => (L'.KRecord (elabKind k), loc) 226 | L.KRecord k => (L'.KRecord (elabKind k), loc)
214 | L.KUnit => (L'.KUnit, loc) 227 | L.KUnit => (L'.KUnit, loc)
228 | L.KTuple ks => (L'.KTuple (map elabKind ks), loc)
215 | L.KWild => kunif loc 229 | L.KWild => kunif loc
216 230
217 fun foldKind (dom, ran, loc)= 231 fun foldKind (dom, ran, loc)=
218 (L'.KArrow ((L'.KArrow ((L'.KName, loc), 232 (L'.KArrow ((L'.KArrow ((L'.KName, loc),
219 (L'.KArrow (dom, 233 (L'.KArrow (dom,
220 (L'.KArrow (ran, ran), loc)), loc)), loc), 234 (L'.KArrow (ran, ran), loc)), loc)), loc),
221 (L'.KArrow (ran, 235 (L'.KArrow (ran,
222 (L'.KArrow ((L'.KRecord dom, loc), 236 (L'.KArrow ((L'.KRecord dom, loc),
223 ran), loc)), loc)), loc) 237 ran), loc)), loc)), loc)
238
239 fun hnormKind (kAll as (k, _)) =
240 case k of
241 L'.KUnif (_, _, ref (SOME k)) => hnormKind k
242 | _ => kAll
224 243
225 fun elabCon (env, denv) (c, loc) = 244 fun elabCon (env, denv) (c, loc) =
226 case c of 245 case c of
227 L.CAnnot (c, k) => 246 L.CAnnot (c, k) =>
228 let 247 let
408 foldKind (dom, ran, loc), 427 foldKind (dom, ran, loc),
409 []) 428 [])
410 end 429 end
411 430
412 | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), []) 431 | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), [])
432
433 | L.CTuple cs =>
434 let
435 val (cs', ks, gs) = foldl (fn (c, (cs', ks, gs)) =>
436 let
437 val (c', k, gs') = elabCon (env, denv) c
438 in
439 (c' :: cs', k :: ks, gs' @ gs)
440 end) ([], [], []) cs
441 in
442 ((L'.CTuple (rev cs'), loc), (L'.KTuple (rev ks), loc), gs)
443 end
444 | L.CProj (c, n) =>
445 let
446 val (c', k, gs) = elabCon (env, denv) c
447 in
448 case hnormKind k of
449 (L'.KTuple ks, _) =>
450 if n <= 0 orelse n > length ks then
451 (conError env (ProjBounds (c', n));
452 (cerror, kerror, []))
453 else
454 ((L'.CProj (c', n), loc), List.nth (ks, n - 1), gs)
455 | k => (conError env (ProjMismatch (c', k));
456 (cerror, kerror, []))
457 end
413 458
414 | L.CWild k => 459 | L.CWild k =>
415 let 460 let
416 val k' = elabKind k 461 val k' = elabKind k
417 in 462 in
507 552
508 fun p_summary env s = p_con env (summaryToCon s) 553 fun p_summary env s = p_con env (summaryToCon s)
509 554
510 exception CUnify of L'.con * L'.con * cunify_error 555 exception CUnify of L'.con * L'.con * cunify_error
511 556
512 fun hnormKind (kAll as (k, _)) =
513 case k of
514 L'.KUnif (_, _, ref (SOME k)) => hnormKind k
515 | _ => kAll
516
517 fun kindof env (c, loc) = 557 fun kindof env (c, loc) =
518 case c of 558 case c of
519 L'.TFun _ => ktype 559 L'.TFun _ => ktype
520 | L'.TCFun _ => ktype 560 | L'.TCFun _ => ktype
521 | L'.TDisjoint _ => ktype 561 | L'.TDisjoint _ => ktype
550 | L'.CRecord (k, _) => (L'.KRecord k, loc) 590 | L'.CRecord (k, _) => (L'.KRecord k, loc)
551 | L'.CConcat (c, _) => kindof env c 591 | L'.CConcat (c, _) => kindof env c
552 | L'.CFold (dom, ran) => foldKind (dom, ran, loc) 592 | L'.CFold (dom, ran) => foldKind (dom, ran, loc)
553 593
554 | L'.CUnit => (L'.KUnit, loc) 594 | L'.CUnit => (L'.KUnit, loc)
595
596 | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc)
597 | L'.CProj (c, n) =>
598 (case hnormKind (kindof env c) of
599 (L'.KTuple ks, _) => List.nth (ks, n - 1)
600 | k => raise CUnify' (CKindof (k, c)))
555 601
556 | L'.CError => kerror 602 | L'.CError => kerror
557 | L'.CUnif (_, k, _, _) => k 603 | L'.CUnif (_, k, _, _) => k
558 604
559 val hnormCon = D.hnormCon 605 val hnormCon = D.hnormCon
860 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then 906 if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
861 [] 907 []
862 else 908 else
863 err CIncompatible 909 err CIncompatible
864 910
911 | (L'.CTuple cs1, L'.CTuple cs2) =>
912 ((ListPair.foldlEq (fn (c1, c2, gs) =>
913 let
914 val gs' = unifyCons' (env, denv) c1 c2
915 in
916 gs' @ gs
917 end) [] (cs1, cs2))
918 handle ListPair.UnequalLengths => err CIncompatible)
919 | (L'.CProj (c1, n1), L'.CProj (c2, n2)) =>
920 if n1 = n2 then
921 unifyCons' (env, denv) c1 c2
922 else
923 err CIncompatible
924
865 | (L'.CError, _) => [] 925 | (L'.CError, _) => []
866 | (_, L'.CError) => [] 926 | (_, L'.CError) => []
867 927
868 | (L'.CRecord _, _) => isRecord () 928 | (L'.CRecord _, _) => isRecord ()
869 | (_, L'.CRecord _) => isRecord () 929 | (_, L'.CRecord _) => isRecord ()
870 | (L'.CConcat _, _) => isRecord () 930 | (L'.CConcat _, _) => isRecord ()
871 | (_, L'.CConcat _) => isRecord () 931 | (_, L'.CConcat _) => isRecord ()
872 (*| (L'.CUnif (_, (L'.KRecord _, _), _, _), _) => isRecord ()
873 | (_, L'.CUnif (_, (L'.KRecord _, _), _, _)) => isRecord ()*)
874 932
875 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => 933 | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
876 if r1 = r2 then 934 if r1 = r2 then
877 [] 935 []
878 else 936 else
2906 fun elabFile basis env file = 2964 fun elabFile basis env file =
2907 let 2965 let
2908 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan) 2966 val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan)
2909 val () = case gs of 2967 val () = case gs of
2910 [] => () 2968 [] => ()
2911 | _ => raise Fail "Unresolved disjointness constraints in Basis" 2969 | _ => (app (fn (_, env, _, c1, c2) =>
2970 prefaces "Unresolved"
2971 [("c1", p_con env c1),
2972 ("c2", p_con env c2)]) gs;
2973 raise Fail "Unresolved disjointness constraints in Basis")
2912 2974
2913 val (env', basis_n) = E.pushStrNamed env "Basis" sgn 2975 val (env', basis_n) = E.pushStrNamed env "Basis" sgn
2914 2976
2915 val (ds, (env', _)) = dopen (env', D.empty) {str = basis_n, strs = [], sgn = sgn} 2977 val (ds, (env', _)) = dopen (env', D.empty) {str = basis_n, strs = [], sgn = sgn}
2916 2978