pluggingTestBot.idr

(.|) : TestBot -> IOSpec r -> IOSpec r
(.|) (MkTestBot actions) prog = pull actions prog where
  mutual -- To define mutually recursive functions
 
    pull : List TestBotAction -> IOSpec r -> IOSpec r
    pull actions (Pure r) = Pure r
    pull actions (WriteLine s next) = do
      prnLine s          -- Print the line to display (such as "Password:")
      pull actions next  -- Keep on traversing the IOSpec computation
    pull actions (ReadLine cont) =
      push actions cont -- Give control to bot actions
 
    push : List TestBotAction -> (String -> IOSpec r )-> IOSpec r
    push [] cont = ReadLine cont
    push (Typing x::xs) cont = do
      prnLine x         -- Display the value typed by the bot
      pull xs (cont x)  -- Send `x` to the main program, and give it control back
    push (Thinking x::xs) cont = do
      prnLine x         -- Print the thoughts of our bot
      readLine          -- Wait for a line (notification to continue)
      push xs cont      -- Keep going