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