git.iko.soy/Idris-dev
on dd7a2b2 help sign in
Idris-dev/src/IRTS/Compiler.hs
446 lines 18 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.Erasure
22import Idris.Error
24import Idris.Core.TT
25import Idris.Core.Evaluate
26import Idris.Core.CaseTree
28import Control.Monad.State
29import Data.List
30import qualified Data.IntMap as IM
31import qualified Data.IntSet as IS
32import qualified Data.Map as M
33import qualified Data.Set as S
34import System.Process
35import System.IO
36import System.Directory
37import System.Environment
38import System.FilePath ((</>), addTrailingPathSeparator)
40import Paths_idris
42compile :: Codegen -> FilePath -> Term -> Idris ()
43compile codegen f tm
44 = do checkMVs
45 let tmnames = namesUsed (STerm tm)
46 usedIn <- mapM (allNames []) tmnames
47 let used = sUN "prim__subBigInt" : sUN "prim__addBigInt" : concat usedIn
48 defsIn <- mkDecls tm used
49 findUnusedArgs used
51 -- TODO: traverse all names correctly
53 -- TODO: DEBUG-ONLY, remove
54 ist <- getIState
55 let depMap = buildDepMap (tt_ctxt ist) used
56 let printItem (cond, deps) = show (S.toList cond) ++ " -> " ++ show (S.toList deps)
57 iLOG $ "USAGE ANALYSIS:\n" ++ unlines (map printItem . M.toList $ depMap)
59 let minUse = minimalUsage depMap
60 iLOG $ "MINIMAL USAGE:\n" ++ unlines (map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) $ M.toList minUse)
61 -- END TODO
63 maindef <- irMain tm
64 objs <- getObjectFiles codegen
65 libs <- getLibs codegen
66 flags <- getFlags codegen
67 hdrs <- getHdrs codegen
68 impdirs <- allImportDirs
69 let defs = defsIn ++ [(sMN 0 "runMain", maindef)]
70 -- iputStrLn $ showSep "\n" (map show defs)
71 let (nexttag, tagged) = addTags 65536 (liftAll defs)
72 let ctxtIn = addAlist tagged emptyContext
73 iLOG "Defunctionalising"
74 let defuns_in = defunctionalise nexttag ctxtIn
75 logLvl 5 $ show defuns_in
76 iLOG "Inlining"
77 let defuns = inline defuns_in
78 logLvl 5 $ show defuns
79 iLOG "Resolving variables for CG"
80 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))
81 let checked = checkDefs defuns (toAlist defuns)
82 outty <- outputTy
83 dumpCases <- getDumpCases
84 dumpDefun <- getDumpDefun
85 case dumpCases of
86 Nothing -> return ()
87 Just f -> runIO $ writeFile f (showCaseTrees defs)
88 case dumpDefun of
89 Nothing -> return ()
90 Just f -> runIO $ writeFile f (dumpDefuns defuns)
91 triple <- Idris.AbsSyntax.targetTriple
92 cpu <- Idris.AbsSyntax.targetCPU
93 optimise <- optLevel
94 iLOG "Building output"
96 case checked of
97 OK c -> do let cginfo = CodegenInfo f outty triple cpu optimise
98 hdrs impdirs objs libs flags
99 NONE c (toAlist defuns)
100 tagged
101 runIO $ case codegen of
102 ViaC -> codegenC cginfo
103 ViaJava -> codegenJava cginfo
104 ViaJavaScript -> codegenJavaScript cginfo
105 ViaNode -> codegenNode cginfo
106 ViaLLVM -> codegenLLVM cginfo
107 Bytecode -> dumpBC c f
108 Error e -> ierror e
109 where checkMVs = do i <- getIState
110 case map fst (idris_metavars i) \\ primDefs of
111 [] -> return ()
112 ms -> ifail $ "There are undefined metavariables: " ++ show ms
113 inDir d h = do let f = d </> h
114 ex <- doesFileExist f
115 if ex then return f else return h
117irMain :: TT Name -> Idris LDecl
118irMain tm = do i <- ir tm
119 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
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 findUnusedArgs 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 -> sMN 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 $ (declArgs [] True n LNothing) -- postulate, never run
176instance ToIR (TT Name) where
177 ir tm = ir' [] tm where
178 ir' env tm@(App f a)
179 | (P _ (UN m) _, args) <- unApply tm,
180 m == txt "mkForeignPrim"
181 = doForeign env args
182 | (P _ (UN u) _, [_, arg]) <- unApply tm,
183 u == txt "unsafePerformPrimIO"
184 = ir' env arg
185 -- TMP HACK - until we get inlining.
186 | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,
187 r == txt "replace"
188 = ir' env arg
189 -- Laziness, the old way
190 | (P _ (UN l) _, [_, arg]) <- unApply tm,
191 l == txt "lazy"
192 = do arg' <- ir' env arg
193 error "lazy has crept in somehow"
194-- return $ LLazyExp arg'
195 | (P _ (UN l) _, [_, arg]) <- unApply tm,
196 l == txt "force"
197 = do arg' <- ir' env arg
198 return $ LForce arg'
199 -- Laziness, the new way
200 | (P _ (UN l) _, [arg]) <- unApply tm,
201 l == txt "Delay"
202 = do arg' <- ir' env arg
203 return $ LLazyExp arg'
204 | (P _ (UN l) _, [_, _, arg]) <- unApply tm,
205 l == txt "Force"
206 = do arg' <- ir' env arg
207 return $ LForce arg'
208 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
209 a == txt "assert_smaller"
210 = ir' env arg
211 | (P _ (UN a) _, [_, arg]) <- unApply tm,
212 a == txt "assert_total"
213 = ir' env arg
214 | (P _ (UN p) _, [_, arg]) <- unApply tm,
215 p == txt "par"
216 = do arg' <- ir' env arg
217 return $ LOp LPar [LLazyExp arg']
218 | (P _ (UN pf) _, [arg]) <- unApply tm,
219 pf == txt "prim_fork"
220 = do arg' <- ir' env arg
221 return $ LOp LFork [LLazyExp arg']
222 | (P _ (UN m) _, [_,size,t]) <- unApply tm,
223 m == txt "malloc"
224 = do size' <- ir' env size
225 t' <- ir' env t
226 return t' -- TODO $ malloc_ size' t'
227 | (P _ (UN tm) _, [_,t]) <- unApply tm,
228 tm == txt "trace_malloc"
229 = do t' <- ir' env t
230 return t' -- TODO
231 -- This case is here until we get more general inlining. It's just
232 -- a really common case, and the laziness hurts...
233 | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
234 (App (P _ (UN d') _) e)]) <- unApply tm,
235 be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"
236 = do x' <- ir' env x
237 t' <- ir' env t
238 e' <- ir' env e
239 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',
240 LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])
241 | (P (DCon t a) n _, args) <- unApply tm
242 = irCon env t a n args
243 | (P (TCon t a) n _, args) <- unApply tm
244 = return LNothing
245 | (P _ n _, args) <- unApply tm
246 = do i <- getIState
247 args' <- mapM (ir' env) args
248 case getPrim i n args' of
249 Just tm -> return tm
250 _ -> do
251 let collapse
252 = case lookupCtxtExact n
253 (idris_optimisation i) of
254 Just oi -> collapsible oi
255 _ -> False
256 let unused
257 = case lookupCtxtExact n
258 (idris_callgraph i) of
259 Just (CGInfo _ _ _ _ unusedpos) ->
260 unusedpos
261 _ -> []
262 if collapse
263 then return LNothing
264 else return (LApp False (LV (Glob n))
265 (mkUnused unused 0 args'))
266 | (f, args) <- unApply tm
267 = do f' <- ir' env f
268 args' <- mapM (ir' env) args
269 return (LApp False f' args')
270 where mkUnused u i [] = []
271 mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
272 | otherwise = x : mkUnused u (i + 1) xs
273-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
274-- = return $ LConst (BI 0)
275 ir' env (P _ n _) = return $ LV (Glob n)
276 ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
277 | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm
278 ir' env (Bind n (Lam _) sc)
279 = do let n' = uniqueName n env
280 sc' <- ir' (n' : env) sc
281 return $ LLam [n'] sc'
282 ir' env (Bind n (Let _ v) sc)
283 = do sc' <- ir' (n : env) sc
284 v' <- ir' env v
285 return $ LLet n v' sc'
286 ir' env (Bind _ _ _) = return $ LNothing
287 ir' env (Proj t i) | i == -1
288 = do t' <- ir' env t
289 return $ LOp (LMinus (ATInt ITBig))
290 [t', LConst (BI 1)]
291 ir' env (Proj t i) = do t' <- ir' env t
292 return $ LProj t' i
293 ir' env (Constant c) = return $ LConst c
294 ir' env (TType _) = return $ LNothing
295 ir' env Erased = return $ LNothing
296 ir' env Impossible = return $ LNothing
297-- ir' env _ = return $ LError "Impossible"
299 irCon env t arity n args
300 | length args == arity = buildApp env (LV (Glob n)) args
301 | otherwise = let extra = satArgs (arity - length args) in
302 do sc' <- irCon env t arity n
303 (args ++ map (\n -> P Bound n undefined) extra)
304 return $ LLam extra sc'
306 satArgs n = map (\i -> sMN i "sat") [1..n]
308 buildApp env e [] = return e
309 buildApp env e xs = do xs' <- mapM (ir' env) xs
310 return $ LApp False e xs'
312 doForeign :: [Name] -> [TT Name] -> Idris LExp
313 doForeign env (_ : fgn : args)
314 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
315 = let maybeTys = getFTypes fgnArgTys
316 rty = mkIty' ret in
317 case maybeTys of
318 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
319 Just tys -> do
320 args' <- mapM (ir' env) (init args)
321 -- wrap it in a prim__IO
322 -- return $ con_ 0 @@ impossible @@
323 return $ -- LLazyExp $
324 LForeign LANG_C rty fgnName (zip tys args')
325 | otherwise = ifail "Badly formed foreign function call"
327getFTypes :: TT Name -> Maybe [FType]
328getFTypes tm = case unApply tm of
329 (nil, []) -> Just []
330 (cons, [ty, xs]) ->
331 fmap (mkIty' ty :) (getFTypes xs)
332 _ -> Nothing
334mkIty' (P _ (UN ty) _) = mkIty (str ty)
335mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
336 | fi == txt "FIntT" = mkIntIty (str intTy)
337mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
338 | ff == txt "FFunction" && fa == txt "FAny" &&
339 io == txt "IO"
340 = FFunctionIO
341mkIty' (App (App (P _ (UN ff) _) _) _)
342 | ff == txt "FFunction" = FFunction
343mkIty' _ = FAny
345-- would be better if these FInt types were evaluated at compile time
346-- TODO: add %eval directive for such things
348mkIty "FFloat" = FArith ATFloat
349mkIty "FInt" = mkIntIty "ITNative"
350mkIty "FChar" = mkIntIty "ITChar"
351mkIty "FByte" = mkIntIty "IT8"
352mkIty "FShort" = mkIntIty "IT16"
353mkIty "FLong" = mkIntIty "IT64"
354mkIty "FBits8" = mkIntIty "IT8"
355mkIty "FBits16" = mkIntIty "IT16"
356mkIty "FBits32" = mkIntIty "IT32"
357mkIty "FBits64" = mkIntIty "IT64"
358mkIty "FString" = FString
359mkIty "FPtr" = FPtr
360mkIty "FManagedPtr" = FManagedPtr
361mkIty "FUnit" = FUnit
362mkIty "FFunction" = FFunction
363mkIty "FFunctionIO" = FFunctionIO
364mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
365mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
366mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
367mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
368mkIty x = error $ "Unknown type " ++ x
370mkIntIty "ITNative" = FArith (ATInt ITNative)
371mkIntIty "ITChar" = FArith (ATInt ITChar)
372mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
373mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
374mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
375mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
377zname = sNS (sUN "Z") ["Nat","Prelude"]
378sname = sNS (sUN "S") ["Nat","Prelude"]
380instance ToIR ([Name], SC) where
381 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
382 tree' <- ir tree
383 return $ LLam args tree'
385instance ToIR SC where
386 ir t = ir' t where
388 ir' (STerm t) = ir t
389 ir' (UnmatchedCase str) = return $ LError str
390 ir' (ProjCase tm alt) = do tm' <- ir tm
391 alt' <- mkIRAlt tm' alt
392 return $ LCase tm' [alt']
393 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
394 return $ LCase (LV (Glob n)) alts'
395 ir' ImpossibleCase = return LNothing
397 -- special cases for Z and S
398 -- Needs rethink: projections make this fail
399-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
400-- = mkIRAlt n (ConstCase (BI 0) rhs)
401-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
402-- = do n' <- ir n
403-- rhs' <- ir rhs
404-- return $ LDefaultCase
405-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
406-- rhs')
407 mkIRAlt _ (ConCase n t args rhs)
408 = do rhs' <- ir rhs
409 return $ LConCase (-1) n args rhs'
410 mkIRAlt _ (ConstCase x rhs)
411 | matchable x
412 = do rhs' <- ir rhs
413 return $ LConstCase x rhs'
414 | matchableTy x
415 = do rhs' <- ir rhs
416 return $ LDefaultCase rhs'
417 mkIRAlt tm (SucCase n rhs)
418 = do rhs' <- ir rhs
419 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
420 [tm,
421 LConst (BI 1)]) rhs')
422-- return $ LSucCase n rhs'
423 mkIRAlt _ (ConstCase c rhs)
424 = ifail $ "Can't match on (" ++ show c ++ ")"
425 mkIRAlt _ (DefaultCase rhs)
426 = do rhs' <- ir rhs
427 return $ LDefaultCase rhs'
429 matchable (I _) = True
430 matchable (BI _) = True
431 matchable (Ch _) = True
432 matchable (Str _) = True
433 matchable _ = False
435 matchableTy (AType (ATInt ITNative)) = True
436 matchableTy (AType (ATInt ITBig)) = True
437 matchableTy (AType (ATInt ITChar)) = True
438 matchableTy StrType = True
440 matchableTy (AType (ATInt (ITFixed IT8))) = True
441 matchableTy (AType (ATInt (ITFixed IT16))) = True
442 matchableTy (AType (ATInt (ITFixed IT32))) = True
443 matchableTy (AType (ATInt (ITFixed IT64))) = True
445 matchableTy _ = False