git.iko.soy/Idris-dev
on 7ea4422 help sign in
Idris-dev/src/Idris/Compiler.hs
117 lines 4.2 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
16compile :: FilePath -> Idris ()
17compile f = do ds <- mkDecls
18 lift $ compileWith [Debug] (mkProgram ds) f
20mkDecls :: Idris [EpicDecl]
21mkDecls = do i <- getIState
22 decls <- mapM build (toAlist (tt_ctxt i))
23 return $ basic_defs ++ EpicFn (name "main") epicMain : decls
25ename x = name ("idris_" ++ show x)
26aname x = name ("a_" ++ show x)
28epicMain = ref (ename (UN ["main"]))
30class ToEpic a where
31 epic :: a -> Idris E.Term
33build :: (Name, Def) -> Idris EpicDecl
34build (n, d) = do i <- getIState
35 case lookup n (idris_prims i) of
36 Just opDef -> return $ EpicFn (ename n) opDef
37 _ -> do def <- epic d
38 return $ EpicFn (ename n) def
40impossible = int 42424242
42instance ToEpic Def where
43 epic (Function (Fun _ _ tm _)) = epic tm
44 epic (CaseOp _ pats args sc) = epic (args, sc) -- TODO: redo case comp after optimising
45 epic _ = return impossible
47instance ToEpic (TT Name) where
48 epic tm = epic' [] tm where
49 epic' env tm@(App f a)
50 | (P _ (UN ["mkForeign"]) _, args) <- unApply tm
51 = doForeign args
52 epic' env (P (DCon t a) n _) = return $ con_ t
53 epic' env (P (TCon _) _ _) = return impossible
54 epic' env (P _ n _) = return $ ref (ename n)
55 epic' env (V i) = return $ ref (env!!i)
56 epic' env (Bind n (Lam _) sc)
57 = do sc' <- epic' (aname n : env) sc
58 return $ term ([aname n], sc')
59 epic' env (Bind _ _ _) = return impossible
60 epic' env (App f a) = do f' <- epic' env f
61 a' <- epic' env a
62 logLvl 3 $ "Compiled " ++ show f ++ " @@ " ++ show a
63 return (f' @@ a')
64 epic' env (Constant c) = epic c
65 epic' env (Set _) = return impossible
67doForeign :: [TT Name] -> Idris E.Term
68doForeign (_ : fgn : args)
69 | (_, (Constant (Str fgnName) : fgnArgTys : P _ (UN [ret]) _ : [])) <- unApply fgn
70 = let tys = getFTypes fgnArgTys
71 rty = mkEty ret in
72 do args' <- mapM epic args
73 -- wrap it in a prim__IO
74 return $ con_ 0 @@ impossible @@ foreign_ rty fgnName (zip args' tys)
75 | otherwise = fail "Badly formed foreign function call"
77getFTypes :: TT Name -> [E.Type]
78getFTypes tm = case unApply tm of
79 (nil, [arg]) -> []
80 (cons, [a, (P _ (UN [ty]) _), xs]) ->
81 let rest = getFTypes xs in
82 mkEty ty : rest
84mkEty "FInt" = tyInt
85mkEty "FFloat" = tyFloat
86mkEty "FChar" = tyChar
87mkEty "FString" = tyString
88mkEty "FPtr" = tyPtr
89mkEty "FUnit" = tyUnit
91instance ToEpic Const where
92 epic (I i) = return (int i)
93 epic (Fl f) = return (float f)
94 epic (Str s) = return (str s)
95 epic (Ch c) = return (char c)
96 epic _ = return impossible
98instance ToEpic ([Name], SC) where
99 epic (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
100 tree' <- epic tree
101 return $ term (map ename args, tree')
103instance ToEpic SC where
104 epic (STerm t) = epic t
105 epic (UnmatchedCase str) = return $ error_ str
106 epic (Case n alts) = do alts' <- mapM mkEpicAlt alts
107 return $ case_ (ref (ename n)) alts'
108 where
109 mkEpicAlt (ConCase n t args rhs) = do rhs' <- epic rhs
110 return $ con t (map ename args, rhs')
111 mkEpicAlt (ConstCase (I i) rhs) = do rhs' <- epic rhs
112 return $ constcase i rhs'
113 mkEpicAlt (ConstCase _ rhs) = fail "Can only pattern match on integer constants"
114 mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs
115 return $ defaultcase rhs'