diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-08-16 16:30:07 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-08-16 16:30:07 -0400 |
commit | 2c64a768d33ed6cbead84259a5cefae7d9c6f4e1 (patch) | |
tree | 32a4cb02d9f51c2fd821d54e5052030c0968aefe | |
parent | 402112549b47a76033fa575dc9f5e620ea214cc1 (diff) |
Fun with type classes and modules
-rw-r--r-- | src/elab_env.sml | 7 | ||||
-rw-r--r-- | src/elaborate.sml | 49 | ||||
-rw-r--r-- | tests/type_classMod.lac | 18 |
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] _ |