Binary External Choice

Provider Rule: Offer Choice

macro offer_choice! <C, A, B> {
  Left => $expr: PartialSession<C, A>,
  Right => $expr: PartialSession<C, B>,
} ->
  PartialSession<C, ExternalChoice<Either<A, B>>>

Example

    use ferrite_session::{
      either::*,
      prelude::*,
    };

    let p: Session<
      ExternalChoice<Either<ReceiveValue<String, End>, SendValue<u64, End>>>,
    > = offer_choice! {
      Left =>
        receive_value(move |name| {
          println!("Hello, {}!", name);
          terminate()
        })
      Right =>
        send_value(42, terminate())
    };

Client Rule: Choose Left

macro choose! <N, C1, C2, A1, A2, B> (
  n: N, Left,
  cont: PartialSession<C2, B>
) ->  PartialSession<C1, B>

• C1 is in the form HList[…, N: ExternalChoice<Either<A1, A2>>, …]
• C2 is in the form HList[…, N: A1, …], with the remaining elements being the same as in C1.

Example

    let p: Session<
      ReceiveChannel<
        ExternalChoice<Either<ReceiveValue<String, End>, SendValue<u64, End>>>,
        End,
      >,
    > = receive_channel(move |c| {
      choose!(
        c,
        Left,
        send_value_to(c, "Hello World!".to_string(), wait(c, terminate()))
      )
    });

Client Rule: Choose Right

macro choose! <N, C1, C2, A1, A2, B> (
  $n: N, Right,
  $cont: PartialSession<C2, B>
) ->  PartialSession<C1, B>

• C1 is in the form HList[…, N: ExternalChoice<Either<A1, A2>>, …]
• C2 is in the form HList[…, N: A2, …], with the remaining elements being the same as in C1.

Example

    let p: Session<
      ReceiveChannel<
        ExternalChoice<Either<ReceiveValue<String, End>, SendValue<u64, End>>>,
        End,
      >,
    > = receive_channel(move |c| {
      choose!(
        c,
        Right,
        receive_value_from(c, move |x| {
          println!("{}", x);
          wait(c, terminate())
        })
      )
    });