diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-03-26 14:37:31 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-03-26 14:37:31 -0400 |
| commit | ac2c539c79aeead75760f37285bd29169c0e8e6d (patch) | |
| tree | 34a0b58de26235bd0080d96af77e56fb0a92523e /src/elaborate.sml | |
| parent | f1a5c194580729f1db702d9eb28d3af414ea0a7e (diff) | |
Type class reductions, but no inclusions yet
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index daa6e004..81af6a79 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1480,6 +1480,14 @@ fun normClassConstraint env (c, loc) = in (L'.CApp (f, x), loc) end + | L'.TFun (c1, c2) => + let + val c1 = normClassConstraint env c1 + val c2 = normClassConstraint env c2 + in + (L'.TFun (c1, c2), loc) + end + | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc) | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c | _ => (c, loc) @@ -3045,7 +3053,7 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs)) = val () = checkCon env e' et c' - val c = normClassConstraint env c' + val c' = normClassConstraint env c' val (env', n) = E.pushENamed env x c' in (*prefaces "DVal" [("x", Print.PD.string x), @@ -3068,6 +3076,7 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs)) = val (c', _, gs1) = case co of NONE => (cunif (loc, ktype), ktype, []) | SOME c => elabCon (env, denv) c + val c' = normClassConstraint env c' in ((x, c', e), enD gs1 @ gs) end) gs vis |