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