git.iko.soy/Idris-dev
on 02003d7 help sign in
Idris-dev/src/Idris/Compiler.hs
226 lines 8.5 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 = epic' env v
101 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
102 = do v' <- epic' env v
103 k' <- epic' env k
104 return (k' @@ (effect_ v'))
105 | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
106 = do size' <- epic' env size
107 t' <- epic' env t
108 return $ malloc_ size' t'
109 | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm
110 = do t' <- epic' env t
111 return $ mallocTrace_ t'
112 | (P (DCon t a) n _, args) <- unApply tm
113 = epicCon env t a n args
114 epic' env (P (DCon t a) n _) = return $ con_ t
115 epic' env (P (TCon t a) n _) = return $ con_ t
116 epic' env (P _ n _) = return $ ref (ename n)
117 epic' env (V i) = return $ ref (env!!i)
118 epic' env (Bind n (Lam _) sc)
119 = do sc' <- epic' (aname n : env) sc
120 return $ term ([aname n], sc')
121 epic' env (Bind n (Let _ v) sc)
122 = do sc' <- epic' (aname n : env) sc
123 v' <- epic' env v
124 return $ let_ v' (aname n, sc')
125 epic' env (Bind _ _ _) = return impossible
126 epic' env (App f a) = do f' <- epic' env f
127 a' <- epic' env a
128 return (f' @@ a')
129 epic' env (Constant c) = epic c
130 epic' env Erased = return impossible
131 epic' env (Set _) = return impossible
133 epicCon env t arity n args
134 | length args == arity = buildApp env (con_ t) args
135 | otherwise = let extra = satArgs (arity - length args) in
136 do sc' <- epicCon env t arity n
137 (args ++ map (\n -> P Bound n undefined) extra)
138 return $ term (map ename extra, sc')
140 satArgs n = map (\i -> MN i "sat") [1..n]
142 buildApp env e [] = return e
143 buildApp env e (x:xs) = do x' <- epic' env x
144 buildApp env (e @@ x') xs
147doForeign :: [TT Name] -> Idris E.Term
148doForeign (_ : fgn : args)
149 | (_, (Constant (Str fgnName) : fgnArgTys : P _ (UN ret) _ : [])) <- unApply fgn
150 = let tys = getFTypes fgnArgTys
151 rty = mkEty ret in
152 do args' <- mapM epic args
153 -- wrap it in a prim__IO
154 -- return $ con_ 0 @@ impossible @@
155 return $ lazy_ $ foreign_ rty fgnName (zip args' tys)
156 | otherwise = fail "Badly formed foreign function call"
158getFTypes :: TT Name -> [E.Type]
159getFTypes tm = case unApply tm of
160 (nil, []) -> []
161 (cons, [(P _ (UN ty) _), xs]) ->
162 let rest = getFTypes xs in
163 mkEty ty : rest
165mkEty "FInt" = tyInt
166mkEty "FFloat" = tyFloat
167mkEty "FChar" = tyChar
168mkEty "FString" = tyString
169mkEty "FPtr" = tyPtr
170mkEty "FUnit" = tyUnit
172instance ToEpic Const where
173 epic (I i) = return (int i)
174 epic (BI i) = return (bigint i)
175 epic (Fl f) = return (float f)
176 epic (Str s) = return (str s)
177 epic (Ch c) = return (char c)
178 epic IType = return $ con_ 1
179 epic FlType = return $ con_ 2
180 epic ChType = return $ con_ 3
181 epic StrType = return $ con_ 4
182 epic PtrType = return $ con_ 5
183 epic BIType = return $ con_ 6
185instance ToEpic ([Name], SC) where
186 epic (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
187 tree' <- epic tree
188 return $ term (map ename args, tree')
190instance ToEpic SC where
191 epic (Case n [ConCase _ i ns sc])
192 = epicLet n ns 0 sc
193 where
194 epicLet x [] _ sc = epic sc
195 epicLet x (n:ns) i sc
196 = do sc' <- epicLet x ns (i+1) sc
197 return $ let_ (ref (ename x) !. i) (ename n, sc')
199 epic (STerm t) = epic t
200 epic (UnmatchedCase str) = return $ error_ str
201 epic (Case n alts) = do alts' <- mapM mkEpicAlt alts
202 return $ case_ (ref (ename n)) alts'
203 where
204 mkEpicAlt (ConCase n t args rhs) = do rhs' <- epic rhs
205 return $ con t (map ename args, rhs')
206 mkEpicAlt (ConstCase (I i) rhs) = do rhs' <- epic rhs
207 return $ constcase i rhs'
208 mkEpicAlt (ConstCase IType rhs) = do rhs' <- epic rhs
209 return $ defaultcase rhs'
210 mkEpicAlt (ConstCase c rhs)
211 = fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"
212 mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs
213 return $ defaultcase rhs'
215tempfile :: IO (FilePath, Handle)
216tempfile = do env <- environment "TMPDIR"
217 let dir = case env of
218 Nothing -> "/tmp"
219 (Just d) -> d
220 openTempFile dir "esc"
222environment :: String -> IO (Maybe String)
223environment x = catch (do e <- getEnv x
224 return (Just e))
225 (\_ -> return Nothing)