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