git.iko.soy/Idris-dev
on fa0ecde help sign in
Idris-dev/src/Idris/Compiler.hs
246 lines 9.3 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 Paths_idris
21import Epic.Epic hiding (Term, Type, Name, fn, compile)
22import qualified Epic.Epic as E
24primDefs = [UN "unsafePerformIO", UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]
26compile :: FilePath -> Term -> Idris ()
27compile f tm
28 = do checkMVs
29 let tmnames = namesUsed (STerm tm)
30 used <- mapM (allNames []) tmnames
31 ds <- mkDecls tm (concat used)
32 objs <- getObjectFiles
33 libs <- getLibs
34 hdrs <- getHdrs
35 ddir <- liftIO $ getDataDir
36 -- if any includes exist in the data directory, use that
37 hdrs' <- liftIO $ mapM (inDir ddir) hdrs
38 let incs = map Include hdrs'
39 so <- getSO
40-- let ilib = ddir ++ "/libidris.a"
41 case so of
42 Nothing ->
43 do m <- epicMain tm
44 let mainval = EpicFn (name "main") m
45 liftIO $ compileObjWith []
46 (mkProgram (incs ++ mainval : ds)) (f ++ ".o")
47 liftIO $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f
48 where checkMVs = do i <- get
49 case idris_metavars i \\ primDefs of
50 [] -> return ()
51 ms -> fail $ "There are undefined metavariables: " ++ show ms
52 inDir d h = do let f = d ++ "/" ++ h
53 ex <- doesFileExist f
54 if ex then return f else return h
57allNames :: [Name] -> Name -> Idris [Name]
58allNames ns n | n `elem` ns = return []
59allNames ns n = do i <- get
60 case lookupCtxt Nothing n (idris_callgraph i) of
61 [ns'] -> do more <- mapM (allNames (n:ns)) ns'
62 return (nub (n : concat more))
63 _ -> return [n]
65mkDecls :: Term -> [Name] -> Idris [EpicDecl]
66mkDecls t used
67 = do i <- getIState
68 let ds = filter (\ (n, d) -> n `elem` used) $ ctxtAlist (tt_ctxt i)
69 decls <- mapM build ds
70 return $ basic_defs ++ decls
72-- EpicFn (name "main") epicMain : decls
74ename x = name ("idris_" ++ show x)
75aname x = name ("a_" ++ show x)
77epicMain tm = do e <- epic tm
78 return $ effect_ e
80-- epicMain = effect_ $ -- ref (ename (UN "run__IO")) @@
81-- ref (ename (NS (UN "main") ["main"]))
83class ToEpic a where
84 epic :: a -> Idris E.Term
86build :: (Name, Def) -> Idris EpicDecl
87build (n, d) = do i <- getIState
88 case lookup n (idris_prims i) of
89 Just opDef -> return $ EpicFn (ename n) opDef
90 _ -> do def <- epic d
91 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
92 return $ EpicFn (ename n) def
94impossible = int 42424242
96instance ToEpic Def where
97 epic (Function tm _) = epic tm
98 epic (CaseOp _ _ pats _ _ args sc) = epic (args, sc) -- optimised version
99 epic _ = return impossible
101instance ToEpic (TT Name) where
102 epic tm = epic' [] tm where
103 epic' env tm@(App f a)
104 | (P _ (UN "mkForeign") _, args) <- unApply tm
105 = doForeign False args
106 | (P _ (UN "mkLazyForeign") _, args) <- unApply tm
107 = doForeign True args
108 | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm
109 = epic' env arg
110 | (P _ (UN "lazy") _, [_,arg]) <- unApply tm
111 = do arg' <- epic' env arg
112 return $ lazy_ arg'
113 | (P _ (UN "prim__IO") _, [v]) <- unApply tm
114 = do v' <- epic' env v
115 return (effect_ v')
116 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
117 = do v' <- epic' env v
118 k' <- epic' env k
119 return (effect_ (k' @@ (effect_ v')))
120 | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
121 = do size' <- epic' env size
122 t' <- epic' env t
123 return $ malloc_ size' t'
124 | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm
125 = do t' <- epic' env t
126 return $ mallocTrace_ t'
127 | (P (DCon t a) n _, args) <- unApply tm
128 = epicCon env t a n args
129 epic' env (P (DCon t a) n _) = return $ con_ t
130 epic' env (P (TCon t a) n _) = return $ con_ t
131 epic' env (P _ n _) = return $ ref (ename n)
132 epic' env (V i) = return $ ref (env!!i)
133 epic' env (Bind n (Lam _) sc)
134 = do sc' <- epic' (aname n : env) sc
135 return $ term ([aname n], sc')
136 epic' env (Bind n (Let _ v) sc)
137 = do sc' <- epic' (aname n : env) sc
138 v' <- epic' env v
139 return $ let_ v' (aname n, sc')
140 epic' env (Bind _ _ _) = return impossible
141 epic' env (App f a) = do f' <- epic' env f
142 a' <- epic' env a
143 return (f' @@ a')
144 epic' env (Constant c) = epic c
145 epic' env Erased = return impossible
146 epic' env (Set _) = return impossible
148 epicCon env t arity n args
149 | length args == arity = buildApp env (con_ t) args
150 | otherwise = let extra = satArgs (arity - length args) in
151 do sc' <- epicCon env t arity n
152 (args ++ map (\n -> P Bound n undefined) extra)
153 return $ term (map ename extra, sc')
155 satArgs n = map (\i -> MN i "sat") [1..n]
157 buildApp env e [] = return e
158 buildApp env e (x:xs) = do x' <- epic' env x
159 buildApp env (e @@ x') xs
162doForeign :: Bool -> [TT Name] -> Idris E.Term
163doForeign lazy (_ : fgn : args)
164 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
165 = let tys = getFTypes fgnArgTys
166 rty = mkEty' ret in
167 do args' <- mapM epic args
168 -- wrap it in a prim__IO
169 -- return $ con_ 0 @@ impossible @@
170 if lazy
171 then return $ lazy_ $ foreignL_ rty fgnName (zip args' tys)
172 else return $ lazy_ $ foreign_ rty fgnName (zip args' tys)
173 | otherwise = fail "Badly formed foreign function call"
175getFTypes :: TT Name -> [E.Type]
176getFTypes tm = case unApply tm of
177 (nil, []) -> []
178 (cons, [ty, xs]) ->
179 let rest = getFTypes xs in
180 mkEty' ty : rest
182mkEty' (P _ (UN ty) _) = mkEty ty
183mkEty' _ = tyAny
185mkEty "FInt" = tyInt
186mkEty "FFloat" = tyFloat
187mkEty "FChar" = tyChar
188mkEty "FString" = tyString
189mkEty "FPtr" = tyPtr
190mkEty "FUnit" = tyUnit
192instance ToEpic Const where
193 epic (I i) = return (int i)
194 epic (BI i) = return (bigint i)
195 epic (Fl f) = return (float f)
196 epic (Str s) = return (str s)
197 epic (Ch c) = return (char c)
198 epic IType = return $ con_ 1
199 epic FlType = return $ con_ 2
200 epic ChType = return $ con_ 3
201 epic StrType = return $ con_ 4
202 epic PtrType = return $ con_ 5
203 epic BIType = return $ con_ 6
205instance ToEpic ([Name], SC) where
206 epic (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
207 tree' <- epic tree
208 return $ term (map ename args, tree')
210instance ToEpic SC where
211 epic (Case n [ConCase _ i ns sc])
212 = epicLet n ns 0 sc
213 where
214 epicLet x [] _ sc = epic sc
215 epicLet x (n:ns) i sc
216 = do sc' <- epicLet x ns (i+1) sc
217 return $ let_ (ref (ename x) !. i) (ename n, sc')
219 epic (STerm t) = epic t
220 epic (UnmatchedCase str) = return $ error_ str
221 epic (Case n alts) = do alts' <- mapM mkEpicAlt alts
222 return $ case_ (ref (ename n)) alts'
223 where
224 mkEpicAlt (ConCase n t args rhs) = do rhs' <- epic rhs
225 return $ con t (map ename args, rhs')
226 mkEpicAlt (ConstCase (I i) rhs) = do rhs' <- epic rhs
227 return $ constcase i rhs'
228 mkEpicAlt (ConstCase IType rhs) = do rhs' <- epic rhs
229 return $ defaultcase rhs'
230 mkEpicAlt (ConstCase c rhs)
231 = fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"
232 mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs
233 return $ defaultcase rhs'
235tempfile :: IO (FilePath, Handle)
236tempfile = do env <- environment "TMPDIR"
237 let dir = case env of
238 Nothing -> "/tmp"
239 (Just d) -> d
240 openTempFile dir "esc"
242environment :: String -> IO (Maybe String)
243environment x = catch (do e <- getEnv x
244 return (Just e))
245 (\_ -> return Nothing)