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