summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-01-26 15:26:12 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-01-26 15:26:12 -0500
commite0a8e775a4c1e12debb2a3fa458007340685dc9d (patch)
treeed45e466a53dc18a1c772e2bdaad2e5f7ac8025b /src/elaborate.sml
parent485f8c00cc43334ba7bb429a830eb3b651ff92f6 (diff)
Elaborating cons and decls
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml200
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