{-# LANGUAGE CPP #-}
-- | How to call foreign function, following the "abstract" calling convention
module Cryptol.Eval.FFI.Abstract where

#ifdef FFI_ENABLED

import Cryptol.Utils.Panic(panic)
import Cryptol.ModuleSystem.Name(Name)
import Cryptol.TypeCheck.Type(Type(..), TVar(..))
import Cryptol.TypeCheck.FFI.FFIType
import Cryptol.Eval.FFI.ForeignSrc(ForeignImpl)
import Cryptol.Eval.Type(TypeEnv,evalType,evalNumType,finNat')
import Cryptol.Eval.Value
import Cryptol.Backend.Monad
import Cryptol.Backend.Concrete
import Cryptol.Eval.FFI.Abstract.Export(exportSizes,exportValues)
import Cryptol.Eval.FFI.Abstract.Call(runFFI)


-- | Call a foreign function that follows the \"abstract\" calling convention.
callForeignAbstract ::
  Name                           {- ^ Name of foreign function -} ->
  FFIFunType Type                {- ^ FFI type -} ->
  ForeignImpl                    {- ^ Address of foreign worker -} ->
  TypeEnv                        {- ^ Values for numeric type parameters -} ->
  [(Type, GenValue Concrete)]    {- ^ Function arguments -} ->
  Eval (GenValue Concrete)
callForeignAbstract :: Name
-> FFIFunType Type
-> ForeignImpl
-> TypeEnv
-> [(Type, GenValue Concrete)]
-> Eval (GenValue Concrete)
callForeignAbstract Name
nm FFIFunType Type
ty ForeignImpl
impl TypeEnv
tenv [(Type, GenValue Concrete)]
args =
  case TypeEnv -> Type -> Either Nat' TValue
evalType TypeEnv
tenv (FFIFunType Type -> Type
forall t. FFIFunType t -> t
ffiRetType FFIFunType Type
ty) of
    Right TValue
resT ->
      do let targs :: [ExportVal]
targs = [Integer] -> [ExportVal] -> [ExportVal]
exportSizes ((TParam -> Integer) -> [TParam] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map TParam -> Integer
evalFinType (FFIFunType Type -> [TParam]
forall t. FFIFunType t -> [TParam]
ffiTParams FFIFunType Type
ty)) []
         [ExportVal]
allArgs <- [Value] -> [ExportVal] -> Eval [ExportVal]
exportValues (((Type, GenValue Concrete) -> Eval (GenValue Concrete))
-> [(Type, GenValue Concrete)] -> [Eval (GenValue Concrete)]
forall a b. (a -> b) -> [a] -> [b]
map (GenValue Concrete -> Eval (GenValue Concrete)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue Concrete -> Eval (GenValue Concrete))
-> ((Type, GenValue Concrete) -> GenValue Concrete)
-> (Type, GenValue Concrete)
-> Eval (GenValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, GenValue Concrete) -> GenValue Concrete
forall a b. (a, b) -> b
snd) [(Type, GenValue Concrete)]
args) [ExportVal]
targs
         Either ImportErrorMessage (Eval (GenValue Concrete))
mb <- IO (Either ImportErrorMessage (Eval (GenValue Concrete)))
-> Eval (Either ImportErrorMessage (Eval (GenValue Concrete)))
forall a. IO a -> Eval a
io ([ExportVal]
-> TValue -> ForeignImpl -> IO (Either ImportErrorMessage Value)
runFFI [ExportVal]
allArgs TValue
resT ForeignImpl
impl)
         case Either ImportErrorMessage (Eval (GenValue Concrete))
mb of
           Right Eval (GenValue Concrete)
a -> Eval (GenValue Concrete)
a
           Left ImportErrorMessage
err -> Concrete -> EvalError -> Value
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
forall a. Concrete -> EvalError -> SEval Concrete a
raiseError Concrete
Concrete (ImportErrorMessage -> EvalError
FFIImportError ImportErrorMessage
err)
    Left Nat'
_ -> String -> [String] -> Eval (GenValue Concrete)
forall a. HasCallStack => String -> [String] -> a
panic String
"callForeginAbstract" [String
"Result type is a number"]


   where
   evalFinType :: TParam -> Integer
evalFinType = Nat' -> Integer
finNat' (Nat' -> Integer) -> (TParam -> Nat') -> TParam -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeEnv -> Type -> Nat'
evalNumType TypeEnv
tenv (Type -> Nat') -> (TParam -> Type) -> TParam -> Nat'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TVar -> Type
TVar (TVar -> Type) -> (TParam -> TVar) -> TParam -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TParam -> TVar
TVBound

#endif