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