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