git.iko.soy/Idris-dev
on bba84d5 help sign in
Idris-dev/src/IRTS/Compiler.hs
279 lines 11 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module IRTS.Compiler where
5import IRTS.Lang
6import IRTS.Defunctionalise
7import IRTS.Simplified
8import IRTS.CodegenC
9import IRTS.CodegenJava
10import IRTS.Inliner
12import Idris.AbsSyntax
13import Idris.UnusedArgs
15import Core.TT
16import Core.Evaluate
17import Core.CaseTree
19import Control.Monad.State
20import Data.List
21import System.Process
22import System.IO
23import System.Directory
24import System.Environment
26import Paths_idris
28compile :: Target -> FilePath -> Term -> Idris ()
29compile target f tm
30 = do checkMVs
31 let tmnames = namesUsed (STerm tm)
32 used <- mapM (allNames []) tmnames
33 defsIn <- mkDecls tm (concat used)
34 findUnusedArgs (concat used)
35 maindef <- irMain tm
36 objs <- getObjectFiles
37 libs <- getLibs
38 hdrs <- getHdrs
39 let defs = defsIn ++ [(MN 0 "runMain", maindef)]
40 -- iputStrLn $ showSep "\n" (map show defs)
41 let (nexttag, tagged) = addTags 65536 (liftAll defs)
42 let ctxtIn = addAlist tagged emptyContext
43 iLOG "Defunctionalising"
44 let defuns_in = defunctionalise nexttag ctxtIn
45 logLvl 5 $ show defuns_in
46 iLOG "Inlining"
47 let defuns = inline defuns_in
48 logLvl 5 $ show defuns
49 iLOG "Resolving variables for CG"
50 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))
51 let checked = checkDefs defuns (toAlist defuns)
52 dumpC <- getDumpC
53 dumpCases <- getDumpCases
54 dumpDefun <- getDumpDefun
55 case dumpCases of
56 Nothing -> return ()
57 Just f -> liftIO $ writeFile f (showCaseTrees tagged)
58 case dumpDefun of
59 Nothing -> return ()
60 Just f -> liftIO $ writeFile f (dumpDefuns defuns)
61 iLOG "Building output"
62 case checked of
63 OK c -> case target of
64 ViaC -> liftIO $ codegenC dumpC c f True hdrs
65 (concatMap mkObj objs)
66 (concatMap mkLib libs) NONE
67 ViaJava -> liftIO $ codegenJava c f
68 Error e -> fail $ show e
69 where checkMVs = do i <- get
70 case idris_metavars i \\ primDefs of
71 [] -> return ()
72 ms -> fail $ "There are undefined metavariables: " ++ show ms
73 inDir d h = do let f = d ++ "/" ++ h
74 ex <- doesFileExist f
75 if ex then return f else return h
76 mkObj f = f ++ " "
77 mkLib l = "-l" ++ l ++ " "
81irMain :: TT Name -> Idris LDecl
82irMain tm = do i <- ir tm
83 return $ LFun (MN 0 "runMain") [] (LForce i)
85allNames :: [Name] -> Name -> Idris [Name]
86allNames ns n | n `elem` ns = return []
87allNames ns n = do i <- get
88 case lookupCtxt Nothing n (idris_callgraph i) of
89 [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
90 return (nub (n : concat more))
91 _ -> return [n]
93mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
94mkDecls t used
95 = do i <- getIState
96 let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
97 mapM traceUnused used
98 decls <- mapM build ds
99 return decls
101showCaseTrees :: [(Name, LDecl)] -> String
102showCaseTrees ds = showSep "\n\n" (map showCT ds)
103 where
104 showCT (n, LFun f args lexp)
105 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t "
106 ++ show lexp
107 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
109isCon (TyDecl _ _) = True
110isCon _ = False
112class ToIR a where
113 ir :: a -> Idris LExp
115build :: (Name, Def) -> Idris (Name, LDecl)
116build (n, d)
117 = do i <- getIState
118 case lookup n (idris_scprims i) of
119 Just (ar, op) ->
120 let args = map (\x -> MN x "op") [0..] in
121 return (n, (LFun n (take ar args)
122 (LOp op (map (LV . Glob) (take ar args)))))
123 _ -> do def <- mkLDecl n d
124 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
125 return (n, def)
127declArgs args n (LLam xs x) = declArgs (args ++ xs) n x
128declArgs args n x = LFun n args x
130mkLDecl n (Function tm _) = do e <- ir tm
131 return (declArgs [] n e)
132mkLDecl n (CaseOp _ _ _ pats _ _ args sc) = do e <- ir (args, sc)
133 return (declArgs [] n e)
134mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
135mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
136mkLDecl n _ = return (LFun n [] (LError ("Impossible declaration " ++ show n)))
138instance ToIR (TT Name) where
139 ir tm = ir' [] tm where
140 ir' env tm@(App f a)
141 | (P _ (UN "mkForeign") _, args) <- unApply tm
142 = doForeign env args
143 | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm
144 = ir' env arg
145 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm
146 = do arg' <- ir' env arg
147 return $ LLazyExp arg'
148 | (P _ (UN "fork") _, [arg]) <- unApply tm
149 = do arg' <- ir' env arg
150 return $ LOp LFork [LLazyExp arg']
151 | (P _ (UN "prim__IO") _, [v]) <- unApply tm
152 = do v' <- ir' env v
153 return v'
154 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
155 = do v' <- ir' env v
156 k' <- ir' env k
157 return (LApp False k' [LForce v'])
158 | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
159 = do size' <- ir' env size
160 t' <- ir' env t
161 return t' -- TODO $ malloc_ size' t'
162 | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm
163 = do t' <- ir' env t
164 return t' -- TODO
165 | (P (DCon t a) n _, args) <- unApply tm
166 = irCon env t a n args
167 | (P _ n _, args) <- unApply tm
168 = do i <- get
169 let collapse = case lookupCtxt Nothing n (idris_optimisation i) of
170 [oi] -> collapsible oi
171 _ -> False
172 let unused = case lookupCtxt Nothing n (idris_callgraph i) of
173 [CGInfo _ _ _ _ unusedpos] -> unusedpos
174 _ -> []
175 args' <- mapM (ir' env) args
176 if collapse then return LNothing
177 else return (LApp False (LV (Glob n))
178 (mkUnused unused 0 args'))
179 | (f, args) <- unApply tm
180 = do f' <- ir' env f
181 args' <- mapM (ir' env) args
182 return (LApp False f' args')
183 where mkUnused u i [] = []
184 mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
185 | otherwise = x : mkUnused u (i + 1) xs
186 ir' env (P _ n _) = return $ LV (Glob n)
187 ir' env (V i) | i < length env = return $ LV (Glob (env!!i))
188 | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm
189 ir' env (Bind n (Lam _) sc)
190 = do let n' = uniqueName n env
191 sc' <- ir' (n' : env) sc
192 return $ LLam [n'] sc'
193 ir' env (Bind n (Let _ v) sc)
194 = do sc' <- ir' (n : env) sc
195 v' <- ir' env v
196 return $ LLet n v' sc'
197 ir' env (Bind _ _ _) = return $ LNothing
198 ir' env (Proj t i) = do t' <- ir' env t
199 return $ LProj t' i
200 ir' env (Constant c) = return $ LConst c
201 ir' env (Set _) = return $ LNothing
202 ir' env Erased = return $ LNothing
203 ir' env Impossible = return $ LNothing
204-- ir' env _ = return $ LError "Impossible"
206 irCon env t arity n args
207 | length args == arity = buildApp env (LV (Glob n)) args
208 | otherwise = let extra = satArgs (arity - length args) in
209 do sc' <- irCon env t arity n
210 (args ++ map (\n -> P Bound n undefined) extra)
211 return $ LLam extra sc'
213 satArgs n = map (\i -> MN i "sat") [1..n]
215 buildApp env e [] = return e
216 buildApp env e xs = do xs' <- mapM (ir' env) xs
217 return $ LApp False e xs'
219 doForeign :: [Name] -> [TT Name] -> Idris LExp
220 doForeign env (_ : fgn : args)
221 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
222 = let tys = getFTypes fgnArgTys
223 rty = mkIty' ret in
224 do args' <- mapM (ir' env) args
225 -- wrap it in a prim__IO
226 -- return $ con_ 0 @@ impossible @@
227 return $ LLazyExp $
228 LForeign LANG_C rty fgnName (zip tys args')
229 | otherwise = fail "Badly formed foreign function call"
231getFTypes :: TT Name -> [FType]
232getFTypes tm = case unApply tm of
233 (nil, []) -> []
234 (cons, [ty, xs]) ->
235 let rest = getFTypes xs in
236 mkIty' ty : rest
238mkIty' (P _ (UN ty) _) = mkIty ty
239mkIty' _ = FAny
241mkIty "FInt" = FInt
242mkIty "FFloat" = FDouble
243mkIty "FChar" = FChar
244mkIty "FString" = FString
245mkIty "FPtr" = FPtr
246mkIty "FUnit" = FUnit
248instance ToIR ([Name], SC) where
249 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
250 tree' <- ir tree
251 return $ LLam args tree'
253instance ToIR SC where
254 ir t = ir' t where
256 ir' (STerm t) = ir t
257 ir' (UnmatchedCase str) = return $ LError str
258 ir' (ProjCase tm alts) = do alts' <- mapM mkIRAlt alts
259 tm' <- ir tm
260 return $ LCase tm' alts'
261 ir' (Case n alts) = do alts' <- mapM mkIRAlt alts
262 return $ LCase (LV (Glob n)) alts'
263 ir' ImpossibleCase = return LNothing
265 mkIRAlt (ConCase n t args rhs)
266 = do rhs' <- ir rhs
267 return $ LConCase (-1) n args rhs'
268 mkIRAlt (ConstCase (I i) rhs)
269 = do rhs' <- ir rhs
270 return $ LConstCase (I i) rhs'
271 mkIRAlt (ConstCase IType rhs)
272 = do rhs' <- ir rhs
273 return $ LDefaultCase rhs'
274 mkIRAlt (ConstCase c rhs)
275 = fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"
276 mkIRAlt (DefaultCase rhs)
277 = do rhs' <- ir rhs
278 return $ LDefaultCase rhs'