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