Merge pull request #365 from edwinb/lineario

Add linear network library

Makefile

@@ -73,7 +73,7 @@ network: prelude
 contrib: prelude
 	${MAKE} -C libs/contrib IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
 
-libs : prelude base network contrib
+libs : prelude base contrib network
 
 testbin:
 	@${MAKE} -C tests testbin
@@ -90,8 +90,8 @@ support-clean:
 clean-libs:
 	${MAKE} -C libs/prelude clean
 	${MAKE} -C libs/base clean
-	${MAKE} -C libs/network clean
 	${MAKE} -C libs/contrib clean
+	${MAKE} -C libs/network clean
 
 clean: clean-libs support-clean
 	-${IDRIS2_BOOT} --clean ${IDRIS2_IPKG}
@@ -127,8 +127,8 @@ install-support: support
 install-libs: libs
 	${MAKE} -C libs/prelude install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
 	${MAKE} -C libs/base install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
-	${MAKE} -C libs/network install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
 	${MAKE} -C libs/contrib install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
+	${MAKE} -C libs/network install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH}
 
 
 .PHONY: bootstrap bootstrap-build bootstrap-racket bootstrap-racket-build bootstrap-test bootstrap-clean

libs/contrib/Control/Linear/LIO.idr

@@ -76,6 +76,7 @@ runK (Bind {u_act = Unrestricted} act next) k = runK act (\x => runK (next x) k)
 
 ||| Run a linear program exactly once, with unrestricted return value in the
 ||| underlying context
+export
 run : (Applicative io, LinearBind io) =>
       (1 _ : L io a) -> io a
 run prog = runK prog pure

libs/network/Control/Linear/Network.idr

@@ -0,0 +1,126 @@
+module Control.Linear.Network
+
+-- An experimental linear type based API to sockets
+
+import Control.Linear.LIO
+
+import public Network.Socket.Data
+import Network.Socket
+
+public export
+data SocketState = Ready | Bound | Listening | Open | Closed
+
+export
+data Socket : SocketState -> Type where
+     MkSocket : Socket.Data.Socket -> Socket st
+
+export
+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)
+
+export
+close : LinearIO io => (1 _ : Socket st) -> L io {use=1} (Socket Closed)
+close (MkSocket sock)
+    = do Socket.close sock
+         pure1 (MkSocket sock)
+
+export
+done : LinearIO io => (1 _ : Socket Closed) -> L io ()
+done (MkSocket sock) = pure ()
+
+export
+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 # MkSocket sock)
+            else pure1 (False # MkSocket sock)
+
+export
+connect : LinearIO io =>
+          (sock : Socket) ->
+          (addr : SocketAddress) ->
+          (port : Port) ->
+          L io {use=1} (Res Bool (\res => Socket (case res of
+                                                       False => Closed
+                                                       True => Open)))
+connect sock addr port
+    = do ok <- Socket.connect sock addr port
+         if ok == 0
+            then pure1 (True # MkSocket sock)
+            else pure1 (False # MkSocket sock)
+
+export
+listen : LinearIO io =>
+         (1 _ : Socket Bound) ->
+         L io {use=1} (Res Bool (\res => Socket (case res of
+                                                      False => Closed
+                                                      True => Listening)))
+listen (MkSocket sock)
+    = do ok <- Socket.listen sock
+         if ok == 0
+            then pure1 (True # MkSocket sock)
+            else pure1 (False # MkSocket sock)
+
+export
+accept : LinearIO io =>
+         (1 _ : Socket Listening) ->
+         L io {use=1} (Res Bool (\case
+                                    False => Socket Listening
+                                    True => (Socket Listening, Socket Open)))
+accept (MkSocket sock)
+    = do Right (sock', sockaddr) <- Socket.accept sock
+             | Left err => pure1 (False # MkSocket sock)
+         pure1 (True # (MkSocket sock, MkSocket sock'))
+
+export
+send : LinearIO io =>
+       (1 _ : Socket Open) ->
+       (msg : String) ->
+       L io {use=1} (Res Bool (\res => Socket (case res of
+                                                    False => Closed
+                                                    True => Open)))
+send (MkSocket sock) msg
+    = do Right c <- Socket.send sock msg
+             | Left err => pure1 (False # MkSocket sock)
+         pure1 (True # MkSocket sock)
+               
+export
+recv : LinearIO io =>
+       (1 _ : Socket Open) ->
+       (len : ByteLength) ->
+       L io {use=1} (Res (Maybe (String, ResultCode))
+                         (\res => Socket (case res of
+                                               Nothing => Closed
+                                               Just msg => Open)))
+recv (MkSocket sock) len
+    = do Right msg <- Socket.recv sock len
+             | Left err => pure1 (Nothing # MkSocket sock)
+         pure1 (Just msg # MkSocket sock)
+
+export
+recvAll : LinearIO io =>
+          (1 _ : Socket Open) ->
+          L io {use=1} (Res (Maybe String)
+                            (\res => Socket (case res of
+                                                  Nothing => Closed
+                                                  Just msg => Open)))
+recvAll (MkSocket sock)
+    = do Right msg <- Socket.recvAll sock
+             | Left err => pure1 (Nothing # MkSocket sock)
+         pure1 (Just msg # MkSocket sock)

libs/network/network.ipkg

@@ -1,6 +1,10 @@
 package network
 
-modules = Network.Socket,
+opts = "-p contrib"
+
+modules = Control.Linear.Network,
+
+          Network.Socket,
           Network.Socket.Data,
           Network.Socket.Raw,
           Network.FFI