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