mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-26 21:23:53 +03:00
ebc413ede5
It's worth delaying in case doing some more work (and some more interface resolution) can make the type more concrete. This makes test linear011 work more smoothly, and will help with this sort of program in general. A better way, later, would be to try elaborating and delay only if the type is not yet known. We have the facilities, but it's too fiddly for me to want to implement it right now...
34 lines
1.0 KiB
Idris
34 lines
1.0 KiB
Idris
import Control.Linear.LIO
|
|
|
|
import Network.Socket
|
|
|
|
data SocketState = Ready | Bound | Listening | Open | Closed
|
|
|
|
data Socket : SocketState -> Type where
|
|
MkSocket : Socket.Data.Socket -> Socket st
|
|
|
|
newSocket : LinearIO io
|
|
=> (fam : SocketFamily)
|
|
-> (ty : SocketType)
|
|
-> (pnum : ProtocolNumber)
|
|
-> (success : (1 _ : Socket Ready) -> L io ())
|
|
-> (fail : SocketError -> L io ())
|
|
-> L io ()
|
|
newSocket fam ty pnum success fail
|
|
= do Right rawsock <- socket fam ty pnum
|
|
| Left err => fail err
|
|
success (MkSocket rawsock)
|
|
|
|
bind : LinearIO io =>
|
|
(1 _ : Socket Ready) ->
|
|
(addr : Maybe SocketAddress) ->
|
|
(port : Port) ->
|
|
L io {use=1} (Res Bool (\res => Socket (case res of
|
|
False => Closed
|
|
True => Bound)))
|
|
bind (MkSocket sock) addr port
|
|
= do ok <- Socket.bind sock addr port
|
|
if ok == 0
|
|
then pure1 (True # ?foo1)
|
|
else pure1 (False # ?foo2)
|