# HG changeset patch # User Adam Chlipala # Date 1201383879 18000 # Node ID 38bf996e1c2e383285f2f574259687caeddb5150 # Parent 258261a538428380b9c2e92c6bb749885772c49f Check for leftover kind unifs diff -r 258261a53842 -r 38bf996e1c2e src/elab.sml --- a/src/elab.sml Sat Jan 26 16:02:47 2008 -0500 +++ b/src/elab.sml Sat Jan 26 16:44:39 2008 -0500 @@ -60,7 +60,7 @@ | CConcat of con * con | CError - | CUnif of string * con option ref + | CUnif of kind * string * con option ref withtype con = con' located diff -r 258261a53842 -r 38bf996e1c2e src/elab_print.sml --- a/src/elab_print.sml Sat Jan 26 16:02:47 2008 -0500 +++ b/src/elab_print.sml Sat Jan 26 16:44:39 2008 -0500 @@ -121,8 +121,10 @@ p_con env c2]) | CError => string "" - | CUnif (_, ref (SOME c)) => p_con' par env c - | CUnif (s, _) => string ("") + | CUnif (_, _, ref (SOME c)) => p_con' par env c + | CUnif (k, s, _) => box [string (""] and p_con env = p_con' false env diff -r 258261a53842 -r 38bf996e1c2e src/elab_util.sig --- a/src/elab_util.sig Sat Jan 26 16:02:47 2008 -0500 +++ b/src/elab_util.sig Sat Jan 26 16:44:39 2008 -0500 @@ -28,11 +28,19 @@ signature ELAB_UTIL = sig structure Kind : sig - val mapfold : (Elab.kind', 'state, 'abort) Search.mapfold_arg + val mapfold : (Elab.kind', 'state, 'abort) Search.mapfolder -> (Elab.kind, 'state, 'abort) Search.mapfolder val exists : (Elab.kind' -> bool) -> Elab.kind -> bool end +structure Con : sig + val mapfold : {kind : (Elab.kind', '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 + val declBinds : ElabEnv.env -> Elab.decl -> ElabEnv.env end diff -r 258261a53842 -r 38bf996e1c2e src/elab_util.sml --- a/src/elab_util.sml Sat Jan 26 16:02:47 2008 -0500 +++ b/src/elab_util.sml Sat Jan 26 16:44:39 2008 -0500 @@ -33,7 +33,7 @@ structure Kind = struct -fun mapfold (f : (Elab.kind', 'state, 'abort) S.mapfold_arg) : (Elab.kind, 'state, 'abort) S.mapfolder = +fun mapfold f = let fun mfk k acc = S.bindP (mfk' k acc, f) @@ -65,11 +65,98 @@ end fun exists f k = - case mapfold (fn (k, ()) => - if f k then - S.Return () - else - S.Continue (k, ())) k () of + case mapfold (fn k => fn () => + if f k then + S.Return () + else + S.Continue (k, ())) k () of + S.Return _ => true + | S.Continue _ => false + +end + +structure Con = struct + +fun mapfold {kind = fk, con = fc} = + let + val mfk = Kind.mapfold fk + + fun mfc c acc = + S.bindP (mfc' c acc, fc) + + and mfc' (cAll as (c, loc)) = + case c of + TFun (c1, c2) => + S.bind2 (mfc c1, + fn c1' => + S.map2 (mfc c2, + fn c2' => + (TFun (c1', c2'), loc))) + | TCFun (e, x, k, c) => + S.bind2 (mfk k, + fn k' => + S.map2 (mfc c, + fn c' => + (TCFun (e, x, k', c'), loc))) + | TRecord c => + S.map2 (mfc c, + fn c' => + (TRecord c', loc)) + + | CRel _ => S.return2 cAll + | CNamed _ => S.return2 cAll + | CApp (c1, c2) => + S.bind2 (mfc c1, + fn c1' => + S.map2 (mfc c2, + fn c2' => + (CApp (c1', c2'), loc))) + | CAbs (e, x, k, c) => + S.bind2 (mfk k, + fn k' => + S.map2 (mfc c, + fn c' => + (CAbs (e, x, k', c'), loc))) + + | CName _ => S.return2 cAll + + | CRecord (k, xcs) => + S.bind2 (mfk k, + fn k' => + S.map2 (ListUtil.mapfold (fn (x, c) => + S.bind2 (mfc x, + fn x' => + S.map2 (mfc c, + fn c' => + (x', c')))) + xcs, + fn xcs' => + (CRecord (k', xcs'), loc))) + | CConcat (c1, c2) => + S.bind2 (mfc c1, + fn c1' => + S.map2 (mfc c2, + fn c2' => + (CConcat (c1', c2'), loc))) + + | CError => S.return2 cAll + | CUnif (_, _, ref (SOME c)) => mfc' c + | CUnif _ => S.return2 cAll + in + mfc + end + +fun exists {kind, con} 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, ())} k () of S.Return _ => true | S.Continue _ => false diff -r 258261a53842 -r 38bf996e1c2e src/elaborate.sml --- a/src/elaborate.sml Sat Jan 26 16:02:47 2008 -0500 +++ b/src/elaborate.sml Sat Jan 26 16:44:39 2008 -0500 @@ -261,6 +261,28 @@ ((L'.CConcat (c1', c2'), loc), k) end +fun kunifsRemain k = + case k of + L'.KUnif (_, ref NONE) => true + | _ => false + +val kunifsInKind = U.Kind.exists kunifsRemain +val kunifsInCon = U.Con.exists {kind = kunifsRemain, + con = fn _ => false} + +datatype decl_error = + KunifsRemainKind of ErrorMsg.span * L'.kind + | KunifsRemainCon of ErrorMsg.span * L'.con + +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)]) + fun elabDecl env (d, loc) = (resetKunif (); case d of @@ -274,6 +296,17 @@ val (env', n) = E.pushCNamed env x k' in checkKind env c' ck k'; + + if kunifsInKind k' then + declError env (KunifsRemainKind (loc, k')) + else + (); + + if kunifsInCon c' then + declError env (KunifsRemainCon (loc, c')) + else + (); + (env', (L'.DCon (x, n, k', c'), loc)) end) diff -r 258261a53842 -r 38bf996e1c2e src/lacweb.grm --- a/src/lacweb.grm Sat Jan 26 16:02:47 2008 -0500 +++ b/src/lacweb.grm Sat Jan 26 16:44:39 2008 -0500 @@ -69,6 +69,7 @@ %nonassoc DARROW %nonassoc COLON +%nonassoc DCOLON TCOLON %right COMMA %right ARROW LARROW %right PLUSPLUS @@ -102,6 +103,8 @@ | FN SYMBOL kcolon kind DARROW cexp (CAbs (kcolon, SYMBOL, kind, cexp), s (FNleft, cexpright)) + | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, RPARENright)) + kcolon : DCOLON (Explicit) | TCOLON (Implicit) diff -r 258261a53842 -r 38bf996e1c2e src/list_util.sig --- a/src/list_util.sig Sat Jan 26 16:02:47 2008 -0500 +++ b/src/list_util.sig Sat Jan 26 16:44:39 2008 -0500 @@ -30,4 +30,7 @@ val mapfoldl : ('data1 * 'state -> 'state * 'data2) -> 'state -> 'data1 list -> 'state * 'data2 list + val mapfold : ('data, 'state, 'abort) Search.mapfolder + -> ('data list, 'state, 'abort) Search.mapfolder + end diff -r 258261a53842 -r 38bf996e1c2e src/list_util.sml --- a/src/list_util.sml Sat Jan 26 16:02:47 2008 -0500 +++ b/src/list_util.sml Sat Jan 26 16:44:39 2008 -0500 @@ -42,4 +42,22 @@ mf i [] end +structure S = Search + +fun mapfold f = + let + fun mf ls s = + case ls of + nil => S.Continue (nil, s) + | h :: t => + case f h s of + S.Return x => S.Return x + | S.Continue (h', s) => + case mf t s of + S.Return x => S.Return x + | S.Continue (t', s) => S.Continue (h' :: t', s) + in + mf + end + end diff -r 258261a53842 -r 38bf996e1c2e src/search.sig --- a/src/search.sig Sat Jan 26 16:02:47 2008 -0500 +++ b/src/search.sig Sat Jan 26 16:44:39 2008 -0500 @@ -31,9 +31,6 @@ Return of 'abort | Continue of 'state - type ('data, 'state, 'abort) mapfold_arg = - 'data * 'state -> ('data * 'state, 'abort) result - type ('data, 'state, 'abort) mapfolder = 'data -> 'state -> ('data * 'state, 'abort) result @@ -52,11 +49,11 @@ -> ('state2, 'abort) result val bind2 : ('state2 -> ('state1 * 'state2, 'abort) result) - * ('state1 -> 'state2 -> ('state1 * 'state2, 'abort) result) - -> ('state2 -> ('state1 * 'state2, 'abort) result) + * ('state1 -> 'state2 -> ('state1' * 'state2, 'abort) result) + -> ('state2 -> ('state1' * 'state2, 'abort) result) val bindP : (('state11 * 'state12) * 'state2, 'abort) result - * ('state11 * 'state2 -> ('state11 * 'state2, 'abort) result) + * ('state11 -> 'state2 -> ('state11 * 'state2, 'abort) result) -> (('state11 * 'state12) * 'state2, 'abort) result end diff -r 258261a53842 -r 38bf996e1c2e src/search.sml --- a/src/search.sml Sat Jan 26 16:02:47 2008 -0500 +++ b/src/search.sml Sat Jan 26 16:44:39 2008 -0500 @@ -62,7 +62,7 @@ fun bindP (r, f) = case r of Continue ((x, pos), acc) => - map (f (x, acc), + map (f x acc, fn (x', acc') => ((x', pos), acc')) | Return x => Return x diff -r 258261a53842 -r 38bf996e1c2e src/sources --- a/src/sources Sat Jan 26 16:02:47 2008 -0500 +++ b/src/sources Sat Jan 26 16:44:39 2008 -0500 @@ -1,3 +1,6 @@ +search.sig +search.sml + list_util.sig list_util.sml @@ -17,9 +20,6 @@ elab.sml -search.sig -search.sml - elab_util.sig elab_util.sml diff -r 258261a53842 -r 38bf996e1c2e tests/stuff.lac --- a/tests/stuff.lac Sat Jan 26 16:02:47 2008 -0500 +++ b/tests/stuff.lac Sat Jan 26 16:44:39 2008 -0500 @@ -10,3 +10,6 @@ con c7 = [A = c1, name = c2] con c8 = fn t :: Type => t + +con c9 = {} +con c10 = ([]) :: {Type}