(*
    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 → `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 = int C.channel
  type 's channel    = rep
  type 's rendezvous = rep C.channel

  let newRendezvous () = C.new ()

  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) (c: rep) =
    C.send c (Unsafe.unsafeCoerce a);
    ((), c)

  let recv (c: rep) = (Unsafe.unsafeCoerce (C.recv c), c)

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

  let choose (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 =
              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