git.iko.soy/Idris-dev
on 589bb4b help sign in
Idris-dev/src/IRTS/Compiler.hs
475 lines 20 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: " ++ 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
280 (idris_optimisation i) of
281 Just oi -> collapsible oi
282 _ -> False
283 let used
284 = case lookupCtxtExact n
285 (idris_callgraph i) of
286 Just (CGInfo _ _ _ _ usedpos) ->
287 usedpos
288 _ -> [] -- TODO: is this correct?
289 if collapse
290 then return LNothing
291 else do
292 iLOG $ "ERASE:\n " ++ show tm ++ "\n ==>\n " ++ show (LApp False (LV (Glob n)) (mkUsed used 0 args'))
293 return (LApp False (LV (Glob n))
294 (mkUsed used 0 args'))
295 | (f, args) <- unApply tm
296 = do f' <- ir' env f
297 args' <- mapM (ir' env) args
298 return (LApp False f' args')
299 where mkUsed u i [] = []
300 mkUsed u i (x : xs) | i `elem` u = x : mkUsed u (i + 1) xs
301 | otherwise = LNothing : mkUsed u (i + 1) xs
302-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
303-- = return $ LConst (BI 0)
304 ir' env (P _ n _) = return $ LV (Glob n)
305 ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
306 | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm
307 ir' env (Bind n (Lam _) sc)
308 = do let n' = uniqueName n env
309 sc' <- ir' (n' : env) sc
310 return $ LLam [n'] sc'
311 ir' env (Bind n (Let _ v) sc)
312 = do sc' <- ir' (n : env) sc
313 v' <- ir' env v
314 return $ LLet n v' sc'
315 ir' env (Bind _ _ _) = return $ LNothing
316 ir' env (Proj t i) | i == -1
317 = do t' <- ir' env t
318 return $ LOp (LMinus (ATInt ITBig))
319 [t', LConst (BI 1)]
320 ir' env (Proj t i) = do t' <- ir' env t
321 return $ LProj t' i
322 ir' env (Constant c) = return $ LConst c
323 ir' env (TType _) = return $ LNothing
324 ir' env Erased = return $ LNothing
325 ir' env Impossible = return $ LNothing
326-- ir' env _ = return $ LError "Impossible"
328 irCon env t arity n args
329 | length args == arity = buildApp env (LV (Glob n)) args
330 | otherwise = let extra = satArgs (arity - length args) in
331 do sc' <- irCon env t arity n
332 (args ++ map (\n -> P Bound n undefined) extra)
333 return $ LLam extra sc'
335 satArgs n = map (\i -> sMN i "sat") [1..n]
337 buildApp env e [] = return e
338 buildApp env e xs = do xs' <- mapM (ir' env) xs
339 return $ LApp False e xs'
341 doForeign :: [Name] -> [TT Name] -> Idris LExp
342 doForeign env (_ : fgn : args)
343 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
344 = let maybeTys = getFTypes fgnArgTys
345 rty = mkIty' ret in
346 case maybeTys of
347 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
348 Just tys -> do
349 args' <- mapM (ir' env) (init args)
350 -- wrap it in a prim__IO
351 -- return $ con_ 0 @@ impossible @@
352 return $ -- LLazyExp $
353 LForeign LANG_C rty fgnName (zip tys args')
354 | otherwise = ifail "Badly formed foreign function call"
356getFTypes :: TT Name -> Maybe [FType]
357getFTypes tm = case unApply tm of
358 (nil, []) -> Just []
359 (cons, [ty, xs]) ->
360 fmap (mkIty' ty :) (getFTypes xs)
361 _ -> Nothing
363mkIty' (P _ (UN ty) _) = mkIty (str ty)
364mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
365 | fi == txt "FIntT" = mkIntIty (str intTy)
366mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
367 | ff == txt "FFunction" && fa == txt "FAny" &&
368 io == txt "IO"
369 = FFunctionIO
370mkIty' (App (App (P _ (UN ff) _) _) _)
371 | ff == txt "FFunction" = FFunction
372mkIty' _ = FAny
374-- would be better if these FInt types were evaluated at compile time
375-- TODO: add %eval directive for such things
377mkIty "FFloat" = FArith ATFloat
378mkIty "FInt" = mkIntIty "ITNative"
379mkIty "FChar" = mkIntIty "ITChar"
380mkIty "FByte" = mkIntIty "IT8"
381mkIty "FShort" = mkIntIty "IT16"
382mkIty "FLong" = mkIntIty "IT64"
383mkIty "FBits8" = mkIntIty "IT8"
384mkIty "FBits16" = mkIntIty "IT16"
385mkIty "FBits32" = mkIntIty "IT32"
386mkIty "FBits64" = mkIntIty "IT64"
387mkIty "FString" = FString
388mkIty "FPtr" = FPtr
389mkIty "FManagedPtr" = FManagedPtr
390mkIty "FUnit" = FUnit
391mkIty "FFunction" = FFunction
392mkIty "FFunctionIO" = FFunctionIO
393mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
394mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
395mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
396mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
397mkIty x = error $ "Unknown type " ++ x
399mkIntIty "ITNative" = FArith (ATInt ITNative)
400mkIntIty "ITChar" = FArith (ATInt ITChar)
401mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
402mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
403mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
404mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
406zname = sNS (sUN "Z") ["Nat","Prelude"]
407sname = sNS (sUN "S") ["Nat","Prelude"]
409instance ToIR ([Name], SC) where
410 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
411 tree' <- ir tree
412 return $ LLam args tree'
414instance ToIR SC where
415 ir t = ir' t where
417 ir' (STerm t) = ir t
418 ir' (UnmatchedCase str) = return $ LError str
419 ir' (ProjCase tm alt) = do tm' <- ir tm
420 alt' <- mkIRAlt tm' alt
421 return $ LCase tm' [alt']
422 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
423 return $ LCase (LV (Glob n)) alts'
424 ir' ImpossibleCase = return LNothing
426 -- special cases for Z and S
427 -- Needs rethink: projections make this fail
428-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
429-- = mkIRAlt n (ConstCase (BI 0) rhs)
430-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
431-- = do n' <- ir n
432-- rhs' <- ir rhs
433-- return $ LDefaultCase
434-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
435-- rhs')
436 mkIRAlt _ (ConCase n t args rhs)
437 = do rhs' <- ir rhs
438 return $ LConCase (-1) n args rhs'
439 mkIRAlt _ (ConstCase x rhs)
440 | matchable x
441 = do rhs' <- ir rhs
442 return $ LConstCase x rhs'
443 | matchableTy x
444 = do rhs' <- ir rhs
445 return $ LDefaultCase rhs'
446 mkIRAlt tm (SucCase n rhs)
447 = do rhs' <- ir rhs
448 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
449 [tm,
450 LConst (BI 1)]) rhs')
451-- return $ LSucCase n rhs'
452 mkIRAlt _ (ConstCase c rhs)
453 = ifail $ "Can't match on (" ++ show c ++ ")"
454 mkIRAlt _ (DefaultCase rhs)
455 = do rhs' <- ir rhs
456 return $ LDefaultCase rhs'
458 matchable (I _) = True
459 matchable (BI _) = True
460 matchable (Ch _) = True
461 matchable (Str _) = True
462 matchable _ = False
464 matchableTy (AType (ATInt ITNative)) = True
465 matchableTy (AType (ATInt ITBig)) = True
466 matchableTy (AType (ATInt ITChar)) = True
467 matchableTy StrType = True
469 matchableTy (AType (ATInt (ITFixed IT8))) = True
470 matchableTy (AType (ATInt (ITFixed IT16))) = True
471 matchableTy (AType (ATInt (ITFixed IT32))) = True
472 matchableTy (AType (ATInt (ITFixed IT64))) = True
474 matchableTy _ = False