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