Mercurial > urweb
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] _