(*
    A session types library
*)

module type SESSION_TYPE = sig
  type 1
  type +'a ; +'s rec 's
  type ! -`a
  type ? +`a
  type +'a |+| +'b
  type +'a |&| +'b

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

  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 's. (!`a; 's) channel -> `a -o 's channel
  val recv      : all `a 's. (?`a; 's) channel -> `a * 's channel
  val sel1      : all 's 'r. ('s |+| 'r) channel -> 's channel
  val sel2      : all 's 'r. ('s |+| 'r) channel -> 'r channel
  val follow    : all 's 'r. ('s |&| 'r) channel -> 's channel + 'r channel
end

module SessionType : SESSION_TYPE = struct
  module C = Channel

  type 1
  type +'a ; +'s
  type ! -`a
  type ? +`a
  type +'a |+| +'b
  type +'a |&| +'b

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

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

  let newRendezvous () = C.new ()

  let request (r: 's rendezvous) = C.recv r

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

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

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

  let sel1 (c: ('s1 |+| 's2) channel)
                     : 's1 channel =
    C.send c true;
    c

  let sel2 (c: rep) =
    C.send c false;
    c

  let follow (c: rep) =
    if C.recv c
      then Left  c
      else Right c
end