git.iko.soy/Idris-dev
on ccadc82 help sign in
Idris-dev/src/IRTS/Compiler.hs
436 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.Map as M
31import System.Process
32import System.IO
33import System.Directory
34import System.Environment
35import System.FilePath ((</>), addTrailingPathSeparator)
37import Paths_idris
39compile :: Codegen -> FilePath -> Term -> Idris ()
40compile codegen f tm
41 = do checkMVs
42 let tmnames = namesUsed (STerm tm)
43 usedIn <- mapM (allNames []) tmnames
44 let used = [sUN "prim__subBigInt", sUN "prim__addBigInt"] : usedIn
45 defsIn <- mkDecls tm (concat used)
46 findUnusedArgs (concat used)
48 -- TODO: DEBUG-ONLY, remove
49 ist <- getIState
50 let usedCtorArgs = findUsed (tt_ctxt ist) (idris_callgraph ist) (concat used)
51 iLOG $ "USED CTOR ARGS:\n" ++ unlines (map show . M.toList $ usedCtorArgs)
53 maindef <- irMain tm
54 objs <- getObjectFiles codegen
55 libs <- getLibs codegen
56 flags <- getFlags codegen
57 hdrs <- getHdrs codegen
58 impdirs <- allImportDirs
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 findUnusedArgs used
116 decls <- mapM build ds
117 return decls
119showCaseTrees :: [(Name, LDecl)] -> String
120showCaseTrees ds = showSep "\n\n" (map showCT ds)
121 where
122 showCT (n, LFun _ f args lexp)
123 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t "
124 ++ show lexp
125 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
127isCon (TyDecl _ _) = True
128isCon _ = False
130class ToIR a where
131 ir :: a -> Idris LExp
133build :: (Name, Def) -> Idris (Name, LDecl)
134build (n, d)
135 = do i <- getIState
136 case lookup n (idris_scprims i) of
137 Just (ar, op) ->
138 let args = map (\x -> sMN x "op") [0..] in
139 return (n, (LFun [] n (take ar args)
140 (LOp op (map (LV . Glob) (take ar args)))))
141 _ -> do def <- mkLDecl n d
142 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
143 return (n, def)
145getPrim :: IState -> Name -> [LExp] -> Maybe LExp
146getPrim i n args = case lookup n (idris_scprims i) of
147 Just (ar, op) ->
148 if (ar == length args)
149 then return (LOp op args)
150 else Nothing
151 _ -> Nothing
153declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
154declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
156mkLDecl n (Function tm _) = do e <- ir tm
157 return (declArgs [] True n e)
158mkLDecl n (CaseOp ci _ _ _ pats cd)
159 = let (args, sc) = cases_runtime cd in
160 do e <- ir (args, sc)
161 return (declArgs [] (case_inlinable ci) n e)
162mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
163mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
164mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
166instance ToIR (TT Name) where
167 ir tm = ir' [] tm where
168 ir' env tm@(App f a)
169 | (P _ (UN m) _, args) <- unApply tm,
170 m == txt "mkForeignPrim"
171 = doForeign env args
172 | (P _ (UN u) _, [_, arg]) <- unApply tm,
173 u == txt "unsafePerformPrimIO"
174 = ir' env arg
175 -- TMP HACK - until we get inlining.
176 | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,
177 r == txt "replace"
178 = ir' env arg
179 -- Laziness, the old way
180 | (P _ (UN l) _, [_, arg]) <- unApply tm,
181 l == txt "lazy"
182 = do arg' <- ir' env arg
183 error "lazy has crept in somehow"
184-- return $ LLazyExp arg'
185 | (P _ (UN l) _, [_, arg]) <- unApply tm,
186 l == txt "force"
187 = do arg' <- ir' env arg
188 return $ LForce arg'
189 -- Laziness, the new way
190 | (P _ (UN l) _, [arg]) <- unApply tm,
191 l == txt "Delay"
192 = do arg' <- ir' env arg
193 return $ LLazyExp arg'
194 | (P _ (UN l) _, [_, _, arg]) <- unApply tm,
195 l == txt "Force"
196 = do arg' <- ir' env arg
197 return $ LForce arg'
198 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
199 a == txt "assert_smaller"
200 = ir' env arg
201 | (P _ (UN a) _, [_, arg]) <- unApply tm,
202 a == txt "assert_total"
203 = ir' env arg
204 | (P _ (UN p) _, [_, arg]) <- unApply tm,
205 p == txt "par"
206 = do arg' <- ir' env arg
207 return $ LOp LPar [LLazyExp arg']
208 | (P _ (UN pf) _, [arg]) <- unApply tm,
209 pf == txt "prim_fork"
210 = do arg' <- ir' env arg
211 return $ LOp LFork [LLazyExp arg']
212 | (P _ (UN m) _, [_,size,t]) <- unApply tm,
213 m == txt "malloc"
214 = do size' <- ir' env size
215 t' <- ir' env t
216 return t' -- TODO $ malloc_ size' t'
217 | (P _ (UN tm) _, [_,t]) <- unApply tm,
218 tm == txt "trace_malloc"
219 = do t' <- ir' env t
220 return t' -- TODO
221 -- This case is here until we get more general inlining. It's just
222 -- a really common case, and the laziness hurts...
223 | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
224 (App (P _ (UN d') _) e)]) <- unApply tm,
225 be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"
226 = do x' <- ir' env x
227 t' <- ir' env t
228 e' <- ir' env e
229 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',
230 LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])
231 | (P (DCon t a) n _, args) <- unApply tm
232 = irCon env t a n args
233 | (P (TCon t a) n _, args) <- unApply tm
234 = return LNothing
235 | (P _ n _, args) <- unApply tm
236 = do i <- getIState
237 args' <- mapM (ir' env) args
238 case getPrim i n args' of
239 Just tm -> return tm
240 _ -> do
241 let collapse
242 = case lookupCtxtExact n
243 (idris_optimisation i) of
244 Just oi -> collapsible oi
245 _ -> False
246 let unused
247 = case lookupCtxtExact n
248 (idris_callgraph i) of
249 Just (CGInfo _ _ _ _ unusedpos) ->
250 unusedpos
251 _ -> []
252 if collapse
253 then return LNothing
254 else return (LApp False (LV (Glob n))
255 (mkUnused unused 0 args'))
256 | (f, args) <- unApply tm
257 = do f' <- ir' env f
258 args' <- mapM (ir' env) args
259 return (LApp False f' args')
260 where mkUnused u i [] = []
261 mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
262 | otherwise = x : mkUnused u (i + 1) xs
263-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
264-- = return $ LConst (BI 0)
265 ir' env (P _ n _) = return $ LV (Glob n)
266 ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
267 | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm
268 ir' env (Bind n (Lam _) sc)
269 = do let n' = uniqueName n env
270 sc' <- ir' (n' : env) sc
271 return $ LLam [n'] sc'
272 ir' env (Bind n (Let _ v) sc)
273 = do sc' <- ir' (n : env) sc
274 v' <- ir' env v
275 return $ LLet n v' sc'
276 ir' env (Bind _ _ _) = return $ LNothing
277 ir' env (Proj t i) | i == -1
278 = do t' <- ir' env t
279 return $ LOp (LMinus (ATInt ITBig))
280 [t', LConst (BI 1)]
281 ir' env (Proj t i) = do t' <- ir' env t
282 return $ LProj t' i
283 ir' env (Constant c) = return $ LConst c
284 ir' env (TType _) = return $ LNothing
285 ir' env Erased = return $ LNothing
286 ir' env Impossible = return $ LNothing
287-- ir' env _ = return $ LError "Impossible"
289 irCon env t arity n args
290 | length args == arity = buildApp env (LV (Glob n)) args
291 | otherwise = let extra = satArgs (arity - length args) in
292 do sc' <- irCon env t arity n
293 (args ++ map (\n -> P Bound n undefined) extra)
294 return $ LLam extra sc'
296 satArgs n = map (\i -> sMN i "sat") [1..n]
298 buildApp env e [] = return e
299 buildApp env e xs = do xs' <- mapM (ir' env) xs
300 return $ LApp False e xs'
302 doForeign :: [Name] -> [TT Name] -> Idris LExp
303 doForeign env (_ : fgn : args)
304 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
305 = let maybeTys = getFTypes fgnArgTys
306 rty = mkIty' ret in
307 case maybeTys of
308 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
309 Just tys -> do
310 args' <- mapM (ir' env) (init args)
311 -- wrap it in a prim__IO
312 -- return $ con_ 0 @@ impossible @@
313 return $ -- LLazyExp $
314 LForeign LANG_C rty fgnName (zip tys args')
315 | otherwise = ifail "Badly formed foreign function call"
317getFTypes :: TT Name -> Maybe [FType]
318getFTypes tm = case unApply tm of
319 (nil, []) -> Just []
320 (cons, [ty, xs]) ->
321 fmap (mkIty' ty :) (getFTypes xs)
322 _ -> Nothing
324mkIty' (P _ (UN ty) _) = mkIty (str ty)
325mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
326 | fi == txt "FIntT" = mkIntIty (str intTy)
327mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
328 | ff == txt "FFunction" && fa == txt "FAny" &&
329 io == txt "IO"
330 = FFunctionIO
331mkIty' (App (App (P _ (UN ff) _) _) _)
332 | ff == txt "FFunction" = FFunction
333mkIty' _ = FAny
335-- would be better if these FInt types were evaluated at compile time
336-- TODO: add %eval directive for such things
338mkIty "FFloat" = FArith ATFloat
339mkIty "FInt" = mkIntIty "ITNative"
340mkIty "FChar" = mkIntIty "ITChar"
341mkIty "FByte" = mkIntIty "IT8"
342mkIty "FShort" = mkIntIty "IT16"
343mkIty "FLong" = mkIntIty "IT64"
344mkIty "FBits8" = mkIntIty "IT8"
345mkIty "FBits16" = mkIntIty "IT16"
346mkIty "FBits32" = mkIntIty "IT32"
347mkIty "FBits64" = mkIntIty "IT64"
348mkIty "FString" = FString
349mkIty "FPtr" = FPtr
350mkIty "FManagedPtr" = FManagedPtr
351mkIty "FUnit" = FUnit
352mkIty "FFunction" = FFunction
353mkIty "FFunctionIO" = FFunctionIO
354mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
355mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
356mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
357mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
358mkIty x = error $ "Unknown type " ++ x
360mkIntIty "ITNative" = FArith (ATInt ITNative)
361mkIntIty "ITChar" = FArith (ATInt ITChar)
362mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
363mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
364mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
365mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
367zname = sNS (sUN "Z") ["Nat","Prelude"]
368sname = sNS (sUN "S") ["Nat","Prelude"]
370instance ToIR ([Name], SC) where
371 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
372 tree' <- ir tree
373 return $ LLam args tree'
375instance ToIR SC where
376 ir t = ir' t where
378 ir' (STerm t) = ir t
379 ir' (UnmatchedCase str) = return $ LError str
380 ir' (ProjCase tm alt) = do tm' <- ir tm
381 alt' <- mkIRAlt tm' alt
382 return $ LCase tm' [alt']
383 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
384 return $ LCase (LV (Glob n)) alts'
385 ir' ImpossibleCase = return LNothing
387 -- special cases for Z and S
388 -- Needs rethink: projections make this fail
389-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
390-- = mkIRAlt n (ConstCase (BI 0) rhs)
391-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
392-- = do n' <- ir n
393-- rhs' <- ir rhs
394-- return $ LDefaultCase
395-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
396-- rhs')
397 mkIRAlt _ (ConCase n t args rhs)
398 = do rhs' <- ir rhs
399 return $ LConCase (-1) n args rhs'
400 mkIRAlt _ (ConstCase x rhs)
401 | matchable x
402 = do rhs' <- ir rhs
403 return $ LConstCase x rhs'
404 | matchableTy x
405 = do rhs' <- ir rhs
406 return $ LDefaultCase rhs'
407 mkIRAlt tm (SucCase n rhs)
408 = do rhs' <- ir rhs
409 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
410 [tm,
411 LConst (BI 1)]) rhs')
412-- return $ LSucCase n rhs'
413 mkIRAlt _ (ConstCase c rhs)
414 = ifail $ "Can't match on (" ++ show c ++ ")"
415 mkIRAlt _ (DefaultCase rhs)
416 = do rhs' <- ir rhs
417 return $ LDefaultCase rhs'
419 matchable (I _) = True
420 matchable (BI _) = True
421 matchable (Ch _) = True
422 matchable (Str _) = True
423 matchable _ = False
425 matchableTy (AType (ATInt ITNative)) = True
426 matchableTy (AType (ATInt ITBig)) = True
427 matchableTy (AType (ATInt ITChar)) = True
428 matchableTy StrType = True
430 matchableTy (AType (ATInt (ITFixed IT8))) = True
431 matchableTy (AType (ATInt (ITFixed IT16))) = True
432 matchableTy (AType (ATInt (ITFixed IT32))) = True
433 matchableTy (AType (ATInt (ITFixed IT64))) = True
435 matchableTy _ = False