Mercurial > urweb
diff src/elaborate.sml @ 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 | 2b665e822e9a |
line wrap: on
line diff
--- 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