type epsilon         = unit
type ('r, 'a) send   = unit
type ('r, 'a) recv   = unit
type ('r, 's) choose = unit
type ('r, 's) offer  = unit

type ('r, 's) dual   = unit

module ModuleLevelProofs = struct
  module type TYPE = sig
    type t
  end

  module type DUAL = sig
    type client
    type server

    val witness : (client, server) dual
  end

  module Epsilon = struct
    type client = epsilon
    type server = epsilon

    let witness = ()
  end

  module Send (T : TYPE) (R : DUAL) = struct
    type client = (R.client, T.t) send
    type server = (R.server, T.t) recv

    let witness = ()
  end

  module Recv (T : TYPE) (R : DUAL) = struct
    type client = (R.client, T.t) recv
    type server = (R.server, T.t) send

    let witness = ()
  end

  module Choose (R : DUAL) (S : DUAL) = struct
    type client = (R.client, S.client) choose
    type server = (R.server, S.server) offer

    let witness = ()
  end

  module Offer (R : DUAL) (S : DUAL) = struct
    type client = (R.client, S.client) offer
    type server = (R.server, S.server) choose

    let witness = ()
  end

  module Flip (R : DUAL) = struct
    type client = R.server
    type server = R.client

    let witness = ()
  end
end

module ValueLevelProofs = struct
  let epsilon = ()
  let send _ = ()
  let recv _ = ()
  let send' _ _ = ()
  let recv' _ _ = ()
  let offer _ _ = ()
  let choose _ _ = ()

  let flip _ = ()
end

module ImplicitProofs = struct
  type ('s, 't, 'a) session = unit -> 'a

  let ret a () = a
  let (>>=) m k () = k (m ()) ()
  let (>>) m n = m >>= fun _ -> n

  let send _ () = ()
  let recv () = failwith "recv"
  let mock_recv a () = a
  let sel1 () = ()
  let sel2 () = ()
  let offer a _ () = a ()
  let close () = ()

  let run a b = b ()
end