git.iko.soy/Idris-dev
on 52ea5a0 help sign in
Idris-dev/src/IRTS/Compiler.hs
516 lines 21 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 i <- ir tm
109 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
111mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
112mkDecls t used
113 = do i <- getIState
114 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
115 decls <- mapM build ds
116 return decls
118showCaseTrees :: [(Name, LDecl)] -> String
119showCaseTrees ds = showSep "\n\n" (map showCT ds)
120 where
121 showCT (n, LFun _ f args lexp)
122 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t "
123 ++ show lexp
124 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
126isCon (TyDecl _ _) = True
127isCon _ = False
129class ToIR a where
130 ir :: a -> Idris LExp
132build :: (Name, Def) -> Idris (Name, LDecl)
133build (n, d)
134 = do i <- getIState
135 case lookup n (idris_scprims i) of
136 Just (ar, op) ->
137 let args = map (\x -> sMN x "op") [0..] in
138 return (n, (LFun [] n (take ar args)
139 (LOp op (map (LV . Glob) (take ar args)))))
140 _ -> do def <- mkLDecl n d
141 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
142 return (n, def)
144declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
145declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
147mkLDecl n (Function tm _) = do e <- ir tm
148 return (declArgs [] True n e)
149mkLDecl n (CaseOp ci _ _ _ pats cd)
150 = let (args, sc) = cases_runtime cd in
151 do e <- ir (args, sc)
152 return (declArgs [] (case_inlinable ci) n e)
154mkLDecl n (TyDecl (DCon tag arity) _) =
155 LConstructor n tag . maybe arity (length . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState
157mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
158mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
160instance ToIR (TT Name) where
161 ir tm = ir' [] tm where
162 ir' env tm@(App f a)
163 | (P _ (UN m) _, args) <- unApply tm,
164 m == txt "mkForeignPrim"
165 = doForeign env args
166 | (P _ (UN u) _, [_, arg]) <- unApply tm,
167 u == txt "unsafePerformPrimIO"
168 = ir' env arg
169 -- TMP HACK - until we get inlining.
170 | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,
171 r == txt "replace"
172 = ir' env arg
173 -- Laziness, the old way
174 | (P _ (UN l) _, [_, arg]) <- unApply tm,
175 l == txt "lazy"
176 = do arg' <- ir' env arg
177 error "lazy has crept in somehow"
178-- return $ LLazyExp arg'
179 | (P _ (UN l) _, [_, arg]) <- unApply tm,
180 l == txt "force"
181 = do arg' <- ir' env arg
182 return $ LForce arg'
183 -- Laziness, the new way
184 | (P _ (UN l) _, [_, arg]) <- unApply tm,
185 l == txt "Delay"
186 = do arg' <- ir' env arg
187 return $ LLazyExp arg'
188 | (P _ (UN l) _, [_, arg]) <- unApply tm,
189 l == txt "Force"
190 = do arg' <- ir' env arg
191 return $ LForce arg'
192 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
193 a == txt "assert_smaller"
194 = ir' env arg
195 | (P _ (UN a) _, [_, arg]) <- unApply tm,
196 a == txt "assert_total"
197 = ir' env arg
198 | (P _ (UN p) _, [_, arg]) <- unApply tm,
199 p == txt "par"
200 = do arg' <- ir' env arg
201 return $ LOp LPar [LLazyExp arg']
202 | (P _ (UN pf) _, [arg]) <- unApply tm,
203 pf == txt "prim_fork"
204 = do arg' <- ir' env arg
205 return $ LOp LFork [LLazyExp arg']
206 | (P _ (UN m) _, [_,size,t]) <- unApply tm,
207 m == txt "malloc"
208 = do size' <- ir' env size
209 t' <- ir' env t
210 return t' -- TODO $ malloc_ size' t'
211 | (P _ (UN tm) _, [_,t]) <- unApply tm,
212 tm == txt "trace_malloc"
213 = do t' <- ir' env t
214 return t' -- TODO
216 -- This case is here until we get more general inlining. It's just
217 -- a really common case, and the laziness hurts...
218 | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
219 (App (P _ (UN d') _) e)]) <- unApply tm,
220 be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"
221 = do x' <- ir' env x
222 t' <- ir' env t
223 e' <- ir' env e
224 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',
225 LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])
227 | (P (DCon t arity) n _, args) <- unApply tm = do
228 ist <- getIState
229 let detag = maybe False detaggable . lookupCtxtExact n $ idris_optimisation ist
230 used = maybe [] (map fst . usedpos) . lookupCtxtExact n $ idris_callgraph ist
231 args' = [a | (i,a) <- zip [0..] args, i `elem` used]
233 when (length args > arity) $
234 ifail ("oversaturated data ctor: " ++ show tm)
236 if length args' == 1 && detag -- detaggable
237 then ir' env (head args') -- newtype
238 else irCon env t (length used) n args'
240 | (P (TCon t a) n _, args) <- unApply tm
241 = return LNothing
243 | (P _ n _, args) <- unApply tm = do
244 ist <- getIState
245 case lookup n (idris_scprims ist) of
246 -- if it's a primitive which is already saturated,
247 -- compile to the corresponding op here already to save work
248 Just (arity, op) | length args == arity
249 -> LOp op <$> mapM (ir' env) args
251 _ -> applyName n ist args
253 | (f, args) <- unApply tm
254 = do f' <- ir' env f
255 args' <- mapM (ir' env) args
256 return (LApp False f' args')
258 where
259 applyName :: Name -> IState -> [Term] -> Idris LExp
260 applyName n ist args =
261 LApp False (LV $ Glob n) <$> mapM (ir' env . erase) (zip [0..] args)
262 where
263 erase (i, x)
264 | i >= arity || i `elem` used = x
265 | otherwise = Erased
267 arity = case fst4 <$> lookupCtxt n (definitions . tt_ctxt $ ist) of
268 [CaseOp ci ty tys def tot cdefs] -> length tys
269 [TyDecl (DCon tag ar) _] -> ar
270 [Operator ty ar op] -> ar
271 _ -> 0
273 used = maybe [] (map fst . usedpos) $ lookupCtxtExact n (idris_callgraph ist)
274 fst4 (x,_,_,_) = x
276-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
277-- = return $ LConst (BI 0)
278 ir' env (P _ n _) = return $ LV (Glob n)
279 ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
280 | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm
281 ir' env (Bind n (Lam _) sc)
282 = do let n' = uniqueName n env
283 sc' <- ir' (n' : env) sc
284 return $ LLam [n'] sc'
285 ir' env (Bind n (Let _ v) sc)
286 = do sc' <- ir' (n : env) sc
287 v' <- ir' env v
288 return $ LLet n v' sc'
289 ir' env (Bind _ _ _) = return $ LNothing
290 ir' env (Proj t i) | i == -1
291 = do t' <- ir' env t
292 return $ LOp (LMinus (ATInt ITBig))
293 [t', LConst (BI 1)]
294 ir' env (Proj t i) = do t' <- ir' env t
295 return $ LProj t' i
296 ir' env (Constant c) = return $ LConst c
297 ir' env (TType _) = return $ LNothing
298 ir' env Erased = return $ LNothing
299 ir' env Impossible = return $ LNothing
300-- ir' env _ = return $ LError "Impossible"
302 irCon env t arity n args
303 | length args == arity = buildApp env (LV (Glob n)) args
304 | otherwise = let extra = satArgs (arity - length args) in
305 do sc' <- irCon env t arity n
306 (args ++ map (\n -> P Bound n undefined) extra)
307 return $ LLam extra sc'
309 satArgs n = map (\i -> sMN i "sat") [1..n]
311 buildApp env e [] = return e
312 buildApp env e xs = do xs' <- mapM (ir' env) xs
313 return $ LApp False e xs'
315 doForeign :: [Name] -> [TT Name] -> Idris LExp
316 doForeign env (_ : fgn : args)
317 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
318 = let maybeTys = getFTypes fgnArgTys
319 rty = mkIty' ret in
320 case maybeTys of
321 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
322 Just tys -> do
323 args' <- mapM (ir' env) (init args)
324 -- wrap it in a prim__IO
325 -- return $ con_ 0 @@ impossible @@
326 return $ -- LLazyExp $
327 LForeign LANG_C rty fgnName (zip tys args')
328 | otherwise = ifail "Badly formed foreign function call"
330getFTypes :: TT Name -> Maybe [FType]
331getFTypes tm = case unApply tm of
332 -- nil : {a : Type} -> List a
333 (nil, [_]) -> Just []
334 -- cons : {a : Type} -> a -> List a -> List a
335 (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
336 _ -> Nothing
338mkIty' (P _ (UN ty) _) = mkIty (str ty)
339mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
340 | fi == txt "FIntT" = mkIntIty (str intTy)
341mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
342 | ff == txt "FFunction" && fa == txt "FAny" &&
343 io == txt "IO"
344 = FFunctionIO
345mkIty' (App (App (P _ (UN ff) _) _) _)
346 | ff == txt "FFunction" = FFunction
347mkIty' _ = FAny
349-- would be better if these FInt types were evaluated at compile time
350-- TODO: add %eval directive for such things
352mkIty "FFloat" = FArith ATFloat
353mkIty "FInt" = mkIntIty "ITNative"
354mkIty "FChar" = mkIntIty "ITChar"
355mkIty "FByte" = mkIntIty "IT8"
356mkIty "FShort" = mkIntIty "IT16"
357mkIty "FLong" = mkIntIty "IT64"
358mkIty "FBits8" = mkIntIty "IT8"
359mkIty "FBits16" = mkIntIty "IT16"
360mkIty "FBits32" = mkIntIty "IT32"
361mkIty "FBits64" = mkIntIty "IT64"
362mkIty "FString" = FString
363mkIty "FPtr" = FPtr
364mkIty "FManagedPtr" = FManagedPtr
365mkIty "FUnit" = FUnit
366mkIty "FFunction" = FFunction
367mkIty "FFunctionIO" = FFunctionIO
368mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
369mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
370mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
371mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
372mkIty x = error $ "Unknown type " ++ x
374mkIntIty "ITNative" = FArith (ATInt ITNative)
375mkIntIty "ITChar" = FArith (ATInt ITChar)
376mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
377mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
378mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
379mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
381zname = sNS (sUN "Z") ["Nat","Prelude"]
382sname = sNS (sUN "S") ["Nat","Prelude"]
384instance ToIR ([Name], SC) where
385 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
386 tree' <- ir tree
387 return $ LLam args tree'
389instance ToIR SC where
390 ir t = ir' t where
392 ir' (STerm t) = ir t
393 ir' (UnmatchedCase str) = return $ LError str
394 ir' (ProjCase tm alt) = do tm' <- ir tm
395 alt' <- mkIRAlt tm' alt
396 return $ LCase tm' [alt']
398 -- There are two transformations in this case:
399 --
400 -- 1. Newtype-case elimination:
401 -- case {e0} of
402 -- wrap({e1}) -> P({e1}) ==> P({e0})
403 --
404 -- This is important because newtyped constructors are compiled away entirely
405 -- and we need to do that everywhere.
406 --
407 -- 2. Unused-case elimination:
408 -- case {e0} of
409 -- C(x,y) -> P[... x,y not used ...] ==> P
410 --
411 -- This is important for runtime because sometimes we case on irrelevant data:
412 --
413 -- In the example above, {e0} will most probably have been erased
414 -- so this vain projection would make the resulting program segfault
415 -- because the code generator still emits a PROJECT(...) STG instruction.
416 --
417 -- Hence, we check whether the variables are used at all
418 -- and erase the casesplit if they are not.
419 ir' (Case n [alt]) = do
420 replacement <- case alt of
421 ConCase cn a ns sc -> do
422 detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState
423 used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState
424 if detag && length used == 1
425 then return . Just $ substSC (ns !! head used) n sc
426 else return Nothing
427 _ -> return Nothing
429 case replacement of
430 Just sc -> ir' sc
431 _ -> do
432 alt' <- mkIRAlt (LV (Glob n)) alt
433 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
434 [] -> subexpr alt' -- strip the unused top-most case
435 _ -> LCase (LV (Glob n)) [alt']
436 where
437 namesBoundIn :: LAlt -> [Name]
438 namesBoundIn (LConCase cn i ns sc) = ns
439 namesBoundIn (LConstCase c sc) = []
440 namesBoundIn (LDefaultCase sc) = []
442 subexpr :: LAlt -> LExp
443 subexpr (LConCase _ _ _ e) = e
444 subexpr (LConstCase _ e) = e
445 subexpr (LDefaultCase e) = e
447 substSC :: Name -> Name -> SC -> SC
448 substSC n repl (Case n' alts)
449 | n == n' = Case repl (map (substAlt n repl) alts)
450 | otherwise = Case n' (map (substAlt n repl) alts)
451 substSC n repl (STerm t) = STerm $ subst n (P Bound repl Erased) t
452 substSC n repl sc = error $ "unsupported in substSC: " ++ show sc
454 substAlt :: Name -> Name -> CaseAlt -> CaseAlt
455 substAlt n repl (ConCase cn a ns sc) = ConCase cn a ns (substSC n repl sc)
456 substAlt n repl (FnCase fn ns sc) = FnCase fn ns (substSC n repl sc)
457 substAlt n repl (ConstCase c sc) = ConstCase c (substSC n repl sc)
458 substAlt n repl (SucCase n' sc)
459 | n == n' = SucCase n (substSC n repl sc)
460 | otherwise = SucCase n' (substSC n repl sc)
461 substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)
463 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
464 return $ LCase (LV (Glob n)) alts'
465 ir' ImpossibleCase = return LNothing
467 -- special cases for Z and S
468 -- Needs rethink: projections make this fail
469-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
470-- = mkIRAlt n (ConstCase (BI 0) rhs)
471-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
472-- = do n' <- ir n
473-- rhs' <- ir rhs
474-- return $ LDefaultCase
475-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
476-- rhs')
477 mkIRAlt _ (ConCase n t args rhs)
478 = do rhs' <- ir rhs
479 return $ LConCase (-1) n args rhs'
480 mkIRAlt _ (ConstCase x rhs)
481 | matchable x
482 = do rhs' <- ir rhs
483 return $ LConstCase x rhs'
484 | matchableTy x
485 = do rhs' <- ir rhs
486 return $ LDefaultCase rhs'
487 mkIRAlt tm (SucCase n rhs)
488 = do rhs' <- ir rhs
489 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
490 [tm,
491 LConst (BI 1)]) rhs')
492-- return $ LSucCase n rhs'
493 mkIRAlt _ (ConstCase c rhs)
494 = ifail $ "Can't match on (" ++ show c ++ ")"
495 mkIRAlt _ (DefaultCase rhs)
496 = do rhs' <- ir rhs
497 return $ LDefaultCase rhs'
499 matchable (I _) = True
500 matchable (BI _) = True
501 matchable (Ch _) = True
502 matchable (Str _) = True
503 matchable _ = False
505 matchableTy (AType (ATInt ITNative)) = True
506 matchableTy (AType (ATInt ITBig)) = True
507 matchableTy (AType (ATInt ITChar)) = True
508 matchableTy StrType = True
510 matchableTy (AType (ATInt (ITFixed IT8))) = True
511 matchableTy (AType (ATInt (ITFixed IT16))) = True
512 matchableTy (AType (ATInt (ITFixed IT32))) = True
513 matchableTy (AType (ATInt (ITFixed IT64))) = True
515 matchableTy _ = False