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