git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/samples/ST/Net/RandServer.idr
156 lines 6.0 kB history raw
1import Network.Socket
2import Control.ST
3import Control.ST.ImplicitCall
4import System
6import Network
7import Threads
9{- A random number server.
11This receives requests from a client, as a number, and sends a reply
12which is a random number within the requested bound.
14There are two states: one for the server, and one for a connected session.
15The server repeatedly listens for requests and creats a session for each
16incoming request.
17-}
19-- States of a connected session
20data SessionState = Waiting -- waiting for the client to send
21 | Processing -- calculating a response to send back
22 | Done -- received message and replied to it
24interface RandomSession (m : Type -> Type) where
25 -- A connected session
26 Connection : SessionState -> Type
27 -- A server listening for connections
28 Server : Type
30 -- Receive a request on a Waiting connection. If there is a request
31 -- available, move to the Processing state
32 recvReq : (conn : Var) ->
33 ST m (Maybe Integer)
34 [conn ::: Connection Waiting :->
35 \res => Connection (case res of
36 Nothing => Done
37 Just _ => Processing)]
38 -- Send a reply, and move the connection to the Done state
39 sendResp : (conn : Var) -> Integer ->
40 ST m () [conn ::: Connection Processing :-> Connection Done]
42 -- Create a server
43 start : ST m (Maybe Var) [addIfJust Server]
44 -- Close a server
45 quit : (srv : Var) -> ST m () [Remove srv Server]
46 -- Finish a connection
47 done : (conn : Var) -> ST m () [Remove conn (Connection Done)]
49 -- Listen for an incoming connection. If there is one, create a session
50 -- with a connection in the Waiting state
51 accept : (srv : Var) ->
52 ST m (Maybe Var)
53 [srv ::: Server, addIfJust (Connection Waiting)]
55interface Sleep (m : Type -> Type) where
56 usleep : (i : Int) -> { auto prf : So (i >= 0 && i <= 1000000) } ->
57 STrans m () xs (const xs)
59Sleep IO where
60 usleep x = lift (System.usleep x)
63using (Sleep io, ConsoleIO io, RandomSession io, Conc io)
64 rndSession : (conn : Var) ->
65 ST io () [Remove conn (Connection {m=io} Waiting)]
66 rndSession conn =
67 do Just bound <- call (recvReq conn)
68 | Nothing => do putStr "Nothing received\n"
69 call (done conn)
70 putStr "Calculating reply...\n"
71 usleep 1000000
72 sendResp conn bound -- (seed `mod` (bound + 1))
73 call (done conn)
75 rndLoop : (srv : Var) -> ST io () [srv ::: Server {m=io}]
76 rndLoop srv
77 = do Just conn <- accept srv
78 | Nothing => putStr "accept failed\n"
79 putStr "Connection received\n"
80 fork (rndSession conn)
81 rndLoop srv
83 rndServer : ST io () []
84 rndServer
85 = do Just srv <- start
86 | Nothing => putStr "Can't start server\n"
87 call (rndLoop srv)
88 quit srv
90implementation (ConsoleIO io, Sockets io) => RandomSession io where
92 -- Connections and servers are composite states, so to implement things
93 -- in terms of them we need to 'split' at the state and 'combine' at the
94 -- end, in every method
95 Connection Waiting = Composite [State Integer, Sock {m=io} Open]
96 Connection Processing = Composite [State Integer, Sock {m=io} Open]
97 Connection Done = Composite [State Integer, Sock {m=io} Closed]
99 Server = Composite [State Integer, Sock {m=io} Listening]
101 recvReq rec = do [seed, conn] <- split rec
102 Right msg <- recv conn
103 | Left err => do combine rec [seed, conn]
104 pure Nothing
105 putStr ("Incoming " ++ show msg ++ "\n")
106 combine rec [seed, conn]
107 pure (Just (cast msg))
109 sendResp rec val = do [seed, conn] <- split rec
110 Right () <- send conn (cast (!(read seed) `mod` val) ++ "\n")
111 | Left err => do combine rec [seed, conn]
112 pure ()
113 close conn
114 combine rec [seed, conn]
116 start = do srv <- new ()
117 Right sock <- socket Stream
118 | Left err => do delete srv; pure Nothing
119 Right () <- bind sock Nothing 9442
120 | Left err => do call (remove sock)
121 delete srv
122 pure Nothing
123 Right () <- listen sock
124 | Left err => do call (remove sock)
125 delete srv
126 pure Nothing
127 putStr "Started server\n"
128 seed <- new 12345
129 combine srv [seed, sock]
130 pure (Just srv)
132 quit srv = do [seed, sock] <- split srv -- need to delete everything
133 close sock; remove sock; delete seed; delete srv
134 done conn = do [seed, sock] <- split conn -- need to delete connection data
135 remove sock; delete seed; delete conn
137 accept srv = do [seed, sock] <- split srv
138 seedVal <- read seed
139 write seed ((1664525 * seedVal + 1013904223)
140 `prim__sremBigInt` (pow 2 32))
141 Right conn <- accept sock
142 | Left err => do combine srv [seed, sock]
143 pure Nothing -- no incoming message
144 -- We're sending the seed to the child process and keeping
145 -- a copy ourselves, so we need to explicitly make a new
146 -- one
147 rec <- new ()
148 seed' <- new seedVal
149 combine rec [seed', conn]
150 combine srv [seed, sock]
151 toEnd rec
152 pure (Just rec)
154main : IO ()
155main = run rndServer