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