idris-0.9.6: src/Idris/Compiler.hs
{-# LANGUAGE PatternGuards #-}
module Idris.Compiler where
import Idris.AbsSyntax
import Core.TT
{-
import Idris.Transforms
import Core.Evaluate
import Core.CaseTree
import Control.Monad.State
import Data.List
import System.Process
import System.IO
import System.Directory
import System.Environment
import Paths_idris
import Epic.Epic hiding (Term, Type, Name, fn, compile)
import qualified Epic.Epic as E
-}
compileEpic :: FilePath -> Term -> Idris ()
compileEpic f t = fail "Epic backend disabled"
{-
compile f tm
= do checkMVs
let tmnames = namesUsed (STerm tm)
used <- mapM (allNames []) tmnames
ds <- mkDecls tm (concat used)
objs <- getObjectFiles
libs <- getLibs
hdrs <- getHdrs
ddir <- liftIO $ getDataDir
-- if any includes exist in the data directory, use that
hdrs' <- liftIO $ mapM (inDir ddir) hdrs
let incs = map Include hdrs'
so <- getSO
-- let ilib = ddir ++ "/libidris.a"
case so of
Nothing ->
do m <- epicMain tm
let mainval = EpicFn (name "main") m
liftIO $ compileObjWith []
(mkProgram (incs ++ mainval : ds)) (f ++ ".o")
liftIO $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f
where checkMVs = do i <- get
case idris_metavars i \\ primDefs of
[] -> return ()
ms -> fail $ "There are undefined metavariables: " ++ show ms
inDir d h = do let f = d ++ "/" ++ h
ex <- doesFileExist f
if ex then return f else return h
allNames :: [Name] -> Name -> Idris [Name]
allNames ns n | n `elem` ns = return []
allNames ns n = do i <- get
case lookupCtxt Nothing n (idris_callgraph i) of
[ns'] -> do more <- mapM (allNames (n:ns)) ns'
return (nub (n : concat more))
_ -> return [n]
mkDecls :: Term -> [Name] -> Idris [EpicDecl]
mkDecls t used
= do i <- getIState
let ds = filter (\ (n, d) -> n `elem` used) $ ctxtAlist (tt_ctxt i)
decls <- mapM build ds
return $ basic_defs ++ decls
-- EpicFn (name "main") epicMain : decls
ename x = name ("idris_" ++ show x)
aname x = name ("a_" ++ show x)
epicMain tm = do e <- epic tm
return $ effect_ e
-- epicMain = effect_ $ -- ref (ename (UN "run__IO")) @@
-- ref (ename (NS (UN "main") ["main"]))
class ToEpic a where
epic :: a -> Idris E.Term
build :: (Name, Def) -> Idris EpicDecl
build (n, d) = do i <- getIState
case lookup n (idris_prims i) of
Just opDef -> return $ EpicFn (ename n) opDef
_ -> do def <- epic d
logLvl 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
return $ EpicFn (ename n) def
impossible = int 42424242
instance ToEpic Def where
epic (Function tm _) = epic tm
epic (CaseOp _ _ pats _ _ args sc) = epic (args, sc) -- optimised version
epic _ = return impossible
instance ToEpic (TT Name) where
epic tm = epic' [] tm where
epic' env tm@(App f a)
| (P _ (UN "mkForeign") _, args) <- unApply tm
= doForeign False args
| (P _ (UN "mkLazyForeign") _, args) <- unApply tm
= doForeign True args
| (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm
= epic' env arg
| (P _ (UN "lazy") _, [_,arg]) <- unApply tm
= do arg' <- epic' env arg
return $ lazy_ arg'
| (P _ (UN "prim__IO") _, [v]) <- unApply tm
= do v' <- epic' env v
return (effect_ v')
| (P _ (UN "io_bind") _, [_,_,v,k]) <- unApply tm
= do v' <- epic' env v
k' <- epic' env k
return (effect_ (k' @@ (effect_ v')))
| (P _ (UN "malloc") _, [_,size,t]) <- unApply tm
= do size' <- epic' env size
t' <- epic' env t
return $ malloc_ size' t'
| (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm
= do t' <- epic' env t
return $ mallocTrace_ t'
| (P (DCon t a) n _, args) <- unApply tm
= epicCon env t a n args
epic' env (P (DCon t a) n _) = return $ con_ t
epic' env (P (TCon t a) n _) = return $ con_ t
epic' env (P _ n _) = return $ ref (ename n)
epic' env (V i) = return $ ref (env!!i)
epic' env (Bind n (Lam _) sc)
= do sc' <- epic' (aname n : env) sc
return $ term ([aname n], sc')
epic' env (Bind n (Let _ v) sc)
= do sc' <- epic' (aname n : env) sc
v' <- epic' env v
return $ let_ v' (aname n, sc')
epic' env (Bind _ _ _) = return impossible
epic' env (App f a) = do f' <- epic' env f
a' <- epic' env a
return (f' @@ a')
epic' env (Constant c) = epic c
epic' env Erased = return impossible
epic' env (TType _) = return impossible
epicCon env t arity n args
| length args == arity = buildApp env (con_ t) args
| otherwise = let extra = satArgs (arity - length args) in
do sc' <- epicCon env t arity n
(args ++ map (\n -> P Bound n undefined) extra)
return $ term (map ename extra, sc')
satArgs n = map (\i -> MN i "sat") [1..n]
buildApp env e [] = return e
buildApp env e (x:xs) = do x' <- epic' env x
buildApp env (e @@ x') xs
doForeign :: Bool -> [TT Name] -> Idris E.Term
doForeign lazy (_ : fgn : args)
| (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn
= let tys = getFTypes fgnArgTys
rty = mkEty' ret in
do args' <- mapM epic args
-- wrap it in a prim__IO
-- return $ con_ 0 @@ impossible @@
if lazy
then return $ lazy_ $ foreignL_ rty fgnName (zip args' tys)
else return $ lazy_ $ foreign_ rty fgnName (zip args' tys)
| otherwise = fail "Badly formed foreign function call"
getFTypes :: TT Name -> [E.Type]
getFTypes tm = case unApply tm of
(nil, []) -> []
(cons, [ty, xs]) ->
let rest = getFTypes xs in
mkEty' ty : rest
mkEty' (P _ (UN ty) _) = mkEty ty
mkEty' _ = tyAny
mkEty "FInt" = tyInt
mkEty "FFloat" = tyFloat
mkEty "FChar" = tyChar
mkEty "FString" = tyString
mkEty "FPtr" = tyPtr
mkEty "FUnit" = tyUnit
instance ToEpic Const where
epic (I i) = return (int i)
epic (BI i) = return (bigint i)
epic (Fl f) = return (float f)
epic (Str s) = return (str s)
epic (Ch c) = return (char c)
epic IType = return $ con_ 1
epic FlType = return $ con_ 2
epic ChType = return $ con_ 3
epic StrType = return $ con_ 4
epic PtrType = return $ con_ 5
epic BIType = return $ con_ 6
instance ToEpic ([Name], SC) where
epic (args, tree) = do logLvl 3 $ "Compiling " ++ show args ++ "\n" ++ show tree
tree' <- epic tree
return $ term (map ename args, tree')
instance ToEpic SC where
epic (Case n [ConCase _ i ns sc])
= epicLet n ns 0 sc
where
epicLet x [] _ sc = epic sc
epicLet x (n:ns) i sc
= do sc' <- epicLet x ns (i+1) sc
return $ let_ (ref (ename x) !. i) (ename n, sc')
epic (STerm t) = epic t
epic (UnmatchedCase str) = return $ error_ str
epic (Case n alts) = do alts' <- mapM mkEpicAlt alts
return $ case_ (ref (ename n)) alts'
where
mkEpicAlt (ConCase n t args rhs) = do rhs' <- epic rhs
return $ con t (map ename args, rhs')
mkEpicAlt (ConstCase (I i) rhs) = do rhs' <- epic rhs
return $ constcase i rhs'
mkEpicAlt (ConstCase IType rhs) = do rhs' <- epic rhs
return $ defaultcase rhs'
mkEpicAlt (ConstCase c rhs)
= fail $ "Can only pattern match on integer constants (" ++ show c ++ ")"
mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs
return $ defaultcase rhs'
-}