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