git.iko.soy/Idris-dev
on 64353d2 help sign in
Idris-dev/src/IRTS/Compiler.hs
529 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 -- turn de bruijn vars into regular named references and try again
270 (V i, args) -> irTerm vs env $ mkApp (P Bound (env !! i) Erased) args
272 (f, args)
273 -> LApp False
274 <$> irTerm vs env f
275 <*> mapM (irTerm vs env) args
277 where
278 applyName :: Name -> IState -> [Term] -> Idris LExp
279 applyName n ist args =
280 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
281 where
282 erase (i, x)
283 | i >= arity || i `elem` used = x
284 | otherwise = Erased
286 arity = case fst4 <$> lookupCtxt n (definitions . tt_ctxt $ ist) of
287 [CaseOp ci ty tys def tot cdefs] -> length tys
288 [TyDecl (DCon tag ar) _] -> ar
289 [TyDecl Ref ty] -> length $ getArgTys ty
290 [Operator ty ar op] -> ar
291 [] -> 0 -- no definition, probably local name => can't erase anything
292 def -> error $ "unknown arity: " ++ show (n, def)
294 -- name for purposes of usage info lookup
295 uName
296 | Just n' <- viMethod =<< M.lookup n vs = n'
297 | otherwise = n
299 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
300 fst4 (x,_,_,_) = x
302irTerm vs env (P _ n _) = return $ LV (Glob n)
303irTerm vs env (V i)
304 | i >= 0 && i < length env = return $ LV (Glob (env!!i))
305 | otherwise = ifail $ "bad de bruijn index: " ++ show i
307irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc
308 where
309 n' = uniqueName n env
311irTerm vs env (Bind n (Let _ v) sc)
312 = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc
314irTerm vs env (Bind _ _ _) = return $ LNothing
316irTerm vs env (Proj t (-1)) = do
317 t' <- irTerm vs env t
318 return $ LOp (LMinus (ATInt ITBig))
319 [t', LConst (BI 1)]
321irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i
322irTerm vs env (Constant c) = return $ LConst c
323irTerm vs env (TType _) = return $ LNothing
324irTerm vs env Erased = return $ LNothing
325irTerm vs env Impossible = return $ LNothing
327irCon :: Vars -> [Name] -> Int -> Name -> [Term] -> Idris LExp
328irCon vs env arity n args
329 | length args > arity
330 = error $ "oversaturated data constructor: " ++ show (n, args)
332 -- saturated
333 | length args == arity
334 = buildApp (LV (Glob n)) args
336 -- undersaturated, wrap in lambdas
337 | otherwise
338 = let extraNs = [sMN i "sat" | i <- [length args .. arity-1]]
339 extraTs = [P Bound n undefined | n <- extraNs]
340 in LLam extraNs <$> irCon vs env arity n (args ++ extraTs)
341 where
342 buildApp e [] = return e
343 buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
345doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp
346doForeign vs env (_ : fgn : args)
347 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
348 = case getFTypes fgnArgTys of
349 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
350 Just tys -> do
351 args' <- mapM (irTerm vs env) (init args)
352 return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')
354 | otherwise = ifail "Badly formed foreign function call"
355 where
356 getFTypes :: TT Name -> Maybe [FType]
357 getFTypes tm = case unApply tm of
358 -- nil : {a : Type} -> List a
359 (nil, [_]) -> Just []
360 -- cons : {a : Type} -> a -> List a -> List a
361 (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
362 _ -> Nothing
364 mkIty' (P _ (UN ty) _) = mkIty (str ty)
365 mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
366 | fi == txt "FIntT"
367 = mkIntIty (str intTy)
369 mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
370 | ff == txt "FFunction"
371 , fa == txt "FAny"
372 , io == txt "IO"
373 = FFunctionIO
375 mkIty' (App (App (P _ (UN ff) _) _) _)
376 | ff == txt "FFunction"
377 = FFunction
379 mkIty' _ = FAny
381 -- would be better if these FInt types were evaluated at compile time
382 -- TODO: add %eval directive for such things
384 mkIty "FFloat" = FArith ATFloat
385 mkIty "FInt" = mkIntIty "ITNative"
386 mkIty "FChar" = mkIntIty "ITChar"
387 mkIty "FByte" = mkIntIty "IT8"
388 mkIty "FShort" = mkIntIty "IT16"
389 mkIty "FLong" = mkIntIty "IT64"
390 mkIty "FBits8" = mkIntIty "IT8"
391 mkIty "FBits16" = mkIntIty "IT16"
392 mkIty "FBits32" = mkIntIty "IT32"
393 mkIty "FBits64" = mkIntIty "IT64"
394 mkIty "FString" = FString
395 mkIty "FPtr" = FPtr
396 mkIty "FManagedPtr" = FManagedPtr
397 mkIty "FUnit" = FUnit
398 mkIty "FFunction" = FFunction
399 mkIty "FFunctionIO" = FFunctionIO
400 mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
401 mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
402 mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
403 mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
404 mkIty x = error $ "Unknown type " ++ x
406 mkIntIty "ITNative" = FArith (ATInt ITNative)
407 mkIntIty "ITChar" = FArith (ATInt ITChar)
408 mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
409 mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
410 mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
411 mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
413irTree :: [Name] -> SC -> Idris LExp
414irTree args tree = do
415 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
416 LLam args <$> irSC M.empty tree
418irSC :: Vars -> SC -> Idris LExp
419irSC vs (STerm t) = irTerm vs [] t
420irSC vs (UnmatchedCase str) = return $ LError str
421irSC vs (ProjCase tm alt) = do
422 tm' <- irTerm vs [] tm
423 alt' <- irAlt vs tm' alt
424 return $ LCase tm' [alt']
426-- There are two transformations in this case:
427--
428-- 1. Newtype-case elimination:
429-- case {e0} of
430-- wrap({e1}) -> P({e1}) ==> P({e0})
431--
432-- This is important because newtyped constructors are compiled away entirely
433-- and we need to do that everywhere.
434--
435-- 2. Unused-case elimination (only valid for singleton branches):
436-- case {e0} of ==> P
437-- C(x,y) -> P[... x,y not used ...]
438--
439-- This is important for runtime because sometimes we case on irrelevant data:
440--
441-- In the example above, {e0} will most probably have been erased
442-- so this vain projection would make the resulting program segfault
443-- because the code generator still emits a PROJECT(...) STG instruction.
444--
445-- Hence, we check whether the variables are used at all
446-- and erase the casesplit if they are not.
447irSC vs (Case n [alt]) = do
448 replacement <- case alt of
449 ConCase cn a ns sc -> do
450 detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState
451 used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState
452 if detag && length used == 1
453 then return . Just $ substSC (ns !! head used) n sc
454 else return Nothing
455 _ -> return Nothing
457 case replacement of
458 Just sc -> irSC vs sc
459 _ -> do
460 alt' <- irAlt vs (LV (Glob n)) alt
461 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
462 [] -> subexpr alt' -- strip the unused top-most case
463 _ -> LCase (LV (Glob n)) [alt']
464 where
465 namesBoundIn :: LAlt -> [Name]
466 namesBoundIn (LConCase cn i ns sc) = ns
467 namesBoundIn (LConstCase c sc) = []
468 namesBoundIn (LDefaultCase sc) = []
470 subexpr :: LAlt -> LExp
471 subexpr (LConCase _ _ _ e) = e
472 subexpr (LConstCase _ e) = e
473 subexpr (LDefaultCase e) = e
475irSC vs (Case n alts) = LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
476irSC vs ImpossibleCase = return LNothing
478irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
480-- this leaves out all unused arguments of the constructor
481irAlt vs _ (ConCase n t args sc) = do
482 used <- getUsed . lookup n <$> getIState
483 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
484 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
485 where
486 lookup n = lookupCtxtExact n . idris_callgraph
487 getUsed = maybe [] (map fst . usedpos)
489 methodVars = case n of
490 SN (InstanceCtorN className)
491 -> M.fromList [(v, VI
492 { viMethod = Just $ mkFieldName n i
493 }) | (v,i) <- zip args [0..]]
494 _
495 -> M.empty -- not an instance constructor
497irAlt vs _ (ConstCase x rhs)
498 | matchable x = LConstCase x <$> irSC vs rhs
499 | matchableTy x = LDefaultCase <$> irSC vs rhs
500 where
501 matchable (I _) = True
502 matchable (BI _) = True
503 matchable (Ch _) = True
504 matchable (Str _) = True
505 matchable _ = False
507 matchableTy (AType (ATInt ITNative)) = True
508 matchableTy (AType (ATInt ITBig)) = True
509 matchableTy (AType (ATInt ITChar)) = True
510 matchableTy StrType = True
512 matchableTy (AType (ATInt (ITFixed IT8))) = True
513 matchableTy (AType (ATInt (ITFixed IT16))) = True
514 matchableTy (AType (ATInt (ITFixed IT32))) = True
515 matchableTy (AType (ATInt (ITFixed IT64))) = True
517 matchableTy _ = False
519irAlt vs tm (SucCase n rhs) = do
520 rhs' <- irSC vs rhs
521 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
522 [tm,
523 LConst (BI 1)]) rhs')
525irAlt vs _ (ConstCase c rhs)
526 = ifail $ "Can't match on (" ++ show c ++ ")"
528irAlt vs _ (DefaultCase rhs)
529 = LDefaultCase <$> irSC vs rhs