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