0 | module Control.Linear.Network
  1 |
  2 | -- An experimental linear type based API to sockets
  3 |
  4 | import public Data.Either
  5 | import public Data.Linear.LEither
  6 | import public Data.Maybe
  7 |
  8 | import Control.Linear.LIO
  9 |
 10 | import public Network.Socket.Data
 11 | import Network.Socket
 12 |
 13 | public export
 14 | data SocketState = Ready | Bound | Listening | Open | Closed
 15 |
 16 | ||| Define the domain of SocketState transitions.
 17 | ||| Label every such transition.
 18 | public export
 19 | data Action : SocketState -> Type where
 20 |   Bind    : Action Ready
 21 |   Listen  : Action Bound
 22 |   Accept  : Action Listening
 23 |   Connect : Action Ready
 24 |   Send    : Action Open
 25 |   Receive : Action Open
 26 |   Close   : Action st
 27 |
 28 | export
 29 | data Socket : SocketState -> Type where
 30 |      MkSocket : Socket.Data.Socket -> Socket st
 31 |
 32 | ||| For every label of a SocketState transition
 33 | ||| and a success value of the transition,
 34 | ||| define its result.
 35 | public export
 36 | Next : (action : Action st)
 37 |     -> (success : Bool)
 38 |     -> Type
 39 | Next Bind    True  = Socket Bound
 40 | Next Listen  True  = Socket Listening
 41 | Next Accept  True  = LPair (Socket Listening) (Socket Open)
 42 | Next Connect True  = Socket Open
 43 | Next Send    True  = Socket Open
 44 | Next Receive True  = Socket Open
 45 | Next Close   True  = Socket Closed
 46 | Next _       False = Socket Closed
 47 |
 48 | export
 49 | newSocket : LinearIO io
 50 |       => (fam  : SocketFamily)
 51 |       -> (ty   : SocketType)
 52 |       -> (pnum : ProtocolNumber)
 53 |       -> (1 f : (1 sock : LEither (!* SocketError) (Socket Ready)) -> L io a)
 54 |       -> L io a
 55 | newSocket fam ty pnum f
 56 |     = do Right rawsock <- socket fam ty pnum
 57 |                | Left err => f (Left $ MkBang err)
 58 |          f (Right $ MkSocket rawsock)
 59 |
 60 | export
 61 | close : LinearIO io => (1 sock : Socket st) -> L1 io (Socket Closed)
 62 | close (MkSocket sock)
 63 |     = do Socket.close sock
 64 |          pure1 (MkSocket sock)
 65 |
 66 | export
 67 | done : LinearIO io => (1 sock : Socket Closed) -> L io ()
 68 | done (MkSocket sock) = pure ()
 69 |
 70 | export
 71 | bind : LinearIO io =>
 72 |        (1 sock : Socket Ready) ->
 73 |        (addr : Maybe SocketAddress) ->
 74 |        (port : Port) ->
 75 |        L1 io (Res (Maybe SocketError)
 76 |          (\res => Next Bind (isNothing res)))
 77 | bind (MkSocket sock) addr port
 78 |     = do code <- Socket.bind sock addr port
 79 |          case code of
 80 |            0 =>
 81 |              pure1 $ Nothing # MkSocket sock
 82 |            err =>
 83 |              pure1 $ Just err # MkSocket sock
 84 |
 85 | export
 86 | connect : LinearIO io =>
 87 |           (1 sock : Socket Ready) ->
 88 |           (addr : SocketAddress) ->
 89 |           (port : Port) ->
 90 |           L1 io (Res (Maybe SocketError)
 91 |             (\res => Next Connect (isNothing res)))
 92 | connect (MkSocket sock) addr port
 93 |     = do code <- Socket.connect sock addr port
 94 |          case code of
 95 |            0 =>
 96 |              pure1 $ Nothing # MkSocket sock
 97 |            err =>
 98 |              pure1 $ Just err # MkSocket sock
 99 |
100 | export
101 | listen : LinearIO io =>
102 |          (1 sock : Socket Bound) ->
103 |          L1 io (Res (Maybe SocketError)
104 |            (\res => Next Listen (isNothing res)))
105 | listen (MkSocket sock)
106 |     = do code <- Socket.listen sock
107 |          case code of
108 |            0 =>
109 |              pure1 $ Nothing # MkSocket sock
110 |            err =>
111 |              pure1 $ Just err # MkSocket sock
112 |
113 |
114 | export
115 | accept : LinearIO io =>
116 |          (1 sock : Socket Listening) ->
117 |          L1 io (Res (Maybe SocketError)
118 |            (\res => Next Accept (isNothing res)))
119 | accept (MkSocket sock)
120 |     = do Right (sock', sockaddr) <- Socket.accept sock
121 |              | Left err => pure1 (Just err # MkSocket sock)
122 |          pure1 (Nothing # (MkSocket sock # MkSocket sock'))
123 |
124 | export
125 | send : LinearIO io =>
126 |        (1 sock : Socket Open) ->
127 |        (msg : String) ->
128 |        L1 io (Res (Maybe SocketError)
129 |          (\res => Next Send (isNothing res)))
130 | send (MkSocket sock) msg
131 |     = do Right c <- Socket.send sock msg
132 |              | Left err => pure1 (Just err # MkSocket sock)
133 |          pure1 (Nothing # MkSocket sock)
134 |
135 | export
136 | recv : LinearIO io =>
137 |        (1 sock : Socket Open) ->
138 |        (len : ByteLength) ->
139 |        L1 io (Res (Either SocketError (String, ResultCode))
140 |          (\res => Next Receive (isRight res)))
141 | recv (MkSocket sock) len
142 |     = do Right msg <- Socket.recv sock len
143 |              | Left err => pure1 (Left err # MkSocket sock)
144 |          pure1 (Right msg # MkSocket sock)
145 |
146 | export
147 | recvAll : LinearIO io =>
148 |           (1 sock : Socket Open) ->
149 |           L1 io (Res (Either SocketError String)
150 |             (\res => Next Receive (isRight res)))
151 | recvAll (MkSocket sock)
152 |     = do Right msg <- Socket.recvAll sock
153 |              | Left err => pure1 (Left err # MkSocket sock)
154 |          pure1 (Right msg # MkSocket sock)
155 |
156 | export
157 | sendBytes : LinearIO io =>
158 |             (1 sock : Socket Open) ->
159 |             (msg : List Bits8) ->
160 |             L1 io (Res (Maybe SocketError)
161 |               (\res => Next Send (isNothing res)))
162 | sendBytes (MkSocket sock) msg
163 |     = do Right c <- Socket.sendBytes sock msg
164 |              | Left err => pure1 (Just err # MkSocket sock)
165 |          pure1 (Nothing # MkSocket sock)
166 |
167 | export
168 | recvBytes : LinearIO io =>
169 |             (1 sock : Socket Open) ->
170 |             (len : ByteLength) ->
171 |             L1 io (Res (Either SocketError (List Bits8))
172 |               (\res => Next Receive (isRight res)))
173 | recvBytes (MkSocket sock) len
174 |     = do Right msg <- Socket.recvBytes sock len
175 |              | Left err => pure1 (Left err # MkSocket sock)
176 |          pure1 (Right msg # MkSocket sock)
177 |
178 | export
179 | recvAllBytes : LinearIO io =>
180 |               (1 sock : Socket Open) ->
181 |               L1 io (Res (Either SocketError (List Bits8))
182 |                 (\res => Next Receive (isRight res)))
183 | recvAllBytes (MkSocket sock)
184 |     = do Right msg <- Socket.recvAllBytes sock
185 |              | Left err => pure1 (Left err # MkSocket sock)
186 |          pure1 (Right msg # MkSocket sock)
187 |