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

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

pub type R = TestResults;

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

pub trait Eqr: WeakFunctor {
    fn eqr<'a, A: PartialEq + Debug>(
        name: &'a str,
        left: Self::F<'a, A>,
        right: Self::F<'a, 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(le), Err(re)) => Err(le + "\n" + re.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 le), Err(re)) => {
                *le += "\n";
                *le += re.as_str()
            }
            (_, Ok(_)) => {}
            (lr, Err(re)) => *lr = Err(re),
        }
    }
}

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

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

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

pub fn seq_respects_composition<
    'a,
    T: 'a + Applicative + Eqr,
    A: 'a,
    B: 'a,
    C: 'a + Debug + PartialEq,
    F: 'a + Fn(B) -> C,
    G: 'a + Fn(A) -> B,
    FF0: Fn() -> T::F<'a, F>,
    FG0: Fn() -> T::F<'a, G>,
    FA0: Fn() -> T::F<'a, A>,
>(
    ff0: FF0,
    fg0: FG0,
    fa0: FA0,
) -> 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: 'a + Applicative + Eqr,
    A: 'a,
    B: 'a + Debug + PartialEq,
    A0: Fn() -> A,
    F: 'a + Fn(A) -> B,
>(
    f: F,
    a0: A0,
) -> 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: 'a + Applicative + Eqr,
    A: 'a,
    B: 'a + Debug + PartialEq,
    F: 'a + Fn(A) -> B,
    A0: 'a + Fn() -> A,
    FF0: Fn() -> T::F<'a, F>,
>(
    ff0: FF0,
    a0: A0,
) -> 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: 'a + Applicative + Eqr,
    A: 'a,
    B: 'a + Debug + PartialEq,
    F: 'a + Fn(A) -> B,
    FA0: Fn() -> T::F<'a, A>,
    FF0: Fn() -> T::F<'a, F>,
>(
    ff0: FF0,
    fa0: FA0,
) -> R {
    T::eqr(
        "seq via la2: (<*>) = liftA2 id",
        T::seq(ff0(), fa0()),
        T::la2(|f, a| f(a), ff0(), fa0()),
    )
}

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

pub fn discard_can_be_expressed_via_seq_or_la2<
    'a,
    T: 'a + Applicative + Eqr,
    A: 'a,
    B: 'a + Debug + PartialEq,
    FA0: 'a + Fn() -> T::F<'a, A>,
    FB0: 'a + Fn() -> T::F<'a, B>,
>(
    fa0: FA0,
    fb0: FB0,
) -> 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(|b, _| b, fb0(), fa0()),
    )
}

pub fn bind_respects_left_identity<
    'a,
    T: 'a + Monad + Eqr,
    A: 'a,
    B: 'a + Debug + PartialEq,
    F: 'a + Fn(A) -> T::F<'a, B>,
    A0: Fn() -> A,
>(
    f: F,
    a0: A0,
) -> 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: 'a + Monad + Eqr,
    A: 'a + Debug + PartialEq,
    FA0: Fn() -> T::F<'a, A>,
>(
    fa0: FA0,
) -> R {
    T::eqr(
        "right identity: m >>= bind = m",
        T::bind(fa0(), T::pure),
        fa0(),
    )
}

pub fn bind_is_associative<
    'a,
    T: 'a + Monad + Eqr,
    A: 'a,
    B: 'a,
    C: 'a + Debug + PartialEq,
    F: 'a + Clone + Fn(B) -> T::F<'a, C>,
    G: 'a + Clone + Fn(A) -> T::F<'a, B>,
    FA0: 'a + Fn() -> T::F<'a, A>,
>(
    f: F,
    g: G,
    fa0: FA0,
) -> 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: 'a + Monad + Eqr,
    A: 'a,
    B: 'a + Debug + PartialEq,
    F: 'a + Fn(A) -> B,
    FA0: 'a + Fn() -> T::F<'a, A>,
    FF0: Fn() -> T::F<'a, F>,
>(
    ff0: FF0,
    fa0: FA0,
) -> 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: 'a + Monad + Eqr,
    A: 'a,
    B: 'a + Debug + PartialEq,
    F: 'a + Copy + Fn(A) -> B,
    FA0: 'a + Fn() -> T::F<'a, A>,
>(
    f: F,
    fa0: FA0,
) -> R {
    T::eqr(
        "fmap via bind: fmap f xs  =  xs >>= return . f",
        T::fmap(f, fa0()),
        T::bind(fa0(), move |a| T::pure(f(a))),
    )
}