git.iko.soy/Idris-dev
on bfd9900 help sign in
Idris-dev/src/IRTS/Compiler.hs
520 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 0 (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 [TyDecl Ref ty] -> length $ getArgTys ty
271 [Operator ty ar op] -> ar
272 [] -> 0 -- no definition, probably local name => can't erase anything
273 def -> error $ "unknown arity: " ++ show (n, def)
275 used = maybe [] (map fst . usedpos) $ lookupCtxtExact n (idris_callgraph ist)
276 fst4 (x,_,_,_) = x
278-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
279-- = return $ LConst (BI 0)
280 ir' env (P _ n _) = return $ LV (Glob n)
281 ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
282 | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm
283 ir' env (Bind n (Lam _) sc)
284 = do let n' = uniqueName n env
285 sc' <- ir' (n' : env) sc
286 return $ LLam [n'] sc'
287 ir' env (Bind n (Let _ v) sc)
288 = do sc' <- ir' (n : env) sc
289 v' <- ir' env v
290 return $ LLet n v' sc'
291 ir' env (Bind _ _ _) = return $ LNothing
292 ir' env (Proj t i) | i == -1
293 = do t' <- ir' env t
294 return $ LOp (LMinus (ATInt ITBig))
295 [t', LConst (BI 1)]
296 ir' env (Proj t i) = do t' <- ir' env t
297 return $ LProj t' i
298 ir' env (Constant c) = return $ LConst c
299 ir' env (TType _) = return $ LNothing
300 ir' env Erased = return $ LNothing
301 ir' env Impossible = return $ LNothing
302-- ir' env _ = return $ LError "Impossible"
304 irCon env t arity n args
305 | length args == arity = buildApp env (LV (Glob n)) args
306 | otherwise = let extra = satArgs (arity - length args) in
307 do sc' <- irCon env t arity n
308 (args ++ map (\n -> P Bound n undefined) extra)
309 return $ LLam extra sc'
311 satArgs n = map (\i -> sMN i "sat") [1..n]
313 buildApp env e [] = return e
314 buildApp env e xs = do xs' <- mapM (ir' env) xs
315 return $ LApp False e xs'
317 doForeign :: [Name] -> [TT Name] -> Idris LExp
318 doForeign env (_ : fgn : args)
319 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
320 = let maybeTys = getFTypes fgnArgTys
321 rty = mkIty' ret in
322 case maybeTys of
323 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
324 Just tys -> do
325 args' <- mapM (ir' env) (init args)
326 -- wrap it in a prim__IO
327 -- return $ con_ 0 @@ impossible @@
328 return $ -- LLazyExp $
329 LForeign LANG_C rty fgnName (zip tys args')
330 | otherwise = ifail "Badly formed foreign function call"
332getFTypes :: TT Name -> Maybe [FType]
333getFTypes tm = case unApply tm of
334 -- nil : {a : Type} -> List a
335 (nil, [_]) -> Just []
336 -- cons : {a : Type} -> a -> List a -> List a
337 (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
338 _ -> Nothing
340mkIty' (P _ (UN ty) _) = mkIty (str ty)
341mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
342 | fi == txt "FIntT" = mkIntIty (str intTy)
343mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
344 | ff == txt "FFunction" && fa == txt "FAny" &&
345 io == txt "IO"
346 = FFunctionIO
347mkIty' (App (App (P _ (UN ff) _) _) _)
348 | ff == txt "FFunction" = FFunction
349mkIty' _ = FAny
351-- would be better if these FInt types were evaluated at compile time
352-- TODO: add %eval directive for such things
354mkIty "FFloat" = FArith ATFloat
355mkIty "FInt" = mkIntIty "ITNative"
356mkIty "FChar" = mkIntIty "ITChar"
357mkIty "FByte" = mkIntIty "IT8"
358mkIty "FShort" = mkIntIty "IT16"
359mkIty "FLong" = mkIntIty "IT64"
360mkIty "FBits8" = mkIntIty "IT8"
361mkIty "FBits16" = mkIntIty "IT16"
362mkIty "FBits32" = mkIntIty "IT32"
363mkIty "FBits64" = mkIntIty "IT64"
364mkIty "FString" = FString
365mkIty "FPtr" = FPtr
366mkIty "FManagedPtr" = FManagedPtr
367mkIty "FUnit" = FUnit
368mkIty "FFunction" = FFunction
369mkIty "FFunctionIO" = FFunctionIO
370mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
371mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
372mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
373mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
374mkIty x = error $ "Unknown type " ++ x
376mkIntIty "ITNative" = FArith (ATInt ITNative)
377mkIntIty "ITChar" = FArith (ATInt ITChar)
378mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
379mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
380mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
381mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
383zname = sNS (sUN "Z") ["Nat","Prelude"]
384sname = sNS (sUN "S") ["Nat","Prelude"]
386instance ToIR ([Name], SC) where
387 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
388 tree' <- ir tree
389 return $ LLam args tree'
391instance ToIR SC where
392 ir t = ir' t where
394 ir' (STerm t) = ir t
395 ir' (UnmatchedCase str) = return $ LError str
396 ir' (ProjCase tm alt) = do tm' <- ir tm
397 alt' <- mkIRAlt tm' alt
398 return $ LCase tm' [alt']
400 -- There are two transformations in this case:
401 --
402 -- 1. Newtype-case elimination:
403 -- case {e0} of
404 -- wrap({e1}) -> P({e1}) ==> P({e0})
405 --
406 -- This is important because newtyped constructors are compiled away entirely
407 -- and we need to do that everywhere.
408 --
409 -- 2. Unused-case elimination:
410 -- case {e0} of
411 -- C(x,y) -> P[... x,y not used ...] ==> P
412 --
413 -- This is important for runtime because sometimes we case on irrelevant data:
414 --
415 -- In the example above, {e0} will most probably have been erased
416 -- so this vain projection would make the resulting program segfault
417 -- because the code generator still emits a PROJECT(...) STG instruction.
418 --
419 -- Hence, we check whether the variables are used at all
420 -- and erase the casesplit if they are not.
421 ir' (Case n [alt]) = do
422 replacement <- case alt of
423 ConCase cn a ns sc -> do
424 detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState
425 used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState
426 if detag && length used == 1
427 then return . Just $ substSC (ns !! head used) n sc
428 else return Nothing
429 _ -> return Nothing
431 case replacement of
432 Just sc -> ir' sc
433 _ -> do
434 alt' <- mkIRAlt (LV (Glob n)) alt
435 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
436 [] -> subexpr alt' -- strip the unused top-most case
437 _ -> LCase (LV (Glob n)) [alt']
438 where
439 namesBoundIn :: LAlt -> [Name]
440 namesBoundIn (LConCase cn i ns sc) = ns
441 namesBoundIn (LConstCase c sc) = []
442 namesBoundIn (LDefaultCase sc) = []
444 subexpr :: LAlt -> LExp
445 subexpr (LConCase _ _ _ e) = e
446 subexpr (LConstCase _ e) = e
447 subexpr (LDefaultCase e) = e
449 substSC :: Name -> Name -> SC -> SC
450 substSC n repl (Case n' alts)
451 | n == n' = Case repl (map (substAlt n repl) alts)
452 | otherwise = Case n' (map (substAlt n repl) alts)
453 substSC n repl (STerm t) = STerm $ subst n (P Bound repl Erased) t
454 substSC n repl sc = error $ "unsupported in substSC: " ++ show sc
456 substAlt :: Name -> Name -> CaseAlt -> CaseAlt
457 substAlt n repl (ConCase cn a ns sc) = ConCase cn a ns (substSC n repl sc)
458 substAlt n repl (FnCase fn ns sc) = FnCase fn ns (substSC n repl sc)
459 substAlt n repl (ConstCase c sc) = ConstCase c (substSC n repl sc)
460 substAlt n repl (SucCase n' sc)
461 | n == n' = SucCase n (substSC n repl sc)
462 | otherwise = SucCase n' (substSC n repl sc)
463 substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)
465 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
466 return $ LCase (LV (Glob n)) alts'
467 ir' ImpossibleCase = return LNothing
469 -- special cases for Z and S
470 -- Needs rethink: projections make this fail
471-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
472-- = mkIRAlt n (ConstCase (BI 0) rhs)
473-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
474-- = do n' <- ir n
475-- rhs' <- ir rhs
476-- return $ LDefaultCase
477-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
478-- rhs')
479 mkIRAlt _ (ConCase n t args sc) = do
480 sc' <- ir sc
481 used <- maybe [] (map fst . usedpos) . lookupCtxtExact n . idris_callgraph <$> getIState
482 return $ LConCase (-1) n [a | (i,a) <- zip [0..] args, i `elem` used] sc'
484 mkIRAlt _ (ConstCase x rhs)
485 | matchable x
486 = do rhs' <- ir rhs
487 return $ LConstCase x rhs'
488 | matchableTy x
489 = do rhs' <- ir rhs
490 return $ LDefaultCase rhs'
491 mkIRAlt tm (SucCase n rhs)
492 = do rhs' <- ir rhs
493 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
494 [tm,
495 LConst (BI 1)]) rhs')
496-- return $ LSucCase n rhs'
497 mkIRAlt _ (ConstCase c rhs)
498 = ifail $ "Can't match on (" ++ show c ++ ")"
499 mkIRAlt _ (DefaultCase rhs)
500 = do rhs' <- ir rhs
501 return $ LDefaultCase rhs'
503 matchable (I _) = True
504 matchable (BI _) = True
505 matchable (Ch _) = True
506 matchable (Str _) = True
507 matchable _ = False
509 matchableTy (AType (ATInt ITNative)) = True
510 matchableTy (AType (ATInt ITBig)) = True
511 matchableTy (AType (ATInt ITChar)) = True
512 matchableTy StrType = True
514 matchableTy (AType (ATInt (ITFixed IT8))) = True
515 matchableTy (AType (ATInt (ITFixed IT16))) = True
516 matchableTy (AType (ATInt (ITFixed IT32))) = True
517 matchableTy (AType (ATInt (ITFixed IT64))) = True
519 matchableTy _ = False