git.iko.soy/Idris-dev
on bd89fdc help sign in
Idris-dev/src/IRTS/Compiler.hs
295 lines 11 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module IRTS.Compiler where
5import IRTS.Lang
6import IRTS.Defunctionalise
7import IRTS.Simplified
8import IRTS.CodegenC
9import IRTS.CodegenJava
10import IRTS.Inliner
12import Idris.AbsSyntax
13import Idris.UnusedArgs
15import Core.TT
16import Core.Evaluate
17import Core.CaseTree
19import Control.Monad.State
20import Data.List
21import System.Process
22import System.IO
23import System.Directory
24import System.Environment
26import Paths_idris
28compile :: Target -> FilePath -> Term -> Idris ()
29compile target f tm
30 = do checkMVs
31 let tmnames = namesUsed (STerm tm)
32 used <- mapM (allNames []) tmnames
33 defsIn <- mkDecls tm (concat used)
34 findUnusedArgs (concat used)
35 maindef <- irMain tm
36 objs <- getObjectFiles
37 libs <- getLibs
38 hdrs <- getHdrs
39 let defs = defsIn ++ [(MN 0 "runMain", maindef)]
40 -- iputStrLn $ showSep "\n" (map show defs)
41 let (nexttag, tagged) = addTags 65536 (liftAll defs)
42 let ctxtIn = addAlist tagged emptyContext
43 iLOG "Defunctionalising"
44 let defuns_in = defunctionalise nexttag ctxtIn
45 logLvl 5 $ show defuns_in
46 iLOG "Inlining"
47 let defuns = inline defuns_in
48 logLvl 5 $ show defuns
49 iLOG "Resolving variables for CG"
50 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))
51 let checked = checkDefs defuns (toAlist defuns)
52 dumpC <- getDumpC
53 dumpCases <- getDumpCases
54 dumpDefun <- getDumpDefun
55 case dumpCases of
56 Nothing -> return ()
57 Just f -> liftIO $ writeFile f (showCaseTrees tagged)
58 case dumpDefun of
59 Nothing -> return ()
60 Just f -> liftIO $ writeFile f (dumpDefuns defuns)
61 iLOG "Building output"
62 case checked of
63 OK c -> case target of
64 ViaC -> liftIO $ codegenC dumpC c f True hdrs
65 (concatMap mkObj objs)
66 (concatMap mkLib libs) NONE
67 ViaJava -> liftIO $ codegenJava c f
68 Error e -> fail $ show e
69 where checkMVs = do i <- get
70 case idris_metavars i \\ primDefs of
71 [] -> return ()
72 ms -> fail $ "There are undefined metavariables: " ++ show ms
73 inDir d h = do let f = d ++ "/" ++ h
74 ex <- doesFileExist f
75 if ex then return f else return h
76 mkObj f = f ++ " "
77 mkLib l = "-l" ++ l ++ " "
81irMain :: TT Name -> Idris LDecl
82irMain tm = do i <- ir tm
83 return $ LFun (MN 0 "runMain") [] (LForce i)
85allNames :: [Name] -> Name -> Idris [Name]
86allNames ns n | n `elem` ns = return []
87allNames ns n = do i <- get
88 case lookupCtxt Nothing n (idris_callgraph i) of
89 [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
90 return (nub (n : concat more))
91 _ -> return [n]
93mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
94mkDecls t used
95 = do i <- getIState
96 let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
97 mapM traceUnused used
98 decls <- mapM build ds
99 return decls
101showCaseTrees :: [(Name, LDecl)] -> String
102showCaseTrees ds = showSep "\n\n" (map showCT ds)
103 where
104 showCT (n, LFun f args lexp)
105 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t "
106 ++ show lexp
107 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
109isCon (TyDecl _ _) = True
110isCon _ = False
112class ToIR a where
113 ir :: a -> Idris LExp
115build :: (Name, Def) -> Idris (Name, LDecl)
116build (n, d)
117 = do i <- getIState
118 case lookup n (idris_scprims i) of
119 Just (ar, op) ->
120 let args = map (\x -> MN x "op") [0..] in
121 return (n, (LFun n (take ar args)
122 (LOp op (map (LV . Glob) (take ar args)))))
123 _ -> do def <- mkLDecl n d
124 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
125 return (n, def)
127declArgs args n (LLam xs x) = declArgs (args ++ xs) n x
128declArgs args n x = LFun n args x
130mkLDecl n (Function tm _) = do e <- ir tm
131 return (declArgs [] n e)
132mkLDecl n (CaseOp _ _ _ _ pats _ _ args sc) = do e <- ir (args, sc)
133 return (declArgs [] n e)
134mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
135mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
136mkLDecl n _ = return (LFun n [] (LError ("Impossible declaration " ++ show n)))
138instance ToIR (TT Name) where
139 ir tm = ir' [] tm where
140 ir' env tm@(App f a)
141 | (P _ (UN "mkForeign") _, args) <- unApply tm
142 = doForeign env args
143 | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm
144 = ir' env arg
145 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm
146 = do arg' <- ir' env arg
147 return $ LLazyExp arg'
148 | (P _ (UN "par") _, [_, arg]) <- unApply tm
149 = do arg' <- ir' env arg
150 return $ LOp LPar [LLazyExp arg']
151 | (P _ (UN "fork") _, [arg]) <- unApply tm
152 = do arg' <- ir' env arg
153 return $ LOp LFork [LLazyExp arg']
154 | (P _ (UN "prim__IO") _, [v]) <- unApply tm
155 = do v' <- ir' env v
156 return v'
157 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
158 = do v' <- ir' env v
159 k' <- ir' env k
160 return (LApp False k' [LForce v'])
161 | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
162 = do size' <- ir' env size
163 t' <- ir' env t
164 return t' -- TODO $ malloc_ size' t'
165 | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm
166 = do t' <- ir' env t
167 return t' -- TODO
168 | (P (DCon t a) n _, args) <- unApply tm
169 = irCon env t a n args
170 | (P _ n _, args) <- unApply tm
171 = do i <- get
172 let collapse = case lookupCtxt Nothing n (idris_optimisation i) of
173 [oi] -> collapsible oi
174 _ -> False
175 let unused = case lookupCtxt Nothing n (idris_callgraph i) of
176 [CGInfo _ _ _ _ unusedpos] -> unusedpos
177 _ -> []
178 args' <- mapM (ir' env) args
179 if collapse then return LNothing
180 else return (LApp False (LV (Glob n))
181 (mkUnused unused 0 args'))
182 | (f, args) <- unApply tm
183 = do f' <- ir' env f
184 args' <- mapM (ir' env) args
185 return (LApp False f' args')
186 where mkUnused u i [] = []
187 mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
188 | otherwise = x : mkUnused u (i + 1) xs
189 ir' env (P _ n _) = return $ LV (Glob n)
190 ir' env (V i) | i < length env = return $ LV (Glob (env!!i))
191 | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm
192 ir' env (Bind n (Lam _) sc)
193 = do let n' = uniqueName n env
194 sc' <- ir' (n' : env) sc
195 return $ LLam [n'] sc'
196 ir' env (Bind n (Let _ v) sc)
197 = do sc' <- ir' (n : env) sc
198 v' <- ir' env v
199 return $ LLet n v' sc'
200 ir' env (Bind _ _ _) = return $ LNothing
201 ir' env (Proj t i) = do t' <- ir' env t
202 return $ LProj t' i
203 ir' env (Constant c) = return $ LConst c
204 ir' env (Set _) = return $ LNothing
205 ir' env Erased = return $ LNothing
206 ir' env Impossible = return $ LNothing
207-- ir' env _ = return $ LError "Impossible"
209 irCon env t arity n args
210 | length args == arity = buildApp env (LV (Glob n)) args
211 | otherwise = let extra = satArgs (arity - length args) in
212 do sc' <- irCon env t arity n
213 (args ++ map (\n -> P Bound n undefined) extra)
214 return $ LLam extra sc'
216 satArgs n = map (\i -> MN i "sat") [1..n]
218 buildApp env e [] = return e
219 buildApp env e xs = do xs' <- mapM (ir' env) xs
220 return $ LApp False e xs'
222 doForeign :: [Name] -> [TT Name] -> Idris LExp
223 doForeign env (_ : fgn : args)
224 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
225 = let tys = getFTypes fgnArgTys
226 rty = mkIty' ret in
227 do args' <- mapM (ir' env) args
228 -- wrap it in a prim__IO
229 -- return $ con_ 0 @@ impossible @@
230 return $ LLazyExp $
231 LForeign LANG_C rty fgnName (zip tys args')
232 | otherwise = fail "Badly formed foreign function call"
234getFTypes :: TT Name -> [FType]
235getFTypes tm = case unApply tm of
236 (nil, []) -> []
237 (cons, [ty, xs]) ->
238 let rest = getFTypes xs in
239 mkIty' ty : rest
241mkIty' (P _ (UN ty) _) = mkIty ty
242mkIty' _ = FAny
244mkIty "FInt" = FInt
245mkIty "FFloat" = FDouble
246mkIty "FChar" = FChar
247mkIty "FString" = FString
248mkIty "FPtr" = FPtr
249mkIty "FUnit" = FUnit
251instance ToIR ([Name], SC) where
252 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
253 tree' <- ir tree
254 return $ LLam args tree'
256instance ToIR SC where
257 ir t = ir' t where
259 ir' (STerm t) = ir t
260 ir' (UnmatchedCase str) = return $ LError str
261 ir' (ProjCase tm alts) = do alts' <- mapM mkIRAlt alts
262 tm' <- ir tm
263 return $ LCase tm' alts'
264 ir' (Case n alts) = do alts' <- mapM mkIRAlt alts
265 return $ LCase (LV (Glob n)) alts'
266 ir' ImpossibleCase = return LNothing
268 mkIRAlt (ConCase n t args rhs)
269 = do rhs' <- ir rhs
270 return $ LConCase (-1) n args rhs'
271 mkIRAlt (ConstCase x rhs)
272 | matchable x
273 = do rhs' <- ir rhs
274 return $ LConstCase x rhs'
275 | matchableTy x
276 = do rhs' <- ir rhs
277 return $ LDefaultCase rhs'
278 mkIRAlt (ConstCase c rhs)
279 = fail $ "Can't match on (" ++ show c ++ ")"
280 mkIRAlt (DefaultCase rhs)
281 = do rhs' <- ir rhs
282 return $ LDefaultCase rhs'
284 matchable (I _) = True
285 matchable (BI _) = True
286 matchable (Ch _) = True
287 matchable (Str _) = True
288 matchable _ = False
290 matchableTy IType = True
291 matchableTy BIType = True
292 matchableTy ChType = True
293 matchableTy StrType = True
294 matchableTy _ = False