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