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