git.iko.soy/Idris-dev
on f0d7876 help sign in
Idris-dev/src/IRTS/Compiler.hs
451 lines 18 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.Erasure
22import Idris.Error
24import Idris.Core.TT
25import Idris.Core.Evaluate
26import Idris.Core.CaseTree
28import Control.Applicative
29import Control.Monad.State
30import Data.List
31import qualified Data.IntMap as IM
32import qualified Data.IntSet as IS
33import qualified Data.Map as M
34import qualified Data.Set as S
35import System.Process
36import System.IO
37import System.Directory
38import System.Environment
39import System.FilePath ((</>), addTrailingPathSeparator)
41import Paths_idris
43compile :: Codegen -> FilePath -> Term -> Idris ()
44compile codegen f tm
45 = do checkMVs
46 let tmnames = namesUsed (STerm tm)
47 usedIn <- mapM (allNames []) tmnames
48 let used = sUN "prim__subBigInt" : sUN "prim__addBigInt" : concat usedIn
49 defsIn <- mkDecls tm used
50 findUnusedArgs used
52 -- TODO: traverse all names correctly
54 -- TODO: DEBUG-ONLY, remove
55 ctx <- tt_ctxt <$> getIState
56 let depMap = buildDepMap ctx used
57 let printItem (cond, deps) = show (S.toList cond) ++ " -> " ++ show (S.toList deps)
58 iLOG $ "USAGE ANALYSIS:\n" ++ unlines (map printItem . M.toList $ depMap)
60 let fmtDepMap = unlines . map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) . M.toList
61 let minUse = minimalUsage depMap
62 iLOG $ "MINIMAL USAGE:\n" ++ fmtDepMap minUse
64 let unusedMap = usedToUnused ctx minUse
65 iLOG $ "UNUSED:\n" ++ fmtDepMap unusedMap
66 -- END TODO
68 maindef <- irMain tm
69 objs <- getObjectFiles codegen
70 libs <- getLibs codegen
71 flags <- getFlags codegen
72 hdrs <- getHdrs codegen
73 impdirs <- allImportDirs
74 let defs = defsIn ++ [(sMN 0 "runMain", maindef)]
75 -- iputStrLn $ showSep "\n" (map show defs)
76 let (nexttag, tagged) = addTags 65536 (liftAll defs)
77 let ctxtIn = addAlist tagged emptyContext
78 iLOG "Defunctionalising"
79 let defuns_in = defunctionalise nexttag ctxtIn
80 logLvl 5 $ show defuns_in
81 iLOG "Inlining"
82 let defuns = inline defuns_in
83 logLvl 5 $ show defuns
84 iLOG "Resolving variables for CG"
85 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))
86 let checked = checkDefs defuns (toAlist defuns)
87 outty <- outputTy
88 dumpCases <- getDumpCases
89 dumpDefun <- getDumpDefun
90 case dumpCases of
91 Nothing -> return ()
92 Just f -> runIO $ writeFile f (showCaseTrees defs)
93 case dumpDefun of
94 Nothing -> return ()
95 Just f -> runIO $ writeFile f (dumpDefuns defuns)
96 triple <- Idris.AbsSyntax.targetTriple
97 cpu <- Idris.AbsSyntax.targetCPU
98 optimise <- optLevel
99 iLOG "Building output"
101 case checked of
102 OK c -> do let cginfo = CodegenInfo f outty triple cpu optimise
103 hdrs impdirs objs libs flags
104 NONE c (toAlist defuns)
105 tagged
106 runIO $ case codegen of
107 ViaC -> codegenC cginfo
108 ViaJava -> codegenJava cginfo
109 ViaJavaScript -> codegenJavaScript cginfo
110 ViaNode -> codegenNode cginfo
111 ViaLLVM -> codegenLLVM cginfo
112 Bytecode -> dumpBC c f
113 Error e -> ierror e
114 where checkMVs = do i <- getIState
115 case map fst (idris_metavars i) \\ primDefs of
116 [] -> return ()
117 ms -> ifail $ "There are undefined metavariables: " ++ show ms
118 inDir d h = do let f = d </> h
119 ex <- doesFileExist f
120 if ex then return f else return h
122irMain :: TT Name -> Idris LDecl
123irMain tm = do i <- ir tm
124 return $ LFun [] (sMN 0 "runMain") [] (LForce i)
126mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
127mkDecls t used
128 = do i <- getIState
129 let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
130 findUnusedArgs used
131 decls <- mapM build ds
132 return decls
134showCaseTrees :: [(Name, LDecl)] -> String
135showCaseTrees ds = showSep "\n\n" (map showCT ds)
136 where
137 showCT (n, LFun _ f args lexp)
138 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t "
139 ++ show lexp
140 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
142isCon (TyDecl _ _) = True
143isCon _ = False
145class ToIR a where
146 ir :: a -> Idris LExp
148build :: (Name, Def) -> Idris (Name, LDecl)
149build (n, d)
150 = do i <- getIState
151 case lookup n (idris_scprims i) of
152 Just (ar, op) ->
153 let args = map (\x -> sMN x "op") [0..] in
154 return (n, (LFun [] n (take ar args)
155 (LOp op (map (LV . Glob) (take ar args)))))
156 _ -> do def <- mkLDecl n d
157 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
158 return (n, def)
160getPrim :: IState -> Name -> [LExp] -> Maybe LExp
161getPrim i n args = case lookup n (idris_scprims i) of
162 Just (ar, op) ->
163 if (ar == length args)
164 then return (LOp op args)
165 else Nothing
166 _ -> Nothing
168declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
169declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
171mkLDecl n (Function tm _) = do e <- ir tm
172 return (declArgs [] True n e)
173mkLDecl n (CaseOp ci _ _ _ pats cd)
174 = let (args, sc) = cases_runtime cd in
175 do e <- ir (args, sc)
176 return (declArgs [] (case_inlinable ci) n e)
177mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
178mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
179mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
181instance ToIR (TT Name) where
182 ir tm = ir' [] tm where
183 ir' env tm@(App f a)
184 | (P _ (UN m) _, args) <- unApply tm,
185 m == txt "mkForeignPrim"
186 = doForeign env args
187 | (P _ (UN u) _, [_, arg]) <- unApply tm,
188 u == txt "unsafePerformPrimIO"
189 = ir' env arg
190 -- TMP HACK - until we get inlining.
191 | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,
192 r == txt "replace"
193 = ir' env arg
194 -- Laziness, the old way
195 | (P _ (UN l) _, [_, arg]) <- unApply tm,
196 l == txt "lazy"
197 = do arg' <- ir' env arg
198 error "lazy has crept in somehow"
199-- return $ LLazyExp arg'
200 | (P _ (UN l) _, [_, arg]) <- unApply tm,
201 l == txt "force"
202 = do arg' <- ir' env arg
203 return $ LForce arg'
204 -- Laziness, the new way
205 | (P _ (UN l) _, [arg]) <- unApply tm,
206 l == txt "Delay"
207 = do arg' <- ir' env arg
208 return $ LLazyExp arg'
209 | (P _ (UN l) _, [_, _, arg]) <- unApply tm,
210 l == txt "Force"
211 = do arg' <- ir' env arg
212 return $ LForce arg'
213 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
214 a == txt "assert_smaller"
215 = ir' env arg
216 | (P _ (UN a) _, [_, arg]) <- unApply tm,
217 a == txt "assert_total"
218 = ir' env arg
219 | (P _ (UN p) _, [_, arg]) <- unApply tm,
220 p == txt "par"
221 = do arg' <- ir' env arg
222 return $ LOp LPar [LLazyExp arg']
223 | (P _ (UN pf) _, [arg]) <- unApply tm,
224 pf == txt "prim_fork"
225 = do arg' <- ir' env arg
226 return $ LOp LFork [LLazyExp arg']
227 | (P _ (UN m) _, [_,size,t]) <- unApply tm,
228 m == txt "malloc"
229 = do size' <- ir' env size
230 t' <- ir' env t
231 return t' -- TODO $ malloc_ size' t'
232 | (P _ (UN tm) _, [_,t]) <- unApply tm,
233 tm == txt "trace_malloc"
234 = do t' <- ir' env t
235 return t' -- TODO
236 -- This case is here until we get more general inlining. It's just
237 -- a really common case, and the laziness hurts...
238 | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
239 (App (P _ (UN d') _) e)]) <- unApply tm,
240 be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"
241 = do x' <- ir' env x
242 t' <- ir' env t
243 e' <- ir' env e
244 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',
245 LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])
246 | (P (DCon t a) n _, args) <- unApply tm
247 = irCon env t a n args
248 | (P (TCon t a) n _, args) <- unApply tm
249 = return LNothing
250 | (P _ n _, args) <- unApply tm
251 = do i <- getIState
252 args' <- mapM (ir' env) args
253 case getPrim i n args' of
254 Just tm -> return tm
255 _ -> do
256 let collapse
257 = case lookupCtxtExact n
258 (idris_optimisation i) of
259 Just oi -> collapsible oi
260 _ -> False
261 let unused
262 = case lookupCtxtExact n
263 (idris_callgraph i) of
264 Just (CGInfo _ _ _ _ unusedpos) ->
265 unusedpos
266 _ -> []
267 if collapse
268 then return LNothing
269 else return (LApp False (LV (Glob n))
270 (mkUnused unused 0 args'))
271 | (f, args) <- unApply tm
272 = do f' <- ir' env f
273 args' <- mapM (ir' env) args
274 return (LApp False f' args')
275 where mkUnused u i [] = []
276 mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
277 | otherwise = x : mkUnused u (i + 1) xs
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, []) -> Just []
335 (cons, [ty, xs]) ->
336 fmap (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']
398 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
399 return $ LCase (LV (Glob n)) alts'
400 ir' ImpossibleCase = return LNothing
402 -- special cases for Z and S
403 -- Needs rethink: projections make this fail
404-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
405-- = mkIRAlt n (ConstCase (BI 0) rhs)
406-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
407-- = do n' <- ir n
408-- rhs' <- ir rhs
409-- return $ LDefaultCase
410-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
411-- rhs')
412 mkIRAlt _ (ConCase n t args rhs)
413 = do rhs' <- ir rhs
414 return $ LConCase (-1) n args rhs'
415 mkIRAlt _ (ConstCase x rhs)
416 | matchable x
417 = do rhs' <- ir rhs
418 return $ LConstCase x rhs'
419 | matchableTy x
420 = do rhs' <- ir rhs
421 return $ LDefaultCase rhs'
422 mkIRAlt tm (SucCase n rhs)
423 = do rhs' <- ir rhs
424 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
425 [tm,
426 LConst (BI 1)]) rhs')
427-- return $ LSucCase n rhs'
428 mkIRAlt _ (ConstCase c rhs)
429 = ifail $ "Can't match on (" ++ show c ++ ")"
430 mkIRAlt _ (DefaultCase rhs)
431 = do rhs' <- ir rhs
432 return $ LDefaultCase rhs'
434 matchable (I _) = True
435 matchable (BI _) = True
436 matchable (Ch _) = True
437 matchable (Str _) = True
438 matchable _ = False
440 matchableTy (AType (ATInt ITNative)) = True
441 matchableTy (AType (ATInt ITBig)) = True
442 matchableTy (AType (ATInt ITChar)) = True
443 matchableTy StrType = True
445 matchableTy (AType (ATInt (ITFixed IT8))) = True
446 matchableTy (AType (ATInt (ITFixed IT16))) = True
447 matchableTy (AType (ATInt (ITFixed IT32))) = True
448 matchableTy (AType (ATInt (ITFixed IT64))) = True
450 matchableTy _ = False