git.iko.soy/Idris-dev
on 4caab41 help sign in
Idris-dev/src/IRTS/Compiler.hs
458 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
50 defsIn <- mkDecls tm used
51 findUnusedArgs used
53 -- TODO: traverse all names correctly
55 -- TODO: DEBUG-ONLY, remove
56 ctx <- tt_ctxt <$> getIState
57 let depMap = buildDepMap 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 fmtDepMap = unlines . map (\(n,is) -> show n ++ " -> " ++ show (IS.toList is)) . M.toList
62 let minUse = minimalUsage depMap
63 iLOG $ "MINIMAL USAGE:\n" ++ fmtDepMap minUse
65 mapM_ (uncurry storeUsage) (M.toList minUse)
66 -- END TODO
68 maindef <- irMain tm
69 objs <- getObjectFiles codegen
70 libs <- getLibs codegen
71 flags <- getFlags codegen
72 hdrs <- getHdrs codegen
73 impdirs <- allImportDirs
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 findUnusedArgs used
138 decls <- mapM build ds
139 return decls
141showCaseTrees :: [(Name, LDecl)] -> String
142showCaseTrees ds = showSep "\n\n" (map showCT ds)
143 where
144 showCT (n, LFun _ f args lexp)
145 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t "
146 ++ show lexp
147 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
149isCon (TyDecl _ _) = True
150isCon _ = False
152class ToIR a where
153 ir :: a -> Idris LExp
155build :: (Name, Def) -> Idris (Name, LDecl)
156build (n, d)
157 = do i <- getIState
158 case lookup n (idris_scprims i) of
159 Just (ar, op) ->
160 let args = map (\x -> sMN x "op") [0..] in
161 return (n, (LFun [] n (take ar args)
162 (LOp op (map (LV . Glob) (take ar args)))))
163 _ -> do def <- mkLDecl n d
164 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
165 return (n, def)
167getPrim :: IState -> Name -> [LExp] -> Maybe LExp
168getPrim i n args = case lookup n (idris_scprims i) of
169 Just (ar, op) ->
170 if (ar == length args)
171 then return (LOp op args)
172 else Nothing
173 _ -> Nothing
175declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
176declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
178mkLDecl n (Function tm _) = do e <- ir tm
179 return (declArgs [] True n e)
180mkLDecl n (CaseOp ci _ _ _ pats cd)
181 = let (args, sc) = cases_runtime cd in
182 do e <- ir (args, sc)
183 return (declArgs [] (case_inlinable ci) n e)
184mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
185mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
186mkLDecl n _ = return $ (declArgs [] True n LNothing) -- postulate, never run
188instance ToIR (TT Name) where
189 ir tm = ir' [] tm where
190 ir' env tm@(App f a)
191 | (P _ (UN m) _, args) <- unApply tm,
192 m == txt "mkForeignPrim"
193 = doForeign env args
194 | (P _ (UN u) _, [_, arg]) <- unApply tm,
195 u == txt "unsafePerformPrimIO"
196 = ir' env arg
197 -- TMP HACK - until we get inlining.
198 | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,
199 r == txt "replace"
200 = ir' env arg
201 -- Laziness, the old way
202 | (P _ (UN l) _, [_, arg]) <- unApply tm,
203 l == txt "lazy"
204 = do arg' <- ir' env arg
205 error "lazy has crept in somehow"
206-- return $ LLazyExp arg'
207 | (P _ (UN l) _, [_, arg]) <- unApply tm,
208 l == txt "force"
209 = do arg' <- ir' env arg
210 return $ LForce arg'
211 -- Laziness, the new way
212 | (P _ (UN l) _, [arg]) <- unApply tm,
213 l == txt "Delay"
214 = do arg' <- ir' env arg
215 return $ LLazyExp arg'
216 | (P _ (UN l) _, [_, _, arg]) <- unApply tm,
217 l == txt "Force"
218 = do arg' <- ir' env arg
219 return $ LForce arg'
220 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
221 a == txt "assert_smaller"
222 = ir' env arg
223 | (P _ (UN a) _, [_, arg]) <- unApply tm,
224 a == txt "assert_total"
225 = ir' env arg
226 | (P _ (UN p) _, [_, arg]) <- unApply tm,
227 p == txt "par"
228 = do arg' <- ir' env arg
229 return $ LOp LPar [LLazyExp arg']
230 | (P _ (UN pf) _, [arg]) <- unApply tm,
231 pf == txt "prim_fork"
232 = do arg' <- ir' env arg
233 return $ LOp LFork [LLazyExp arg']
234 | (P _ (UN m) _, [_,size,t]) <- unApply tm,
235 m == txt "malloc"
236 = do size' <- ir' env size
237 t' <- ir' env t
238 return t' -- TODO $ malloc_ size' t'
239 | (P _ (UN tm) _, [_,t]) <- unApply tm,
240 tm == txt "trace_malloc"
241 = do t' <- ir' env t
242 return t' -- TODO
243 -- This case is here until we get more general inlining. It's just
244 -- a really common case, and the laziness hurts...
245 | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
246 (App (P _ (UN d') _) e)]) <- unApply tm,
247 be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"
248 = do x' <- ir' env x
249 t' <- ir' env t
250 e' <- ir' env e
251 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',
252 LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])
253 | (P (DCon t a) n _, args) <- unApply tm
254 = irCon env t a n args
255 | (P (TCon t a) n _, args) <- unApply tm
256 = return LNothing
257 | (P _ n _, args) <- unApply tm
258 = do i <- getIState
259 args' <- mapM (ir' env) args
260 case getPrim i n args' of
261 Just tm -> return tm
262 _ -> do
263 let collapse
264 = case lookupCtxtExact n
265 (idris_optimisation i) of
266 Just oi -> collapsible oi
267 _ -> False
268 let used
269 = case lookupCtxtExact n
270 (idris_callgraph i) of
271 Just (CGInfo _ _ _ _ usedpos) ->
272 usedpos
273 _ -> [] -- TODO: is this correct?
274 if collapse
275 then return LNothing
276 else return (LApp False (LV (Glob n))
277 (mkUsed used 0 args'))
278 | (f, args) <- unApply tm
279 = do f' <- ir' env f
280 args' <- mapM (ir' env) args
281 return (LApp False f' args')
282 where mkUsed u i [] = []
283 mkUsed u i (x : xs) | i `notElem` u = LNothing : mkUsed u (i + 1) xs
284 | otherwise = x : mkUsed u (i + 1) xs
285-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
286-- = return $ LConst (BI 0)
287 ir' env (P _ n _) = return $ LV (Glob n)
288 ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
289 | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm
290 ir' env (Bind n (Lam _) sc)
291 = do let n' = uniqueName n env
292 sc' <- ir' (n' : env) sc
293 return $ LLam [n'] sc'
294 ir' env (Bind n (Let _ v) sc)
295 = do sc' <- ir' (n : env) sc
296 v' <- ir' env v
297 return $ LLet n v' sc'
298 ir' env (Bind _ _ _) = return $ LNothing
299 ir' env (Proj t i) | i == -1
300 = do t' <- ir' env t
301 return $ LOp (LMinus (ATInt ITBig))
302 [t', LConst (BI 1)]
303 ir' env (Proj t i) = do t' <- ir' env t
304 return $ LProj t' i
305 ir' env (Constant c) = return $ LConst c
306 ir' env (TType _) = return $ LNothing
307 ir' env Erased = return $ LNothing
308 ir' env Impossible = return $ LNothing
309-- ir' env _ = return $ LError "Impossible"
311 irCon env t arity n args
312 | length args == arity = buildApp env (LV (Glob n)) args
313 | otherwise = let extra = satArgs (arity - length args) in
314 do sc' <- irCon env t arity n
315 (args ++ map (\n -> P Bound n undefined) extra)
316 return $ LLam extra sc'
318 satArgs n = map (\i -> sMN i "sat") [1..n]
320 buildApp env e [] = return e
321 buildApp env e xs = do xs' <- mapM (ir' env) xs
322 return $ LApp False e xs'
324 doForeign :: [Name] -> [TT Name] -> Idris LExp
325 doForeign env (_ : fgn : args)
326 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
327 = let maybeTys = getFTypes fgnArgTys
328 rty = mkIty' ret in
329 case maybeTys of
330 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
331 Just tys -> do
332 args' <- mapM (ir' env) (init args)
333 -- wrap it in a prim__IO
334 -- return $ con_ 0 @@ impossible @@
335 return $ -- LLazyExp $
336 LForeign LANG_C rty fgnName (zip tys args')
337 | otherwise = ifail "Badly formed foreign function call"
339getFTypes :: TT Name -> Maybe [FType]
340getFTypes tm = case unApply tm of
341 (nil, []) -> Just []
342 (cons, [ty, xs]) ->
343 fmap (mkIty' ty :) (getFTypes xs)
344 _ -> Nothing
346mkIty' (P _ (UN ty) _) = mkIty (str ty)
347mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
348 | fi == txt "FIntT" = mkIntIty (str intTy)
349mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
350 | ff == txt "FFunction" && fa == txt "FAny" &&
351 io == txt "IO"
352 = FFunctionIO
353mkIty' (App (App (P _ (UN ff) _) _) _)
354 | ff == txt "FFunction" = FFunction
355mkIty' _ = FAny
357-- would be better if these FInt types were evaluated at compile time
358-- TODO: add %eval directive for such things
360mkIty "FFloat" = FArith ATFloat
361mkIty "FInt" = mkIntIty "ITNative"
362mkIty "FChar" = mkIntIty "ITChar"
363mkIty "FByte" = mkIntIty "IT8"
364mkIty "FShort" = mkIntIty "IT16"
365mkIty "FLong" = mkIntIty "IT64"
366mkIty "FBits8" = mkIntIty "IT8"
367mkIty "FBits16" = mkIntIty "IT16"
368mkIty "FBits32" = mkIntIty "IT32"
369mkIty "FBits64" = mkIntIty "IT64"
370mkIty "FString" = FString
371mkIty "FPtr" = FPtr
372mkIty "FManagedPtr" = FManagedPtr
373mkIty "FUnit" = FUnit
374mkIty "FFunction" = FFunction
375mkIty "FFunctionIO" = FFunctionIO
376mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
377mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
378mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
379mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
380mkIty x = error $ "Unknown type " ++ x
382mkIntIty "ITNative" = FArith (ATInt ITNative)
383mkIntIty "ITChar" = FArith (ATInt ITChar)
384mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
385mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
386mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
387mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
389zname = sNS (sUN "Z") ["Nat","Prelude"]
390sname = sNS (sUN "S") ["Nat","Prelude"]
392instance ToIR ([Name], SC) where
393 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
394 tree' <- ir tree
395 return $ LLam args tree'
397instance ToIR SC where
398 ir t = ir' t where
400 ir' (STerm t) = ir t
401 ir' (UnmatchedCase str) = return $ LError str
402 ir' (ProjCase tm alt) = do tm' <- ir tm
403 alt' <- mkIRAlt tm' alt
404 return $ LCase tm' [alt']
405 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
406 return $ LCase (LV (Glob n)) alts'
407 ir' ImpossibleCase = return LNothing
409 -- special cases for Z and S
410 -- Needs rethink: projections make this fail
411-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
412-- = mkIRAlt n (ConstCase (BI 0) rhs)
413-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
414-- = do n' <- ir n
415-- rhs' <- ir rhs
416-- return $ LDefaultCase
417-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
418-- rhs')
419 mkIRAlt _ (ConCase n t args rhs)
420 = do rhs' <- ir rhs
421 return $ LConCase (-1) n args rhs'
422 mkIRAlt _ (ConstCase x rhs)
423 | matchable x
424 = do rhs' <- ir rhs
425 return $ LConstCase x rhs'
426 | matchableTy x
427 = do rhs' <- ir rhs
428 return $ LDefaultCase rhs'
429 mkIRAlt tm (SucCase n rhs)
430 = do rhs' <- ir rhs
431 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
432 [tm,
433 LConst (BI 1)]) rhs')
434-- return $ LSucCase n rhs'
435 mkIRAlt _ (ConstCase c rhs)
436 = ifail $ "Can't match on (" ++ show c ++ ")"
437 mkIRAlt _ (DefaultCase rhs)
438 = do rhs' <- ir rhs
439 return $ LDefaultCase rhs'
441 matchable (I _) = True
442 matchable (BI _) = True
443 matchable (Ch _) = True
444 matchable (Str _) = True
445 matchable _ = False
447 matchableTy (AType (ATInt ITNative)) = True
448 matchableTy (AType (ATInt ITBig)) = True
449 matchableTy (AType (ATInt ITChar)) = True
450 matchableTy StrType = True
452 matchableTy (AType (ATInt (ITFixed IT8))) = True
453 matchableTy (AType (ATInt (ITFixed IT16))) = True
454 matchableTy (AType (ATInt (ITFixed IT32))) = True
455 matchableTy (AType (ATInt (ITFixed IT64))) = True
457 matchableTy _ = False