Mercurial > urweb

comparison src/elaborate.sml @ 674:fab5998b840e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Type class reductions, but no inclusions yet
author Adam Chlipala <adamc@hcoop.net>
date Thu, 26 Mar 2009 14:37:31 -0400
parents ae374df5ccbd
children 70cbdcf5989b
comparison
equal deleted inserted replaced
673:a8effb6159c2 674:fab5998b840e
1478 val f = unmodCon env f 1478 val f = unmodCon env f
1479 val x = normClassKey env x 1479 val x = normClassKey env x
1480 in 1480 in
1481 (L'.CApp (f, x), loc) 1481 (L'.CApp (f, x), loc)
1482 end 1482 end
1483 | L'.TFun (c1, c2) =>
1484 let
1485 val c1 = normClassConstraint env c1
1486 val c2 = normClassConstraint env c2
1487 in
1488 (L'.TFun (c1, c2), loc)
1489 end
1490 | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc)
1483 | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c 1491 | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c
1484 | _ => (c, loc) 1492 | _ => (c, loc)
1485 1493
1486 fun elabExp (env, denv) (eAll as (e, loc)) = 1494 fun elabExp (env, denv) (eAll as (e, loc)) =
1487 let 1495 let
3043 3051
3044 val (e', et, gs2) = elabExp (env, denv) e 3052 val (e', et, gs2) = elabExp (env, denv) e
3045 3053
3046 val () = checkCon env e' et c' 3054 val () = checkCon env e' et c'
3047 3055
3048 val c = normClassConstraint env c' 3056 val c' = normClassConstraint env c'
3049 val (env', n) = E.pushENamed env x c' 3057 val (env', n) = E.pushENamed env x c'
3050 in 3058 in
3051 (*prefaces "DVal" [("x", Print.PD.string x), 3059 (*prefaces "DVal" [("x", Print.PD.string x),
3052 ("c'", p_con env c')];*) 3060 ("c'", p_con env c')];*)
3053 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ gs)) 3061 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ gs))
3066 (fn ((x, co, e), gs) => 3074 (fn ((x, co, e), gs) =>
3067 let 3075 let
3068 val (c', _, gs1) = case co of 3076 val (c', _, gs1) = case co of
3069 NONE => (cunif (loc, ktype), ktype, []) 3077 NONE => (cunif (loc, ktype), ktype, [])
3070 | SOME c => elabCon (env, denv) c 3078 | SOME c => elabCon (env, denv) c
3079 val c' = normClassConstraint env c'
3071 in 3080 in
3072 ((x, c', e), enD gs1 @ gs) 3081 ((x, c', e), enD gs1 @ gs)
3073 end) gs vis 3082 end) gs vis
3074 3083
3075 val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) => 3084 val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) =>