on bb76c6c help sign in
Idris-dev/src/IRTS/Compiler.hs
232 lines 8.6 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 Core.TT
14import Core.Evaluate
15import Core.CaseTree
17import Control.Monad.State
18import Data.List
19import System.Process
20import System.IO
21import System.Directory
22import System.Environment
24import Paths_idris
26compile :: Target -> FilePath -> Term -> Idris ()
27compile target f tm
28 = do checkMVs
29 let tmnames = namesUsed (STerm tm)
30 used <- mapM (allNames []) tmnames
31 defsIn <- mkDecls tm (concat used)
32 maindef <- irMain tm
33 objs <- getObjectFiles
34 libs <- getLibs
35 hdrs <- getHdrs
36 let defs = defsIn ++ [(MN 0 "runMain", maindef)]
37 -- iputStrLn $ showSep "\n" (map show defs)
38 let (nexttag, tagged) = addTags 65536 (liftAll defs)
39 let ctxtIn = addAlist tagged emptyContext
40 iLOG "Defunctionalising"
41 let defuns_in = defunctionalise nexttag ctxtIn
42 logLvl 5 $ show defuns_in
43 iLOG "Inlining"
44 let defuns = inline defuns_in
45 logLvl 5 $ show defuns
47 -- iputStrLn $ showSep "\n" (map show (toAlist defuns))
48 let checked = checkDefs defuns (toAlist defuns)
49 case checked of
50 OK c -> case target of
51 ViaC -> liftIO $ codegenC c f True hdrs
52 (concatMap mkObj objs)
53 (concatMap mkLib libs) NONE
54 ViaJava -> liftIO $ codegenJava c f
55 Error e -> fail $ show e
56 where checkMVs = do i <- get
57 case idris_metavars i \\ primDefs of
58 [] -> return ()
59 ms -> fail $ "There are undefined metavariables: " ++ show ms
60 inDir d h = do let f = d ++ "/" ++ h
61 ex <- doesFileExist f
62 if ex then return f else return h
63 mkObj f = f ++ " "
64 mkLib l = "-l" ++ l ++ " "
66irMain :: TT Name -> Idris LDecl
67irMain tm = do i <- ir tm
68 return $ LFun (MN 0 "runMain") [] (LForce i)
70allNames :: [Name] -> Name -> Idris [Name]
71allNames ns n | n `elem` ns = return []
72allNames ns n = do i <- get
73 case lookupCtxt Nothing n (idris_callgraph i) of
74 [ns'] -> do more <- mapM (allNames (n:ns)) ns'
75 return (nub (n : concat more))
76 _ -> return [n]
78mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
79mkDecls t used
80 = do i <- getIState
81 let ds = filter (\ (n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)
82 decls <- mapM build ds
83 return decls
85isCon (TyDecl _ _) = True
86isCon _ = False
88class ToIR a where
89 ir :: a -> Idris LExp
91build :: (Name, Def) -> Idris (Name, LDecl)
92build (n, d)
93 = do i <- getIState
94 case lookup n (idris_scprims i) of
95 Just (ar, op) ->
96 let args = map (\x -> MN x "op") [0..] in
97 return (n, (LFun n (take ar args)
98 (LOp op (map (LV . Glob) (take ar args)))))
99 _ -> do def <- mkLDecl n d
100 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
101 return (n, def)
103declArgs args n (LLam xs x) = declArgs (args ++ xs) n x
104declArgs args n x = LFun n args x
106mkLDecl n (Function tm _) = do e <- ir tm
107 return (declArgs [] n e)
108mkLDecl n (CaseOp _ _ pats _ _ args sc) = do e <- ir (args, sc)
109 return (declArgs [] n e)
110mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n t a
111mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
112mkLDecl n _ = return (LFun n [] (LError ("Impossible declaration " ++ show n)))
114instance ToIR (TT Name) where
115 ir tm = ir' [] tm where
116 ir' env tm@(App f a)
117 | (P _ (UN "mkForeign") _, args) <- unApply tm
118 = doForeign env args
119 | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm
120 = ir' env arg
121 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm
122 = do arg' <- ir' env arg
123 return $ LLazyExp arg'
124 | (P _ (UN "fork") _, [arg]) <- unApply tm
125 = do arg' <- ir' env arg
126 return $ LOp LFork [LLazyExp arg']
127 | (P _ (UN "prim__IO") _, [v]) <- unApply tm
128 = do v' <- ir' env v
129 return v'
130 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
131 = do v' <- ir' env v
132 k' <- ir' env k
133 return (LApp False k' [LForce v'])
134 | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
135 = do size' <- ir' env size
136 t' <- ir' env t
137 return t' -- TODO $ malloc_ size' t'
138 | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm
139 = do t' <- ir' env t
140 return t' -- TODO
141 | (P (DCon t a) n _, args) <- unApply tm
142 = irCon env t a n args
143 | (f, args) <- unApply tm
144 = do f' <- ir' env f
145 args' <- mapM (ir' env) args
146 return (LApp False f' args')
147 ir' env (P _ n _) = return $ LV (Glob n)
148 ir' env (V i) | i < length env = return $ LV (Glob (env!!i))
149 | otherwise = error $ "IR fail " ++ show i ++ " " ++ show tm
150 ir' env (Bind n (Lam _) sc)
151 = do let n' = uniqueName n env
152 sc' <- ir' (n' : env) sc
153 return $ LLam [n'] sc'
154 ir' env (Bind n (Let _ v) sc)
155 = do sc' <- ir' (n : env) sc
156 v' <- ir' env v
157 return $ LLet n v' sc'
158 ir' env (Bind _ _ _) = return $ LConst (I 424242)
159 ir' env (Constant c) = return $ LConst c
160 ir' env _ = return $ LError "Impossible"
162 irCon env t arity n args
163 | length args == arity = buildApp env (LV (Glob n)) args
164 | otherwise = let extra = satArgs (arity - length args) in
165 do sc' <- irCon env t arity n
166 (args ++ map (\n -> P Bound n undefined) extra)
167 return $ LLam extra sc'
169 satArgs n = map (\i -> MN i "sat") [1..n]
171 buildApp env e [] = return e
172 buildApp env e xs = do xs' <- mapM (ir' env) xs
173 return $ LApp False e xs'
175 doForeign :: [Name] -> [TT Name] -> Idris LExp
176 doForeign env (_ : fgn : args)
177 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
178 = let tys = getFTypes fgnArgTys
179 rty = mkIty' ret in
180 do args' <- mapM (ir' env) args
181 -- wrap it in a prim__IO
182 -- return $ con_ 0 @@ impossible @@
183 return $ LLazyExp $ LForeign LANG_C rty fgnName (zip tys args')
184 | otherwise = fail "Badly formed foreign function call"
186getFTypes :: TT Name -> [FType]
187getFTypes tm = case unApply tm of
188 (nil, []) -> []
189 (cons, [ty, xs]) ->
190 let rest = getFTypes xs in
191 mkIty' ty : rest
193mkIty' (P _ (UN ty) _) = mkIty ty
194mkIty' _ = FAny
196mkIty "FInt" = FInt
197mkIty "FFloat" = FDouble
198mkIty "FChar" = FChar
199mkIty "FString" = FString
200mkIty "FPtr" = FPtr
201mkIty "FUnit" = FUnit
203instance ToIR ([Name], SC) where
204 ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
205 tree' <- ir tree
206 return $ LLam args tree'
208instance ToIR SC where
209 ir (STerm t) = ir t
210 ir (UnmatchedCase str) = return $ LError str
211 ir (Case n alts) = do alts' <- mapM mkIRAlt alts
212 return $ LCase (LV (Glob n)) alts'
213 where
214 mkIRAlt (ConCase n t args rhs)
215 = do rhs' <- ir rhs
216 return $ LConCase (-1) n args rhs'
217 mkIRAlt (ConstCase (I i) rhs)
218 = do rhs' <- ir rhs
219 return $ LConstCase (I i) rhs'
220 mkIRAlt (ConstCase IType rhs)
221 = do rhs' <- ir rhs
222 return $ LDefaultCase rhs'
223 mkIRAlt (ConstCase c rhs)
224 = fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"
225 mkIRAlt (DefaultCase rhs)
226 = do rhs' <- ir rhs
227 return $ LDefaultCase rhs'