Trait dialectic::types::Then

pub trait Then<P, N: Unary = Z>: IsSession {
    type Combined: 'static;
}

Substitute P for every Done in Self, thus concatenating the session P to Self.

This does not require P to be a closed session type; it is reasonable to use open session types (those with Continues that refer outside of themselves) as P. Then is careful to adjust the indices of such open types so that they refer correctly outside of Self even when Self contains Loops.

Associated Types

type Combined: 'static

The combined type resulting from substituting P for Done in Self.

Loading content...

Implementors

impl<N: Unary, P, Choices> Then<P, N> for Choose<Choices> where
    Choices: Tuple + 'static,
    Choices::AsList: EachThen<P, N>,
    <Choices::AsList as EachThen<P, N>>::Combined: List, 

type Combined = Choose<<<Choices::AsList as EachThen<P, N>>::Combined as List>::AsTuple>

impl<N: Unary, P, Choices> Then<P, N> for Offer<Choices> where
    Choices: Tuple + 'static,
    Choices::AsList: EachThen<P, N>,
    <Choices::AsList as EachThen<P, N>>::Combined: List, 

type Combined = Offer<<<Choices::AsList as EachThen<P, N>>::Combined as List>::AsTuple>

impl<N: Unary, P: 'static, Q: 'static, R: Then<S, N>, S> Then<S, N> for Split<P, Q, R>

type Combined = Split<P, Q, R::Combined>

impl<N: Unary, P: 'static, Q: Then<R, N>, R> Then<R, N> for Call<P, Q>

type Combined = Call<P, Q::Combined>

impl<N: Unary, T: 'static, P: Then<Q, N>, Q> Then<Q, N> for Recv<T, P>

type Combined = Recv<T, P::Combined>

impl<N: Unary, T: 'static, P: Then<Q, N>, Q> Then<Q, N> for Send<T, P>

type Combined = Send<T, P::Combined>

impl<P, N: Unary> Then<P, N> for Done where
    P: Lift<N>, 

type Combined = P::Lifted

impl<P, N: Unary, const I: usize> Then<P, N> for Continue<I>

type Combined = Continue<I>

impl<P, Q, N: Unary> Then<Q, N> for Loop<P> where
    P: Then<Q, S<N>>, 

type Combined = Loop<<P as Then<Q, S<N>>>::Combined>

Loading content...