git.iko.soy/Idris-dev
on cfbb64f help sign in
Idris-dev/src/IRTS/Compiler.hs
552 lines 19 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.ASTUtils
23import Idris.Erasure
24import Idris.Error
26import Debug.Trace
28import Idris.Core.TT
29import Idris.Core.Evaluate
30import Idris.Core.CaseTree
32import Control.Category
33import Prelude hiding (id, (.))
35import Control.Applicative
36import Control.Monad.State
37import Data.Maybe
38import Data.List
39import Data.Ord
40import Data.IntSet (IntSet)
41import qualified Data.IntSet as IS
42import qualified Data.Map as M
43import qualified Data.Set as S
44import System.Process
45import System.IO
46import System.Directory
47import System.Environment
48import System.FilePath ((</>), addTrailingPathSeparator)
50import Paths_idris
52compile :: Codegen -> FilePath -> Term -> Idris ()
53compile codegen f tm
54 = do checkMVs -- check for undefined metavariables
55 reachableNames <- performUsageAnalysis
56 maindef <- irMain tm
57 iLOG $ "MAIN: " ++ show maindef
58 objs <- getObjectFiles codegen
59 libs <- getLibs codegen
60 flags <- getFlags codegen
61 hdrs <- getHdrs codegen
62 impdirs <- allImportDirs
63 defsIn <- mkDecls tm reachableNames
64 let defs = defsIn ++ [(sMN 0 "runMain", maindef)]
65 -- iputStrLn $ showSep "\n" (map show defs)
66 let (nexttag, tagged) = addTags 65536 (liftAll defs)
67 let ctxtIn = addAlist tagged emptyContext
68 iLOG "Defunctionalising"
69 let defuns_in = defunctionalise nexttag ctxtIn
70 logLvl 5 $ show defuns_in
71 iLOG "Inlining"
72 let defuns = inline defuns_in
73 logLvl 5 $ show defuns
74 iLOG "Resolving variables for CG"
75 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))
76 let checked = checkDefs defuns (toAlist defuns)
77 outty <- outputTy
78 dumpCases <- getDumpCases
79 dumpDefun <- getDumpDefun
80 case dumpCases of
81 Nothing -> return ()
82 Just f -> runIO $ writeFile f (showCaseTrees defs)
83 case dumpDefun of
84 Nothing -> return ()
85 Just f -> runIO $ writeFile f (dumpDefuns defuns)
86 triple <- Idris.AbsSyntax.targetTriple
87 cpu <- Idris.AbsSyntax.targetCPU
88 optimise <- optLevel
89 iLOG "Building output"
91 case checked of
92 OK c -> do let cginfo = CodegenInfo f outty triple cpu optimise
93 hdrs impdirs objs libs flags
94 NONE c (toAlist defuns)
95 tagged
96 runIO $ case codegen of
97 ViaC -> codegenC cginfo
98 ViaJava -> codegenJava cginfo
99 ViaJavaScript -> codegenJavaScript cginfo
100 ViaNode -> codegenNode cginfo
101 ViaLLVM -> codegenLLVM cginfo
102 Bytecode -> dumpBC c f
103 Error e -> ierror e
104 where checkMVs = do i <- getIState
105 case map fst (idris_metavars i) \\ primDefs of
106 [] -> return ()
107 ms -> ifail $ "There are undefined metavariables: " ++ show ms
108 inDir d h = do let f = d </> h
109 ex <- doesFileExist f
110 if ex then return f else return h
112irMain :: TT Name -> Idris LDecl
113irMain tm = do
114 i <- irTerm M.empty [] tm
115 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
117mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
118mkDecls t used
119 = do i <- getIState
120 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
121 decls <- mapM build ds
122 return decls
124showCaseTrees :: [(Name, LDecl)] -> String
125showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)
126 where
127 showCT (n, LFun _ f args lexp)
128 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t"
129 ++ show lexp
130 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
132 defnRank :: (Name, LDecl) -> String
133 defnRank (n, LFun _ _ _ _) = "1" ++ nameRank n
134 defnRank (n, LConstructor _ _ _) = "2" ++ nameRank n
136 nameRank :: Name -> String
137 nameRank (UN s) = "1" ++ show s
138 nameRank (MN i s) = "2" ++ show s ++ show i
139 nameRank (NS n ns) = "3" ++ concatMap show (reverse ns) ++ nameRank n
140 nameRank (SN sn) = "4" ++ snRank sn
141 nameRank n = "5" ++ show n
143 snRank :: SpecialName -> String
144 snRank (WhereN i n n') = "1" ++ nameRank n' ++ nameRank n ++ show i
145 snRank (InstanceN n args) = "2" ++ nameRank n ++ concatMap show args
146 snRank (ParentN n s) = "3" ++ nameRank n ++ show s
147 snRank (MethodN n) = "4" ++ nameRank n
148 snRank (CaseN n) = "5" ++ nameRank n
149 snRank (ElimN n) = "6" ++ nameRank n
150 snRank (InstanceCtorN n) = "7" ++ nameRank n
152isCon (TyDecl _ _) = True
153isCon _ = False
155build :: (Name, Def) -> Idris (Name, LDecl)
156build (n, d)
157 = do i <- getIState
158 case lookup n (idris_scprims i) of
159 Just (ar, op) ->
160 let args = map (\x -> sMN x "op") [0..] in
161 return (n, (LFun [] n (take ar args)
162 (LOp op (map (LV . Glob) (take ar args)))))
163 _ -> do def <- mkLDecl n d
164 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
165 return (n, def)
167declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
168declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
170mkLDecl n (Function tm _)
171 = declArgs [] True n <$> irTerm M.empty [] tm
173mkLDecl n (CaseOp ci _ _ _ pats cd)
174 = declArgs [] (case_inlinable ci) n <$> irTree args sc
175 where
176 (args, sc) = cases_runtime cd
178mkLDecl n (TyDecl (DCon tag arity) _) =
179 LConstructor n tag . length <$> fgetState (cg_usedpos . ist_callgraph n)
181mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
182mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
184data VarInfo = VI
185 { viMethod :: Maybe Name
186 }
187 deriving Show
189type Vars = M.Map Name VarInfo
191irTerm :: Vars -> [Name] -> Term -> Idris LExp
192irTerm vs env tm@(App f a) = case unApply tm of
193 (P _ (UN m) _, args)
194 | m == txt "mkForeignPrim"
195 -> doForeign vs env args
197 (P _ (UN u) _, [_, arg])
198 | u == txt "unsafePerformPrimIO"
199 -> irTerm vs env arg
201 -- TMP HACK - until we get inlining.
202 (P _ (UN r) _, [_, _, _, _, _, arg])
203 | r == txt "replace"
204 -> irTerm vs env arg
206 -- Laziness, the old way
207 (P _ (UN l) _, [_, arg])
208 | l == txt "lazy"
209 -> error "lazy has crept in somehow"
211 (P _ (UN l) _, [_, arg])
212 | l == txt "force"
213 -> LForce <$> irTerm vs env arg
215 -- Laziness, the new way
216 (P _ (UN l) _, [_, _, arg])
217 | l == txt "Delay"
218 -> LLazyExp <$> irTerm vs env arg
220 (P _ (UN l) _, [_, _, arg])
221 | l == txt "Force"
222 -> LForce <$> irTerm vs env arg
224 (P _ (UN a) _, [_, _, arg])
225 | a == txt "assert_smaller"
226 -> irTerm vs env arg
228 (P _ (UN a) _, [_, arg])
229 | a == txt "assert_total"
230 -> irTerm vs env arg
232 (P _ (UN p) _, [_, arg])
233 | p == txt "par"
234 -> do arg' <- irTerm vs env arg
235 return $ LOp LPar [LLazyExp arg']
237 (P _ (UN pf) _, [arg])
238 | pf == txt "prim_fork"
239 -> do arg' <- irTerm vs env arg
240 return $ LOp LFork [LLazyExp arg']
242 (P _ (UN m) _, [_,size,t])
243 | m == txt "malloc"
244 -> irTerm vs env t
246 (P _ (UN tm) _, [_,t])
247 | tm == txt "trace_malloc"
248 -> irTerm vs env t -- TODO
250 -- This case is here until we get more general inlining. It's just
251 -- a really common case, and the laziness hurts...
252 (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
253 (App (P _ (UN d') _) e)])
254 | be == txt "boolElim"
255 , d == txt "Delay"
256 , d' == txt "Delay"
257 -> do
258 x' <- irTerm vs env x
259 t' <- irTerm vs env t
260 e' <- irTerm vs env e
261 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
262 ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
263 ])
265 (P (DCon t arity) n _, args) -> do
266 detag <- fgetState (opt_detaggable . ist_optimisation n)
267 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
269 when (length args > arity) $
270 ifail ("oversaturated data ctor: " ++ show tm)
272 let args' = [a | (i,a) <- zip [0..] args, i `elem` used]
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 <- fgetState (opt_detaggable . ist_optimisation cn)
477 used <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
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 <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
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 methodVars = case n of
513 SN (InstanceCtorN className)
514 -> M.fromList [(v, VI
515 { viMethod = Just $ mkFieldName n i
516 }) | (v,i) <- zip args [0..]]
517 _
518 -> M.empty -- not an instance constructor
520irAlt vs _ (ConstCase x rhs)
521 | matchable x = LConstCase x <$> irSC vs rhs
522 | matchableTy x = LDefaultCase <$> irSC vs rhs
523 where
524 matchable (I _) = True
525 matchable (BI _) = True
526 matchable (Ch _) = True
527 matchable (Str _) = True
528 matchable _ = False
530 matchableTy (AType (ATInt ITNative)) = True
531 matchableTy (AType (ATInt ITBig)) = True
532 matchableTy (AType (ATInt ITChar)) = True
533 matchableTy StrType = True
535 matchableTy (AType (ATInt (ITFixed IT8))) = True
536 matchableTy (AType (ATInt (ITFixed IT16))) = True
537 matchableTy (AType (ATInt (ITFixed IT32))) = True
538 matchableTy (AType (ATInt (ITFixed IT64))) = True
540 matchableTy _ = False
542irAlt vs tm (SucCase n rhs) = do
543 rhs' <- irSC vs rhs
544 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
545 [tm,
546 LConst (BI 1)]) rhs')
548irAlt vs _ (ConstCase c rhs)
549 = ifail $ "Can't match on (" ++ show c ++ ")"
551irAlt vs _ (DefaultCase rhs)
552 = LDefaultCase <$> irSC vs rhs