diff options
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 200 |
1 files changed, 189 insertions, 11 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index ca950de2..e6044e49 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -32,6 +32,9 @@ structure L' = Elab structure E = ElabEnv structure U = ElabUtil +open Print +open ElabPrint + fun elabKind (k, loc) = case k of L.KType => (L'.KType, loc) @@ -48,34 +51,40 @@ fun occursKind r = U.Kind.exists (fn L'.KUnif (_, r') => r = r' | _ => false) -datatype unify_error = +datatype kunify_error = KOccursCheckFailed of L'.kind * L'.kind | KIncompatible of L'.kind * L'.kind -fun unifyError err = +exception KUnify' of kunify_error + +fun kunifyError err = case err of KOccursCheckFailed (k1, k2) => - ErrorMsg.errorAt (#2 k1) "Kind occurs check failed" + eprefaces "Kind occurs check failed" + [("Kind 1", p_kind k1), + ("Kind 2", p_kind k2)] | KIncompatible (k1, k2) => - ErrorMsg.errorAt (#2 k1) "Incompatible kinds" + eprefaces "Incompatible kinds" + [("Kind 1", p_kind k1), + ("Kind 2", p_kind k2)] -fun unifyKinds (k1All as (k1, pos)) (k2All as (k2, _)) = +fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) = let - fun err f = unifyError (f (k1All, k2All)) + fun err f = raise KUnify' (f (k1All, k2All)) in case (k1, k2) of (L'.KType, L'.KType) => () | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) => - (unifyKinds d1 d2; - unifyKinds r1 r2) + (unifyKinds' d1 d2; + unifyKinds' r1 r2) | (L'.KName, L'.KName) => () - | (L'.KRecord k1, L'.KRecord k2) => unifyKinds k1 k2 + | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2 | (L'.KError, _) => () | (_, L'.KError) => () - | (L'.KUnif (_, ref (SOME k1All)), _) => unifyKinds k1All k2All - | (_, L'.KUnif (_, ref (SOME k2All))) => unifyKinds k1All k2All + | (L'.KUnif (_, ref (SOME k1All)), _) => unifyKinds' k1All k2All + | (_, L'.KUnif (_, ref (SOME k2All))) => unifyKinds' k1All k2All | (L'.KUnif (_, r1), L'.KUnif (_, r2)) => if r1 = r2 then @@ -97,6 +106,175 @@ fun unifyKinds (k1All as (k1, pos)) (k2All as (k2, _)) = | _ => err KIncompatible end +exception KUnify of L'.kind * L'.kind * kunify_error + +fun unifyKinds k1 k2 = + unifyKinds' k1 k2 + handle KUnify' err => raise KUnify (k1, k2, err) + +datatype con_error = + UnboundCon of ErrorMsg.span * string + | WrongKind of L'.con * L'.kind * L'.kind * kunify_error + +fun conError err = + case err of + UnboundCon (loc, s) => + ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s) + | WrongKind (c, k1, k2, kerr) => + (ErrorMsg.errorAt (#2 c) "Wrong kind"; + eprefaces' [("Have", p_kind k1), + ("Need", p_kind k2)]; + kunifyError kerr) + +fun checkKind c k1 k2 = + unifyKinds k1 k2 + handle KUnify (k1, k2, err) => + conError (WrongKind (c, k1, k2, err)) + +val dummy = ErrorMsg.dummySpan + +val ktype = (L'.KType, dummy) +val kname = (L'.KName, dummy) + +val cerror = (L'.CError, dummy) +val kerror = (L'.KError, dummy) + +local + val count = ref 0 +in + +fun resetKunif () = count := 0 + +fun kunif () = + let + val n = !count + val s = if n <= 26 then + str (chr (ord #"A" + n)) + else + "U" ^ Int.toString (n - 26) + in + count := n + 1; + (L'.KUnif (s, ref NONE), dummy) + end + +end + +fun elabCon env (c, loc) = + case c of + L.CAnnot (c, k) => + let + val k' = elabKind k + val (c', ck) = elabCon env c + in + checkKind c' ck k'; + (c', k') + end + + | L.TFun (t1, t2) => + let + val (t1', k1) = elabCon env t1 + val (t2', k2) = elabCon env t2 + in + checkKind t1' k1 ktype; + checkKind t2' k2 ktype; + ((L'.TFun (t1', t2'), loc), ktype) + end + | L.TCFun (e, x, k, t) => + let + val e' = elabExplicitness e + val k' = elabKind k + val env' = E.pushCRel env x k' + val (t', tk) = elabCon env' t + in + checkKind t' tk ktype; + ((L'.TCFun (e', x, k', t'), loc), ktype) + end + | L.TRecord c => + let + val (c', ck) = elabCon env c + val k = (L'.KRecord ktype, loc) + in + checkKind c' ck k; + ((L'.TRecord c', loc), ktype) + end + + | L.CVar s => + (case E.lookupC env s of + E.CNotBound => + (conError (UnboundCon (loc, s)); + (cerror, kerror)) + | E.CRel (n, k) => + ((L'.CRel n, loc), k) + | E.CNamed (n, k) => + ((L'.CNamed n, loc), k)) + | L.CApp (c1, c2) => + let + val (c1', k1) = elabCon env c1 + val (c2', k2) = elabCon env c2 + val dom = kunif () + val ran = kunif () + in + checkKind c1' k1 (L'.KArrow (dom, ran), loc); + checkKind c2' k2 dom; + ((L'.CApp (c1', c2'), loc), ran) + end + | L.CAbs (e, x, k, t) => + let + val e' = elabExplicitness e + val k' = elabKind k + val env' = E.pushCRel env x k' + val (t', tk) = elabCon env' t + in + ((L'.CAbs (e', x, k', t'), loc), + (L'.KArrow (k', tk), loc)) + end + + | L.CName s => + ((L'.CName s, loc), kname) + + | L.CRecord xcs => + let + val k = kunif () + + val xcs' = map (fn (x, c) => + let + val (x', xk) = elabCon env x + val (c', ck) = elabCon env c + in + checkKind x' xk kname; + checkKind c' ck k; + (x', c') + end) xcs + in + ((L'.CRecord (k, xcs'), loc), k) + end + | L.CConcat (c1, c2) => + let + val (c1', k1) = elabCon env c1 + val (c2', k2) = elabCon env c2 + val ku = kunif () + val k = (L'.KRecord ku, loc) + in + checkKind c1' k1 k; + checkKind c2' k2 k; + ((L'.CConcat (c1', c2'), loc), k) + end + +fun elabDecl env (d, loc) = + case d of + L.DCon (x, ko, c) => + let + val k' = case ko of + NONE => kunif () + | SOME k => elabKind k + + val (c', ck) = elabCon env c + in + checkKind c' ck k'; + (E.pushCNamed env x k', + L'.DCon (x, k', c')) + end + fun elabFile _ = raise Fail "" end |