mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-21 11:51:31 +03:00
e6121e0935
This is the result of running the command:
$ find . -name '*.idr' -type f -exec sed -i -E 's/\s+$//' {} +
I confirmed before running it that this would not affect any markdown
formatting in documentation comments.
97 lines
2.4 KiB
Idris
97 lines
2.4 KiB
Idris
module PrimIO
|
|
|
|
import Builtin
|
|
|
|
public export
|
|
data IORes : Type -> Type where
|
|
MkIORes : (result : a) -> (1 x : %World) -> IORes a
|
|
|
|
export
|
|
data IO : Type -> Type where
|
|
MkIO : (1 fn : (1 x : %World) -> IORes a) -> IO a
|
|
|
|
export
|
|
io_pure : a -> IO a
|
|
io_pure x = MkIO (\w => MkIORes x w)
|
|
|
|
export
|
|
io_bind : (1 act : IO a) -> (1 k : a -> IO b) -> IO b
|
|
io_bind (MkIO fn)
|
|
= \k => MkIO (\w => let MkIORes x' w' = fn w
|
|
MkIO res = k x' in
|
|
res w')
|
|
|
|
public export
|
|
PrimIO : Type -> Type
|
|
PrimIO a = (1 x : %World) -> IORes a
|
|
|
|
%extern prim__putStr : String -> (1 x : %World) -> IORes ()
|
|
%extern prim__getStr : (1 x : %World) -> IORes String
|
|
|
|
-- A pointer representing a given parameter type
|
|
-- The parameter is a phantom type, to help differentiate between
|
|
-- different pointer types
|
|
public export
|
|
data Ptr : Type -> Type where
|
|
|
|
-- A pointer to any type (representing a void* in foreign calls)
|
|
public export
|
|
data AnyPtr : Type where
|
|
|
|
public export
|
|
data ThreadID : Type where
|
|
|
|
public export
|
|
data FArgList : Type where
|
|
Nil : FArgList
|
|
(::) : {a : Type} -> (1 arg : a) -> (1 args : FArgList) -> FArgList
|
|
|
|
%extern prim__cCall : (ret : Type) -> String -> (1 args : FArgList) ->
|
|
(1 x : %World) -> IORes ret
|
|
%extern prim__schemeCall : (ret : Type) -> String -> (1 args : FArgList) ->
|
|
(1 x : %World) -> IORes ret
|
|
|
|
export %inline
|
|
primIO : (1 fn : (1 x : %World) -> IORes a) -> IO a
|
|
primIO op = MkIO op
|
|
|
|
export %inline
|
|
toPrim : IO a -> PrimIO a
|
|
toPrim (MkIO fn) = fn
|
|
|
|
export %inline
|
|
schemeCall : (ret : Type) -> String -> (1 args : FArgList) -> IO ret
|
|
schemeCall ret fn args = primIO (prim__schemeCall ret fn args)
|
|
|
|
export %inline
|
|
cCall : (ret : Type) -> String -> FArgList -> IO ret
|
|
cCall ret fn args = primIO (prim__cCall ret fn args)
|
|
|
|
export
|
|
putStr : String -> IO ()
|
|
putStr str = primIO (prim__putStr str)
|
|
|
|
export
|
|
putStrLn : String -> IO ()
|
|
putStrLn str = putStr (prim__strAppend str "\n")
|
|
|
|
export
|
|
getLine : IO String
|
|
getLine = primIO prim__getStr
|
|
|
|
export
|
|
fork : (1 prog : IO ()) -> IO ThreadID
|
|
fork (MkIO act) = schemeCall ThreadID "blodwen-thread" [act]
|
|
|
|
unsafeCreateWorld : (1 f : (1 x : %World) -> a) -> a
|
|
unsafeCreateWorld f = f %MkWorld
|
|
|
|
unsafeDestroyWorld : (1 x : %World) -> a -> a
|
|
unsafeDestroyWorld %MkWorld x = x
|
|
|
|
export
|
|
unsafePerformIO : IO a -> a
|
|
unsafePerformIO (MkIO f)
|
|
= unsafeCreateWorld (\w => case f w of
|
|
MkIORes res w' => unsafeDestroyWorld w' res)
|