rust-type-level-smallfuck-running-trait.rs

pub trait Running<B: StateTy>: ProgramTy {
    type Output: StateTy;
}

pub type Run<A: ProgramTy, B: StateTy> = <A as Running<B>>::Output;


// [(Left P), (St Nil C R)] => (# P (St Nil F (Cons C R)))
impl<P: ProgramTy, C: Bit, R: List> Running<St<Nil, C, R>> for Left<P>
    where P: Running<St<Nil, F, Cons<C, R>>>
{
    type Output = <P as Running<St<Nil, F, Cons<C, R>>>>::Output;
}

// [(Right P), (St L C Nil)] => (# P (St (Cons C L) F Nil))
impl<P: ProgramTy, L: List, C: Bit> Running<St<L, C, Nil>> for Right<P>
    where P: Running<St<Cons<C, L>, F, Nil>>
{
    type Output = <P as Running<St<Cons<C, L>, F, Nil>>>::Output;
}

// [(Left P), (St (Cons N L) C R)] => (# P (St L N (Cons C R)))
impl<P: ProgramTy, L: List, C: Bit, N: Bit, R: List> Running<St<Cons<N, L>, C, R>> for Left<P>
    where P: Running<St<L, N, Cons<C, R>>>
{
    type Output = <P as Running<St<L, N, Cons<C, R>>>>::Output;
}

// [(Right P), (St L C (Cons N R))] => (# P (St (Cons C L) N R))
impl<P: ProgramTy, L: List, C: Bit, N: Bit, R: List> Running<St<L, C, Cons<N, R>>> for Right<P>
    where P: Running<St<Cons<C, L>, N, R>>
{
    type Output = <P as Running<St<Cons<C, L>, N, R>>>::Output;
}

// [(Flip P), (St L F R)] => (# P (St L T R))
impl<P: ProgramTy, L: List, R: List> Running<St<L, F, R>> for Flip<P>
    where P: Running<St<L, T, R>>
{
    type Output = <P as Running<St<L, T, R>>>::Output;
}

// [(Flip P), (St L T R)] => (# P (St L F R))
impl<P: ProgramTy, L: List, R: List> Running<St<L, T, R>> for Flip<P>
    where P: Running<St<L, F, R>>
{
    type Output = <P as Running<St<L, F, R>>>::Output;
}

// [(Loop P Q), (St L F R)] => (# Q (St L F R))
impl<P: ProgramTy, Q: ProgramTy, L: List, R: List> Running<St<L, F, R>> for Loop<P, Q>
    where Q: Running<St<L, F, R>>
{
    type Output = <Q as Running<St<L, F, R>>>::Output;
}

// [(Loop P Q), (St L T R)] => (# (Loop P Q) (# P (St L T R)))
impl<P: ProgramTy, Q: ProgramTy, L: List, R: List> Running<St<L, T, R>> for Loop<P, Q>
    where Loop<P, Q>: Running<<P as Running<St<L, T, R>>>::Output>,
          P: Running<St<L, T, R>>
{
    type Output = <Loop<P, Q> as Running<<P as Running<St<L, T, R>>>::Output>>::Output;
}

// [Empty, S] => S
impl<S: StateTy> Running<S> for Empty {
    type Output = S;
}