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