From 0ce7847026a7be88c3cde012c5f74d69d682a491 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 5 Aug 2012 14:55:28 -0400 Subject: Tweaking treatment of function application: substitute or introduce a 'let'? --- src/reduce.sml | 55 +++++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 43 insertions(+), 12 deletions(-) (limited to 'src/reduce.sml') diff --git a/src/reduce.sml b/src/reduce.sml index 1fbf526d..c5733b97 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -232,6 +232,21 @@ fun monadRecord m loc = ((CName "Bind", loc), bindType m loc)]), loc), loc) +fun passive (e : exp) = + case #1 e of + EPrim _ => true + | ERel _ => true + | ENamed _ => true + | ECon (_, _, _, NONE) => true + | ECon (_, _, _, SOME e) => passive e + | EFfi _ => true + | EAbs _ => true + | ECAbs _ => true + | EKAbs _ => true + | ERecord xes => List.all (passive o #2) xes + | EField (e, _, _) => passive e + | _ => false + fun kindConAndExp (namedC, namedE) = let fun kind env (all as (k, loc)) = @@ -534,16 +549,30 @@ fun kindConAndExp (namedC, namedE) = val e2 = exp env e2 in case #1 e1 of - EAbs (_, _, _, b) => - let - val r = exp (KnownE e2 :: env') b - in - (*Print.prefaces "eapp" [("b", CorePrint.p_exp CoreEnv.empty b), - ("env", Print.PD.string (e2s env')), - ("e2", CorePrint.p_exp CoreEnv.empty e2), - ("r", CorePrint.p_exp CoreEnv.empty r)];*) - r - end + ELet (x, t, e1', e2') => + (ELet (x, t, e1', exp (UnknownE :: env') (EApp (e2', E.liftExpInExp 0 e2), loc)), loc) + + | EAbs (x, dom, _, b) => + if count b <= 1 orelse passive e2 orelse ESpecialize.functionInside dom then + let + val r = exp (KnownE e2 :: env') b + in + (*Print.prefaces "eapp" [("b", CorePrint.p_exp CoreEnv.empty b), + ("env", Print.PD.string (e2s env')), + ("e2", CorePrint.p_exp CoreEnv.empty e2), + ("r", CorePrint.p_exp CoreEnv.empty r)];*) + r + end + else + let + val dom = con env' dom + val r = exp (UnknownE :: env') b + in + (*Print.prefaces "El skippo" [("x", Print.PD.string x), + ("e2", CorePrint.p_exp CoreEnv.empty e2)];*) + (ELet (x, dom, e2, r), loc) + end + | ECase (e, pes, cc as {disc, result = res as (TFun (_, c2), _)}) => let val pes' = map (fn (p, body) => @@ -760,12 +789,14 @@ fun kindConAndExp (namedC, namedE) = | ELet (x, t, e1, e2) => let + val e1' = exp env e1 + val t = con env t in - if ESpecialize.functionInside t then + if passive e1' orelse count e2 <= 1 orelse ESpecialize.functionInside t then exp (KnownE e1 :: env) e2 else - (ELet (x, t, exp env e1, exp (UnknownE :: env) e2), loc) + (ELet (x, t, e1', exp (UnknownE :: env) e2), loc) end | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, con env t), loc) -- cgit v1.2.3