comparison src/elaborate.sml @ 825:7f871c03e3a1

Destructing local let, to the point where demo compiles
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 May 2009 12:07:05 -0400
parents d4e811beb8eb
children d07980bf1444
comparison
equal deleted inserted replaced
824:be0988e46336 825:7f871c03e3a1
2091 | L.ELet (eds, e) => 2091 | L.ELet (eds, e) =>
2092 let 2092 let
2093 val (eds, (env, gs1)) = ListUtil.foldlMap (elabEdecl denv) (env, []) eds 2093 val (eds, (env, gs1)) = ListUtil.foldlMap (elabEdecl denv) (env, []) eds
2094 val (e, t, gs2) = elabExp (env, denv) e 2094 val (e, t, gs2) = elabExp (env, denv) e
2095 in 2095 in
2096 ((L'.ELet (eds, e), loc), t, gs1 @ gs2) 2096 ((L'.ELet (eds, e, t), loc), t, gs1 @ gs2)
2097 end 2097 end
2098 in 2098 in
2099 (*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*) 2099 (*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*)
2100 r 2100 r
2101 end 2101 end
2102 2102
2103 and elabEdecl denv (dAll as (d, loc), (env, gs)) = 2103 and elabEdecl denv (dAll as (d, loc), (env, gs)) =
2104 let 2104 let
2105 val r = 2105 val r =
2106 case d of 2106 case d of
2107 L.EDVal (x, co, e) => 2107 L.EDVal (p, e) =>
2108 let 2108 let
2109 val (c', _, gs1) = case co of 2109 val ((p', pt), (env', _)) = elabPat (p, (env, SS.empty))
2110 NONE => (cunif (loc, ktype), ktype, []) 2110 val (e', et, gs1) = elabExp (env, denv) e
2111 | SOME c => elabCon (env, denv) c 2111
2112 2112 val () = checkCon env e' et pt
2113 val (e', et, gs2) = elabExp (env, denv) e 2113
2114 2114 val pt = normClassConstraint env pt
2115 val () = checkCon env e' et c'
2116
2117 val c' = normClassConstraint env c'
2118 val env' = E.pushERel env x c'
2119 in 2115 in
2120 ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ gs)) 2116 ((L'.EDVal (p', pt, e'), loc), (env', gs1 @ gs))
2121 end 2117 end
2122 | L.EDValRec vis => 2118 | L.EDValRec vis =>
2123 let 2119 let
2124 fun allowable (e, _) = 2120 fun allowable (e, _) =
2125 case e of 2121 case e of