git.iko.soy/Idris-dev
on cee5985 help sign in
Idris-dev/src/IRTS/Compiler.hs
521 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
319irCon :: Vars -> [Name] -> Int -> Name -> [Term] -> Idris LExp
320irCon vs env arity n args
321 | length args > arity
322 = error $ "oversaturated data constructor: " ++ show (n, args)
324 -- saturated
325 | length args == arity
326 = buildApp (LV (Glob n)) args
328 -- undersaturated, wrap in lambdas
329 | otherwise
330 = let extraNs = [sMN i "sat" | i <- [length args .. arity-1]]
331 extraTs = [P Bound n undefined | n <- extraNs]
332 in LLam extraNs <$> irCon vs env arity n (args ++ extraTs)
333 where
334 buildApp e [] = return e
335 buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
337doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp
338doForeign vs env (_ : fgn : args)
339 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
340 = case getFTypes fgnArgTys of
341 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
342 Just tys -> do
343 args' <- mapM (irTerm vs env) (init args)
344 return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')
346 | otherwise = ifail "Badly formed foreign function call"
347 where
348 getFTypes :: TT Name -> Maybe [FType]
349 getFTypes tm = case unApply tm of
350 -- nil : {a : Type} -> List a
351 (nil, [_]) -> Just []
352 -- cons : {a : Type} -> a -> List a -> List a
353 (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
354 _ -> Nothing
356 mkIty' (P _ (UN ty) _) = mkIty (str ty)
357 mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
358 | fi == txt "FIntT"
359 = mkIntIty (str intTy)
361 mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
362 | ff == txt "FFunction"
363 , fa == txt "FAny"
364 , io == txt "IO"
365 = FFunctionIO
367 mkIty' (App (App (P _ (UN ff) _) _) _)
368 | ff == txt "FFunction"
369 = FFunction
371 mkIty' _ = FAny
373 -- would be better if these FInt types were evaluated at compile time
374 -- TODO: add %eval directive for such things
376 mkIty "FFloat" = FArith ATFloat
377 mkIty "FInt" = mkIntIty "ITNative"
378 mkIty "FChar" = mkIntIty "ITChar"
379 mkIty "FByte" = mkIntIty "IT8"
380 mkIty "FShort" = mkIntIty "IT16"
381 mkIty "FLong" = mkIntIty "IT64"
382 mkIty "FBits8" = mkIntIty "IT8"
383 mkIty "FBits16" = mkIntIty "IT16"
384 mkIty "FBits32" = mkIntIty "IT32"
385 mkIty "FBits64" = mkIntIty "IT64"
386 mkIty "FString" = FString
387 mkIty "FPtr" = FPtr
388 mkIty "FManagedPtr" = FManagedPtr
389 mkIty "FUnit" = FUnit
390 mkIty "FFunction" = FFunction
391 mkIty "FFunctionIO" = FFunctionIO
392 mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
393 mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
394 mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
395 mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
396 mkIty x = error $ "Unknown type " ++ x
398 mkIntIty "ITNative" = FArith (ATInt ITNative)
399 mkIntIty "ITChar" = FArith (ATInt ITChar)
400 mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
401 mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
402 mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
403 mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
405irTree :: [Name] -> SC -> Idris LExp
406irTree args tree = do
407 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
408 LLam args <$> irSC M.empty tree
410irSC :: Vars -> SC -> Idris LExp
411irSC vs (STerm t) = irTerm vs [] t
412irSC vs (UnmatchedCase str) = return $ LError str
413irSC vs (ProjCase tm alt) = do
414 tm' <- irTerm vs [] tm
415 alt' <- irAlt vs tm' alt
416 return $ LCase tm' [alt']
418-- There are two transformations in this case:
419--
420-- 1. Newtype-case elimination:
421-- case {e0} of
422-- wrap({e1}) -> P({e1}) ==> P({e0})
423--
424-- This is important because newtyped constructors are compiled away entirely
425-- and we need to do that everywhere.
426--
427-- 2. Unused-case elimination (only valid for singleton branches):
428-- case {e0} of ==> P
429-- C(x,y) -> P[... x,y not used ...]
430--
431-- This is important for runtime because sometimes we case on irrelevant data:
432--
433-- In the example above, {e0} will most probably have been erased
434-- so this vain projection would make the resulting program segfault
435-- because the code generator still emits a PROJECT(...) STG instruction.
436--
437-- Hence, we check whether the variables are used at all
438-- and erase the casesplit if they are not.
439irSC vs (Case n [alt]) = do
440 replacement <- case alt of
441 ConCase cn a ns sc -> do
442 detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState
443 used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState
444 if detag && length used == 1
445 then return . Just $ substSC (ns !! head used) n sc
446 else return Nothing
447 _ -> return Nothing
449 case replacement of
450 Just sc -> irSC vs sc
451 _ -> do
452 alt' <- irAlt vs (LV (Glob n)) alt
453 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
454 [] -> subexpr alt' -- strip the unused top-most case
455 _ -> LCase (LV (Glob n)) [alt']
456 where
457 namesBoundIn :: LAlt -> [Name]
458 namesBoundIn (LConCase cn i ns sc) = ns
459 namesBoundIn (LConstCase c sc) = []
460 namesBoundIn (LDefaultCase sc) = []
462 subexpr :: LAlt -> LExp
463 subexpr (LConCase _ _ _ e) = e
464 subexpr (LConstCase _ e) = e
465 subexpr (LDefaultCase e) = e
467irSC vs (Case n alts) = LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
468irSC vs ImpossibleCase = return LNothing
470irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
472-- this leaves out all unused arguments of the constructor
473irAlt vs _ (ConCase n t args sc) = do
474 used <- getUsed . lookup n <$> getIState
475 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
476 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
477 where
478 lookup n = lookupCtxtExact n . idris_callgraph
479 getUsed = maybe [] (map fst . usedpos)
481 methodVars = case n of
482 SN (InstanceCtorN className)
483 -> M.fromList [(v, VI
484 { viMethod = Just $ mkFieldName n i
485 }) | (v,i) <- zip args [0..]]
486 _
487 -> M.empty -- not an instance constructor
489irAlt vs _ (ConstCase x rhs)
490 | matchable x = LConstCase x <$> irSC vs rhs
491 | matchableTy x = LDefaultCase <$> irSC vs rhs
492 where
493 matchable (I _) = True
494 matchable (BI _) = True
495 matchable (Ch _) = True
496 matchable (Str _) = True
497 matchable _ = False
499 matchableTy (AType (ATInt ITNative)) = True
500 matchableTy (AType (ATInt ITBig)) = True
501 matchableTy (AType (ATInt ITChar)) = True
502 matchableTy StrType = True
504 matchableTy (AType (ATInt (ITFixed IT8))) = True
505 matchableTy (AType (ATInt (ITFixed IT16))) = True
506 matchableTy (AType (ATInt (ITFixed IT32))) = True
507 matchableTy (AType (ATInt (ITFixed IT64))) = True
509 matchableTy _ = False
511irAlt vs tm (SucCase n rhs) = do
512 rhs' <- irSC vs rhs
513 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
514 [tm,
515 LConst (BI 1)]) rhs')
517irAlt vs _ (ConstCase c rhs)
518 = ifail $ "Can't match on (" ++ show c ++ ")"
520irAlt vs _ (DefaultCase rhs)
521 = LDefaultCase <$> irSC vs rhs