---------------------------------------------
-- Session definitions for the POP3 protocol

-- Transaction
type T = μY. &{ stat => #{ ok => !(Int @ Int).Y },
                retr => #{ ok => ?Int.#{ ok => !String.!String.Y,
                                         error => !String.Y }},
                quit => #{ ok => !String.end }}
         
-- Authorization
type A = μX. &{ quit => #{ ok => !String.end },
                user => ?String.
                #{ error => !String.X,
                   ok => !String.
                   &{ quit => #{ ok => !String.end },
                      pass => ?String.
                      #{ error => !String.X,
                         ok => !String.T }}}}

-- Start
type S = #{ ok => !String.A }

------------------------------------------------------------
-- Aliases for case branches that aren't currently inferred
type Q = #{ ok => !String.end }

type TS = #{ ok => !(Int @ Int).T }
type TR = #{ ok => ?Int.#{ ok => !String.!String.T,
                           error => !String.T }}

type AP = ?String.
          #{ error => !String.A,
             ok => !String.T }
type AU = ?String.
          #{ error => !String.A,
             ok => !String.&{ quit => Q, pass => AP }}

---------------------------------
-- Example server implementation

accesspoint :: <S, -S>
accesspoint = concurrent S

goodbye :: String
goodbye = "POP3 server signing off"

transaction :: T -> end -> end
transaction chan fixed =
  case chan of {
    stat => (\chan: TS.
      let chan = select ok chan in
      let chan = send (2, 3) chan in
      fixed),
    retr => (\chan: TR.
      let chan = select ok chan in
      let index, chan = receive chan in
      let chan = chan in
      if index == 1
      then
        let chan = select ok chan in
        let chan = send "11 octets" chan in
        let chan = send "Hello word" chan in
        fixed
      else
        let chan = select error chan in
        let chan = send "No such message" chan in
        fixed),
    quit => (\chan: Q.
      let chan = select ok chan in
      send goodbye chan)
  }

authorization :: A -> end -> end
authorization chan fixed =
  case chan of {
    quit => (\chan: Q.
      let chan = select ok chan in
      send goodbye chan),
    user => (\chan: AU.
      let user, chan = receive chan in
      if user == "paul"
      then
        let chan = select ok chan in
        let chan = send "User accepted" chan in
        case chan of {
          quit => (\chan: Q.
            let chan = select ok chan in
            send goodbye chan),
          pass => (\chan: AP.
            let pass, chan = receive chan in
            if pass == "p4U|_"
            then
              let chan = select ok chan in
              let chan = send "Pass accepted" chan in
              fix (transaction chan)
            else
              let chan = select error chan in
              let chan = send "Pass denied" chan in
              fixed)
          }
      else
        let chan = select error chan in
        let chan = send "User denied" chan in
        fixed)
  }

start :: S -> end
start chan =
  let chan = select ok chan in
  let chan = send "POP3 server ready <mypopserver>" chan in
  fix (authorization chan)

main :: end
main = let chan = accept 0 accesspoint in start chan