git.iko.soy/Idris-dev
on 048e2a7 help sign in
Idris-dev/src/Idris/Compiler.hs
139 lines 5.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 objs <- getObjectFiles
21 libs <- getLibs
22 lift $ compileObjWith [Debug] (mkProgram ds) (f ++ ".o")
23 lift $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f
25mkDecls :: Idris [EpicDecl]
26mkDecls = do i <- getIState
27 decls <- mapM build (toAlist (tt_ctxt i))
28 return $ basic_defs ++ EpicFn (name "main") epicMain : decls
30ename x = name ("idris_" ++ show x)
31aname x = name ("a_" ++ show x)
33epicMain = effect_ $ ref (ename (UN ["run__IO"])) @@
34 ref (ename (UN ["main"]))
36class ToEpic a where
37 epic :: a -> Idris E.Term
39build :: (Name, Def) -> Idris EpicDecl
40build (n, d) = do i <- getIState
41 case lookup n (idris_prims i) of
42 Just opDef -> return $ EpicFn (ename n) opDef
43 _ -> do def <- epic d
44 logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
45 return $ EpicFn (ename n) def
47impossible = int 42424242
49instance ToEpic Def where
50 epic (Function (Fun _ _ tm _)) = epic tm
51 epic (CaseOp _ _ pats args sc) = epic (args, sc) -- TODO: redo case comp after optimising
52 epic _ = return impossible
54instance ToEpic (TT Name) where
55 epic tm = epic' [] tm where
56 epic' env tm@(App f a)
57 | (P _ (UN ["mkForeign"]) _, args) <- unApply tm
58 = doForeign args
59 | (P _ (UN ["lazy"]) _, [_, arg]) <- unApply tm
60 = do arg' <- epic' env arg
61 return $ lazy_ arg'
62 epic' env (P (DCon t a) n _) = return $ con_ t
63 epic' env (P (TCon t a) n _) = return $ con_ t
64 epic' env (P _ n _) = return $ ref (ename n)
65 epic' env (V i) = return $ ref (env!!i)
66 epic' env (Bind n (Lam _) sc)
67 = do sc' <- epic' (aname n : env) sc
68 return $ term ([aname n], sc')
69 epic' env (Bind n (Let _ v) sc)
70 = do sc' <- epic' (aname n : env) sc
71 v' <- epic' env v
72 return $ let_ v' (aname n, sc')
73 epic' env (Bind _ _ _) = return impossible
74 epic' env (App f a) = do f' <- epic' env f
75 a' <- epic' env a
76 return (f' @@ a')
77 epic' env (Constant c) = epic c
78 epic' env (Set _) = return impossible
80doForeign :: [TT Name] -> Idris E.Term
81doForeign (_ : fgn : args)
82 | (_, (Constant (Str fgnName) : fgnArgTys : P _ (UN [ret]) _ : [])) <- unApply fgn
83 = let tys = getFTypes fgnArgTys
84 rty = mkEty ret in
85 do args' <- mapM epic args
86 -- wrap it in a prim__IO
87 return $ con_ 0 @@ impossible @@ foreign_ rty fgnName (zip args' tys)
88 | otherwise = fail "Badly formed foreign function call"
90getFTypes :: TT Name -> [E.Type]
91getFTypes tm = case unApply tm of
92 (nil, [arg]) -> []
93 (cons, [a, (P _ (UN [ty]) _), xs]) ->
94 let rest = getFTypes xs in
95 mkEty ty : rest
97mkEty "FInt" = tyInt
98mkEty "FFloat" = tyFloat
99mkEty "FChar" = tyChar
100mkEty "FString" = tyString
101mkEty "FPtr" = tyPtr
102mkEty "FUnit" = tyUnit
104instance ToEpic Const where
105 epic (I i) = return (int i)
106 epic (BI i) = return (bigint i)
107 epic (Fl f) = return (float f)
108 epic (Str s) = return (str s)
109 epic (Ch c) = return (char c)
110 epic IType = return $ con_ 1
111 epic FlType = return $ con_ 2
112 epic ChType = return $ con_ 3
113 epic StrType = return $ con_ 4
114 epic PtrType = return $ con_ 5
115 epic BIType = return $ con_ 6
117instance ToEpic ([Name], SC) where
118 epic (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
119 tree' <- epic tree
120 return $ term (map ename args, tree')
122instance ToEpic SC where
123 epic (STerm t) = epic t
124 epic (UnmatchedCase str) = return $ error_ str
125 epic (Case n alts) = do alts' <- mapM mkEpicAlt alts
126 return $ case_ (ref (ename n)) alts'
127 where
128 mkEpicAlt (ConCase n t args rhs) = do rhs' <- epic rhs
129 return $ con t (map ename args, rhs')
130 mkEpicAlt (ConstCase (I i) rhs) = do rhs' <- epic rhs
131 return $ constcase i rhs'
132 mkEpicAlt (ConstCase IType rhs) = do rhs' <- epic rhs
133 return $ defaultcase rhs'
134 mkEpicAlt (ConstCase c rhs)
135 = fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"
136 mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs
137 return $ defaultcase rhs'