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