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

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

  val send      : `a → (!`a; 's) channel → 's channel
  val recv      : (?`a; 's) channel → `a * 's channel
  val sel1      : ('s |+| 'r) channel → 's channel
  val sel2      : ('s |+| 'r) channel → 'r channel
  val follow    : ('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 '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 sel1 c = C.send c true; c

  let sel2 c = C.send c false; c

  let follow c =
    if C.recv c
      then Left  c
      else Right c
end