git.iko.soy/Idris-dev
on b63e9bb help sign in
Idris-dev/src/Idris/Compiler.hs
207 lines 7.7 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 ds <- mkDecls tm
28 objs <- getObjectFiles
29 libs <- getLibs
30 hdrs <- getHdrs
31 let incs = map Include hdrs
32 so <- getSO
33 case so of
34 Nothing ->
35 do m <- epicMain tm
36 let mainval = EpicFn (name "main") m
37 liftIO $ compileObjWith []
38 (mkProgram (incs ++ mainval : ds)) (f ++ ".o")
39 liftIO $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f
40 where checkMVs = do i <- get
41 case idris_metavars i \\ primDefs of
42 [] -> return ()
43 ms -> fail $ "There are undefined metavariables: " ++ show ms
45mkDecls :: Term -> Idris [EpicDecl]
46mkDecls t = do i <- getIState
47 decls <- mapM build (ctxtAlist (tt_ctxt i))
48 return $ basic_defs ++ decls
50-- EpicFn (name "main") epicMain : decls
52ename x = name ("idris_" ++ show x)
53aname x = name ("a_" ++ show x)
55epicMain tm = do e <- epic tm
56 return $ effect_ e
58-- epicMain = effect_ $ -- ref (ename (UN "run__IO")) @@
59-- ref (ename (NS (UN "main") ["main"]))
61class ToEpic a where
62 epic :: a -> Idris E.Term
64build :: (Name, Def) -> Idris EpicDecl
65build (n, d) = do i <- getIState
66 case lookup n (idris_prims i) of
67 Just opDef -> return $ EpicFn (ename n) opDef
68 _ -> do def <- epic d
69 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
70 return $ EpicFn (ename n) def
72impossible = int 42424242
74instance ToEpic Def where
75 epic (Function tm _) = epic tm
76 epic (CaseOp _ _ pats _ _ args sc) = epic (args, sc) -- optimised version
77 epic _ = return impossible
79instance ToEpic (TT Name) where
80 epic tm = epic' [] tm where
81 epic' env tm@(App f a)
82 | (P _ (UN "mkForeign") _, args) <- unApply tm
83 = doForeign args
84 | (P _ (UN "lazy") _, [_,arg]) <- unApply tm
85 = do arg' <- epic' env arg
86 return $ lazy_ arg'
87 | (P _ (UN "prim__IO") _, [v]) <- unApply tm
88 = epic' env v
89 | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
90 = do v' <- epic' env v
91 k' <- epic' env k
92 return (k' @@ (effect_ v'))
93 | (P (DCon t a) n _, args) <- unApply tm
94 = epicCon env t a n args
95 epic' env (P (DCon t a) n _) = return $ con_ t
96 epic' env (P (TCon t a) n _) = return $ con_ t
97 epic' env (P _ n _) = return $ ref (ename n)
98 epic' env (V i) = return $ ref (env!!i)
99 epic' env (Bind n (Lam _) sc)
100 = do sc' <- epic' (aname n : env) sc
101 return $ term ([aname n], sc')
102 epic' env (Bind n (Let _ v) sc)
103 = do sc' <- epic' (aname n : env) sc
104 v' <- epic' env v
105 return $ let_ v' (aname n, sc')
106 epic' env (Bind _ _ _) = return impossible
107 epic' env (App f a) = do f' <- epic' env f
108 a' <- epic' env a
109 return (f' @@ a')
110 epic' env (Constant c) = epic c
111 epic' env Erased = return impossible
112 epic' env (Set _) = return impossible
114 epicCon env t arity n args
115 | length args == arity = buildApp env (con_ t) args
116 | otherwise = let extra = satArgs (arity - length args) in
117 do sc' <- epicCon env t arity n
118 (args ++ map (\n -> P Bound n undefined) extra)
119 return $ term (map ename extra, sc')
121 satArgs n = map (\i -> MN i "sat") [1..n]
123 buildApp env e [] = return e
124 buildApp env e (x:xs) = do x' <- epic' env x
125 buildApp env (e @@ x') xs
128doForeign :: [TT Name] -> Idris E.Term
129doForeign (_ : fgn : args)
130 | (_, (Constant (Str fgnName) : fgnArgTys : P _ (UN ret) _ : [])) <- unApply fgn
131 = let tys = getFTypes fgnArgTys
132 rty = mkEty ret in
133 do args' <- mapM epic args
134 -- wrap it in a prim__IO
135 -- return $ con_ 0 @@ impossible @@
136 return $ lazy_ $ foreign_ rty fgnName (zip args' tys)
137 | otherwise = fail "Badly formed foreign function call"
139getFTypes :: TT Name -> [E.Type]
140getFTypes tm = case unApply tm of
141 (nil, []) -> []
142 (cons, [(P _ (UN ty) _), xs]) ->
143 let rest = getFTypes xs in
144 mkEty ty : rest
146mkEty "FInt" = tyInt
147mkEty "FFloat" = tyFloat
148mkEty "FChar" = tyChar
149mkEty "FString" = tyString
150mkEty "FPtr" = tyPtr
151mkEty "FUnit" = tyUnit
153instance ToEpic Const where
154 epic (I i) = return (int i)
155 epic (BI i) = return (bigint i)
156 epic (Fl f) = return (float f)
157 epic (Str s) = return (str s)
158 epic (Ch c) = return (char c)
159 epic IType = return $ con_ 1
160 epic FlType = return $ con_ 2
161 epic ChType = return $ con_ 3
162 epic StrType = return $ con_ 4
163 epic PtrType = return $ con_ 5
164 epic BIType = return $ con_ 6
166instance ToEpic ([Name], SC) where
167 epic (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
168 tree' <- epic tree
169 return $ term (map ename args, tree')
171instance ToEpic SC where
172 epic (Case n [ConCase _ i ns sc])
173 = epicLet n ns 0 sc
174 where
175 epicLet x [] _ sc = epic sc
176 epicLet x (n:ns) i sc
177 = do sc' <- epicLet x ns (i+1) sc
178 return $ let_ (ref (ename x) !. i) (ename n, sc')
180 epic (STerm t) = epic t
181 epic (UnmatchedCase str) = return $ error_ str
182 epic (Case n alts) = do alts' <- mapM mkEpicAlt alts
183 return $ case_ (ref (ename n)) alts'
184 where
185 mkEpicAlt (ConCase n t args rhs) = do rhs' <- epic rhs
186 return $ con t (map ename args, rhs')
187 mkEpicAlt (ConstCase (I i) rhs) = do rhs' <- epic rhs
188 return $ constcase i rhs'
189 mkEpicAlt (ConstCase IType rhs) = do rhs' <- epic rhs
190 return $ defaultcase rhs'
191 mkEpicAlt (ConstCase c rhs)
192 = fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"
193 mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs
194 return $ defaultcase rhs'
196tempfile :: IO (FilePath, Handle)
197tempfile = do env <- environment "TMPDIR"
198 let dir = case env of
199 Nothing -> "/tmp"
200 (Just d) -> d
201 openTempFile dir "esc"
203environment :: String -> IO (Maybe String)
204environment x = catch (do e <- getEnv x
205 return (Just e))
206 (\_ -> return Nothing)