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()) }) ) });