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