git.iko.soy/Idris-dev
on 73d95bb help sign in
Idris-dev/src/IRTS/Compiler.hs
473 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 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
212 -- This case is here until we get more general inlining. It's just
213 -- a really common case, and the laziness hurts...
214 | (P _ (NS (UN be) [b,p]) _, [_,x,(App (P _ (UN d) _) t),
215 (App (P _ (UN d') _) e)]) <- unApply tm,
216 be == txt "boolElim" && d == txt "Delay" && d' == txt "Delay"
217 = do x' <- ir' env x
218 t' <- ir' env t
219 e' <- ir' env e
220 return (LCase x' [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e',
221 LConCase 1 (sNS (sUN "True") ["Bool","Prelude"]) [] t'])
223 | (P (DCon t a) n _, args) <- unApply tm = do
224 cg <- idris_callgraph <$> getIState
225 case lookupCtxtExact n cg of
226 Just (CGInfo _ _ _ _ usedpos)
227 -> irCon env t a n [if i `elem` map fst usedpos then a else Erased | (i,a) <- zip [0..] args]
228 Nothing -> return LNothing -- no usage info -> not used at all
230 | (P (TCon t a) n _, args) <- unApply tm
231 = return LNothing
233 | (P _ n _, args) <- unApply tm = do
234 ist <- getIState
235 case lookup n (idris_scprims ist) of
236 -- if it's a primitive which is already saturated,
237 -- compile to the corresponding op here already to save work
238 Just (arity, op) | length args == arity
239 -> LOp op <$> mapM (ir' env) args
241 _
242 -- if it's collapsible, compile to LNothing
243 | (collapsible <$> lookupCtxtExact n (idris_optimisation ist)) == Just True
244 -> return LNothing
246 -- otherwise, compile normally
247 | otherwise -> applyName n ist args
249 | (f, args) <- unApply tm
250 = do f' <- ir' env f
251 args' <- mapM (ir' env) args
252 return (LApp False f' args')
254 where
255 applyName :: Name -> IState -> [Term] -> Idris LExp
256 applyName n ist args =
257 LApp False (LV $ Glob n) <$> mapM (ir' env . erase) (zip [0..] args)
258 where
259 erase (i, x)
260 | i >= arity || i `elem` used = x
261 | otherwise = Erased
263 arity = case fst4 <$> lookupCtxt n (definitions . tt_ctxt $ ist) of
264 [CaseOp ci ty tys def tot cdefs] -> length tys
265 [TyDecl (DCon tag ar) _] -> ar
266 [Operator ty ar op] -> ar
267 _ -> 0
269 used = fromMaybe [] (map fst . usedpos <$> lookupCtxtExact n (idris_callgraph ist))
270 fst4 (x,_,_,_) = x
272-- ir' env (P _ (NS (UN "Z") ["Nat", "Prelude"]) _)
273-- = return $ LConst (BI 0)
274 ir' env (P _ n _) = return $ LV (Glob n)
275 ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
276 | otherwise = ifail $ "IR fail " ++ show i ++ " " ++ show tm
277 ir' env (Bind n (Lam _) sc)
278 = do let n' = uniqueName n env
279 sc' <- ir' (n' : env) sc
280 return $ LLam [n'] sc'
281 ir' env (Bind n (Let _ v) sc)
282 = do sc' <- ir' (n : env) sc
283 v' <- ir' env v
284 return $ LLet n v' sc'
285 ir' env (Bind _ _ _) = return $ LNothing
286 ir' env (Proj t i) | i == -1
287 = do t' <- ir' env t
288 return $ LOp (LMinus (ATInt ITBig))
289 [t', LConst (BI 1)]
290 ir' env (Proj t i) = do t' <- ir' env t
291 return $ LProj t' i
292 ir' env (Constant c) = return $ LConst c
293 ir' env (TType _) = return $ LNothing
294 ir' env Erased = return $ LNothing
295 ir' env Impossible = return $ LNothing
296-- ir' env _ = return $ LError "Impossible"
298 irCon env t arity n args
299 | length args == arity = buildApp env (LV (Glob n)) args
300 | otherwise = let extra = satArgs (arity - length args) in
301 do sc' <- irCon env t arity n
302 (args ++ map (\n -> P Bound n undefined) extra)
303 return $ LLam extra sc'
305 satArgs n = map (\i -> sMN i "sat") [1..n]
307 buildApp env e [] = return e
308 buildApp env e xs = do xs' <- mapM (ir' env) xs
309 return $ LApp False e xs'
311 doForeign :: [Name] -> [TT Name] -> Idris LExp
312 doForeign env (_ : fgn : args)
313 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
314 = let maybeTys = getFTypes fgnArgTys
315 rty = mkIty' ret in
316 case maybeTys of
317 Nothing -> ifail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
318 Just tys -> do
319 args' <- mapM (ir' env) (init args)
320 -- wrap it in a prim__IO
321 -- return $ con_ 0 @@ impossible @@
322 return $ -- LLazyExp $
323 LForeign LANG_C rty fgnName (zip tys args')
324 | otherwise = ifail "Badly formed foreign function call"
326getFTypes :: TT Name -> Maybe [FType]
327getFTypes tm = case unApply tm of
328 -- nil : {a : Type} -> List a
329 (nil, [_]) -> Just []
330 -- cons : {a : Type} -> a -> List a -> List a
331 (cons, [_, ty, xs]) -> (mkIty' ty :) <$> getFTypes xs
332 _ -> Nothing
334mkIty' (P _ (UN ty) _) = mkIty (str ty)
335mkIty' (App (P _ (UN fi) _) (P _ (UN intTy) _))
336 | fi == txt "FIntT" = mkIntIty (str intTy)
337mkIty' (App (App (P _ (UN ff) _) _) (App (P _ (UN fa) _) (App (P _ (UN io) _) _)))
338 | ff == txt "FFunction" && fa == txt "FAny" &&
339 io == txt "IO"
340 = FFunctionIO
341mkIty' (App (App (P _ (UN ff) _) _) _)
342 | ff == txt "FFunction" = FFunction
343mkIty' _ = FAny
345-- would be better if these FInt types were evaluated at compile time
346-- TODO: add %eval directive for such things
348mkIty "FFloat" = FArith ATFloat
349mkIty "FInt" = mkIntIty "ITNative"
350mkIty "FChar" = mkIntIty "ITChar"
351mkIty "FByte" = mkIntIty "IT8"
352mkIty "FShort" = mkIntIty "IT16"
353mkIty "FLong" = mkIntIty "IT64"
354mkIty "FBits8" = mkIntIty "IT8"
355mkIty "FBits16" = mkIntIty "IT16"
356mkIty "FBits32" = mkIntIty "IT32"
357mkIty "FBits64" = mkIntIty "IT64"
358mkIty "FString" = FString
359mkIty "FPtr" = FPtr
360mkIty "FManagedPtr" = FManagedPtr
361mkIty "FUnit" = FUnit
362mkIty "FFunction" = FFunction
363mkIty "FFunctionIO" = FFunctionIO
364mkIty "FBits8x16" = FArith (ATInt (ITVec IT8 16))
365mkIty "FBits16x8" = FArith (ATInt (ITVec IT16 8))
366mkIty "FBits32x4" = FArith (ATInt (ITVec IT32 4))
367mkIty "FBits64x2" = FArith (ATInt (ITVec IT64 2))
368mkIty x = error $ "Unknown type " ++ x
370mkIntIty "ITNative" = FArith (ATInt ITNative)
371mkIntIty "ITChar" = FArith (ATInt ITChar)
372mkIntIty "IT8" = FArith (ATInt (ITFixed IT8))
373mkIntIty "IT16" = FArith (ATInt (ITFixed IT16))
374mkIntIty "IT32" = FArith (ATInt (ITFixed IT32))
375mkIntIty "IT64" = FArith (ATInt (ITFixed IT64))
377zname = sNS (sUN "Z") ["Nat","Prelude"]
378sname = sNS (sUN "S") ["Nat","Prelude"]
380instance ToIR ([Name], SC) where
381 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
382 tree' <- ir tree
383 return $ LLam args tree'
385instance ToIR SC where
386 ir t = ir' t where
388 ir' (STerm t) = ir t
389 ir' (UnmatchedCase str) = return $ LError str
390 ir' (ProjCase tm alt) = do tm' <- ir tm
391 alt' <- mkIRAlt tm' alt
392 return $ LCase tm' [alt']
394 -- This is important for runtime because sometimes we case on irrelevant data:
395 --
396 -- case {foo} of
397 -- SingleConstructor x y => ... x, y never used ...
398 --
399 -- In the example above, {foo} will most probably have been erased
400 -- so this vain projection would make the resulting program segfault.
401 --
402 -- Hence, we check whether the variables are used at all
403 -- and erase the casesplit if they are not.
404 ir' (Case n [alt]) = do
405 alt' <- mkIRAlt (LV (Glob n)) alt
406 return $ case namesBoundIn alt' `usedIn` subexpr alt' of
407 [] -> subexpr alt' -- strip the unused top-most case
408 _ -> LCase (LV (Glob n)) [alt']
409 where
410 namesBoundIn :: LAlt -> [Name]
411 namesBoundIn (LConCase cn i ns sc) = ns
412 namesBoundIn (LConstCase c sc) = []
413 namesBoundIn (LDefaultCase sc) = []
415 subexpr :: LAlt -> LExp
416 subexpr (LConCase _ _ _ e) = e
417 subexpr (LConstCase _ e) = e
418 subexpr (LDefaultCase e) = e
420 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
421 return $ LCase (LV (Glob n)) alts'
422 ir' ImpossibleCase = return LNothing
424 -- special cases for Z and S
425 -- Needs rethink: projections make this fail
426-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
427-- = mkIRAlt n (ConstCase (BI 0) rhs)
428-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
429-- = do n' <- ir n
430-- rhs' <- ir rhs
431-- return $ LDefaultCase
432-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
433-- rhs')
434 mkIRAlt _ (ConCase n t args rhs)
435 = do rhs' <- ir rhs
436 return $ LConCase (-1) n args rhs'
437 mkIRAlt _ (ConstCase x rhs)
438 | matchable x
439 = do rhs' <- ir rhs
440 return $ LConstCase x rhs'
441 | matchableTy x
442 = do rhs' <- ir rhs
443 return $ LDefaultCase rhs'
444 mkIRAlt tm (SucCase n rhs)
445 = do rhs' <- ir rhs
446 return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
447 [tm,
448 LConst (BI 1)]) rhs')
449-- return $ LSucCase n rhs'
450 mkIRAlt _ (ConstCase c rhs)
451 = ifail $ "Can't match on (" ++ show c ++ ")"
452 mkIRAlt _ (DefaultCase rhs)
453 = do rhs' <- ir rhs
454 return $ LDefaultCase rhs'
456 matchable (I _) = True
457 matchable (BI _) = True
458 matchable (Ch _) = True
459 matchable (Str _) = True
460 matchable _ = False
462 matchableTy (AType (ATInt ITNative)) = True
463 matchableTy (AType (ATInt ITBig)) = True
464 matchableTy (AType (ATInt ITChar)) = True
465 matchableTy StrType = True
467 matchableTy (AType (ATInt (ITFixed IT8))) = True
468 matchableTy (AType (ATInt (ITFixed IT16))) = True
469 matchableTy (AType (ATInt (ITFixed IT32))) = True
470 matchableTy (AType (ATInt (ITFixed IT64))) = True
472 matchableTy _ = False