/*
Compile time Brainfuck implementation in Rust using types (not macros; the two
macros are just for convenience)

In short, it uses trait impls as Prolog-like terms, and rustc's type inference
does unification.  All impls are for the same dummy type; both 'input' and
'output' arguments are generic parameters.
*/

#![feature(macro_rules)]
#![allow(unused_variables)]
#![allow(dead_code)]
use std::default::Default;
use std::fmt::{Show, Formatter};

struct Nothing; // the dummy type

trait Nice : Default + Show {}

trait Church : Nice {
    fn as_int(self) -> int;
}
#[deriving(Default)]
struct Zero;
#[deriving(Default)]
struct Succ<P: Church>;

impl Nice for Zero {}
impl Church for Zero {
    fn as_int(self) -> int { 0 }
}
impl<P: Church> Nice for Succ<P> {}
impl<P: Church> Church for Succ<P> {
    fn as_int(self) -> int {
        let p: P = Default::default();
        p.as_int() + 1
    }
}

// not sure why I can't just impl<N: Church> Show for N; it gives a crate error
impl Show for Zero {
    fn fmt(&self, fmt: &mut Formatter) -> Result<(), std::fmt::Error> {
        write!(fmt, "0")
    }
}
impl<P: Church> Show for Succ<P> {
    fn fmt(&self, fmt: &mut Formatter) -> Result<(), std::fmt::Error> {
        write!(fmt, "{}", self.as_int())
    }
}

// our integers are infinitely ranged, because this is easiest to implement; 0
// decrements to 0

trait PlusOne<A: Church, R: Church> {}
impl<P: Church> PlusOne<P, Succ<P>> for Nothing {}


trait MinusOne<A: Church, R: Church> {}
impl<P: Church> MinusOne<Succ<P>, P> for Nothing {}
impl MinusOne<Zero, Zero> for Nothing {}





trait ConsCell : Nice {}

#[deriving(Default)]
struct Nil;
#[deriving(Default)]
struct Cons<A: Nice, B: ConsCell>;

impl<A: Nice, B: ConsCell> ConsCell for Cons<A, B> {}
impl<A: Nice, B: ConsCell> Nice for Cons<A, B> {}
impl ConsCell for Nil {}
impl Nice for Nil {}


impl Show for Nil {
    fn fmt(&self, fmt: &mut Formatter) -> Result<(), std::fmt::Error> {
        write!(fmt, "Nil")
    }
}
impl<A: Nice, B: ConsCell> Show for Cons<A, B> {
    fn fmt(&self, fmt: &mut Formatter) -> Result<(), std::fmt::Error> {
        let a: A = Default::default();
        let b: B = Default::default();
        write!(fmt, "({}, {})", a, b)
    }
}

// append(a -> b):
//    appends this to the end of the list
trait Append<A: ConsCell, B: Nice, R: ConsCell> {}
impl<B: Nice>
    Append<Nil, B, Cons<B, Nil>> for Nothing {}
impl<Car: Nice, Cdr: ConsCell, B: Nice, R: ConsCell, N>
    Append<Cons<Car, Cdr>, B, Cons<Car, R>> for Nothing
    where N: Append<Cdr, B, R> {}

// rol(a -> b):
//    rotates the list to the left, e.g. cons(1, cons(2, cons(3, nil))) ->
//                                       cons(2, cons(3, cons(1, nil)))
trait Rol<A: ConsCell, R: ConsCell> {}
impl<Car: Nice, Cdr: ConsCell, R: ConsCell, N>
    Rol<Cons<Car, Cdr>, R> for Nothing
    where N: Append<Cdr, Car, R> {}

// removelast(a -> b, l)
//    removes and returns the last element
trait RemoveLast<A: ConsCell, R: ConsCell, L: Nice> {}
impl<L: Nice>
    RemoveLast<Cons<L, Nil>, Nil, L> for Nothing {}
impl<Fst: Nice, Snd: Nice, Rest: ConsCell, L: Nice, R: ConsCell, N>
    RemoveLast<Cons<Fst, Cons<Snd, Rest>>, Cons<Fst, R>, L> for Nothing
    where N: RemoveLast<Cons<Snd, Rest>, R, L> {}


// ror(a -> b):
//    rotates the list to the right
trait Ror<A: ConsCell, R: ConsCell> {}
impl<A: ConsCell, R: ConsCell, L: Nice, N>
    Ror<A, Cons<L, R>> for Nothing
    where N: RemoveLast<A, R, L> {}

trait BFInsn : Nice {}
macro_rules! define_insn(($n:ident) => {
    #[deriving(Default, Show)]
    struct $n;
    impl Nice for $n {}
})
define_insn!(BFPlus)
define_insn!(BFMinus)
define_insn!(BFLeft)
define_insn!(BFRight)
define_insn!(BFOutput)

#[deriving(Default, Show)]
struct BFLoop<InnerInsns: ConsCell>;
impl<II: ConsCell> Nice for BFLoop<II> {}

// bf(state, insns, output -> newstate, newoutput)
trait BF<State: ConsCell, Insns: ConsCell, Output: ConsCell, NewState: ConsCell, NewOutput: ConsCell> {}
// State is a ConsCell of Church numerals, where the BF pointer is always in
// the first position: to move the pointer, we instead rotate the entire
// memory, as this is easier to implement.  Insns is a ConsCell of BFInsns.

// +
impl<Car: Church, Cdr: ConsCell, OtherInsns: ConsCell, Output: ConsCell, NewState: ConsCell, NewOutput: ConsCell, CarPlusOne: Church, N1, N2>
    BF<Cons<Car, Cdr>, Cons<BFPlus, OtherInsns>, Output, NewState, NewOutput>
    for Nothing where
        N1: BF<Cons<CarPlusOne, Cdr>, OtherInsns, Output, NewState, NewOutput>,
        N2: PlusOne<Car, CarPlusOne> {}

// -
impl<Car: Church, Cdr: ConsCell, OtherInsns: ConsCell, Output: ConsCell, NewState: ConsCell, NewOutput: ConsCell, CarMinusOne: Church, N1, N2>
    BF<Cons<Car, Cdr>, Cons<BFMinus, OtherInsns>, Output, NewState, NewOutput>
    for Nothing where
        N1: BF<Cons<CarMinusOne, Cdr>, OtherInsns, Output, NewState, NewOutput>,
        N2: MinusOne<Car, CarMinusOne> {}

// <
impl<State: ConsCell, OtherInsns: ConsCell, Output: ConsCell, NewState: ConsCell, NewOutput: ConsCell, MiddleState: ConsCell, N1, N2>
    BF<State, Cons<BFLeft, OtherInsns>, Output, NewState, NewOutput>
    for Nothing where
        N1: Ror<State, MiddleState>,
        N2: BF<MiddleState, OtherInsns, Output, NewState, NewOutput> {}

// >
impl<State: ConsCell, OtherInsns: ConsCell, Output: ConsCell, NewState: ConsCell, NewOutput: ConsCell, MiddleState: ConsCell, N1, N2>
    BF<State, Cons<BFRight, OtherInsns>, Output, NewState, NewOutput>
    for Nothing where
        N1: Rol<State, MiddleState>,
        N2: BF<MiddleState, OtherInsns, Output, NewState, NewOutput> {}

// .
impl<Car: Church, Cdr: ConsCell, OtherInsns: ConsCell, Output: ConsCell, NewState: ConsCell, NewOutput: ConsCell, N>
    BF<Cons<Car, Cdr>, Cons<BFOutput, OtherInsns>, Output, NewState, Cons<Car, NewOutput>>
    for Nothing where
        N: BF<Cons<Car, Cdr>, OtherInsns, Output, NewState, NewOutput> {}

// [] (current cell is zero)
impl<Cdr: ConsCell, Inner: ConsCell, PastLoop: ConsCell, Output: ConsCell, NewState: ConsCell, NewOutput: ConsCell, N>
    BF<Cons<Zero, Cdr>, Cons<BFLoop<Inner>, PastLoop>, Output, NewState, NewOutput>
    for Nothing where
        N: BF<Cons<Zero, Cdr>, PastLoop, Output, NewState, NewOutput> {}

// [] (current cell is nonzero)
impl<P: Church, Cdr: ConsCell, Inner: ConsCell, PastLoop: ConsCell, Output: ConsCell, NewState: ConsCell, NewOutput: ConsCell, MiddleState: ConsCell, MiddleOutput: ConsCell, N1, N2>
    BF<Cons<Succ<P>, Cdr>, Cons<BFLoop<Inner>, PastLoop>, Output, NewState, NewOutput>
    for Nothing where
        // run one iteration
        N1: BF<Cons<Succ<P>, Cdr>, Inner, Output, MiddleState, MiddleOutput>,
        // repeat
        N2: BF<MiddleState, Cons<BFLoop<Inner>, PastLoop>, MiddleOutput, NewState, NewOutput> {}

// reached the end of input?
impl<State: ConsCell, Output: ConsCell>
    BF<State, Nil, Output, State, Output> for Nothing {}

// helpers to more easily specify the input instructions (can't have a macro
// that evaluates to a type)
fn cons<Car: Nice, Cdr: ConsCell>(car: Car, cdr: Cdr) -> Cons<Car, Cdr> {
    Default::default()
}
fn bf_loop<InnerInsns: ConsCell>(ii: InnerInsns) -> BFLoop<InnerInsns> {
    BFLoop
}
macro_rules! list_literal[
    ($a:expr, $($b:expr),*) => {cons($a, list_literal![$($b),*])};
    ($a:expr) => {cons($a, Nil)};
    () => {Nil};
]
/*

*/

fn main() {
    // +++[->++<]+.>.
    let insns = list_literal![
        BFPlus,
        BFPlus,
        BFPlus,
        bf_loop(list_literal![BFMinus, BFRight, BFPlus, BFPlus, BFLeft]),
        BFPlus,
        // Uncomment this to get 'overflow evaluating' errors
        // bf_loop(list_literal![]),
        BFOutput,
        BFRight,
        BFOutput
    ];
    let state = list_literal![Zero, Zero, Zero, Zero, Zero, Zero, Zero, Zero, Zero];


    fn print_bf<State: ConsCell, Insns: ConsCell, N, NewState: ConsCell, NewOutput: ConsCell>(state: State, insns: Insns)
        where N: BF<State, Insns, Nil, NewState, NewOutput> {
        let ns: NewState = Default::default();
        println!("final state: {}", ns);
        let no: NewOutput = Default::default();
        println!("final output: {}", no);
    }
    print_bf(state, insns);

}