(*
    A session types library
*)

module type SESSION_TYPE = sig
  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 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['s] () =
    (C.new['s channel] ())

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

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

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

  let recv[`a, 's] (c: rep) =
    (Unsafe.unsafeCoerce[`a] (C.recv c),  c)

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

  let sel2['s1, 's2] (c: rep) =
    C.send c false;
    c

  let follow['s1, 's2] (c: rep) =
    if C.recv c
      then Left [rep, rep] c
      else Right[rep, rep] c
end