RandServer.idr

import Network.Socket
import Control.ST
import Control.ST.ImplicitCall
import System

import Network
import Threads

{- A random number server.

This receives requests from a client, as a number, and sends a reply
which is a random number within the requested bound.

There are two states: one for the server, and one for a connected session.
The server repeatedly listens for requests and creats a session for each
incoming request.
-}

-- States of a connected session
data SessionState = Waiting -- waiting for the client to send
                  | Processing -- calculating a response to send back
                  | Done -- received message and replied to it

interface RandomSession (m : Type -> Type) where
  -- A connected session
  Connection : SessionState -> Type
  -- A server listening for connections
  Server : Type

  -- Receive a request on a Waiting connection. If there is a request
  -- available, move to the Processing state
  recvReq : (conn : Var) ->
            ST m (Maybe Integer) 
                 [conn ::: Connection Waiting :->
                           \res => Connection (case res of
                                                    Nothing => Done
                                                    Just _ => Processing)]
  -- Send a reply, and move the connection to the Done state
  sendResp : (conn : Var) -> Integer ->
             ST m () [conn ::: Connection Processing :-> Connection Done]

  -- Create a server
  start : ST m (Maybe Var) [addIfJust Server]
  -- Close a server
  quit : (srv : Var) -> ST m () [Remove srv Server]
  -- Finish a connection
  done : (conn : Var) -> ST m () [Remove conn (Connection Done)]

  -- Listen for an incoming connection. If there is one, create a session
  -- with a connection in the Waiting state
  accept : (srv : Var) ->
           ST m (Maybe Var) 
                [srv ::: Server, addIfJust (Connection Waiting)]

interface Sleep (m : Type -> Type) where
  usleep : (i : Int) -> { auto prf : So (i >= 0 && i <= 1000000) } -> 
           STrans m () xs (const xs)

Sleep IO where
  usleep x = lift (System.usleep x)


using (Sleep io, ConsoleIO io, RandomSession io, Conc io)
  rndSession : (conn : Var) -> 
               ST io () [Remove conn (Connection {m=io} Waiting)]
  rndSession conn =
         do Just bound <- call (recvReq conn)
              | Nothing => do putStr "Nothing received\n"
                              call (done conn)
            putStr "Calculating reply...\n"
            usleep 1000000
            sendResp conn bound -- (seed `mod` (bound + 1))
            call (done conn)

  rndLoop : (srv : Var) -> ST io () [srv ::: Server {m=io}]
  rndLoop srv 
    = do Just conn <- accept srv
              | Nothing => putStr "accept failed\n"
         putStr "Connection received\n"
         fork (rndSession conn)
         rndLoop srv

  rndServer : ST io () []
  rndServer 
    = do Just srv <- start
              | Nothing => putStr "Can't start server\n"
         call (rndLoop srv)
         quit srv

implementation (ConsoleIO io, Sockets io) => RandomSession io where
  
  -- Connections and servers are composite states, so to implement things
  -- in terms of them we need to 'split' at the state and 'combine' at the
  -- end, in every method
  Connection Waiting = Composite [State Integer, Sock {m=io} Open]
  Connection Processing = Composite [State Integer, Sock {m=io} Open]
  Connection Done = Composite [State Integer, Sock {m=io} Closed]

  Server = Composite [State Integer, Sock {m=io} Listening]

  recvReq rec = do [seed, conn] <- split rec
                   Right msg <- recv conn
                         | Left err => do combine rec [seed, conn]
                                          pure Nothing
                   putStr ("Incoming " ++ show msg ++ "\n")
                   combine rec [seed, conn]
                   pure (Just (cast msg))

  sendResp rec val = do [seed, conn] <- split rec
                        Right () <- send conn (cast (!(read seed) `mod` val) ++ "\n")
                              | Left err => do combine rec [seed, conn]
                                               pure ()
                        close conn
                        combine rec [seed, conn]
  
  start = do srv <- new ()
             Right sock <- socket Stream
                   | Left err => do delete srv; pure Nothing
             Right () <- bind sock Nothing 9442
                   | Left err => do call (remove sock)
                                    delete srv
                                    pure Nothing
             Right () <- listen sock
                   | Left err => do call (remove sock)
                                    delete srv
                                    pure Nothing
             putStr "Started server\n"
             seed <- new 12345
             combine srv [seed, sock]
             pure (Just srv)
  
  quit srv = do [seed, sock] <- split srv -- need to delete everything
                close sock; remove sock; delete seed; delete srv
  done conn = do [seed, sock] <- split conn -- need to delete connection data
                 remove sock; delete seed; delete conn
  
  accept srv = do [seed, sock] <- split srv
                  seedVal <- read seed
                  write seed ((1664525 * seedVal + 1013904223) 
                                `prim__sremBigInt` (pow 2 32))
                  Right conn <- accept sock
                        | Left err => do combine srv [seed, sock]
                                         pure Nothing -- no incoming message
                  -- We're sending the seed to the child process and keeping
                  -- a copy ourselves, so we need to explicitly make a new
                  -- one
                  rec <- new ()
                  seed' <- new seedVal
                  combine rec [seed', conn]
                  combine srv [seed, sock]
                  toEnd rec
                  pure (Just rec)

main : IO ()
main = run rndServer