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