idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 19:13:02 +03:00
Code Issues Projects Releases Wiki Activity

Seemingly outdated and non-typechecking module was removed.

Browse Source
This commit is contained in:
Denis Buzdalov 2021-02-01 18:56:57 +03:00 committed by G. Allais
parent 173edb14a6
commit 5beda25da6
1 changed files with 0 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
libs/base/Control/App/Network.idr
View File

@ -1,28 +0,0 @@
module Control.App.Network
import Control.App
import Control.App.Network.Data
data SocketState = Ready | Bound | Listening | Open | Closed
data Socket : SocketState -> Type where
MkSocket : Int -> Socket s
data NetworkError = Foo
interface Has [Exception NetworkError] e => Network e where
newSocket : (1 p : (1 s : Socket Ready) -> App e a) -> App e a
done : (1 s : Socket Closed) -> App e ()
bind : (1 sock : Socket Ready) ->
(addr : Maybe SocketAddress) -> (port : Port) ->
Either NetworkError (Socket Bound)
{-
connect : (sock : Socket) -> (addr : SocketAddress) -> (port : Port) -> IO ResultCode
listen : (sock : Socket) -> IO Int
accept : (sock : Socket) -> IO (Either SocketError (Socket, SocketAddress))
send : (sock : Socket) -> (msg : String) -> IO (Either SocketError ResultCode)
recv : (sock : Socket) -> (len : ByteLength) -> IO (Either SocketError (String, ResultCode))
close : Socket -> IO ()
-}