Mercurial > urweb
changeset 76:522f4bd3955e
Broaden unification context
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 29 Jun 2008 10:39:43 -0400 |
| parents | 88ffb3d61817 |
| children | a1026ae076ea |
| files | src/elab.sml src/elab_print.sml src/elab_util.sig src/elab_util.sml src/elaborate.sml src/explify.sml tests/broad_unif.lac |
| diffstat | 7 files changed, 503 insertions(+), 299 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab.sml Thu Jun 26 12:35:26 2008 -0400 +++ b/src/elab.sml Sun Jun 29 10:39:43 2008 -0400 @@ -36,7 +36,7 @@ | KRecord of kind | KError - | KUnif of string * kind option ref + | KUnif of ErrorMsg.span * string * kind option ref withtype kind = kind' located @@ -62,7 +62,7 @@ | CFold of kind * kind | CError - | CUnif of kind * string * con option ref + | CUnif of ErrorMsg.span * kind * string * con option ref withtype con = con' located
--- a/src/elab_print.sml Thu Jun 26 12:35:26 2008 -0400 +++ b/src/elab_print.sml Sun Jun 29 10:39:43 2008 -0400 @@ -50,8 +50,8 @@ | KRecord k => box [string "{", p_kind k, string "}"] | KError => string "<ERROR>" - | KUnif (_, ref (SOME k)) => p_kind' par k - | KUnif (s, _) => string ("<UNIF:" ^ s ^ ">") + | KUnif (_, _, ref (SOME k)) => p_kind' par k + | KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">") and p_kind k = p_kind' false k @@ -156,10 +156,10 @@ | CFold _ => string "fold" | CError => string "<ERROR>" - | CUnif (_, _, ref (SOME c)) => p_con' par env c - | CUnif (k, s, _) => box [string ("<UNIF:" ^ s ^ "::"), - p_kind k, - string ">"] + | CUnif (_, _, _, ref (SOME c)) => p_con' par env c + | CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"), + p_kind k, + string ">"] and p_con env = p_con' false env
--- a/src/elab_util.sig Thu Jun 26 12:35:26 2008 -0400 +++ b/src/elab_util.sig Sun Jun 29 10:39:43 2008 -0400 @@ -107,4 +107,48 @@ end +structure Decl : sig + datatype binder = + RelC of string * Elab.kind + | NamedC of string * Elab.kind + | RelE of string * Elab.con + | NamedE of string * Elab.con + | Str of string * Elab.sgn + | Sgn of string * Elab.sgn + + val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, + con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, + exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB, + sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB, + sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB, + str : ('context, Elab.str', 'state, 'abort) Search.mapfolderB, + decl : ('context, Elab.decl', 'state, 'abort) Search.mapfolderB, + bind : 'context * binder -> 'context} + -> ('context, Elab.decl, 'state, 'abort) Search.mapfolderB + val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, + con : (Elab.con', 'state, 'abort) Search.mapfolder, + exp : (Elab.exp', 'state, 'abort) Search.mapfolder, + sgn_item : (Elab.sgn_item', 'state, 'abort) Search.mapfolder, + sgn : (Elab.sgn', 'state, 'abort) Search.mapfolder, + str : (Elab.str', 'state, 'abort) Search.mapfolder, + decl : (Elab.decl', 'state, 'abort) Search.mapfolder} + -> (Elab.decl, 'state, 'abort) Search.mapfolder + val exists : {kind : Elab.kind' -> bool, + con : Elab.con' -> bool, + exp : Elab.exp' -> bool, + sgn_item : Elab.sgn_item' -> bool, + sgn : Elab.sgn' -> bool, + str : Elab.str' -> bool, + decl : Elab.decl' -> bool} + -> Elab.decl -> bool + val search : {kind : Elab.kind' -> 'a option, + con : Elab.con' -> 'a option, + exp : Elab.exp' -> 'a option, + sgn_item : Elab.sgn_item' -> 'a option, + sgn : Elab.sgn' -> 'a option, + str : Elab.str' -> 'a option, + decl : Elab.decl' -> 'a option} + -> Elab.decl -> 'a option end + +end
--- a/src/elab_util.sml Thu Jun 26 12:35:26 2008 -0400 +++ b/src/elab_util.sml Sun Jun 29 10:39:43 2008 -0400 @@ -58,7 +58,7 @@ | KError => S.return2 kAll - | KUnif (_, ref (SOME k)) => mfk' k + | KUnif (_, _, ref (SOME k)) => mfk' k | KUnif _ => S.return2 kAll in mfk @@ -151,7 +151,7 @@ (CFold (k1', k2'), loc))) | CError => S.return2 cAll - | CUnif (_, _, ref (SOME c)) => mfc' ctx c + | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c | CUnif _ => S.return2 cAll in mfc @@ -417,4 +417,219 @@ end +structure Decl = struct + +datatype binder = + RelC of string * Elab.kind + | NamedC of string * Elab.kind + | RelE of string * Elab.con + | NamedE of string * Elab.con + | Str of string * Elab.sgn + | Sgn of string * Elab.sgn + +fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} = + let + val mfk = Kind.mapfold fk + + fun bind' (ctx, b) = + let + val b' = case b of + Con.Rel x => RelC x + | Con.Named x => NamedC x + in + bind (ctx, b') + end + val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'} + + fun bind' (ctx, b) = + let + val b' = case b of + Exp.RelC x => RelC x + | Exp.NamedC x => NamedC x + | Exp.RelE x => RelE x + | Exp.NamedE x => NamedE x + in + bind (ctx, b') + end + val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind'} + + fun bind' (ctx, b) = + let + val b' = case b of + Sgn.RelC x => RelC x + | Sgn.NamedC x => NamedC x + | Sgn.Sgn x => Sgn x + | Sgn.Str x => Str x + in + bind (ctx, b') + end + val mfsg = Sgn.mapfoldB {kind = fk, con = fc, sgn_item = fsgi, sgn = fsg, bind = bind'} + + fun mfst ctx str acc = + S.bindP (mfst' ctx str acc, fst ctx) + + and mfst' ctx (strAll as (str, loc)) = + case str of + StrConst ds => + S.map2 (ListUtil.mapfoldB (fn (ctx, d) => + (case #1 d of + DCon (x, _, k, _) => + bind (ctx, NamedC (x, k)) + | DVal (x, _, c, _) => + bind (ctx, NamedE (x, c)) + | DSgn (x, _, sgn) => + bind (ctx, Sgn (x, sgn)) + | DStr (x, _, sgn, _) => + bind (ctx, Str (x, sgn)) + | DFfiStr (x, _, sgn) => + bind (ctx, Str (x, sgn)), + mfd ctx d)) ctx ds, + fn ds' => (StrConst ds', loc)) + | StrVar _ => S.return2 strAll + | StrProj (str, x) => + S.map2 (mfst ctx str, + fn str' => + (StrProj (str', x), loc)) + | StrFun (x, n, sgn1, sgn2, str) => + S.bind2 (mfsg ctx sgn1, + fn sgn1' => + S.bind2 (mfsg ctx sgn2, + fn sgn2' => + S.map2 (mfst ctx str, + fn str' => + (StrFun (x, n, sgn1', sgn2', str'), loc)))) + | StrApp (str1, str2) => + S.bind2 (mfst ctx str1, + fn str1' => + S.map2 (mfst ctx str2, + fn str2' => + (StrApp (str1', str2'), loc))) + | StrError => S.return2 strAll + + and mfd ctx d acc = + S.bindP (mfd' ctx d acc, fd ctx) + + and mfd' ctx (dAll as (d, loc)) = + case d of + DCon (x, n, k, c) => + S.bind2 (mfk k, + fn k' => + S.map2 (mfc ctx c, + fn c' => + (DCon (x, n, k', c'), loc))) + | DVal (x, n, c, e) => + S.bind2 (mfc ctx c, + fn c' => + S.map2 (mfe ctx e, + fn e' => + (DVal (x, n, c', e'), loc))) + | DSgn (x, n, sgn) => + S.map2 (mfsg ctx sgn, + fn sgn' => + (DSgn (x, n, sgn'), loc)) + | DStr (x, n, sgn, str) => + S.bind2 (mfsg ctx sgn, + fn sgn' => + S.map2 (mfst ctx str, + fn str' => + (DStr (x, n, sgn', str'), loc))) + | DFfiStr (x, n, sgn) => + S.map2 (mfsg ctx sgn, + fn sgn' => + (DFfiStr (x, n, sgn'), loc)) + in + mfd + end + +fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} = + mapfoldB {kind = kind, + con = fn () => con, + exp = fn () => exp, + sgn_item = fn () => sgn_item, + sgn = fn () => sgn, + str = fn () => str, + decl = fn () => decl, + bind = fn ((), _) => ()} () + +fun exists {kind, con, exp, sgn_item, sgn, str, decl} 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, ()), + sgn_item = fn sgi => fn () => + if sgn_item sgi then + S.Return () + else + S.Continue (sgi, ()), + sgn = fn x => fn () => + if sgn x then + S.Return () + else + S.Continue (x, ()), + str = fn x => fn () => + if str x then + S.Return () + else + S.Continue (x, ()), + decl = fn x => fn () => + if decl x then + S.Return () + else + S.Continue (x, ())} k () of + S.Return _ => true + | S.Continue _ => false + +fun search {kind, con, exp, sgn_item, sgn, str, decl} k = + case mapfold {kind = fn x => fn () => + case kind x of + NONE => S.Continue (x, ()) + | SOME v => S.Return v, + + con = fn x => fn () => + case con x of + NONE => S.Continue (x, ()) + | SOME v => S.Return v, + + exp = fn x => fn () => + case exp x of + NONE => S.Continue (x, ()) + | SOME v => S.Return v, + + sgn_item = fn x => fn () => + case sgn_item x of + NONE => S.Continue (x, ()) + | SOME v => S.Return v, + + sgn = fn x => fn () => + case sgn x of + NONE => S.Continue (x, ()) + | SOME v => S.Return v, + + str = fn x => fn () => + case str x of + NONE => S.Continue (x, ()) + | SOME v => S.Return v, + + decl = fn x => fn () => + case decl x of + NONE => S.Continue (x, ()) + | SOME v => S.Return v + + } k () of + S.Return x => SOME x + | S.Continue _ => NONE + end + +end
--- a/src/elaborate.sml Thu Jun 26 12:35:26 2008 -0400 +++ b/src/elaborate.sml Sun Jun 29 10:39:43 2008 -0400 @@ -47,7 +47,7 @@ | L.Implicit => L'.Implicit fun occursKind r = - U.Kind.exists (fn L'.KUnif (_, r') => r = r' + U.Kind.exists (fn L'.KUnif (_, _, r') => r = r' | _ => false) datatype kunify_error = @@ -82,21 +82,21 @@ | (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)) => + | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) => if r1 = r2 then () else r1 := SOME k2All - | (L'.KUnif (_, r), _) => + | (L'.KUnif (_, _, r), _) => if occursKind r k2All then err KOccursCheckFailed else r := SOME k2All - | (_, L'.KUnif (_, r)) => + | (_, L'.KUnif (_, _, r)) => if occursKind r k1All then err KOccursCheckFailed else @@ -159,7 +159,7 @@ fun resetKunif () = count := 0 -fun kunif () = +fun kunif loc = let val n = !count val s = if n <= 26 then @@ -168,7 +168,7 @@ "U" ^ Int.toString (n - 26) in count := n + 1; - (L'.KUnif (s, ref NONE), dummy) + (L'.KUnif (loc, s, ref NONE), dummy) end end @@ -179,7 +179,7 @@ fun resetCunif () = count := 0 -fun cunif k = +fun cunif (loc, k) = let val n = !count val s = if n <= 26 then @@ -188,7 +188,7 @@ "U" ^ Int.toString (n - 26) in count := n + 1; - (L'.CUnif (k, s, ref NONE), dummy) + (L'.CUnif (loc, k, s, ref NONE), dummy) end end @@ -199,7 +199,7 @@ | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) | L.KName => (L'.KName, loc) | L.KRecord k => (L'.KRecord (elabKind k), loc) - | L.KWild => kunif () + | L.KWild => kunif loc fun foldKind (dom, ran, loc)= (L'.KArrow ((L'.KArrow ((L'.KName, loc), @@ -282,8 +282,8 @@ let val (c1', k1) = elabCon env c1 val (c2', k2) = elabCon env c2 - val dom = kunif () - val ran = kunif () + val dom = kunif loc + val ran = kunif loc in checkKind env c1' k1 (L'.KArrow (dom, ran), loc); checkKind env c2' k2 dom; @@ -292,7 +292,7 @@ | L.CAbs (x, ko, t) => let val k' = case ko of - NONE => kunif () + NONE => kunif loc | SOME k => elabKind k val env' = E.pushCRel env x k' val (t', tk) = elabCon env' t @@ -306,7 +306,7 @@ | L.CRecord xcs => let - val k = kunif () + val k = kunif loc val xcs' = map (fn (x, c) => let @@ -327,7 +327,7 @@ let val (c1', k1) = elabCon env c1 val (c2', k2) = elabCon env c2 - val ku = kunif () + val ku = kunif loc val k = (L'.KRecord ku, loc) in checkKind env c1' k1 k; @@ -336,8 +336,8 @@ end | L.CFold => let - val dom = kunif () - val ran = kunif () + val dom = kunif loc + val ran = kunif loc in ((L'.CFold (dom, ran), loc), foldKind (dom, ran, loc)) @@ -347,34 +347,37 @@ let val k' = elabKind k in - (cunif k', k') + (cunif (loc, k'), k') end fun kunifsRemain k = case k of - L'.KUnif (_, ref NONE) => true + L'.KUnif (_, _, ref NONE) => true | _ => false fun cunifsRemain c = case c of - L'.CUnif (_, _, ref NONE) => true - | _ => false + L'.CUnif (loc, _, _, ref NONE) => SOME loc + | _ => NONE -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 kunifsInDecl = U.Decl.exists {kind = kunifsRemain, + con = fn _ => false, + exp = fn _ => false, + sgn_item = fn _ => false, + sgn = fn _ => false, + str = fn _ => false, + decl = 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} +val cunifsInDecl = U.Decl.search {kind = fn _ => NONE, + con = cunifsRemain, + exp = fn _ => NONE, + sgn_item = fn _ => NONE, + sgn = fn _ => NONE, + str = fn _ => NONE, + decl = fn _ => NONE} fun occursCon r = U.Con.exists {kind = fn _ => false, - con = fn L'.CUnif (_, _, r') => r = r' + con = fn L'.CUnif (_, _, _, r') => r = r' | _ => false} datatype cunify_error = @@ -461,7 +464,7 @@ fun hnormKind (kAll as (k, _)) = case k of - L'.KUnif (_, ref (SOME k)) => hnormKind k + L'.KUnif (_, _, ref (SOME k)) => hnormKind k | _ => kAll fun kindof env (c, loc) = @@ -500,7 +503,7 @@ | L'.CFold (dom, ran) => foldKind (dom, ran, loc) | L'.CError => kerror - | L'.CUnif (k, _, _) => k + | L'.CUnif (_, k, _, _) => k fun unifyRecordCons env (c1, c2) = let @@ -523,8 +526,8 @@ unifs = #unifs s1 @ #unifs s2, others = #others s1 @ #others s2} end - | (L'.CUnif (_, _, ref (SOME c)), _) => recordSummary env c - | c' as (L'.CUnif (_, _, r), _) => {fields = [], unifs = [(c', r)], others = []} + | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary env c + | c' as (L'.CUnif (_, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []} | c' => {fields = [], unifs = [], others = [c']} and consEq env (c1, c2) = @@ -577,7 +580,7 @@ | (_, _, (_, r) :: rest) => let val r' = ref NONE - val cr' = (L'.CUnif (k, "recd", r'), dummy) + val cr' = (L'.CUnif (dummy, k, "recd", r'), dummy) val prefix = case (fs, others) of ([], other :: others) => @@ -626,7 +629,7 @@ and hnormCon env (cAll as (c, loc)) = case c of - L'.CUnif (_, _, ref (SOME c)) => hnormCon env c + L'.CUnif (_, _, _, ref (SOME c)) => hnormCon env c | L'.CNamed xn => (case E.lookupCNamed env xn of @@ -758,22 +761,22 @@ | (L'.CError, _) => () | (_, L'.CError) => () - | (L'.CUnif (_, _, ref (SOME c1All)), _) => unifyCons' env c1All c2All - | (_, L'.CUnif (_, _, ref (SOME c2All))) => unifyCons' env c1All c2All + | (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)) => + | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => if r1 = r2 then () else (unifyKinds k1 k2; r1 := SOME c2All) - | (L'.CUnif (_, _, r), _) => + | (L'.CUnif (_, _, _, r), _) => if occursCon r c2All then err COccursCheckFailed else r := SOME c2All - | (_, L'.CUnif (_, _, r)) => + | (_, L'.CUnif (_, _, _, r)) => if occursCon r c1All then err COccursCheckFailed else @@ -898,7 +901,7 @@ case hnormCon env t of (L'.TCFun (L'.Implicit, x, k, t'), _) => let - val u = cunif k + val u = cunif (loc, k) in unravel (subConInCon (0, u) t', (L'.ECApp (e, u), loc)) @@ -954,8 +957,8 @@ val (e1', t1) = elabHead env e1' t1 val (e2', t2) = elabExp env e2 - val dom = cunif ktype - val ran = cunif ktype + val dom = cunif (loc, ktype) + val ran = cunif (loc, ktype) val t = (L'.TFun (dom, ran), dummy) in checkCon env e1' t1 t; @@ -965,7 +968,7 @@ | L.EAbs (x, to, e) => let val t' = case to of - NONE => cunif ktype + NONE => cunif (loc, ktype) | SOME t => let val (t', tk) = elabCon env t @@ -1034,8 +1037,8 @@ val (e', et) = elabExp env e val (c', ck) = elabCon env c - val ft = cunif ktype - val rest = cunif ktype_record + val ft = cunif (loc, ktype) + val rest = cunif (loc, ktype_record) in checkKind env c' ck kname; checkCon env e' et (L'.TRecord (L'.CConcat ((L'.CRecord (ktype, [(c', ft)]), loc), rest), loc), loc); @@ -1044,36 +1047,22 @@ | L.EFold => let - val dom = kunif () + val dom = kunif loc in ((L'.EFold dom, loc), foldType (dom, loc)) end 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 + KunifsRemain of ErrorMsg.span + | CunifsRemain of ErrorMsg.span fun declError env err = case err of - KunifsRemainKind (loc, k) => - (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in kind"; - eprefaces' [("Kind", p_kind k)]) - | 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)]) + KunifsRemain loc => + ErrorMsg.errorAt loc "Some kind unification variables are undetermined in declaration" + | CunifsRemain loc => + ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in declaration" datatype sgn_error = UnboundSgn of ErrorMsg.span * string @@ -1164,107 +1153,68 @@ val hnormSgn = E.hnormSgn fun elabSgn_item ((sgi, loc), env) = - let - - in - resetKunif (); - resetCunif (); - case sgi of - L.SgiConAbs (x, k) => - let - val k' = elabKind k + case sgi of + L.SgiConAbs (x, k) => + let + val k' = elabKind k - val (env', n) = E.pushCNamed env x k' NONE - in - if ErrorMsg.anyErrors () then - () - else ( - if kunifsInKind k' then - declError env (KunifsRemainKind (loc, k')) - else - () - ); + val (env', n) = E.pushCNamed env x k' NONE + in + ([(L'.SgiConAbs (x, n, k'), loc)], env') + end - ([(L'.SgiConAbs (x, n, k'), loc)], env') - end + | L.SgiCon (x, ko, c) => + let + val k' = case ko of + NONE => kunif loc + | SOME k => elabKind k - | L.SgiCon (x, ko, c) => - let - val k' = case ko of - NONE => kunif () - | SOME k => elabKind k + val (c', ck) = elabCon env c + val (env', n) = E.pushCNamed env x k' (SOME c') + in + checkKind env c' ck k'; - val (c', ck) = elabCon env c - val (env', n) = E.pushCNamed env x k' (SOME c') - in - checkKind env c' ck k'; + ([(L'.SgiCon (x, n, k', c'), loc)], env') + end - if ErrorMsg.anyErrors () then - () - else ( - if kunifsInKind k' then - declError env (KunifsRemainKind (loc, k')) - else - (); + | L.SgiVal (x, c) => + let + val (c', ck) = elabCon env c - if kunifsInCon c' then - declError env (KunifsRemainCon (loc, c')) - else - () - ); + val (env', n) = E.pushENamed env x c' + in + (unifyKinds ck ktype + handle KUnify ue => strError env (NotType (ck, ue))); - ([(L'.SgiCon (x, n, k', c'), loc)], env') - end + ([(L'.SgiVal (x, n, c'), loc)], env') + end - | L.SgiVal (x, c) => - let - val (c', ck) = elabCon env c + | L.SgiStr (x, sgn) => + let + val sgn' = elabSgn env sgn + val (env', n) = E.pushStrNamed env x sgn' + in + ([(L'.SgiStr (x, n, sgn'), loc)], env') + end - val (env', n) = E.pushENamed env x c' - in - (unifyKinds ck ktype - handle KUnify ue => strError env (NotType (ck, ue))); + | L.SgiSgn (x, sgn) => + let + val sgn' = elabSgn env sgn + val (env', n) = E.pushSgnNamed env x sgn' + in + ([(L'.SgiSgn (x, n, sgn'), loc)], env') + end - if ErrorMsg.anyErrors () then - () - else ( - if kunifsInCon c' then - declError env (KunifsRemainCon (loc, c')) - else - () - ); - - ([(L'.SgiVal (x, n, c'), loc)], env') - end - - | L.SgiStr (x, sgn) => - let - val sgn' = elabSgn env sgn - val (env', n) = E.pushStrNamed env x sgn' - in - ([(L'.SgiStr (x, n, sgn'), loc)], env') - end - - | L.SgiSgn (x, sgn) => - let - val sgn' = elabSgn env sgn - val (env', n) = E.pushSgnNamed env x sgn' - in - ([(L'.SgiSgn (x, n, sgn'), loc)], env') - end - - | L.SgiInclude sgn => - let - val sgn' = elabSgn env sgn - in - case #1 (hnormSgn env sgn') of - L'.SgnConst sgis => - (sgis, foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis) - | _ => (sgnError env (NotIncludable sgn'); - ([], env)) - end - - end + | L.SgiInclude sgn => + let + val sgn' = elabSgn env sgn + in + case #1 (hnormSgn env sgn') of + L'.SgnConst sgis => + (sgis, foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis) + | _ => (sgnError env (NotIncludable sgn'); + ([], env)) + end and elabSgn env (sgn, loc) = case sgn of @@ -1580,132 +1530,89 @@ fun elabDecl ((d, loc), env) = - let - - in - resetKunif (); - resetCunif (); - case d of - L.DCon (x, ko, c) => + case d of + L.DCon (x, ko, c) => + let + val k' = case ko of + NONE => kunif loc + | SOME k => elabKind k + + val (c', ck) = elabCon env c + val (env', n) = E.pushCNamed env x k' (SOME c') + in + checkKind env c' ck k'; + + ([(L'.DCon (x, n, k', c'), loc)], env') + end + | L.DVal (x, co, e) => + let + val (c', ck) = case co of + NONE => (cunif (loc, 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'; + + ([(L'.DVal (x, n, c', e'), loc)], env') + end + + | L.DSgn (x, sgn) => + let + val sgn' = elabSgn env sgn + val (env', n) = E.pushSgnNamed env x sgn' + in + ([(L'.DSgn (x, n, sgn'), loc)], env') + end + + | L.DStr (x, sgno, str) => + let + val formal = Option.map (elabSgn env) sgno + val (str', actual) = elabStr env str + + val sgn' = case formal of + NONE => selfifyAt env {str = str', sgn = actual} + | SOME formal => + (subSgn env actual formal; + formal) + + val (env', n) = E.pushStrNamed env x sgn' + in + case #1 (hnormSgn env sgn') of + L'.SgnFun _ => + (case #1 str' of + L'.StrFun _ => () + | _ => strError env (FunctorRebind loc)) + | _ => (); + + ([(L'.DStr (x, n, sgn', str'), loc)], env') + end + + | L.DFfiStr (x, sgn) => + let + val sgn' = elabSgn env sgn + + val (env', n) = E.pushStrNamed env x sgn' + in + ([(L'.DFfiStr (x, n, sgn'), loc)], env') + end + + | L.DOpen (m, ms) => + case E.lookupStr env m of + NONE => (strError env (UnboundStr (loc, m)); + ([], env)) + | SOME (n, sgn) => let - val k' = case ko of - NONE => kunif () - | SOME k => elabKind k - - val (c', ck) = elabCon env c - val (env', n) = E.pushCNamed env x k' (SOME c') + val (_, sgn) = foldl (fn (m, (str, sgn)) => + case E.projectStr env {str = str, sgn = sgn, field = m} of + NONE => (strError env (UnboundStr (loc, m)); + (strerror, sgnerror)) + | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) + ((L'.StrVar n, loc), sgn) ms in - checkKind env c' ck k'; - - if ErrorMsg.anyErrors () then - () - else ( - if kunifsInKind k' then - declError env (KunifsRemainKind (loc, k')) - else - (); - - if kunifsInCon c' then - declError env (KunifsRemainCon (loc, c')) - else - () - ); - - ([(L'.DCon (x, n, k', c'), loc)], env') + dopen env {str = n, strs = ms, sgn = sgn} 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 ErrorMsg.anyErrors () then - () - else ( - 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 - ()); - - ([(L'.DVal (x, n, c', e'), loc)], env') - end - - | L.DSgn (x, sgn) => - let - val sgn' = elabSgn env sgn - val (env', n) = E.pushSgnNamed env x sgn' - in - ([(L'.DSgn (x, n, sgn'), loc)], env') - end - - | L.DStr (x, sgno, str) => - let - val formal = Option.map (elabSgn env) sgno - val (str', actual) = elabStr env str - - val sgn' = case formal of - NONE => selfifyAt env {str = str', sgn = actual} - | SOME formal => - (subSgn env actual formal; - formal) - - val (env', n) = E.pushStrNamed env x sgn' - in - case #1 (hnormSgn env sgn') of - L'.SgnFun _ => - (case #1 str' of - L'.StrFun _ => () - | _ => strError env (FunctorRebind loc)) - | _ => (); - - ([(L'.DStr (x, n, sgn', str'), loc)], env') - end - - | L.DFfiStr (x, sgn) => - let - val sgn' = elabSgn env sgn - - val (env', n) = E.pushStrNamed env x sgn' - in - ([(L'.DFfiStr (x, n, sgn'), loc)], env') - end - - | L.DOpen (m, ms) => - (case E.lookupStr env m of - NONE => (strError env (UnboundStr (loc, m)); - ([], env)) - | SOME (n, sgn) => - let - val (_, sgn) = foldl (fn (m, (str, sgn)) => - case E.projectStr env {str = str, sgn = sgn, field = m} of - NONE => (strError env (UnboundStr (loc, m)); - (strerror, sgnerror)) - | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) - ((L'.StrVar n, loc), sgn) ms - in - dopen env {str = n, strs = ms, sgn = sgn} - end) - end and elabStr env (str, loc) = case str of @@ -1844,7 +1751,30 @@ val () = discoverC float "float" val () = discoverC string "string" - val (file, _) = ListUtil.foldlMapConcat elabDecl env' file + fun elabDecl' (d, env) = + let + val () = resetKunif () + val () = resetCunif () + val (ds, env) = elabDecl (d, env) + in + if ErrorMsg.anyErrors () then + () + else ( + if List.exists kunifsInDecl ds then + declError env (KunifsRemain (#2 d)) + else + (); + + case ListUtil.search cunifsInDecl ds of + NONE => () + | SOME loc => + declError env (CunifsRemain loc) + ); + + (ds, env) + end + + val (file, _) = ListUtil.foldlMapConcat elabDecl' env' file in (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file end
--- a/src/explify.sml Thu Jun 26 12:35:26 2008 -0400 +++ b/src/explify.sml Sun Jun 29 10:39:43 2008 -0400 @@ -39,7 +39,7 @@ | L.KRecord k => (L'.KRecord (explifyKind k), loc) | L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc) - | L.KUnif (_, ref (SOME k)) => explifyKind k + | L.KUnif (_, _, ref (SOME k)) => explifyKind k | L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc) fun explifyCon (c, loc) = @@ -62,7 +62,7 @@ | L.CFold (dom, ran) => (L'.CFold (explifyKind dom, explifyKind ran), loc) | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc) - | L.CUnif (_, _, ref (SOME c)) => explifyCon c + | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc) fun explifyExp (e, loc) =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/broad_unif.lac Sun Jun 29 10:39:43 2008 -0400 @@ -0,0 +1,15 @@ +structure M = struct + type t = int + val f = fn x => x + val y = f 0 +end + +signature S = sig + type t + val f : t -> t +end + +structure M : S = struct + type t = int + val f = fn x => x +end