git.iko.soy/Idris-dev
on 6041ec1 help sign in
Idris-dev/src/IRTS/Compiler.hs
442 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.Monad.State
29import Data.List
30import qualified Data.IntMap as IM
31import qualified Data.Map as M
32import qualified Data.Set as S
33import System.Process
34import System.IO
35import System.Directory
36import System.Environment
37import System.FilePath ((</>), addTrailingPathSeparator)
39import Paths_idris
41compile :: Codegen -> FilePath -> Term -> Idris ()
42compile codegen f tm
43 = do checkMVs
44 let tmnames = namesUsed (STerm tm)
45 usedIn <- mapM (allNames []) tmnames
46 let used = sUN "prim__subBigInt" : sUN "prim__addBigInt" : concat usedIn
47 defsIn <- mkDecls tm used
48 findUnusedArgs used
50 -- TODO: DEBUG-ONLY, remove
51 ist <- getIState
52 let usedF = findUsed (tt_ctxt ist) (idris_callgraph ist) used
53 let printCond (ctors, cond) = "if " ++ show (S.toList cond) ++ " -ctors- " ++ show (S.toList ctors)
54 let printDep (i, conds) = unlines . map (" "++) $ (show i : map printCond (S.toList conds))
55 let printItem (fn, deps) = unlines (show fn : map printDep (IM.toList deps))
56 iLOG $ "USAGE ANALYSIS:\n" ++ unlines (map printItem . M.toList $ usedF)
57 -- END TODO
59 maindef <- irMain tm
60 objs <- getObjectFiles codegen
61 libs <- getLibs codegen
62 flags <- getFlags codegen
63 hdrs <- getHdrs codegen
64 impdirs <- allImportDirs
65 let defs = defsIn ++ [(sMN 0 "runMain", maindef)]
66 -- iputStrLn $ showSep "\n" (map show defs)
67 let (nexttag, tagged) = addTags 65536 (liftAll defs)
68 let ctxtIn = addAlist tagged emptyContext
69 iLOG "Defunctionalising"
70 let defuns_in = defunctionalise nexttag ctxtIn
71 logLvl 5 $ show defuns_in
72 iLOG "Inlining"
73 let defuns = inline defuns_in
74 logLvl 5 $ show defuns
75 iLOG "Resolving variables for CG"
76 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))
77 let checked = checkDefs defuns (toAlist defuns)
78 outty <- outputTy
79 dumpCases <- getDumpCases
80 dumpDefun <- getDumpDefun
81 case dumpCases of
82 Nothing -> return ()
83 Just f -> runIO $ writeFile f (showCaseTrees defs)
84 case dumpDefun of
85 Nothing -> return ()
86 Just f -> runIO $ writeFile f (dumpDefuns defuns)
87 triple <- Idris.AbsSyntax.targetTriple
88 cpu <- Idris.AbsSyntax.targetCPU
89 optimise <- optLevel
90 iLOG "Building output"
92 case checked of
93 OK c -> do let cginfo = CodegenInfo f outty triple cpu optimise
94 hdrs impdirs objs libs flags
95 NONE c (toAlist defuns)
96 tagged
97 runIO $ case codegen of
98 ViaC -> codegenC cginfo
99 ViaJava -> codegenJava cginfo
100 ViaJavaScript -> codegenJavaScript cginfo
101 ViaNode -> codegenNode cginfo
102 ViaLLVM -> codegenLLVM cginfo
103 Bytecode -> dumpBC c f
104 Error e -> ierror e
105 where checkMVs = do i <- getIState
106 case map fst (idris_metavars i) \\ primDefs of
107 [] -> return ()
108 ms -> ifail $ "There are undefined metavariables: " ++ show ms
109 inDir d h = do let f = d </> h
110 ex <- doesFileExist f
111 if ex then return f else return h
113irMain :: TT Name -> Idris LDecl
114irMain tm = do i <- ir 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 findUnusedArgs used
122 decls <- mapM build ds
123 return decls
125showCaseTrees :: [(Name, LDecl)] -> String
126showCaseTrees ds = showSep "\n\n" (map showCT ds)
127 where
128 showCT (n, LFun _ f args lexp)
129 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t "
130 ++ show lexp
131 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
133isCon (TyDecl _ _) = True
134isCon _ = False
136class ToIR a where
137 ir :: a -> Idris LExp
139build :: (Name, Def) -> Idris (Name, LDecl)
140build (n, d)
141 = do i <- getIState
142 case lookup n (idris_scprims i) of
143 Just (ar, op) ->
144 let args = map (\x -> sMN x "op") [0..] in
145 return (n, (LFun [] n (take ar args)
146 (LOp op (map (LV . Glob) (take ar args)))))
147 _ -> do def <- mkLDecl n d
148 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
149 return (n, def)
151getPrim :: IState -> Name -> [LExp] -> Maybe LExp
152getPrim i n args = case lookup n (idris_scprims i) of
153 Just (ar, op) ->
154 if (ar == length args)
155 then return (LOp op args)
156 else Nothing
157 _ -> Nothing
159declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
160declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
162mkLDecl n (Function tm _) = do e <- ir tm
163 return (declArgs [] True n e)
164mkLDecl n (CaseOp ci _ _ _ pats cd)
165 = let (args, sc) = cases_runtime cd in
166 do e <- ir (args, sc)
167 return (declArgs [] (case_inlinable ci) n e)
168mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
169mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
170mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
172instance ToIR (TT Name) where
173 ir tm = ir' [] tm where
174 ir' env tm@(App f a)
175 | (P _ (UN m) _, args) <- unApply tm,
176 m == txt "mkForeignPrim"
177 = doForeign env args
178 | (P _ (UN u) _, [_, arg]) <- unApply tm,
179 u == txt "unsafePerformPrimIO"
180 = ir' env arg
181 -- TMP HACK - until we get inlining.
182 | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,
183 r == txt "replace"
184 = ir' env arg
185 -- Laziness, the old way
186 | (P _ (UN l) _, [_, arg]) <- unApply tm,
187 l == txt "lazy"
188 = do arg' <- ir' env arg
189 error "lazy has crept in somehow"
190-- return $ LLazyExp arg'
191 | (P _ (UN l) _, [_, arg]) <- unApply tm,
192 l == txt "force"
193 = do arg' <- ir' env arg
194 return $ LForce arg'
195 -- Laziness, the new way
196 | (P _ (UN l) _, [arg]) <- unApply tm,
197 l == txt "Delay"
198 = do arg' <- ir' env arg
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 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
205 a == txt "assert_smaller"
206 = ir' env arg
207 | (P _ (UN a) _, [_, arg]) <- unApply tm,
208 a == txt "assert_total"
209 = ir' env arg
210 | (P _ (UN p) _, [_, arg]) <- unApply tm,
211 p == txt "par"
212 = do arg' <- ir' env arg
213 return $ LOp LPar [LLazyExp arg']
214 | (P _ (UN pf) _, [arg]) <- unApply tm,
215 pf == txt "prim_fork"
216 = do arg' <- ir' env arg
217 return $ LOp LFork [LLazyExp arg']
218 | (P _ (UN m) _, [_,size,t]) <- unApply tm,
219 m == txt "malloc"
220 = do size' <- ir' env size
221 t' <- ir' env t
222 return t' -- TODO $ malloc_ size' t'
223 | (P _ (UN tm) _, [_,t]) <- unApply tm,
224 tm == txt "trace_malloc"
225 = do t' <- ir' env t
226 return t' -- TODO
227 -- This case is here until we get more general inlining. It's just
228 -- a really common case, and the laziness hurts...
229 | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
230 (App (P _ (UN d') _) e)]) <- unApply tm,
231 be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"
232 = do x' <- ir' env x
233 t' <- ir' env t
234 e' <- ir' env e
235 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',
236 LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])
237 | (P (DCon t a) n _, args) <- unApply tm
238 = irCon env t a n args
239 | (P (TCon t a) n _, args) <- unApply tm
240 = return LNothing
241 | (P _ n _, args) <- unApply tm
242 = do i <- getIState
243 args' <- mapM (ir' env) args
244 case getPrim i n args' of
245 Just tm -> return tm
246 _ -> do
247 let collapse
248 = case lookupCtxtExact n
249 (idris_optimisation i) of
250 Just oi -> collapsible oi
251 _ -> False
252 let unused
253 = case lookupCtxtExact n
254 (idris_callgraph i) of
255 Just (CGInfo _ _ _ _ unusedpos) ->
256 unusedpos
257 _ -> []
258 if collapse
259 then return LNothing
260 else return (LApp False (LV (Glob n))
261 (mkUnused unused 0 args'))
262 | (f, args) <- unApply tm
263 = do f' <- ir' env f
264 args' <- mapM (ir' env) args
265 return (LApp False f' args')
266 where mkUnused u i [] = []
267 mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
268 | otherwise = x : mkUnused u (i + 1) xs
269-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
270-- = return $ LConst (BI 0)
271 ir' env (P _ n _) = return $ LV (Glob n)
272 ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
273 | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm
274 ir' env (Bind n (Lam _) sc)
275 = do let n' = uniqueName n env
276 sc' <- ir' (n' : env) sc
277 return $ LLam [n'] sc'
278 ir' env (Bind n (Let _ v) sc)
279 = do sc' <- ir' (n : env) sc
280 v' <- ir' env v
281 return $ LLet n v' sc'
282 ir' env (Bind _ _ _) = return $ LNothing
283 ir' env (Proj t i) | i == -1
284 = do t' <- ir' env t
285 return $ LOp (LMinus (ATInt ITBig))
286 [t', LConst (BI 1)]
287 ir' env (Proj t i) = do t' <- ir' env t
288 return $ LProj t' i
289 ir' env (Constant c) = return $ LConst c
290 ir' env (TType _) = return $ LNothing
291 ir' env Erased = return $ LNothing
292 ir' env Impossible = return $ LNothing
293-- ir' env _ = return $ LError "Impossible"
295 irCon env t arity n args
296 | length args == arity = buildApp env (LV (Glob n)) args
297 | otherwise = let extra = satArgs (arity - length args) in
298 do sc' <- irCon env t arity n
299 (args ++ map (\n -> P Bound n undefined) extra)
300 return $ LLam extra sc'
302 satArgs n = map (\i -> sMN i "sat") [1..n]
304 buildApp env e [] = return e
305 buildApp env e xs = do xs' <- mapM (ir' env) xs
306 return $ LApp False e xs'
308 doForeign :: [Name] -> [TT Name] -> Idris LExp
309 doForeign env (_ : fgn : args)
310 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
311 = let maybeTys = getFTypes fgnArgTys
312 rty = mkIty' ret in
313 case maybeTys of
314 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
315 Just tys -> do
316 args' <- mapM (ir' env) (init args)
317 -- wrap it in a prim__IO
318 -- return $ con_ 0 @@ impossible @@
319 return $ -- LLazyExp $
320 LForeign LANG_C rty fgnName (zip tys args')
321 | otherwise = ifail "Badly formed foreign function call"
323getFTypes :: TT Name -> Maybe [FType]
324getFTypes tm = case unApply tm of
325 (nil, []) -> Just []
326 (cons, [ty, xs]) ->
327 fmap (mkIty' ty :) (getFTypes xs)
328 _ -> Nothing
330mkIty' (P _ (UN ty) _) = mkIty (str ty)
331mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
332 | fi == txt "FIntT" = mkIntIty (str intTy)
333mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
334 | ff == txt "FFunction" && fa == txt "FAny" &&
335 io == txt "IO"
336 = FFunctionIO
337mkIty' (App (App (P _ (UN ff) _) _) _)
338 | ff == txt "FFunction" = FFunction
339mkIty' _ = FAny
341-- would be better if these FInt types were evaluated at compile time
342-- TODO: add %eval directive for such things
344mkIty "FFloat" = FArith ATFloat
345mkIty "FInt" = mkIntIty "ITNative"
346mkIty "FChar" = mkIntIty "ITChar"
347mkIty "FByte" = mkIntIty "IT8"
348mkIty "FShort" = mkIntIty "IT16"
349mkIty "FLong" = mkIntIty "IT64"
350mkIty "FBits8" = mkIntIty "IT8"
351mkIty "FBits16" = mkIntIty "IT16"
352mkIty "FBits32" = mkIntIty "IT32"
353mkIty "FBits64" = mkIntIty "IT64"
354mkIty "FString" = FString
355mkIty "FPtr" = FPtr
356mkIty "FManagedPtr" = FManagedPtr
357mkIty "FUnit" = FUnit
358mkIty "FFunction" = FFunction
359mkIty "FFunctionIO" = FFunctionIO
360mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
361mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
362mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
363mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
364mkIty x = error $ "Unknown type " ++ x
366mkIntIty "ITNative" = FArith (ATInt ITNative)
367mkIntIty "ITChar" = FArith (ATInt ITChar)
368mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
369mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
370mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
371mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
373zname = sNS (sUN "Z") ["Nat","Prelude"]
374sname = sNS (sUN "S") ["Nat","Prelude"]
376instance ToIR ([Name], SC) where
377 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
378 tree' <- ir tree
379 return $ LLam args tree'
381instance ToIR SC where
382 ir t = ir' t where
384 ir' (STerm t) = ir t
385 ir' (UnmatchedCase str) = return $ LError str
386 ir' (ProjCase tm alt) = do tm' <- ir tm
387 alt' <- mkIRAlt tm' alt
388 return $ LCase tm' [alt']
389 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
390 return $ LCase (LV (Glob n)) alts'
391 ir' ImpossibleCase = return LNothing
393 -- special cases for Z and S
394 -- Needs rethink: projections make this fail
395-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
396-- = mkIRAlt n (ConstCase (BI 0) rhs)
397-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
398-- = do n' <- ir n
399-- rhs' <- ir rhs
400-- return $ LDefaultCase
401-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
402-- rhs')
403 mkIRAlt _ (ConCase n t args rhs)
404 = do rhs' <- ir rhs
405 return $ LConCase (-1) n args rhs'
406 mkIRAlt _ (ConstCase x rhs)
407 | matchable x
408 = do rhs' <- ir rhs
409 return $ LConstCase x rhs'
410 | matchableTy x
411 = do rhs' <- ir rhs
412 return $ LDefaultCase rhs'
413 mkIRAlt tm (SucCase n rhs)
414 = do rhs' <- ir rhs
415 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
416 [tm,
417 LConst (BI 1)]) rhs')
418-- return $ LSucCase n rhs'
419 mkIRAlt _ (ConstCase c rhs)
420 = ifail $ "Can't match on (" ++ show c ++ ")"
421 mkIRAlt _ (DefaultCase rhs)
422 = do rhs' <- ir rhs
423 return $ LDefaultCase rhs'
425 matchable (I _) = True
426 matchable (BI _) = True
427 matchable (Ch _) = True
428 matchable (Str _) = True
429 matchable _ = False
431 matchableTy (AType (ATInt ITNative)) = True
432 matchableTy (AType (ATInt ITBig)) = True
433 matchableTy (AType (ATInt ITChar)) = True
434 matchableTy StrType = True
436 matchableTy (AType (ATInt (ITFixed IT8))) = True
437 matchableTy (AType (ATInt (ITFixed IT16))) = True
438 matchableTy (AType (ATInt (ITFixed IT32))) = True
439 matchableTy (AType (ATInt (ITFixed IT64))) = True
441 matchableTy _ = False