git.iko.soy/Idris-dev
on b538db9 help sign in
Idris-dev/src/IRTS/Compiler.hs
555 lines 20 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.Ord
36import Data.IntSet (IntSet)
37import qualified Data.IntSet as IS
38import qualified Data.Map as M
39import qualified Data.Set as S
40import System.Process
41import System.IO
42import System.Directory
43import System.Environment
44import System.FilePath ((</>), addTrailingPathSeparator)
46import Paths_idris
48compile :: Codegen -> FilePath -> Term -> Idris ()
49compile codegen f tm
50 = do checkMVs -- check for undefined metavariables
51 reachableNames <- performUsageAnalysis
52 maindef <- irMain tm
53 iLOG $ "MAIN: " ++ show maindef
54 objs <- getObjectFiles codegen
55 libs <- getLibs codegen
56 flags <- getFlags codegen
57 hdrs <- getHdrs codegen
58 impdirs <- allImportDirs
59 defsIn <- mkDecls tm reachableNames
60 let defs = defsIn ++ [(sMN 0 "runMain", maindef)]
61 -- iputStrLn $ showSep "\n" (map show defs)
62 let (nexttag, tagged) = addTags 65536 (liftAll defs)
63 let ctxtIn = addAlist tagged emptyContext
64 iLOG "Defunctionalising"
65 let defuns_in = defunctionalise nexttag ctxtIn
66 logLvl 5 $ show defuns_in
67 iLOG "Inlining"
68 let defuns = inline defuns_in
69 logLvl 5 $ show defuns
70 iLOG "Resolving variables for CG"
71 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))
72 let checked = checkDefs defuns (toAlist defuns)
73 outty <- outputTy
74 dumpCases <- getDumpCases
75 dumpDefun <- getDumpDefun
76 case dumpCases of
77 Nothing -> return ()
78 Just f -> runIO $ writeFile f (showCaseTrees defs)
79 case dumpDefun of
80 Nothing -> return ()
81 Just f -> runIO $ writeFile f (dumpDefuns defuns)
82 triple <- Idris.AbsSyntax.targetTriple
83 cpu <- Idris.AbsSyntax.targetCPU
84 optimise <- optLevel
85 iLOG "Building output"
87 case checked of
88 OK c -> do let cginfo = CodegenInfo f outty triple cpu optimise
89 hdrs impdirs objs libs flags
90 NONE c (toAlist defuns)
91 tagged
92 runIO $ case codegen of
93 ViaC -> codegenC cginfo
94 ViaJava -> codegenJava cginfo
95 ViaJavaScript -> codegenJavaScript cginfo
96 ViaNode -> codegenNode cginfo
97 ViaLLVM -> codegenLLVM cginfo
98 Bytecode -> dumpBC c f
99 Error e -> ierror e
100 where checkMVs = do i <- getIState
101 case map fst (idris_metavars i) \\ primDefs of
102 [] -> return ()
103 ms -> ifail $ "There are undefined metavariables: " ++ show ms
104 inDir d h = do let f = d </> h
105 ex <- doesFileExist f
106 if ex then return f else return h
108irMain :: TT Name -> Idris LDecl
109irMain tm = do
110 i <- irTerm M.empty [] tm
111 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
113mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
114mkDecls t used
115 = do i <- getIState
116 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
117 decls <- mapM build ds
118 return decls
120showCaseTrees :: [(Name, LDecl)] -> String
121showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
122 where
123 showCT (n, LFun _ f args lexp)
124 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"
125 ++ show lexp
126 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
128 defnRank :: (Name, LDecl) -> String
129 defnRank (n, LFun _ _ _ _) = "1" ++ nameRank n
130 defnRank (n, LConstructor _ _ _) = "2" ++ nameRank n
132 nameRank :: Name -> String
133 nameRank (UN s) = "1" ++ show s
134 nameRank (MN i s) = "2" ++ show s ++ show i
135 nameRank (NS n ns) = "3" ++ concatMap show (reverse ns) ++ nameRank n
136 nameRank (SN sn) = "4" ++ snRank sn
137 nameRank n = "5" ++ show n
139 snRank :: SpecialName -> String
140 snRank (WhereN i n n') = "1" ++ nameRank n' ++ nameRank n ++ show i
141 snRank (InstanceN n args) = "2" ++ nameRank n ++ concatMap show args
142 snRank (ParentN n s) = "3" ++ nameRank n ++ show s
143 snRank (MethodN n) = "4" ++ nameRank n
144 snRank (CaseN n) = "5" ++ nameRank n
145 snRank (ElimN n) = "6" ++ nameRank n
146 snRank (InstanceCtorN n) = "7" ++ nameRank n
148isCon (TyDecl _ _) = True
149isCon _ = False
151build :: (Name, Def) -> Idris (Name, LDecl)
152build (n, d)
153 = do i <- getIState
154 case lookup n (idris_scprims i) of
155 Just (ar, op) ->
156 let args = map (\x -> sMN x "op") [0..] in
157 return (n, (LFun [] n (take ar args)
158 (LOp op (map (LV . Glob) (take ar args)))))
159 _ -> do def <- mkLDecl n d
160 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
161 return (n, def)
163declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
164declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
166mkLDecl n (Function tm _)
167 = declArgs [] True n <$> irTerm M.empty [] tm
169mkLDecl n (CaseOp ci _ _ _ pats cd)
170 = declArgs [] (case_inlinable ci) n <$> irTree args sc
171 where
172 (args, sc) = cases_runtime cd
174mkLDecl n (TyDecl (DCon tag arity) _) =
175 LConstructor n tag . erasedArity . lookup n <$> getIState
176 where
177 lookup n = lookupCtxtExact n . idris_callgraph
178 erasedArity = maybe 0 (length . usedpos)
180mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
181mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
183data VarInfo = VI
184 { viMethod :: Maybe Name
185 }
186 deriving Show
188type Vars = M.Map Name VarInfo
190irTerm :: Vars -> [Name] -> Term -> Idris LExp
191irTerm vs env tm@(App f a) = case unApply tm of
192 (P _ (UN m) _, args)
193 | m == txt "mkForeignPrim"
194 -> doForeign vs env args
196 (P _ (UN u) _, [_, arg])
197 | u == txt "unsafePerformPrimIO"
198 -> irTerm vs env arg
200 -- TMP HACK - until we get inlining.
201 (P _ (UN r) _, [_, _, _, _, _, arg])
202 | r == txt "replace"
203 -> irTerm vs env arg
205 -- Laziness, the old way
206 (P _ (UN l) _, [_, arg])
207 | l == txt "lazy"
208 -> error "lazy has crept in somehow"
210 (P _ (UN l) _, [_, arg])
211 | l == txt "force"
212 -> LForce <$> irTerm vs env arg
214 -- Laziness, the new way
215 (P _ (UN l) _, [_, _, arg])
216 | l == txt "Delay"
217 -> LLazyExp <$> irTerm vs env arg
219 (P _ (UN l) _, [_, _, arg])
220 | l == txt "Force"
221 -> LForce <$> irTerm vs env arg
223 (P _ (UN a) _, [_, _, arg])
224 | a == txt "assert_smaller"
225 -> irTerm vs env arg
227 (P _ (UN a) _, [_, arg])
228 | a == txt "assert_total"
229 -> irTerm vs env arg
231 (P _ (UN p) _, [_, arg])
232 | p == txt "par"
233 -> do arg' <- irTerm vs env arg
234 return $ LOp LPar [LLazyExp arg']
236 (P _ (UN pf) _, [arg])
237 | pf == txt "prim_fork"
238 -> do arg' <- irTerm vs env arg
239 return $ LOp LFork [LLazyExp arg']
241 (P _ (UN m) _, [_,size,t])
242 | m == txt "malloc"
243 -> irTerm vs env t
245 (P _ (UN tm) _, [_,t])
246 | tm == txt "trace_malloc"
247 -> irTerm vs env t -- TODO
249 -- This case is here until we get more general inlining. It's just
250 -- a really common case, and the laziness hurts...
251 (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
252 (App (P _ (UN d') _) e)])
253 | be == txt "boolElim"
254 , d == txt "Delay"
255 , d' == txt "Delay"
256 -> do
257 x' <- irTerm vs env x
258 t' <- irTerm vs env t
259 e' <- irTerm vs env e
260 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
261 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
262 ])
264 (P (DCon t arity) n _, args) -> do
265 ist <- getIState
266 let detag = maybe False detaggable . lookupCtxtExact n $ idris_optimisation ist
267 used = maybe [] (map fst . usedpos) . lookupCtxtExact n $ idris_callgraph ist
268 args' = [a | (i,a) <- zip [0..] args, i `elem` used]
270 when (length args > arity) $
271 ifail ("oversaturated data ctor: " ++ show tm)
273 if length args' == 1 && detag -- detaggable
274 then irTerm vs env (head args') -- newtype
275 else irCon vs env (length used) n args'
277 (P (TCon t a) n _, args) -> return LNothing
279 (P _ n _, args) -> do
280 ist <- getIState
281 case lookup n (idris_scprims ist) of
282 -- if it's a primitive that is already saturated,
283 -- compile to the corresponding op here already to save work
284 Just (arity, op) | length args == arity
285 -> LOp op <$> mapM (irTerm vs env) args
287 -- otherwise, just apply the name
288 _ -> applyName n ist args
290 -- turn de bruijn vars into regular named references and try again
291 (V i, args) -> irTerm vs env $ mkApp (P Bound (env !! i) Erased) args
293 (f, args)
294 -> LApp False
295 <$> irTerm vs env f
296 <*> mapM (irTerm vs env) args
298 where
299 applyName :: Name -> IState -> [Term] -> Idris LExp
300 applyName n ist args =
301 LApp False (LV $ Glob n) <$> mapM (irTerm vs env . erase) (zip [0..] args)
302 where
303 erase (i, x)
304 | i >= arity || i `elem` used = x
305 | otherwise = Erased
307 arity = case fst4 <$> lookupCtxtExact n (definitions . tt_ctxt $ ist) of
308 Just (CaseOp ci ty tys def tot cdefs) -> length tys
309 Just (TyDecl (DCon tag ar) _) -> ar
310 Just (TyDecl Ref ty) -> length $ getArgTys ty
311 Just (Operator ty ar op) -> ar
312 Just def -> error $ "unknown arity: " ++ show (n, def)
313 Nothing -> 0 -- no definition, probably local name => can't erase anything
315 -- name for purposes of usage info lookup
316 uName
317 | Just n' <- viMethod =<< M.lookup n vs = n'
318 | otherwise = n
320 used = maybe [] (map fst . usedpos) $ lookupCtxtExact uName (idris_callgraph ist)
321 fst4 (x,_,_,_) = x
323irTerm vs env (P _ n _) = return $ LV (Glob n)
324irTerm vs env (V i)
325 | i >= 0 && i < length env = return $ LV (Glob (env!!i))
326 | otherwise = ifail $ "bad de bruijn index: " ++ show i
328irTerm vs env (Bind n (Lam _) sc) = LLam [n'] <$> irTerm vs (n':env) sc
329 where
330 n' = uniqueName n env
332irTerm vs env (Bind n (Let _ v) sc)
333 = LLet n <$> irTerm vs env v <*> irTerm vs (n : env) sc
335irTerm vs env (Bind _ _ _) = return $ LNothing
337irTerm vs env (Proj t (-1)) = do
338 t' <- irTerm vs env t
339 return $ LOp (LMinus (ATInt ITBig))
340 [t', LConst (BI 1)]
342irTerm vs env (Proj t i) = LProj <$> irTerm vs env t <*> pure i
343irTerm vs env (Constant c) = return $ LConst c
344irTerm vs env (TType _) = return $ LNothing
345irTerm vs env Erased = return $ LNothing
346irTerm vs env Impossible = return $ LNothing
348irCon :: Vars -> [Name] -> Int -> Name -> [Term] -> Idris LExp
349irCon vs env arity n args
350 | length args > arity
351 = error $ "oversaturated data constructor: " ++ show (n, args)
353 -- saturated
354 | length args == arity
355 = buildApp (LV (Glob n)) args
357 -- undersaturated, wrap in lambdas
358 | otherwise
359 = let extraNs = [sMN i "sat" | i <- [length args .. arity-1]]
360 extraTs = [P Bound n undefined | n <- extraNs]
361 in LLam extraNs <$> irCon vs env arity n (args ++ extraTs)
362 where
363 buildApp e [] = return e
364 buildApp e xs = LApp False e <$> mapM (irTerm vs env) xs
366doForeign :: Vars -> [Name] -> [TT Name] -> Idris LExp
367doForeign vs env (_ : fgn : args)
368 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
369 = case getFTypes fgnArgTys of
370 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
371 Just tys -> do
372 args' <- mapM (irTerm vs env) (init args)
373 return $ LForeign LANG_C (mkIty' ret) fgnName (zip tys args')
375 | otherwise = ifail "Badly formed foreign function call"
376 where
377 getFTypes :: TT Name -> Maybe [FType]
378 getFTypes tm = case unApply tm of
379 -- nil : {a : Type} -> List a
380 (nil, [_]) -> Just []
381 -- cons : {a : Type} -> a -> List a -> List a
382 (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
383 _ -> Nothing
385 mkIty' (P _ (UN ty) _) = mkIty (str ty)
386 mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
387 | fi == txt "FIntT"
388 = mkIntIty (str intTy)
390 mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
391 | ff == txt "FFunction"
392 , fa == txt "FAny"
393 , io == txt "IO"
394 = FFunctionIO
396 mkIty' (App (App (P _ (UN ff) _) _) _)
397 | ff == txt "FFunction"
398 = FFunction
400 mkIty' _ = FAny
402 -- would be better if these FInt types were evaluated at compile time
403 -- TODO: add %eval directive for such things
405 mkIty "FFloat" = FArith ATFloat
406 mkIty "FInt" = mkIntIty "ITNative"
407 mkIty "FChar" = mkIntIty "ITChar"
408 mkIty "FByte" = mkIntIty "IT8"
409 mkIty "FShort" = mkIntIty "IT16"
410 mkIty "FLong" = mkIntIty "IT64"
411 mkIty "FBits8" = mkIntIty "IT8"
412 mkIty "FBits16" = mkIntIty "IT16"
413 mkIty "FBits32" = mkIntIty "IT32"
414 mkIty "FBits64" = mkIntIty "IT64"
415 mkIty "FString" = FString
416 mkIty "FPtr" = FPtr
417 mkIty "FManagedPtr" = FManagedPtr
418 mkIty "FUnit" = FUnit
419 mkIty "FFunction" = FFunction
420 mkIty "FFunctionIO" = FFunctionIO
421 mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
422 mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
423 mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
424 mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
425 mkIty x = error $ "Unknown type " ++ x
427 mkIntIty "ITNative" = FArith (ATInt ITNative)
428 mkIntIty "ITChar" = FArith (ATInt ITChar)
429 mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
430 mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
431 mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
432 mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
434irTree :: [Name] -> SC -> Idris LExp
435irTree args tree = do
436 logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
437 LLam args <$> irSC M.empty tree
439irSC :: Vars -> SC -> Idris LExp
440irSC vs (STerm t) = irTerm vs [] t
441irSC vs (UnmatchedCase str) = return $ LError str
442irSC vs (ProjCase tm alts) = do
443 tm' <- irTerm vs [] tm
444 alts' <- mapM (irAlt vs tm') alts
445 return $ LCase tm' alts'
447-- Transform matching on Delay to applications of Force.
448irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])
449 | delay == txt "Delay"
450 = irSC vs $ mkForce n n' sc
452-- There are two transformations in this case:
453--
454-- 1. Newtype-case elimination:
455-- case {e0} of
456-- wrap({e1}) -> P({e1}) ==> P({e0})
457--
458-- This is important because newtyped constructors are compiled away entirely
459-- and we need to do that everywhere.
460--
461-- 2. Unused-case elimination (only valid for singleton branches):
462-- case {e0} of ==> P
463-- C(x,y) -> P[... x,y not used ...]
464--
465-- This is important for runtime because sometimes we case on irrelevant data:
466--
467-- In the example above, {e0} will most probably have been erased
468-- so this vain projection would make the resulting program segfault
469-- because the code generator still emits a PROJECT(...) G-machine instruction.
470--
471-- Hence, we check whether the variables are used at all
472-- and erase the casesplit if they are not.
473irSC vs (Case n [alt]) = do
474 replacement <- case alt of
475 ConCase cn a ns sc -> do
476 detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState
477 used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState
478 if detag && length used == 1
479 then return . Just $ substSC (ns !! head used) n sc
480 else return Nothing
481 _ -> return Nothing
483 case replacement of
484 Just sc -> irSC vs sc
485 _ -> do
486 alt' <- irAlt vs (LV (Glob n)) alt
487 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
488 [] -> subexpr alt' -- strip the unused top-most case
489 _ -> LCase (LV (Glob n)) [alt']
490 where
491 namesBoundIn :: LAlt -> [Name]
492 namesBoundIn (LConCase cn i ns sc) = ns
493 namesBoundIn (LConstCase c sc) = []
494 namesBoundIn (LDefaultCase sc) = []
496 subexpr :: LAlt -> LExp
497 subexpr (LConCase _ _ _ e) = e
498 subexpr (LConstCase _ e) = e
499 subexpr (LDefaultCase e) = e
501irSC vs (Case n alts) = LCase (LV (Glob n)) <$> mapM (irAlt vs (LV (Glob n))) alts
502irSC vs ImpossibleCase = return LNothing
504irAlt :: Vars -> LExp -> CaseAlt -> Idris LAlt
506-- this leaves out all unused arguments of the constructor
507irAlt vs _ (ConCase n t args sc) = do
508 used <- getUsed . lookup n <$> getIState
509 let usedArgs = [a | (i,a) <- zip [0..] args, i `elem` used]
510 LConCase (-1) n usedArgs <$> irSC (methodVars `M.union` vs) sc
511 where
512 lookup n = lookupCtxtExact n . idris_callgraph
513 getUsed = maybe [] (map fst . usedpos)
515 methodVars = case n of
516 SN (InstanceCtorN className)
517 -> M.fromList [(v, VI
518 { viMethod = Just $ mkFieldName n i
519 }) | (v,i) <- zip args [0..]]
520 _
521 -> M.empty -- not an instance constructor
523irAlt vs _ (ConstCase x rhs)
524 | matchable x = LConstCase x <$> irSC vs rhs
525 | matchableTy x = LDefaultCase <$> irSC vs rhs
526 where
527 matchable (I _) = True
528 matchable (BI _) = True
529 matchable (Ch _) = True
530 matchable (Str _) = True
531 matchable _ = False
533 matchableTy (AType (ATInt ITNative)) = True
534 matchableTy (AType (ATInt ITBig)) = True
535 matchableTy (AType (ATInt ITChar)) = True
536 matchableTy StrType = True
538 matchableTy (AType (ATInt (ITFixed IT8))) = True
539 matchableTy (AType (ATInt (ITFixed IT16))) = True
540 matchableTy (AType (ATInt (ITFixed IT32))) = True
541 matchableTy (AType (ATInt (ITFixed IT64))) = True
543 matchableTy _ = False
545irAlt vs tm (SucCase n rhs) = do
546 rhs' <- irSC vs rhs
547 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
548 [tm,
549 LConst (BI 1)]) rhs')
551irAlt vs _ (ConstCase c rhs)
552 = ifail $ "Can't match on (" ++ show c ++ ")"
554irAlt vs _ (DefaultCase rhs)
555 = LDefaultCase <$> irSC vs rhs