(*
    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 : all 's. unit -> 's rendezvous

  val request   : all 's. 's rendezvous -> 's channel
  val accept    : all 's. 's rendezvous -> 's dual channel

  val send      : all `a. `a -> all 's. (!`a; 's) channel -[a]>
                    unit * 's channel
  val recv      : all `a 's. (?`a; 's) channel -> `a * 's channel

  val follow    : all `c. ?-> `c channel -> unit * `c
  val choose    : all 's `c. ('s channel -> `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 rep = any C.channel
  type 's channel    = rep
  type 's rendezvous = rep C.channel

  let newRendezvous () = C.new[rep] ()

  let request (r: unit rendezvous) = C.recv r

  let accept (r: unit rendezvous) =
    let c = C.new () in
      C.send r c;
      c

  let newPair () =
    let c = C.new () in
      (c, c)

  let send[`a] (a: `a) (c: rep) =
    C.send c (Unsafe.unsafeCoerce a);
    ((), c)

  let recv[`a] (c: rep) = (C.recv c, c)

  let follow (c: rep) =
    let (c', _) = recv c in ((), c')

  let choose[`c] (ctor: rep -> `c) (c: rep) =
    let (theirs, mine) = newPair () in
      send (ctor theirs) c;
      ((), mine)
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: state1 channel) : int * 1 channel =
              send 1 c;
              follow c;
              s2 c
        and s2 !(c: state2) : int * 1 channel =
          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 : state1 dual channel) : unit * 1 channel =
      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