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