mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-11 14:57:30 +03:00
280 lines
8.7 KiB
Idris
280 lines
8.7 KiB
Idris
%unqualified
|
|
|
|
import Builtins
|
|
import Prelude.List
|
|
|
|
%access public
|
|
|
|
||| Idris's primitive IO, for building abstractions on top of
|
|
abstract
|
|
data PrimIO : Type -> Type where
|
|
prim__IO : a -> PrimIO a
|
|
|
|
||| A token representing the world, for use in `IO`
|
|
abstract data World = TheWorld prim__WorldType
|
|
|
|
private
|
|
world : World -> prim__WorldType
|
|
world (TheWorld w) = w
|
|
|
|
abstract WorldRes : Type -> Type
|
|
WorldRes x = x
|
|
|
|
||| An FFI specifier, which describes how a particular compiler
|
|
||| backend handles foreign function calls.
|
|
record FFI where
|
|
constructor MkFFI
|
|
||| A family describing which types are available in the FFI
|
|
ffi_types : Type -> Type
|
|
|
|
||| The type used to specify the names of foreign functions in this FFI
|
|
ffi_fn : Type
|
|
|
|
||| How this FFI describes exported datatypes
|
|
ffi_data : Type
|
|
|
|
||| The IO type, parameterised over the FFI that is available within
|
|
||| it.
|
|
abstract
|
|
data IO' : (lang : FFI) -> Type -> Type where
|
|
MkIO : (World -> PrimIO (WorldRes a)) -> IO' lang a
|
|
|
|
data FTy : FFI -> List Type -> Type -> Type where
|
|
FRet : ffi_types f t -> FTy f xs (IO' f t)
|
|
FFun : ffi_types f s -> FTy f (s :: xs) t -> FTy f xs (s -> t)
|
|
|
|
namespace ForeignEnv
|
|
data FEnv : FFI -> List Type -> Type where
|
|
Nil : FEnv f []
|
|
(::) : (ffi_types f t, t) -> FEnv f xs -> FEnv f (t :: xs)
|
|
|
|
ForeignPrimType : (xs : List Type) -> FEnv ffi xs -> Type -> Type
|
|
ForeignPrimType {ffi} [] [] t = World -> ffi_fn ffi -> ffi_types ffi t -> PrimIO t
|
|
ForeignPrimType {ffi} (x :: xs) ((a, _) :: env) t
|
|
= (ffi_types ffi x, x) -> ForeignPrimType xs env t
|
|
|
|
%inline
|
|
applyEnv : (env : FEnv ffi xs) ->
|
|
ForeignPrimType xs env t ->
|
|
World -> ffi_fn ffi -> ffi_types ffi t -> PrimIO t
|
|
applyEnv [] f = f
|
|
applyEnv (x@(_, _) :: xs) f = applyEnv xs (f x)
|
|
|
|
mkForeignPrim : {xs : _} -> {ffi : _} -> {env : FEnv ffi xs} -> {t : Type} ->
|
|
ForeignPrimType xs env t
|
|
-- compiled as primitive. Compiler assumes argument order, so make it
|
|
-- explicit here.
|
|
|
|
%inline
|
|
foreign_prim : (f : FFI) ->
|
|
(fname : ffi_fn f) -> FTy f xs ty -> FEnv f xs -> ty
|
|
foreign_prim f fname (FRet y) env
|
|
= MkIO (\w => applyEnv env mkForeignPrim w fname y)
|
|
foreign_prim f fname (FFun arg sc) env
|
|
= \x => foreign_prim f fname sc ((arg, x) :: env)
|
|
|
|
||| Call a foreign function.
|
|
|||
|
|
||| The particular semantics of foreign function calls depend on the
|
|
||| Idris compiler backend in use. For the default C backend, see the
|
|
||| documentation for `FFI_C`.
|
|
|||
|
|
||| For more details, please consult [the Idris documentation](http://docs.idris-lang.org/en/latest/reference/ffi.html).
|
|
|||
|
|
||| @ f an FFI descriptor, which is specific to the compiler backend.
|
|
||| @ fname the name of the foreign function
|
|
||| @ ty the Idris type for the foreign function
|
|
||| @ fty an automatically-found proof that the Idris type works with
|
|
||| the FFI in question
|
|
%inline
|
|
foreign : (f : FFI) -> (fname : ffi_fn f) -> (ty : Type) ->
|
|
{auto fty : FTy f [] ty} -> ty
|
|
foreign ffi fname ty {fty} = foreign_prim ffi fname fty []
|
|
|
|
abstract
|
|
prim_io_bind : PrimIO a -> (a -> PrimIO b) -> PrimIO b
|
|
prim_io_bind (prim__IO v) k = k v
|
|
|
|
unsafePerformPrimIO : PrimIO a -> a
|
|
-- compiled as primitive
|
|
|
|
abstract
|
|
prim_io_return : a -> PrimIO a
|
|
prim_io_return x = prim__IO x
|
|
|
|
abstract
|
|
io_bind : IO' l a -> (a -> IO' l b) -> IO' l b
|
|
io_bind (MkIO fn) k
|
|
= MkIO (\w => prim_io_bind (fn w)
|
|
(\ b => case k b of
|
|
MkIO fkb => fkb w))
|
|
|
|
abstract
|
|
io_return : a -> IO' l a
|
|
io_return x = MkIO (\w => prim_io_return x)
|
|
|
|
liftPrimIO : (World -> PrimIO a) -> IO' l a
|
|
liftPrimIO = MkIO
|
|
|
|
call__IO : IO' l a -> PrimIO a
|
|
call__IO (MkIO f) = f (TheWorld prim__TheWorld)
|
|
|
|
-- Concrete type makes it easier to elaborate at top level
|
|
run__IO : IO' l () -> PrimIO ()
|
|
run__IO f = call__IO f
|
|
|
|
unsafePerformIO : IO' ffi a -> a
|
|
unsafePerformIO (MkIO f) = unsafePerformPrimIO
|
|
(prim_io_bind (f (TheWorld prim__TheWorld)) (\ b => prim_io_return b))
|
|
|
|
prim_read : IO' l String
|
|
prim_read = MkIO (\w => prim_io_return (prim__readString (world w)))
|
|
|
|
prim_write : String -> IO' l Int
|
|
prim_write s
|
|
= MkIO (\w => prim_io_return (prim__writeString (world w) s))
|
|
|
|
prim_fread : Ptr -> IO' l String
|
|
prim_fread h = MkIO (\w => prim_io_return (prim__readFile (world w) h))
|
|
|
|
prim_fwrite : Ptr -> String -> IO' l Int
|
|
prim_fwrite h s
|
|
= MkIO (\w => prim_io_return (prim__writeFile (world w) h s))
|
|
|
|
--------- The C FFI
|
|
namespace FFI_C
|
|
data Raw : Type -> Type where
|
|
-- code generated can assume it's compiled just as 't'
|
|
MkRaw : (x : t) -> Raw t
|
|
|
|
-- Tell erasure analysis not to erase the argument
|
|
%used MkRaw x
|
|
|
|
||| Supported C integer types
|
|
data C_IntTypes : Type -> Type where
|
|
C_IntChar : C_IntTypes Char
|
|
C_IntNative : C_IntTypes Int
|
|
C_IntBits8 : C_IntTypes Bits8
|
|
C_IntBits16 : C_IntTypes Bits16
|
|
C_IntBits32 : C_IntTypes Bits32
|
|
C_IntBits64 : C_IntTypes Bits64
|
|
|
|
||| Supported C foreign types
|
|
data C_Types : Type -> Type where
|
|
C_Str : C_Types String
|
|
C_Float : C_Types Float
|
|
C_Ptr : C_Types Ptr
|
|
C_MPtr : C_Types ManagedPtr
|
|
C_Unit : C_Types ()
|
|
C_Any : C_Types (Raw a)
|
|
C_IntT : C_IntTypes i -> C_Types i
|
|
|
|
||| A descriptor for the C FFI. See the constructors of `C_Types`
|
|
||| and `C_IntTypes` for the concrete types that are available.
|
|
FFI_C : FFI
|
|
FFI_C = MkFFI C_Types String String
|
|
|
|
IO : Type -> Type
|
|
IO = IO' FFI_C
|
|
|
|
-- Cannot be relaxed as is used by type providers and they expect IO a
|
|
-- in the first argument.
|
|
run__provider : IO a -> PrimIO a
|
|
run__provider (MkIO f) = f (TheWorld prim__TheWorld)
|
|
|
|
prim_fork : PrimIO () -> PrimIO Ptr
|
|
prim_fork x = prim_io_return prim__vm -- compiled specially
|
|
|
|
namespace IO
|
|
fork : IO' l () -> IO' l Ptr
|
|
fork (MkIO f) = MkIO (\w => prim_io_bind
|
|
(prim_fork (prim_io_bind (f w)
|
|
(\ x => prim_io_return x)))
|
|
(\x => prim_io_return x))
|
|
|
|
forceGC : IO ()
|
|
forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm
|
|
|
|
--------- The Javascript/Node FFI
|
|
|
|
|
|
-- Supported JS foreign types
|
|
mutual
|
|
data JsFn : Type -> Type where
|
|
MkJsFn : (x : t) -> JsFn t
|
|
|
|
data JS_IntTypes : Type -> Type where
|
|
JS_IntChar : JS_IntTypes Char
|
|
JS_IntNative : JS_IntTypes Int
|
|
|
|
data JS_FnTypes : Type -> Type where
|
|
JS_Fn : JS_Types s -> JS_FnTypes t -> JS_FnTypes (s -> t)
|
|
JS_FnIO : JS_Types t -> JS_FnTypes (IO' l t)
|
|
JS_FnBase : JS_Types t -> JS_FnTypes t
|
|
|
|
data JS_Types : Type -> Type where
|
|
JS_Str : JS_Types String
|
|
JS_Float : JS_Types Float
|
|
JS_Ptr : JS_Types Ptr
|
|
JS_Unit : JS_Types ()
|
|
JS_FnT : JS_FnTypes a -> JS_Types (JsFn a)
|
|
JS_IntT : JS_IntTypes i -> JS_Types i
|
|
|
|
-- Tell erasure analysis not to erase the argument. Needs to be outside the
|
|
-- mutual block, since directives are done on the first pass and in the first
|
|
-- pass we only have 'JsFn' and not the constructor.
|
|
%used MkJsFn x
|
|
|
|
||| The JavaScript FFI. The strings naming functions in this API are
|
|
||| JavaScript code snippets, into which the arguments are substituted
|
|
||| for the placeholders `%0`, `%1`, etc.
|
|
FFI_JS : FFI
|
|
FFI_JS = MkFFI JS_Types String String
|
|
|
|
JS_IO : Type -> Type
|
|
JS_IO = IO' FFI_JS
|
|
|
|
|
|
--------- Foreign Exports
|
|
|
|
namespace FFI_Export
|
|
-- It's just like Data.List.Elem, but we don't need all the other stuff
|
|
-- that comes with it, just a proof that a data type is defined.
|
|
data DataDefined : Type -> List (Type, s) -> s -> Type where
|
|
DHere : DataDefined x ((x, t) :: xs) t
|
|
DThere : DataDefined x xs t -> DataDefined x (y :: xs) t
|
|
|
|
data FFI_Base : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where
|
|
FFI_ExpType : {n : ffi_data f} -> (def : DataDefined t xs n) -> FFI_Base f xs t
|
|
FFI_Prim : (prim : ffi_types f t) -> FFI_Base f xs t
|
|
|
|
%used FFI_ExpType n
|
|
%used FFI_ExpType def
|
|
%used FFI_Prim prim
|
|
|
|
data FFI_Exportable : (f : FFI) -> List (Type, ffi_data f) -> Type -> Type where
|
|
FFI_IO : (b : FFI_Base f xs t) -> FFI_Exportable f xs (IO' f t)
|
|
FFI_Fun : (b : FFI_Base f xs s) -> (a : FFI_Exportable f xs t) -> FFI_Exportable f xs (s -> t)
|
|
FFI_Ret : (b : FFI_Base f xs t) -> FFI_Exportable f xs t
|
|
|
|
%used FFI_IO b
|
|
%used FFI_Fun b
|
|
%used FFI_Fun a
|
|
%used FFI_Ret b
|
|
|
|
data FFI_Export : (f : FFI) -> String -> List (Type, ffi_data f) -> Type where
|
|
Data : (x : Type) -> (n : ffi_data f) ->
|
|
(es : FFI_Export f h ((x, n) :: xs)) -> FFI_Export f h xs
|
|
Fun : (fn : t) -> (n : ffi_fn f) -> {auto prf : FFI_Exportable f xs t} ->
|
|
(es : FFI_Export f h xs) -> FFI_Export f h xs
|
|
End : FFI_Export f h xs
|
|
|
|
%used Data x
|
|
%used Data n
|
|
%used Data es
|
|
%used Fun fn
|
|
%used Fun n
|
|
%used Fun es
|
|
%used Fun prf
|
|
|