{-|
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
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 = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ ExecVal
operationNotPermitted

operationNotPermitted :: ExecVal
operationNotPermitted =
  ExecVal -> ExecVal
ioWrap forall a b. (a -> b) -> a -> b
$ ExecVal -> ExecVal
mkRaw forall a b. (a -> b) -> a -> b
$ ExecVal -> ExecVal -> ExecVal
EApp (NameType -> Name -> ExecVal -> ExecVal
EP (Int -> Int -> Bool -> NameType
DCon Int
0 Int
1 Bool
False)
                            (Name -> [String] -> Name
sNS (String -> Name
sUN String
"GenericFileError") [String
"File", String
"Prelude"])
                            ExecVal
EErased)
                        (Const -> ExecVal
EConstant (Int -> Const
I Int
1))

namedFileError :: String -> ExecVal
namedFileError String
name =
  ExecVal -> ExecVal
ioWrap forall a b. (a -> b) -> a -> b
$ ExecVal -> ExecVal
mkRaw forall a b. (a -> b) -> a -> b
$ (NameType -> Name -> ExecVal -> ExecVal
EP (Int -> Int -> Bool -> NameType
DCon Int
0 Int
0 Bool
False)
                       (Name -> [String] -> Name
sNS (String -> Name
sUN String
name) [String
"File", String
"Prelude"])
                       ExecVal
EErased)

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

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

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

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

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

mkEApp :: ExecVal -> [ExecVal] -> ExecVal
mkEApp :: ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [] = ExecVal
f
mkEApp ExecVal
f (ExecVal
a:[ExecVal]
args) = ExecVal -> [ExecVal] -> ExecVal
mkEApp (ExecVal -> ExecVal -> ExecVal
EApp ExecVal
f ExecVal
a) [ExecVal]
args

initState :: Idris ExecState
initState :: Idris ExecState
initState = do IState
ist <- Idris IState
getIState
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [DynamicLib] -> [Name] -> ExecState
ExecState (IState -> [DynamicLib]
idris_dynamic_libs IState
ist) []

type Exec = ExceptT Err (StateT ExecState IO)

runExec :: Exec a -> ExecState -> IO (Either Err a)
runExec :: forall a. Exec a -> ExecState -> IO (Either Err a)
runExec Exec a
ex ExecState
st = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (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 = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *) s. Monad m => StateT s m s
get

execFail :: Err -> Exec a
execFail :: forall a. Err -> Exec a
execFail = forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE

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


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

ioWrap :: ExecVal -> ExecVal
ioWrap :: ExecVal -> ExecVal
ioWrap ExecVal
tm = ExecVal -> [ExecVal] -> ExecVal
mkEApp (NameType -> Name -> ExecVal -> ExecVal
EP (Int -> Int -> Bool -> NameType
DCon Int
0 Int
2 Bool
False) (String -> Name
sUN String
"prim__IO") ExecVal
EErased) [ExecVal
EErased, ExecVal
tm]

ioUnit :: ExecVal
ioUnit :: ExecVal
ioUnit = ExecVal -> ExecVal
ioWrap (NameType -> Name -> ExecVal -> ExecVal
EP NameType
Ref Name
unitCon ExecVal
EErased)

type ExecEnv = [(Name, ExecVal)]

doExec :: ExecEnv -> Context -> Term -> Exec ExecVal
doExec :: ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt p :: TT Name
p@(P NameType
Ref Name
n TT Name
ty) | Just ExecVal
v <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n ExecEnv
env = forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
v
doExec ExecEnv
env Context
ctxt p :: TT Name
p@(P NameType
Ref Name
n TT Name
ty) =
    do let val :: [Def]
val = Name -> Context -> [Def]
lookupDef Name
n Context
ctxt
       case [Def]
val of
         [Function TT Name
_ TT Name
tm] -> ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
tm
         [TyDecl NameType
_ TT Name
_] -> forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> ExecVal -> ExecVal
EP NameType
Ref Name
n ExecVal
EErased) -- abstract def
         [Operator TT Name
tp Int
arity [Value] -> Maybe Value
op] -> 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 CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ (CaseDefs ([], STerm TT Name
tm) ([Name], SC)
_)] -> -- nullary fun
             ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
tm
         [CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ (CaseDefs ([Name]
ns, SC
sc) ([Name], SC)
_)] -> forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> ExecVal -> ExecVal
EP NameType
Ref Name
n ExecVal
EErased)
         [] -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ String
"Could not find " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n forall a. [a] -> [a] -> [a]
++ String
" in definitions."
         [Def]
other | forall (t :: * -> *) a. Foldable t => t a -> Int
length [Def]
other forall a. Ord a => a -> a -> Bool
> Int
1 -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ String
"Multiple definitions found for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n
               | Bool
otherwise        -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take Int
500 forall a b. (a -> b) -> a -> b
$ String
"got to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Def]
other forall a. [a] -> [a] -> [a]
++ String
" lookup up " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Name
n
doExec ExecEnv
env Context
ctxt p :: TT Name
p@(P NameType
Bound Name
n TT Name
ty) =
  case forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n ExecEnv
env of
    Maybe ExecVal
Nothing -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ String
"not found"
    Just ExecVal
tm -> forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
tm
doExec ExecEnv
env Context
ctxt (P (DCon Int
a Int
b Bool
u) Name
n TT Name
_) = forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> ExecVal -> ExecVal
EP (Int -> Int -> Bool -> NameType
DCon Int
a Int
b Bool
u) Name
n ExecVal
EErased)
doExec ExecEnv
env Context
ctxt (P (TCon Int
a Int
b) Name
n TT Name
_) = forall (m :: * -> *) a. Monad m => a -> m a
return (NameType -> Name -> ExecVal -> ExecVal
EP (Int -> Int -> NameType
TCon Int
a Int
b) Name
n ExecVal
EErased)
doExec ExecEnv
env Context
ctxt v :: TT Name
v@(V Int
i) | Int
i forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Int
length ExecEnv
env = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a, b) -> b
snd (ExecEnv
env forall a. [a] -> Int -> a
!! Int
i))
                        | Bool
otherwise      = forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ String
"env too small"
doExec ExecEnv
env Context
ctxt (Bind Name
n (Let RigCount
rig TT Name
t TT Name
v) TT Name
body)
     = do ExecVal
v' <- ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
v
          ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ((Name
n, ExecVal
v')forall a. a -> [a] -> [a]
:ExecEnv
env) Context
ctxt TT Name
body
doExec ExecEnv
env Context
ctxt (Bind Name
n (NLet TT Name
t TT Name
v) TT Name
body) = forall a. HasCallStack => a
undefined
doExec ExecEnv
env Context
ctxt tm :: TT Name
tm@(Bind Name
n Binder (TT Name)
b TT Name
body) = do Binder ExecVal
b' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM Binder (TT Name)
b (ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt)
                                        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
                                          Name -> Binder ExecVal -> (ExecVal -> Exec ExecVal) -> ExecVal
EBind Name
n Binder ExecVal
b' (\ExecVal
arg -> ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ((Name
n, ExecVal
arg)forall a. a -> [a] -> [a]
:ExecEnv
env) Context
ctxt TT Name
body)
doExec ExecEnv
env Context
ctxt a :: TT Name
a@(App AppStatus Name
_ TT Name
_ TT Name
_) =
  do let (TT Name
f, [TT Name]
args) = forall n. TT n -> (TT n, [TT n])
unApply TT Name
a
     ExecVal
f' <- ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
f
     [ExecVal]
args' <- case ExecVal
f' of
                (EP NameType
_ Name
d ExecVal
_) | Name
d forall a. Eq a => a -> a -> Bool
== Name
delay ->
                  case [TT Name]
args of
                    [TT Name
t,TT Name
a,TT Name
tm] -> do ExecVal
t' <- ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
t
                                   ExecVal
a' <- ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
a
                                   forall (m :: * -> *) a. Monad m => a -> m a
return [ExecVal
t', ExecVal
a', Context -> ExecEnv -> TT Name -> ExecVal
EThunk Context
ctxt ExecEnv
env TT Name
tm]
                    [TT Name]
_ -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt) [TT Name]
args -- partial applications are fine to evaluate
                ExecVal
fun' -> do forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt) [TT Name]
args
     ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
f' [ExecVal]
args'
doExec ExecEnv
env Context
ctxt (Constant Const
c) = forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant Const
c)
doExec ExecEnv
env Context
ctxt (Proj TT Name
tm Int
i) = let (TT Name
x, [TT Name]
xs) = forall n. TT n -> (TT n, [TT n])
unApply TT Name
tm in
                              ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt ((TT Name
xforall a. a -> [a] -> [a]
:[TT Name]
xs) forall a. [a] -> Int -> a
!! Int
i)
doExec ExecEnv
env Context
ctxt TT Name
Erased = forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
EErased
doExec ExecEnv
env Context
ctxt TT Name
Impossible = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Tried to execute an impossible case"
doExec ExecEnv
env Context
ctxt (Inferred TT Name
t) = ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
t
doExec ExecEnv
env Context
ctxt (TType UExp
u) = forall (m :: * -> *) a. Monad m => a -> m a
return (UExp -> ExecVal
EType UExp
u)
doExec ExecEnv
env Context
ctxt (UType Universe
u) = forall (m :: * -> *) a. Monad m => a -> m a
return (Universe -> ExecVal
EUType Universe
u)

execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp :: ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
v [] = forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
v -- no args is just a constant! can result from function calls
execApp ExecEnv
env Context
ctxt (EP NameType
_ Name
f ExecVal
_) (ExecVal
t:ExecVal
a:ExecVal
delayed:[ExecVal]
rest)
  | Name
f forall a. Eq a => a -> a -> Bool
== Name
force
  , (ExecVal
_, [ExecVal
_, ExecVal
_, EThunk Context
tmCtxt ExecEnv
tmEnv TT Name
tm]) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
delayed =
    do ExecVal
tm' <- ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
tmEnv Context
tmCtxt TT Name
tm
       ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
tm' [ExecVal]
rest
execApp ExecEnv
env Context
ctxt (EP NameType
_ Name
fp ExecVal
_) (ExecVal
ty:ExecVal
action:[ExecVal]
rest)
  | Name
fp forall a. Eq a => a -> a -> Bool
== Name
upio,
    (ExecVal
prim__IO, [ExecVal
_, ExecVal
v]) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
action
       = ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
v [ExecVal]
rest

execApp ExecEnv
env Context
ctxt (EP NameType
_ Name
fp ExecVal
_) args :: [ExecVal]
args@(ExecVal
_:ExecVal
_:ExecVal
v:ExecVal
k:[ExecVal]
rest)
  | Name
fp forall a. Eq a => a -> a -> Bool
== Name
piobind,
    (ExecVal
prim__IO, [ExecVal
_, ExecVal
v']) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
v =
    do ExecVal
res <- ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
k [ExecVal
v']
       ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res [ExecVal]
rest
execApp ExecEnv
env Context
ctxt con :: ExecVal
con@(EP NameType
_ Name
fp ExecVal
_) args :: [ExecVal]
args@(ExecVal
tp:ExecVal
v:[ExecVal]
rest)
  | Name
fp 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 ExecEnv
env Context
ctxt f :: ExecVal
f@(EP NameType
_ Name
fp ExecVal
_) args :: [ExecVal]
args@(ExecVal
xs:ExecVal
_:ExecVal
_:ExecVal
_:[ExecVal]
args')
    | Name
fp forall a. Eq a => a -> a -> Bool
== Name
mkfprim,
      (ExecVal
ty : ExecVal
fn : ExecVal
w : [ExecVal]
rest) <- forall a. [a] -> [a]
reverse [ExecVal]
args' =
          ExecEnv
-> Context
-> Int
-> ExecVal
-> ExecVal
-> [ExecVal]
-> ExecVal
-> Exec ExecVal
execForeign ExecEnv
env Context
ctxt Int
getArity ExecVal
ty ExecVal
fn [ExecVal]
rest (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args)
  where getArity :: Int
getArity = case ExecVal -> Maybe [ExecVal]
unEList ExecVal
xs of
                        Just [ExecVal]
as -> forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExecVal]
as
                        Maybe [ExecVal]
_ -> Int
0

execApp ExecEnv
env Context
ctxt c :: ExecVal
c@(EP (DCon Int
_ Int
arity Bool
_) Name
n ExecVal
_) [ExecVal]
args =
    do let args' :: [ExecVal]
args' = forall a. Int -> [a] -> [a]
take Int
arity [ExecVal]
args
       let restArgs :: [ExecVal]
restArgs = forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
args
       ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
c [ExecVal]
args') [ExecVal]
restArgs

execApp ExecEnv
env Context
ctxt c :: ExecVal
c@(EP (TCon Int
_ Int
arity) Name
n ExecVal
_) [ExecVal]
args =
    do let args' :: [ExecVal]
args' = forall a. Int -> [a] -> [a]
take Int
arity [ExecVal]
args
       let restArgs :: [ExecVal]
restArgs = forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
args
       ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
c [ExecVal]
args') [ExecVal]
restArgs

execApp ExecEnv
env Context
ctxt f :: ExecVal
f@(EP NameType
_ Name
n ExecVal
_) [ExecVal]
args
    | Just (Exec ExecVal
res, [ExecVal]
rest) <- Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])
getOp Name
n [ExecVal]
args = do ExecVal
r <- Exec ExecVal
res
                                            ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
r [ExecVal]
rest
execApp ExecEnv
env Context
ctxt f :: ExecVal
f@(EP NameType
_ Name
n ExecVal
_) [ExecVal]
args =
    do let val :: [Def]
val = Name -> Context -> [Def]
lookupDef Name
n Context
ctxt
       case [Def]
val of
         [Function TT Name
_ TT Name
tm] -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"should already have been eval'd"
         [TyDecl NameType
nt TT Name
ty] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args
         [Operator TT Name
tp Int
arity [Value] -> Maybe Value
op] ->
             if forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExecVal]
args forall a. Ord a => a -> a -> Bool
>= Int
arity
               then let args' :: [ExecVal]
args' = forall a. Int -> [a] -> [a]
take Int
arity [ExecVal]
args in
                    case Name -> [ExecVal] -> Maybe (Exec ExecVal, [ExecVal])
getOp Name
n [ExecVal]
args' of
                      Just (Exec ExecVal
res, []) -> do ExecVal
r <- Exec ExecVal
res
                                           ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
r (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
args)
                      Maybe (Exec ExecVal, [ExecVal])
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args)
               else forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args)
         [CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ (CaseDefs ([], STerm TT Name
tm) ([Name], SC)
_)] -> -- nullary fun
             do ExecVal
rhs <- ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec ExecEnv
env Context
ctxt TT Name
tm
                ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
rhs [ExecVal]
args
         [CaseOp CaseInfo
_ TT Name
_ [(TT Name, Bool)]
_ [Either (TT Name) (TT Name, TT Name)]
_ [([Name], TT Name, TT Name)]
_ (CaseDefs ([Name]
ns, SC
sc) ([Name], SC)
_)] ->
             do Maybe ExecVal
res <- ExecEnv
-> Context -> [Name] -> SC -> [ExecVal] -> Exec (Maybe ExecVal)
execCase ExecEnv
env Context
ctxt [Name]
ns SC
sc [ExecVal]
args
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args) Maybe ExecVal
res
         [Def]
thing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args
execApp ExecEnv
env Context
ctxt bnd :: ExecVal
bnd@(EBind Name
n Binder ExecVal
b ExecVal -> Exec ExecVal
body) (ExecVal
arg:[ExecVal]
args) = do ExecVal
ret <- ExecVal -> Exec ExecVal
body ExecVal
arg
                                                      let (ExecVal
f', [ExecVal]
as) = ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
ret
                                                      ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
f' ([ExecVal]
as forall a. [a] -> [a] -> [a]
++ [ExecVal]
args)
execApp ExecEnv
env Context
ctxt app :: ExecVal
app@(EApp ExecVal
_ ExecVal
_) [ExecVal]
args2 | (ExecVal
f, [ExecVal]
args1) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
app = ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
f ([ExecVal]
args1 forall a. [a] -> [a] -> [a]
++ [ExecVal]
args2)
execApp ExecEnv
env Context
ctxt ExecVal
f [ExecVal]
args = forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
f [ExecVal]
args)

execForeign :: ExecEnv
-> Context
-> Int
-> ExecVal
-> ExecVal
-> [ExecVal]
-> ExecVal
-> Exec ExecVal
execForeign ExecEnv
env Context
ctxt Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs ExecVal
onfail
    | Just (FFun String
"putStr" [(FDesc
_, ExecVal
str)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
       = case ExecVal
str of
           EConstant (Str String
arg) -> do 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 (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
           ExecVal
_ -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                  String
"The argument to putStr should be a constant string, but it was " forall a. [a] -> [a] -> [a]
++
                  forall a. Show a => a -> String
show ExecVal
str forall a. [a] -> [a] -> [a]
++
                  String
". Are all cases covered?"
    | Just (FFun String
"putchar" [(FDesc
_, ExecVal
ch)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
ch of
               EConstant (Ch Char
c) -> do 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 (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
               EConstant (I Int
i)  -> do forall a. IO a -> Exec a
execIO (Char -> IO ()
putChar (forall a. Enum a => Int -> a
toEnum Int
i))
                                      ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
ioUnit (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
               ExecVal
_ -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                      String
"The argument to putchar should be a constant character, but it was " forall a. [a] -> [a] -> [a]
++
                      forall a. Show a => a -> String
show Text -> String
str forall a. [a] -> [a] -> [a]
++
                      String
". Are all cases covered?"
    | Just (FFun String
"idris_readStr" [(FDesc, ExecVal)
_, (FDesc
_, ExecVal
handle)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
handle of
               EHandle Handle
h -> do String
contents <- forall a. IO a -> Exec a
execIO 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 forall a. [a] -> [a] -> [a]
++ String
"\n"))) (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
               ExecVal
_ -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                      String
"The argument to idris_readStr should be a handle, but it was " forall a. [a] -> [a] -> [a]
++
                      forall a. Show a => a -> String
show ExecVal
handle forall a. [a] -> [a] -> [a]
++
                      String
". Are all cases covered?"
    | Just (FFun String
"getchar" [(FDesc, ExecVal)]
_ FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = do -- The C API returns an Int which Idris library code
                -- converts; thus, we must make an int here.
                ExecVal
ch <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ExecVal -> ExecVal
ioWrap forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> ExecVal
EConstant forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => a -> Int
fromEnum) IO Char
getChar
                ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
ch [ExecVal]
xs
    | Just (FFun String
"idris_time" [(FDesc, ExecVal)]
_ FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = do forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ExecVal -> ExecVal
ioWrap forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExecVal -> ExecVal
mkRaw forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> ExecVal
EConstant forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (RealFrac a, Integral b) => a -> b
round) IO POSIXTime
getPOSIXTime
    | Just (FFun String
"idris_showerror" [(FDesc, ExecVal)]
_ FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = do forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExecVal -> ExecVal
ioWrap forall a b. (a -> b) -> a -> b
$ Const -> ExecVal
EConstant forall a b. (a -> b) -> a -> b
$ String -> Const
Str String
"Operation not permitted"
    | Just (FFun String
"idris_mkFileError" [(FDesc, ExecVal)]
_ FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = do forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef ExecVal
fileError
    | Just (FFun String
"fileOpen" [(FDesc
_,ExecVal
fileStr), (FDesc
_,ExecVal
modeStr)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case (ExecVal
fileStr, ExecVal
modeStr) of
               (EConstant (Str String
f), EConstant (Str String
mode)) ->
                 do Either String (ExecVal, [ExecVal])
f <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$
                         forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch (do let m :: Either String IOMode
m = case forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= Char
'b') String
mode of
                                             String
"r"  -> forall a b. b -> Either a b
Right IOMode
ReadMode
                                             String
"w"  -> forall a b. b -> Either a b
Right IOMode
WriteMode
                                             String
"a"  -> forall a b. b -> Either a b
Right IOMode
AppendMode
                                             String
"rw" -> forall a b. b -> Either a b
Right IOMode
ReadWriteMode
                                             String
"wr" -> forall a b. b -> Either a b
Right IOMode
ReadWriteMode
                                             String
"r+" -> forall a b. b -> Either a b
Right IOMode
ReadWriteMode
                                             String
_    -> forall a b. a -> Either a b
Left (String
"Invalid mode for " forall a. [a] -> [a] -> [a]
++ String
f forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ String
mode)
                                   case forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> IOMode -> IO Handle
openFile String
f) Either String IOMode
m of
                                     Right IO Handle
h -> do Handle
h' <- IO Handle
h
                                                   Handle -> Bool -> IO ()
hSetBinaryMode Handle
h' Bool
True
                                                   forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (ExecVal -> ExecVal
ioWrap (Handle -> ExecVal
EHandle Handle
h'), forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
                                     Left String
err -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left String
err)
                               (\IOError
e -> do forall a. IORef a -> a -> IO ()
writeIORef IORef ExecVal
fileError forall a b. (a -> b) -> a -> b
$ IOError -> ExecVal
mapError IOError
e
                                         forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right (ExecVal -> ExecVal
ioWrap (forall a. Ptr a -> ExecVal
EPtr forall a. Ptr a
nullPtr), forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs))
                    case Either String (ExecVal, [ExecVal])
f of
                      Left String
err -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$ String
err
                      Right (ExecVal
res, [ExecVal]
rest) -> ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res [ExecVal]
rest
               (ExecVal, ExecVal)
_ -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                      String
"The arguments to fileOpen should be constant strings, but they were " forall a. [a] -> [a] -> [a]
++
                      forall a. Show a => a -> String
show ExecVal
fileStr forall a. [a] -> [a] -> [a]
++ String
" and " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ExecVal
modeStr forall a. [a] -> [a] -> [a]
++
                      String
". Are all cases covered?"
    | Just (FFun String
"fileEOF" [(FDesc
_,ExecVal
handle)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
handle of
               EHandle Handle
h -> do Bool
eofp <- forall a. IO a -> Exec a
execIO 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 forall a b. (a -> b) -> a -> b
$ if Bool
eofp then Int
1 else Int
0))
                               ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
               ExecVal
_ -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                      String
"The argument to fileEOF should be a file handle, but it was " forall a. [a] -> [a] -> [a]
++
                      forall a. Show a => a -> String
show ExecVal
handle forall a. [a] -> [a] -> [a]
++
                      String
". Are all cases covered?"
    | Just (FFun String
"fileError" [(FDesc
_,ExecVal
handle)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
handle of
             -- 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 Handle
h -> do let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap (Const -> ExecVal
EConstant (Int -> Const
I Int
0))
                               ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
               ExecVal
_ -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                      String
"The argument to fileError should be a file handle, but it was " forall a. [a] -> [a] -> [a]
++
                      forall a. Show a => a -> String
show ExecVal
handle forall a. [a] -> [a] -> [a]
++
                      String
". Are all cases covered?"
    | Just (FFun String
"fileRemove" [(FDesc
_,ExecVal
fileStr)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
fileStr of
               EConstant (Str String
f) -> do ExecVal
res <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch (do String -> IO ()
removeFile String
f
                                                                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExecVal -> ExecVal
ioWrap forall a b. (a -> b) -> a -> b
$ Const -> ExecVal
EConstant forall a b. (a -> b) -> a -> b
$ Int -> Const
I Int
0)
                                                             (\IOError
e -> do forall a. IORef a -> a -> IO ()
writeIORef IORef ExecVal
fileError forall a b. (a -> b) -> a -> b
$ IOError -> ExecVal
mapError IOError
e
                                                                       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExecVal -> ExecVal
ioWrap forall a b. (a -> b) -> a -> b
$ Const -> ExecVal
EConstant forall a b. (a -> b) -> a -> b
$ Int -> Const
I (-Int
1))
                                       ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
               ExecVal
_ -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                      String
"The argument to fileRemove should be a constant string, but it was " forall a. [a] -> [a] -> [a]
++
                      forall a. Show a => a -> String
show ExecVal
fileStr forall a. [a] -> [a] -> [a]
++
                      String
". Are all cases covered?"
    | Just (FFun String
"fileClose" [(FDesc
_,ExecVal
handle)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
handle of
               EHandle Handle
h -> do forall a. IO a -> Exec a
execIO 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 (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
               ExecVal
_ -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                      String
"The argument to fileClose should be a file handle, but it was " forall a. [a] -> [a] -> [a]
++
                      forall a. Show a => a -> String
show ExecVal
handle forall a. [a] -> [a] -> [a]
++
                      String
". Are all cases covered?"
    | Just (FFun String
"fileSize" [(FDesc
_,ExecVal
handle)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
handle of
               EHandle Handle
h -> do Integer
size <- forall a. IO a -> Exec a
execIO 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 (forall a. Num a => Integer -> a
fromInteger Integer
size)))
                               ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
               ExecVal
_ -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                      String
"The argument to fileSize should be a file handle, but it was " forall a. [a] -> [a] -> [a]
++
                      forall a. Show a => a -> String
show ExecVal
handle forall a. [a] -> [a] -> [a]
++
                      String
". Are all cases covered?"

    | Just (FFun String
"isNull" [(FDesc
_, ExecVal
ptr)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = case ExecVal
ptr of
               EPtr Ptr a
p -> let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> ExecVal
EConstant forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I forall a b. (a -> b) -> a -> b
$
                                   if Ptr a
p forall a. Eq a => a -> a -> Bool
== forall a. Ptr a
nullPtr then Int
1 else Int
0
                         in ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (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 Handle
h -> let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> ExecVal
EConstant forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I forall a b. (a -> b) -> a -> b
$ Int
0
                            in ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
               -- A foreign-returned char* has to be tested for NULL sometimes
               EConstant (Str String
s) -> let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> ExecVal
EConstant forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I forall a b. (a -> b) -> a -> b
$ Int
0
                                    in ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
               ExecVal
_ -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                      String
"The argument to isNull should be a pointer or file handle or string, but it was " forall a. [a] -> [a] -> [a]
++
                      forall a. Show a => a -> String
show ExecVal
ptr forall a. [a] -> [a] -> [a]
++
                      String
". Are all cases covered?"

    | Just (FFun String
"idris_disableBuffering" [(FDesc, ExecVal)]
_ FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
       = do forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ Handle -> BufferMode -> IO ()
hSetBuffering Handle
stdin BufferMode
NoBuffering
            forall a. IO a -> Exec a
execIO 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 (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)

    -- Just use a Haskell String in an IORef for a string buffer
    | Just (FFun String
"idris_makeStringBuffer" [(FDesc
_, ExecVal
len)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
       = case ExecVal
len of
              EConstant (I Int
_) -> do IORef String
buf <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef String
""
                                    let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap (IORef String -> ExecVal
EStringBuf IORef String
buf)
                                    ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)

              ExecVal
_ -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                      String
"The argument to idris_makeStringBuffer should be an Int, but it was " forall a. [a] -> [a] -> [a]
++
                      forall a. Show a => a -> String
show ExecVal
len forall a. [a] -> [a] -> [a]
++
                      String
". Are all cases covered?"
    | Just (FFun String
"idris_addToString" [(FDesc
_, ExecVal
strBuf), (FDesc
_, ExecVal
str)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
       = case (ExecVal
strBuf, ExecVal
str) of
              (EStringBuf IORef String
ref, EConstant (Str String
add)) ->
                  do forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef String
ref (forall a. [a] -> [a] -> [a]
++String
add)
                     ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
ioUnit (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
              (ExecVal, ExecVal)
_ -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                      String
"The arguments to idris_addToString should be a StringBuffer and a String, but were " forall a. [a] -> [a] -> [a]
++
                      forall a. Show a => a -> String
show ExecVal
strBuf forall a. [a] -> [a] -> [a]
++ String
" and " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ExecVal
str forall a. [a] -> [a] -> [a]
++
                      String
". Are all cases covered?"
    | Just (FFun String
"idris_getString" [(FDesc, ExecVal)
_, (FDesc
_, ExecVal
str)] FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
       = case ExecVal
str of
              EStringBuf IORef String
ref -> do String
str <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ 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 (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)
              ExecVal
_ -> forall a. Err -> Exec a
execFail forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Err' t
Msg forall a b. (a -> b) -> a -> b
$
                      String
"The argument to idris_getString should be a StringBuffer, but it was " forall a. [a] -> [a] -> [a]
++
                      forall a. Show a => a -> String
show ExecVal
str forall a. [a] -> [a] -> [a]
++
                      String
". Are all cases covered?"



-- Right now, there's no way to send command-line arguments to the executor,
-- so just return 0.
execForeign ExecEnv
env Context
ctxt Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs ExecVal
onfail
    | Just (FFun String
"idris_numArgs" [(FDesc, ExecVal)]
_ FDesc
_) <- Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs
           = let res :: ExecVal
res = ExecVal -> ExecVal
ioWrap forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> ExecVal
EConstant forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Const
I forall a b. (a -> b) -> a -> b
$ Int
0
             in ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp ExecEnv
env Context
ctxt ExecVal
res (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs)

execForeign ExecEnv
env Context
ctxt Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs ExecVal
onfail
   = case Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
xs of
        Just ffun :: Foreign
ffun@(FFun String
f [(FDesc, ExecVal)]
argTs FDesc
retT) | forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExecVal]
xs forall a. Ord a => a -> a -> Bool
>= Int
arity ->
           do let ([ExecVal]
_, [ExecVal]
xs') = (forall a. Int -> [a] -> [a]
take Int
arity [ExecVal]
xs, -- foreign args
                              forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
xs) -- rest
              Maybe ExecVal
res <- Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
call Foreign
ffun (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(FDesc, ExecVal)]
argTs)
              case Maybe ExecVal
res of
                   Maybe ExecVal
Nothing -> forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"Could not call foreign function \"" forall a. [a] -> [a] -> [a]
++ String
f forall a. [a] -> [a] -> [a]
++
                                     String
"\" with args " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(FDesc, ExecVal)]
argTs)
                   Just ExecVal
r -> forall (m :: * -> *) a. Monad m => a -> m a
return (ExecVal -> [ExecVal] -> ExecVal
mkEApp ExecVal
r [ExecVal]
xs')
        Maybe Foreign
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
onfail


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

toFDesc :: ExecVal -> FDesc
toFDesc ExecVal
tm
   | (EP NameType
_ Name
n ExecVal
_, []) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
tm = Name -> FDesc
FCon (Name -> Name
deNS Name
n)
   | (EP NameType
_ Name
n ExecVal
_, [ExecVal]
as) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
tm = Name -> [FDesc] -> FDesc
FApp (Name -> Name
deNS Name
n) (forall a b. (a -> b) -> [a] -> [b]
map ExecVal -> FDesc
toFDesc [ExecVal]
as)
toFDesc ExecVal
_ = FDesc
FUnknown

deNS :: Name -> Name
deNS (NS Name
n [Text]
_) = Name
n
deNS Name
n = Name
n

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

-- | 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 Name
fn (ExecVal
_ : ExecVal
_ : ExecVal
x : [ExecVal]
xs) | Name
fn forall a. Eq a => a -> a -> Bool
== Name
pbm = forall a. a -> Maybe a
Just (forall (m :: * -> *) a. Monad m => a -> m a
return ExecVal
x, [ExecVal]
xs)
getOp Name
fn (ExecVal
_ : EConstant (Str String
n) : [ExecVal]
xs)
    | Name
fn forall a. Eq a => a -> a -> Bool
== Name
pws =
              forall a. a -> Maybe a
Just (do forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr String
n forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hFlush Handle
stdout
                       forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Int -> Const
I Int
0)), [ExecVal]
xs)
getOp Name
fn (ExecVal
_:[ExecVal]
xs)
    | Name
fn forall a. Eq a => a -> a -> Bool
== Name
prs =
              forall a. a -> Maybe a
Just (do String
line <- forall a. IO a -> Exec a
execIO IO String
getLine
                       forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (String -> Const
Str String
line)), [ExecVal]
xs)
getOp Name
fn (ExecVal
_ : EP NameType
_ Name
fn' ExecVal
_ : EConstant (Str String
n) : [ExecVal]
xs)
    | Name
fn forall a. Eq a => a -> a -> Bool
== Name
pwf Bool -> Bool -> Bool
&& Name
fn' forall a. Eq a => a -> a -> Bool
== Name
pstdout =
              forall a. a -> Maybe a
Just (do forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr String
n forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hFlush Handle
stdout
                       forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Int -> Const
I Int
0)), [ExecVal]
xs)
getOp Name
fn (ExecVal
_ : EP NameType
_ Name
fn' ExecVal
_ : [ExecVal]
xs)
    | Name
fn forall a. Eq a => a -> a -> Bool
== Name
prf Bool -> Bool -> Bool
&& Name
fn' forall a. Eq a => a -> a -> Bool
== Name
pstdin =
              forall a. a -> Maybe a
Just (do String
line <- forall a. IO a -> Exec a
execIO IO String
getLine
                       forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (String -> Const
Str String
line)), [ExecVal]
xs)
getOp Name
fn (ExecVal
_ : EHandle Handle
h : EConstant (Str String
n) : [ExecVal]
xs)
    | Name
fn forall a. Eq a => a -> a -> Bool
== Name
pwf =
              forall a. a -> Maybe a
Just (do forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStr Handle
h String
n forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Handle -> IO ()
hFlush Handle
h
                       forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Int -> Const
I Int
0)), [ExecVal]
xs)
getOp Name
fn (ExecVal
_ : EHandle Handle
h : [ExecVal]
xs)
    | Name
fn forall a. Eq a => a -> a -> Bool
== Name
prf =
              forall a. a -> Maybe a
Just (do String
contents <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ Handle -> IO String
hGetLine Handle
h
                       forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (String -> Const
Str (String
contents forall a. [a] -> [a] -> [a]
++ String
"\n"))), [ExecVal]
xs)
getOp Name
fn (ExecVal
_ : EConstant (I Int
len) : EHandle Handle
h : [ExecVal]
xs)
    | Name
fn forall a. Eq a => a -> a -> Bool
== Name
prc =
              forall a. a -> Maybe a
Just (do String
contents <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall {t}. (Eq t, Num t) => Handle -> t -> IO String
hGetChars Handle
h Int
len
                       forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (String -> Const
Str String
contents)), [ExecVal]
xs)
  where hGetChars :: Handle -> t -> IO String
hGetChars Handle
h t
0 = forall (m :: * -> *) a. Monad m => a -> m a
return String
""
        hGetChars Handle
h t
i = do Bool
eof <- Handle -> IO Bool
hIsEOF Handle
h
                           if Bool
eof then forall (m :: * -> *) a. Monad m => a -> m a
return String
"" else do
                             Char
c <- Handle -> IO Char
hGetChar Handle
h
                             String
rest <- Handle -> t -> IO String
hGetChars Handle
h (t
i forall a. Num a => a -> a -> a
- t
1)
                             forall (m :: * -> *) a. Monad m => a -> m a
return (Char
c forall a. a -> [a] -> [a]
: String
rest)
getOp Name
fn (ExecVal
_ : ExecVal
arg : [ExecVal]
xs)
    | Name
fn forall a. Eq a => a -> a -> Bool
== Name
prf =
              forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ (forall a. Err -> Exec a
execFail (forall t. String -> Err' t
Msg String
"Can't use prim__readFile on a raw pointer in the executor."), [ExecVal]
xs)
getOp Name
n [ExecVal]
args = do (Int
arity, [ExecVal] -> Maybe ExecVal
prim) <- Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)
getPrim Name
n [Prim]
primitives
                  if (forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExecVal]
args 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 (forall a. Int -> [a] -> [a]
take Int
arity [ExecVal]
args)
                             forall a. a -> Maybe a
Just (Exec ExecVal
res, forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
args)
                     else forall a. Maybe a
Nothing
    where getPrim :: Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)
          getPrim :: Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)
getPrim Name
n [] = forall a. Maybe a
Nothing
          getPrim Name
n ((Prim Name
pn TT Name
_ Int
arity [Const] -> Maybe Const
def (Int, PrimFn)
_ Totality
_) : [Prim]
prims)
             | Name
n forall a. Eq a => a -> a -> Bool
== Name
pn   = forall a. a -> Maybe a
Just (Int
arity, ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
execPrim [Const] -> Maybe Const
def)
             | Bool
otherwise = Name -> [Prim] -> Maybe (Int, [ExecVal] -> Maybe ExecVal)
getPrim Name
n [Prim]
prims

          execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
          execPrim :: ([Const] -> Maybe Const) -> [ExecVal] -> Maybe ExecVal
execPrim [Const] -> Maybe Const
f [ExecVal]
args = Const -> ExecVal
EConstant forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ExecVal -> Maybe Const
getConst [ExecVal]
args forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Const] -> Maybe Const
f)

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

          applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
          applyPrim :: ([ExecVal] -> Maybe ExecVal) -> [ExecVal] -> Maybe (Exec ExecVal)
applyPrim [ExecVal] -> Maybe ExecVal
fn [ExecVal]
args = forall (m :: * -> *) a. Monad m => a -> m a
return 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 ExecEnv
env Context
ctxt [Name]
ns SC
sc [ExecVal]
args =
    let arity :: Int
arity = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
ns in
    if Int
arity forall a. Ord a => a -> a -> Bool
<= forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExecVal]
args
    then do let amap :: ExecEnv
amap = 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 ExecVal
res -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecEnv -> Context -> ExecVal -> [ExecVal] -> Exec ExecVal
execApp (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, ExecVal
tm) -> (Name
n, ExecVal
tm)) ExecEnv
amap forall a. [a] -> [a] -> [a]
++ ExecEnv
env) Context
ctxt ExecVal
res (forall a. Int -> [a] -> [a]
drop Int
arity [ExecVal]
args)
              Maybe ExecVal
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    else forall (m :: * -> *) a. Monad m => a -> m a
return 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' ExecEnv
env Context
ctxt ExecEnv
amap (UnmatchedCase String
_) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
execCase' ExecEnv
env Context
ctxt ExecEnv
amap (STerm TT Name
tm) =
    forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecEnv -> Context -> TT Name -> Exec ExecVal
doExec (forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n, ExecVal
v) -> (Name
n, ExecVal
v)) ExecEnv
amap forall a. [a] -> [a] -> [a]
++ ExecEnv
env) Context
ctxt TT Name
tm
execCase' ExecEnv
env Context
ctxt ExecEnv
amap (Case CaseType
sh Name
n [CaseAlt' (TT Name)]
alts) | Just ExecVal
tm <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n ExecEnv
amap =
       case ExecVal -> [CaseAlt' (TT Name)] -> Maybe (SC, ExecEnv)
chooseAlt ExecVal
tm [CaseAlt' (TT Name)]
alts of
         Just (SC
newCase, ExecEnv
newBindings) ->
             let amap' :: ExecEnv
amap' = ExecEnv
newBindings forall a. [a] -> [a] -> [a]
++ (forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
x,ExecVal
_) -> Bool -> Bool
not (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Name
x (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst ExecEnv
newBindings))) ExecEnv
amap) in
             ExecEnv -> Context -> ExecEnv -> SC -> Exec (Maybe ExecVal)
execCase' ExecEnv
env Context
ctxt ExecEnv
amap' SC
newCase
         Maybe (SC, ExecEnv)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
execCase' ExecEnv
_ Context
_ ExecEnv
_ SC
cse = forall (m :: * -> *) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"The impossible happened: tried to exec  " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SC
cse

chooseAlt :: ExecVal -> [CaseAlt] -> Maybe (SC, [(Name, ExecVal)])
chooseAlt :: ExecVal -> [CaseAlt' (TT Name)] -> Maybe (SC, ExecEnv)
chooseAlt ExecVal
tm (DefaultCase SC
sc : [CaseAlt' (TT Name)]
alts) | ExecVal -> Bool
ok ExecVal
tm = forall a. a -> Maybe a
Just (SC
sc, [])
                                     | Bool
otherwise = forall a. Maybe a
Nothing
  where -- Default cases should only work on applications of constructors or on constants
        ok :: ExecVal -> Bool
ok (EApp ExecVal
f ExecVal
x) = ExecVal -> Bool
ok ExecVal
f
        ok (EP NameType
Bound Name
_ ExecVal
_) = Bool
False
        ok (EP NameType
Ref Name
_ ExecVal
_) = Bool
False
        ok ExecVal
_ = Bool
True


chooseAlt (EConstant Const
c) (ConstCase Const
c' SC
sc : [CaseAlt' (TT Name)]
alts) | Const
c forall a. Eq a => a -> a -> Bool
== Const
c' = forall a. a -> Maybe a
Just (SC
sc, [])
chooseAlt ExecVal
tm (ConCase Name
n Int
i [Name]
ns SC
sc : [CaseAlt' (TT Name)]
alts) | ((EP NameType
_ Name
cn ExecVal
_), [ExecVal]
args) <- ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
tm
                                        , Name
cn forall a. Eq a => a -> a -> Bool
== Name
n = forall a. a -> Maybe a
Just (SC
sc, forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
ns [ExecVal]
args)
                                        | Bool
otherwise = ExecVal -> [CaseAlt' (TT Name)] -> Maybe (SC, ExecEnv)
chooseAlt ExecVal
tm [CaseAlt' (TT Name)]
alts
chooseAlt ExecVal
tm (CaseAlt' (TT Name)
_:[CaseAlt' (TT Name)]
alts) = ExecVal -> [CaseAlt' (TT Name)] -> Maybe (SC, ExecEnv)
chooseAlt ExecVal
tm [CaseAlt' (TT Name)]
alts
chooseAlt ExecVal
_ [] = forall a. Maybe a
Nothing


data Foreign = FFun String [(FDesc, ExecVal)] FDesc deriving Int -> Foreign -> ShowS
[Foreign] -> ShowS
Foreign -> String
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 Name
c)
    | Name
c forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_Str" = FType
FString
    | Name
c forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_Float" = ArithTy -> FType
FArith ArithTy
ATFloat
    | Name
c forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_Ptr" = FType
FPtr
    | Name
c forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_MPtr" = FType
FManagedPtr
    | Name
c forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_Unit" = FType
FUnit
toFType (FApp Name
c [FDesc
_,FDesc
ity])
    | Name
c forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_IntT" = ArithTy -> FType
FArith (FDesc -> ArithTy
toAType FDesc
ity)
  where toAType :: FDesc -> ArithTy
toAType (FCon Name
i)
          | Name
i forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_IntChar" = IntTy -> ArithTy
ATInt IntTy
ITChar
          | Name
i forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_IntNative" = IntTy -> ArithTy
ATInt IntTy
ITNative
          | Name
i forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_IntBits8" = IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT8)
          | Name
i forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_IntBits16" = IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT16)
          | Name
i forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_IntBits32" = IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT32)
          | Name
i forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_IntBits64" = IntTy -> ArithTy
ATInt (NativeTy -> IntTy
ITFixed NativeTy
IT64)
        toAType FDesc
t = forall a. HasCallStack => String -> a
error (forall a. Show a => a -> String
show FDesc
t forall a. [a] -> [a] -> [a]
++ String
" not defined in toAType")

toFType (FApp Name
c [FDesc
_])
    | Name
c forall a. Eq a => a -> a -> Bool
== String -> Name
sUN String
"C_Any" = FType
FAny
toFType FDesc
t = forall a. HasCallStack => String -> a
error (forall a. Show a => a -> String
show FDesc
t forall a. [a] -> [a] -> [a]
++ String
" not defined in toFType")

call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
call :: Foreign -> [ExecVal] -> Exec (Maybe ExecVal)
call (FFun String
name [(FDesc, ExecVal)]
argTypes FDesc
retType) [ExecVal]
args =
    do Maybe ForeignFun
fn <- String -> Exec (Maybe ForeignFun)
findForeign String
name
       forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)
             (\ForeignFun
f -> forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExecVal -> ExecVal
ioWrap forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
call' ForeignFun
f [ExecVal]
args (FDesc -> FType
toFType FDesc
retType)) Maybe ForeignFun
fn
    where call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
          call' :: ForeignFun -> [ExecVal] -> FType -> Exec ExecVal
call' (Fun String
_ FunPtr a
h) [ExecVal]
args (FArith (ATInt IntTy
ITNative)) = do
            CInt
res <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CInt
retCInt ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
            forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Int -> Const
I (forall a b. (Integral a, Num b) => a -> b
fromIntegral CInt
res)))
          call' (Fun String
_ FunPtr a
h) [ExecVal]
args (FArith (ATInt (ITFixed NativeTy
IT8))) = do
            CChar
res <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CChar
retCChar ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
            forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Word8 -> Const
B8 (forall a b. (Integral a, Num b) => a -> b
fromIntegral CChar
res)))
          call' (Fun String
_ FunPtr a
h) [ExecVal]
args (FArith (ATInt (ITFixed NativeTy
IT16))) = do
            CWchar
res <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CWchar
retCWchar ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
            forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Word16 -> Const
B16 (forall a b. (Integral a, Num b) => a -> b
fromIntegral CWchar
res)))
          call' (Fun String
_ FunPtr a
h) [ExecVal]
args (FArith (ATInt (ITFixed NativeTy
IT32))) = do
            CInt
res <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CInt
retCInt ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
            forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Word32 -> Const
B32 (forall a b. (Integral a, Num b) => a -> b
fromIntegral CInt
res)))
          call' (Fun String
_ FunPtr a
h) [ExecVal]
args (FArith (ATInt (ITFixed NativeTy
IT64))) = do
            CLong
res <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CLong
retCLong ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
            forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Word64 -> Const
B64 (forall a b. (Integral a, Num b) => a -> b
fromIntegral CLong
res)))
          call' (Fun String
_ FunPtr a
h) [ExecVal]
args (FArith ArithTy
ATFloat) = do
            CDouble
res <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CDouble
retCDouble ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
            forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Double -> Const
Fl (forall a b. (Real a, Fractional b) => a -> b
realToFrac CDouble
res)))
          call' (Fun String
_ FunPtr a
h) [ExecVal]
args (FArith (ATInt IntTy
ITChar)) = do
            CChar
res <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType CChar
retCChar ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
            forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (Char -> Const
Ch (CChar -> Char
castCCharToChar CChar
res)))
          call' (Fun String
_ FunPtr a
h) [ExecVal]
args FType
FString = do CString
res <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ 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 forall a. Eq a => a -> a -> Bool
== forall a. Ptr a
nullPtr
                                               then forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Ptr a -> ExecVal
EPtr CString
res)
                                               else do String
hStr <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ CString -> IO String
peekCString CString
res
                                                       forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> ExecVal
EConstant (String -> Const
Str String
hStr))

          call' (Fun String
_ FunPtr a
h) [ExecVal]
args FType
FPtr = forall a. Ptr a -> ExecVal
EPtr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h (forall a. RetType a -> RetType (Ptr a)
retPtr RetType ()
retVoid) ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args))
          call' (Fun String
_ FunPtr a
h) [ExecVal]
args FType
FUnit = do ()
_ <- forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall a b. FunPtr a -> RetType b -> [Arg] -> IO b
callFFI FunPtr a
h RetType ()
retVoid ([ExecVal] -> [Arg]
prepArgs [ExecVal]
args)
                                          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ NameType -> Name -> ExecVal -> ExecVal
EP NameType
Ref Name
unitCon ExecVal
EErased
          call' ForeignFun
_ [ExecVal]
_ FType
_ = forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"the impossible happened in call' in Execute.hs"

          prepArgs :: [ExecVal] -> [Arg]
prepArgs = forall a b. (a -> b) -> [a] -> [b]
map ExecVal -> Arg
prepArg
          prepArg :: ExecVal -> Arg
prepArg (EConstant (I Int
i)) = CInt -> Arg
argCInt (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i)
          prepArg (EConstant (B8 Word8
i)) = CChar -> Arg
argCChar (forall a b. (Integral a, Num b) => a -> b
fromIntegral Word8
i)
          prepArg (EConstant (B16 Word16
i)) = CWchar -> Arg
argCWchar (forall a b. (Integral a, Num b) => a -> b
fromIntegral Word16
i)
          prepArg (EConstant (B32 Word32
i)) = CInt -> Arg
argCInt (forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
i)
          prepArg (EConstant (B64 Word64
i)) = CLong -> Arg
argCLong (forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
i)
          prepArg (EConstant (Fl Double
f)) = CDouble -> Arg
argCDouble (forall a b. (Real a, Fractional b) => a -> b
realToFrac Double
f)
          prepArg (EConstant (Ch Char
c)) = CChar -> Arg
argCChar (Char -> CChar
castCharToCChar Char
c) -- 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 String
s)) = String -> Arg
argString String
s
          prepArg (EPtr Ptr a
p) = forall a. Ptr a -> Arg
argPtr Ptr a
p
          prepArg ExecVal
other = forall a. String -> a -> a
trace (String
"Could not use " forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [a]
take Int
100 (forall a. Show a => a -> String
show ExecVal
other) forall a. [a] -> [a] -> [a]
++ String
" as FFI arg.") forall a. HasCallStack => a
undefined


foreignFromTT :: Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT :: Int -> ExecVal -> ExecVal -> [ExecVal] -> Maybe Foreign
foreignFromTT Int
arity ExecVal
ty (EConstant (Str String
name)) [ExecVal]
args
    = do [(FDesc, ExecVal)]
argFTyVals <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ExecVal -> Maybe (FDesc, ExecVal)
splitArg (forall a. Int -> [a] -> [a]
take Int
arity [ExecVal]
args)
         forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> [(FDesc, ExecVal)] -> FDesc -> Foreign
FFun String
name [(FDesc, ExecVal)]
argFTyVals (ExecVal -> FDesc
toFDesc ExecVal
ty)
foreignFromTT Int
arity ExecVal
ty ExecVal
fn [ExecVal]
args = forall a. String -> a -> a
trace (String
"failed to construct ffun from " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (ExecVal
ty,ExecVal
fn,[ExecVal]
args)) forall a. Maybe a
Nothing

unEList :: ExecVal -> Maybe [ExecVal]
unEList :: ExecVal -> Maybe [ExecVal]
unEList ExecVal
tm = case ExecVal -> (ExecVal, [ExecVal])
unApplyV ExecVal
tm of
               (ExecVal
nil, [ExecVal
_]) -> forall a. a -> Maybe a
Just []
               (ExecVal
cons, ([ExecVal
_, ExecVal
x, ExecVal
xs])) ->
                   do [ExecVal]
rest <- ExecVal -> Maybe [ExecVal]
unEList ExecVal
xs
                      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ExecVal
xforall a. a -> [a] -> [a]
:[ExecVal]
rest
               (ExecVal
f, [ExecVal]
args) -> forall a. Maybe a
Nothing


mapMaybeM :: (Functor m, Monad m) => (a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM :: forall (m :: * -> *) a b.
(Functor m, Monad m) =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM a -> m (Maybe b)
f [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
mapMaybeM a -> m (Maybe b)
f (a
x:[a]
xs) = do [b]
rest <- forall (m :: * -> *) a b.
(Functor m, Monad m) =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM a -> m (Maybe b)
f [a]
xs
                        forall b a. b -> (a -> b) -> Maybe a -> b
maybe [b]
rest (forall a. a -> [a] -> [a]
:[b]
rest) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m (Maybe b)
f a
x
findForeign :: String -> Exec (Maybe ForeignFun)
findForeign :: String -> Exec (Maybe ForeignFun)
findForeign String
fn = do ExecState
est <- Exec ExecState
getExecState
                    let libs :: [DynamicLib]
libs = ExecState -> [DynamicLib]
exec_dynamic_libs ExecState
est
                    [ForeignFun]
fns <- forall (m :: * -> *) a b.
(Functor m, Monad m) =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM DynamicLib -> Exec (Maybe ForeignFun)
getFn [DynamicLib]
libs
                    case [ForeignFun]
fns of
                      [ForeignFun
f] -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just ForeignFun
f)
                      [] -> do forall a. IO a -> Exec a
execIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Symbol \"" forall a. [a] -> [a] -> [a]
++ String
fn forall a. [a] -> [a] -> [a]
++ String
"\" not found"
                               forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
                      [ForeignFun]
fs -> do forall a. IO a -> Exec a
execIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"Symbol \"" forall a. [a] -> [a] -> [a]
++ String
fn forall a. [a] -> [a] -> [a]
++ String
"\" is ambiguous. Found " forall a. [a] -> [a] -> [a]
++
                                                   forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [ForeignFun]
fs) forall a. [a] -> [a] -> [a]
++ String
" occurrences."
                               forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    where getFn :: DynamicLib -> Exec (Maybe ForeignFun)
getFn DynamicLib
lib = forall a. IO a -> Exec a
execIO forall a b. (a -> b) -> a -> b
$ forall a. IO a -> (IOError -> IO a) -> IO a
catchIO (String -> DynamicLib -> IO (Maybe ForeignFun)
tryLoadFn String
fn DynamicLib
lib) (\IOError
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing)

#endif