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