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