use std::{
    fmt::Debug,
    ops::{Add, AddAssign},
};

use super::*;

pub struct TestResults {
    success: usize,
    total: usize,
    result: Result<(), String>,
}

pub type R = TestResults;

impl R {
    pub fn unwrap(self) {
        match self {
            Self {
                success,
                total,
                result: Err(e),
            } => panic!("failed:\n{success}/{total}\n{e}\n"),
            _ => (),
        };
    }
}

pub trait Eqr<'a>: WeakFunctor<'a> {
    fn eqr<A: PartialEq + Debug + 'a>(name: &'a str, left: Self::F<A>, right: Self::F<A>) -> R;
}

pub fn eqr<T: PartialEq + Debug>(name: &str, left: T, right: T) -> R {
    if left == right {
        TestResults {
            success: 1,
            total: 1,
            result: Ok(()),
        }
    } else {
        TestResults {
            success: 0,
            total: 1,
            result: Err(format!("{name}: {:?} != {:?}", left, right)),
        }
    }
}

impl Default for R {
    fn default() -> Self {
        Self {
            success: 0,
            total: 0,
            result: Ok(()),
        }
    }
}

impl Add for R {
    type Output = R;

    fn add(self, rhs: Self) -> Self::Output {
        Self {
            success: self.success + rhs.success,
            total: self.total + rhs.total,
            result: match (self.result, rhs.result) {
                (Err(el), Err(er)) => Err(el + "\n" + er.as_str()),
                (e, Ok(_)) => e,
                (Ok(_), e) => e,
            },
        }
    }
}

impl AddAssign<R> for R {
    fn add_assign(&mut self, rhs: R) {
        self.success += rhs.success;
        self.total += rhs.total;
        match (&mut self.result, rhs.result) {
            (Err(ref mut el), Err(er)) => {
                *el += "\n";
                *el += er.as_str()
            }
            (_, Ok(_)) => {}
            (rl, Err(er)) => *rl = Err(er),
        }
    }
}

pub fn fmap_respects_identity<'a, T: Functor<'a> + Eqr<'a>, A: 'a + Debug + PartialEq>(
    fa0: impl Fn() -> T::F<A>,
) -> R {
    T::eqr("identity: fmap id == id", T::fmap(fa0(), |a| a), fa0())
}

pub fn fmap_respects_composition<
    'a,
    T: Functor<'a> + Eqr<'a>,
    A: 'a,
    B: 'a,
    C: 'a + Debug + PartialEq,
>(
    f: impl 'a + Copy + Fn(B) -> C,
    g: impl 'a + Copy + Fn(A) -> B,
    fa0: impl Fn() -> T::F<A>,
) -> R {
    T::eqr(
        "composition: fmap (f . g) == fmap f . fmap g",
        T::fmap(fa0(), move |a| f(g(a))),
        T::fmap(T::fmap(fa0(), g), f),
    )
}

pub fn seq_respects_identity<'a, T: Applicative<'a> + Eqr<'a>, A: 'a + Debug + PartialEq>(
    fa0: impl Fn() -> T::F<A>,
) -> R {
    T::eqr(
        "identity: pure id <*> v = v",
        T::seq(T::pure(|a| a), fa0()),
        fa0(),
    )
}

pub fn seq_respects_composition<
    'a,
    T: Applicative<'a> + Eqr<'a>,
    A: 'a,
    B: 'a,
    C: 'a + Debug + PartialEq,
    F: 'a + Fn(B) -> C,
    G: 'a + Fn(A) -> B,
>(
    ff0: impl Fn() -> T::F<F>,
    fg0: impl Fn() -> T::F<G>,
    fa0: impl Fn() -> T::F<A>,
) -> R {
    T::eqr(
        "composition: pure (.) <*> u <*> v <*> w = u <*> (v <*> w)",
        T::seq(
            T::seq(
                T::seq(T::pure(|f: F| move |g: G| move |a| f(g(a))), ff0()),
                fg0(),
            ),
            fa0(),
        ),
        T::seq(ff0(), T::seq(fg0(), fa0())),
    )
}

pub fn seq_is_homomorphic<'a, T: Applicative<'a> + Eqr<'a>, A: 'a, B: 'a + Debug + PartialEq>(
    f: impl 'a + Fn(A) -> B,
    a0: impl Fn() -> A,
) -> R {
    T::eqr(
        "homomorphism: pure f <*> pure x = pure (f x)",
        T::pure(f(a0())),
        T::seq(T::pure(f), T::pure(a0())),
    )
}

pub fn seq_respects_interchange<
    'a,
    T: Applicative<'a> + Eqr<'a>,
    A: 'a,
    B: 'a + Debug + PartialEq,
    F: 'a + Fn(A) -> B,
>(
    ff0: impl Fn() -> T::F<F>,
    a0: impl 'a + Fn() -> A,
) -> R {
    T::eqr(
        "interchange: u <*> pure y = pure ($ y) <*> u",
        T::seq(ff0(), T::pure(a0())),
        T::seq(T::pure(move |f: F| f(a0())), ff0()),
    )
}

pub fn seq_can_be_expressed_via_la2<
    'a,
    T: Applicative<'a> + Eqr<'a>,
    A: 'a,
    B: 'a + Debug + PartialEq,
    F: 'a + Fn(A) -> B,
>(
    ff0: impl Fn() -> T::F<F>,
    fa0: impl Fn() -> T::F<A>,
) -> R {
    T::eqr(
        "seq via la2: (<*>) = liftA2 id",
        T::seq(ff0(), fa0()),
        T::la2(ff0(), fa0(), |f, a| f(a)),
    )
}

pub fn fmap_can_be_expressed_via_seq<
    'a,
    T: Applicative<'a> + Eqr<'a>,
    A: 'a,
    B: 'a + Debug + PartialEq,
>(
    f: impl 'a + Copy + Fn(A) -> B,
    fa0: impl Fn() -> T::F<A>,
) -> R {
    T::eqr(
        "fmap via seq: fmap f x = pure f <*> x",
        T::fmap(fa0(), f),
        T::seq(T::pure(f), fa0()),
    )
}

pub fn discard_can_be_expressed_via_seq_or_la2<
    'a,
    T: Applicative<'a> + Eqr<'a>,
    A: 'a,
    B: 'a + Debug + PartialEq,
>(
    fa0: impl 'a + Fn() -> T::F<A>,
    fb0: impl 'a + Fn() -> T::F<B>,
) -> R {
    T::eqr(
        "discard via seq: u *> v = (id <$ u) <*> v",
        T::discard_first(fa0(), fb0()),
        T::seq(T::replace(fa0(), |b| b), fb0()),
    ) + T::eqr(
        "discard via la2: u <* v = liftA2 const u v",
        T::discard_second(fb0(), fa0()),
        T::la2(fb0(), fa0(), |b, _| b),
    )
}

pub fn bind_respects_left_identity<'a, T: Monad<'a> + Eqr<'a>, A: 'a, B: 'a + Debug + PartialEq>(
    f: impl 'a + Fn(A) -> T::F<B>,
    a0: impl Fn() -> A,
) -> R {
    T::eqr(
        "left identity: pure a >>= k = k a",
        f(a0()),
        T::bind(T::pure(a0()), f),
    )
}

pub fn bind_respects_right_identity<'a, T: Monad<'a> + Eqr<'a>, A: 'a + Debug + PartialEq>(
    fa0: impl Fn() -> T::F<A>,
) -> R {
    T::eqr(
        "right identity: m >>= bind = m",
        T::bind(fa0(), T::pure),
        fa0(),
    )
}

pub fn bind_is_associative<'a, T: Monad<'a> + Eqr<'a>, A: 'a, B: 'a, C: 'a + Debug + PartialEq>(
    f: impl 'a + Clone + Fn(B) -> T::F<C>,
    g: impl 'a + Clone + Fn(A) -> T::F<B>,
    fa0: impl 'a + Fn() -> T::F<A>,
) -> R {
    T::eqr(
        r"associativity: m >>= (\x -> k x >>= h) = (m >>= k) >>= h",
        T::bind(T::bind(fa0(), g.clone()), f.clone()),
        T::bind(fa0(), move |a| T::bind(g(a), f)),
    )
}

pub fn seq_can_be_expressed_via_bind<
    'a,
    T: Monad<'a> + Eqr<'a>,
    A: 'a,
    B: 'a + Debug + PartialEq,
    F: 'a + Fn(A) -> B,
>(
    ff0: impl Fn() -> T::F<F>,
    fa0: impl 'a + Fn() -> T::F<A>,
) -> R {
    T::eqr(
        r"seq via bind: m1 <*> m2 = m1 >>= (\x1 -> m2 >>= (\x2 -> pure (x1 x2)))",
        T::seq(ff0(), fa0()),
        T::bind(ff0(), move |f| T::bind(fa0(), move |a| T::pure(f(a)))),
    )
}

pub fn fmap_can_be_expressed_via_bind<
    'a,
    T: Monad<'a> + Eqr<'a>,
    A: 'a,
    B: 'a + Debug + PartialEq,
>(
    f: impl 'a + Copy + Fn(A) -> B,
    fa0: impl 'a + Fn() -> T::F<A>,
) -> R {
    T::eqr(
        "fmap via bind: fmap f xs  =  xs >>= return . f",
        T::fmap(fa0(), f),
        T::bind(fa0(), move |a| T::pure(f(a))),
    )
}