{-|
Module      : Idris.Core.Execute
Description : Execute Idris code and deal with FFI.

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# 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
-- else is rest of file

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
showList :: [Lazy] -> ShowS
$cshowList :: [Lazy] -> ShowS
show :: Lazy -> String
$cshow :: Lazy -> String
showsPrec :: Int -> Lazy -> ShowS
$cshowsPrec :: Int -> Lazy -> ShowS
Show

data ExecState = ExecState { ExecState -> [DynamicLib]
exec_dynamic_libs :: [DynamicLib] -- ^ Dynamic libs from idris monad
                           , ExecState -> [Name]
binderNames :: [Name] -- ^ Used to uniquify binders when converting to TT
                           }

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 0 1 Bool
False)
                            (Name -> [String] -> Name
sNS (String -> Name
sUN "GenericFileError") ["File", "Prelude"])
                            ExecVal
EErased)
                        (Const -> ExecVal
EConstant (Int -> Const
I 1))

namedFileError :: String -> ExecVal
namedFileError name :: 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 0 0 Bool
False)
                       (Name -> [String] -> Name
sNS (String -> Name
sUN String
name) ["File", "Prelude"])
                       ExecVal
EErased)

mapError :: IOError -> ExecVal
mapError :: IOError -> ExecVal
mapError e :: IOError
e
  | (IOError -> Bool
isDoesNotExistError IOError
e) = String -> ExecVal
namedFileError "FileNotFound"
  | (IOError -> Bool
isPermissionError IOError
e)   = String -> ExecVal
namedFileError "PermissionDenied"
  | Bool
otherwise               = ExecVal
operationNotPermitted

mkRaw :: ExecVal -> ExecVal
mkRaw :: ExecVal -> ExecVal
mkRaw arg :: ExecVal
arg = ExecVal -> ExecVal -> ExecVal
EApp (ExecVal -> ExecVal -> ExecVal
EApp (NameType -> Name -> ExecVal -> ExecVal
EP (Int -> Int -> Bool -> NameType
DCon 0 1 Bool
False) (Name -> [String] -> Name
sNS (String -> Name
sUN "MkRaw") ["FFI_C"]) ExecVal
EErased)
                       ExecVal
EErased) ExecVal
arg

instance Show ExecVal where
  show :: ExecVal -> String
show (EP _ n :: Name
n _)        = Name -> String
forall a. Show a => a -> String
show Name
n
  show (EV i :: Int
i)            = "!!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]
++ "!!"
  show (EBind n :: Name
n b :: Binder ExecVal
b body :: ExecVal -> Exec ExecVal
body)  = "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]
++ " <<fn>>"
  show (EApp e1 :: ExecVal
e1 e2 :: ExecVal
e2)      = ExecVal -> String
forall a. Show a => a -> String
show ExecVal
e1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " (" 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]
++ ")"
  show (EType _)         = "Type"
  show (EUType _)        = "UType"
  show EErased           = "[__]"
  show (EConstant c :: Const
c)     = Const -> String
forall a. Show a => a -> String
show Const
c
  show (EPtr p :: Ptr a
p)          = "<<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]
++ ">>"
  show (EThunk _ env :: ExecEnv
env tm :: Term
tm) = "<<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 -> ShowS
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
tm String -> ShowS
forall a. [a] -> [a] -> [a]
++ ">>"
  show (EHandle h :: Handle
h)       = "<<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]
++ ">>"
  show (EStringBuf h :: IORef String
h)    = "<<string buffer>>"

toTT :: ExecVal -> Exec Term
toTT :: ExecVal -> Exec Term
toTT (EP nt :: NameType
nt n :: Name
n ty :: ExecVal
ty) = (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
nt Name
n) (Term -> Term) -> Exec Term -> Exec Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ExecVal -> Exec Term
toTT ExecVal
ty)
toTT (EV i :: Int
i) = Term -> Exec Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Exec Term) -> Term -> Exec Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
forall n. Int -> TT n
V Int
i
toTT (EBind n :: Name
n b :: Binder ExecVal
b body :: 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 Term
b' <- Binder ExecVal -> ExceptT Err (StateT ExecState IO) (Binder Term)
fixBinder Binder ExecVal
b
                           Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' Binder Term
b' (Term -> Term) -> Exec Term -> Exec Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec Term
toTT ExecVal
body'
    where fixBinder :: Binder ExecVal -> ExceptT Err (StateT ExecState IO) (Binder Term)
fixBinder (Lam rig :: RigCount
rig t :: ExecVal
t)    = RigCount -> Term -> Binder Term
forall b. RigCount -> b -> Binder b
Lam RigCount
rig  (Term -> Binder Term)
-> Exec Term -> ExceptT Err (StateT ExecState IO) (Binder Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec Term
toTT ExecVal
t
          fixBinder (Pi rig :: RigCount
rig i :: Maybe ImplicitInfo
i t :: ExecVal
t k :: ExecVal
k) = RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
rig Maybe ImplicitInfo
i (Term -> Term -> Binder Term)
-> Exec Term
-> ExceptT Err (StateT ExecState IO) (Term -> Binder Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec Term
toTT ExecVal
t ExceptT Err (StateT ExecState IO) (Term -> Binder Term)
-> Exec Term -> ExceptT Err (StateT ExecState IO) (Binder Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExecVal -> Exec Term
toTT ExecVal
k
          fixBinder (Let rig :: RigCount
rig t1 :: ExecVal
t1 t2 :: ExecVal
t2)   = RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rig (Term -> Term -> Binder Term)
-> Exec Term
-> ExceptT Err (StateT ExecState IO) (Term -> Binder Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec Term
toTT ExecVal
t1 ExceptT Err (StateT ExecState IO) (Term -> Binder Term)
-> Exec Term -> ExceptT Err (StateT ExecState IO) (Binder Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExecVal -> Exec Term
toTT ExecVal
t2
          fixBinder (NLet t1 :: ExecVal
t1 t2 :: ExecVal
t2)  = Term -> Term -> Binder Term
forall b. b -> b -> Binder b
NLet    (Term -> Term -> Binder Term)
-> Exec Term
-> ExceptT Err (StateT ExecState IO) (Term -> Binder Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec Term
toTT ExecVal
t1 ExceptT Err (StateT ExecState IO) (Term -> Binder Term)
-> Exec Term -> ExceptT Err (StateT ExecState IO) (Binder Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExecVal -> Exec Term
toTT ExecVal
t2
          fixBinder (Hole t :: ExecVal
t)      = Term -> Binder Term
forall b. b -> Binder b
Hole    (Term -> Binder Term)
-> Exec Term -> ExceptT Err (StateT ExecState IO) (Binder Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec Term
toTT ExecVal
t
          fixBinder (GHole i :: Int
i ns :: [Name]
ns t :: ExecVal
t) = Int -> [Name] -> Term -> Binder Term
forall b. Int -> [Name] -> b -> Binder b
GHole Int
i [Name]
ns (Term -> Binder Term)
-> Exec Term -> ExceptT Err (StateT ExecState IO) (Binder Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec Term
toTT ExecVal
t
          fixBinder (Guess t1 :: ExecVal
t1 t2 :: ExecVal
t2) = Term -> Term -> Binder Term
forall b. b -> b -> Binder b
Guess   (Term -> Term -> Binder Term)
-> Exec Term
-> ExceptT Err (StateT ExecState IO) (Term -> Binder Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec Term
toTT ExecVal
t1 ExceptT Err (StateT ExecState IO) (Term -> Binder Term)
-> Exec Term -> ExceptT Err (StateT ExecState IO) (Binder Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExecVal -> Exec Term
toTT ExecVal
t2
          fixBinder (PVar rig :: RigCount
rig t :: ExecVal
t)  = RigCount -> Term -> Binder Term
forall b. RigCount -> b -> Binder b
PVar RigCount
rig (Term -> Binder Term)
-> Exec Term -> ExceptT Err (StateT ExecState IO) (Binder Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec Term
toTT ExecVal
t
          fixBinder (PVTy t :: ExecVal
t)      = Term -> Binder Term
forall b. b -> Binder b
PVTy    (Term -> Binder Term)
-> Exec Term -> ExceptT Err (StateT ExecState IO) (Binder Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecVal -> Exec Term
toTT ExecVal
t
          newN :: Name -> t (StateT ExecState m) Name
newN n :: Name
n = do (ExecState hs :: [DynamicLib]
hs ns :: [Name]
ns) <- StateT ExecState m ExecState -> t (StateT ExecState m) ExecState
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 (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 (m :: * -> *) a. Monad m => a -> m a
return Name
n'
toTT (EApp e1 :: ExecVal
e1 e2 :: ExecVal
e2) = do Term
e1' <- ExecVal -> Exec Term
toTT ExecVal
e1
                       Term
e2' <- ExecVal -> Exec Term
toTT ExecVal
e2
                       Term -> Exec Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Exec Term) -> Term -> Exec Term
forall a b. (a -> b) -> a -> b
$ AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete Term
e1' Term
e2'
toTT (EType u :: UExp
u) = Term -> Exec Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Exec Term) -> Term -> Exec Term
forall a b. (a -> b) -> a -> b
$ UExp -> Term
forall n. UExp -> TT n
TType UExp
u
toTT (EUType u :: Universe
u) = Term -> Exec Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Exec Term) -> Term -> Exec Term
forall a b. (a -> b) -> a -> b
$ Universe -> Term
forall n. Universe -> TT n
UType Universe
u
toTT EErased = Term -> Exec Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
forall n. TT n
Erased
toTT (EConstant c :: Const
c) = Term -> Exec Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> Term
forall n. Const -> TT n
Constant Const
c)
toTT (EThunk ctxt :: Context
ctxt env :: ExecEnv
env tm :: Term
tm) = do [(Name, RigCount, Binder Term)]
env' <- ((Name, ExecVal)
 -> ExceptT Err (StateT ExecState IO) (Name, RigCount, Binder Term))
-> ExecEnv
-> ExceptT
     Err (StateT ExecState IO) [(Name, RigCount, Binder Term)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, ExecVal)
-> ExceptT Err (StateT ExecState IO) (Name, RigCount, Binder Term)
forall a.
(a, ExecVal)
-> ExceptT Err (StateT ExecState IO) (a, RigCount, Binder Term)
toBinder ExecEnv
env
                               Term -> Exec Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Exec Term) -> Term -> Exec Term
forall a b. (a -> b) -> a -> b
$ Context -> [(Name, RigCount, Binder Term)] -> Term -> Term
normalise Context
ctxt [(Name, RigCount, Binder Term)]
env' Term
tm
  where toBinder :: (a, ExecVal)
-> ExceptT Err (StateT ExecState IO) (a, RigCount, Binder Term)
toBinder (n :: a
n, v :: ExecVal
v) = do Term
v' <- ExecVal -> Exec Term
toTT ExecVal
v
                             (a, RigCount, Binder Term)
-> ExceptT Err (StateT ExecState IO) (a, RigCount, Binder Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
n, RigCount
RigW, RigCount -> Term -> Term -> Binder Term
forall b. RigCount -> b -> b -> Binder b
Let RigCount
RigW Term
forall n. TT n
Erased Term
v')
toTT (EHandle _) = Err -> Exec Term
forall a. Err -> Exec a
execFail (Err -> Exec Term) -> Err -> Exec Term
forall a b. (a -> b) -> a -> b
$ String -> Err
forall t. String -> Err' t
Msg "Can't convert handles back to TT after execution."
toTT (EPtr ptr :: Ptr a
ptr) = Err -> Exec Term
forall a. Err -> Exec a
execFail (Err -> Exec Term) -> Err -> Exec Term
forall a b. (a -> b) -> a -> b
$ String -> Err
forall t. String -> Err' t
Msg "Can't convert pointers back to TT after execution."
toTT (EStringBuf ptr :: IORef String
ptr) = Err -> Exec Term
forall a. Err -> Exec a
execFail (Err -> Exec Term) -> Err -> Exec Term
forall a b. (a -> b) -> a -> b
$ String -> Err
forall t. String -> Err' t
Msg "Can't convert string buffers back to TT after execution."

unApplyV :: ExecVal -> (ExecVal, [ExecVal])
unApplyV :: ExecVal -> (ExecVal, [ExecVal])
unApplyV tm :: ExecVal
tm = [ExecVal] -> ExecVal -> (ExecVal, [ExecVal])
ua [] ExecVal
tm
    where ua :: [ExecVal] -> ExecVal -> (ExecVal, [ExecVal])
ua args :: [ExecVal]
args (EApp f :: ExecVal
f a :: ExecVal
a) = [ExecVal] -> ExecVal -> (ExecVal, [ExecVal])
ua (ExecVal
aExecVal -> [ExecVal] -> [ExecVal]
forall a. a -> [a] -> [a]
:[ExecVal]
args) ExecVal
f
          ua args :: [ExecVal]
args t :: ExecVal
t = (ExecVal
t, [ExecVal]
args)

mkEApp :: ExecVal -> [ExecVal] -> ExecVal
mkEApp :: ExecVal -> [ExecVal] -> ExecVal
mkEApp f :: ExecVal
f [] = ExecVal
f
mkEApp f :: ExecVal
f (a :: ExecVal
a:args :: [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 (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 :: Exec a -> ExecState -> IO (Either Err a)
runExec ex :: Exec a
ex st :: 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 (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 :: Err -> Exec a
execFail = Err -> Exec a
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE

execIO :: IO a -> Exec a
execIO :: IO a -> Exec a
execIO = StateT ExecState IO a -> Exec a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT ExecState IO a -> Exec a)
-> (IO a -> StateT ExecState IO a) -> IO a -> Exec a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO a -> StateT ExecState IO a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift


execute :: Term -> Idris Term
execute :: Term -> Idris Term
execute tm :: Term
tm = do ExecState
est <- Idris ExecState
initState
                Context
ctxt <- Idris Context
getContext
                Either Err Term
res <- ExceptT Err IO (Either Err Term)
-> StateT IState (ExceptT Err IO) (Either Err Term)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ExceptT Err IO (Either Err Term)
 -> StateT IState (ExceptT Err IO) (Either Err Term))
-> (Exec Term -> ExceptT Err IO (Either Err Term))
-> Exec Term
-> StateT IState (ExceptT Err IO) (Either Err Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO (Either Err Term) -> ExceptT Err IO (Either Err Term)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Either Err Term) -> ExceptT Err IO (Either Err Term))
-> (Exec Term -> IO (Either Err Term))
-> Exec Term
-> ExceptT Err IO (Either Err Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Exec Term -> ExecState -> IO (Either Err Term))
-> ExecState -> Exec Term -> IO (Either Err Term)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Exec Term -> ExecState -> IO (Either Err Term)
forall a. Exec a -> ExecState -> IO (Either Err a)
runExec ExecState
est (Exec Term -> StateT IState (ExceptT Err IO) (Either Err Term))
-> Exec Term -> StateT IState (ExceptT Err IO) (Either Err Term)
forall a b. (a -> b) -> a -> b
$
                         do ExecVal
res <- ExecEnv -> Context -> Term -> Exec ExecVal
doExec [] Context
ctxt Term
tm
                            ExecVal -> Exec Term
toTT ExecVal
res
                case Either Err Term
res of
                  Left err :: Err
err -> Err -> Idris Term
forall a. Err -> Idris a
ierror Err
err
                  Right tm' :: Term
tm' -> Term -> Idris Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
tm'

ioWrap :: ExecVal -> ExecVal
ioWrap :: ExecVal -> ExecVal
ioWrap tm :: ExecVal
tm = ExecVal -> [ExecVal] -> ExecVal
mkEApp (NameType -> Name -> ExecVal -> ExecVal
EP (Int -> Int -> Bool -> NameType
DCon 0 2 Bool
False) (String -> Name
sUN "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 -> Term -> Exec ExecVal
doExec env :: ExecEnv
env ctxt :: Context
ctxt p :: Term
p@(P Ref n :: Name
n ty :: Term
ty) | Just v :: 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 (m :: * -> *) a. Monad m => a -> m a
return ExecVal
v
doExec env :: ExecEnv
env ctxt :: Context
ctxt p :: Term
p@(P Ref n :: Name
n ty :: Term
ty) =
    do let val :: [Def]
val = Name -> Context -> [Def]
lookupDef Name
n Context
ctxt
       case [Def]
val of
         [Function _ tm :: Term
tm] -> ExecEnv -> Context -> Term -> Exec ExecVal
doExec ExecEnv
env Context
ctxt Term
tm
         [TyDecl _ _] -> ExecVal -> Exec ExecVal
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> ExecVal -> ExecVal
EP NameType
Ref Name
n ExecVal
EErased) -- abstract def
         [Operator tp :: Term
tp arity :: Int
arity op :: [Value] -> Maybe Value
op] -> ExecVal -> Exec ExecVal
forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> ExecVal -> ExecVal
EP NameType
Ref Name
n ExecVal
EErased) -- will be special-cased later
         [CaseOp _ _ _ _ _ (CaseDefs ([], STerm tm :: Term
tm) _)] -> -- nullary fun
             ExecEnv -> Context -> Term -> Exec ExecVal
doExec ExecEnv
env Context
ctxt Term
tm
         [CaseOp _ _ _ _ _ (CaseDefs (ns :: [Name]
ns, sc :: SC
sc) _)] -> ExecVal -> Exec ExecVal
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
$ "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]
++ " in definitions."
         other :: [Def]
other | [Def] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Def]
other Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 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
$ "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 500 (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ "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]
++ " lookup up " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
doExec env :: ExecEnv
env ctxt :: Context
ctxt p :: Term
p@(P Bound n :: Name
n ty :: Term
ty) =
  case Name -> ExecEnv -> Maybe ExecVal
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n ExecEnv
env of
    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
$ "not found"
    Just tm :: ExecVal
tm -> ExecVal -> Exec ExecVal
forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
tm
doExec env :: ExecEnv
env ctxt :: Context
ctxt (P (DCon a :: Int
a b :: Int
b u :: Bool
u) n :: Name
n _) = ExecVal -> Exec ExecVal
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 env :: ExecEnv
env ctxt :: Context
ctxt (P (TCon a :: Int
a b :: Int
b) n :: Name
n _) = ExecVal -> Exec ExecVal
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 env :: ExecEnv
env ctxt :: Context
ctxt v :: Term
v@(V i :: Int
i) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< ExecEnv -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ExecEnv
env = ExecVal -> Exec ExecVal
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. [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
$ "env too small"
doExec env :: ExecEnv
env ctxt :: Context
ctxt (Bind n :: Name
n (Let rig :: RigCount
rig t :: Term
t v :: Term
v) body :: Term
body)
     = do ExecVal
v' <- ExecEnv -> Context -> Term -> Exec ExecVal
doExec ExecEnv
env Context
ctxt Term
v
          ExecEnv -> Context -> Term -> Exec ExecVal
doExec ((Name
n, ExecVal
v')(Name, ExecVal) -> ExecEnv -> ExecEnv
forall a. a -> [a] -> [a]
:ExecEnv
env) Context
ctxt Term
body
doExec env :: ExecEnv
env ctxt :: Context
ctxt (Bind n :: Name
n (NLet t :: Term
t v :: Term
v) body :: Term
body) = Exec ExecVal
forall a. HasCallStack => a
undefined
doExec env :: ExecEnv
env ctxt :: Context
ctxt tm :: Term
tm@(Bind n :: Name
n b :: Binder Term
b body :: Term
body) = do Binder ExecVal
b' <- Binder Term
-> (Term -> 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 Term
b (ExecEnv -> Context -> Term -> Exec ExecVal
doExec ExecEnv
env Context
ctxt)
                                        ExecVal -> Exec ExecVal
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' (\arg :: ExecVal
arg -> ExecEnv -> Context -> Term -> Exec ExecVal
doExec ((Name
n, ExecVal
arg)(Name, ExecVal) -> ExecEnv -> ExecEnv
forall a. a -> [a] -> [a]
:ExecEnv
env) Context
ctxt Term
body)
doExec env :: ExecEnv
env ctxt :: Context
ctxt a :: Term
a@(App _ _ _) =
  do let (f :: Term
f, args :: [Term]
args) = Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
a
     ExecVal
f' <- ExecEnv -> Context -> Term -> Exec ExecVal
doExec ExecEnv
env Context
ctxt Term
f
     [ExecVal]
args' <- case ExecVal
f' of
                (EP _ d :: Name
d _) | Name
d Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
delay ->
                  case [Term]
args of
                    [t :: Term
t,a :: Term
a,tm :: Term
tm] -> do ExecVal
t' <- ExecEnv -> Context -> Term -> Exec ExecVal
doExec ExecEnv
env Context
ctxt Term
t
                                   ExecVal
a' <- ExecEnv -> Context -> Term -> Exec ExecVal
doExec ExecEnv
env Context
ctxt Term
a
                                   [ExecVal] -> ExceptT Err (StateT ExecState IO) [ExecVal]
forall (m :: * -> *) a. Monad m => a -> m a
return [ExecVal
t', ExecVal
a', Context -> ExecEnv -> Term -> ExecVal
EThunk Context
ctxt ExecEnv
env Term
tm]
                    _ -> (Term -> Exec ExecVal)
-> [Term] -> ExceptT Err (StateT ExecState IO) [ExecVal]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ExecEnv -> Context -> Term -> Exec ExecVal
doExec ExecEnv
env Context
ctxt) [Term]
args -- partial applications are fine to evaluate
                fun' :: ExecVal
fun' -> do (Term -> Exec ExecVal)
-> [Term] -> ExceptT Err (StateT ExecState IO) [ExecVal]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ExecEnv -> Context -> Term -> Exec ExecVal
doExec ExecEnv
env Context
ctxt) [Term]
args
     ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
f' [ExecVal]
args'
doExec env :: ExecEnv
env ctxt :: Context
ctxt (Constant c :: Const
c) = ExecVal -> Exec ExecVal
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant Const
c)
doExec env :: ExecEnv
env ctxt :: Context
ctxt (Proj tm :: Term
tm i :: Int
i) = let (x :: Term
x, xs :: [Term]
xs) = Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm in
                              ExecEnv -> Context -> Term -> Exec ExecVal
doExec ExecEnv
env Context
ctxt ((Term
xTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
xs) [Term] -> Int -> Term
forall a. [a] -> Int -> a
!! Int
i)
doExec env :: ExecEnv
env ctxt :: Context
ctxt Erased = ExecVal -> Exec ExecVal
forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
EErased
doExec env :: ExecEnv
env ctxt :: Context
ctxt Impossible = String -> Exec ExecVal
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "Tried to execute an impossible case"
doExec env :: ExecEnv
env ctxt :: Context
ctxt (Inferred t :: Term
t) = ExecEnv -> Context -> Term -> Exec ExecVal
doExec ExecEnv
env Context
ctxt Term
t
doExec env :: ExecEnv
env ctxt :: Context
ctxt (TType u :: UExp
u) = ExecVal -> Exec ExecVal
forall (m :: * -> *) a. Monad m => a -> m a
return (UExp -> ExecVal
EType UExp
u)
doExec env :: ExecEnv
env ctxt :: Context
ctxt (UType u :: Universe
u) = ExecVal -> Exec ExecVal
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 env :: ExecEnv
env ctxt :: Context
ctxt v :: ExecVal
v [] = ExecVal -> Exec ExecVal
forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
v -- no args is just a constant! can result from function calls
execApp env :: ExecEnv
env ctxt :: Context
ctxt (EP _ f :: Name
f _) (t :: ExecVal
t:a :: ExecVal
a:delayed :: ExecVal
delayed:rest :: [ExecVal]
rest)
  | Name
f Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
force
  , (_, [_, _, EThunk tmCtxt :: Context
tmCtxt tmEnv :: ExecEnv
tmEnv tm :: Term
tm]) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
delayed =
    do ExecVal
tm' <- ExecEnv -> Context -> Term -> Exec ExecVal
doExec ExecEnv
tmEnv Context
tmCtxt Term
tm
       ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
tm' [ExecVal]
rest
execApp env :: ExecEnv
env ctxt :: Context
ctxt (EP _ fp :: Name
fp _) (ty :: ExecVal
ty:action :: ExecVal
action:rest :: [ExecVal]
rest)
  | Name
fp Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
upio,
    (prim__IO :: ExecVal
prim__IO, [_, v :: ExecVal
v]) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
action
       = ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
v [ExecVal]
rest

execApp env :: ExecEnv
env ctxt :: Context
ctxt (EP _ fp :: Name
fp _) args :: [ExecVal]
args@(_:_:v :: ExecVal
v:k :: ExecVal
k:rest :: [ExecVal]
rest)
  | Name
fp Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
piobind,
    (prim__IO :: ExecVal
prim__IO, [_, v' :: 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 env :: ExecEnv
env ctxt :: Context
ctxt con :: ExecVal
con@(EP _ fp :: Name
fp _) args :: [ExecVal]
args@(tp :: ExecVal
tp:v :: ExecVal
v:rest :: [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

-- Special cases arising from not having access to the C RTS in the interpreter
execApp env :: ExecEnv
env ctxt :: Context
ctxt f :: ExecVal
f@(EP _ fp :: Name
fp _) args :: [ExecVal]
args@(xs :: ExecVal
xs:_:_:_:args' :: [ExecVal]
args')
    | Name
fp Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
mkfprim,
      (ty :: ExecVal
ty : fn :: ExecVal
fn : w :: ExecVal
w : rest :: [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 as :: [ExecVal]
as -> [ExecVal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExecVal]
as
                        _ -> 0

execApp env :: ExecEnv
env ctxt :: Context
ctxt c :: ExecVal
c@(EP (DCon _ arity :: Int
arity _) n :: Name
n _) args :: [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 env :: ExecEnv
env ctxt :: Context
ctxt c :: ExecVal
c@(EP (TCon _ arity :: Int
arity) n :: Name
n _) args :: [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 env :: ExecEnv
env ctxt :: Context
ctxt f :: ExecVal
f@(EP _ n :: Name
n _) args :: [ExecVal]
args
    | Just (res :: Exec ExecVal
res, rest :: [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 env :: ExecEnv
env ctxt :: Context
ctxt f :: ExecVal
f@(EP _ n :: Name
n _) args :: [ExecVal]
args =
    do let val :: [Def]
val = Name -> Context -> [Def]
lookupDef Name
n Context
ctxt
       case [Def]
val of
         [Function _ tm :: Term
tm] -> String -> Exec ExecVal
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "should already have been eval'd"
         [TyDecl nt :: NameType
nt ty :: Term
ty] -> ExecVal -> Exec ExecVal
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 tp :: Term
tp arity :: Int
arity op :: [Value] -> Maybe Value
op] ->
             if [ExecVal] -> 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 (res :: 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)
                      _ -> ExecVal -> Exec ExecVal
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args)
               else ExecVal -> Exec ExecVal
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args)
         [CaseOp _ _ _ _ _ (CaseDefs ([], STerm tm :: Term
tm) _)] -> -- nullary fun
             do ExecVal
rhs <- ExecEnv -> Context -> Term -> Exec ExecVal
doExec ExecEnv
env Context
ctxt Term
tm
                ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
rhs [ExecVal]
args
         [CaseOp _ _ _ _ _ (CaseDefs (ns :: [Name]
ns, sc :: SC
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 (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
         thing :: [Def]
thing -> ExecVal -> Exec ExecVal
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 env :: ExecEnv
env ctxt :: Context
ctxt bnd :: ExecVal
bnd@(EBind n :: Name
n b :: Binder ExecVal
b body :: ExecVal -> Exec ExecVal
body) (arg :: ExecVal
arg:args :: [ExecVal]
args) = do ExecVal
ret <- ExecVal -> Exec ExecVal
body ExecVal
arg
                                                      let (f' :: ExecVal
f', as :: [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 env :: ExecEnv
env ctxt :: Context
ctxt app :: ExecVal
app@(EApp _ _) args2 :: [ExecVal]
args2 | (f :: ExecVal
f, args1 :: [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 env :: ExecEnv
env ctxt :: Context
ctxt f :: ExecVal
f args :: [ExecVal]
args = ExecVal -> Exec ExecVal
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 env :: ExecEnv
env ctxt :: Context
ctxt arity :: Int
arity ty :: ExecVal
ty fn :: ExecVal
fn xs :: [ExecVal]
xs onfail :: ExecVal
onfail
    | Just (FFun "putStr" [(_, str :: ExecVal
str)] _) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
       = case ExecVal
str of
           EConstant (Str arg :: 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)
           _ -> 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
$
                  "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]
++
                  ". Are all cases covered?"
    | Just (FFun "putchar" [(_, ch :: ExecVal
ch)] _) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
ch of
               EConstant (Ch c :: 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 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)
               _ -> 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
$
                      "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]
++
                      ". Are all cases covered?"
    | Just (FFun "idris_readStr" [_, (_, handle :: ExecVal
handle)] _) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
handle of
               EHandle h :: 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]
++ "\n"))) (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
               _ -> 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
$
                      "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]
++
                      ". Are all cases covered?"
    | Just (FFun "getchar" _ _) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = do -- The C API returns an Int which Idris library code
                -- converts; thus, we must make an int here.
                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 (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 "idris_time" _ _) <- 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 (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 a b. (RealFrac a, Integral b) => a -> b
round) IO POSIXTime
getPOSIXTime
    | Just (FFun "idris_showerror" _ _) <- 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 (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 "Operation not permitted"
    | Just (FFun "idris_mkFileError" _ _) <- 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 "fileOpen" [(_,fileStr :: ExecVal
fileStr), (_,modeStr :: ExecVal
modeStr)] _) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case (ExecVal
fileStr, ExecVal
modeStr) of
               (EConstant (Str f :: String
f), EConstant (Str mode :: 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
/= 'b') String
mode of
                                             "r"  -> IOMode -> Either String IOMode
forall a b. b -> Either a b
Right IOMode
ReadMode
                                             "w"  -> IOMode -> Either String IOMode
forall a b. b -> Either a b
Right IOMode
WriteMode
                                             "a"  -> IOMode -> Either String IOMode
forall a b. b -> Either a b
Right IOMode
AppendMode
                                             "rw" -> IOMode -> Either String IOMode
forall a b. b -> Either a b
Right IOMode
ReadWriteMode
                                             "wr" -> IOMode -> Either String IOMode
forall a b. b -> Either a b
Right IOMode
ReadWriteMode
                                             "r+" -> IOMode -> Either String IOMode
forall a b. b -> Either a b
Right IOMode
ReadWriteMode
                                             _    -> String -> Either String IOMode
forall a b. a -> Either a b
Left ("Invalid mode for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ ": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
mode)
                                   case (IOMode -> IO Handle)
-> Either String IOMode -> Either String (IO Handle)
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 h :: 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 (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 err :: String
err -> Either String (ExecVal, [ExecVal])
-> IO (Either String (ExecVal, [ExecVal]))
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)
                               (\e :: 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 (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 err :: 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 (res :: ExecVal
res, rest :: [ExecVal]
rest) -> ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res [ExecVal]
rest
               _ -> 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
$
                      "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]
++ " 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]
++
                      ". Are all cases covered?"
    | Just (FFun "fileEOF" [(_,handle :: ExecVal
handle)] _) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
handle of
               EHandle h :: 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 1 else 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)
               _ -> 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
$
                      "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]
++
                      ". Are all cases covered?"
    | Just (FFun "fileError" [(_,handle :: ExecVal
handle)] _) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
handle of
             -- errors handled differently in Haskell than in C, so if
             -- there's been an error we'll have had an exception already.
             -- Therefore, assume we're okay.
               EHandle h :: Handle
h -> do let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap (Const -> ExecVal
EConstant (Int -> Const
I 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)
               _ -> 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
$
                      "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]
++
                      ". Are all cases covered?"
    | Just (FFun "fileRemove" [(_,fileStr :: ExecVal
fileStr)] _) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
fileStr of
               EConstant (Str f :: 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 (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 0)
                                                             (\e :: 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 (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 (-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)
               _ -> 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
$
                      "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]
++
                      ". Are all cases covered?"
    | Just (FFun "fileClose" [(_,handle :: ExecVal
handle)] _) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
handle of
               EHandle h :: 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)
               _ -> 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
$
                      "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]
++
                      ". Are all cases covered?"
    | Just (FFun "fileSize" [(_,handle :: ExecVal
handle)] _) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
handle of
               EHandle h :: 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)
               _ -> 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
$
                      "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]
++
                      ". Are all cases covered?"

    | Just (FFun "isNull" [(_, ptr :: ExecVal
ptr)] _) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
ptr of
               EPtr p :: 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 1 else 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)
               -- Handles will be checked as null pointers sometimes - but if we got a
               -- real Handle, then it's valid, so just return 1.
               EHandle h :: 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
$ 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)
               -- A foreign-returned char* has to be tested for NULL sometimes
               EConstant (Str s :: 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
$ 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)
               _ -> 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
$
                      "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]
++
                      ". Are all cases covered?"

    | Just (FFun "idris_disableBuffering" _ _) <- 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 use a Haskell String in an IORef for a string buffer
    | Just (FFun "idris_makeStringBuffer" [(_, len :: ExecVal
len)] _) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
       = case ExecVal
len of
              EConstant (I _) -> 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 ""
                                    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)

              _ -> 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
$
                      "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]
++
                      ". Are all cases covered?"
    | Just (FFun "idris_addToString" [(_, strBuf :: ExecVal
strBuf), (_, str :: ExecVal
str)] _) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
       = case (ExecVal
strBuf, ExecVal
str) of
              (EStringBuf ref :: IORef String
ref, EConstant (Str add :: 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)
              _ -> 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
$
                      "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]
++ " 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]
++
                      ". Are all cases covered?"
    | Just (FFun "idris_getString" [_, (_, str :: ExecVal
str)] _) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
       = case ExecVal
str of
              EStringBuf ref :: 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)
              _ -> 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
$
                      "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]
++
                      ". Are all cases covered?"



-- Right now, there's no way to send command-line arguments to the executor,
-- so just return 0.
execForeign env :: ExecEnv
env ctxt :: Context
ctxt arity :: Int
arity ty :: ExecVal
ty fn :: ExecVal
fn xs :: [ExecVal]
xs onfail :: ExecVal
onfail
    | Just (FFun "idris_numArgs" _ _) <- 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
$ 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 env :: ExecEnv
env ctxt :: Context
ctxt arity :: Int
arity ty :: ExecVal
ty fn :: ExecVal
fn xs :: [ExecVal]
xs onfail :: ExecVal
onfail
   = case Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs of
        Just ffun :: Foreign
ffun@(FFun f :: String
f argTs :: [(FDesc, ExecVal)]
argTs retT :: FDesc
retT) | [ExecVal] -> 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 (_, xs' :: [ExecVal]
xs') = (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
take Int
arity [ExecVal]
xs, -- foreign args
                              Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs) -- rest
              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
                   Nothing -> String -> Exec ExecVal
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Exec ExecVal) -> String -> Exec ExecVal
forall a b. (a -> b) -> a -> b
$ "Could not call foreign function \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                     "\" 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 r :: ExecVal
r -> ExecVal -> Exec ExecVal
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
r [ExecVal]
xs')
        _ -> ExecVal -> Exec ExecVal
forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
onfail


splitArg :: ExecVal -> Maybe (FDesc, ExecVal)
splitArg tm :: ExecVal
tm | (_, [_,_,l :: ExecVal
l,r :: ExecVal
r]) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
tm -- pair, two implicits
    = (FDesc, ExecVal) -> Maybe (FDesc, ExecVal)
forall a. a -> Maybe a
Just (ExecVal -> FDesc
toFDesc ExecVal
l, ExecVal
r)
splitArg _ = Maybe (FDesc, ExecVal)
forall a. Maybe a
Nothing

toFDesc :: ExecVal -> FDesc
toFDesc tm :: ExecVal
tm
   | (EP _ n :: Name
n _, []) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
tm = Name -> FDesc
FCon (Name -> Name
deNS Name
n)
   | (EP _ n :: Name
n _, as :: [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 _ = FDesc
FUnknown

deNS :: Name -> Name
deNS (NS n :: Name
n _) = Name
n
deNS n :: Name
n = Name
n

prf :: Name
prf = String -> Name
sUN "prim__readFile"
prc :: Name
prc = String -> Name
sUN "prim__readChars"
pwf :: Name
pwf = String -> Name
sUN "prim__writeFile"
prs :: Name
prs = String -> Name
sUN "prim__readString"
pws :: Name
pws = String -> Name
sUN "prim__writeString"
pbm :: Name
pbm = String -> Name
sUN "prim__believe_me"
pstdin :: Name
pstdin = String -> Name
sUN "prim__stdin"
pstdout :: Name
pstdout = String -> Name
sUN "prim__stdout"
mkfprim :: Name
mkfprim = String -> Name
sUN "mkForeignPrim"
pioret :: Name
pioret = String -> Name
sUN "prim_io_pure"
piobind :: Name
piobind = String -> Name
sUN "prim_io_bind"
upio :: Name
upio = String -> Name
sUN "unsafePerformPrimIO"
delay :: Name
delay = String -> Name
sUN "Delay"
force :: Name
force = String -> Name
sUN "Force"

-- | Look up primitive operations in the global table and transform
-- them into ExecVal functions
getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])
getOp :: Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])
getOp fn :: Name
fn (_ : _ : x :: ExecVal
x : xs :: [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 (m :: * -> *) a. Monad m => a -> m a
return ExecVal
x, [ExecVal]
xs)
getOp fn :: Name
fn (_ : EConstant (Str n :: String
n) : xs :: [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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hFlush Handle
stdout
                       ExecVal -> Exec ExecVal
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Int -> Const
I 0)), [ExecVal]
xs)
getOp fn :: Name
fn (_:xs :: [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 (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (String -> Const
Str String
line)), [ExecVal]
xs)
getOp fn :: Name
fn (_ : EP _ fn' :: Name
fn' _ : EConstant (Str n :: String
n) : xs :: [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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hFlush Handle
stdout
                       ExecVal -> Exec ExecVal
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Int -> Const
I 0)), [ExecVal]
xs)
getOp fn :: Name
fn (_ : EP _ fn' :: Name
fn' _ : xs :: [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 (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (String -> Const
Str String
line)), [ExecVal]
xs)
getOp fn :: Name
fn (_ : EHandle h :: Handle
h : EConstant (Str n :: String
n) : xs :: [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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hFlush Handle
h
                       ExecVal -> Exec ExecVal
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Int -> Const
I 0)), [ExecVal]
xs)
getOp fn :: Name
fn (_ : EHandle h :: Handle
h : xs :: [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 (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (String -> Const
Str (String
contents String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n"))), [ExecVal]
xs)
getOp fn :: Name
fn (_ : EConstant (I len :: Int
len) : EHandle h :: Handle
h : xs :: [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 (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 h :: Handle
h 0 = String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return ""
        hGetChars h :: Handle
h i :: t
i = do Bool
eof <- Handle -> IO Bool
hIsEOF Handle
h
                           if Bool
eof then String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return "" 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
- 1)
                             String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
c Char -> ShowS
forall a. a -> [a] -> [a]
: String
rest)
getOp fn :: Name
fn (_ : arg :: ExecVal
arg : xs :: [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 "Can't use prim__readFile on a raw pointer in the executor."), [ExecVal]
xs)
getOp n :: Name
n args :: [ExecVal]
args = do (arity :: Int
arity, prim :: [ExecVal] -> Maybe ExecVal
prim) <- Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)
getPrim Name
n [Prim]
primitives
                  if ([ExecVal] -> 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 n :: Name
n [] = Maybe (Int, [ExecVal] -> Maybe ExecVal)
forall a. Maybe a
Nothing
          getPrim n :: Name
n ((Prim pn :: Name
pn _ arity :: Int
arity def :: [Const] -> Maybe Const
def _ _) : prims :: [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 f :: [Const] -> Maybe Const
f args :: [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)
mapM ExecVal -> Maybe Const
getConst [ExecVal]
args Maybe [Const] -> ([Const] -> Maybe Const) -> Maybe Const
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Const] -> Maybe Const
f)

          getConst :: ExecVal -> Maybe Const
getConst (EConstant c :: Const
c) = Const -> Maybe Const
forall a. a -> Maybe a
Just Const
c
          getConst _             = Maybe Const
forall a. Maybe a
Nothing

          applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
          applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
applyPrim fn :: [ExecVal] -> Maybe ExecVal
fn args :: [ExecVal]
args = ExecVal -> Exec ExecVal
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




-- | Overall wrapper for case tree execution. If there are enough arguments, it takes them,
-- evaluates them, then begins the checks for matching cases.
execCase :: ExecEnv -> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
execCase :: ExecEnv
-> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
execCase env :: ExecEnv
env ctxt :: Context
ctxt ns :: [Name]
ns sc :: SC
sc args :: [ExecVal]
args =
    let arity :: Int
arity = [Name] -> 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 (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
--            trace ("Case " ++ show sc ++ "\n   in " ++ show amap ++"\n   in env " ++ show env ++ "\n\n" ) $ return ()
            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 res :: 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 (\(n :: Name
n, tm :: 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)
              Nothing -> Maybe ExecVal -> Exec (Maybe ExecVal)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ExecVal
forall a. Maybe a
Nothing
    else Maybe ExecVal -> Exec (Maybe ExecVal)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ExecVal
forall a. Maybe a
Nothing

-- | Take bindings and a case tree and examines them, executing the matching case if possible.
execCase' :: ExecEnv -> Context -> [(Name, ExecVal)] -> SC -> Exec (Maybe ExecVal)
execCase' :: ExecEnv -> Context -> ExecEnv -> SC -> Exec (Maybe ExecVal)
execCase' env :: ExecEnv
env ctxt :: Context
ctxt amap :: ExecEnv
amap (UnmatchedCase _) = Maybe ExecVal -> Exec (Maybe ExecVal)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ExecVal
forall a. Maybe a
Nothing
execCase' env :: ExecEnv
env ctxt :: Context
ctxt amap :: ExecEnv
amap (STerm tm :: Term
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 -> Term -> Exec ExecVal
doExec (((Name, ExecVal) -> (Name, ExecVal)) -> ExecEnv -> ExecEnv
forall a b. (a -> b) -> [a] -> [b]
map (\(n :: Name
n, v :: ExecVal
v) -> (Name
n, ExecVal
v)) ExecEnv
amap ExecEnv -> ExecEnv -> ExecEnv
forall a. [a] -> [a] -> [a]
++ ExecEnv
env) Context
ctxt Term
tm
execCase' env :: ExecEnv
env ctxt :: Context
ctxt amap :: ExecEnv
amap (Case sh :: CaseType
sh n :: Name
n alts :: [CaseAlt' Term]
alts) | Just tm :: ExecVal
tm <- Name -> ExecEnv -> Maybe ExecVal
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n ExecEnv
amap =
       case ExecVal -> [CaseAlt' Term] -> Maybe (SC, ExecEnv)
chooseAlt ExecVal
tm [CaseAlt' Term]
alts of
         Just (newCase :: SC
newCase, newBindings :: 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 (\(x :: Name
x,_) -> Bool -> Bool
not (Name -> [Name] -> 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
         Nothing -> Maybe ExecVal -> Exec (Maybe ExecVal)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ExecVal
forall a. Maybe a
Nothing
execCase' _ _ _ cse :: SC
cse = String -> Exec (Maybe ExecVal)
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Exec (Maybe ExecVal)) -> String -> Exec (Maybe ExecVal)
forall a b. (a -> b) -> a -> b
$ "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' Term] -> Maybe (SC, ExecEnv)
chooseAlt tm :: ExecVal
tm (DefaultCase sc :: SC
sc : alts :: [CaseAlt' Term]
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 -- Default cases should only work on applications of constructors or on constants
        ok :: ExecVal -> Bool
ok (EApp f :: ExecVal
f x :: ExecVal
x) = ExecVal -> Bool
ok ExecVal
f
        ok (EP Bound _ _) = Bool
False
        ok (EP Ref _ _) = Bool
False
        ok _ = Bool
True


chooseAlt (EConstant c :: Const
c) (ConstCase c' :: Const
c' sc :: SC
sc : alts :: [CaseAlt' Term]
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 tm :: ExecVal
tm (ConCase n :: Name
n i :: Int
i ns :: [Name]
ns sc :: SC
sc : alts :: [CaseAlt' Term]
alts) | ((EP _ cn :: Name
cn _), args :: [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' Term] -> Maybe (SC, ExecEnv)
chooseAlt ExecVal
tm [CaseAlt' Term]
alts
chooseAlt tm :: ExecVal
tm (_:alts :: [CaseAlt' Term]
alts) = ExecVal -> [CaseAlt' Term] -> Maybe (SC, ExecEnv)
chooseAlt ExecVal
tm [CaseAlt' Term]
alts
chooseAlt _ [] = 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
showList :: [Foreign] -> ShowS
$cshowList :: [Foreign] -> ShowS
show :: Foreign -> String
$cshow :: Foreign -> String
showsPrec :: Int -> Foreign -> ShowS
$cshowsPrec :: Int -> Foreign -> ShowS
Show

toFType :: FDesc -> FType
toFType :: FDesc -> FType
toFType (FCon c :: Name
c)
    | Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "C_Str" = FType
FString
    | Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "C_Float" = ArithTy -> FType
FArith ArithTy
ATFloat
    | Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "C_Ptr" = FType
FPtr
    | Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "C_MPtr" = FType
FManagedPtr
    | Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "C_Unit" = FType
FUnit
toFType (FApp c :: Name
c [_,ity :: FDesc
ity])
    | Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "C_IntT" = ArithTy -> FType
FArith (FDesc -> ArithTy
toAType FDesc
ity)
  where toAType :: FDesc -> ArithTy
toAType (FCon i :: Name
i)
          | Name
i Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "C_IntChar" = IntTy -> ArithTy
ATInt IntTy
ITChar
          | Name
i Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "C_IntNative" = IntTy -> ArithTy
ATInt IntTy
ITNative
          | Name
i Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "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 "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 "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 "C_IntBits64" = IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT64)
        toAType t :: 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]
++ " not defined in toAType")

toFType (FApp c :: Name
c [_])
    | Name
c Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name
sUN "C_Any" = FType
FAny
toFType t :: 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]
++ " not defined in toFType")

call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
call (FFun name :: String
name argTypes :: [(FDesc, ExecVal)]
argTypes retType :: FDesc
retType) args :: [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 (m :: * -> *) a. Monad m => a -> m a
return Maybe ExecVal
forall a. Maybe a
Nothing)
             (\f :: 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 _ h :: FunPtr a
h) args :: [ExecVal]
args (FArith (ATInt 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 (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 _ h :: FunPtr a
h) args :: [ExecVal]
args (FArith (ATInt (ITFixed 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 (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 _ h :: FunPtr a
h) args :: [ExecVal]
args (FArith (ATInt (ITFixed 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 (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 _ h :: FunPtr a
h) args :: [ExecVal]
args (FArith (ATInt (ITFixed 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 (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 _ h :: FunPtr a
h) args :: [ExecVal]
args (FArith (ATInt (ITFixed 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 (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 _ h :: FunPtr a
h) args :: [ExecVal]
args (FArith 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 (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 _ h :: FunPtr a
h) args :: [ExecVal]
args (FArith (ATInt 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 (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Char -> Const
Ch (CChar -> Char
castCCharToChar CChar
res)))
          call' (Fun _ h :: FunPtr a
h) args :: [ExecVal]
args 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 (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 (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (String -> Const
Str String
hStr))

          call' (Fun _ h :: FunPtr a
h) args :: [ExecVal]
args 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 _ h :: FunPtr a
h) args :: [ExecVal]
args 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 (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' _ _ _ = String -> Exec ExecVal
forall (m :: * -> *) a. MonadFail m => String -> m a
fail "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 i :: Int
i)) = CInt -> Arg
argCInt (Int -> CInt
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)
          prepArg (EConstant (B8 i :: Word8
i)) = CChar -> Arg
argCChar (Word8 -> CChar
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word8
i)
          prepArg (EConstant (B16 i :: Word16
i)) = CWchar -> Arg
argCWchar (Word16 -> CWchar
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word16
i)
          prepArg (EConstant (B32 i :: Word32
i)) = CInt -> Arg
argCInt (Word32 -> CInt
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
i)
          prepArg (EConstant (B64 i :: Word64
i)) = CLong -> Arg
argCLong (Word64 -> CLong
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i)
          prepArg (EConstant (Fl f :: Double
f)) = CDouble -> Arg
argCDouble (Double -> CDouble
forall a b. (Real a, Fractional b) => a -> b
realToFrac Double
f)
          prepArg (EConstant (Ch c :: Char
c)) = CChar -> Arg
argCChar (Char -> CChar
castCharToCChar Char
c) -- FIXME - castCharToCChar only safe for first 256 chars
                                                                    -- Issue #1720 on the issue tracker.
                                                                    -- https://github.com/idris-lang/Idris-dev/issues/1720
          prepArg (EConstant (Str s :: String
s)) = String -> Arg
argString String
s
          prepArg (EPtr p :: Ptr a
p) = Ptr a -> Arg
forall a. Ptr a -> Arg
argPtr Ptr a
p
          prepArg other :: ExecVal
other = String -> Arg -> Arg
forall a. String -> a -> a
trace ("Could not use " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ShowS
forall a. Int -> [a] -> [a]
take 100 (ExecVal -> String
forall a. Show a => a -> String
show ExecVal
other) String -> ShowS
forall a. [a] -> [a] -> [a]
++ " as FFI arg.") Arg
forall a. HasCallStack => a
undefined


foreignFromTT :: Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT :: Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT arity :: Int
arity ty :: ExecVal
ty (EConstant (Str name :: String
name)) args :: [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)
mapM ExecVal -> Maybe (FDesc, ExecVal)
splitArg (Int -> [ExecVal] -> [ExecVal]
forall a. Int -> [a] -> [a]
take Int
arity [ExecVal]
args)
         Foreign -> Maybe Foreign
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 arity :: Int
arity ty :: ExecVal
ty fn :: ExecVal
fn args :: [ExecVal]
args = String -> Maybe Foreign -> Maybe Foreign
forall a. String -> a -> a
trace ("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 tm :: ExecVal
tm = case ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
tm of
               (nil :: ExecVal
nil, [_]) -> [ExecVal] -> Maybe [ExecVal]
forall a. a -> Maybe a
Just []
               (cons :: ExecVal
cons, ([_, x :: ExecVal
x, xs :: ExecVal
xs])) ->
                   do [ExecVal]
rest <- ExecVal -> Maybe [ExecVal]
unEList ExecVal
xs
                      [ExecVal] -> Maybe [ExecVal]
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
               (f :: ExecVal
f, args :: [ExecVal]
args) -> Maybe [ExecVal]
forall a. Maybe a
Nothing


mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM :: (a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM f :: a -> m (Maybe b)
f [] = [b] -> m [b]
forall (m :: * -> *) a. Monad m => a -> m a
return []
mapMaybeM f :: a -> m (Maybe b)
f (x :: a
x:xs :: [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 fn :: 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
                      [f :: ForeignFun
f] -> Maybe ForeignFun -> Exec (Maybe ForeignFun)
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
$ "Symbol \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fn String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\" not found"
                               Maybe ForeignFun -> Exec (Maybe ForeignFun)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ForeignFun
forall a. Maybe a
Nothing
                      fs :: [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
$ "Symbol \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fn String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\" is ambiguous. Found " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                                   Int -> String
forall a. Show a => a -> String
show ([ForeignFun] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ForeignFun]
fs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ " occurrences."
                               Maybe ForeignFun -> Exec (Maybe ForeignFun)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ForeignFun
forall a. Maybe a
Nothing
    where getFn :: DynamicLib -> Exec (Maybe ForeignFun)
getFn lib :: 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) (\_ -> Maybe ForeignFun -> IO (Maybe ForeignFun)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ForeignFun
forall a. Maybe a
Nothing)

#endif