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