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