git.iko.soy/Idris-dev
on da67875 help sign in
Idris-dev/src/IRTS/Compiler.hs
448 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 printCond (ctors, cond) = "if " ++ show (S.toList cond) ++ " -ctors- " ++ show (S.toList ctors)
57 let printDep (i, conds) = unlines . map (" "++) $ (show i : map printCond (S.toList conds))
58 let printItem (fn, deps) = unlines (show fn : map printDep (IM.toList deps))
59 iLOG $ "USAGE ANALYSIS:\n" ++ unlines (map printItem . M.toList $ depMap)
61 let minUse = minimalUsage depMap
62 iLOG $ "MINIMAL USAGE:\n" ++ unlines (map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) $ M.toList minUse)
63 -- END TODO
65 maindef <- irMain tm
66 objs <- getObjectFiles codegen
67 libs <- getLibs codegen
68 flags <- getFlags codegen
69 hdrs <- getHdrs codegen
70 impdirs <- allImportDirs
71 let defs = defsIn ++ [(sMN 0 "runMain", maindef)]
72 -- iputStrLn $ showSep "\n" (map show defs)
73 let (nexttag, tagged) = addTags 65536 (liftAll defs)
74 let ctxtIn = addAlist tagged emptyContext
75 iLOG "Defunctionalising"
76 let defuns_in = defunctionalise nexttag ctxtIn
77 logLvl 5 $ show defuns_in
78 iLOG "Inlining"
79 let defuns = inline defuns_in
80 logLvl 5 $ show defuns
81 iLOG "Resolving variables for CG"
82 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))
83 let checked = checkDefs defuns (toAlist defuns)
84 outty <- outputTy
85 dumpCases <- getDumpCases
86 dumpDefun <- getDumpDefun
87 case dumpCases of
88 Nothing -> return ()
89 Just f -> runIO $ writeFile f (showCaseTrees defs)
90 case dumpDefun of
91 Nothing -> return ()
92 Just f -> runIO $ writeFile f (dumpDefuns defuns)
93 triple <- Idris.AbsSyntax.targetTriple
94 cpu <- Idris.AbsSyntax.targetCPU
95 optimise <- optLevel
96 iLOG "Building output"
98 case checked of
99 OK c -> do let cginfo = CodegenInfo f outty triple cpu optimise
100 hdrs impdirs objs libs flags
101 NONE c (toAlist defuns)
102 tagged
103 runIO $ case codegen of
104 ViaC -> codegenC cginfo
105 ViaJava -> codegenJava cginfo
106 ViaJavaScript -> codegenJavaScript cginfo
107 ViaNode -> codegenNode cginfo
108 ViaLLVM -> codegenLLVM cginfo
109 Bytecode -> dumpBC c f
110 Error e -> ierror e
111 where checkMVs = do i <- getIState
112 case map fst (idris_metavars i) \\ primDefs of
113 [] -> return ()
114 ms -> ifail $ "There are undefined metavariables: " ++ show ms
115 inDir d h = do let f = d </> h
116 ex <- doesFileExist f
117 if ex then return f else return h
119irMain :: TT Name -> Idris LDecl
120irMain tm = do i <- ir tm
121 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
123mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
124mkDecls t used
125 = do i <- getIState
126 let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
127 findUnusedArgs used
128 decls <- mapM build ds
129 return decls
131showCaseTrees :: [(Name, LDecl)] -> String
132showCaseTrees ds = showSep "\n\n" (map showCT ds)
133 where
134 showCT (n, LFun _ f args lexp)
135 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t "
136 ++ show lexp
137 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
139isCon (TyDecl _ _) = True
140isCon _ = False
142class ToIR a where
143 ir :: a -> Idris LExp
145build :: (Name, Def) -> Idris (Name, LDecl)
146build (n, d)
147 = do i <- getIState
148 case lookup n (idris_scprims i) of
149 Just (ar, op) ->
150 let args = map (\x -> sMN x "op") [0..] in
151 return (n, (LFun [] n (take ar args)
152 (LOp op (map (LV . Glob) (take ar args)))))
153 _ -> do def <- mkLDecl n d
154 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
155 return (n, def)
157getPrim :: IState -> Name -> [LExp] -> Maybe LExp
158getPrim i n args = case lookup n (idris_scprims i) of
159 Just (ar, op) ->
160 if (ar == length args)
161 then return (LOp op args)
162 else Nothing
163 _ -> Nothing
165declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
166declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
168mkLDecl n (Function tm _) = do e <- ir tm
169 return (declArgs [] True n e)
170mkLDecl n (CaseOp ci _ _ _ pats cd)
171 = let (args, sc) = cases_runtime cd in
172 do e <- ir (args, sc)
173 return (declArgs [] (case_inlinable ci) n e)
174mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
175mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
176mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
178instance ToIR (TT Name) where
179 ir tm = ir' [] tm where
180 ir' env tm@(App f a)
181 | (P _ (UN m) _, args) <- unApply tm,
182 m == txt "mkForeignPrim"
183 = doForeign env args
184 | (P _ (UN u) _, [_, arg]) <- unApply tm,
185 u == txt "unsafePerformPrimIO"
186 = ir' env arg
187 -- TMP HACK - until we get inlining.
188 | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,
189 r == txt "replace"
190 = ir' env arg
191 -- Laziness, the old way
192 | (P _ (UN l) _, [_, arg]) <- unApply tm,
193 l == txt "lazy"
194 = do arg' <- ir' env arg
195 error "lazy has crept in somehow"
196-- return $ LLazyExp arg'
197 | (P _ (UN l) _, [_, arg]) <- unApply tm,
198 l == txt "force"
199 = do arg' <- ir' env arg
200 return $ LForce arg'
201 -- Laziness, the new way
202 | (P _ (UN l) _, [arg]) <- unApply tm,
203 l == txt "Delay"
204 = do arg' <- ir' env arg
205 return $ LLazyExp arg'
206 | (P _ (UN l) _, [_, _, arg]) <- unApply tm,
207 l == txt "Force"
208 = do arg' <- ir' env arg
209 return $ LForce arg'
210 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
211 a == txt "assert_smaller"
212 = ir' env arg
213 | (P _ (UN a) _, [_, arg]) <- unApply tm,
214 a == txt "assert_total"
215 = ir' env arg
216 | (P _ (UN p) _, [_, arg]) <- unApply tm,
217 p == txt "par"
218 = do arg' <- ir' env arg
219 return $ LOp LPar [LLazyExp arg']
220 | (P _ (UN pf) _, [arg]) <- unApply tm,
221 pf == txt "prim_fork"
222 = do arg' <- ir' env arg
223 return $ LOp LFork [LLazyExp arg']
224 | (P _ (UN m) _, [_,size,t]) <- unApply tm,
225 m == txt "malloc"
226 = do size' <- ir' env size
227 t' <- ir' env t
228 return t' -- TODO $ malloc_ size' t'
229 | (P _ (UN tm) _, [_,t]) <- unApply tm,
230 tm == txt "trace_malloc"
231 = do t' <- ir' env t
232 return t' -- TODO
233 -- This case is here until we get more general inlining. It's just
234 -- a really common case, and the laziness hurts...
235 | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
236 (App (P _ (UN d') _) e)]) <- unApply tm,
237 be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"
238 = do x' <- ir' env x
239 t' <- ir' env t
240 e' <- ir' env e
241 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',
242 LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])
243 | (P (DCon t a) n _, args) <- unApply tm
244 = irCon env t a n args
245 | (P (TCon t a) n _, args) <- unApply tm
246 = return LNothing
247 | (P _ n _, args) <- unApply tm
248 = do i <- getIState
249 args' <- mapM (ir' env) args
250 case getPrim i n args' of
251 Just tm -> return tm
252 _ -> do
253 let collapse
254 = case lookupCtxtExact n
255 (idris_optimisation i) of
256 Just oi -> collapsible oi
257 _ -> False
258 let unused
259 = case lookupCtxtExact n
260 (idris_callgraph i) of
261 Just (CGInfo _ _ _ _ unusedpos) ->
262 unusedpos
263 _ -> []
264 if collapse
265 then return LNothing
266 else return (LApp False (LV (Glob n))
267 (mkUnused unused 0 args'))
268 | (f, args) <- unApply tm
269 = do f' <- ir' env f
270 args' <- mapM (ir' env) args
271 return (LApp False f' args')
272 where mkUnused u i [] = []
273 mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
274 | otherwise = x : mkUnused u (i + 1) xs
275-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
276-- = return $ LConst (BI 0)
277 ir' env (P _ n _) = return $ LV (Glob n)
278 ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
279 | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm
280 ir' env (Bind n (Lam _) sc)
281 = do let n' = uniqueName n env
282 sc' <- ir' (n' : env) sc
283 return $ LLam [n'] sc'
284 ir' env (Bind n (Let _ v) sc)
285 = do sc' <- ir' (n : env) sc
286 v' <- ir' env v
287 return $ LLet n v' sc'
288 ir' env (Bind _ _ _) = return $ LNothing
289 ir' env (Proj t i) | i == -1
290 = do t' <- ir' env t
291 return $ LOp (LMinus (ATInt ITBig))
292 [t', LConst (BI 1)]
293 ir' env (Proj t i) = do t' <- ir' env t
294 return $ LProj t' i
295 ir' env (Constant c) = return $ LConst c
296 ir' env (TType _) = return $ LNothing
297 ir' env Erased = return $ LNothing
298 ir' env Impossible = return $ LNothing
299-- ir' env _ = return $ LError "Impossible"
301 irCon env t arity n args
302 | length args == arity = buildApp env (LV (Glob n)) args
303 | otherwise = let extra = satArgs (arity - length args) in
304 do sc' <- irCon env t arity n
305 (args ++ map (\n -> P Bound n undefined) extra)
306 return $ LLam extra sc'
308 satArgs n = map (\i -> sMN i "sat") [1..n]
310 buildApp env e [] = return e
311 buildApp env e xs = do xs' <- mapM (ir' env) xs
312 return $ LApp False e xs'
314 doForeign :: [Name] -> [TT Name] -> Idris LExp
315 doForeign env (_ : fgn : args)
316 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
317 = let maybeTys = getFTypes fgnArgTys
318 rty = mkIty' ret in
319 case maybeTys of
320 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
321 Just tys -> do
322 args' <- mapM (ir' env) (init args)
323 -- wrap it in a prim__IO
324 -- return $ con_ 0 @@ impossible @@
325 return $ -- LLazyExp $
326 LForeign LANG_C rty fgnName (zip tys args')
327 | otherwise = ifail "Badly formed foreign function call"
329getFTypes :: TT Name -> Maybe [FType]
330getFTypes tm = case unApply tm of
331 (nil, []) -> Just []
332 (cons, [ty, xs]) ->
333 fmap (mkIty' ty :) (getFTypes xs)
334 _ -> Nothing
336mkIty' (P _ (UN ty) _) = mkIty (str ty)
337mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
338 | fi == txt "FIntT" = mkIntIty (str intTy)
339mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
340 | ff == txt "FFunction" && fa == txt "FAny" &&
341 io == txt "IO"
342 = FFunctionIO
343mkIty' (App (App (P _ (UN ff) _) _) _)
344 | ff == txt "FFunction" = FFunction
345mkIty' _ = FAny
347-- would be better if these FInt types were evaluated at compile time
348-- TODO: add %eval directive for such things
350mkIty "FFloat" = FArith ATFloat
351mkIty "FInt" = mkIntIty "ITNative"
352mkIty "FChar" = mkIntIty "ITChar"
353mkIty "FByte" = mkIntIty "IT8"
354mkIty "FShort" = mkIntIty "IT16"
355mkIty "FLong" = mkIntIty "IT64"
356mkIty "FBits8" = mkIntIty "IT8"
357mkIty "FBits16" = mkIntIty "IT16"
358mkIty "FBits32" = mkIntIty "IT32"
359mkIty "FBits64" = mkIntIty "IT64"
360mkIty "FString" = FString
361mkIty "FPtr" = FPtr
362mkIty "FManagedPtr" = FManagedPtr
363mkIty "FUnit" = FUnit
364mkIty "FFunction" = FFunction
365mkIty "FFunctionIO" = FFunctionIO
366mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
367mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
368mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
369mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
370mkIty x = error $ "Unknown type " ++ x
372mkIntIty "ITNative" = FArith (ATInt ITNative)
373mkIntIty "ITChar" = FArith (ATInt ITChar)
374mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
375mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
376mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
377mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
379zname = sNS (sUN "Z") ["Nat","Prelude"]
380sname = sNS (sUN "S") ["Nat","Prelude"]
382instance ToIR ([Name], SC) where
383 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
384 tree' <- ir tree
385 return $ LLam args tree'
387instance ToIR SC where
388 ir t = ir' t where
390 ir' (STerm t) = ir t
391 ir' (UnmatchedCase str) = return $ LError str
392 ir' (ProjCase tm alt) = do tm' <- ir tm
393 alt' <- mkIRAlt tm' alt
394 return $ LCase tm' [alt']
395 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
396 return $ LCase (LV (Glob n)) alts'
397 ir' ImpossibleCase = return LNothing
399 -- special cases for Z and S
400 -- Needs rethink: projections make this fail
401-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
402-- = mkIRAlt n (ConstCase (BI 0) rhs)
403-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
404-- = do n' <- ir n
405-- rhs' <- ir rhs
406-- return $ LDefaultCase
407-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
408-- rhs')
409 mkIRAlt _ (ConCase n t args rhs)
410 = do rhs' <- ir rhs
411 return $ LConCase (-1) n args rhs'
412 mkIRAlt _ (ConstCase x rhs)
413 | matchable x
414 = do rhs' <- ir rhs
415 return $ LConstCase x rhs'
416 | matchableTy x
417 = do rhs' <- ir rhs
418 return $ LDefaultCase rhs'
419 mkIRAlt tm (SucCase n rhs)
420 = do rhs' <- ir rhs
421 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
422 [tm,
423 LConst (BI 1)]) rhs')
424-- return $ LSucCase n rhs'
425 mkIRAlt _ (ConstCase c rhs)
426 = ifail $ "Can't match on (" ++ show c ++ ")"
427 mkIRAlt _ (DefaultCase rhs)
428 = do rhs' <- ir rhs
429 return $ LDefaultCase rhs'
431 matchable (I _) = True
432 matchable (BI _) = True
433 matchable (Ch _) = True
434 matchable (Str _) = True
435 matchable _ = False
437 matchableTy (AType (ATInt ITNative)) = True
438 matchableTy (AType (ATInt ITBig)) = True
439 matchableTy (AType (ATInt ITChar)) = True
440 matchableTy StrType = True
442 matchableTy (AType (ATInt (ITFixed IT8))) = True
443 matchableTy (AType (ATInt (ITFixed IT16))) = True
444 matchableTy (AType (ATInt (ITFixed IT32))) = True
445 matchableTy (AType (ATInt (ITFixed IT64))) = True
447 matchableTy _ = False