de1d865 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Much improved inlining

de1d865Edwin Brady9 years ago

libs/prelude/IO.idr+3−2

compare with master

unifiedsplit

@@ -101,9 +101,10 @@ unsafePerformPrimIO : PrimIO a -> a

101prim_io_pure : a -> PrimIO a

102prim_io_pure x = Prim__IO x

103

104+-- %inline

104io_bind : IO' l a -> (a -> IO' l b) -> IO' l b

105io_bind : IO' l a -> (a -> IO' l b) -> IO' l b

105−io_bind (MkIO fn) k

106+io_bind (MkIO fn)

106− = MkIO (\w => prim_io_bind (fn w)

107+ = \k => MkIO (\w => prim_io_bind (fn w)

107 (\ b => case k b of

108 (\ b => case k b of

108 MkIO fkb => fkb w))

109 MkIO fkb => fkb w))

109

110

src/IRTS/CodegenC.hs+19−22

@@ -697,29 +697,26 @@ ifaceC (ExportFun n cn ret args)

697

698 argNames = zipWith (++) (repeat "arg") (map show [0..])

699

700+mkBody n as_in t

700−mkBody n as t = indent 1 ++ "INITFRAME;\n" ++

701+ = indent 1 ++ "INITFRAME;\n" ++

701− indent 1 ++ "RESERVE(" ++ show (max (length as) 3) ++ ");\n" ++

702+ indent 1 ++ "RESERVE(" ++ show (max (length as) 3) ++ ");\n" ++

702− push 0 as ++ call n ++ retval t

703+ push 0 as ++ call n ++ retval t

703− where push i [] = ""

704+ where

705+ as = case t of

706+ FIO t -> as_in ++ [("NULL", FUnknown)] -- add world token

707+ _ -> as_in

708+ push i [] = ""

704− push i ((n, t) : ts) = indent 1 ++ c_irts (toFType t)

709+ push i ((n, t) : ts) = indent 1 ++ c_irts (toFType t)

705− ("TOP(" ++ show i ++ ") = ") n

710+ ("TOP(" ++ show i ++ ") = ") n

706− ++ ";\n" ++ push (i + 1) ts

711+ ++ ";\n" ++ push (i + 1) ts

707−

712+

708− call _ = indent 1 ++ "STOREOLD;\n" ++

709− indent 1 ++ "BASETOP(0);\n" ++

710− indent 1 ++ "ADDTOP(" ++ show (length as) ++ ");\n" ++

711− indent 1 ++ "CALL(" ++ cname n ++ ");\n"

712−

713− retval (FIO t)

714− = indent 1 ++ "TOP(0) = NULL;\n" ++

715− indent 1 ++ "TOP(1) = NULL;\n" ++

716− indent 1 ++ "TOP(2) = RVAL;\n" ++

717− indent 1 ++ "STOREOLD;\n" ++

713+ call _ = indent 1 ++ "STOREOLD;\n" ++

718 indent 1 ++ "BASETOP(0);\n" ++

714 indent 1 ++ "BASETOP(0);\n" ++

719− indent 1 ++ "ADDTOP(3);\n" ++

715+ indent 1 ++ "ADDTOP(" ++ show (length as) ++ ");\n" ++

720− indent 1 ++ "CALL(" ++ cname (sUN "call__IO") ++ ");\n" ++

716+ indent 1 ++ "CALL(" ++ cname n ++ ");\n"

717+

721− retval t

718+ retval (FIO t) = retval t

722− retval t = indent 1 ++ "return " ++ irts_c (toFType t) "RVAL" ++ ";\n"

719+ retval t = indent 1 ++ "return " ++ irts_c (toFType t) "RVAL" ++ ";\n"

723

720

724ctype (FCon c)

721ctype (FCon c)

725 | c == sUN "C_Str" = "char*"

722 | c == sUN "C_Str" = "char*"

src/IRTS/Compiler.hs+14−7

@@ -81,7 +81,14 @@ compile codegen f mtm = do

81 let defsUniq = map (allocUnique (addAlist defsInlined emptyContext))

82 defsInlined

84+ logCodeGen 1 "Inlining"

85+

86+ dumpCases <- getDumpCases

87+ case dumpCases of

88+ Nothing -> return ()

89+ Just f -> runIO $ writeFile f (showCaseTrees defsUniq)

90+

84− let (nexttag, tagged) = addTags 65536 (liftAll defsUniq)

91+ let (nexttag, tagged) = addTags 65536 (liftAll defsInlined)

85 let ctxtIn = addAlist tagged emptyContext

92 let ctxtIn = addAlist tagged emptyContext

87 logCodeGen 1 "Defunctionalising"

94 logCodeGen 1 "Defunctionalising"

@@ -96,11 +103,7 @@ compile codegen f mtm = do

103

97 let checked = simplifyDefs defuns (toAlist defuns)

104 let checked = simplifyDefs defuns (toAlist defuns)

98 outty <- outputTy

105 outty <- outputTy

99− dumpCases <- getDumpCases

100 dumpDefun <- getDumpDefun

106 dumpDefun <- getDumpDefun

101− case dumpCases of

102− Nothing -> return ()

103− Just f -> runIO $ writeFile f (showCaseTrees defs)

104 case dumpDefun of

107 case dumpDefun of

105 Nothing -> return ()

108 Nothing -> return ()

106 Just f -> runIO $ writeFile f (dumpDefuns defuns)

109 Just f -> runIO $ writeFile f (dumpDefuns defuns)

@@ -168,9 +171,13 @@ getDeclarations used

168showCaseTrees :: [(Name, LDecl)] -> String

171showCaseTrees :: [(Name, LDecl)] -> String

169showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)

172showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)

170 where

173 where

171− showCT (n, LFun _ f args lexp)

174+ showCT (n, LFun opts f args lexp)

175+ = showOpts ++

172− = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"

176+ show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"

173 ++ show lexp

177 ++ show lexp

178+ where

179+ showOpts | Inline `elem` opts = "%inline "

180+ | otherwise = ""

174 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a

181 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a

175

182

176 defnRank :: (Name, LDecl) -> String

183 defnRank :: (Name, LDecl) -> String

src/IRTS/Lang.hs+2−2

@@ -346,8 +346,8 @@ instance Show LExp where

346 ++ " in " ++ show' (env ++ [show n]) ind e

347

348 show' env ind (LLam args e)

349− = "\\ " ++ showSep "," (map show args)

349+ = "(\\ " ++ showSep "," (map show args)

350− ++ " => " ++ show' (env ++ (map show args)) ind e

350+ ++ " => " ++ show' (env ++ (map show args)) ind e ++ ") "

351

352 show' env ind (LProj t i) = show t ++ "!" ++ show i

353

src/IRTS/LangOpts.hs+108−49

@@ -7,12 +7,16 @@ Maintainer : The Idris Community.

7-}

8{-# LANGUAGE DeriveFunctor, PatternGuards #-}

10−module IRTS.LangOpts where

10+module IRTS.LangOpts(inlineAll) where

12+import Idris.Core.CaseTree

12import Idris.Core.TT

13import Idris.Core.TT

13import IRTS.Lang

14import IRTS.Lang

15import Control.Monad.State hiding (lift)

16import Control.Monad.State hiding (lift)

17+import Data.List

18+

19+import Debug.Trace

17inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)]

21inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)]

18inlineAll lds = let defs = addAlist lds emptyContext in

22inlineAll lds = let defs = addAlist lds emptyContext in

@@ -31,53 +35,108 @@ nextN = do i <- get

31doInline :: LDefs -> LDecl -> LDecl

35doInline :: LDefs -> LDecl -> LDecl

32doInline defs d@(LConstructor _ _ _) = d

36doInline defs d@(LConstructor _ _ _) = d

33doInline defs (LFun opts topn args exp)

37doInline defs (LFun opts topn args exp)

38+ = let res = evalState (eval [] initEnv [topn] defs exp)

39+ (length args) in

34− = let res = evalState (inlineWith [topn] (map (\n -> (n, LV n)) args) exp) 0 in

40+-- = let res = evalState (inlineWith [topn] (map (\n -> (n, LV n)) args) exp) 0 in

41+ case res of

35− LFun opts topn args res

42+ LLam args' body -> LFun opts topn (map snd initNames ++ args') body

43+ _ -> LFun opts topn (map snd initNames) res

36 where

44 where

45+ initNames = zipWith (\n i -> (n, newn n i)) args [0..]

46+ initEnv = map (\(n, n') -> (n, LV n')) initNames

47+ newn (UN n) i = MN i n

48+ newn _ i = sMN i "arg"

49+

50+unload :: [LExp] -> LExp -> LExp

51+unload [] e = e

52+unload stk (LApp tc e args) = LApp tc e (args ++ stk)

53+unload stk e = LApp False e stk

54+

55+takeStk :: [(Name, LExp)] -> [Name] -> [LExp] ->

56+ ([(Name, LExp)], [Name], [LExp])

57+takeStk env (a : args) (v : stk) = takeStk ((a, v) : env) args stk

58+takeStk env args stk = (env, args, stk)

59+

37− inlineWith :: [Name] -> [(Name, LExp)] -> LExp -> State Int LExp

60+eval :: [LExp] -> [(Name, LExp)] -> [Name] -> LDefs -> LExp -> State Int LExp

38− inlineWith done env var@(LV n)

61+eval stk env rec defs (LLazyApp n es)

62+ = unload stk <$> LLazyApp n <$> (mapM (eval [] env rec defs) es)

63+eval stk env rec defs (LForce e)

64+ = unload stk <$> LForce <$> eval [] env rec defs e

65+eval stk env rec defs (LLazyExp e)

66+ = unload stk <$> LLazyExp <$> eval [] env rec defs e

67+-- Special case for io_bind, because it needs to keep executing the first

68+-- action, and is worth inlining to avoid the thunk

69+eval [] env rec defs (LApp t (LV n) [_, _, _, act, (LLam [arg] k)])

70+ | n == sUN "io_bind"

71+ = do w <- nextN

72+ let env' = (w, LV w) : env

73+ act' <- eval [] env' rec defs (LApp False act [LV w])

74+ argn <- nextN

75+ k' <- eval [] ((arg, LV argn) : env') rec defs (LApp False k [LV w])

76+ return $ LLam [w] (LLet argn act' k')

77+eval (world : stk) env rec defs (LApp t (LV n) [_, _, _, act, (LLam [arg] k)])

78+ | n == sUN "io_bind"

79+ = do act' <- eval [] env rec defs (LApp False act [world])

80+ argn <- nextN

81+ k' <- eval stk ((arg, LV argn) : env) rec defs (LApp False k [world])

82+ return $ LLet argn act' k'

83+

84+eval stk env rec defs (LApp t f es)

85+ = do es' <- mapM (eval [] env rec defs) es

86+ eval (es' ++ stk) env rec defs f

87+eval stk env rec defs (LLet n val sc)

88+ = do n' <- nextN

89+ LLet n' <$> eval [] env rec defs val

90+ <*> eval stk ((n, LV n') : env) rec defs sc

91+eval stk env rec defs (LProj exp i)

92+ = unload stk <$> (LProj <$> eval [] env rec defs exp <*> return i)

93+eval stk env rec defs (LCon loc i n es)

94+ = unload stk <$> (LCon loc i n <$> mapM (eval [] env rec defs) es)

95+eval stk env rec defs (LCase ty e alts)

96+ = LCase ty <$> eval [] env rec defs e

97+ <*> mapM (evalAlt stk env rec defs) alts

98+eval stk env rec defs (LOp f es)

99+ = unload stk <$> LOp f <$> mapM (eval [] env rec defs) es

100+eval stk env rec defs (LForeign t s args)

101+ = unload stk <$>

102+ LForeign t s <$> mapM (\(t, e) -> do e' <- eval [] env rec defs e

103+ return (t, e')) args

104+-- save the interesting cases for the end:

105+-- lambdas, and names to reduce

106+eval stk env rec defs (LLam args sc)

107+ | (env', args', stk') <- takeStk env args stk

108+ = case args' of

109+ [] -> eval stk' env' rec defs sc

110+ as -> do ns' <- mapM (\n -> do n' <- nextN

111+ return (n, n')) args'

112+ LLam (map snd ns') <$>

113+ eval [] (map (\ (n, n') -> (n, LV n')) ns' ++ env')

114+ rec defs sc

115+eval stk env rec defs var@(LV n)

39− = case lookup n env of

116+ = case lookup n env of

40− Just t -> return t

117+ Just t

118+ | t /= LV n && n `notElem` rec ->

119+ eval stk env (n : rec) defs t

120+ | otherwise -> return (unload stk t)

41− Nothing -> return var

121+ Nothing

42− inlineWith done env (LLazyApp n es) = LLazyApp n <$> (mapM (inlineWith done env) es)

43− inlineWith done env (LForce e) = LForce <$> inlineWith done env e

44− inlineWith done env (LLazyExp e) = LLazyExp <$> inlineWith done env e

45− -- Extend the environment for Let and Lam so that bound names aren't

46− -- expanded with any top level argument definitions they shadow

47− inlineWith done env (LLet n val sc)

48− = do n' <- nextN

49− LLet n' <$> inlineWith done env val <*>

50− inlineWith done ((n, LV n') : env) sc

51− inlineWith done env (LLam args sc)

52− = do ns' <- mapM (\n -> do n' <- nextN

53− return (n, n')) args

54− LLam (map snd ns') <$>

55− inlineWith done (map (\ (n,n') -> (n, LV n')) ns' ++ env) sc

56− inlineWith done env (LProj exp i) = LProj <$> inlineWith done env exp <*> return i

57− inlineWith done env (LCon loc i n es)

58− = LCon loc i n <$> mapM (inlineWith done env) es

59− inlineWith done env (LCase ty e alts)

60− = LCase ty <$> inlineWith done env e <*> mapM (inlineWithAlt done env) alts

61− inlineWith done env (LOp f es) = LOp f <$> mapM (inlineWith done env) es

62− -- the interesting case!

63− inlineWith done env (LApp t (LV n) es)

64− | n `notElem` done,

122+ | n `notElem` rec,

65− [LFun opts _ args body] <- lookupCtxt n defs,

123+ Just (LFun opts _ args body) <- lookupCtxtExact n defs,

66− Inline `elem` opts,

124+ Inline `elem` opts ->

67− length es == length args

125+ apply stk env (n : rec) defs var args body

68− = do es' <- mapM (inlineWith done env) es

126+ | otherwise -> return (unload stk var)

69− inlineWith (n : done) (zip args es' ++ env) body

127+eval stk env rec defs t = return (unload stk t)

70− inlineWith done env (LApp t f es)

128+

71− = LApp t <$> inlineWith done env f <*> mapM (inlineWith done env) es

129+evalAlt stk env rec defs (LConCase i n es rhs)

72− inlineWith done env (LForeign t s args)

130+ = do ns' <- mapM (\n -> do n' <- nextN

73− = LForeign t s <$> mapM (\(t, e) -> do e' <- inlineWith done env e

131+ return (n, n')) es

74− return (t, e')) args

132+ LConCase i n (map snd ns') <$>

75− inlineWith done env t = return t

133+ eval stk (map (\ (n, n') -> (n, LV n')) ns' ++ env) rec defs rhs

134+evalAlt stk env rec defs (LConstCase c e)

135+ = LConstCase c <$> eval stk env rec defs e

136+evalAlt stk env rec defs (LDefaultCase e)

137+ = LDefaultCase <$> eval stk env rec defs e

138

77− inlineWithAlt done env (LConCase i n es rhs)

139+apply :: [LExp] -> [(Name, LExp)] -> [Name] -> LDefs -> LExp ->

78− = do ns' <- mapM (\n -> do n' <- nextN

140+ [Name] -> LExp -> State Int LExp

79− return (n, n')) es

141+apply stk env rec defs var args body

80− LConCase i n (map snd ns') <$>

142+ = eval stk env rec defs (LLam args body)

81− inlineWith done (map (\ (n,n') -> (n, LV n')) ns' ++ env) rhs

82− inlineWithAlt done env (LConstCase c e) = LConstCase c <$> inlineWith done env e

83− inlineWithAlt done env (LDefaultCase e) = LDefaultCase <$> inlineWith done env e