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