diff src/elaborate.sml @ 217:56db662ebcfd

Fun with type classes and modules
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 Aug 2008 16:30:07 -0400
parents 38b299373676
children a3413288cce1
line wrap: on
line diff
--- a/src/elaborate.sml	Sat Aug 16 15:58:25 2008 -0400
+++ b/src/elaborate.sml	Sat Aug 16 16:30:07 2008 -0400
@@ -1373,20 +1373,33 @@
         isTotal (combinedCoverage ps, t)
     end
 
-fun normClassConstraint envs c =
-    let
-        val ((c, loc), gs1) = hnormCon envs c
-    in
-        case c of
-            L'.CApp (f, x) =>
-            let
-                val (f, gs2) = hnormCon envs f
-                val (x, gs3) = hnormCon envs x
-            in
-                ((L'.CApp (f, x), loc), gs1 @ gs2 @ gs3)
-            end
-          | _ => ((c, loc), gs1)
-    end
+fun unmodCon env (c, loc) =
+    case c of
+        L'.CNamed n =>
+        (case E.lookupCNamed env n of
+             (_, _, SOME (c as (L'.CModProj _, _))) => unmodCon env c
+           | _ => (c, loc))
+      | L'.CModProj (m1, ms, x) =>
+        let
+            val (str, sgn) = E.chaseMpath env (m1, ms)
+        in
+            case E.projectCon env {str = str, sgn = sgn, field = x} of
+                NONE => raise Fail "unmodCon: Can't projectCon"
+              | SOME (_, SOME (c as (L'.CModProj _, _))) => unmodCon env c
+              | _ => (c, loc)
+        end
+      | _ => (c, loc)
+
+fun normClassConstraint envs (c, loc) =
+    case c of
+        L'.CApp (f, x) =>
+        let
+            val f = unmodCon (#1 envs) f
+            val (x, gs) = hnormCon envs x
+        in
+            ((L'.CApp (f, x), loc), gs)
+        end
+      | _ => ((c, loc), [])
 
 fun elabExp (env, denv) (eAll as (e, loc)) =
     let
@@ -2728,11 +2741,13 @@
                                   | SOME c => elabCon (env, denv) c
 
             val (e', et, gs2) = elabExp (env, denv) e
+            val gs3 = checkCon (env, denv) e' et c'
+            val (c', gs4) = normClassConstraint (env, denv) c'
             val (env', n) = E.pushENamed env x c'
-
-            val gs3 = checkCon (env, denv) e' et c'
         in
-            ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs))
+            (*prefaces "DVal" [("x", Print.PD.string x),
+                             ("c'", p_con env c')];*)
+            ([(L'.DVal (x, n, c', e'), loc)], (env', denv, gs1 @ gs2 @ gs3 @ gs4 @ gs))
         end
       | L.DValRec vis =>
         let