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