summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-08-16 16:30:07 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-08-16 16:30:07 -0400
commit2c64a768d33ed6cbead84259a5cefae7d9c6f4e1 (patch)
tree32a4cb02d9f51c2fd821d54e5052030c0968aefe
parent402112549b47a76033fa575dc9f5e620ea214cc1 (diff)
Fun with type classes and modules
-rw-r--r--src/elab_env.sml7
-rw-r--r--src/elaborate.sml49
-rw-r--r--tests/type_classMod.lac18
3 files changed, 56 insertions, 18 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 1b25749f..392fcf02 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -713,7 +713,11 @@ fun enrichClasses env classes (m1, ms) sgn =
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 @@ fun enrichClasses env classes (m1, ms) sgn =
newClasses,
fmap)
end)
+ | SgiVal _ => default ()
| _ => default ()
end)
(classes, IM.empty, (IM.empty, IM.empty, IM.empty)) sgis
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 2046432b..ebd46eca 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1373,20 +1373,33 @@ fun exhaustive (env, denv, t, ps) =
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 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
| SOME c => elabCon (env, denv) c
val (e', et, gs2) = elabExp (env, denv) e
- val (env', n) = E.pushENamed env x c'
-
val gs3 = checkCon (env, denv) e' et c'
+ val (c', gs4) = normClassConstraint (env, denv) c'
+ val (env', n) = E.pushENamed env x 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
diff --git a/tests/type_classMod.lac b/tests/type_classMod.lac
new file mode 100644
index 00000000..bcf03d1e
--- /dev/null
+++ b/tests/type_classMod.lac
@@ -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] _