git.iko.soy/Idris-dev
on ca257e0 help sign in
Idris-dev/src/IRTS/Compiler.hs
511 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.AbsSyntaxTree
22import Idris.Erasure
23import Idris.Error
25import Debug.Trace
27import Idris.Core.TT
28import Idris.Core.Evaluate
29import Idris.Core.CaseTree
31import Control.Applicative
32import Control.Monad.State
33import Data.Maybe
34import Data.List
35import Data.IntSet (IntSet)
36import qualified Data.IntSet as IS
37import qualified Data.Map as M
38import qualified Data.Set as S
39import System.Process
40import System.IO
41import System.Directory
42import System.Environment
43import System.FilePath ((</>), addTrailingPathSeparator)
45import Paths_idris
47compile :: Codegen -> FilePath -> Term -> Idris ()
48compile codegen f tm
49 = do checkMVs -- check for undefined metavariables
50 reachableNames <- performUsageAnalysis
51 maindef <- irMain tm
52 iLOG $ "MAIN: " ++ show maindef
53 objs <- getObjectFiles codegen
54 libs <- getLibs codegen
55 flags <- getFlags codegen
56 hdrs <- getHdrs codegen
57 impdirs <- allImportDirs
58 defsIn <- mkDecls tm reachableNames
59 let defs = defsIn ++ [(sMN 0 "runMain", maindef)]
60 -- iputStrLn $ showSep "\n" (map show defs)
61 let (nexttag, tagged) = addTags 65536 (liftAll defs)
62 let ctxtIn = addAlist tagged emptyContext
63 iLOG "Defunctionalising"
64 let defuns_in = defunctionalise nexttag ctxtIn
65 logLvl 5 $ show defuns_in
66 iLOG "Inlining"
67 let defuns = inline defuns_in
68 logLvl 5 $ show defuns
69 iLOG "Resolving variables for CG"
70 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))
71 let checked = checkDefs defuns (toAlist defuns)
72 outty <- outputTy
73 dumpCases <- getDumpCases
74 dumpDefun <- getDumpDefun
75 case dumpCases of
76 Nothing -> return ()
77 Just f -> runIO $ writeFile f (showCaseTrees defs)
78 case dumpDefun of
79 Nothing -> return ()
80 Just f -> runIO $ writeFile f (dumpDefuns defuns)
81 triple <- Idris.AbsSyntax.targetTriple
82 cpu <- Idris.AbsSyntax.targetCPU
83 optimise <- optLevel
84 iLOG "Building output"
86 case checked of
87 OK c -> do let cginfo = CodegenInfo f outty triple cpu optimise
88 hdrs impdirs objs libs flags
89 NONE c (toAlist defuns)
90 tagged
91 runIO $ case codegen of
92 ViaC -> codegenC cginfo
93 ViaJava -> codegenJava cginfo
94 ViaJavaScript -> codegenJavaScript cginfo
95 ViaNode -> codegenNode cginfo
96 ViaLLVM -> codegenLLVM cginfo
97 Bytecode -> dumpBC c f
98 Error e -> ierror e
99 where checkMVs = do i <- getIState
100 case map fst (idris_metavars i) \\ primDefs of
101 [] -> return ()
102 ms -> ifail $ "There are undefined metavariables: " ++ show ms
103 inDir d h = do let f = d </> h
104 ex <- doesFileExist f
105 if ex then return f else return h
107irMain :: TT Name -> Idris LDecl
108irMain tm = do
109 i <- irTerm M.empty [] tm
110 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
112mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
113mkDecls t used
114 = do i <- getIState
115 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
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
130build :: (Name, Def) -> Idris (Name, LDecl)
131build (n, d)
132 = do i <- getIState
133 case lookup n (idris_scprims i) of
134 Just (ar, op) ->
135 let args = map (\x -> sMN x "op") [0..] in
136 return (n, (LFun [] n (take ar args)
137 (LOp op (map (LV . Glob) (take ar args)))))
138 _ -> do def <- mkLDecl n d
139 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
140 return (n, def)
142declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
143declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
145mkLDecl n (Function tm _)
146 = declArgs [] True n <$> irTerm M.empty [] tm
148mkLDecl n (CaseOp ci _ _ _ pats cd)
149 = declArgs [] (case_inlinable ci) n <$> irTree args sc
150 where
151 (args, sc) = cases_runtime cd
153mkLDecl n (TyDecl (DCon tag arity) _) =
154 LConstructor n tag . erasedArity . lookup n <$> getIState
155 where
156 lookup n = lookupCtxtExact n . idris_callgraph
157 erasedArity = maybe 0 (length . usedpos)
159mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
160mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
162data VarInfo = VI
163 { viMethod :: Maybe Name
164 }
165 deriving Show
167type Vars = M.Map Name VarInfo
169irTerm :: Vars -> [Name] -> Term -> Idris LExp
170irTerm vs env tm@(App f a) = case unApply tm of
171 (P _ (UN m) _, args)
172 | m == txt "mkForeignPrim"
173 -> doForeign vs env args
175 (P _ (UN u) _, [_, arg])
176 | u == txt "unsafePerformPrimIO"
177 -> irTerm vs env arg
179 -- TMP HACK - until we get inlining.
180 (P _ (UN r) _, [_, _, _, _, _, arg])
181 | r == txt "replace"
182 -> irTerm vs env arg
184 -- Laziness, the old way
185 (P _ (UN l) _, [_, arg])
186 | l == txt "lazy"
187 -> error "lazy has crept in somehow"
189 (P _ (UN l) _, [_, arg])
190 | l == txt "force"
191 -> LForce <$> irTerm vs env arg
193 -- Laziness, the new way
194 (P _ (UN l) _, [_, arg])
195 | l == txt "Delay"
196 -> LLazyExp <$> irTerm vs env arg
198 (P _ (UN l) _, [_, arg])
199 | l == txt "Force"
200 -> LForce <$> irTerm vs env arg
202 (P _ (UN a) _, [_, _, arg])
203 | a == txt "assert_smaller"
204 -> irTerm vs env arg
206 (P _ (UN a) _, [_, arg])
207 | a == txt "assert_total"
208 -> irTerm vs env arg
210 (P _ (UN p) _, [_, arg])
211 | p == txt "par"
212 -> do arg' <- irTerm vs env arg
213 return $ LOp LPar [LLazyExp arg']
215 (P _ (UN pf) _, [arg])
216 | pf == txt "prim_fork"
217 -> do arg' <- irTerm vs env arg
218 return $ LOp LFork [LLazyExp arg']
220 (P _ (UN m) _, [_,size,t])
221 | m == txt "malloc"
222 -> irTerm vs env t
224 (P _ (UN tm) _, [_,t])
225 | tm == txt "trace_malloc"
226 -> irTerm vs env t -- TODO
228 -- This case is here until we get more general inlining. It's just
229 -- a really common case, and the laziness hurts...
230 (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
231 (App (P _ (UN d') _) e)])
232 | be == txt "boolElim"
233 , d == txt "Delay"
234 , d' == txt "Delay"
235 -> do
236 x' <- irTerm vs env x
237 t' <- irTerm vs env t
238 e' <- irTerm vs env e
239 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
240 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
241 ])
243 (P (DCon t arity) n _, args) -> do
244 ist <- getIState
245 let detag = maybe False detaggable . lookupCtxtExact n $ idris_optimisation ist
246 used = maybe [] (map fst . usedpos) . lookupCtxtExact n $ idris_callgraph ist
247 args' = [a | (i,a) <- zip [0..] args, i `elem` used]
249 when (length args > arity) $
250 ifail ("oversaturated data ctor: " ++ show tm)
252 if length args' == 1 && detag -- detaggable
253 then irTerm vs env (head args') -- newtype
254 else irCon vs env (length used) n args'
256 (P (TCon t a) n _, args) -> return LNothing
258 (P _ n _, args) -> do
259 ist <- getIState
260 case lookup n (idris_scprims ist) of
261 -- if it's a primitive that is already saturated,
262 -- compile to the corresponding op here already to save work
263 Just (arity, op) | length args == arity
264 -> LOp op <$> mapM (irTerm vs env) args
266 -- otherwise, just apply the name
267 _ -> applyName n ist args
269 (f, args)
270 -> LApp False
271 <$> irTerm vs env f
272 <*> mapM (irTerm vs env) args
274 where
275 applyName :: Name -> IState -> [Term] -> Idris LExp
276 applyName n ist args =
277 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
278 where
279 erase (i, x)
280 | i >= arity || i `elem` used = x
281 | otherwise = Erased
283 arity = case fst4 <$> lookupCtxt n (definitions . tt_ctxt $ ist) of
284 [CaseOp ci ty tys def tot cdefs] -> length tys
285 [TyDecl (DCon tag ar) _] -> ar
286 [TyDecl Ref ty] -> length $ getArgTys ty
287 [Operator ty ar op] -> ar
288 [] -> 0 -- no definition, probably local name => can't erase anything
289 def -> error $ "unknown arity: " ++ show (n, def)
291 used = maybe [] (map fst . usedpos) $ lookupCtxtExact n (idris_callgraph ist)
292 fst4 (x,_,_,_) = x
294irTerm vs env (P _ n _) = return $ LV (Glob n)
295irTerm vs env (V i)
296 | i >= 0 && i < length env = return $ LV (Glob (env!!i))
297 | otherwise = ifail $ "bad de bruijn index: " ++ show i
299irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc
300 where
301 n' = uniqueName n env
303irTerm vs env (Bind n (Let _ v) sc)
304 = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc
306irTerm vs env (Bind _ _ _) = return $ LNothing
308irTerm vs env (Proj t (-1)) = do
309 t' <- irTerm vs env t
310 return $ LOp (LMinus (ATInt ITBig))
311 [t', LConst (BI 1)]
313irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i
314irTerm vs env (Constant c) = return $ LConst c
315irTerm vs env (TType _) = return $ LNothing
316irTerm vs env Erased = return $ LNothing
317irTerm vs env Impossible = return $ LNothing
318-- ir' env _ = return $ LError "Impossible"
320irCon :: Vars -> [Name] -> Int -> Name -> [Term] -> Idris LExp
321irCon vs env arity n args
322 | length args > arity
323 = error $ "oversaturated data constructor: " ++ show (n, args)
325 -- saturated
326 | length args == arity
327 = buildApp (LV (Glob n)) args
329 -- undersaturated, wrap in lambdas
330 | otherwise
331 = let extraNs = [sMN i "sat" | i <- [length args .. arity-1]]
332 extraTs = [P Bound n undefined | n <- extraNs]
333 in LLam extraNs <$> irCon vs env arity n (args ++ extraTs)
334 where
335 buildApp e [] = return e
336 buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
338doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp
339doForeign vs env (_ : fgn : args)
340 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
341 = case getFTypes fgnArgTys of
342 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
343 Just tys -> do
344 args' <- mapM (irTerm vs env) (init args)
345 return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')
347 | otherwise = ifail "Badly formed foreign function call"
348 where
349 getFTypes :: TT Name -> Maybe [FType]
350 getFTypes tm = case unApply tm of
351 -- nil : {a : Type} -> List a
352 (nil, [_]) -> Just []
353 -- cons : {a : Type} -> a -> List a -> List a
354 (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
355 _ -> Nothing
357 mkIty' (P _ (UN ty) _) = mkIty (str ty)
358 mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
359 | fi == txt "FIntT"
360 = mkIntIty (str intTy)
362 mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
363 | ff == txt "FFunction"
364 , fa == txt "FAny"
365 , io == txt "IO"
366 = FFunctionIO
368 mkIty' (App (App (P _ (UN ff) _) _) _)
369 | ff == txt "FFunction"
370 = FFunction
372 mkIty' _ = FAny
374 -- would be better if these FInt types were evaluated at compile time
375 -- TODO: add %eval directive for such things
377 mkIty "FFloat" = FArith ATFloat
378 mkIty "FInt" = mkIntIty "ITNative"
379 mkIty "FChar" = mkIntIty "ITChar"
380 mkIty "FByte" = mkIntIty "IT8"
381 mkIty "FShort" = mkIntIty "IT16"
382 mkIty "FLong" = mkIntIty "IT64"
383 mkIty "FBits8" = mkIntIty "IT8"
384 mkIty "FBits16" = mkIntIty "IT16"
385 mkIty "FBits32" = mkIntIty "IT32"
386 mkIty "FBits64" = mkIntIty "IT64"
387 mkIty "FString" = FString
388 mkIty "FPtr" = FPtr
389 mkIty "FManagedPtr" = FManagedPtr
390 mkIty "FUnit" = FUnit
391 mkIty "FFunction" = FFunction
392 mkIty "FFunctionIO" = FFunctionIO
393 mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
394 mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
395 mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
396 mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
397 mkIty x = error $ "Unknown type " ++ x
399 mkIntIty "ITNative" = FArith (ATInt ITNative)
400 mkIntIty "ITChar" = FArith (ATInt ITChar)
401 mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
402 mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
403 mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
404 mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
406irTree :: [Name] -> SC -> Idris LExp
407irTree args tree = do
408 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
409 LLam args <$> irSC M.empty tree
411irSC :: Vars -> SC -> Idris LExp
412irSC vs (STerm t) = irTerm vs [] t
413irSC vs (UnmatchedCase str) = return $ LError str
414irSC vs (ProjCase tm alt) = do
415 tm' <- irTerm vs [] tm
416 alt' <- irAlt vs tm' alt
417 return $ LCase tm' [alt']
419-- There are two transformations in this case:
420--
421-- 1. Newtype-case elimination:
422-- case {e0} of
423-- wrap({e1}) -> P({e1}) ==> P({e0})
424--
425-- This is important because newtyped constructors are compiled away entirely
426-- and we need to do that everywhere.
427--
428-- 2. Unused-case elimination:
429-- case {e0} of ==> P
430-- C(x,y) -> P[... x,y not used ...]
431--
432-- This is important for runtime because sometimes we case on irrelevant data:
433--
434-- In the example above, {e0} will most probably have been erased
435-- so this vain projection would make the resulting program segfault
436-- because the code generator still emits a PROJECT(...) STG instruction.
437--
438-- Hence, we check whether the variables are used at all
439-- and erase the casesplit if they are not.
440irSC vs (Case n [alt]) = do
441 replacement <- case alt of
442 ConCase cn a ns sc -> do
443 detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState
444 used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState
445 if detag && length used == 1
446 then return . Just $ substSC (ns !! head used) n sc
447 else return Nothing
448 _ -> return Nothing
450 case replacement of
451 Just sc -> irSC vs sc
452 _ -> do
453 alt' <- irAlt vs (LV (Glob n)) alt
454 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
455 [] -> subexpr alt' -- strip the unused top-most case
456 _ -> LCase (LV (Glob n)) [alt']
457 where
458 namesBoundIn :: LAlt -> [Name]
459 namesBoundIn (LConCase cn i ns sc) = ns
460 namesBoundIn (LConstCase c sc) = []
461 namesBoundIn (LDefaultCase sc) = []
463 subexpr :: LAlt -> LExp
464 subexpr (LConCase _ _ _ e) = e
465 subexpr (LConstCase _ e) = e
466 subexpr (LDefaultCase e) = e
468irSC vs (Case n alts) = LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
469irSC vs ImpossibleCase = return LNothing
471irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
473-- this leaves out all unused arguments of the constructor
474irAlt vs _ (ConCase n t args sc) = do
475 sc' <- irSC vs sc
476 used <- maybe [] (map fst . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState
477 return $ LConCase (-1) n [a | (i,a) <- zip [0..] args, i `elem` used] sc'
479irAlt vs _ (ConstCase x rhs)
480 | matchable x = LConstCase x <$> irSC vs rhs
481 | matchableTy x = LDefaultCase <$> irSC vs rhs
482 where
483 matchable (I _) = True
484 matchable (BI _) = True
485 matchable (Ch _) = True
486 matchable (Str _) = True
487 matchable _ = False
489 matchableTy (AType (ATInt ITNative)) = True
490 matchableTy (AType (ATInt ITBig)) = True
491 matchableTy (AType (ATInt ITChar)) = True
492 matchableTy StrType = True
494 matchableTy (AType (ATInt (ITFixed IT8))) = True
495 matchableTy (AType (ATInt (ITFixed IT16))) = True
496 matchableTy (AType (ATInt (ITFixed IT32))) = True
497 matchableTy (AType (ATInt (ITFixed IT64))) = True
499 matchableTy _ = False
501irAlt vs tm (SucCase n rhs) = do
502 rhs' <- irSC vs rhs
503 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
504 [tm,
505 LConst (BI 1)]) rhs')
507irAlt vs _ (ConstCase c rhs)
508 = ifail $ "Can't match on (" ++ show c ++ ")"
510irAlt vs _ (DefaultCase rhs)
511 = LDefaultCase <$> irSC vs rhs