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