git.iko.soy/Idris-dev
on a391979 help sign in
Idris-dev/src/Idris/Compiler.hs
227 lines 8.6 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Compiler where
5import Idris.AbsSyntax
6import Idris.Transforms
8import Core.TT
9import Core.Evaluate
10import Core.CaseTree
12import Control.Monad.State
13import Data.List
14import System.Process
15import System.IO
16import System.Directory
17import System.Environment
19import Epic.Epic hiding (Term, Type, Name, fn, compile)
20import qualified Epic.Epic as E
22primDefs = [UN "mkForeign", UN "FalseElim"]
24compile :: FilePath -> Term -> Idris ()
25compile f tm
26 = do checkMVs
27 let tmnames = namesUsed (STerm tm)
28 used <- mapM (allNames []) tmnames
29 ds <- mkDecls tm (concat used)
30 objs <- getObjectFiles
31 libs <- getLibs
32 hdrs <- getHdrs
33 let incs = map Include hdrs
34 so <- getSO
35 case so of
36 Nothing ->
37 do m <- epicMain tm
38 let mainval = EpicFn (name "main") m
39 liftIO $ compileObjWith []
40 (mkProgram (incs ++ mainval : ds)) (f ++ ".o")
41 liftIO $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f
42 where checkMVs = do i <- get
43 case idris_metavars i \\ primDefs of
44 [] -> return ()
45 ms -> fail $ "There are undefined metavariables: " ++ show ms
47allNames :: [Name] -> Name -> Idris [Name]
48allNames ns n | n `elem` ns = return []
49allNames ns n = do i <- get
50 case lookupCtxt Nothing n (idris_callgraph i) of
51 [ns'] -> do more <- mapM (allNames (n:ns)) ns'
52 return (nub (n : concat more))
53 _ -> return [n]
55mkDecls :: Term -> [Name] -> Idris [EpicDecl]
56mkDecls t used
57 = do i <- getIState
58 let ds = filter (\ (n, d) -> n `elem` used) $ ctxtAlist (tt_ctxt i)
59 decls <- mapM build ds
60 return $ basic_defs ++ decls
62-- EpicFn (name "main") epicMain : decls
64ename x = name ("idris_" ++ show x)
65aname x = name ("a_" ++ show x)
67epicMain tm = do e <- epic tm
68 return $ effect_ e
70-- epicMain = effect_ $ -- ref (ename (UN "run__IO")) @@
71-- ref (ename (NS (UN "main") ["main"]))
73class ToEpic a where
74 epic :: a -> Idris E.Term
76build :: (Name, Def) -> Idris EpicDecl
77build (n, d) = do i <- getIState
78 case lookup n (idris_prims i) of
79 Just opDef -> return $ EpicFn (ename n) opDef
80 _ -> do def <- epic d
81 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
82 return $ EpicFn (ename n) def
84impossible = int 42424242
86instance ToEpic Def where
87 epic (Function tm _) = epic tm
88 epic (CaseOp _ _ pats _ _ args sc) = epic (args, sc) -- optimised version
89 epic _ = return impossible
91instance ToEpic (TT Name) where
92 epic tm = epic' [] tm where
93 epic' env tm@(App f a)
94 | (P _ (UN "mkForeign") _, args) <- unApply tm
95 = doForeign args
96 | (P _ (UN "lazy") _, [_,arg]) <- unApply tm
97 = do arg' <- epic' env arg
98 return $ lazy_ arg'
99 | (P _ (UN "prim__IO") _, [v]) <- unApply tm
100 = do v' <- epic' env v
101 return (effect_ v')
102 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
103 = do v' <- epic' env v
104 k' <- epic' env k
105 return (effect_ (k' @@ (effect_ v')))
106 | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
107 = do size' <- epic' env size
108 t' <- epic' env t
109 return $ malloc_ size' t'
110 | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm
111 = do t' <- epic' env t
112 return $ mallocTrace_ t'
113 | (P (DCon t a) n _, args) <- unApply tm
114 = epicCon env t a n args
115 epic' env (P (DCon t a) n _) = return $ con_ t
116 epic' env (P (TCon t a) n _) = return $ con_ t
117 epic' env (P _ n _) = return $ ref (ename n)
118 epic' env (V i) = return $ ref (env!!i)
119 epic' env (Bind n (Lam _) sc)
120 = do sc' <- epic' (aname n : env) sc
121 return $ term ([aname n], sc')
122 epic' env (Bind n (Let _ v) sc)
123 = do sc' <- epic' (aname n : env) sc
124 v' <- epic' env v
125 return $ let_ v' (aname n, sc')
126 epic' env (Bind _ _ _) = return impossible
127 epic' env (App f a) = do f' <- epic' env f
128 a' <- epic' env a
129 return (f' @@ a')
130 epic' env (Constant c) = epic c
131 epic' env Erased = return impossible
132 epic' env (Set _) = return impossible
134 epicCon env t arity n args
135 | length args == arity = buildApp env (con_ t) args
136 | otherwise = let extra = satArgs (arity - length args) in
137 do sc' <- epicCon env t arity n
138 (args ++ map (\n -> P Bound n undefined) extra)
139 return $ term (map ename extra, sc')
141 satArgs n = map (\i -> MN i "sat") [1..n]
143 buildApp env e [] = return e
144 buildApp env e (x:xs) = do x' <- epic' env x
145 buildApp env (e @@ x') xs
148doForeign :: [TT Name] -> Idris E.Term
149doForeign (_ : fgn : args)
150 | (_, (Constant (Str fgnName) : fgnArgTys : P _ (UN ret) _ : [])) <- unApply fgn
151 = let tys = getFTypes fgnArgTys
152 rty = mkEty ret in
153 do args' <- mapM epic args
154 -- wrap it in a prim__IO
155 -- return $ con_ 0 @@ impossible @@
156 return $ lazy_ $ foreign_ rty fgnName (zip args' tys)
157 | otherwise = fail "Badly formed foreign function call"
159getFTypes :: TT Name -> [E.Type]
160getFTypes tm = case unApply tm of
161 (nil, []) -> []
162 (cons, [(P _ (UN ty) _), xs]) ->
163 let rest = getFTypes xs in
164 mkEty ty : rest
166mkEty "FInt" = tyInt
167mkEty "FFloat" = tyFloat
168mkEty "FChar" = tyChar
169mkEty "FString" = tyString
170mkEty "FPtr" = tyPtr
171mkEty "FUnit" = tyUnit
173instance ToEpic Const where
174 epic (I i) = return (int i)
175 epic (BI i) = return (bigint i)
176 epic (Fl f) = return (float f)
177 epic (Str s) = return (str s)
178 epic (Ch c) = return (char c)
179 epic IType = return $ con_ 1
180 epic FlType = return $ con_ 2
181 epic ChType = return $ con_ 3
182 epic StrType = return $ con_ 4
183 epic PtrType = return $ con_ 5
184 epic BIType = return $ con_ 6
186instance ToEpic ([Name], SC) where
187 epic (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
188 tree' <- epic tree
189 return $ term (map ename args, tree')
191instance ToEpic SC where
192 epic (Case n [ConCase _ i ns sc])
193 = epicLet n ns 0 sc
194 where
195 epicLet x [] _ sc = epic sc
196 epicLet x (n:ns) i sc
197 = do sc' <- epicLet x ns (i+1) sc
198 return $ let_ (ref (ename x) !. i) (ename n, sc')
200 epic (STerm t) = epic t
201 epic (UnmatchedCase str) = return $ error_ str
202 epic (Case n alts) = do alts' <- mapM mkEpicAlt alts
203 return $ case_ (ref (ename n)) alts'
204 where
205 mkEpicAlt (ConCase n t args rhs) = do rhs' <- epic rhs
206 return $ con t (map ename args, rhs')
207 mkEpicAlt (ConstCase (I i) rhs) = do rhs' <- epic rhs
208 return $ constcase i rhs'
209 mkEpicAlt (ConstCase IType rhs) = do rhs' <- epic rhs
210 return $ defaultcase rhs'
211 mkEpicAlt (ConstCase c rhs)
212 = fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"
213 mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs
214 return $ defaultcase rhs'
216tempfile :: IO (FilePath, Handle)
217tempfile = do env <- environment "TMPDIR"
218 let dir = case env of
219 Nothing -> "/tmp"
220 (Just d) -> d
221 openTempFile dir "esc"
223environment :: String -> IO (Maybe String)
224environment x = catch (do e <- getEnv x
225 return (Just e))
226 (\_ -> return Nothing)