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