concurrent counting

stream.idr

module Main

import Effects
import Effect.StdIO

import System.Protocol

data Command = Next | SetIncrement | Stop 

count : Protocol ['Client, 'Server] ()
count = do cmd <- 'Client ==> 'Server | Command 
           case cmd of
              Next => do 'Server ==> 'Client | Int 
                         Rec count 
              SetIncrement => do 'Client ==> 'Server | Int
                                 Rec count
              Stop => Done

covering
countServer : (c : Int) -> (v : Int) -> (inc : Int) -> (client : PID) ->
              Process count 'Server ['Client := client] [] (MsgResult ())
countServer c v inc client 
        = do OK cmd <- recvFrom 'Client
                          | abandon InvalidData
             case cmd of
                    Next => do OK () <- sendTo 'Client v
                                           | abandon InvalidData
                               continue
                               countServer 0 (v + inc) inc client
                    SetIncrement => do OK i <- recvFrom 'Client
                                                  | abandon InvalidData
                                       rec (countServer 0 v i client)
                    Stop => return (OK ())

covering
countClient : (server : PID) ->
              Process count 'Client ['Server := server] [STDIO] (MsgResult ())
countClient server = do 
                 putStr "More? ('n' to stop) "
                 x <- getStr
                 case (trim x /= "n") of
                    True => let xval : Int = cast (trim x) in
                                case xval /= 0 of
                                     True => do
                                       OK () <- sendTo 'Server SetIncrement
                                                   | abandon InvalidData
                                       OK () <- sendTo 'Server xval
                                                   | abandon InvalidData
                                       rec (countClient server)
                                     False => do
                                       OK () <- sendTo 'Server Next
                                                   | abandon InvalidData
                                       OK ans <- recvFrom 'Server 
                                                   | abandon InvalidData
                                       putStrLn (show ans)
                                       rec (countClient server)
                    False => do OK () <- sendTo 'Server Stop
                                                   | abandon InvalidData
                                return (OK ())


doCount : Process count 'Client [] [STDIO] ()
doCount = do server <- spawn (countServer 0 0 1) []
             setChan 'Server server 
             countClient server
             dropChan 'Server

main : IO ()
main = runConc [()] doCount