git.iko.soy/Idris-dev
on 77e407e help sign in
Idris-dev/src/IRTS/Compiler.hs
318 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 -- TMP HACK - until we get inlining.
148 | (P _ (UN "replace") _, [_, _, _, _, _, arg]) <- unApply tm
149 = ir' env arg
150 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm
151 = do arg' <- ir' env arg
152 return $ LLazyExp arg'
153 | (P _ (UN "par") _, [_, arg]) <- unApply tm
154 = do arg' <- ir' env arg
155 return $ LOp LPar [LLazyExp arg']
156 | (P _ (UN "fork") _, [arg]) <- unApply tm
157 = do arg' <- ir' env arg
158 return $ LOp LFork [LLazyExp arg']
159 | (P _ (UN "prim__IO") _, [v]) <- unApply tm
160 = do v' <- ir' env v
161 return v'
162 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
163 = do v' <- ir' env v
164 k' <- ir' env k
165 return (LApp False k' [LForce v'])
166 | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
167 = do size' <- ir' env size
168 t' <- ir' env t
169 return t' -- TODO $ malloc_ size' t'
170 | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm
171 = do t' <- ir' env t
172 return t' -- TODO
173-- | (P _ (NS (UN "S") ["Nat", "Prelude"]) _, [k]) <- unApply tm
174-- = do k' <- ir' env k
175-- return (LOp LBPlus [k', LConst (BI 1)])
176 | (P (DCon t a) n _, args) <- unApply tm
177 = irCon env t a n args
178 | (P _ n _, args) <- unApply tm
179 = do i <- get
180 let collapse = case lookupCtxt Nothing n (idris_optimisation i) of
181 [oi] -> collapsible oi
182 _ -> False
183 let unused = case lookupCtxt Nothing n (idris_callgraph i) of
184 [CGInfo _ _ _ _ unusedpos] -> unusedpos
185 _ -> []
186 args' <- mapM (ir' env) args
187 if collapse then return LNothing
188 else return (LApp False (LV (Glob n))
189 (mkUnused unused 0 args'))
190 | (f, args) <- unApply tm
191 = do f' <- ir' env f
192 args' <- mapM (ir' env) args
193 return (LApp False f' args')
194 where mkUnused u i [] = []
195 mkUnused u i (x : xs) | i `elem` u = LNothing : mkUnused u (i + 1) xs
196 | otherwise = x : mkUnused u (i + 1) xs
197-- ir' env (P _ (NS (UN "O") ["Nat", "Prelude"]) _)
198-- = return $ LConst (BI 0)
199 ir' env (P _ n _) = return $ LV (Glob n)
200 ir' env (V i) | i < length env = return $ LV (Glob (env!!i))
201 | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm
202 ir' env (Bind n (Lam _) sc)
203 = do let n' = uniqueName n env
204 sc' <- ir' (n' : env) sc
205 return $ LLam [n'] sc'
206 ir' env (Bind n (Let _ v) sc)
207 = do sc' <- ir' (n : env) sc
208 v' <- ir' env v
209 return $ LLet n v' sc'
210 ir' env (Bind _ _ _) = return $ LNothing
211 ir' env (Proj t i) = do t' <- ir' env t
212 return $ LProj t' i
213 ir' env (Constant c) = return $ LConst c
214 ir' env (Set _) = return $ LNothing
215 ir' env Erased = return $ LNothing
216 ir' env Impossible = return $ LNothing
217-- ir' env _ = return $ LError "Impossible"
219 irCon env t arity n args
220 | length args == arity = buildApp env (LV (Glob n)) args
221 | otherwise = let extra = satArgs (arity - length args) in
222 do sc' <- irCon env t arity n
223 (args ++ map (\n -> P Bound n undefined) extra)
224 return $ LLam extra sc'
226 satArgs n = map (\i -> MN i "sat") [1..n]
228 buildApp env e [] = return e
229 buildApp env e xs = do xs' <- mapM (ir' env) xs
230 return $ LApp False e xs'
232 doForeign :: [Name] -> [TT Name] -> Idris LExp
233 doForeign env (_ : fgn : args)
234 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
235 = let tys = getFTypes fgnArgTys
236 rty = mkIty' ret in
237 do args' <- mapM (ir' env) args
238 -- wrap it in a prim__IO
239 -- return $ con_ 0 @@ impossible @@
240 return $ LLazyExp $
241 LForeign LANG_C rty fgnName (zip tys args')
242 | otherwise = fail "Badly formed foreign function call"
244getFTypes :: TT Name -> [FType]
245getFTypes tm = case unApply tm of
246 (nil, []) -> []
247 (cons, [ty, xs]) ->
248 let rest = getFTypes xs in
249 mkIty' ty : rest
251mkIty' (P _ (UN ty) _) = mkIty ty
252mkIty' _ = FAny
254mkIty "FInt" = FInt
255mkIty "FFloat" = FDouble
256mkIty "FChar" = FChar
257mkIty "FString" = FString
258mkIty "FPtr" = FPtr
259mkIty "FUnit" = FUnit
261zname = NS (UN "O") ["Nat","Prelude"]
262sname = NS (UN "S") ["Nat","Prelude"]
264instance ToIR ([Name], SC) where
265 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
266 tree' <- ir tree
267 return $ LLam args tree'
269instance ToIR SC where
270 ir t = ir' t where
272 ir' (STerm t) = ir t
273 ir' (UnmatchedCase str) = return $ LError str
274 ir' (ProjCase tm alts) = do alts' <- mapM (mkIRAlt tm) alts
275 tm' <- ir tm
276 return $ LCase tm' alts'
277 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (P Bound n Erased)) alts
278 return $ LCase (LV (Glob n)) alts'
279 ir' ImpossibleCase = return LNothing
281 -- special cases for O and S
282 -- Needs rethink: projections make this fail
283-- mkIRAlt n (ConCase z _ [] rhs) | z == zname
284-- = mkIRAlt n (ConstCase (BI 0) rhs)
285-- mkIRAlt n (ConCase s _ [arg] rhs) | s == sname
286-- = do n' <- ir n
287-- rhs' <- ir rhs
288-- return $ LDefaultCase
289-- (LLet arg (LOp LBMinus [n', LConst (BI 1)])
290-- rhs')
291 mkIRAlt _ (ConCase n t args rhs)
292 = do rhs' <- ir rhs
293 return $ LConCase (-1) n args rhs'
294 mkIRAlt _ (ConstCase x rhs)
295 | matchable x
296 = do rhs' <- ir rhs
297 return $ LConstCase x rhs'
298 | matchableTy x
299 = do rhs' <- ir rhs
300 return $ LDefaultCase rhs'
301 mkIRAlt _ (ConstCase c rhs)
302 = fail $ "Can't match on (" ++ show c ++ ")"
303 mkIRAlt _ (DefaultCase rhs)
304 = do rhs' <- ir rhs
305 return $ LDefaultCase rhs'
307 matchable (I _) = True
308 matchable (BI _) = True
309 matchable (Ch _) = True
310 matchable (Str _) = True
311 matchable _ = False
313 matchableTy IType = True
314 matchableTy BIType = True
315 matchableTy ChType = True
316 matchableTy StrType = True
317 matchableTy _ = False