@@ -0,0 +1,207 @@
1+{-# LANGUAGE PatternGuards #-}
2+
3+module IRTS.Compiler where
4+
5+import IRTS.Lang
6+import IRTS.Defunctionalise
7+import IRTS.Simplified
8+import IRTS.CodegenC
9+
10+import Idris.AbsSyntax
11+import Core.TT
12+import Core.Evaluate
13+import Core.CaseTree
14+
15+import Control.Monad.State
16+import Data.List
17+import System.Process
18+import System.IO
19+import System.Directory
20+import System.Environment
21+
22+import Paths_idris
23+
24+compileC :: FilePath -> Term -> Idris ()
25+compileC f tm = do checkMVs
26+ let tmnames = namesUsed (STerm tm)
27+ used <- mapM (allNames []) tmnames
28+ defsIn <- mkDecls tm (concat used)
29+ maindef <- irMain tm
30+ let defs = defsIn ++ [(MN 0 "runMain", maindef)]
31+ iputStrLn (show defs)
32+ let (nexttag, tagged) = addTags 0 (liftAll defs)
33+ let ctxtIn = addAlist tagged emptyContext
34+ let defuns = defunctionalise nexttag ctxtIn
35+-- print defuns
36+ let checked = checkDefs defuns (toAlist defuns)
37+-- print checked
38+ case checked of
39+ OK c -> liftIO $ codegenC c f True [] "" TRACE
40+ Error e -> fail $ show e
41+ where checkMVs = do i <- get
42+ case idris_metavars i \\ primDefs of
43+ [] -> return ()
44+ ms -> fail $ "There are undefined metavariables: " ++ show ms
45+ inDir d h = do let f = d ++ "/" ++ h
46+ ex <- doesFileExist f
47+ if ex then return f else return h
48+
49+irMain :: TT Name -> Idris LDecl
50+irMain tm = do i <- ir tm
51+ return $ LFun (MN 0 "runMain") [] (LForce i)
52+
53+allNames :: [Name] -> Name -> Idris [Name]
54+allNames ns n | n `elem` ns = return []
55+allNames ns n = do i <- get
56+ case lookupCtxt Nothing n (idris_callgraph i) of
57+ [ns'] -> do more <- mapM (allNames (n:ns)) ns'
58+ return (nub (n : concat more))
59+ _ -> return [n]
60+
61+mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]
62+mkDecls t used
63+ = do i <- getIState
64+ let ds = filter (\ (n, d) -> n `elem` used) $ ctxtAlist (tt_ctxt i)
65+ decls <- mapM build ds
66+ return decls
67+
68+class ToIR a where
69+ ir :: a -> Idris LExp
70+
71+build :: (Name, Def) -> Idris (Name, LDecl)
72+build (n, d)
73+ = do i <- getIState
74+ case lookup n (idris_scprims i) of
75+ Just (ar, op) ->
76+ let args = map (\x -> MN x "op") [0..] in
77+ return (n, (LFun n (take ar args)
78+ (LOp op (map (LV . Glob) (take ar args)))))
79+ _ -> do def <- mkLDecl n d
80+ logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
81+ return (n, def)
82+
83+declArgs args n (LLam xs x) = declArgs (args ++ xs) n x
84+declArgs args n x = LFun n args x
85+
86+mkLDecl n (Function tm _) = do e <- ir tm
87+ return (declArgs [] n e)
88+mkLDecl n (CaseOp _ _ pats _ _ args sc) = do e <- ir (args, sc)
89+ return (declArgs [] n e)
90+mkLDecl n (TyDecl (DCon t a) _) = return $ LConstructor n (-1) a
91+mkLDecl n (TyDecl (TCon t a) _) = return $ LConstructor n (-1) a
92+mkLDecl n _ = return (LFun n [] (LError "Impossible"))
93+
94+instance ToIR (TT Name) where
95+ ir tm = ir' [] tm where
96+ ir' env tm@(App f a)
97+ | (P _ (UN "mkForeign") _, args) <- unApply tm
98+ = doForeign args
99+ | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm
100+ = ir' env arg
101+ | (P _ (UN "lazy") _, [_, arg]) <- unApply tm
102+ = do arg' <- ir' env arg
103+ return $ LLazyExp arg'
104+ | (P _ (UN "prim__IO") _, [v]) <- unApply tm
105+ = do v' <- ir' env v
106+ return v'
107+ | (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
108+ = do v' <- ir' env v
109+ k' <- ir' env k
110+ return (LApp False k' [LForce v'])
111+ | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
112+ = do size' <- ir' env size
113+ t' <- ir' env t
114+ return t' -- TODO $ malloc_ size' t'
115+ | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm
116+ = do t' <- ir' env t
117+ return t' -- TODO
118+ | (P (DCon t a) n _, args) <- unApply tm
119+ = irCon env t a n args
120+ | (f, args) <- unApply tm
121+ = do f' <- ir' env f
122+ args' <- mapM (ir' env) args
123+ return (LApp False f' args')
124+ ir' env (P _ n _) = return $ LV (Glob n)
125+ ir' env (V i) = return $ LV (Glob (env!!i))
126+ ir' env (Bind n (Lam _) sc)
127+ = do sc' <- ir' (n : env) sc
128+ return $ LLam [n] sc'
129+ ir' env (Bind n (Let _ v) sc)
130+ = do sc' <- ir' (n : env) sc
131+ v' <- ir' env v
132+ return $ LLet n v' sc'
133+ ir' env (Bind _ _ _) = return $ LError "Impossible"
134+ ir' env (Constant c) = return $ LConst c
135+ ir' env _ = return $ LError "Impossible"
136+
137+ irCon env t arity n args
138+ | length args == arity = buildApp env (LV (Glob n)) args
139+ | otherwise = let extra = satArgs (arity - length args) in
140+ do sc' <- irCon env t arity n
141+ (args ++ map (\n -> P Bound n undefined) extra)
142+ return $ LLam extra sc'
143+
144+ satArgs n = map (\i -> MN i "sat") [1..n]
145+
146+ buildApp env e [] = return e
147+ buildApp env e xs = do xs' <- mapM (ir' env) xs
148+ return $ LApp False e xs'
149+
150+doForeign :: [TT Name] -> Idris LExp
151+doForeign (_ : fgn : args)
152+ | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
153+ = let tys = getFTypes fgnArgTys
154+ rty = mkIty' ret in
155+ do args' <- mapM ir args
156+ -- wrap it in a prim__IO
157+ -- return $ con_ 0 @@ impossible @@
158+ return $ LLazyExp $ LForeign LANG_C rty fgnName (zip tys args')
159+ | otherwise = fail "Badly formed foreign function call"
160+
161+getFTypes :: TT Name -> [FType]
162+getFTypes tm = case unApply tm of
163+ (nil, []) -> []
164+ (cons, [ty, xs]) ->
165+ let rest = getFTypes xs in
166+ mkIty' ty : rest
167+
168+mkIty' (P _ (UN ty) _) = mkIty ty
169+mkIty' _ = FAny
170+
171+mkIty "FInt" = FInt
172+mkIty "FFloat" = FDouble
173+mkIty "FChar" = FChar
174+mkIty "FString" = FString
175+mkIty "FPtr" = FPtr
176+mkIty "FUnit" = FUnit
177+
178+instance ToIR ([Name], SC) where
179+ ir (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
180+ tree' <- ir tree
181+ return $ LLam args tree'
182+
183+instance ToIR SC where
184+ ir (STerm t) = ir t
185+ ir (UnmatchedCase str) = return $ LError str
186+ ir (Case n alts) = do alts' <- mapM mkIRAlt alts
187+ return $ LCase (LV (Glob n)) alts'
188+ where
189+ mkIRAlt (ConCase n t args rhs)
190+ = do rhs' <- ir rhs
191+ return $ LConCase (-1) n args rhs'
192+ mkIRAlt (ConstCase (I i) rhs)
193+ = do rhs' <- ir rhs
194+ return $ LConstCase (I i) rhs'
195+ mkIRAlt (ConstCase IType rhs)
196+ = do rhs' <- ir rhs
197+ return $ LDefaultCase rhs'
198+ mkIRAlt (ConstCase c rhs)
199+ = fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"
200+ mkIRAlt (DefaultCase rhs)
201+ = do rhs' <- ir rhs
202+ return $ LDefaultCase rhs'
203+
204+
205+
206+
207+