{-# LANGUAGE CPP, ExistentialQuantification, PatternGuards #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module Idris.Core.Execute (execute) where
import Idris.AbsSyntax
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Error
import Idris.Primitives (Prim(..), primitives)
import IRTS.Lang (FDesc(..), FType(..))
import Util.DynamicLinker
import Util.System
import Control.Exception
import Control.Monad.Trans
import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)
import Control.Monad.Trans.State.Strict
import Data.IORef
import Data.Maybe
import Data.Time.Clock.POSIX (getPOSIXTime)
import Data.Traversable (forM)
import Debug.Trace
import System.Directory
import System.IO
import System.IO.Error
import System.IO.Unsafe
#ifdef IDRIS_FFI
import Foreign.C.String
import Foreign.LibFFI
import Foreign.Ptr
#endif
#ifndef IDRIS_FFI
execute :: Term -> Idris Term
execute tm = fail "libffi not supported, rebuild Idris with -f FFI"
#else
data Lazy = Delayed ExecEnv Context Term | Forced ExecVal deriving Int -> Lazy -> ShowS
[Lazy] -> ShowS
Lazy -> String
(Int -> Lazy -> ShowS)
-> (Lazy -> String) -> ([Lazy] -> ShowS) -> Show Lazy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Lazy -> ShowS
showsPrec :: Int -> Lazy -> ShowS
$cshow :: Lazy -> String
show :: Lazy -> String
$cshowList :: [Lazy] -> ShowS
showList :: [Lazy] -> ShowS
Show
data ExecState = ExecState { ExecState -> [DynamicLib]
exec_dynamic_libs :: [DynamicLib]
, ExecState -> [Name]
binderNames :: [Name]
}
data ExecVal = EP NameType Name ExecVal
| EV Int
| EBind Name (Binder ExecVal) (ExecVal -> Exec ExecVal)
| EApp ExecVal ExecVal
| EType UExp
| EUType Universe
| EErased
| EConstant Const
| forall a. EPtr (Ptr a)
| EThunk Context ExecEnv Term
| EHandle Handle
| EStringBuf (IORef String)
fileError :: IORef ExecVal
{-# NOINLINE fileError #-}
fileError :: IORef ExecVal
fileError = IO (IORef ExecVal) -> IORef ExecVal
forall a. IO a -> a
unsafePerformIO (IO (IORef ExecVal) -> IORef ExecVal)
-> IO (IORef ExecVal) -> IORef ExecVal
forall a b. (a -> b) -> a -> b
$ ExecVal -> IO (IORef ExecVal)
forall a. a -> IO (IORef a)
newIORef (ExecVal -> IO (IORef ExecVal)) -> ExecVal -> IO (IORef ExecVal)
forall a b. (a -> b) -> a -> b
$ ExecVal
operationNotPermitted
operationNotPermitted :: ExecVal
operationNotPermitted =
ExecVal -> ExecVal
ioWrap (ExecVal -> ExecVal) -> ExecVal -> ExecVal
forall a b. (a -> b) -> a -> b
$ ExecVal -> ExecVal
mkRaw (ExecVal -> ExecVal) -> ExecVal -> ExecVal
forall a b. (a -> b) -> a -> b
$ ExecVal -> ExecVal -> ExecVal
EApp (NameType -> Name -> ExecVal -> ExecVal
EP (Int -> Int -> Bool -> NameType
DCon Int
0 Int
1 Bool
False)
(Name -> [String] -> Name
sNS (String -> Name
sUN String
"GenericFileError") [String
"File", String
"Prelude"])
ExecVal
EErased)
(Const -> ExecVal
EConstant (Int -> Const
I Int
1))
namedFileError :: String -> ExecVal
namedFileError String
name =
ExecVal -> ExecVal
ioWrap (ExecVal -> ExecVal) -> ExecVal -> ExecVal
forall a b. (a -> b) -> a -> b
$ ExecVal -> ExecVal
mkRaw (ExecVal -> ExecVal) -> ExecVal -> ExecVal
forall a b. (a -> b) -> a -> b
$ (NameType -> Name -> ExecVal -> ExecVal
EP (Int -> Int -> Bool -> NameType
DCon Int
0 Int
0 Bool
False)
(Name -> [String] -> Name
sNS (String -> Name
sUN String
name) [String
"File", String
"Prelude"])
ExecVal
EErased)
mapError :: IOError -> ExecVal
mapError :: IOError -> ExecVal
mapError IOError
e
| (IOError -> Bool
isDoesNotExistError IOError
e) = String -> ExecVal
namedFileError String
"FileNotFound"
| (IOError -> Bool
isPermissionError IOError
e) = String -> ExecVal
namedFileError String
"PermissionDenied"
| Bool
otherwise = ExecVal
operationNotPermitted
mkRaw :: ExecVal -> ExecVal
mkRaw :: ExecVal -> ExecVal
mkRaw ExecVal
arg = ExecVal -> ExecVal -> ExecVal
EApp (ExecVal -> ExecVal -> ExecVal
EApp (NameType -> Name -> ExecVal -> ExecVal
EP (Int -> Int -> Bool -> NameType
DCon Int
0 Int
1 Bool
False) (Name -> [String] -> Name
sNS (String -> Name
sUN String
"MkRaw") [String
"FFI_C"]) ExecVal
EErased)
ExecVal
EErased) ExecVal
arg
instance Show ExecVal where
show :: ExecVal -> String
show (EP NameType
_ Name
n ExecVal
_) = Name -> String
forall a. Show a => a -> String
show Name
n
show (EV Int
i) = String
"!!V" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"!!"
show (EBind Name
n Binder ExecVal
b ExecVal -> Exec ExecVal
body) = String
"EBind " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Binder ExecVal -> String
forall a. Show a => a -> String
show Binder ExecVal
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" <<fn>>"
show (EApp ExecVal
e1 ExecVal
e2) = ExecVal -> String
forall a. Show a => a -> String
show ExecVal
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ExecVal -> String
forall a. Show a => a -> String
show ExecVal
e2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
show (EType UExp
_) = String
"Type"
show (EUType Universe
_) = String
"UType"
show ExecVal
EErased = String
"[__]"
show (EConstant Const
c) = Const -> String
forall a. Show a => a -> String
show Const
c
show (EPtr Ptr a
p) = String
"<<ptr " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Ptr a -> String
forall a. Show a => a -> String
show Ptr a
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">>"
show (EThunk Context
_ ExecEnv
env TT Name
tm) = String
"<<thunk " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ExecEnv -> String
forall a. Show a => a -> String
show ExecEnv
env String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"||||" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
tm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">>"
show (EHandle Handle
h) = String
"<<handle " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Handle -> String
forall a. Show a => a -> String
show Handle
h String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">>"
show (EStringBuf IORef String
h) = String
"<<string buffer>>"
toTT :: ExecVal -> Exec Term
toTT :: ExecVal -> Exec (TT Name)
toTT (EP NameType
nt Name
n ExecVal
ty) = (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
n) (TT Name -> TT Name) -> Exec (TT Name) -> Exec (TT Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ExecVal -> Exec (TT Name)
toTT ExecVal
ty)
toTT (EV Int
i) = TT Name -> Exec (TT Name)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Exec (TT Name)) -> TT Name -> Exec (TT Name)
forall a b. (a -> b) -> a -> b
$ Int -> TT Name
forall n. Int -> TT n
V Int
i
toTT (EBind Name
n Binder ExecVal
b ExecVal -> Exec ExecVal
body) = do Name
n' <- Name -> ExceptT Err (StateT ExecState IO) Name
forall {t :: (* -> *) -> * -> *} {m :: * -> *}.
(MonadTrans t, Monad m, Monad (t (StateT ExecState m))) =>
Name -> t (StateT ExecState m) Name
newN Name
n
ExecVal
body' <- ExecVal -> Exec ExecVal
body (ExecVal -> Exec ExecVal) -> ExecVal -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ NameType -> Name -> ExecVal -> ExecVal
EP NameType
Bound Name
n' ExecVal
EErased
Binder (TT Name)
b' <- Binder ExecVal
-> ExceptT Err (StateT ExecState IO) (Binder (TT Name))
fixBinder Binder ExecVal
b
Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' Binder (TT Name)
b' (TT Name -> TT Name) -> Exec (TT Name) -> Exec (TT Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec (TT Name)
toTT ExecVal
body'
where fixBinder :: Binder ExecVal
-> ExceptT Err (StateT ExecState IO) (Binder (TT Name))
fixBinder (Lam RigCount
rig ExecVal
t) = RigCount -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> Binder b
Lam RigCount
rig (TT Name -> Binder (TT Name))
-> Exec (TT Name)
-> ExceptT Err (StateT ExecState IO) (Binder (TT Name))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec (TT Name)
toTT ExecVal
t
fixBinder (Pi RigCount
rig Maybe ImplicitInfo
i ExecVal
t ExecVal
k) = RigCount
-> Maybe ImplicitInfo -> TT Name -> TT Name -> Binder (TT Name)
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i (TT Name -> TT Name -> Binder (TT Name))
-> Exec (TT Name)
-> ExceptT Err (StateT ExecState IO) (TT Name -> Binder (TT Name))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec (TT Name)
toTT ExecVal
t ExceptT Err (StateT ExecState IO) (TT Name -> Binder (TT Name))
-> Exec (TT Name)
-> ExceptT Err (StateT ExecState IO) (Binder (TT Name))
forall a b.
ExceptT Err (StateT ExecState IO) (a -> b)
-> ExceptT Err (StateT ExecState IO) a
-> ExceptT Err (StateT ExecState IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExecVal -> Exec (TT Name)
toTT ExecVal
k
fixBinder (Let RigCount
rig ExecVal
t1 ExecVal
t2) = RigCount -> TT Name -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig (TT Name -> TT Name -> Binder (TT Name))
-> Exec (TT Name)
-> ExceptT Err (StateT ExecState IO) (TT Name -> Binder (TT Name))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec (TT Name)
toTT ExecVal
t1 ExceptT Err (StateT ExecState IO) (TT Name -> Binder (TT Name))
-> Exec (TT Name)
-> ExceptT Err (StateT ExecState IO) (Binder (TT Name))
forall a b.
ExceptT Err (StateT ExecState IO) (a -> b)
-> ExceptT Err (StateT ExecState IO) a
-> ExceptT Err (StateT ExecState IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExecVal -> Exec (TT Name)
toTT ExecVal
t2
fixBinder (NLet ExecVal
t1 ExecVal
t2) = TT Name -> TT Name -> Binder (TT Name)
forall b. b -> b -> Binder b
NLet (TT Name -> TT Name -> Binder (TT Name))
-> Exec (TT Name)
-> ExceptT Err (StateT ExecState IO) (TT Name -> Binder (TT Name))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec (TT Name)
toTT ExecVal
t1 ExceptT Err (StateT ExecState IO) (TT Name -> Binder (TT Name))
-> Exec (TT Name)
-> ExceptT Err (StateT ExecState IO) (Binder (TT Name))
forall a b.
ExceptT Err (StateT ExecState IO) (a -> b)
-> ExceptT Err (StateT ExecState IO) a
-> ExceptT Err (StateT ExecState IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExecVal -> Exec (TT Name)
toTT ExecVal
t2
fixBinder (Hole ExecVal
t) = TT Name -> Binder (TT Name)
forall b. b -> Binder b
Hole (TT Name -> Binder (TT Name))
-> Exec (TT Name)
-> ExceptT Err (StateT ExecState IO) (Binder (TT Name))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec (TT Name)
toTT ExecVal
t
fixBinder (GHole Int
i [Name]
ns ExecVal
t) = Int -> [Name] -> TT Name -> Binder (TT Name)
forall b. Int -> [Name] -> b -> Binder b
GHole Int
i [Name]
ns (TT Name -> Binder (TT Name))
-> Exec (TT Name)
-> ExceptT Err (StateT ExecState IO) (Binder (TT Name))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec (TT Name)
toTT ExecVal
t
fixBinder (Guess ExecVal
t1 ExecVal
t2) = TT Name -> TT Name -> Binder (TT Name)
forall b. b -> b -> Binder b
Guess (TT Name -> TT Name -> Binder (TT Name))
-> Exec (TT Name)
-> ExceptT Err (StateT ExecState IO) (TT Name -> Binder (TT Name))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec (TT Name)
toTT ExecVal
t1 ExceptT Err (StateT ExecState IO) (TT Name -> Binder (TT Name))
-> Exec (TT Name)
-> ExceptT Err (StateT ExecState IO) (Binder (TT Name))
forall a b.
ExceptT Err (StateT ExecState IO) (a -> b)
-> ExceptT Err (StateT ExecState IO) a
-> ExceptT Err (StateT ExecState IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExecVal -> Exec (TT Name)
toTT ExecVal
t2
fixBinder (PVar RigCount
rig ExecVal
t) = RigCount -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> Binder b
PVar RigCount
rig (TT Name -> Binder (TT Name))
-> Exec (TT Name)
-> ExceptT Err (StateT ExecState IO) (Binder (TT Name))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec (TT Name)
toTT ExecVal
t
fixBinder (PVTy ExecVal
t) = TT Name -> Binder (TT Name)
forall b. b -> Binder b
PVTy (TT Name -> Binder (TT Name))
-> Exec (TT Name)
-> ExceptT Err (StateT ExecState IO) (Binder (TT Name))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec (TT Name)
toTT ExecVal
t
newN :: Name -> t (StateT ExecState m) Name
newN Name
n = do (ExecState [DynamicLib]
hs [Name]
ns) <- StateT ExecState m ExecState -> t (StateT ExecState m) ExecState
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift StateT ExecState m ExecState
forall (m :: * -> *) s. Monad m => StateT s m s
get
let n' :: Name
n' = Name -> [Name] -> Name
uniqueName Name
n [Name]
ns
StateT ExecState m () -> t (StateT ExecState m) ()
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExecState -> StateT ExecState m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put ([DynamicLib] -> [Name] -> ExecState
ExecState [DynamicLib]
hs (Name
n'Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
ns)))
Name -> t (StateT ExecState m) Name
forall a. a -> t (StateT ExecState m) a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n'
toTT (EApp ExecVal
e1 ExecVal
e2) = do TT Name
e1' <- ExecVal -> Exec (TT Name)
toTT ExecVal
e1
TT Name
e2' <- ExecVal -> Exec (TT Name)
toTT ExecVal
e2
TT Name -> Exec (TT Name)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Exec (TT Name)) -> TT Name -> Exec (TT Name)
forall a b. (a -> b) -> a -> b
$ AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete TT Name
e1' TT Name
e2'
toTT (EType UExp
u) = TT Name -> Exec (TT Name)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Exec (TT Name)) -> TT Name -> Exec (TT Name)
forall a b. (a -> b) -> a -> b
$ UExp -> TT Name
forall n. UExp -> TT n
TType UExp
u
toTT (EUType Universe
u) = TT Name -> Exec (TT Name)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Exec (TT Name)) -> TT Name -> Exec (TT Name)
forall a b. (a -> b) -> a -> b
$ Universe -> TT Name
forall n. Universe -> TT n
UType Universe
u
toTT ExecVal
EErased = TT Name -> Exec (TT Name)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
forall n. TT n
Erased
toTT (EConstant Const
c) = TT Name -> Exec (TT Name)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> TT Name
forall n. Const -> TT n
Constant Const
c)
toTT (EThunk Context
ctxt ExecEnv
env TT Name
tm) = do [(Name, RigCount, Binder (TT Name))]
env' <- ((Name, ExecVal)
-> ExceptT
Err (StateT ExecState IO) (Name, RigCount, Binder (TT Name)))
-> ExecEnv
-> ExceptT
Err (StateT ExecState IO) [(Name, RigCount, Binder (TT Name))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Name, ExecVal)
-> ExceptT
Err (StateT ExecState IO) (Name, RigCount, Binder (TT Name))
forall {a}.
(a, ExecVal)
-> ExceptT
Err (StateT ExecState IO) (a, RigCount, Binder (TT Name))
toBinder ExecEnv
env
TT Name -> Exec (TT Name)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Exec (TT Name)) -> TT Name -> Exec (TT Name)
forall a b. (a -> b) -> a -> b
$ Context
-> [(Name, RigCount, Binder (TT Name))] -> TT Name -> TT Name
normalise Context
ctxt [(Name, RigCount, Binder (TT Name))]
env' TT Name
tm
where toBinder :: (a, ExecVal)
-> ExceptT
Err (StateT ExecState IO) (a, RigCount, Binder (TT Name))
toBinder (a
n, ExecVal
v) = do TT Name
v' <- ExecVal -> Exec (TT Name)
toTT ExecVal
v
(a, RigCount, Binder (TT Name))
-> ExceptT
Err (StateT ExecState IO) (a, RigCount, Binder (TT Name))
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
n, RigCount
RigW, RigCount -> TT Name -> TT Name -> Binder (TT Name)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
RigW TT Name
forall n. TT n
Erased TT Name
v')
toTT (EHandle Handle
_) = Err -> Exec (TT Name)
forall a. Err -> Exec a
execFail (Err -> Exec (TT Name)) -> Err -> Exec (TT Name)
forall a b. (a -> b) -> a -> b
$ String -> Err
forall t. String -> Err' t
Msg String
"Can't convert handles back to TT after execution."
toTT (EPtr Ptr a
ptr) = Err -> Exec (TT Name)
forall a. Err -> Exec a
execFail (Err -> Exec (TT Name)) -> Err -> Exec (TT Name)
forall a b. (a -> b) -> a -> b
$ String -> Err
forall t. String -> Err' t
Msg String
"Can't convert pointers back to TT after execution."
toTT (EStringBuf IORef String
ptr) = Err -> Exec (TT Name)
forall a. Err -> Exec a
execFail (Err -> Exec (TT Name)) -> Err -> Exec (TT Name)
forall a b. (a -> b) -> a -> b
$ String -> Err
forall t. String -> Err' t
Msg String
"Can't convert string buffers back to TT after execution."
unApplyV :: ExecVal -> (ExecVal, [ExecVal])
unApplyV :: ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
tm = [ExecVal] -> ExecVal -> (ExecVal, [ExecVal])
ua [] ExecVal
tm
where ua :: [ExecVal] -> ExecVal -> (ExecVal, [ExecVal])
ua [ExecVal]
args (EApp ExecVal
f ExecVal
a) = [ExecVal] -> ExecVal -> (ExecVal, [ExecVal])
ua (ExecVal
aExecVal -> [ExecVal] -> [ExecVal]
forall a. a -> [a] -> [a]
:[ExecVal]
args) ExecVal
f
ua [ExecVal]
args ExecVal
t = (ExecVal
t, [ExecVal]
args)
mkEApp :: ExecVal -> [ExecVal] -> ExecVal
mkEApp :: ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [] = ExecVal
f
mkEApp ExecVal
f (ExecVal
a:[ExecVal]
args) = ExecVal -> [ExecVal] -> ExecVal
mkEApp (ExecVal -> ExecVal -> ExecVal
EApp ExecVal
f ExecVal
a) [ExecVal]
args
initState :: Idris ExecState
initState :: Idris ExecState
initState = do IState
ist <- Idris IState
getIState
ExecState -> Idris ExecState
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecState -> Idris ExecState) -> ExecState -> Idris ExecState
forall a b. (a -> b) -> a -> b
$ [DynamicLib] -> [Name] -> ExecState
ExecState (IState -> [DynamicLib]
idris_dynamic_libs IState
ist) []
type Exec = ExceptT Err (StateT ExecState IO)
runExec :: Exec a -> ExecState -> IO (Either Err a)
runExec :: forall a. Exec a -> ExecState -> IO (Either Err a)
runExec Exec a
ex ExecState
st = (Either Err a, ExecState) -> Either Err a
forall a b. (a, b) -> a
fst ((Either Err a, ExecState) -> Either Err a)
-> IO (Either Err a, ExecState) -> IO (Either Err a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ExecState IO (Either Err a)
-> ExecState -> IO (Either Err a, ExecState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Exec a -> StateT ExecState IO (Either Err a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT Exec a
ex) ExecState
st
getExecState :: Exec ExecState
getExecState :: Exec ExecState
getExecState = StateT ExecState IO ExecState -> Exec ExecState
forall (m :: * -> *) a. Monad m => m a -> ExceptT Err m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift StateT ExecState IO ExecState
forall (m :: * -> *) s. Monad m => StateT s m s
get
execFail :: Err -> Exec a
execFail :: forall a. Err -> Exec a
execFail = Err -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE
execIO :: IO a -> Exec a
execIO :: forall a. IO a -> Exec a
execIO = StateT ExecState IO a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => m a -> ExceptT Err m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT ExecState IO a -> ExceptT Err (StateT ExecState IO) a)
-> (IO a -> StateT ExecState IO a)
-> IO a
-> ExceptT Err (StateT ExecState IO) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> StateT ExecState IO a
forall (m :: * -> *) a. Monad m => m a -> StateT ExecState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
execute :: Term -> Idris Term
execute :: TT Name -> Idris (TT Name)
execute TT Name
tm = do ExecState
est <- Idris ExecState
initState
Context
ctxt <- Idris Context
getContext
Either Err (TT Name)
res <- ExceptT Err IO (Either Err (TT Name))
-> StateT IState (ExceptT Err IO) (Either Err (TT Name))
forall (m :: * -> *) a. Monad m => m a -> StateT IState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT Err IO (Either Err (TT Name))
-> StateT IState (ExceptT Err IO) (Either Err (TT Name)))
-> (Exec (TT Name) -> ExceptT Err IO (Either Err (TT Name)))
-> Exec (TT Name)
-> StateT IState (ExceptT Err IO) (Either Err (TT Name))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO (Either Err (TT Name)) -> ExceptT Err IO (Either Err (TT Name))
forall (m :: * -> *) a. Monad m => m a -> ExceptT Err m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Either Err (TT Name))
-> ExceptT Err IO (Either Err (TT Name)))
-> (Exec (TT Name) -> IO (Either Err (TT Name)))
-> Exec (TT Name)
-> ExceptT Err IO (Either Err (TT Name))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Exec (TT Name) -> ExecState -> IO (Either Err (TT Name)))
-> ExecState -> Exec (TT Name) -> IO (Either Err (TT Name))
forall a b c. (a -> b -> c) -> b -> a -> c
flip Exec (TT Name) -> ExecState -> IO (Either Err (TT Name))
forall a. Exec a -> ExecState -> IO (Either Err a)
runExec ExecState
est (Exec (TT Name)
-> StateT IState (ExceptT Err IO) (Either Err (TT Name)))
-> Exec (TT Name)
-> StateT IState (ExceptT Err IO) (Either Err (TT Name))
forall a b. (a -> b) -> a -> b
$
do ExecVal
res <- ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec [] Context
ctxt TT Name
tm
ExecVal -> Exec (TT Name)
toTT ExecVal
res
case Either Err (TT Name)
res of
Left Err
err -> Err -> Idris (TT Name)
forall a. Err -> Idris a
ierror Err
err
Right TT Name
tm' -> TT Name -> Idris (TT Name)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TT Name
tm'
ioWrap :: ExecVal -> ExecVal
ioWrap :: ExecVal -> ExecVal
ioWrap ExecVal
tm = ExecVal -> [ExecVal] -> ExecVal
mkEApp (NameType -> Name -> ExecVal -> ExecVal
EP (Int -> Int -> Bool -> NameType
DCon Int
0 Int
2 Bool
False) (String -> Name
sUN String
"prim__IO") ExecVal
EErased) [ExecVal
EErased, ExecVal
tm]
ioUnit :: ExecVal
ioUnit :: ExecVal
ioUnit = ExecVal -> ExecVal
ioWrap (NameType -> Name -> ExecVal -> ExecVal
EP NameType
Ref Name
unitCon ExecVal
EErased)
type ExecEnv = [(Name, ExecVal)]
doExec :: ExecEnv -> Context -> Term -> Exec ExecVal
doExec :: ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt p :: TT Name
p@(P NameType
Ref Name
n TT Name
ty) | Just ExecVal
v <- Name -> ExecEnv -> Maybe ExecVal
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n ExecEnv
env = ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
v
doExec ExecEnv
env Context
ctxt p :: TT Name
p@(P NameType
Ref Name
n TT Name
ty) =
do let val :: [Def]
val = Name -> Context -> [Def]
lookupDef Name
n Context
ctxt
case [Def]
val of
[Function TT Name
_ TT Name
tm] -> ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
tm
[TyDecl NameType
_ TT Name
_] -> ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> ExecVal -> ExecVal
EP NameType
Ref Name
n ExecVal
EErased)
[Operator TT Name
tp Int
arity [Value] -> Maybe Value
op] -> ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> ExecVal -> ExecVal
EP NameType
Ref Name
n ExecVal
EErased)
[CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ (CaseDefs ([], STerm TT Name
tm) ([Name], SC)
_)] ->
ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
tm
[CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ (CaseDefs ([Name]
ns, SC
sc) ([Name], SC)
_)] -> ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> ExecVal -> ExecVal
EP NameType
Ref Name
n ExecVal
EErased)
[] -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ String
"Could not find " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in definitions."
[Def]
other | [Def] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Def]
other Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ String
"Multiple definitions found for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
| Bool
otherwise -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Err) -> ShowS -> String -> Err
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
500 (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ String
"got to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Def] -> String
forall a. Show a => a -> String
show [Def]
other String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" lookup up " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
doExec ExecEnv
env Context
ctxt p :: TT Name
p@(P NameType
Bound Name
n TT Name
ty) =
case Name -> ExecEnv -> Maybe ExecVal
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n ExecEnv
env of
Maybe ExecVal
Nothing -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ String
"not found"
Just ExecVal
tm -> ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
tm
doExec ExecEnv
env Context
ctxt (P (DCon Int
a Int
b Bool
u) Name
n TT Name
_) = ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> ExecVal -> ExecVal
EP (Int -> Int -> Bool -> NameType
DCon Int
a Int
b Bool
u) Name
n ExecVal
EErased)
doExec ExecEnv
env Context
ctxt (P (TCon Int
a Int
b) Name
n TT Name
_) = ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> ExecVal -> ExecVal
EP (Int -> Int -> NameType
TCon Int
a Int
b) Name
n ExecVal
EErased)
doExec ExecEnv
env Context
ctxt v :: TT Name
v@(V Int
i) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< ExecEnv -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ExecEnv
env = ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Name, ExecVal) -> ExecVal
forall a b. (a, b) -> b
snd (ExecEnv
env ExecEnv -> Int -> (Name, ExecVal)
forall a. HasCallStack => [a] -> Int -> a
!! Int
i))
| Bool
otherwise = Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ String
"env too small"
doExec ExecEnv
env Context
ctxt (Bind Name
n (Let RigCount
rig TT Name
t TT Name
v) TT Name
body)
= do ExecVal
v' <- ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
v
ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ((Name
n, ExecVal
v')(Name, ExecVal) -> ExecEnv -> ExecEnv
forall a. a -> [a] -> [a]
:ExecEnv
env) Context
ctxt TT Name
body
doExec ExecEnv
env Context
ctxt (Bind Name
n (NLet TT Name
t TT Name
v) TT Name
body) = Exec ExecVal
forall a. HasCallStack => a
undefined
doExec ExecEnv
env Context
ctxt tm :: TT Name
tm@(Bind Name
n Binder (TT Name)
b TT Name
body) = do Binder ExecVal
b' <- Binder (TT Name)
-> (TT Name -> Exec ExecVal)
-> ExceptT Err (StateT ExecState IO) (Binder ExecVal)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Binder (TT Name)
b (ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt)
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> Exec ExecVal) -> ExecVal -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$
Name -> Binder ExecVal -> (ExecVal -> Exec ExecVal) -> ExecVal
EBind Name
n Binder ExecVal
b' (\ExecVal
arg -> ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ((Name
n, ExecVal
arg)(Name, ExecVal) -> ExecEnv -> ExecEnv
forall a. a -> [a] -> [a]
:ExecEnv
env) Context
ctxt TT Name
body)
doExec ExecEnv
env Context
ctxt a :: TT Name
a@(App AppStatus Name
_ TT Name
_ TT Name
_) =
do let (TT Name
f, [TT Name]
args) = TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
a
ExecVal
f' <- ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
f
[ExecVal]
args' <- case ExecVal
f' of
(EP NameType
_ Name
d ExecVal
_) | Name
d Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
delay ->
case [TT Name]
args of
[TT Name
t,TT Name
a,TT Name
tm] -> do ExecVal
t' <- ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
t
ExecVal
a' <- ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
a
[ExecVal] -> ExceptT Err (StateT ExecState IO) [ExecVal]
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [ExecVal
t', ExecVal
a', Context -> ExecEnv -> TT Name -> ExecVal
EThunk Context
ctxt ExecEnv
env TT Name
tm]
[TT Name]
_ -> (TT Name -> Exec ExecVal)
-> [TT Name] -> ExceptT Err (StateT ExecState IO) [ExecVal]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt) [TT Name]
args
ExecVal
fun' -> do (TT Name -> Exec ExecVal)
-> [TT Name] -> ExceptT Err (StateT ExecState IO) [ExecVal]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt) [TT Name]
args
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
f' [ExecVal]
args'
doExec ExecEnv
env Context
ctxt (Constant Const
c) = ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant Const
c)
doExec ExecEnv
env Context
ctxt (Proj TT Name
tm Int
i) = let (TT Name
x, [TT Name]
xs) = TT Name -> (TT Name, [TT Name])
forall n. TT n -> (TT n, [TT n])
unApply TT Name
tm in
ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt ((TT Name
xTT Name -> [TT Name] -> [TT Name]
forall a. a -> [a] -> [a]
:[TT Name]
xs) [TT Name] -> Int -> TT Name
forall a. HasCallStack => [a] -> Int -> a
!! Int
i)
doExec ExecEnv
env Context
ctxt TT Name
Erased = ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
EErased
doExec ExecEnv
env Context
ctxt TT Name
Impossible = String -> Exec ExecVal
forall a. String -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Tried to execute an impossible case"
doExec ExecEnv
env Context
ctxt (Inferred TT Name
t) = ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
t
doExec ExecEnv
env Context
ctxt (TType UExp
u) = ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UExp -> ExecVal
EType UExp
u)
doExec ExecEnv
env Context
ctxt (UType Universe
u) = ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Universe -> ExecVal
EUType Universe
u)
execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
v [] = ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
v
execApp ExecEnv
env Context
ctxt (EP NameType
_ Name
f ExecVal
_) (ExecVal
t:ExecVal
a:ExecVal
delayed:[ExecVal]
rest)
| Name
f Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
force
, (ExecVal
_, [ExecVal
_, ExecVal
_, EThunk Context
tmCtxt ExecEnv
tmEnv TT Name
tm]) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
delayed =
do ExecVal
tm' <- ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
tmEnv Context
tmCtxt TT Name
tm
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
tm' [ExecVal]
rest
execApp ExecEnv
env Context
ctxt (EP NameType
_ Name
fp ExecVal
_) (ExecVal
ty:ExecVal
action:[ExecVal]
rest)
| Name
fp Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
upio,
(ExecVal
prim__IO, [ExecVal
_, ExecVal
v]) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
action
= ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
v [ExecVal]
rest
execApp ExecEnv
env Context
ctxt (EP NameType
_ Name
fp ExecVal
_) args :: [ExecVal]
args@(ExecVal
_:ExecVal
_:ExecVal
v:ExecVal
k:[ExecVal]
rest)
| Name
fp Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
piobind,
(ExecVal
prim__IO, [ExecVal
_, ExecVal
v']) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
v =
do ExecVal
res <- ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
k [ExecVal
v']
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res [ExecVal]
rest
execApp ExecEnv
env Context
ctxt con :: ExecVal
con@(EP NameType
_ Name
fp ExecVal
_) args :: [ExecVal]
args@(ExecVal
tp:ExecVal
v:[ExecVal]
rest)
| Name
fp Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pioret = ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
con [ExecVal
tp, ExecVal
v]) [ExecVal]
rest
execApp ExecEnv
env Context
ctxt f :: ExecVal
f@(EP NameType
_ Name
fp ExecVal
_) args :: [ExecVal]
args@(ExecVal
xs:ExecVal
_:ExecVal
_:ExecVal
_:[ExecVal]
args')
| Name
fp Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
mkfprim,
(ExecVal
ty : ExecVal
fn : ExecVal
w : [ExecVal]
rest) <- [ExecVal] -> [ExecVal]
forall a. [a] -> [a]
reverse [ExecVal]
args' =
ExecEnv
-> Context
-> Int
-> ExecVal
-> ExecVal
-> [ExecVal]
-> ExecVal
-> Exec ExecVal
execForeign ExecEnv
env Context
ctxt Int
getArity ExecVal
ty ExecVal
fn [ExecVal]
rest (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args)
where getArity :: Int
getArity = case ExecVal -> Maybe [ExecVal]
unEList ExecVal
xs of
Just [ExecVal]
as -> [ExecVal] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExecVal]
as
Maybe [ExecVal]
_ -> Int
0
execApp ExecEnv
env Context
ctxt c :: ExecVal
c@(EP (DCon Int
_ Int
arity Bool
_) Name
n ExecVal
_) [ExecVal]
args =
do let args' :: [ExecVal]
args' = Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
take Int
arity [ExecVal]
args
let restArgs :: [ExecVal]
restArgs = Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
args
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
c [ExecVal]
args') [ExecVal]
restArgs
execApp ExecEnv
env Context
ctxt c :: ExecVal
c@(EP (TCon Int
_ Int
arity) Name
n ExecVal
_) [ExecVal]
args =
do let args' :: [ExecVal]
args' = Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
take Int
arity [ExecVal]
args
let restArgs :: [ExecVal]
restArgs = Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
args
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
c [ExecVal]
args') [ExecVal]
restArgs
execApp ExecEnv
env Context
ctxt f :: ExecVal
f@(EP NameType
_ Name
n ExecVal
_) [ExecVal]
args
| Just (Exec ExecVal
res, [ExecVal]
rest) <- Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])
getOp Name
n [ExecVal]
args = do ExecVal
r <- Exec ExecVal
res
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
r [ExecVal]
rest
execApp ExecEnv
env Context
ctxt f :: ExecVal
f@(EP NameType
_ Name
n ExecVal
_) [ExecVal]
args =
do let val :: [Def]
val = Name -> Context -> [Def]
lookupDef Name
n Context
ctxt
case [Def]
val of
[Function TT Name
_ TT Name
tm] -> String -> Exec ExecVal
forall a. String -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"should already have been eval'd"
[TyDecl NameType
nt TT Name
ty] -> ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> Exec ExecVal) -> ExecVal -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args
[Operator TT Name
tp Int
arity [Value] -> Maybe Value
op] ->
if [ExecVal] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExecVal]
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
arity
then let args' :: [ExecVal]
args' = Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
take Int
arity [ExecVal]
args in
case Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])
getOp Name
n [ExecVal]
args' of
Just (Exec ExecVal
res, []) -> do ExecVal
r <- Exec ExecVal
res
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
r (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
args)
Maybe (Exec ExecVal, [ExecVal])
_ -> ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args)
else ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args)
[CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ (CaseDefs ([], STerm TT Name
tm) ([Name], SC)
_)] ->
do ExecVal
rhs <- ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
tm
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
rhs [ExecVal]
args
[CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ (CaseDefs ([Name]
ns, SC
sc) ([Name], SC)
_)] ->
do Maybe ExecVal
res <- ExecEnv
-> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
execCase ExecEnv
env Context
ctxt [Name]
ns SC
sc [ExecVal]
args
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> Exec ExecVal) -> ExecVal -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ ExecVal -> Maybe ExecVal -> ExecVal
forall a. a -> Maybe a -> a
fromMaybe (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args) Maybe ExecVal
res
[Def]
thing -> ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> Exec ExecVal) -> ExecVal -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args
execApp ExecEnv
env Context
ctxt bnd :: ExecVal
bnd@(EBind Name
n Binder ExecVal
b ExecVal -> Exec ExecVal
body) (ExecVal
arg:[ExecVal]
args) = do ExecVal
ret <- ExecVal -> Exec ExecVal
body ExecVal
arg
let (ExecVal
f', [ExecVal]
as) = ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
ret
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
f' ([ExecVal]
as [ExecVal] -> [ExecVal] -> [ExecVal]
forall a. [a] -> [a] -> [a]
++ [ExecVal]
args)
execApp ExecEnv
env Context
ctxt app :: ExecVal
app@(EApp ExecVal
_ ExecVal
_) [ExecVal]
args2 | (ExecVal
f, [ExecVal]
args1) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
app = ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
f ([ExecVal]
args1 [ExecVal] -> [ExecVal] -> [ExecVal]
forall a. [a] -> [a] -> [a]
++ [ExecVal]
args2)
execApp ExecEnv
env Context
ctxt ExecVal
f [ExecVal]
args = ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args)
execForeign :: ExecEnv
-> Context
-> Int
-> ExecVal
-> ExecVal
-> [ExecVal]
-> ExecVal
-> Exec ExecVal
execForeign ExecEnv
env Context
ctxt Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs ExecVal
onfail
| Just (FFun String
"putStr" [(FDesc
_, ExecVal
str)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= case ExecVal
str of
EConstant (Str String
arg) -> do IO () -> Exec ()
forall a. IO a -> Exec a
execIO (String -> IO ()
putStr String
arg)
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
ioUnit (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
ExecVal
_ -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$
String
"The argument to putStr should be a constant string, but it was " String -> ShowS
forall a. [a] -> [a] -> [a]
++
ExecVal -> String
forall a. Show a => a -> String
show ExecVal
str String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
". Are all cases covered?"
| Just (FFun String
"putchar" [(FDesc
_, ExecVal
ch)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= case ExecVal
ch of
EConstant (Ch Char
c) -> do IO () -> Exec ()
forall a. IO a -> Exec a
execIO (Char -> IO ()
putChar Char
c)
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
ioUnit (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
EConstant (I Int
i) -> do IO () -> Exec ()
forall a. IO a -> Exec a
execIO (Char -> IO ()
putChar (Int -> Char
forall a. Enum a => Int -> a
toEnum Int
i))
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
ioUnit (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
ExecVal
_ -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$
String
"The argument to putchar should be a constant character, but it was " String -> ShowS
forall a. [a] -> [a] -> [a]
++
(Text -> String) -> String
forall a. Show a => a -> String
show Text -> String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
". Are all cases covered?"
| Just (FFun String
"idris_readStr" [(FDesc, ExecVal)
_, (FDesc
_, ExecVal
handle)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= case ExecVal
handle of
EHandle Handle
h -> do String
contents <- IO String -> Exec String
forall a. IO a -> Exec a
execIO (IO String -> Exec String) -> IO String -> Exec String
forall a b. (a -> b) -> a -> b
$ Handle -> IO String
hGetLine Handle
h
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt (Const -> ExecVal
EConstant (String -> Const
Str (String
contents String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"))) (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
ExecVal
_ -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$
String
"The argument to idris_readStr should be a handle, but it was " String -> ShowS
forall a. [a] -> [a] -> [a]
++
ExecVal -> String
forall a. Show a => a -> String
show ExecVal
handle String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
". Are all cases covered?"
| Just (FFun String
"getchar" [(FDesc, ExecVal)]
_ FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= do
ExecVal
ch <- IO ExecVal -> Exec ExecVal
forall a. IO a -> Exec a
execIO (IO ExecVal -> Exec ExecVal) -> IO ExecVal -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ (Char -> ExecVal) -> IO Char -> IO ExecVal
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ExecVal -> ExecVal
ioWrap (ExecVal -> ExecVal) -> (Char -> ExecVal) -> Char -> ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> ExecVal
EConstant (Const -> ExecVal) -> (Char -> Const) -> Char -> ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I (Int -> Const) -> (Char -> Int) -> Char -> Const
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
forall a. Enum a => a -> Int
fromEnum) IO Char
getChar
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
ch [ExecVal]
xs
| Just (FFun String
"idris_time" [(FDesc, ExecVal)]
_ FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= do IO ExecVal -> Exec ExecVal
forall a. IO a -> Exec a
execIO (IO ExecVal -> Exec ExecVal) -> IO ExecVal -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ (POSIXTime -> ExecVal) -> IO POSIXTime -> IO ExecVal
forall a b. (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ExecVal -> ExecVal
ioWrap (ExecVal -> ExecVal)
-> (POSIXTime -> ExecVal) -> POSIXTime -> ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExecVal -> ExecVal
mkRaw (ExecVal -> ExecVal)
-> (POSIXTime -> ExecVal) -> POSIXTime -> ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> ExecVal
EConstant (Const -> ExecVal) -> (POSIXTime -> Const) -> POSIXTime -> ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I (Int -> Const) -> (POSIXTime -> Int) -> POSIXTime -> Const
forall b c a. (b -> c) -> (a -> b) -> a -> c
. POSIXTime -> Int
forall b. Integral b => POSIXTime -> b
forall a b. (RealFrac a, Integral b) => a -> b
round) IO POSIXTime
getPOSIXTime
| Just (FFun String
"idris_showerror" [(FDesc, ExecVal)]
_ FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= do IO ExecVal -> Exec ExecVal
forall a. IO a -> Exec a
execIO (IO ExecVal -> Exec ExecVal) -> IO ExecVal -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ ExecVal -> IO ExecVal
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> IO ExecVal) -> ExecVal -> IO ExecVal
forall a b. (a -> b) -> a -> b
$ ExecVal -> ExecVal
ioWrap (ExecVal -> ExecVal) -> ExecVal -> ExecVal
forall a b. (a -> b) -> a -> b
$ Const -> ExecVal
EConstant (Const -> ExecVal) -> Const -> ExecVal
forall a b. (a -> b) -> a -> b
$ String -> Const
Str String
"Operation not permitted"
| Just (FFun String
"idris_mkFileError" [(FDesc, ExecVal)]
_ FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= do IO ExecVal -> Exec ExecVal
forall a. IO a -> Exec a
execIO (IO ExecVal -> Exec ExecVal) -> IO ExecVal -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ IORef ExecVal -> IO ExecVal
forall a. IORef a -> IO a
readIORef IORef ExecVal
fileError
| Just (FFun String
"fileOpen" [(FDesc
_,ExecVal
fileStr), (FDesc
_,ExecVal
modeStr)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= case (ExecVal
fileStr, ExecVal
modeStr) of
(EConstant (Str String
f), EConstant (Str String
mode)) ->
do Either String (ExecVal, [ExecVal])
f <- IO (Either String (ExecVal, [ExecVal]))
-> Exec (Either String (ExecVal, [ExecVal]))
forall a. IO a -> Exec a
execIO (IO (Either String (ExecVal, [ExecVal]))
-> Exec (Either String (ExecVal, [ExecVal])))
-> IO (Either String (ExecVal, [ExecVal]))
-> Exec (Either String (ExecVal, [ExecVal]))
forall a b. (a -> b) -> a -> b
$
IO (Either String (ExecVal, [ExecVal]))
-> (IOError -> IO (Either String (ExecVal, [ExecVal])))
-> IO (Either String (ExecVal, [ExecVal]))
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch (do let m :: Either String IOMode
m = case (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'b') String
mode of
String
"r" -> IOMode -> Either String IOMode
forall a b. b -> Either a b
Right IOMode
ReadMode
String
"w" -> IOMode -> Either String IOMode
forall a b. b -> Either a b
Right IOMode
WriteMode
String
"a" -> IOMode -> Either String IOMode
forall a b. b -> Either a b
Right IOMode
AppendMode
String
"rw" -> IOMode -> Either String IOMode
forall a b. b -> Either a b
Right IOMode
ReadWriteMode
String
"wr" -> IOMode -> Either String IOMode
forall a b. b -> Either a b
Right IOMode
ReadWriteMode
String
"r+" -> IOMode -> Either String IOMode
forall a b. b -> Either a b
Right IOMode
ReadWriteMode
String
_ -> String -> Either String IOMode
forall a b. a -> Either a b
Left (String
"Invalid mode for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
mode)
case (IOMode -> IO Handle)
-> Either String IOMode -> Either String (IO Handle)
forall a b. (a -> b) -> Either String a -> Either String b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> IOMode -> IO Handle
openFile String
f) Either String IOMode
m of
Right IO Handle
h -> do Handle
h' <- IO Handle
h
Handle -> Bool -> IO ()
hSetBinaryMode Handle
h' Bool
True
Either String (ExecVal, [ExecVal])
-> IO (Either String (ExecVal, [ExecVal]))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String (ExecVal, [ExecVal])
-> IO (Either String (ExecVal, [ExecVal])))
-> Either String (ExecVal, [ExecVal])
-> IO (Either String (ExecVal, [ExecVal]))
forall a b. (a -> b) -> a -> b
$ (ExecVal, [ExecVal]) -> Either String (ExecVal, [ExecVal])
forall a b. b -> Either a b
Right (ExecVal -> ExecVal
ioWrap (Handle -> ExecVal
EHandle Handle
h'), Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
Left String
err -> Either String (ExecVal, [ExecVal])
-> IO (Either String (ExecVal, [ExecVal]))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String (ExecVal, [ExecVal])
-> IO (Either String (ExecVal, [ExecVal])))
-> Either String (ExecVal, [ExecVal])
-> IO (Either String (ExecVal, [ExecVal]))
forall a b. (a -> b) -> a -> b
$ String -> Either String (ExecVal, [ExecVal])
forall a b. a -> Either a b
Left String
err)
(\IOError
e -> do IORef ExecVal -> ExecVal -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef ExecVal
fileError (ExecVal -> IO ()) -> ExecVal -> IO ()
forall a b. (a -> b) -> a -> b
$ IOError -> ExecVal
mapError IOError
e
Either String (ExecVal, [ExecVal])
-> IO (Either String (ExecVal, [ExecVal]))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either String (ExecVal, [ExecVal])
-> IO (Either String (ExecVal, [ExecVal])))
-> Either String (ExecVal, [ExecVal])
-> IO (Either String (ExecVal, [ExecVal]))
forall a b. (a -> b) -> a -> b
$ (ExecVal, [ExecVal]) -> Either String (ExecVal, [ExecVal])
forall a b. b -> Either a b
Right (ExecVal -> ExecVal
ioWrap (Ptr Any -> ExecVal
forall a. Ptr a -> ExecVal
EPtr Ptr Any
forall a. Ptr a
nullPtr), Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs))
case Either String (ExecVal, [ExecVal])
f of
Left String
err -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ String
err
Right (ExecVal
res, [ExecVal]
rest) -> ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res [ExecVal]
rest
(ExecVal, ExecVal)
_ -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$
String
"The arguments to fileOpen should be constant strings, but they were " String -> ShowS
forall a. [a] -> [a] -> [a]
++
ExecVal -> String
forall a. Show a => a -> String
show ExecVal
fileStr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ExecVal -> String
forall a. Show a => a -> String
show ExecVal
modeStr String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
". Are all cases covered?"
| Just (FFun String
"fileEOF" [(FDesc
_,ExecVal
handle)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= case ExecVal
handle of
EHandle Handle
h -> do Bool
eofp <- IO Bool -> Exec Bool
forall a. IO a -> Exec a
execIO (IO Bool -> Exec Bool) -> IO Bool -> Exec Bool
forall a b. (a -> b) -> a -> b
$ Handle -> IO Bool
hIsEOF Handle
h
let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap (Const -> ExecVal
EConstant (Int -> Const
I (Int -> Const) -> Int -> Const
forall a b. (a -> b) -> a -> b
$ if Bool
eofp then Int
1 else Int
0))
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
ExecVal
_ -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$
String
"The argument to fileEOF should be a file handle, but it was " String -> ShowS
forall a. [a] -> [a] -> [a]
++
ExecVal -> String
forall a. Show a => a -> String
show ExecVal
handle String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
". Are all cases covered?"
| Just (FFun String
"fileError" [(FDesc
_,ExecVal
handle)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= case ExecVal
handle of
EHandle Handle
h -> do let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap (Const -> ExecVal
EConstant (Int -> Const
I Int
0))
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
ExecVal
_ -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$
String
"The argument to fileError should be a file handle, but it was " String -> ShowS
forall a. [a] -> [a] -> [a]
++
ExecVal -> String
forall a. Show a => a -> String
show ExecVal
handle String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
". Are all cases covered?"
| Just (FFun String
"fileRemove" [(FDesc
_,ExecVal
fileStr)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= case ExecVal
fileStr of
EConstant (Str String
f) -> do ExecVal
res <- IO ExecVal -> Exec ExecVal
forall a. IO a -> Exec a
execIO (IO ExecVal -> Exec ExecVal) -> IO ExecVal -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ IO ExecVal -> (IOError -> IO ExecVal) -> IO ExecVal
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch (do String -> IO ()
removeFile String
f
ExecVal -> IO ExecVal
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> IO ExecVal) -> ExecVal -> IO ExecVal
forall a b. (a -> b) -> a -> b
$ ExecVal -> ExecVal
ioWrap (ExecVal -> ExecVal) -> ExecVal -> ExecVal
forall a b. (a -> b) -> a -> b
$ Const -> ExecVal
EConstant (Const -> ExecVal) -> Const -> ExecVal
forall a b. (a -> b) -> a -> b
$ Int -> Const
I Int
0)
(\IOError
e -> do IORef ExecVal -> ExecVal -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef ExecVal
fileError (ExecVal -> IO ()) -> ExecVal -> IO ()
forall a b. (a -> b) -> a -> b
$ IOError -> ExecVal
mapError IOError
e
ExecVal -> IO ExecVal
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> IO ExecVal) -> ExecVal -> IO ExecVal
forall a b. (a -> b) -> a -> b
$ ExecVal -> ExecVal
ioWrap (ExecVal -> ExecVal) -> ExecVal -> ExecVal
forall a b. (a -> b) -> a -> b
$ Const -> ExecVal
EConstant (Const -> ExecVal) -> Const -> ExecVal
forall a b. (a -> b) -> a -> b
$ Int -> Const
I (-Int
1))
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
ExecVal
_ -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$
String
"The argument to fileRemove should be a constant string, but it was " String -> ShowS
forall a. [a] -> [a] -> [a]
++
ExecVal -> String
forall a. Show a => a -> String
show ExecVal
fileStr String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
". Are all cases covered?"
| Just (FFun String
"fileClose" [(FDesc
_,ExecVal
handle)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= case ExecVal
handle of
EHandle Handle
h -> do IO () -> Exec ()
forall a. IO a -> Exec a
execIO (IO () -> Exec ()) -> IO () -> Exec ()
forall a b. (a -> b) -> a -> b
$ Handle -> IO ()
hClose Handle
h
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
ioUnit (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
ExecVal
_ -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$
String
"The argument to fileClose should be a file handle, but it was " String -> ShowS
forall a. [a] -> [a] -> [a]
++
ExecVal -> String
forall a. Show a => a -> String
show ExecVal
handle String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
". Are all cases covered?"
| Just (FFun String
"fileSize" [(FDesc
_,ExecVal
handle)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= case ExecVal
handle of
EHandle Handle
h -> do Integer
size <- IO Integer -> Exec Integer
forall a. IO a -> Exec a
execIO (IO Integer -> Exec Integer) -> IO Integer -> Exec Integer
forall a b. (a -> b) -> a -> b
$ Handle -> IO Integer
hFileSize Handle
h
let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap (Const -> ExecVal
EConstant (Int -> Const
I (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
size)))
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
ExecVal
_ -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$
String
"The argument to fileSize should be a file handle, but it was " String -> ShowS
forall a. [a] -> [a] -> [a]
++
ExecVal -> String
forall a. Show a => a -> String
show ExecVal
handle String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
". Are all cases covered?"
| Just (FFun String
"isNull" [(FDesc
_, ExecVal
ptr)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= case ExecVal
ptr of
EPtr Ptr a
p -> let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap (ExecVal -> ExecVal) -> (Int -> ExecVal) -> Int -> ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> ExecVal
EConstant (Const -> ExecVal) -> (Int -> Const) -> Int -> ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I (Int -> ExecVal) -> Int -> ExecVal
forall a b. (a -> b) -> a -> b
$
if Ptr a
p Ptr a -> Ptr a -> Bool
forall a. Eq a => a -> a -> Bool
== Ptr a
forall a. Ptr a
nullPtr then Int
1 else Int
0
in ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
EHandle Handle
h -> let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap (ExecVal -> ExecVal) -> (Int -> ExecVal) -> Int -> ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> ExecVal
EConstant (Const -> ExecVal) -> (Int -> Const) -> Int -> ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I (Int -> ExecVal) -> Int -> ExecVal
forall a b. (a -> b) -> a -> b
$ Int
0
in ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
EConstant (Str String
s) -> let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap (ExecVal -> ExecVal) -> (Int -> ExecVal) -> Int -> ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> ExecVal
EConstant (Const -> ExecVal) -> (Int -> Const) -> Int -> ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I (Int -> ExecVal) -> Int -> ExecVal
forall a b. (a -> b) -> a -> b
$ Int
0
in ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
ExecVal
_ -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$
String
"The argument to isNull should be a pointer or file handle or string, but it was " String -> ShowS
forall a. [a] -> [a] -> [a]
++
ExecVal -> String
forall a. Show a => a -> String
show ExecVal
ptr String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
". Are all cases covered?"
| Just (FFun String
"idris_disableBuffering" [(FDesc, ExecVal)]
_ FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= do IO () -> Exec ()
forall a. IO a -> Exec a
execIO (IO () -> Exec ()) -> IO () -> Exec ()
forall a b. (a -> b) -> a -> b
$ Handle -> BufferMode -> IO ()
hSetBuffering Handle
stdin BufferMode
NoBuffering
IO () -> Exec ()
forall a. IO a -> Exec a
execIO (IO () -> Exec ()) -> IO () -> Exec ()
forall a b. (a -> b) -> a -> b
$ Handle -> BufferMode -> IO ()
hSetBuffering Handle
stdout BufferMode
NoBuffering
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
ioUnit (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
| Just (FFun String
"idris_makeStringBuffer" [(FDesc
_, ExecVal
len)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= case ExecVal
len of
EConstant (I Int
_) -> do IORef String
buf <- IO (IORef String) -> Exec (IORef String)
forall a. IO a -> Exec a
execIO (IO (IORef String) -> Exec (IORef String))
-> IO (IORef String) -> Exec (IORef String)
forall a b. (a -> b) -> a -> b
$ String -> IO (IORef String)
forall a. a -> IO (IORef a)
newIORef String
""
let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap (IORef String -> ExecVal
EStringBuf IORef String
buf)
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
ExecVal
_ -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$
String
"The argument to idris_makeStringBuffer should be an Int, but it was " String -> ShowS
forall a. [a] -> [a] -> [a]
++
ExecVal -> String
forall a. Show a => a -> String
show ExecVal
len String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
". Are all cases covered?"
| Just (FFun String
"idris_addToString" [(FDesc
_, ExecVal
strBuf), (FDesc
_, ExecVal
str)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= case (ExecVal
strBuf, ExecVal
str) of
(EStringBuf IORef String
ref, EConstant (Str String
add)) ->
do IO () -> Exec ()
forall a. IO a -> Exec a
execIO (IO () -> Exec ()) -> IO () -> Exec ()
forall a b. (a -> b) -> a -> b
$ IORef String -> ShowS -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef String
ref (String -> ShowS
forall a. [a] -> [a] -> [a]
++String
add)
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
ioUnit (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
(ExecVal, ExecVal)
_ -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$
String
"The arguments to idris_addToString should be a StringBuffer and a String, but were " String -> ShowS
forall a. [a] -> [a] -> [a]
++
ExecVal -> String
forall a. Show a => a -> String
show ExecVal
strBuf String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ExecVal -> String
forall a. Show a => a -> String
show ExecVal
str String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
". Are all cases covered?"
| Just (FFun String
"idris_getString" [(FDesc, ExecVal)
_, (FDesc
_, ExecVal
str)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= case ExecVal
str of
EStringBuf IORef String
ref -> do String
str <- IO String -> Exec String
forall a. IO a -> Exec a
execIO (IO String -> Exec String) -> IO String -> Exec String
forall a b. (a -> b) -> a -> b
$ IORef String -> IO String
forall a. IORef a -> IO a
readIORef IORef String
ref
let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap (ExecVal -> ExecVal
mkRaw (Const -> ExecVal
EConstant (String -> Const
Str String
str)))
ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
ExecVal
_ -> Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (Err -> Exec ExecVal) -> (String -> Err) -> String -> Exec ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$
String
"The argument to idris_getString should be a StringBuffer, but it was " String -> ShowS
forall a. [a] -> [a] -> [a]
++
ExecVal -> String
forall a. Show a => a -> String
show ExecVal
str String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
". Are all cases covered?"
execForeign ExecEnv
env Context
ctxt Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs ExecVal
onfail
| Just (FFun String
"idris_numArgs" [(FDesc, ExecVal)]
_ FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
= let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap (ExecVal -> ExecVal) -> (Int -> ExecVal) -> Int -> ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> ExecVal
EConstant (Const -> ExecVal) -> (Int -> Const) -> Int -> ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I (Int -> ExecVal) -> Int -> ExecVal
forall a b. (a -> b) -> a -> b
$ Int
0
in ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
execForeign ExecEnv
env Context
ctxt Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs ExecVal
onfail
= case Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs of
Just ffun :: Foreign
ffun@(FFun String
f [(FDesc, ExecVal)]
argTs FDesc
retT) | [ExecVal] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExecVal]
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
arity ->
do let ([ExecVal]
_, [ExecVal]
xs') = (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
take Int
arity [ExecVal]
xs,
Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
Maybe ExecVal
res <- Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
call Foreign
ffun (((FDesc, ExecVal) -> ExecVal) -> [(FDesc, ExecVal)] -> [ExecVal]
forall a b. (a -> b) -> [a] -> [b]
map (FDesc, ExecVal) -> ExecVal
forall a b. (a, b) -> b
snd [(FDesc, ExecVal)]
argTs)
case Maybe ExecVal
res of
Maybe ExecVal
Nothing -> String -> Exec ExecVal
forall a. String -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ String
"Could not call foreign function \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"\" with args " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [ExecVal] -> String
forall a. Show a => a -> String
show (((FDesc, ExecVal) -> ExecVal) -> [(FDesc, ExecVal)] -> [ExecVal]
forall a b. (a -> b) -> [a] -> [b]
map (FDesc, ExecVal) -> ExecVal
forall a b. (a, b) -> b
snd [(FDesc, ExecVal)]
argTs)
Just ExecVal
r -> ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
r [ExecVal]
xs')
Maybe Foreign
_ -> ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
onfail
splitArg :: ExecVal -> Maybe (FDesc, ExecVal)
splitArg ExecVal
tm | (ExecVal
_, [ExecVal
_,ExecVal
_,ExecVal
l,ExecVal
r]) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
tm
= (FDesc, ExecVal) -> Maybe (FDesc, ExecVal)
forall a. a -> Maybe a
Just (ExecVal -> FDesc
toFDesc ExecVal
l, ExecVal
r)
splitArg ExecVal
_ = Maybe (FDesc, ExecVal)
forall a. Maybe a
Nothing
toFDesc :: ExecVal -> FDesc
toFDesc ExecVal
tm
| (EP NameType
_ Name
n ExecVal
_, []) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
tm = Name -> FDesc
FCon (Name -> Name
deNS Name
n)
| (EP NameType
_ Name
n ExecVal
_, [ExecVal]
as) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
tm = Name -> [FDesc] -> FDesc
FApp (Name -> Name
deNS Name
n) ((ExecVal -> FDesc) -> [ExecVal] -> [FDesc]
forall a b. (a -> b) -> [a] -> [b]
map ExecVal -> FDesc
toFDesc [ExecVal]
as)
toFDesc ExecVal
_ = FDesc
FUnknown
deNS :: Name -> Name
deNS (NS Name
n [Text]
_) = Name
n
deNS Name
n = Name
n
prf :: Name
prf = String -> Name
sUN String
"prim__readFile"
prc :: Name
prc = String -> Name
sUN String
"prim__readChars"
pwf :: Name
pwf = String -> Name
sUN String
"prim__writeFile"
prs :: Name
prs = String -> Name
sUN String
"prim__readString"
pws :: Name
pws = String -> Name
sUN String
"prim__writeString"
pbm :: Name
pbm = String -> Name
sUN String
"prim__believe_me"
pstdin :: Name
pstdin = String -> Name
sUN String
"prim__stdin"
pstdout :: Name
pstdout = String -> Name
sUN String
"prim__stdout"
mkfprim :: Name
mkfprim = String -> Name
sUN String
"mkForeignPrim"
pioret :: Name
pioret = String -> Name
sUN String
"prim_io_pure"
piobind :: Name
piobind = String -> Name
sUN String
"prim_io_bind"
upio :: Name
upio = String -> Name
sUN String
"unsafePerformPrimIO"
delay :: Name
delay = String -> Name
sUN String
"Delay"
force :: Name
force = String -> Name
sUN String
"Force"
getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])
getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])
getOp Name
fn (ExecVal
_ : ExecVal
_ : ExecVal
x : [ExecVal]
xs) | Name
fn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pbm = (Exec ExecVal, [ExecVal]) -> Maybe (Exec ExecVal, [ExecVal])
forall a. a -> Maybe a
Just (ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
x, [ExecVal]
xs)
getOp Name
fn (ExecVal
_ : EConstant (Str String
n) : [ExecVal]
xs)
| Name
fn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pws =
(Exec ExecVal, [ExecVal]) -> Maybe (Exec ExecVal, [ExecVal])
forall a. a -> Maybe a
Just (do IO () -> Exec ()
forall a. IO a -> Exec a
execIO (IO () -> Exec ()) -> IO () -> Exec ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr String
n IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hFlush Handle
stdout
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Int -> Const
I Int
0)), [ExecVal]
xs)
getOp Name
fn (ExecVal
_:[ExecVal]
xs)
| Name
fn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
prs =
(Exec ExecVal, [ExecVal]) -> Maybe (Exec ExecVal, [ExecVal])
forall a. a -> Maybe a
Just (do String
line <- IO String -> Exec String
forall a. IO a -> Exec a
execIO IO String
getLine
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (String -> Const
Str String
line)), [ExecVal]
xs)
getOp Name
fn (ExecVal
_ : EP NameType
_ Name
fn' ExecVal
_ : EConstant (Str String
n) : [ExecVal]
xs)
| Name
fn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pwf Bool -> Bool -> Bool
&& Name
fn' Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pstdout =
(Exec ExecVal, [ExecVal]) -> Maybe (Exec ExecVal, [ExecVal])
forall a. a -> Maybe a
Just (do IO () -> Exec ()
forall a. IO a -> Exec a
execIO (IO () -> Exec ()) -> IO () -> Exec ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr String
n IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hFlush Handle
stdout
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Int -> Const
I Int
0)), [ExecVal]
xs)
getOp Name
fn (ExecVal
_ : EP NameType
_ Name
fn' ExecVal
_ : [ExecVal]
xs)
| Name
fn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
prf Bool -> Bool -> Bool
&& Name
fn' Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pstdin =
(Exec ExecVal, [ExecVal]) -> Maybe (Exec ExecVal, [ExecVal])
forall a. a -> Maybe a
Just (do String
line <- IO String -> Exec String
forall a. IO a -> Exec a
execIO IO String
getLine
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (String -> Const
Str String
line)), [ExecVal]
xs)
getOp Name
fn (ExecVal
_ : EHandle Handle
h : EConstant (Str String
n) : [ExecVal]
xs)
| Name
fn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pwf =
(Exec ExecVal, [ExecVal]) -> Maybe (Exec ExecVal, [ExecVal])
forall a. a -> Maybe a
Just (do IO () -> Exec ()
forall a. IO a -> Exec a
execIO (IO () -> Exec ()) -> IO () -> Exec ()
forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStr Handle
h String
n IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hFlush Handle
h
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Int -> Const
I Int
0)), [ExecVal]
xs)
getOp Name
fn (ExecVal
_ : EHandle Handle
h : [ExecVal]
xs)
| Name
fn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
prf =
(Exec ExecVal, [ExecVal]) -> Maybe (Exec ExecVal, [ExecVal])
forall a. a -> Maybe a
Just (do String
contents <- IO String -> Exec String
forall a. IO a -> Exec a
execIO (IO String -> Exec String) -> IO String -> Exec String
forall a b. (a -> b) -> a -> b
$ Handle -> IO String
hGetLine Handle
h
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (String -> Const
Str (String
contents String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"))), [ExecVal]
xs)
getOp Name
fn (ExecVal
_ : EConstant (I Int
len) : EHandle Handle
h : [ExecVal]
xs)
| Name
fn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
prc =
(Exec ExecVal, [ExecVal]) -> Maybe (Exec ExecVal, [ExecVal])
forall a. a -> Maybe a
Just (do String
contents <- IO String -> Exec String
forall a. IO a -> Exec a
execIO (IO String -> Exec String) -> IO String -> Exec String
forall a b. (a -> b) -> a -> b
$ Handle -> Int -> IO String
forall {t}. (Eq t, Num t) => Handle -> t -> IO String
hGetChars Handle
h Int
len
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (String -> Const
Str String
contents)), [ExecVal]
xs)
where hGetChars :: Handle -> t -> IO String
hGetChars Handle
h t
0 = String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return String
""
hGetChars Handle
h t
i = do Bool
eof <- Handle -> IO Bool
hIsEOF Handle
h
if Bool
eof then String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return String
"" else do
Char
c <- Handle -> IO Char
hGetChar Handle
h
String
rest <- Handle -> t -> IO String
hGetChars Handle
h (t
i t -> t -> t
forall a. Num a => a -> a -> a
- t
1)
String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
c Char -> ShowS
forall a. a -> [a] -> [a]
: String
rest)
getOp Name
fn (ExecVal
_ : ExecVal
arg : [ExecVal]
xs)
| Name
fn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
prf =
(Exec ExecVal, [ExecVal]) -> Maybe (Exec ExecVal, [ExecVal])
forall a. a -> Maybe a
Just ((Exec ExecVal, [ExecVal]) -> Maybe (Exec ExecVal, [ExecVal]))
-> (Exec ExecVal, [ExecVal]) -> Maybe (Exec ExecVal, [ExecVal])
forall a b. (a -> b) -> a -> b
$ (Err -> Exec ExecVal
forall a. Err -> Exec a
execFail (String -> Err
forall t. String -> Err' t
Msg String
"Can't use prim__readFile on a raw pointer in the executor."), [ExecVal]
xs)
getOp Name
n [ExecVal]
args = do (Int
arity, [ExecVal] -> Maybe ExecVal
prim) <- Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)
getPrim Name
n [Prim]
primitives
if ([ExecVal] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExecVal]
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
arity)
then do Exec ExecVal
res <- ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
applyPrim [ExecVal] -> Maybe ExecVal
prim (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
take Int
arity [ExecVal]
args)
(Exec ExecVal, [ExecVal]) -> Maybe (Exec ExecVal, [ExecVal])
forall a. a -> Maybe a
Just (Exec ExecVal
res, Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
args)
else Maybe (Exec ExecVal, [ExecVal])
forall a. Maybe a
Nothing
where getPrim :: Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)
getPrim :: Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)
getPrim Name
n [] = Maybe (Int, [ExecVal] -> Maybe ExecVal)
forall a. Maybe a
Nothing
getPrim Name
n ((Prim Name
pn TT Name
_ Int
arity [Const] -> Maybe Const
def (Int, PrimFn)
_ Totality
_) : [Prim]
prims)
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
pn = (Int, [ExecVal] -> Maybe ExecVal)
-> Maybe (Int, [ExecVal] -> Maybe ExecVal)
forall a. a -> Maybe a
Just (Int
arity, ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
execPrim [Const] -> Maybe Const
def)
| Bool
otherwise = Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)
getPrim Name
n [Prim]
prims
execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
execPrim [Const] -> Maybe Const
f [ExecVal]
args = Const -> ExecVal
EConstant (Const -> ExecVal) -> Maybe Const -> Maybe ExecVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((ExecVal -> Maybe Const) -> [ExecVal] -> Maybe [Const]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ExecVal -> Maybe Const
getConst [ExecVal]
args Maybe [Const] -> ([Const] -> Maybe Const) -> Maybe Const
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Const] -> Maybe Const
f)
getConst :: ExecVal -> Maybe Const
getConst (EConstant Const
c) = Const -> Maybe Const
forall a. a -> Maybe a
Just Const
c
getConst ExecVal
_ = Maybe Const
forall a. Maybe a
Nothing
applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
applyPrim [ExecVal] -> Maybe ExecVal
fn [ExecVal]
args = ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> Exec ExecVal) -> Maybe ExecVal -> Maybe (Exec ExecVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExecVal] -> Maybe ExecVal
fn [ExecVal]
args
execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
execCase :: ExecEnv
-> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
execCase ExecEnv
env Context
ctxt [Name]
ns SC
sc [ExecVal]
args =
let arity :: Int
arity = [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns in
if Int
arity Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [ExecVal] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExecVal]
args
then do let amap :: ExecEnv
amap = [Name] -> [ExecVal] -> ExecEnv
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [ExecVal]
args
Maybe ExecVal
caseRes <- ExecEnv -> Context -> ExecEnv -> SC -> Exec (Maybe ExecVal)
execCase' ExecEnv
env Context
ctxt ExecEnv
amap SC
sc
case Maybe ExecVal
caseRes of
Just ExecVal
res -> ExecVal -> Maybe ExecVal
forall a. a -> Maybe a
Just (ExecVal -> Maybe ExecVal) -> Exec ExecVal -> Exec (Maybe ExecVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp (((Name, ExecVal) -> (Name, ExecVal)) -> ExecEnv -> ExecEnv
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, ExecVal
tm) -> (Name
n, ExecVal
tm)) ExecEnv
amap ExecEnv -> ExecEnv -> ExecEnv
forall a. [a] -> [a] -> [a]
++ ExecEnv
env) Context
ctxt ExecVal
res (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
args)
Maybe ExecVal
Nothing -> Maybe ExecVal -> Exec (Maybe ExecVal)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ExecVal
forall a. Maybe a
Nothing
else Maybe ExecVal -> Exec (Maybe ExecVal)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ExecVal
forall a. Maybe a
Nothing
execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
execCase' :: ExecEnv -> Context -> ExecEnv -> SC -> Exec (Maybe ExecVal)
execCase' ExecEnv
env Context
ctxt ExecEnv
amap (UnmatchedCase String
_) = Maybe ExecVal -> Exec (Maybe ExecVal)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ExecVal
forall a. Maybe a
Nothing
execCase' ExecEnv
env Context
ctxt ExecEnv
amap (STerm TT Name
tm) =
ExecVal -> Maybe ExecVal
forall a. a -> Maybe a
Just (ExecVal -> Maybe ExecVal) -> Exec ExecVal -> Exec (Maybe ExecVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec (((Name, ExecVal) -> (Name, ExecVal)) -> ExecEnv -> ExecEnv
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, ExecVal
v) -> (Name
n, ExecVal
v)) ExecEnv
amap ExecEnv -> ExecEnv -> ExecEnv
forall a. [a] -> [a] -> [a]
++ ExecEnv
env) Context
ctxt TT Name
tm
execCase' ExecEnv
env Context
ctxt ExecEnv
amap (Case CaseType
sh Name
n [CaseAlt' (TT Name)]
alts) | Just ExecVal
tm <- Name -> ExecEnv -> Maybe ExecVal
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n ExecEnv
amap =
case ExecVal -> [CaseAlt' (TT Name)] -> Maybe (SC, ExecEnv)
chooseAlt ExecVal
tm [CaseAlt' (TT Name)]
alts of
Just (SC
newCase, ExecEnv
newBindings) ->
let amap' :: ExecEnv
amap' = ExecEnv
newBindings ExecEnv -> ExecEnv -> ExecEnv
forall a. [a] -> [a] -> [a]
++ (((Name, ExecVal) -> Bool) -> ExecEnv -> ExecEnv
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
x,ExecVal
_) -> Bool -> Bool
not (Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Name
x (((Name, ExecVal) -> Name) -> ExecEnv -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, ExecVal) -> Name
forall a b. (a, b) -> a
fst ExecEnv
newBindings))) ExecEnv
amap) in
ExecEnv -> Context -> ExecEnv -> SC -> Exec (Maybe ExecVal)
execCase' ExecEnv
env Context
ctxt ExecEnv
amap' SC
newCase
Maybe (SC, ExecEnv)
Nothing -> Maybe ExecVal -> Exec (Maybe ExecVal)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ExecVal
forall a. Maybe a
Nothing
execCase' ExecEnv
_ Context
_ ExecEnv
_ SC
cse = String -> Exec (Maybe ExecVal)
forall a. String -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Exec (Maybe ExecVal)) -> String -> Exec (Maybe ExecVal)
forall a b. (a -> b) -> a -> b
$ String
"The impossible happened: tried to exec " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SC -> String
forall a. Show a => a -> String
show SC
cse
chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
chooseAlt :: ExecVal -> [CaseAlt' (TT Name)] -> Maybe (SC, ExecEnv)
chooseAlt ExecVal
tm (DefaultCase SC
sc : [CaseAlt' (TT Name)]
alts) | ExecVal -> Bool
ok ExecVal
tm = (SC, ExecEnv) -> Maybe (SC, ExecEnv)
forall a. a -> Maybe a
Just (SC
sc, [])
| Bool
otherwise = Maybe (SC, ExecEnv)
forall a. Maybe a
Nothing
where
ok :: ExecVal -> Bool
ok (EApp ExecVal
f ExecVal
x) = ExecVal -> Bool
ok ExecVal
f
ok (EP NameType
Bound Name
_ ExecVal
_) = Bool
False
ok (EP NameType
Ref Name
_ ExecVal
_) = Bool
False
ok ExecVal
_ = Bool
True
chooseAlt (EConstant Const
c) (ConstCase Const
c' SC
sc : [CaseAlt' (TT Name)]
alts) | Const
c Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
c' = (SC, ExecEnv) -> Maybe (SC, ExecEnv)
forall a. a -> Maybe a
Just (SC
sc, [])
chooseAlt ExecVal
tm (ConCase Name
n Int
i [Name]
ns SC
sc : [CaseAlt' (TT Name)]
alts) | ((EP NameType
_ Name
cn ExecVal
_), [ExecVal]
args) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
tm
, Name
cn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n = (SC, ExecEnv) -> Maybe (SC, ExecEnv)
forall a. a -> Maybe a
Just (SC
sc, [Name] -> [ExecVal] -> ExecEnv
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [ExecVal]
args)
| Bool
otherwise = ExecVal -> [CaseAlt' (TT Name)] -> Maybe (SC, ExecEnv)
chooseAlt ExecVal
tm [CaseAlt' (TT Name)]
alts
chooseAlt ExecVal
tm (CaseAlt' (TT Name)
_:[CaseAlt' (TT Name)]
alts) = ExecVal -> [CaseAlt' (TT Name)] -> Maybe (SC, ExecEnv)
chooseAlt ExecVal
tm [CaseAlt' (TT Name)]
alts
chooseAlt ExecVal
_ [] = Maybe (SC, ExecEnv)
forall a. Maybe a
Nothing
data Foreign = FFun String [(FDesc, ExecVal)] FDesc deriving Int -> Foreign -> ShowS
[Foreign] -> ShowS
Foreign -> String
(Int -> Foreign -> ShowS)
-> (Foreign -> String) -> ([Foreign] -> ShowS) -> Show Foreign
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Foreign -> ShowS
showsPrec :: Int -> Foreign -> ShowS
$cshow :: Foreign -> String
show :: Foreign -> String
$cshowList :: [Foreign] -> ShowS
showList :: [Foreign] -> ShowS
Show
toFType :: FDesc -> FType
toFType :: FDesc -> FType
toFType (FCon Name
c)
| Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_Str" = FType
FString
| Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_Float" = ArithTy -> FType
FArith ArithTy
ATFloat
| Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_Ptr" = FType
FPtr
| Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_MPtr" = FType
FManagedPtr
| Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_Unit" = FType
FUnit
toFType (FApp Name
c [FDesc
_,FDesc
ity])
| Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_IntT" = ArithTy -> FType
FArith (FDesc -> ArithTy
toAType FDesc
ity)
where toAType :: FDesc -> ArithTy
toAType (FCon Name
i)
| Name
i Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_IntChar" = IntTy -> ArithTy
ATInt IntTy
ITChar
| Name
i Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_IntNative" = IntTy -> ArithTy
ATInt IntTy
ITNative
| Name
i Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_IntBits8" = IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT8)
| Name
i Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_IntBits16" = IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT16)
| Name
i Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_IntBits32" = IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT32)
| Name
i Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_IntBits64" = IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT64)
toAType FDesc
t = String -> ArithTy
forall a. HasCallStack => String -> a
error (FDesc -> String
forall a. Show a => a -> String
show FDesc
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not defined in toAType")
toFType (FApp Name
c [FDesc
_])
| Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_Any" = FType
FAny
toFType FDesc
t = String -> FType
forall a. HasCallStack => String -> a
error (FDesc -> String
forall a. Show a => a -> String
show FDesc
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not defined in toFType")
call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
call (FFun String
name [(FDesc, ExecVal)]
argTypes FDesc
retType) [ExecVal]
args =
do Maybe ForeignFun
fn <- String -> Exec (Maybe ForeignFun)
findForeign String
name
Exec (Maybe ExecVal)
-> (ForeignFun -> Exec (Maybe ExecVal))
-> Maybe ForeignFun
-> Exec (Maybe ExecVal)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Maybe ExecVal -> Exec (Maybe ExecVal)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ExecVal
forall a. Maybe a
Nothing)
(\ForeignFun
f -> ExecVal -> Maybe ExecVal
forall a. a -> Maybe a
Just (ExecVal -> Maybe ExecVal)
-> (ExecVal -> ExecVal) -> ExecVal -> Maybe ExecVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExecVal -> ExecVal
ioWrap (ExecVal -> Maybe ExecVal) -> Exec ExecVal -> Exec (Maybe ExecVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
call' ForeignFun
f [ExecVal]
args (FDesc -> FType
toFType FDesc
retType)) Maybe ForeignFun
fn
where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
call' (Fun String
_ FunPtr a
h) [ExecVal]
args (FArith (ATInt IntTy
ITNative)) = do
CInt
res <- IO CInt -> Exec CInt
forall a. IO a -> Exec a
execIO (IO CInt -> Exec CInt) -> IO CInt -> Exec CInt
forall a b. (a -> b) -> a -> b
$ FunPtr a -> RetType CInt -> [Arg] -> IO CInt
forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CInt
retCInt ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Int -> Const
I (CInt -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral CInt
res)))
call' (Fun String
_ FunPtr a
h) [ExecVal]
args (FArith (ATInt (ITFixed NativeTy
IT8))) = do
CChar
res <- IO CChar -> Exec CChar
forall a. IO a -> Exec a
execIO (IO CChar -> Exec CChar) -> IO CChar -> Exec CChar
forall a b. (a -> b) -> a -> b
$ FunPtr a -> RetType CChar -> [Arg] -> IO CChar
forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CChar
retCChar ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Word8 -> Const
B8 (CChar -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral CChar
res)))
call' (Fun String
_ FunPtr a
h) [ExecVal]
args (FArith (ATInt (ITFixed NativeTy
IT16))) = do
CWchar
res <- IO CWchar -> Exec CWchar
forall a. IO a -> Exec a
execIO (IO CWchar -> Exec CWchar) -> IO CWchar -> Exec CWchar
forall a b. (a -> b) -> a -> b
$ FunPtr a -> RetType CWchar -> [Arg] -> IO CWchar
forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CWchar
retCWchar ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Word16 -> Const
B16 (CWchar -> Word16
forall a b. (Integral a, Num b) => a -> b
fromIntegral CWchar
res)))
call' (Fun String
_ FunPtr a
h) [ExecVal]
args (FArith (ATInt (ITFixed NativeTy
IT32))) = do
CInt
res <- IO CInt -> Exec CInt
forall a. IO a -> Exec a
execIO (IO CInt -> Exec CInt) -> IO CInt -> Exec CInt
forall a b. (a -> b) -> a -> b
$ FunPtr a -> RetType CInt -> [Arg] -> IO CInt
forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CInt
retCInt ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Word32 -> Const
B32 (CInt -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral CInt
res)))
call' (Fun String
_ FunPtr a
h) [ExecVal]
args (FArith (ATInt (ITFixed NativeTy
IT64))) = do
CLong
res <- IO CLong -> Exec CLong
forall a. IO a -> Exec a
execIO (IO CLong -> Exec CLong) -> IO CLong -> Exec CLong
forall a b. (a -> b) -> a -> b
$ FunPtr a -> RetType CLong -> [Arg] -> IO CLong
forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CLong
retCLong ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Word64 -> Const
B64 (CLong -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral CLong
res)))
call' (Fun String
_ FunPtr a
h) [ExecVal]
args (FArith ArithTy
ATFloat) = do
CDouble
res <- IO CDouble -> Exec CDouble
forall a. IO a -> Exec a
execIO (IO CDouble -> Exec CDouble) -> IO CDouble -> Exec CDouble
forall a b. (a -> b) -> a -> b
$ FunPtr a -> RetType CDouble -> [Arg] -> IO CDouble
forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CDouble
retCDouble ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Double -> Const
Fl (CDouble -> Double
forall a b. (Real a, Fractional b) => a -> b
realToFrac CDouble
res)))
call' (Fun String
_ FunPtr a
h) [ExecVal]
args (FArith (ATInt IntTy
ITChar)) = do
CChar
res <- IO CChar -> Exec CChar
forall a. IO a -> Exec a
execIO (IO CChar -> Exec CChar) -> IO CChar -> Exec CChar
forall a b. (a -> b) -> a -> b
$ FunPtr a -> RetType CChar -> [Arg] -> IO CChar
forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CChar
retCChar ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Char -> Const
Ch (CChar -> Char
castCCharToChar CChar
res)))
call' (Fun String
_ FunPtr a
h) [ExecVal]
args FType
FString = do CString
res <- IO CString -> Exec CString
forall a. IO a -> Exec a
execIO (IO CString -> Exec CString) -> IO CString -> Exec CString
forall a b. (a -> b) -> a -> b
$ FunPtr a -> RetType CString -> [Arg] -> IO CString
forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CString
retCString ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
if CString
res CString -> CString -> Bool
forall a. Eq a => a -> a -> Bool
== CString
forall a. Ptr a
nullPtr
then ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (CString -> ExecVal
forall a. Ptr a -> ExecVal
EPtr CString
res)
else do String
hStr <- IO String -> Exec String
forall a. IO a -> Exec a
execIO (IO String -> Exec String) -> IO String -> Exec String
forall a b. (a -> b) -> a -> b
$ CString -> IO String
peekCString CString
res
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (String -> Const
Str String
hStr))
call' (Fun String
_ FunPtr a
h) [ExecVal]
args FType
FPtr = Ptr () -> ExecVal
forall a. Ptr a -> ExecVal
EPtr (Ptr () -> ExecVal)
-> ExceptT Err (StateT ExecState IO) (Ptr ()) -> Exec ExecVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (IO (Ptr ()) -> ExceptT Err (StateT ExecState IO) (Ptr ())
forall a. IO a -> Exec a
execIO (IO (Ptr ()) -> ExceptT Err (StateT ExecState IO) (Ptr ()))
-> IO (Ptr ()) -> ExceptT Err (StateT ExecState IO) (Ptr ())
forall a b. (a -> b) -> a -> b
$ FunPtr a -> RetType (Ptr ()) -> [Arg] -> IO (Ptr ())
forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h (RetType () -> RetType (Ptr ())
forall a. RetType a -> RetType (Ptr a)
retPtr RetType ()
retVoid) ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args))
call' (Fun String
_ FunPtr a
h) [ExecVal]
args FType
FUnit = do ()
_ <- IO () -> Exec ()
forall a. IO a -> Exec a
execIO (IO () -> Exec ()) -> IO () -> Exec ()
forall a b. (a -> b) -> a -> b
$ FunPtr a -> RetType () -> [Arg] -> IO ()
forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType ()
retVoid ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
ExecVal -> Exec ExecVal
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> Exec ExecVal) -> ExecVal -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ NameType -> Name -> ExecVal -> ExecVal
EP NameType
Ref Name
unitCon ExecVal
EErased
call' ForeignFun
_ [ExecVal]
_ FType
_ = String -> Exec ExecVal
forall a. String -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"the impossible happened in call' in Execute.hs"
prepArgs :: [ExecVal] -> [Arg]
prepArgs = (ExecVal -> Arg) -> [ExecVal] -> [Arg]
forall a b. (a -> b) -> [a] -> [b]
map ExecVal -> Arg
prepArg
prepArg :: ExecVal -> Arg
prepArg (EConstant (I Int
i)) = CInt -> Arg
argCInt (Int -> CInt
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)
prepArg (EConstant (B8 Word8
i)) = CChar -> Arg
argCChar (Word8 -> CChar
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word8
i)
prepArg (EConstant (B16 Word16
i)) = CWchar -> Arg
argCWchar (Word16 -> CWchar
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word16
i)
prepArg (EConstant (B32 Word32
i)) = CInt -> Arg
argCInt (Word32 -> CInt
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
i)
prepArg (EConstant (B64 Word64
i)) = CLong -> Arg
argCLong (Word64 -> CLong
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i)
prepArg (EConstant (Fl Double
f)) = CDouble -> Arg
argCDouble (Double -> CDouble
forall a b. (Real a, Fractional b) => a -> b
realToFrac Double
f)
prepArg (EConstant (Ch Char
c)) = CChar -> Arg
argCChar (Char -> CChar
castCharToCChar Char
c)
prepArg (EConstant (Str String
s)) = String -> Arg
argString String
s
prepArg (EPtr Ptr a
p) = Ptr a -> Arg
forall a. Ptr a -> Arg
argPtr Ptr a
p
prepArg ExecVal
other = String -> Arg -> Arg
forall a. String -> a -> a
trace (String
"Could not use " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
100 (ExecVal -> String
forall a. Show a => a -> String
show ExecVal
other) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" as FFI arg.") Arg
forall a. HasCallStack => a
undefined
foreignFromTT :: Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT :: Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty (EConstant (Str String
name)) [ExecVal]
args
= do [(FDesc, ExecVal)]
argFTyVals <- (ExecVal -> Maybe (FDesc, ExecVal))
-> [ExecVal] -> Maybe [(FDesc, ExecVal)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ExecVal -> Maybe (FDesc, ExecVal)
splitArg (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
take Int
arity [ExecVal]
args)
Foreign -> Maybe Foreign
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Foreign -> Maybe Foreign) -> Foreign -> Maybe Foreign
forall a b. (a -> b) -> a -> b
$ String -> [(FDesc, ExecVal)] -> FDesc -> Foreign
FFun String
name [(FDesc, ExecVal)]
argFTyVals (ExecVal -> FDesc
toFDesc ExecVal
ty)
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
args = String -> Maybe Foreign -> Maybe Foreign
forall a. String -> a -> a
trace (String
"failed to construct ffun from " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (ExecVal, ExecVal, [ExecVal]) -> String
forall a. Show a => a -> String
show (ExecVal
ty,ExecVal
fn,[ExecVal]
args)) Maybe Foreign
forall a. Maybe a
Nothing
unEList :: ExecVal -> Maybe [ExecVal]
unEList :: ExecVal -> Maybe [ExecVal]
unEList ExecVal
tm = case ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
tm of
(ExecVal
nil, [ExecVal
_]) -> [ExecVal] -> Maybe [ExecVal]
forall a. a -> Maybe a
Just []
(ExecVal
cons, ([ExecVal
_, ExecVal
x, ExecVal
xs])) ->
do [ExecVal]
rest <- ExecVal -> Maybe [ExecVal]
unEList ExecVal
xs
[ExecVal] -> Maybe [ExecVal]
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ([ExecVal] -> Maybe [ExecVal]) -> [ExecVal] -> Maybe [ExecVal]
forall a b. (a -> b) -> a -> b
$ ExecVal
xExecVal -> [ExecVal] -> [ExecVal]
forall a. a -> [a] -> [a]
:[ExecVal]
rest
(ExecVal
f, [ExecVal]
args) -> Maybe [ExecVal]
forall a. Maybe a
Nothing
mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM :: forall (m :: * -> *) a b.
(Functor m, Monad m) =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM a -> m (Maybe b)
f [] = [b] -> m [b]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
mapMaybeM a -> m (Maybe b)
f (a
x:[a]
xs) = do [b]
rest <- (a -> m (Maybe b)) -> [a] -> m [b]
forall (m :: * -> *) a b.
(Functor m, Monad m) =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM a -> m (Maybe b)
f [a]
xs
[b] -> (b -> [b]) -> Maybe b -> [b]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [b]
rest (b -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
rest) (Maybe b -> [b]) -> m (Maybe b) -> m [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m (Maybe b)
f a
x
findForeign :: String -> Exec (Maybe ForeignFun)
findForeign :: String -> Exec (Maybe ForeignFun)
findForeign String
fn = do ExecState
est <- Exec ExecState
getExecState
let libs :: [DynamicLib]
libs = ExecState -> [DynamicLib]
exec_dynamic_libs ExecState
est
[ForeignFun]
fns <- (DynamicLib -> Exec (Maybe ForeignFun))
-> [DynamicLib] -> ExceptT Err (StateT ExecState IO) [ForeignFun]
forall (m :: * -> *) a b.
(Functor m, Monad m) =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM DynamicLib -> Exec (Maybe ForeignFun)
getFn [DynamicLib]
libs
case [ForeignFun]
fns of
[ForeignFun
f] -> Maybe ForeignFun -> Exec (Maybe ForeignFun)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ForeignFun -> Maybe ForeignFun
forall a. a -> Maybe a
Just ForeignFun
f)
[] -> do IO () -> Exec ()
forall a. IO a -> Exec a
execIO (IO () -> Exec ()) -> (String -> IO ()) -> String -> Exec ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Exec ()) -> String -> Exec ()
forall a b. (a -> b) -> a -> b
$ String
"Symbol \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fn String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\" not found"
Maybe ForeignFun -> Exec (Maybe ForeignFun)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ForeignFun
forall a. Maybe a
Nothing
[ForeignFun]
fs -> do IO () -> Exec ()
forall a. IO a -> Exec a
execIO (IO () -> Exec ()) -> (String -> IO ()) -> String -> Exec ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> Exec ()) -> String -> Exec ()
forall a b. (a -> b) -> a -> b
$ String
"Symbol \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fn String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\" is ambiguous. Found " String -> ShowS
forall a. [a] -> [a] -> [a]
++
Int -> String
forall a. Show a => a -> String
show ([ForeignFun] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ForeignFun]
fs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" occurrences."
Maybe ForeignFun -> Exec (Maybe ForeignFun)
forall a. a -> ExceptT Err (StateT ExecState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ForeignFun
forall a. Maybe a
Nothing
where getFn :: DynamicLib -> Exec (Maybe ForeignFun)
getFn DynamicLib
lib = IO (Maybe ForeignFun) -> Exec (Maybe ForeignFun)
forall a. IO a -> Exec a
execIO (IO (Maybe ForeignFun) -> Exec (Maybe ForeignFun))
-> IO (Maybe ForeignFun) -> Exec (Maybe ForeignFun)
forall a b. (a -> b) -> a -> b
$ IO (Maybe ForeignFun)
-> (IOError -> IO (Maybe ForeignFun)) -> IO (Maybe ForeignFun)
forall a. IO a -> (IOError -> IO a) -> IO a
catchIO (String -> DynamicLib -> IO (Maybe ForeignFun)
tryLoadFn String
fn DynamicLib
lib) (\IOError
_ -> Maybe ForeignFun -> IO (Maybe ForeignFun)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ForeignFun
forall a. Maybe a
Nothing)
#endif