idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-21 10:18:23 +03:00
Code Issues Projects Releases Wiki Activity

Introduce aliases L0 & L1 as specialised versions of L

Browse Source
This commit is contained in:
Ruslan Feizerakhmanov 2021-04-08 20:19:33 +03:00 committed by G. Allais
parent 8d806552b0
commit 0cef4e3743
2 changed files with 16 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
libs/contrib/Control/Linear/LIO.idr
View File

@ -49,6 +49,14 @@ data L : (io : Type -> Type) ->
(1 _ : ContType io u_act u_k a b) ->
L io {use=u_k} b
public export
L0 : (io : Type -> Type) -> (ty : Type) -> Type
L0 io ty = L io {use = 0} ty
public export
L1 : (io : Type -> Type) -> (ty : Type) -> Type
L1 io ty = L io {use = 1} ty
ContType io None u_k a b = (0 _ : a) -> L io {use=u_k} b
ContType io Linear u_k a b = (1 _ : a) -> L io {use=u_k} b
ContType io Unrestricted u_k a b = a -> L io {use=u_k} b

16
libs/network/Control/Linear/Network.idr
View File

@ -57,7 +57,7 @@ newSocket fam ty pnum success fail
success (MkSocket rawsock)
export
close : LinearIO io => (1 sock : Socket st) -> L io {use=1} (Socket Closed)
close : LinearIO io => (1 sock : Socket st) -> L1 io (Socket Closed)
close (MkSocket sock)
= do Socket.close sock
pure1 (MkSocket sock)
@ -71,7 +71,7 @@ bind : LinearIO io =>
(1 sock : Socket Ready) ->
(addr : Maybe SocketAddress) ->
(port : Port) ->
L io {use=1} (Res (Maybe SocketError)
L1 io (Res (Maybe SocketError)
(\res => Next Bind (isNothing res)))
bind (MkSocket sock) addr port
= do code <- Socket.bind sock addr port
@ -86,7 +86,7 @@ connect : LinearIO io =>
(sock : Socket) ->
(addr : SocketAddress) ->
(port : Port) ->
L io {use=1} (Res (Maybe SocketError)
L1 io (Res (Maybe SocketError)
(\case Nothing => Socket Ready
Just _ => Socket Closed))
connect sock addr port
@ -100,7 +100,7 @@ connect sock addr port
export
listen : LinearIO io =>
(1 sock : Socket Bound) ->
L io {use=1} (Res (Maybe SocketError)
L1 io (Res (Maybe SocketError)
(\res => Next Listen (isNothing res)))
listen (MkSocket sock)
= do code <- Socket.listen sock
@ -114,7 +114,7 @@ listen (MkSocket sock)
export
accept : LinearIO io =>
(1 sock : Socket Listening) ->
L io {use=1} (Res (Maybe SocketError)
L1 io (Res (Maybe SocketError)
(\res => Next Accept (isNothing res)))
accept (MkSocket sock)
= do Right (sock', sockaddr) <- Socket.accept sock
@ -125,7 +125,7 @@ export
send : LinearIO io =>
(1 sock : Socket Open) ->
(msg : String) ->
L io {use=1} (Res (Maybe SocketError)
L1 io (Res (Maybe SocketError)
(\res => Next Send (isNothing res)))
send (MkSocket sock) msg
= do Right c <- Socket.send sock msg
@ -136,7 +136,7 @@ export
recv : LinearIO io =>
(1 sock : Socket Open) ->
(len : ByteLength) ->
L io {use=1} (Res (Either SocketError (String, ResultCode))
L1 io (Res (Either SocketError (String, ResultCode))
(\res => Next Receive (isRight res)))
recv (MkSocket sock) len
= do Right msg <- Socket.recv sock len
@ -146,7 +146,7 @@ recv (MkSocket sock) len
export
recvAll : LinearIO io =>
(1 sock : Socket Open) ->
L io {use=1} (Res (Either SocketError String)
L1 io (Res (Either SocketError String)
(\res => Next Receive (isRight res)))
recvAll (MkSocket sock)
= do Right msg <- Socket.recvAll sock