git.iko.soy/Idris-dev
on fc79985 help sign in
Idris-dev/src/IRTS/Compiler.hs
371 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.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 target
42 libs <- getLibs target
43 hdrs <- getHdrs target
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 "assert_smaller") _, [_, _, _, arg]) <- unApply tm
173 = ir' env arg
174 | (P _ (UN "par") _, [_, arg]) <- unApply tm
175 = do arg' <- ir' env arg
176 return $ LOp LPar [LLazyExp arg']
177 | (P _ (UN "fork") _, [arg]) <- unApply tm
178 = do arg' <- ir' env arg
179 return $ LOp LFork [LLazyExp arg']
180 | (P _ (UN "prim__IO") _, [v]) <- unApply tm
181 = do v' <- ir' env v
182 return v'
183 | (P _ (UN "io_bind") _, [_,_,v,Bind n (Lam _) sc]) <- unApply tm
184 = do v' <- ir' env v
185 sc' <- ir' (n:env) sc
186 return (LLet n (LForce v') sc')
187 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
188 = do v' <- ir' env v
189 k' <- ir' env k
190 return (LApp False k' [LForce v'])
191 | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
192 = do size' <- ir' env size
193 t' <- ir' env t
194 return t' -- TODO $ malloc_ size' t'
195 | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm
196 = do t' <- ir' env t
197 return t' -- TODO
198-- | (P _ (NS (UN "S") ["Nat", "Prelude"]) _, [k]) <- unApply tm
199-- = do k' <- ir' env k
200-- return (LOp LBPlus [k', LConst (BI 1)])
201 | (P (DCon t a) n _, args) <- unApply tm
202 = irCon env t a n args
203 | (P _ n _, args) <- unApply tm
204 = do i <- getIState
205 args' <- mapM (ir' env) args
206 case getPrim i n args' of
207 Just tm -> return tm
208 _ -> do
209 let collapse
210 = case lookupCtxt n
211 (idris_optimisation i) of
212 [oi] -> collapsible oi
213 _ -> False
214 let unused
215 = case lookupCtxt n
216 (idris_callgraph i) of
217 [CGInfo _ _ _ _ unusedpos] ->
218 unusedpos
219 _ -> []
220 if collapse
221 then return LNothing
222 else return (LApp False (LV (Glob n))
223 (mkUnused unused 0 args'))
224 | (f, args) <- unApply tm
225 = do f' <- ir' env f
226 args' <- mapM (ir' env) args
227 return (LApp False f' args')
228 where mkUnused u i [] = []
229 mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
230 | otherwise = x : mkUnused u (i + 1) xs
231-- ir' env (P _ (NS (UN "O") ["Nat", "Prelude"]) _)
232-- = return $ LConst (BI 0)
233 ir' env (P _ n _) = return $ LV (Glob n)
234 ir' env (V i) | i >= 0 && i < length env = return $ LV (Glob (env!!i))
235 | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm
236 ir' env (Bind n (Lam _) sc)
237 = do let n' = uniqueName n env
238 sc' <- ir' (n' : env) sc
239 return $ LLam [n'] sc'
240 ir' env (Bind n (Let _ v) sc)
241 = do sc' <- ir' (n : env) sc
242 v' <- ir' env v
243 return $ LLet n v' sc'
244 ir' env (Bind _ _ _) = return $ LNothing
245 ir' env (Proj t i) = do t' <- ir' env t
246 return $ LProj t' i
247 ir' env (Constant c) = return $ LConst c
248 ir' env (TType _) = return $ LNothing
249 ir' env Erased = return $ LNothing
250 ir' env Impossible = return $ LNothing
251-- ir' env _ = return $ LError "Impossible"
253 irCon env t arity n args
254 | length args == arity = buildApp env (LV (Glob n)) args
255 | otherwise = let extra = satArgs (arity - length args) in
256 do sc' <- irCon env t arity n
257 (args ++ map (\n -> P Bound n undefined) extra)
258 return $ LLam extra sc'
260 satArgs n = map (\i -> MN i "sat") [1..n]
262 buildApp env e [] = return e
263 buildApp env e xs = do xs' <- mapM (ir' env) xs
264 return $ LApp False e xs'
266 doForeign :: [Name] -> [TT Name] -> Idris LExp
267 doForeign env (_ : fgn : args)
268 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
269 = let maybeTys = getFTypes fgnArgTys
270 rty = mkIty' ret in
271 case maybeTys of
272 Nothing -> fail $ "Foreign type specification is not a constant list: " ++ show (fgn:args)
273 Just tys -> do
274 args' <- mapM (ir' env) args
275 -- wrap it in a prim__IO
276 -- return $ con_ 0 @@ impossible @@
277 return $ -- LLazyExp $
278 LForeign LANG_C rty fgnName (zip tys args')
279 | otherwise = fail "Badly formed foreign function call"
281getFTypes :: TT Name -> Maybe [FType]
282getFTypes tm = case unApply tm of
283 (nil, []) -> Just []
284 (cons, [ty, xs]) ->
285 fmap (mkIty' ty :) (getFTypes xs)
286 _ -> Nothing
288mkIty' (P _ (UN ty) _) = mkIty ty
289mkIty' (App (P _ (UN "FIntT") _) (P _ (UN intTy) _)) = mkIntIty intTy
290mkIty' (App (App (P _ (UN "FFunction") _) _) (App (P _ (UN "FAny") _) (App (P _ (UN "IO") _) _))) = FFunctionIO
291mkIty' (App (App (P _ (UN "FFunction") _) _) _) = FFunction
292mkIty' _ = FAny
294mkIty "FFloat" = FDouble
295mkIty "FChar" = FChar
296mkIty "FString" = FString
297mkIty "FPtr" = FPtr
298mkIty "FUnit" = FUnit
299mkIty "FFunction" = FFunction
300mkIty "FFunctionIO" = FFunctionIO
302mkIntIty "ITNative" = FInt ITNative
303mkIntIty "IT8" = FInt IT8
304mkIntIty "IT16" = FInt IT16
305mkIntIty "IT32" = FInt IT32
306mkIntIty "IT64" = FInt IT64
308zname = NS (UN "O") ["Nat","Prelude"]
309sname = NS (UN "S") ["Nat","Prelude"]
311instance ToIR ([Name], SC) where
312 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
313 tree' <- ir tree
314 return $ LLam args tree'
316instance ToIR SC where
317 ir t = ir' t where
319 ir' (STerm t) = ir t
320 ir' (UnmatchedCase str) = return $ LError str
321 ir' (ProjCase tm alts) = do alts' <- mapM (mkIRAlt tm) alts
322 tm' <- ir tm
323 return $ LCase tm' alts'
324 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (P Bound n Erased)) alts
325 return $ LCase (LV (Glob n)) alts'
326 ir' ImpossibleCase = return LNothing
328 -- special cases for O and S
329 -- Needs rethink: projections make this fail
330-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
331-- = mkIRAlt n (ConstCase (BI 0) rhs)
332-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
333-- = do n' <- ir n
334-- rhs' <- ir rhs
335-- return $ LDefaultCase
336-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
337-- rhs')
338 mkIRAlt _ (ConCase n t args rhs)
339 = do rhs' <- ir rhs
340 return $ LConCase (-1) n args rhs'
341 mkIRAlt _ (ConstCase x rhs)
342 | matchable x
343 = do rhs' <- ir rhs
344 return $ LConstCase x rhs'
345 | matchableTy x
346 = do rhs' <- ir rhs
347 return $ LDefaultCase rhs'
348 mkIRAlt _ (ConstCase c rhs)
349 = fail $ "Can't match on (" ++ show c ++ ")"
350 mkIRAlt _ (DefaultCase rhs)
351 = do rhs' <- ir rhs
352 return $ LDefaultCase rhs'
354 matchable (I _) = True
355 matchable (BI _) = True
356 matchable (Ch _) = True
357 matchable (Str _) = True
358 matchable _ = False
360 matchableTy IType = True
361 matchableTy BIType = True
362 matchableTy ChType = True
363 matchableTy StrType = True
365 matchableTy B8Type = True
366 matchableTy B16Type = True
367 matchableTy B32Type = True
368 matchableTy B64Type = True
370 matchableTy _ = False