git.iko.soy/Idris-dev
on b894841 help sign in
Idris-dev/src/IRTS/Compiler.hs
260 lines 9.8 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 case dumpCases of
55 Nothing -> return ()
56 Just f -> do cs <- getCaseTrees (concat used)
57 liftIO $ writeFile f (showCaseTrees cs)
58 iLOG "Building output"
59 case checked of
60 OK c -> case target of
61 ViaC -> liftIO $ codegenC dumpC c f True hdrs
62 (concatMap mkObj objs)
63 (concatMap mkLib libs) NONE
64 ViaJava -> liftIO $ codegenJava c f
65 Error e -> fail $ show e
66 where checkMVs = do i <- get
67 case idris_metavars i \\ primDefs of
68 [] -> return ()
69 ms -> fail $ "There are undefined metavariables: " ++ show ms
70 inDir d h = do let f = d ++ "/" ++ h
71 ex <- doesFileExist f
72 if ex then return f else return h
73 mkObj f = f ++ " "
74 mkLib l = "-l" ++ l ++ " "
78irMain :: TT Name -> Idris LDecl
79irMain tm = do i <- ir tm
80 return $ LFun (MN 0 "runMain") [] (LForce i)
82allNames :: [Name] -> Name -> Idris [Name]
83allNames ns n | n `elem` ns = return []
84allNames ns n = do i <- get
85 case lookupCtxt Nothing n (idris_callgraph i) of
86 [ns'] -> do more <- mapM (allNames (n:ns)) (map fst (calls ns'))
87 return (nub (n : concat more))
88 _ -> return [n]
90mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
91mkDecls t used
92 = do i <- getIState
93 let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
94 decls <- mapM build ds
95 return decls
97getCaseTrees :: [Name] -> Idris [(Name, Def)]
98getCaseTrees used
99 = do i <- getIState
100 let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
101 return ds
103showCaseTrees :: [(Name, Def)] -> String
104showCaseTrees ds = showSep "\n\n" (map showCT ds)
105 where
106 showCT (n, CaseOp _ _ _ _ _ args sc)
107 = show n ++ " " ++ showSep " " (map show args) ++ " = " ++ show sc
108 showCT (n, _) = ""
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 "fork") _, [arg]) <- unApply tm
150 = do arg' <- ir' env arg
151 return $ LOp LFork [LLazyExp arg']
152 | (P _ (UN "prim__IO") _, [v]) <- unApply tm
153 = do v' <- ir' env v
154 return v'
155 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
156 = do v' <- ir' env v
157 k' <- ir' env k
158 return (LApp False k' [LForce v'])
159 | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
160 = do size' <- ir' env size
161 t' <- ir' env t
162 return t' -- TODO $ malloc_ size' t'
163 | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm
164 = do t' <- ir' env t
165 return t' -- TODO
166 | (P (DCon t a) n _, args) <- unApply tm
167 = irCon env t a n args
168 | (f, args) <- unApply tm
169 = do f' <- ir' env f
170 args' <- mapM (ir' env) args
171 return (LApp False f' args')
172 ir' env (P _ n _) = return $ LV (Glob n)
173 ir' env (V i) | i < length env = return $ LV (Glob (env!!i))
174 | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm
175 ir' env (Bind n (Lam _) sc)
176 = do let n' = uniqueName n env
177 sc' <- ir' (n' : env) sc
178 return $ LLam [n'] sc'
179 ir' env (Bind n (Let _ v) sc)
180 = do sc' <- ir' (n : env) sc
181 v' <- ir' env v
182 return $ LLet n v' sc'
183 ir' env (Bind _ _ _) = return $ LConst (I 424242)
184 ir' env (Proj t i) = do t' <- ir' env t
185 return $ LProj t' i
186 ir' env (Constant c) = return $ LConst c
187 ir' env _ = return $ LError "Impossible"
189 irCon env t arity n args
190 | length args == arity = buildApp env (LV (Glob n)) args
191 | otherwise = let extra = satArgs (arity - length args) in
192 do sc' <- irCon env t arity n
193 (args ++ map (\n -> P Bound n undefined) extra)
194 return $ LLam extra sc'
196 satArgs n = map (\i -> MN i "sat") [1..n]
198 buildApp env e [] = return e
199 buildApp env e xs = do xs' <- mapM (ir' env) xs
200 return $ LApp False e xs'
202 doForeign :: [Name] -> [TT Name] -> Idris LExp
203 doForeign env (_ : fgn : args)
204 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
205 = let tys = getFTypes fgnArgTys
206 rty = mkIty' ret in
207 do args' <- mapM (ir' env) args
208 -- wrap it in a prim__IO
209 -- return $ con_ 0 @@ impossible @@
210 return $ LLazyExp $ LForeign LANG_C rty fgnName (zip tys args')
211 | otherwise = fail "Badly formed foreign function call"
213getFTypes :: TT Name -> [FType]
214getFTypes tm = case unApply tm of
215 (nil, []) -> []
216 (cons, [ty, xs]) ->
217 let rest = getFTypes xs in
218 mkIty' ty : rest
220mkIty' (P _ (UN ty) _) = mkIty ty
221mkIty' _ = FAny
223mkIty "FInt" = FInt
224mkIty "FFloat" = FDouble
225mkIty "FChar" = FChar
226mkIty "FString" = FString
227mkIty "FPtr" = FPtr
228mkIty "FUnit" = FUnit
230instance ToIR ([Name], SC) where
231 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
232 tree' <- ir tree
233 return $ LLam args tree'
235instance ToIR SC where
236 ir t = ir' t where
238 ir' (STerm t) = ir t
239 ir' (UnmatchedCase str) = return $ LError str
240 ir' (ProjCase tm alts) = do alts' <- mapM mkIRAlt alts
241 tm' <- ir tm
242 return $ LCase tm' alts'
243 ir' (Case n alts) = do alts' <- mapM mkIRAlt alts
244 return $ LCase (LV (Glob n)) alts'
246 mkIRAlt (ConCase n t args rhs)
247 = do rhs' <- ir rhs
248 return $ LConCase (-1) n args rhs'
249 mkIRAlt (ConstCase (I i) rhs)
250 = do rhs' <- ir rhs
251 return $ LConstCase (I i) rhs'
252 mkIRAlt (ConstCase IType rhs)
253 = do rhs' <- ir rhs
254 return $ LDefaultCase rhs'
255 mkIRAlt (ConstCase c rhs)
256 = fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"
257 mkIRAlt (DefaultCase rhs)
258 = do rhs' <- ir rhs
259 return $ LDefaultCase rhs'