git.iko.soy/Idris-dev
on 11d4fee help sign in
Idris-dev/src/Idris/Compiler.hs
149 lines 5.7 kB history raw
1{-# LANGUAGE PatternGuards #-}
3module Idris.Compiler where
5import Idris.AbsSyntax
7import Core.TT
8import Core.Evaluate
9import Core.CaseTree
11import Control.Monad.State
13import Epic.Epic hiding (Term, Type, Name, fn, compile)
14import qualified Epic.Epic as E
16primDefs = [UN "mkForeign", UN "FalseElim", UN "believe_me"]
18compile :: FilePath -> Idris ()
19compile f = do ds <- mkDecls
20 objs <- getObjectFiles
21 libs <- getLibs
22 hdrs <- getHdrs
23 let incs = map Include hdrs
24 lift $ compileObjWith [Debug] (mkProgram (incs ++ ds)) (f ++ ".o")
25 lift $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f
27mkDecls :: Idris [EpicDecl]
28mkDecls = do i <- getIState
29 decls <- mapM build (ctxtAlist (tt_ctxt i))
30 return $ basic_defs ++ EpicFn (name "main") epicMain : decls
32ename x = name ("idris_" ++ show x)
33aname x = name ("a_" ++ show x)
35epicMain = effect_ $ -- ref (ename (UN "run__IO")) @@
36 ref (ename (NS (UN "main") ["main"]))
38class ToEpic a where
39 epic :: a -> Idris E.Term
41build :: (Name, Def) -> Idris EpicDecl
42build (n, d) = do i <- getIState
43 case lookup n (idris_prims i) of
44 Just opDef -> return $ EpicFn (ename n) opDef
45 _ -> do def <- epic d
46 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
47 return $ EpicFn (ename n) def
49impossible = int 42424242
51instance ToEpic Def where
52 epic (Function tm _) = epic tm
53 epic (CaseOp _ _ pats args sc) = epic (args, sc) -- TODO: redo case comp after optimising
54 epic _ = return impossible
56instance ToEpic (TT Name) where
57 epic tm = epic' [] tm where
58 epic' env tm@(App f a)
59 | (P _ (UN "mkForeign") _, args) <- unApply tm
60 = doForeign args
61 | (P _ (UN "lazy") _, [_, arg]) <- unApply tm
62 = do arg' <- epic' env arg
63 return $ lazy_ arg'
64 | (P _ (UN "believe_me") _, [_, _, arg]) <- unApply tm
65 = epic' env arg
66-- | (P _ (UN "prim__IO") _, [_, v]) <- unApply tm
67-- = epic' env v
68-- | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
69-- = do v' <- epic' env v
70-- k' <- epic' env k
71-- return (k' @@ v')
72 epic' env (P (DCon t a) n _) = return $ con_ t
73 epic' env (P (TCon t a) n _) = return $ con_ t
74 epic' env (P _ n _) = return $ ref (ename n)
75 epic' env (V i) = return $ ref (env!!i)
76 epic' env (Bind n (Lam _) sc)
77 = do sc' <- epic' (aname n : env) sc
78 return $ term ([aname n], sc')
79 epic' env (Bind n (Let _ v) sc)
80 = do sc' <- epic' (aname n : env) sc
81 v' <- epic' env v
82 return $ let_ v' (aname n, sc')
83 epic' env (Bind _ _ _) = return impossible
84 epic' env (App f a) = do f' <- epic' env f
85 a' <- epic' env a
86 return (f' @@ a')
87 epic' env (Constant c) = epic c
88 epic' env (Set _) = return impossible
90doForeign :: [TT Name] -> Idris E.Term
91doForeign (_ : fgn : args)
92 | (_, (Constant (Str fgnName) : fgnArgTys : P _ (UN ret) _ : [])) <- unApply fgn
93 = let tys = getFTypes fgnArgTys
94 rty = mkEty ret in
95 do args' <- mapM epic args
96 -- wrap it in a prim__IO
97 return $ con_ 0 @@ impossible @@ foreign_ rty fgnName (zip args' tys)
98 | otherwise = fail "Badly formed foreign function call"
100getFTypes :: TT Name -> [E.Type]
101getFTypes tm = case unApply tm of
102 (nil, [arg]) -> []
103 (cons, [a, (P _ (UN ty) _), xs]) ->
104 let rest = getFTypes xs in
105 mkEty ty : rest
107mkEty "FInt" = tyInt
108mkEty "FFloat" = tyFloat
109mkEty "FChar" = tyChar
110mkEty "FString" = tyString
111mkEty "FPtr" = tyPtr
112mkEty "FUnit" = tyUnit
114instance ToEpic Const where
115 epic (I i) = return (int i)
116 epic (BI i) = return (bigint i)
117 epic (Fl f) = return (float f)
118 epic (Str s) = return (str s)
119 epic (Ch c) = return (char c)
120 epic IType = return $ con_ 1
121 epic FlType = return $ con_ 2
122 epic ChType = return $ con_ 3
123 epic StrType = return $ con_ 4
124 epic PtrType = return $ con_ 5
125 epic BIType = return $ con_ 6
127instance ToEpic ([Name], SC) where
128 epic (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
129 tree' <- epic tree
130 return $ term (map ename args, tree')
132instance ToEpic SC where
133 epic (STerm t) = epic t
134 epic (UnmatchedCase str) = return $ error_ str
135 epic (Case n alts) = do alts' <- mapM mkEpicAlt alts
136 return $ case_ (ref (ename n)) alts'
137 where
138 mkEpicAlt (ConCase n t args rhs) = do rhs' <- epic rhs
139 return $ con t (map ename args, rhs')
140 mkEpicAlt (ConstCase (I i) rhs) = do rhs' <- epic rhs
141 return $ constcase i rhs'
142 mkEpicAlt (ConstCase IType rhs) = do rhs' <- epic rhs
143 return $ defaultcase rhs'
144 mkEpicAlt (ConstCase c rhs)
145 = fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"
146 mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs
147 return $ defaultcase rhs'