Multi-Form Knock Knock Protocol

Knock.idr

||| The Knock Knock Protocol.
module Knock

import Effects
import Effect.Default
import Effect.StdIO
import Effect.Msg

import System.Protocol

||| A dependent pair to describe literal messages.
||| @val The literal value.
Lit : (val : String) -> Type
Lit msg = (m ** m = msg)

||| A containter type to represent the final message in Knock Knock Protocols.
|||
||| @setup Maybe the joke requires a setup.
data KnockRes : (setup : Maybe String) -> Type where
  ||| Create a response for protocols that require a value received earlier in the communication.
  ||| @val The value seen earlier in the communication.
  ||| @msg The message to be appended to `val`.
  Resp : (val : String) -> (msg : String) -> KnockRes (Just val)
  ||| Create a response that does not depend on an earlier value.
  RespNew : String -> KnockRes Nothing

instance Show (KnockRes x) where
  show (Resp val msg) = unwords [val, msg] -- here we append msg to val.
  show (RespNew val) = val

||| The `Knock Knock` Protocol.
||| 
||| @form `True` if the final message depends on an earlier value, `False` otherwise.
total
knock : Bool -> Protocol ['A, 'B] ()
knock b = do
  'A ==> 'B | Lit "Knock Knock"
  'B ==> 'A | Lit "Who's there?"
  res <- 'A ==> 'B | String
  'B ==> 'A | Lit (res ++ " who?")
  case b of
    True  => 'A ==> 'B | KnockRes (Just res)
    False => 'A ==> 'B | KnockRes Nothing
  Done

-- ---------------------------------------------------------- [ Client Process ]
||| Implementation of the Knocker whose last message depends
||| on an earlier message.
covering
knocker : String -> String -> (knee : PID)
        -> Process (knock True) 'A ['B := knee] [STDIO] ()
knocker setup reveal knee = do
    sendTo 'B ("Knock Knock" ** Refl)

    (res ** _) <- recvFrom 'B
    putStrLn $ "From Mark: " ++ res

    sendTo 'B setup

    (res' ** _) <- recvFrom 'B
    putStrLn $ "From Mark: " ++ res'

    sendTo 'B (Resp setup reveal)

||| Implementation of the Knocker whose final message is not dependent
||| on an earlier message.
covering
knocker' : String -> String -> (knee : PID)
        -> Process (knock False) 'A ['B := knee] [STDIO] ()
knocker' setup reveal knee = do
    sendTo 'B ("Knock Knock" ** Refl)

    (res ** _) <- recvFrom 'B
    putStrLn $ "From Mark: " ++ res

    sendTo 'B setup

    (res' ** _) <- recvFrom 'B
    putStrLn $ "From Mark: " ++ res'

    sendTo 'B (RespNew reveal)

||| Implementation of the Knockee.
covering
knockee : (knocker : PID)
        -> Process (knock True) 'B ['A := knocker] [STDIO] ()
knockee client = do
    (kk ** _ ) <- recvFrom 'A
    putStrLn $ "From Teller: " ++ kk

    sendTo 'A ("Who's there?" ** Refl)

    res <- recvFrom 'A
    putStrLn $ "From Teller: " ++ res

    sendTo 'A ((res ++ " who?") ** Refl)

    putStrLn $ "From Teller: " ++ show !(recvFrom 'A)


-- ------------------------------------------------------ [ Sample Innvocation ]

||| Run a single instance of the `Knock Knock` Protocol.
covering
doKnockKnock : String -> String -> IO ()
doKnockKnock setup reveal = runConc [()] (doKnock setup reveal)
  where
    doKnock : String -> String
            -> Process (knock True) 'A Nil [STDIO] ()
    doKnock s r = do
       k <- spawn (knockee) [()]
       setChan 'B k
       knocker s r k
       dropChan 'B

-- -------------------------------------------------------------------- [ Main ]
namespace Main
  main : IO ()
  main = do
    doKnockKnock knocker "A mos" "Quito"
    
-- --------------------------------------------------------------------- [ EOF ]