Suggestion is to add a macro for writing the session types down.
Something like:
proto!{Atm, Client,
?<Id>,
+[
act: &[
?<u64>, !<u64>, act;
?<u64>, +[act; act];
!<u64>;
eps
];
eps
]
}where
?<T>, P denotes Recv<T, P>!<T>, P denotes Send<T, P>+[A; B; C] is Choose<A, Choose<B, C>>&[A; B; C] is Offer<A, Offer<B, C>>t: P should be Rec<P>. Any occurrences of t in P should be replaced with an appropriate Var<N> constructeps is just Eps
The output of proto!() is then two type aliases:
type Atm = ...;
type Client = <Atm as HasDual>::Dual;
This should replace the current constructs like this:
type Atm = Recv<Id, Choose<Rec<AtmInner>, Eps>>;
type AtmInner = Offer<AtmDeposit, Offer<AtmWithdraw, Offer<AtmBalance, Eps>>>;
type AtmDeposit = Recv<u64, Send<u64, Var<Z>>>;
type AtmWithdraw = Recv<u64, Choose<Var<Z>, Var<Z>>>;
type AtmBalance = Send<u64, Var<Z>>;
type Client = <Atm as HasDual>::Dual;
Suggestion is to add a macro for writing the session types down.
Something like:
where
?<T>, PdenotesRecv<T, P>!<T>, PdenotesSend<T, P>+[A; B; C]isChoose<A, Choose<B, C>>&[A; B; C]isOffer<A, Offer<B, C>>t: Pshould beRec<P>. Any occurrences oftinPshould be replaced with an appropriateVar<N>constructepsis justEpsThe output of
proto!()is then two type aliases:This should replace the current constructs like this: