# HG changeset patch # User Adam Chlipala # Date 1206727143 14400 # Node ID dde5c52e5e5e9ee5dd133ad7676ba0676832ef21 # Parent 14b533dbe6ccc969c92a7291fc922518f94b76a7 Start of elaborating expressions diff -r 14b533dbe6cc -r dde5c52e5e5e src/elab_print.sig --- a/src/elab_print.sig Sat Jan 26 17:26:14 2008 -0500 +++ b/src/elab_print.sig Fri Mar 28 13:59:03 2008 -0400 @@ -31,6 +31,7 @@ val p_kind : Elab.kind Print.printer val p_explicitness : Elab.explicitness Print.printer val p_con : ElabEnv.env -> Elab.con Print.printer + val p_exp : ElabEnv.env -> Elab.exp Print.printer val p_decl : ElabEnv.env -> Elab.decl Print.printer val p_file : ElabEnv.env -> Elab.file Print.printer end diff -r 14b533dbe6cc -r dde5c52e5e5e src/elab_util.sig --- a/src/elab_util.sig Sat Jan 26 17:26:14 2008 -0500 +++ b/src/elab_util.sig Fri Mar 28 13:59:03 2008 -0400 @@ -35,12 +35,22 @@ structure Con : sig val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, - con : (Elab.con', 'state, 'abort) Search.mapfolder} + con : (Elab.con', 'state, 'abort) Search.mapfolder} -> (Elab.con, 'state, 'abort) Search.mapfolder val exists : {kind : Elab.kind' -> bool, con : Elab.con' -> bool} -> Elab.con -> bool end +structure Exp : sig + val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, + con : (Elab.con', 'state, 'abort) Search.mapfolder, + exp : (Elab.exp', 'state, 'abort) Search.mapfolder} + -> (Elab.exp, 'state, 'abort) Search.mapfolder + val exists : {kind : Elab.kind' -> bool, + con : Elab.con' -> bool, + exp : Elab.exp' -> bool} -> Elab.exp -> bool +end + val declBinds : ElabEnv.env -> Elab.decl -> ElabEnv.env end diff -r 14b533dbe6cc -r dde5c52e5e5e src/elab_util.sml --- a/src/elab_util.sml Sat Jan 26 17:26:14 2008 -0500 +++ b/src/elab_util.sml Fri Mar 28 13:59:03 2008 -0400 @@ -162,6 +162,72 @@ end +structure Exp = struct + +fun mapfold {kind = fk, con = fc, exp = fe} = + let + val mfk = Kind.mapfold fk + val mfc = Con.mapfold {kind = fk, con = fc} + + fun mfe e acc = + S.bindP (mfe' e acc, fe) + + and mfe' (eAll as (e, loc)) = + case e of + ERel _ => S.return2 eAll + | ENamed _ => S.return2 eAll + | EApp (e1, e2) => + S.bind2 (mfe e1, + fn e1' => + S.map2 (mfe e2, + fn e2' => + (EApp (e1', e2'), loc))) + | EAbs (x, t, e) => + S.bind2 (mfc t, + fn t' => + S.map2 (mfe e, + fn e' => + (EAbs (x, t', e'), loc))) + + | ECApp (e, c) => + S.bind2 (mfe e, + fn e' => + S.map2 (mfc c, + fn c' => + (ECApp (e', c'), loc))) + | ECAbs (expl, x, k, e) => + S.bind2 (mfk k, + fn k' => + S.map2 (mfe e, + fn e' => + (ECAbs (expl, x, k', e'), loc))) + + | EError => S.return2 eAll + in + mfe + end + +fun exists {kind, con, exp} k = + case mapfold {kind = fn k => fn () => + if kind k then + S.Return () + else + S.Continue (k, ()), + con = fn c => fn () => + if con c then + S.Return () + else + S.Continue (c, ()), + exp = fn e => fn () => + if exp e then + S.Return () + else + S.Continue (e, ())} k () of + S.Return _ => true + | S.Continue _ => false + +end + structure E = ElabEnv fun declBinds env (d, _) = diff -r 14b533dbe6cc -r dde5c52e5e5e src/elaborate.sml --- a/src/elaborate.sml Sat Jan 26 17:26:14 2008 -0500 +++ b/src/elaborate.sml Fri Mar 28 13:59:03 2008 -0400 @@ -139,6 +139,7 @@ val cerror = (L'.CError, dummy) val kerror = (L'.KError, dummy) +val eerror = (L'.EError, dummy) local val count = ref 0 @@ -160,6 +161,26 @@ end +local + val count = ref 0 +in + +fun resetCunif () = count := 0 + +fun cunif k = + 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'.CUnif (k, s, ref NONE), dummy) + end + +end + fun elabCon env (c, loc) = case c of L.CAnnot (c, k) => @@ -264,14 +285,224 @@ case k of L'.KUnif (_, ref NONE) => true | _ => false +fun cunifsRemain c = + case c of + L'.CUnif (_, _, ref NONE) => true + | _ => false val kunifsInKind = U.Kind.exists kunifsRemain val kunifsInCon = U.Con.exists {kind = kunifsRemain, con = fn _ => false} +val kunifsInExp = U.Exp.exists {kind = kunifsRemain, + con = fn _ => false, + exp = fn _ => false} + +val cunifsInCon = U.Con.exists {kind = fn _ => false, + con = cunifsRemain} +val cunifsInExp = U.Exp.exists {kind = fn _ => false, + con = cunifsRemain, + exp = fn _ => false} + +fun occursCon r = + U.Con.exists {kind = fn _ => false, + con = fn L'.CUnif (_, _, r') => r = r' + | _ => false} + +datatype cunify_error = + CKind of L'.kind * L'.kind * kunify_error + | COccursCheckFailed of L'.con * L'.con + | CIncompatible of L'.con * L'.con + | CExplicitness of L'.con * L'.con + +exception CUnify' of cunify_error + +fun cunifyError env err = + case err of + CKind (k1, k2, kerr) => + (eprefaces "Kind unification failure" + [("Kind 1", p_kind k1), + ("Kind 2", p_kind k2)]; + kunifyError kerr) + | COccursCheckFailed (c1, c2) => + eprefaces "Constructor occurs check failed" + [("Con 1", p_con env c1), + ("Con 2", p_con env c2)] + | CIncompatible (c1, c2) => + eprefaces "Incompatible constructors" + [("Con 1", p_con env c1), + ("Con 2", p_con env c2)] + | CExplicitness (c1, c2) => + eprefaces "Differing constructor function explicitness" + [("Con 1", p_con env c1), + ("Con 2", p_con env c2)] + +fun unifyCons' env (c1All as (c1, _)) (c2All as (c2, _)) = + let + fun err f = raise CUnify' (f (c1All, c2All)) + in + case (c1, c2) of + (L'.TFun (d1, r1), L'.TFun (d2, r2)) => + (unifyCons' env d1 d2; + unifyCons' env r1 r2) + | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => + if expl1 <> expl2 then + err CExplicitness + else + (unifyKinds d1 d2; + unifyCons' (E.pushCRel env x1 d1) r1 r2) + | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env r1 r2 + + | (L'.CRel n1, L'.CRel n2) => + if n1 = n2 then + () + else + err CIncompatible + | (L'.CNamed n1, L'.CNamed n2) => + if n1 = n2 then + () + else + err CIncompatible + + | (L'.CApp (d1, r1), L'.CApp (d2, r2)) => + (unifyCons' env d1 d2; + unifyCons' env r1 r2) + | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => + (unifyKinds k1 k2; + unifyCons' (E.pushCRel env x1 k1) c1 c2) + + | (L'.CName n1, L'.CName n2) => + if n1 = n2 then + () + else + err CIncompatible + + | (L'.CRecord (k1, rs1), L'.CRecord (k2, rs2)) => + (unifyKinds k1 k2; + ((ListPair.appEq (fn ((n1, v1), (n2, v2)) => + (unifyCons' env n1 n2; + unifyCons' env v1 v2)) (rs1, rs2)) + handle ListPair.UnequalLengths => err CIncompatible)) + | (L'.CConcat (d1, r1), L'.CConcat (d2, r2)) => + (unifyCons' env d1 d2; + unifyCons' env r1 r2) + + + | (L'.CError, _) => () + | (_, L'.CError) => () + + | (L'.CUnif (_, _, ref (SOME c1All)), _) => unifyCons' env c1All c2All + | (_, L'.CUnif (_, _, ref (SOME c2All))) => unifyCons' env c1All c2All + + | (L'.CUnif (k1, _, r1), L'.CUnif (k2, _, r2)) => + if r1 = r2 then + () + else + (unifyKinds k1 k2; + r1 := SOME c2All) + + | (L'.CUnif (_, _, r), _) => + if occursCon r c2All then + err COccursCheckFailed + else + r := SOME c2All + | (_, L'.CUnif (_, _, r)) => + if occursCon r c1All then + err COccursCheckFailed + else + r := SOME c1All + + | _ => err CIncompatible + end + +exception CUnify of L'.con * L'.con * cunify_error + +fun unifyCons env c1 c2 = + unifyCons' env c1 c2 + handle CUnify' err => raise CUnify (c1, c2, err) + | KUnify args => raise CUnify (c1, c2, CKind args) + +datatype exp_error = + UnboundExp of ErrorMsg.span * string + | Unify of L'.exp * L'.con * L'.con * cunify_error + +fun expError env err = + case err of + UnboundExp (loc, s) => + ErrorMsg.errorAt loc ("Unbound expression variable " ^ s) + | Unify (e, c1, c2, uerr) => + (ErrorMsg.errorAt (#2 e) "Unification failure"; + eprefaces' [("Expression", p_exp env e), + ("Have con", p_con env c1), + ("Need con", p_con env c2)]; + cunifyError env uerr) + +fun checkCon env e c1 c2 = + unifyCons env c1 c2 + handle CUnify (c1, c2, err) => + expError env (Unify (e, c1, c2, err)) + +fun elabExp env (e, loc) = + case e of + L.EAnnot (e, t) => + let + val (e', et) = elabExp env e + val (t', _) = elabCon env t + in + checkCon env e' et t'; + (e', t') + end + + | L.EVar s => + (case E.lookupE env s of + E.NotBound => + (expError env (UnboundExp (loc, s)); + (eerror, cerror)) + | E.Rel (n, t) => ((L'.ERel n, loc), t) + | E.Named (n, t) => ((L'.ENamed n, loc), t)) + | L.EApp (e1, e2) => + let + val (e1', t1) = elabExp env e1 + val (e2', t2) = elabExp env e2 + + val dom = cunif ktype + val ran = cunif ktype + val t = (L'.TFun (dom, ran), dummy) + in + checkCon env e1' t1 t; + checkCon env e2' t2 dom; + ((L'.EApp (e1', e2'), loc), ran) + end + | L.EAbs (x, to, e) => + let + val t' = case to of + NONE => cunif ktype + | SOME t => + let + val (t', tk) = elabCon env t + in + checkKind env t' tk ktype; + t' + end + val (e', et) = elabExp (E.pushERel env x t') e + in + ((L'.EAbs (x, t', e'), loc), + (L'.TFun (t', et), loc)) + end + | L.ECApp (e, c) => + let + val (e', et) = elabExp env e + val (c', ck) = elabCon env c + in + raise Fail "ECApp" + end + | L.ECAbs _ => raise Fail "ECAbs" datatype decl_error = KunifsRemainKind of ErrorMsg.span * L'.kind | KunifsRemainCon of ErrorMsg.span * L'.con + | KunifsRemainExp of ErrorMsg.span * L'.exp + | CunifsRemainCon of ErrorMsg.span * L'.con + | CunifsRemainExp of ErrorMsg.span * L'.exp fun declError env err = case err of @@ -281,6 +512,15 @@ | KunifsRemainCon (loc, c) => (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in constructor"; eprefaces' [("Constructor", p_con env c)]) + | KunifsRemainExp (loc, e) => + (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in expression"; + eprefaces' [("Expression", p_exp env e)]) + | CunifsRemainCon (loc, c) => + (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in constructor"; + eprefaces' [("Constructor", p_con env c)]) + | CunifsRemainExp (loc, e) => + (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in expression"; + eprefaces' [("Expression", p_exp env e)]) fun elabDecl env (d, loc) = (resetKunif (); @@ -308,6 +548,40 @@ (env', (L'.DCon (x, n, k', c'), loc)) + end + | L.DVal (x, co, e) => + let + val (c', ck) = case co of + NONE => (cunif ktype, ktype) + | SOME c => elabCon env c + + val (e', et) = elabExp env e + val (env', n) = E.pushENamed env x c' + in + checkCon env e' et c'; + + if kunifsInCon c' then + declError env (KunifsRemainCon (loc, c')) + else + (); + + if cunifsInCon c' then + declError env (CunifsRemainCon (loc, c')) + else + (); + + if kunifsInExp e' then + declError env (KunifsRemainExp (loc, e')) + else + (); + + if cunifsInExp e' then + declError env (CunifsRemainExp (loc, e')) + else + (); + + (env', + (L'.DVal (x, n, c', e'), loc)) end) fun elabFile env ds = diff -r 14b533dbe6cc -r dde5c52e5e5e src/sources --- a/src/sources Sat Jan 26 17:26:14 2008 -0500 +++ b/src/sources Fri Mar 28 13:59:03 2008 -0400 @@ -20,12 +20,12 @@ elab.sml +elab_env.sig +elab_env.sml + elab_util.sig elab_util.sml -elab_env.sig -elab_env.sml - elab_print.sig elab_print.sml