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