git.iko.soy/Idris-dev
on 73ec76f help sign in
Idris-dev/src/IRTS/Compiler.hs
348 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 -> case target of
69 ViaC -> liftIO $ codegenC c f outty hdrs
70 (concatMap mkObj objs)
71 (concatMap mkLib libs) NONE
72 ViaJava -> liftIO $ codegenJava c f outty
73 Bytecode -> liftIO $ dumpBC c f
74 ToJavaScript -> liftIO $ codegenJavaScript c f outty
75 Error e -> fail $ show e
76 where checkMVs = do i <- get
77 case idris_metavars i \\ primDefs of
78 [] -> return ()
79 ms -> fail $ "There are undefined metavariables: " ++ show ms
80 inDir d h = do let f = d </> h
81 ex <- doesFileExist f
82 if ex then return f else return h
83 mkObj f = f ++ " "
84 mkLib l = "-l" ++ l ++ " "
88irMain :: TT Name -> Idris LDecl
89irMain tm = do i <- ir tm
90 return $ LFun [] (MN 0 "runMain") [] (LForce i)
92allNames :: [Name] -> Name -> Idris [Name]
93allNames ns n | n `elem` ns = return []
94allNames ns n = do i <- get
95 case lookupCtxt Nothing n (idris_callgraph i) of
96 [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
97 return (nub (n : concat more))
98 _ -> return [n]
100mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
101mkDecls t used
102 = do i <- getIState
103 let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
104 mapM traceUnused used
105 decls <- mapM build ds
106 return decls
108showCaseTrees :: [(Name, LDecl)] -> String
109showCaseTrees ds = showSep "\n\n" (map showCT ds)
110 where
111 showCT (n, LFun _ f args lexp)
112 = show n ++ " " ++ showSep " " (map show args) ++ " =\n\t "
113 ++ show lexp
114 showCT (n, LConstructor c t a) = "data " ++ show n ++ " " ++ show a
116isCon (TyDecl _ _) = True
117isCon _ = False
119class ToIR a where
120 ir :: a -> Idris LExp
122build :: (Name, Def) -> Idris (Name, LDecl)
123build (n, d)
124 = do i <- getIState
125 case lookup n (idris_scprims i) of
126 Just (ar, op) ->
127 let args = map (\x -> MN x "op") [0..] in
128 return (n, (LFun [] n (take ar args)
129 (LOp op (map (LV . Glob) (take ar args)))))
130 _ -> do def <- mkLDecl n d
131 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
132 return (n, def)
134getPrim :: IState -> Name -> [LExp] -> Maybe LExp
135getPrim i n args = case lookup n (idris_scprims i) of
136 Just (ar, op) ->
137 if (ar == length args)
138 then return (LOp op args)
139 else Nothing
140 _ -> Nothing
142declArgs args inl n (LLam xs x) = declArgs (args ++ xs) inl n x
143declArgs args inl n x = LFun (if inl then [Inline] else []) n args x
145mkLDecl n (Function tm _) = do e <- ir tm
146 return (declArgs [] True n e)
147mkLDecl n (CaseOp _ inl _ _ pats _ _ args sc) = do e <- ir (args, sc)
148 return (declArgs [] inl n e)
149mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
150mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
151mkLDecl n _ = return (LFun [] n [] (LError ("Impossible declaration " ++ show n)))
153instance ToIR (TT Name) where
154 ir tm = ir' [] tm where
155 ir' env tm@(App f a)
156 | (P _ (UN "mkForeign") _, args) <- unApply tm
157 = doForeign env args
158 | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm
159 = ir' env arg
160 -- TMP HACK - until we get inlining.
161 | (P _ (UN "replace") _, [_, _, _, _, _, arg]) <- unApply tm
162 = ir' env arg
163 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm
164 = do arg' <- ir' env arg
165 return $ LLazyExp arg'
166 | (P _ (UN "par") _, [_, arg]) <- unApply tm
167 = do arg' <- ir' env arg
168 return $ LOp LPar [LLazyExp arg']
169 | (P _ (UN "fork") _, [arg]) <- unApply tm
170 = do arg' <- ir' env arg
171 return $ LOp LFork [LLazyExp arg']
172 | (P _ (UN "prim__IO") _, [v]) <- unApply tm
173 = do v' <- ir' env v
174 return v'
175 | (P _ (UN "io_bind") _, [_,_,v,Bind n (Lam _) sc]) <- unApply tm
176 = do v' <- ir' env v
177 sc' <- ir' (n:env) sc
178 return (LLet n (LForce v') sc')
179 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
180 = do v' <- ir' env v
181 k' <- ir' env k
182 return (LApp False k' [LForce v'])
183 | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
184 = do size' <- ir' env size
185 t' <- ir' env t
186 return t' -- TODO $ malloc_ size' t'
187 | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm
188 = do t' <- ir' env t
189 return t' -- TODO
190-- | (P _ (NS (UN "S") ["Nat", "Prelude"]) _, [k]) <- unApply tm
191-- = do k' <- ir' env k
192-- return (LOp LBPlus [k', LConst (BI 1)])
193 | (P (DCon t a) n _, args) <- unApply tm
194 = irCon env t a n args
195 | (P _ n _, args) <- unApply tm
196 = do i <- get
197 args' <- mapM (ir' env) args
198 case getPrim i n args' of
199 Just tm -> return tm
200 _ -> do
201 let collapse
202 = case lookupCtxt Nothing n
203 (idris_optimisation i) of
204 [oi] -> collapsible oi
205 _ -> False
206 let unused
207 = case lookupCtxt Nothing n
208 (idris_callgraph i) of
209 [CGInfo _ _ _ _ unusedpos] ->
210 unusedpos
211 _ -> []
212 if collapse
213 then return LNothing
214 else return (LApp False (LV (Glob n))
215 (mkUnused unused 0 args'))
216 | (f, args) <- unApply tm
217 = do f' <- ir' env f
218 args' <- mapM (ir' env) args
219 return (LApp False f' args')
220 where mkUnused u i [] = []
221 mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
222 | otherwise = x : mkUnused u (i + 1) xs
223-- ir' env (P _ (NS (UN "O") ["Nat", "Prelude"]) _)
224-- = return $ LConst (BI 0)
225 ir' env (P _ n _) = return $ LV (Glob n)
226 ir' env (V i) | i < length env = return $ LV (Glob (env!!i))
227 | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm
228 ir' env (Bind n (Lam _) sc)
229 = do let n' = uniqueName n env
230 sc' <- ir' (n' : env) sc
231 return $ LLam [n'] sc'
232 ir' env (Bind n (Let _ v) sc)
233 = do sc' <- ir' (n : env) sc
234 v' <- ir' env v
235 return $ LLet n v' sc'
236 ir' env (Bind _ _ _) = return $ LNothing
237 ir' env (Proj t i) = do t' <- ir' env t
238 return $ LProj t' i
239 ir' env (Constant c) = return $ LConst c
240 ir' env (TType _) = return $ LNothing
241 ir' env Erased = return $ LNothing
242 ir' env Impossible = return $ LNothing
243-- ir' env _ = return $ LError "Impossible"
245 irCon env t arity n args
246 | length args == arity = buildApp env (LV (Glob n)) args
247 | otherwise = let extra = satArgs (arity - length args) in
248 do sc' <- irCon env t arity n
249 (args ++ map (\n -> P Bound n undefined) extra)
250 return $ LLam extra sc'
252 satArgs n = map (\i -> MN i "sat") [1..n]
254 buildApp env e [] = return e
255 buildApp env e xs = do xs' <- mapM (ir' env) xs
256 return $ LApp False e xs'
258 doForeign :: [Name] -> [TT Name] -> Idris LExp
259 doForeign env (_ : fgn : args)
260 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
261 = let tys = getFTypes fgnArgTys
262 rty = mkIty' ret in
263 do args' <- mapM (ir' env) args
264 -- wrap it in a prim__IO
265 -- return $ con_ 0 @@ impossible @@
266 return $ -- LLazyExp $
267 LForeign LANG_C rty fgnName (zip tys args')
268 | otherwise = fail "Badly formed foreign function call"
270getFTypes :: TT Name -> [FType]
271getFTypes tm = case unApply tm of
272 (nil, []) -> []
273 (cons, [ty, xs]) ->
274 let rest = getFTypes xs in
275 mkIty' ty : rest
277mkIty' (P _ (UN ty) _) = mkIty ty
278mkIty' _ = FAny
280mkIty "FInt" = FInt
281mkIty "FFloat" = FDouble
282mkIty "FChar" = FChar
283mkIty "FString" = FString
284mkIty "FPtr" = FPtr
285mkIty "FUnit" = FUnit
287zname = NS (UN "O") ["Nat","Prelude"]
288sname = NS (UN "S") ["Nat","Prelude"]
290instance ToIR ([Name], SC) where
291 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
292 tree' <- ir tree
293 return $ LLam args tree'
295instance ToIR SC where
296 ir t = ir' t where
298 ir' (STerm t) = ir t
299 ir' (UnmatchedCase str) = return $ LError str
300 ir' (ProjCase tm alts) = do alts' <- mapM (mkIRAlt tm) alts
301 tm' <- ir tm
302 return $ LCase tm' alts'
303 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (P Bound n Erased)) alts
304 return $ LCase (LV (Glob n)) alts'
305 ir' ImpossibleCase = return LNothing
307 -- special cases for O and S
308 -- Needs rethink: projections make this fail
309-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
310-- = mkIRAlt n (ConstCase (BI 0) rhs)
311-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
312-- = do n' <- ir n
313-- rhs' <- ir rhs
314-- return $ LDefaultCase
315-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
316-- rhs')
317 mkIRAlt _ (ConCase n t args rhs)
318 = do rhs' <- ir rhs
319 return $ LConCase (-1) n args rhs'
320 mkIRAlt _ (ConstCase x rhs)
321 | matchable x
322 = do rhs' <- ir rhs
323 return $ LConstCase x rhs'
324 | matchableTy x
325 = do rhs' <- ir rhs
326 return $ LDefaultCase rhs'
327 mkIRAlt _ (ConstCase c rhs)
328 = fail $ "Can't match on (" ++ show c ++ ")"
329 mkIRAlt _ (DefaultCase rhs)
330 = do rhs' <- ir rhs
331 return $ LDefaultCase rhs'
333 matchable (I _) = True
334 matchable (BI _) = True
335 matchable (Ch _) = True
336 matchable (Str _) = True
337 matchable _ = False
339 matchableTy IType = True
340 matchableTy BIType = True
341 matchableTy ChType = True
342 matchableTy StrType = True
344 matchableTy W8Type = True
345 matchableTy W16Type = True
347 matchableTy _ = False