Mercurial > urweb
changeset 218:a3413288cce1
Signature ascription for type classes
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sat, 16 Aug 2008 16:57:21 -0400 |
| parents | 56db662ebcfd |
| children | 5292c0113024 |
| files | src/elab_env.sml src/elaborate.sml tests/type_classMod2.lac |
| diffstat | 3 files changed, 53 insertions(+), 12 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab_env.sml Sat Aug 16 16:30:07 2008 -0400 +++ b/src/elab_env.sml Sat Aug 16 16:57:21 2008 -0400 @@ -700,23 +700,31 @@ case #1 (hnormSgn env sgn) of SgnConst sgis => let - val (classes, _, _) = - foldl (fn (sgi, (classes, newClasses, fmap)) => + val (classes, _, _, _) = + foldl (fn (sgi, (classes, newClasses, fmap, env)) => let fun found (x, n) = (CM.insert (classes, ClProj (m1, ms, x), empty_class), IM.insert (newClasses, n, x), - sgiSeek (#1 sgi, fmap)) + sgiSeek (#1 sgi, fmap), + env) - fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap)) + fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap), env) in case #1 sgi of SgiStr (x, _, sgn) => (enrichClasses env classes (m1, ms @ [x]) sgn, newClasses, - sgiSeek (#1 sgi, fmap)) + sgiSeek (#1 sgi, fmap), + env) + | SgiSgn (x, n, sgn) => + (classes, + newClasses, + fmap, + pushSgnNamedAs env x n sgn) + | SgiClassAbs xn => found xn | SgiClass (x, n, _) => found (x, n) | SgiVal (x, n, (CApp ((CNamed f, _), a), _)) => @@ -737,12 +745,13 @@ in (CM.insert (classes, cn, class), newClasses, - fmap) + fmap, + env) end) | SgiVal _ => default () | _ => default () end) - (classes, IM.empty, (IM.empty, IM.empty, IM.empty)) sgis + (classes, IM.empty, (IM.empty, IM.empty, IM.empty), env) sgis in classes end
--- a/src/elaborate.sml Sat Aug 16 16:30:07 2008 -0400 +++ b/src/elaborate.sml Sat Aug 16 16:57:21 2008 -0400 @@ -1913,11 +1913,12 @@ val (c', ck, gs') = elabCon (env, denv) c val (env', n) = E.pushENamed env x c' + val (c', gs'') = normClassConstraint (env, denv) c' in (unifyKinds ck ktype handle KUnify ue => strError env (NotType (ck, ue))); - ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) + ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs'' @ gs)) end | L.SgiStr (x, sgn) => @@ -2137,6 +2138,8 @@ (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) | (L'.SgiDatatype (x, n, xs, xncs), loc) => (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc) + | (L'.SgiClassAbs (x, n), loc) => + (L'.SgiClass (x, n, (L'.CModProj (str, strs, x), loc)), loc) | (L'.SgiStr (x, n, sgn), loc) => (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) | x => x) sgis), #2 sgn) @@ -2339,9 +2342,9 @@ found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc)) end | L'.SgiClassAbs (x', n1) => found (x', n1, - (L'.KArrow ((L'.KType, loc), - (L'.KType, loc)), loc), - NONE) + (L'.KArrow ((L'.KType, loc), + (L'.KType, loc)), loc), + NONE) | L'.SgiClass (x', n1, c) => found (x', n1, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), @@ -2592,7 +2595,16 @@ fun found (x', n1, c1) = if x = x' then let - fun good () = SOME (E.pushCNamedAs env x n2 k (SOME c2), denv) + fun good () = + let + val env = E.pushCNamedAs env x n2 k (SOME c2) + val env = if n1 = n2 then + env + else + E.pushCNamedAs env x n1 k (SOME c1) + in + SOME (env, denv) + end in (case unifyCons (env, denv) c1 c2 of [] => good () @@ -2823,6 +2835,8 @@ case d of L.DCon (x, _, _) => (SS.delete (needed, x) handle NotFound => needed) + | L.DClass (x, _) => (SS.delete (needed, x) + handle NotFound => needed) | L.DOpen _ => SS.empty | _ => needed) needed ds
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/type_classMod2.lac Sat Aug 16 16:57:21 2008 -0400 @@ -0,0 +1,18 @@ +signature S = sig + class c + val default : t :: Type -> c t -> t + + val string_c : c string + val int_c : c int +end + +structure M : S = struct + class c t = t + val default = fn t :: Type => fn v : c t => v + + val int_c : c int = 0 + val string_c : c string = "Hi" +end + +val hi = M.default [string] _ +val zero = M.default [int] _