summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
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 /src/elaborate.sml
parent402112549b47a76033fa575dc9f5e620ea214cc1 (diff)
Fun with type classes and modules
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml49
1 files changed, 32 insertions, 17 deletions
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