git.iko.soy/Idris-dev
on fd5dfd9 help sign in
Idris-dev/samples/ST/Net/Network.idr
106 lines 3.9 kB history raw
1module Network
3import Control.ST
4import Network.Socket
6public export
7data SocketState = Ready
8 | Bound
9 | Listening
10 | Open
11 | Closed
13public export
14data CloseOK : SocketState -> Type where
15 CloseOpen : CloseOK Open
16 CloseListening : CloseOK Listening
18-- Sockets API. By convention, the methods return 'Left' on failure or
19-- 'Right' on success (even if the error/result is merely unit).
20public export
21interface Sockets (m : Type -> Type) where
22 Sock : SocketState -> Type
24 -- Create a new socket. If successful, it's in the Closed state
25 socket : SocketType ->
26 ST m (Either () Var) [addIfRight (Sock Ready)]
28 -- Bind a socket to a port. If successful, it's moved to the Bound state.
29 bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->
30 ST m (Either () ())
31 [sock ::: Sock Ready :-> (Sock Closed `or` Sock Bound)]
32 -- Listen for connections on a socket. If successful, it's moved to the
33 -- Listening state
34 listen : (sock : Var) ->
35 ST m (Either () ())
36 [sock ::: Sock Bound :-> (Sock Closed `or` Sock Listening)]
37 -- Accept an incoming connection on a Listening socket. If successful,
38 -- creates a new socket in the Open Server state, and keeps the existing
39 -- socket in the Listening state
40 accept : (sock : Var) ->
41 ST m (Either () Var)
42 [sock ::: Sock Listening, addIfRight (Sock Open)]
44 -- Connect to a remote address on a socket. If successful, moves to the
45 -- Open Client state
46 connect : (sock : Var) -> SocketAddress -> Port ->
47 ST m (Either () ())
48 [sock ::: Sock Ready :-> (Sock Closed `or` Sock Open)]
50 -- Close an Open or Listening socket
51 close : (sock : Var) ->
52 {auto prf : CloseOK st} ->
53 ST m () [sock ::: Sock st :-> Sock Closed]
55 remove : (sock : Var) ->
56 ST m () [Remove sock (Sock Closed)]
58 -- Send a message on a connected socket.
59 -- On failure, move the socket to the Closed state
60 send : (sock : Var) -> String ->
61 ST m (Either () ())
62 [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]
63 -- Receive a message on a connected socket
64 -- On failure, move the socket to the Closed state
65 recv : (sock : Var) ->
66 ST m (Either () String)
67 [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]
69export
70implementation Sockets IO where
71 Sock _ = State Socket
73 socket ty = do Right sock <- lift $ Socket.socket AF_INET ty 0
74 | Left err => pure (Left ())
75 lbl <- new sock
76 pure (Right lbl)
78 bind sock addr port = do ok <- lift $ bind !(read sock) addr port
79 if ok /= 0
80 then pure (Left ())
81 else pure (Right ())
82 listen sock = do ok <- lift $ listen !(read sock)
83 if ok /= 0
84 then pure (Left ())
85 else pure (Right ())
86 accept sock = do Right (conn, addr) <- lift $ accept !(read sock)
87 | Left err => pure (Left ())
88 lbl <- new conn
89 returning (Right lbl) (toEnd lbl)
91 connect sock addr port
92 = do ok <- lift $ connect !(read sock) addr port
93 if ok /= 0
94 then pure (Left ())
95 else pure (Right ())
96 close sock = do lift $ close !(read sock)
97 pure ()
98 remove sock = delete sock
100 send sock msg = do Right _ <- lift $ send !(read sock) msg
101 | Left _ => pure (Left ())
102 pure (Right ())
103 recv sock = do Right (msg, len) <- lift $ recv !(read sock) 1024 -- Yes, yes...
104 | Left _ => pure (Left ())
105 pure (Right msg)