bdf11e8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Better IO + faster compilation by avoiding needless cases in EVAL/APPLY

bdf11e8Edwin Brady14 years ago

src/IRTS/Compiler.hs+5−1

compare with master

unifiedsplit

@@ -170,6 +170,10 @@ instance ToIR (TT Name) where

170 | (P _ (UN "prim__IO") _, [v]) <- unApply tm

171 = do v' <- ir' env v

172 return v'

173+ | (P _ (UN "io_bind") _, [_,_,v,Bind n (Lam _) sc]) <- unApply tm

174+ = do v' <- ir' env v

175+ sc' <- ir' (n:env) sc

176+ return (LLet n (LForce v') sc')

173 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm

177 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm

174 = do v' <- ir' env v

178 = do v' <- ir' env v

175 k' <- ir' env k

179 k' <- ir' env k

@@ -257,7 +261,7 @@ instance ToIR (TT Name) where

257 do args' <- mapM (ir' env) args

261 do args' <- mapM (ir' env) args

258 -- wrap it in a prim__IO

262 -- wrap it in a prim__IO

259 -- return $ con_ 0 @@ impossible @@

263 -- return $ con_ 0 @@ impossible @@

260− return $ LLazyExp $

264+ return $ -- LLazyExp $

261 LForeign LANG_C rty fgnName (zip tys args')

265 LForeign LANG_C rty fgnName (zip tys args')

262 | otherwise = fail "Badly formed foreign function call"

266 | otherwise = fail "Badly formed foreign function call"

263

267

src/IRTS/Defunctionalise.hs+71−43

@@ -7,6 +7,8 @@ import Core.TT

7import Debug.Trace

8import Data.Maybe

9import Data.List

10+import Control.Monad

11+import Control.Monad.State

11data DExp = DV LVar

13data DExp = DV LVar

12 | DApp Bool Name [DExp] -- True = tail call

14 | DApp Bool Name [DExp] -- True = tail call

@@ -39,11 +41,12 @@ defunctionalise :: Int -> LDefs -> DDefs

39defunctionalise nexttag defs

41defunctionalise nexttag defs

40 = let all = toAlist defs

42 = let all = toAlist defs

41 -- sort newcons so that EVAL and APPLY cons get sequential tags

43 -- sort newcons so that EVAL and APPLY cons get sequential tags

44+ (allD, enames) = runState (mapM (addApps defs) all) []

42− newcons = sortBy conord $ concatMap toCons (getFn all)

45+ newcons = sortBy conord $ concatMap (toCons enames) (getFn all)

43 eval = mkEval newcons

46 eval = mkEval newcons

44 app = mkApply newcons

47 app = mkApply newcons

45 condecls = declare nexttag newcons in

48 condecls = declare nexttag newcons in

46− addAlist (eval : app : condecls ++ (map (addApps defs) all)) emptyContext

49+ addAlist (eval : app : condecls ++ allD) emptyContext

47 where conord (n, _, _) (n', _, _) = compare n n'

50 where conord (n, _, _) (n', _, _) = compare n n'

49getFn :: [(Name, LDecl)] -> [(Name, Int)]

52getFn :: [(Name, LDecl)] -> [(Name, Int)]

@@ -64,57 +67,80 @@ getFn xs = mapMaybe fnData xs

64-- 7 Wrap unknown applications (i.e. applications of local variables) in chains of APPLY

67-- 7 Wrap unknown applications (i.e. applications of local variables) in chains of APPLY

65-- 8 Add explicit EVAL to case, primitives, and foreign calls

68-- 8 Add explicit EVAL to case, primitives, and foreign calls

67−addApps :: LDefs -> (Name, LDecl) -> (Name, DDecl)

70+addApps :: LDefs -> (Name, LDecl) -> State [Name] (Name, DDecl)

68−addApps defs o@(n, LConstructor _ t a) = (n, DConstructor n t a)

71+addApps defs o@(n, LConstructor _ t a)

72+ = return (n, DConstructor n t a)

69−addApps defs (n, LFun _ _ args e) = (n, DFun n args (aa args e))

73+addApps defs (n, LFun _ _ args e)

74+ = do e' <- aa args e

75+ return (n, DFun n args e')

70 where

76 where

71− aa :: [Name] -> LExp -> DExp

77+ aa :: [Name] -> LExp -> State [Name] DExp

72− aa env (LV (Glob n)) | n `elem` env = DV (Glob n)

78+ aa env (LV (Glob n)) | n `elem` env = return $ DV (Glob n)

73 | otherwise = aa env (LApp False (LV (Glob n)) [])

79 | otherwise = aa env (LApp False (LV (Glob n)) [])

74-- aa env e@(LApp tc (MN 0 "EVAL") [a]) = e

80-- aa env e@(LApp tc (MN 0 "EVAL") [a]) = e

75 aa env (LApp tc (LV (Glob n)) args)

81 aa env (LApp tc (LV (Glob n)) args)

76− = let args' = map (aa env) args in

82+ = do args' <- mapM (aa env) args

77− case lookupCtxt Nothing n defs of

83+ case lookupCtxt Nothing n defs of

78− [LConstructor _ i ar] -> DApp tc n args'

84+ [LConstructor _ i ar] -> return $ DApp tc n args'

79 [LFun _ _ as _] -> let arity = length as in

85 [LFun _ _ as _] -> let arity = length as in

80 fixApply tc n args' arity

86 fixApply tc n args' arity

81− [] -> chainAPPLY (DV (Glob n)) args'

87+ [] -> return $ chainAPPLY (DV (Glob n)) args'

82 aa env (LLazyApp n args)

88 aa env (LLazyApp n args)

83− = let args' = map (aa env) args in

89+ = do args' <- mapM (aa env) args

84− case lookupCtxt Nothing n defs of

90+ case lookupCtxt Nothing n defs of

85− [LConstructor _ i ar] -> DApp False n args'

91+ [LConstructor _ i ar] -> return $ DApp False n args'

86 [LFun _ _ as _] -> let arity = length as in

92 [LFun _ _ as _] -> let arity = length as in

87 fixLazyApply n args' arity

93 fixLazyApply n args' arity

88− [] -> chainAPPLY (DV (Glob n)) args'

94+ [] -> return $ chainAPPLY (DV (Glob n)) args'

95+ aa env (LForce (LLazyApp n args)) = aa env (LApp False (LV (Glob n)) args)

89− aa env (LForce e) = eEVAL (aa env e)

96+ aa env (LForce e) = liftM eEVAL (aa env e)

90− aa env (LLet n v sc) = DLet n (aa env v) (aa (n : env) sc)

97+ aa env (LLet n v sc) = liftM2 (DLet n) (aa env v) (aa (n : env) sc)

91− aa env (LCon i n args) = DC i n (map (aa env) args)

98+ aa env (LCon i n args) = liftM (DC i n) (mapM (aa env) args)

92 aa env (LProj t@(LV (Glob n)) i)

99 aa env (LProj t@(LV (Glob n)) i)

100+ = do t' <- aa env t

93− = DProj (DUpdate n (eEVAL (aa env t))) i

101+ return $ DProj (DUpdate n (eEVAL t')) i

94− aa env (LProj t i) = DProj (eEVAL (aa env t)) i

102+ aa env (LProj t i) = do t' <- aa env t

103+ return $ DProj (eEVAL t') i

104+ aa env (LCase e alts) = do e' <- aa env e

105+ alts' <- mapM (aaAlt env) alts

95− aa env (LCase e alts) = DCase (eEVAL (aa env e)) (map (aaAlt env) alts)

106+ return $ DCase (eEVAL e') alts'

96− aa env (LConst c) = DConst c

107+ aa env (LConst c) = return $ DConst c

97− aa env (LForeign l t n args) = DForeign l t n (map (aaF env) args)

108+ aa env (LForeign l t n args) = liftM (DForeign l t n) (mapM (aaF env) args)

98− aa env (LOp LFork args) = DOp LFork (map (aa env) args)

109+ aa env (LOp LFork args) = liftM (DOp LFork) (mapM (aa env) args)

99− aa env (LOp f args) = DOp f (map (eEVAL . (aa env)) args)

110+ aa env (LOp f args) = do args' <- mapM (aa env) args

111+ return $ DOp f (map eEVAL args')

100− aa env LNothing = DNothing

112+ aa env LNothing = return DNothing

101− aa env (LError e) = DError e

113+ aa env (LError e) = return $ DError e

102−

114+

103− aaF env (t, e) = (t, eEVAL (aa env e))

115+ aaF env (t, e) = do e' <- aa env e

104−

116+ return (t, eEVAL e')

117+

105− aaAlt env (LConCase i n args e) = DConCase i n args (aa (args ++ env) e)

118+ aaAlt env (LConCase i n args e)

119+ = liftM (DConCase i n args) (aa (args ++ env) e)

106− aaAlt env (LConstCase c e) = DConstCase c (aa env e)

120+ aaAlt env (LConstCase c e) = liftM (DConstCase c) (aa env e)

107− aaAlt env (LDefaultCase e) = DDefaultCase (aa env e)

121+ aaAlt env (LDefaultCase e) = liftM DDefaultCase (aa env e)

108

122

109 fixApply tc n args ar

123 fixApply tc n args ar

110− | length args == ar = DApp tc n args

124+ | length args == ar

125+ = return $ DApp tc n args

126+ | length args < ar

127+ = do ns <- get

128+ put $ nub (n : ns)

111− | length args < ar = DApp tc (mkUnderCon n (ar - length args)) args

129+ return $ DApp tc (mkUnderCon n (ar - length args)) args

130+ | length args > ar

112− | length args > ar = chainAPPLY (DApp tc n (take ar args)) (drop ar args)

131+ = return $ chainAPPLY (DApp tc n (take ar args)) (drop ar args)

113

132

114 fixLazyApply n args ar

133 fixLazyApply n args ar

134+ | length args == ar

135+ = do ns <- get

136+ put $ nub (n : ns)

115− | length args == ar = DApp False (mkFnCon n) args

137+ return $ DApp False (mkFnCon n) args

138+ | length args < ar

139+ = do ns <- get

140+ put $ nub (n : ns)

116− | length args < ar = DApp False (mkUnderCon n (ar - length args)) args

141+ return $ DApp False (mkUnderCon n (ar - length args)) args

142+ | length args > ar

117− | length args > ar = chainAPPLY (DApp False n (take ar args)) (drop ar args)

143+ = return $ chainAPPLY (DApp False n (take ar args)) (drop ar args)

118

144

119 chainAPPLY f [] = f

145 chainAPPLY f [] = f

120 chainAPPLY f (a : as) = chainAPPLY (DApp False (MN 0 "APPLY") [f, a]) as

146 chainAPPLY f (a : as) = chainAPPLY (DApp False (MN 0 "APPLY") [f, a]) as

@@ -154,14 +180,16 @@ data EvalApply a = EvalCase (Name -> a)

154-- For a function name, generate a list of

180-- For a function name, generate a list of

155-- data constuctors, and whether to handle them in EVAL or APPLY

181-- data constuctors, and whether to handle them in EVAL or APPLY

156

182

157−toCons :: (Name, Int) -> [(Name, Int, EvalApply DAlt)]

183+toCons :: [Name] -> (Name, Int) -> [(Name, Int, EvalApply DAlt)]

158−toCons (n, i)

184+toCons ns (n, i)

185+ | n `elem` ns

159− = (mkFnCon n, i,

186+ = (mkFnCon n, i,

160− EvalCase (\tlarg ->

187+ EvalCase (\tlarg ->

161 (DConCase (-1) (mkFnCon n) (take i (genArgs 0))

188 (DConCase (-1) (mkFnCon n) (take i (genArgs 0))

162 (dupdate tlarg

189 (dupdate tlarg

163 (eEVAL (DApp False n (map (DV . Glob) (take i (genArgs 0)))))))))

190 (eEVAL (DApp False n (map (DV . Glob) (take i (genArgs 0)))))))))

164 : mkApplyCase n 0 i

191 : mkApplyCase n 0 i

192+ | otherwise = []

165 where dupdate tlarg x = x

193 where dupdate tlarg x = x

166

194

167mkApplyCase fname n ar | n == ar = []

195mkApplyCase fname n ar | n == ar = []

test/test004/test004.idr+2−2

@@ -12,10 +12,10 @@ main : IO ()

12main = do { h <- openFile "testfile" Write

13 fwrite h "Hello!\nWorld!\n"

14 closeFile h

15− putStrLn "Reading testfile"

15+ putStrLn "Reading testfile"

16 f <- readFile "testfile"

17 putStrLn f

18− putStrLn "---"

18+ putStrLn "---"

19 dumpFile "testfile"

20 }

test/test014/Resimp.idr+1−1

@@ -98,7 +98,7 @@ using (i: Fin n, gam : Vect Ty n, gam' : Vect Ty n, gam'' : Vect Ty n)

99{-- Control structures --}

100

101− Lift : IO a -> Res gam gam (R a)

101+ Lift : |(action:IO a) -> Res gam gam (R a)

102 Check : (p:HasType gam i (Choice (interpTy a) (interpTy b))) ->

103 (failure:Res (update gam p a) (update gam p c) t) ->

104 (success:Res (update gam p b) (update gam p c) t) ->