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