{-# LANGUAGE BlockArguments      #-}
{-# LANGUAGE CPP                 #-}
{-# LANGUAGE RecordWildCards     #-}
{-# LANGUAGE TupleSections       #-}

-- | Evaluation of foreign functions.
module Cryptol.Eval.FFI
  ( findForeignDecls
  , evalForeignDecls
  ) where

import Cryptol.Eval.FFI.ForeignSrc
    ( ForeignSrc)
#ifdef FFI_ENABLED
import Cryptol.Eval.FFI.ForeignSrc
    (ForeignImpl, loadForeignImpl )
#else
import Cryptol.Parser.AST (ForeignMode)
#endif
import Cryptol.Eval.FFI.Error ( FFILoadError )
import Cryptol.Eval (Eval, EvalEnv )
import Cryptol.TypeCheck.AST
    ( FFI(..), TVar(TVBound), findForeignDecls )
import Cryptol.TypeCheck.FFI.FFIType ( FFIFunType(..) )

#ifdef FFI_ENABLED

import           Data.Either(partitionEithers)
import           Data.Traversable(for)
import           Cryptol.Backend.Concrete
import           Cryptol.Backend.Monad
import           Cryptol.Eval.Env
import           Cryptol.Eval.Prims
import           Cryptol.Eval.Type
import           Cryptol.Eval.Value
import           Cryptol.ModuleSystem.Name
import           Cryptol.Utils.Ident
import           Cryptol.Eval.FFI.C(callForeignC)
import           Cryptol.Eval.FFI.Abstract(callForeignAbstract)

#endif

#ifdef FFI_ENABLED

-- | Add the given foreign declarations to the environment, loading their
-- implementations from the given 'ForeignSrc'. If some implementations fail to
-- load then errors are reported for them but any successfully loaded
-- implementations are still added to the environment.
--
-- This is a separate pass from the main evaluation functions in "Cryptol.Eval"
-- since it only works for the Concrete backend.
evalForeignDecls :: ForeignSrc -> [(Name, FFI)] -> EvalEnv ->
  Eval ([FFILoadError], EvalEnv)
evalForeignDecls :: ForeignSrc
-> [(Name, FFI)] -> EvalEnv -> Eval ([FFILoadError], EvalEnv)
evalForeignDecls ForeignSrc
fsrc [(Name, FFI)]
decls EvalEnv
env = IO ([FFILoadError], EvalEnv) -> Eval ([FFILoadError], EvalEnv)
forall a. IO a -> Eval a
io do
  ([FFILoadError]
errs, [(Name, Prim Concrete)]
prims) <- [Either FFILoadError (Name, Prim Concrete)]
-> ([FFILoadError], [(Name, Prim Concrete)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either FFILoadError (Name, Prim Concrete)]
 -> ([FFILoadError], [(Name, Prim Concrete)]))
-> IO [Either FFILoadError (Name, Prim Concrete)]
-> IO ([FFILoadError], [(Name, Prim Concrete)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Name, FFI)]
-> ((Name, FFI) -> IO (Either FFILoadError (Name, Prim Concrete)))
-> IO [Either FFILoadError (Name, Prim Concrete)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(Name, FFI)]
decls \(Name
name, FFI
cc) ->
    (ForeignImpl -> (Name, Prim Concrete))
-> Either FFILoadError ForeignImpl
-> Either FFILoadError (Name, Prim Concrete)
forall a b.
(a -> b) -> Either FFILoadError a -> Either FFILoadError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name
name,) (Prim Concrete -> (Name, Prim Concrete))
-> (ForeignImpl -> Prim Concrete)
-> ForeignImpl
-> (Name, Prim Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FFI -> Name -> ForeignImpl -> Prim Concrete
foreignPrimPoly FFI
cc Name
name) (Either FFILoadError ForeignImpl
 -> Either FFILoadError (Name, Prim Concrete))
-> IO (Either FFILoadError ForeignImpl)
-> IO (Either FFILoadError (Name, Prim Concrete))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      ForeignSrc -> String -> IO (Either FFILoadError ForeignImpl)
loadForeignImpl ForeignSrc
fsrc (Ident -> String
unpackIdent (Ident -> String) -> Ident -> String
forall a b. (a -> b) -> a -> b
$ Name -> Ident
nameIdent Name
name)
  ([FFILoadError], EvalEnv) -> IO ([FFILoadError], EvalEnv)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([FFILoadError]
errs, ((Name, Prim Concrete) -> EvalEnv -> EvalEnv)
-> EvalEnv -> [(Name, Prim Concrete)] -> EvalEnv
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Name -> Prim Concrete -> EvalEnv -> EvalEnv)
-> (Name, Prim Concrete) -> EvalEnv -> EvalEnv
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Prim Concrete -> EvalEnv -> EvalEnv
forall sym.
Backend sym =>
Name -> Prim sym -> GenEvalEnv sym -> GenEvalEnv sym
bindVarDirect) EvalEnv
env [(Name, Prim Concrete)]
prims)

-- | Generate a 'Prim' value representing the given foreign function, containing
-- all the code necessary to marshal arguments and return values and do the
-- actual FFI call.
foreignPrimPoly :: FFI -> Name -> ForeignImpl -> Prim Concrete
foreignPrimPoly :: FFI -> Name -> ForeignImpl -> Prim Concrete
foreignPrimPoly FFI
cc Name
name ForeignImpl
impl =
  case FFI
cc of
    CallC FFIFunType FFIType
t -> FFIFunType FFIType
-> (TypeEnv
    -> [(FFIType, GenValue Concrete)]
    -> SEval Concrete (GenValue Concrete))
-> Prim Concrete
forall t s.
FFIFunType t
-> (TypeEnv -> [(t, GenValue s)] -> SEval s (GenValue s)) -> Prim s
foreignPrim FFIFunType FFIType
t (Name
-> FFIFunType FFIType
-> ForeignImpl
-> TypeEnv
-> [(FFIType, GenValue Concrete)]
-> Eval (GenValue Concrete)
callForeignC Name
name FFIFunType FFIType
t ForeignImpl
impl)
    CallAbstract FFIFunType Type
t -> FFIFunType Type
-> (TypeEnv
    -> [(Type, GenValue Concrete)]
    -> SEval Concrete (GenValue Concrete))
-> Prim Concrete
forall t s.
FFIFunType t
-> (TypeEnv -> [(t, GenValue s)] -> SEval s (GenValue s)) -> Prim s
foreignPrim FFIFunType Type
t (Name
-> FFIFunType Type
-> ForeignImpl
-> TypeEnv
-> [(Type, GenValue Concrete)]
-> Eval (GenValue Concrete)
callForeignAbstract Name
name FFIFunType Type
t ForeignImpl
impl)

-- | Generate a Prim for a foreign functions.
foreignPrim ::
  FFIFunType t ->
  (TypeEnv -> [(t,GenValue s)] -> SEval s (GenValue s)) ->
  Prim s 
foreignPrim :: forall t s.
FFIFunType t
-> (TypeEnv -> [(t, GenValue s)] -> SEval s (GenValue s)) -> Prim s
foreignPrim FFIFunType t
ft TypeEnv -> [(t, GenValue s)] -> SEval s (GenValue s)
k = [TParam] -> TypeEnv -> Prim s
buildNumPoly (FFIFunType t -> [TParam]
forall t. FFIFunType t -> [TParam]
ffiTParams FFIFunType t
ft) TypeEnv
forall a. Monoid a => a
mempty
  where
  buildNumPoly :: [TParam] -> TypeEnv -> Prim s
buildNumPoly (TParam
tp:[TParam]
tps) TypeEnv
tenv = (Nat' -> Prim s) -> Prim s
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
n ->
    [TParam] -> TypeEnv -> Prim s
buildNumPoly [TParam]
tps (TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv
bindTypeVar (TParam -> TVar
TVBound TParam
tp) (Nat' -> Either Nat' TValue
forall a b. a -> Either a b
Left Nat'
n) TypeEnv
tenv)
  buildNumPoly [] TypeEnv
tenv = TypeEnv -> [t] -> [(t, GenValue s)] -> Prim s
buildArgs TypeEnv
tenv (FFIFunType t -> [t]
forall t. FFIFunType t -> [t]
ffiArgTypes FFIFunType t
ft) []

  buildArgs :: TypeEnv -> [t] -> [(t, GenValue s)] -> Prim s
buildArgs TypeEnv
tenv (t
argType:[t]
argTypes) [(t, GenValue s)]
typesAndVals = (GenValue s -> Prim s) -> Prim s
forall sym. (GenValue sym -> Prim sym) -> Prim sym
PStrict \GenValue s
val ->
    TypeEnv -> [t] -> [(t, GenValue s)] -> Prim s
buildArgs TypeEnv
tenv [t]
argTypes ((t
argType,GenValue s
val) (t, GenValue s) -> [(t, GenValue s)] -> [(t, GenValue s)]
forall a. a -> [a] -> [a]
: [(t, GenValue s)]
typesAndVals)
  buildArgs TypeEnv
tenv [] [(t, GenValue s)]
typesAndVals = SEval s (GenValue s) -> Prim s
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (TypeEnv -> [(t, GenValue s)] -> SEval s (GenValue s)
k TypeEnv
tenv ([(t, GenValue s)] -> [(t, GenValue s)]
forall a. [a] -> [a]
reverse [(t, GenValue s)]
typesAndVals))


#else

-- | Dummy implementation for when FFI is disabled. Does not add anything to
-- the environment or report any errors.
evalForeignDecls :: ForeignSrc -> [(Name, FFI)] -> EvalEnv ->
  Eval ([FFILoadError], EvalEnv)
evalForeignDecls _ _ env = pure ([], env)

#endif