git.iko.soy/Idris-dev
on 436bf95 help sign in
Idris-dev/src/IRTS/Compiler.hs
383 lines 16 kB history raw
1{-# LANGUAGE PatternGuards, TypeSynonymInstances #-}
3module IRTS.Compiler where
5import IRTS.Lang
6import IRTS.Defunctionalise
7import IRTS.Simplified
8import IRTS.CodegenCommon
9import IRTS.CodegenC
10import IRTS.CodegenJava
11import IRTS.DumpBC
12import IRTS.CodegenJavaScript
13import IRTS.CodegenLLVM
14import IRTS.Inliner
16import Idris.AbsSyntax
17import Idris.UnusedArgs
19import Core.TT
20import Core.Evaluate
21import Core.CaseTree
23import Control.Monad.State
24import Data.List
25import System.Process
26import System.IO
27import System.Directory
28import System.Environment
29import System.FilePath ((</>), addTrailingPathSeparator)
31import Paths_idris
33compile :: Codegen -> FilePath -> Term -> Idris ()
34compile codegen f tm
35 = do checkMVs
36 let tmnames = namesUsed (STerm tm)
37 usedIn <- mapM (allNames []) tmnames
38 let used = [UN "prim__subBigInt", UN "prim__addBigInt"] : usedIn
39 defsIn <- mkDecls tm (concat used)
40 findUnusedArgs (concat used)
41 maindef <- irMain tm
42 objs <- getObjectFiles codegen
43 libs <- getLibs codegen
44 hdrs <- getHdrs codegen
45 let defs = defsIn ++ [(MN 0 "runMain", maindef)]
46 -- iputStrLn $ showSep "\n" (map show defs)
47 let (nexttag, tagged) = addTags 65536 (liftAll defs)
48 let ctxtIn = addAlist tagged emptyContext
49 iLOG "Defunctionalising"
50 let defuns_in = defunctionalise nexttag ctxtIn
51 logLvl 5 $ show defuns_in
52 iLOG "Inlining"
53 let defuns = inline defuns_in
54 logLvl 5 $ show defuns
55 iLOG "Resolving variables for CG"
56 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))
57 let checked = checkDefs defuns (toAlist defuns)
58 outty <- outputTy
59 dumpCases <- getDumpCases
60 dumpDefun <- getDumpDefun
61 case dumpCases of
62 Nothing -> return ()
63 Just f -> liftIO $ writeFile f (showCaseTrees tagged)
64 case dumpDefun of
65 Nothing -> return ()
66 Just f -> liftIO $ writeFile f (dumpDefuns defuns)
67 triple <- targetTriple
68 cpu <- targetCPU
69 optimize <- optLevel
70 iLOG "Building output"
71 case checked of
72 OK c -> liftIO $ case codegen of
73 ViaC ->
74 codegenC c f outty hdrs
75 (concatMap mkObj objs)
76 (concatMap mkLib libs) NONE
77 ViaJava ->
78 codegenJava [] c f hdrs libs outty
79 ViaJavaScript ->
80 codegenJavaScript JavaScript c f outty
81 ViaNode ->
82 codegenJavaScript Node c f outty
83 ViaLLVM -> codegenLLVM c triple cpu optimize f outty
85 Bytecode -> dumpBC c f
86 Error e -> fail $ show e
87 where checkMVs = do i <- getIState
88 case idris_metavars i \\ primDefs of
89 [] -> return ()
90 ms -> fail $ "There are undefined metavariables: " ++ show ms
91 inDir d h = do let f = d </> h
92 ex <- doesFileExist f
93 if ex then return f else return h
94 mkObj f = f ++ " "
95 mkLib l = "-l" ++ l ++ " "
99irMain :: TT Name -> Idris LDecl
100irMain tm = do i <- ir tm
101 return $ LFun [] (MN 0 "runMain") [] (LForce i)
103allNames :: [Name] -> Name -> Idris [Name]
104allNames ns n | n `elem` ns = return []
105allNames ns n = do i <- getIState
106 case lookupCtxt n (idris_callgraph i) of
107 [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
108 return (nub (n : concat more))
109 _ -> return [n]
111mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
112mkDecls t used
113 = do i <- getIState
114 let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
115 mapM traceUnused used
116 decls <- mapM build ds
117 return decls
119showCaseTrees :: [(Name, LDecl)] -> String
120showCaseTrees ds = showSep "\n\n" (map showCT ds)
121 where
122 showCT (n, LFun _ f args lexp)
123 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t "
124 ++ show lexp
125 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
127isCon (TyDecl _ _) = True
128isCon _ = False
130class ToIR a where
131 ir :: a -> Idris LExp
133build :: (Name, Def) -> Idris (Name, LDecl)
134build (n, d)
135 = do i <- getIState
136 case lookup n (idris_scprims i) of
137 Just (ar, op) ->
138 let args = map (\x -> MN x "op") [0..] in
139 return (n, (LFun [] n (take ar args)
140 (LOp op (map (LV . Glob) (take ar args)))))
141 _ -> do def <- mkLDecl n d
142 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
143 return (n, def)
145getPrim :: IState -> Name -> [LExp] -> Maybe LExp
146getPrim i n args = case lookup n (idris_scprims i) of
147 Just (ar, op) ->
148 if (ar == length args)
149 then return (LOp op args)
150 else Nothing
151 _ -> Nothing
153declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
154declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
156mkLDecl n (Function tm _) = do e <- ir tm
157 return (declArgs [] True n e)
158mkLDecl n (CaseOp _ inl _ _ pats _ _ args sc) = do e <- ir (args, sc)
159 return (declArgs [] inl n e)
160mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
161mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
162mkLDecl n _ = return (LFun [] n [] (LError ("Impossible declaration " ++ show n)))
164instance ToIR (TT Name) where
165 ir tm = ir' [] tm where
166 ir' env tm@(App f a)
167 | (P _ (UN "mkForeign") _, args) <- unApply tm
168 = doForeign env args
169 | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm
170 = ir' env arg
171 -- TMP HACK - until we get inlining.
172 | (P _ (UN "replace") _, [_, _, _, _, _, arg]) <- unApply tm
173 = ir' env arg
174 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm
175 = do arg' <- ir' env arg
176 return $ LLazyExp arg'
177 | (P _ (UN "assert_smaller") _, [_, _, _, arg]) <- unApply tm
178 = ir' env arg
179 | (P _ (UN "par") _, [_, arg]) <- unApply tm
180 = do arg' <- ir' env arg
181 return $ LOp LPar [LLazyExp arg']
182 | (P _ (UN "fork") _, [arg]) <- unApply tm
183 = do arg' <- ir' env arg
184 return $ LOp LFork [LLazyExp arg']
185 | (P _ (UN "prim__IO") _, [v]) <- unApply tm
186 = do v' <- ir' env v
187 return v'
188 | (P _ (UN "io_bind") _, [_,_,v,Bind n (Lam _) sc]) <- unApply tm
189 = do v' <- ir' env v
190 sc' <- ir' (n:env) sc
191 return (LLet n (LForce v') sc')
192 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
193 = do v' <- ir' env v
194 k' <- ir' env k
195 return (LApp False k' [LForce v'])
196 | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
197 = do size' <- ir' env size
198 t' <- ir' env t
199 return t' -- TODO $ malloc_ size' t'
200 | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm
201 = do t' <- ir' env t
202 return t' -- TODO
203-- | (P _ (NS (UN "S") ["Nat", "Prelude"]) _, [k]) <- unApply tm
204-- = do k' <- ir' env k
205-- return (LOp LBPlus [k', LConst (BI 1)])
206 | (P (DCon t a) n _, args) <- unApply tm
207 = irCon env t a n args
208 | (P _ n _, args) <- unApply tm
209 = do i <- getIState
210 args' <- mapM (ir' env) args
211 case getPrim i n args' of
212 Just tm -> return tm
213 _ -> do
214 let collapse
215 = case lookupCtxt n
216 (idris_optimisation i) of
217 [oi] -> collapsible oi
218 _ -> False
219 let unused
220 = case lookupCtxt n
221 (idris_callgraph i) of
222 [CGInfo _ _ _ _ unusedpos] ->
223 unusedpos
224 _ -> []
225 if collapse
226 then return LNothing
227 else return (LApp False (LV (Glob n))
228 (mkUnused unused 0 args'))
229 | (f, args) <- unApply tm
230 = do f' <- ir' env f
231 args' <- mapM (ir' env) args
232 return (LApp False f' args')
233 where mkUnused u i [] = []
234 mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
235 | otherwise = x : mkUnused u (i + 1) xs
236-- ir' env (P _ (NS (UN "O") ["Nat", "Prelude"]) _)
237-- = return $ LConst (BI 0)
238 ir' env (P _ n _) = return $ LV (Glob n)
239 ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
240 | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm
241 ir' env (Bind n (Lam _) sc)
242 = do let n' = uniqueName n env
243 sc' <- ir' (n' : env) sc
244 return $ LLam [n'] sc'
245 ir' env (Bind n (Let _ v) sc)
246 = do sc' <- ir' (n : env) sc
247 v' <- ir' env v
248 return $ LLet n v' sc'
249 ir' env (Bind _ _ _) = return $ LNothing
250 ir' env (Proj t i) = do t' <- ir' env t
251 return $ LProj t' i
252 ir' env (Constant c) = return $ LConst c
253 ir' env (TType _) = return $ LNothing
254 ir' env Erased = return $ LNothing
255 ir' env Impossible = return $ LNothing
256-- ir' env _ = return $ LError "Impossible"
258 irCon env t arity n args
259 | length args == arity = buildApp env (LV (Glob n)) args
260 | otherwise = let extra = satArgs (arity - length args) in
261 do sc' <- irCon env t arity n
262 (args ++ map (\n -> P Bound n undefined) extra)
263 return $ LLam extra sc'
265 satArgs n = map (\i -> MN i "sat") [1..n]
267 buildApp env e [] = return e
268 buildApp env e xs = do xs' <- mapM (ir' env) xs
269 return $ LApp False e xs'
271 doForeign :: [Name] -> [TT Name] -> Idris LExp
272 doForeign env (_ : fgn : args)
273 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
274 = let maybeTys = getFTypes fgnArgTys
275 rty = mkIty' ret in
276 case maybeTys of
277 Nothing -> fail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
278 Just tys -> do
279 args' <- mapM (ir' env) args
280 -- wrap it in a prim__IO
281 -- return $ con_ 0 @@ impossible @@
282 return $ -- LLazyExp $
283 LForeign LANG_C rty fgnName (zip tys args')
284 | otherwise = fail "Badly formed foreign function call"
286getFTypes :: TT Name -> Maybe [FType]
287getFTypes tm = case unApply tm of
288 (nil, []) -> Just []
289 (cons, [ty, xs]) ->
290 fmap (mkIty' ty :) (getFTypes xs)
291 _ -> Nothing
293mkIty' (P _ (UN ty) _) = mkIty ty
294mkIty' (App (P _ (UN "FIntT") _) (P _ (UN intTy) _)) = mkIntIty intTy
295mkIty' (App (App (P _ (UN "FFunction") _) _) (App (P _ (UN "FAny") _) (App (P _ (UN "IO") _) _))) = FFunctionIO
296mkIty' (App (App (P _ (UN "FFunction") _) _) _) = FFunction
297mkIty' _ = FAny
299-- would be better if these FInt types were evaluated at compile time
300-- TODO: add %eval directive for such things
302mkIty "FFloat" = FArith ATFloat
303mkIty "FInt" = mkIntIty "ITNative"
304mkIty "FChar" = mkIntIty "IT8"
305mkIty "FShort" = mkIntIty "IT16"
306mkIty "FLong" = mkIntIty "IT64"
307mkIty "FString" = FString
308mkIty "FPtr" = FPtr
309mkIty "FUnit" = FUnit
310mkIty "FFunction" = FFunction
311mkIty "FFunctionIO" = FFunctionIO
312mkIty x = error $ "Unknown type " ++ x
314mkIntIty "ITNative" = FArith (ATInt ITNative)
315mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
316mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
317mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
318mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
320zname = NS (UN "O") ["Nat","Prelude"]
321sname = NS (UN "S") ["Nat","Prelude"]
323instance ToIR ([Name], SC) where
324 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
325 tree' <- ir tree
326 return $ LLam args tree'
328instance ToIR SC where
329 ir t = ir' t where
331 ir' (STerm t) = ir t
332 ir' (UnmatchedCase str) = return $ LError str
333 ir' (ProjCase tm alts) = do alts' <- mapM (mkIRAlt tm) alts
334 tm' <- ir tm
335 return $ LCase tm' alts'
336 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (P Bound n Erased)) alts
337 return $ LCase (LV (Glob n)) alts'
338 ir' ImpossibleCase = return LNothing
340 -- special cases for O and S
341 -- Needs rethink: projections make this fail
342-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
343-- = mkIRAlt n (ConstCase (BI 0) rhs)
344-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
345-- = do n' <- ir n
346-- rhs' <- ir rhs
347-- return $ LDefaultCase
348-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
349-- rhs')
350 mkIRAlt _ (ConCase n t args rhs)
351 = do rhs' <- ir rhs
352 return $ LConCase (-1) n args rhs'
353 mkIRAlt _ (ConstCase x rhs)
354 | matchable x
355 = do rhs' <- ir rhs
356 return $ LConstCase x rhs'
357 | matchableTy x
358 = do rhs' <- ir rhs
359 return $ LDefaultCase rhs'
360 mkIRAlt _ (ConstCase c rhs)
361 = fail $ "Can't match on (" ++ show c ++ ")"
362 mkIRAlt _ (DefaultCase rhs)
363 = do rhs' <- ir rhs
364 return $ LDefaultCase rhs'
366 matchable (I _) = True
367 matchable (BI _) = True
368 matchable (Ch _) = True
369 matchable (Str _) = True
370 matchable _ = False
372 matchableTy (AType (ATInt ITNative)) = True
373 matchableTy (AType (ATInt ITBig)) = True
374 matchableTy ChType = True
375 matchableTy StrType = True
377 matchableTy (AType (ATInt (ITFixed IT8))) = True
378 matchableTy (AType (ATInt (ITFixed IT16))) = True
379 matchableTy (AType (ATInt (ITFixed IT32))) = True
380 matchableTy (AType (ATInt (ITFixed IT64))) = True
382 matchableTy _ = False