mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 16:51:51 +03:00
854804dbfb
We need to check below top level too, since there could be holes that we're happy to resolve by searching. The linearity test added illustrates a place where this is needed.
36 lines
1.2 KiB
Idris
36 lines
1.2 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 <- liftIO {io=(L io {use=Unrestricted})} $
|
|
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 <- liftIO {io=(L io {use=Unrestricted})} $
|
|
Socket.bind sock addr port
|
|
if ok == 0
|
|
then pure1 (True # ?foo1)
|
|
else pure1 (False # ?foo2)
|