changeset 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
files src/elab_env.sml src/elaborate.sml tests/type_classMod.lac
diffstat 3 files changed, 56 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/src/elab_env.sml	Sat Aug 16 15:58:25 2008 -0400
+++ b/src/elab_env.sml	Sat Aug 16 16:30:07 2008 -0400
@@ -713,7 +713,11 @@
                               fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap))
                           in
                               case #1 sgi of
-                                  SgiClassAbs xn => found xn
+                                  SgiStr (x, _, sgn) =>
+                                  (enrichClasses env classes (m1, ms @ [x]) sgn,
+                                   newClasses,
+                                   sgiSeek (#1 sgi, fmap))
+                                | SgiClassAbs xn => found xn
                                 | SgiClass (x, n, _) => found (x, n)
                                 | SgiVal (x, n, (CApp ((CNamed f, _), a), _)) =>
                                   (case IM.find (newClasses, f) of
@@ -735,6 +739,7 @@
                                                 newClasses,
                                                 fmap)
                                            end)
+                                | SgiVal _ => default ()
                                 | _ => default ()
                           end)
                 (classes, IM.empty, (IM.empty, IM.empty, IM.empty)) sgis
--- 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
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tests/type_classMod.lac	Sat Aug 16 16:30:07 2008 -0400
@@ -0,0 +1,18 @@
+structure M = struct
+        structure N = struct
+                class c t = t
+                val string_c : c string = "Hi"
+        end
+end
+
+val c : t :: Type -> M.N.c t -> t =
+        fn t :: Type => fn pf : M.N.c t => pf
+val hi = c [string] _
+
+val bool_c : M.N.c bool = True
+val true = c [bool] _
+val hi = c [string] _
+
+con c = M.N.c
+val int_c : c int = 0
+val zero = c [int] _