Trait dialectic::types::Subst

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

Substitute P for every Continue referring to the outermost scope in the given session type.

When entering a Loop, all Continues which refer to that Loop are unrolled by one loop iteration so that the session type remains valid. This trait implements that type-level operation.

Examples

use dialectic::types::*;
use dialectic::prelude::*;

assert_type_eq_all!(
    <Send<i64, Continue<0>> as Subst<Recv<(), Done>>>::Substituted,
    Send<i64, Recv<(), Done>>,
);

Associated Types

type Substituted: 'static

The result of the substitution.

Loading content...

Implementors

impl<N: Unary, P, Choices> Subst<P, N> for Choose<Choices> where
    Choices: Tuple + 'static,
    Choices::AsList: EachSubst<P, N>,
    <Choices::AsList as EachSubst<P, N>>::Substituted: List, 

type Substituted = Choose<<<Choices::AsList as EachSubst<P, N>>::Substituted as List>::AsTuple>

impl<N: Unary, P, Choices> Subst<P, N> for Offer<Choices> where
    Choices: Tuple + 'static,
    Choices::AsList: EachSubst<P, N>,
    <Choices::AsList as EachSubst<P, N>>::Substituted: List, 

type Substituted = Offer<<<Choices::AsList as EachSubst<P, N>>::Substituted as List>::AsTuple>

impl<N: Unary, P: Subst<R, N>, Q: Subst<R, N>, R> Subst<R, N> for Call<P, Q>

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

impl<N: Unary, P: Subst<S, N>, Q: Subst<S, N>, R: Subst<S, N>, S> Subst<S, N> for Split<P, Q, R>

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

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

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

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

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

impl<P, N: Unary> Subst<P, N> for Done

type Substituted = Done

impl<P, N: Unary, M: Unary, const I: usize> Subst<P, N> for Continue<I> where
    Number<I>: ToUnary<AsUnary = M>,
    (N, M): Compare<Continue<I>, P, Continue<I>>,
    <(N, M) as Compare<Continue<I>, P, Continue<I>>>::Result: 'static, 

type Substituted = <(N, M) as Compare<Continue<I>, P, Continue<I>>>::Result

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

type Substituted = Loop<<P as Subst<Q, S<N>>>::Substituted>

Loading content...