(*
    Another session types library.  Doesn't use equirecursive types.
*)

module type SESSION_TYPE = sig
  type 1
  type +'a ; +'s
  type ! -`a
  type ? +`a

  type 1          dual = 1
     | (!`a ; 's) dual = ?`a ; 's dual
     | (?`a ; 's) dual = !`a ; 's dual

  type ?-> `c = ?`c; 1
  type !-> `c = !`c; 1

  type 's rendezvous
  type +'s channel qualifier A

  val newRendezvous : unit → 's rendezvous

  val request   : 's rendezvous → 's channel
  val accept    : 's rendezvous → 's dual channel

  val send      : `a → (!`a; 's) channel → unit * 's channel
  val recv      : (?`a; 's) channel → `a * 's channel

  val follow    : ?-> `c channel → unit * `c
  val choose    : ('s channel -A> `c) → !-> `c channel →
                    unit * 's dual channel
end

module SessionType : SESSION_TYPE = struct
  module C = Channel

  type 1
  type +'a ; +'s
  type ! -`a
  type ? +`a

  type 1          dual = 1
     | (!`a ; 's) dual = ?`a ; 's dual
     | (?`a ; 's) dual = !`a ; 's dual

  type ?-> `c = ?`c; 1
  type !-> `c = !`c; 1

  type 's channel    = bool C.channel
  type 's rendezvous = 's channel C.channel

  let newRendezvous = C.new

  let request = C.recv

  let accept rv =
    let c = C.new () in
      C.send rv c;
      c

  let send a c      = (C.send (Unsafe.unsafeCoerce c) a, c)
  let recv c        = (C.recv (Unsafe.unsafeCoerce c), c)

  let follow c      = ((), fst (recv c))
  let choose ctor c = send (ctor c) c
end

module SessionType2Test = struct
  open SessionType

  type state1 = !int; ?->state2
   and state2 = Done of (?int; 1) channel
              | More of (!int; ?->state2) channel
              | Again of (?int; state1) channel


  let client (c: state1 channel) =
    let rec s1 !c =
              send 1 c;
              follow c;
              s2 c
        and s2 !c =
          match c with
          | Done c  -> recv c
          | More c  -> send 2 c;
                       follow c;
                       s2 c
          | Again c -> let z = recv c in
                       s1 c
     in fst (s1 c)

  let server (c: state1 dual channel) =
    let rec s1 !c =
      match recv c with
        | 0 -> choose More c;
               let z' = recv c in
               choose Done c;
               send z' c
        | 1 -> choose Again c;
               send 1 c;
               s1 c
        | z -> choose Done c;
               send z c
     in fst (s1 c)
end