/*!
Judgemental equality and typing judgements
*/
use crate::graph::region::Parameter;
use super::{
    ValId,
    ValueEnum,
    lambda::Lambda,
    expr::Sexpr
};
use super::primitive::{
    logical::{Bool, LogicalOp, Unary, Binary},
    Unit
};

/// Objects which can be compared for judgemental equality.
///
/// Equal objects should *always* be judgementally equal:
/// equality will sometimes be referred to as "structural equality".
pub trait JEq<Rhs=Self> {
    /// Check whether two objects are judgementally equal
    fn jeq(&self, other: &Rhs) -> bool;
}

/// Set judgemental equality between two types to be the same as `PartialEq`
#[macro_export]
macro_rules! trivial_judgemental_equality {
    ($l:ty, $r:ty) => {
        impl JEq<$r> for $l {
            fn jeq(&self, other: &$r) -> bool { self.eq(other) }
        }
    };
    ($l:ty, $r:ty, comm) => {
        trivial_judgemental_equality!($l, $r);
        trivial_judgemental_equality!($r, $l);
    };
    ($p:ty) => { trivial_judgemental_equality!($p, $p); };
}

/// Implement judgemental equality with `ValueEnum`, and `ValId` from `JEq<ValueEnum>`
#[macro_export]
macro_rules! value_judgemental_equality {
    ($v:ty) => {
        impl JEq<$v> for ValueEnum {
            #[inline] fn jeq(&self, v: &$v) -> bool { v.jeq(self) }
        }
        impl JEq<$v> for ValId {
            #[inline] fn jeq(&self, v: &$v) -> bool { v.jeq(&self.data().value) }
        }
        impl JEq<ValId> for $v {
            #[inline] fn jeq(&self, v: &ValId) -> bool { v.jeq(self) }
        }
    }
}

/// Implemented judgemental equality with `Sexpr` from `JEq<ValueEnum>`
#[macro_export]
macro_rules! sexpr_judgemental_equality {
    ($v:ty) => {
        impl JEq<Sexpr> for $v {
            #[inline] fn jeq(&self, s: &Sexpr) -> bool { s.singleton_jeq(self) }
        }
        impl JEq<$v> for Sexpr {
            #[inline] fn jeq(&self, v: &$v) -> bool { v.jeq(self) }
        }
    }
}

/// Assert two values are judgementally equal
#[macro_export]
macro_rules! assert_jeq {
    ($l:expr, $r:expr) => {{ use crate::value::judgement::JEq; assert!($l.jeq($r)) }};
    ($l:expr, $r:expr, $m:literal $(, $vs:expr)*) => {{
        use crate::value::judgement::JEq;
        assert!($l.jeq($r), $m $(, $vs)*)
    }}
}

macro_rules! value_enum_variant_jeq {
    ($v:ty, $p:path) => {
        impl JEq<ValueEnum> for $v {
            fn jeq(&self, other: &ValueEnum) -> bool {
                match other {
                    ValueEnum::Sexpr(s) => s.jeq(self),
                    $p(v) => v.jeq(self),
                    _ => false
                }
            }
        }
        value_judgemental_equality!($v);
    }
}

macro_rules! trivial_value_enum_variant_jeq {
    ($v:ty, $p:path) => {
        trivial_judgemental_equality!($v);
        value_enum_variant_jeq!($v, $p);
        sexpr_judgemental_equality!($v);
    }
}

trivial_value_enum_variant_jeq!(bool, ValueEnum::Bool);
trivial_value_enum_variant_jeq!(Bool, ValueEnum::BoolTy);
trivial_value_enum_variant_jeq!(Unit, ValueEnum::UnitTy);
trivial_value_enum_variant_jeq!(LogicalOp, ValueEnum::LogicalOp);
trivial_value_enum_variant_jeq!(Lambda, ValueEnum::Lambda);
trivial_value_enum_variant_jeq!(Parameter, ValueEnum::Parameter);
trivial_judgemental_equality!(LogicalOp, Unary);
trivial_judgemental_equality!(LogicalOp, Binary);
trivial_value_enum_variant_jeq!(Unary, ValueEnum::LogicalOp);
trivial_value_enum_variant_jeq!(Binary, ValueEnum::LogicalOp);

impl Sexpr {
    /// Check if an S-expression is a singleton judgementally equal to `other`
    pub fn singleton_jeq<T: JEq<ValId>>(&self, other: &T) -> bool {
        if self.len() == 1 { other.jeq(&self[0]) } else { false }
    }
    /// Check if an S-expression is a singleton equal to `other`
    pub fn singleton_eq<T: PartialEq<ValId>>(&self, other: &T) -> bool {
        if self.len() == 1 { other == &self[0] } else { false }
    }
    /// Check if an S-expression is judgementally equal to the given arguments
    pub fn args_jeq<T: JEq<ValId>>(&self, other: &[T]) -> bool {
        if self.len() != other.len() { false }
        else {
            for (v, t) in self.iter().zip(other.iter()) {
                if !t.jeq(v) { return false }
            }
            return true
        }
    }
}

impl JEq<Sexpr> for Sexpr {
    fn jeq(&self, other: &Sexpr) -> bool {
        if self == other { true}
        else if self.len() == other.len() {
            for (l, r) in self.iter().zip(other.iter()) {
                if !l.jeq(r) { return false }
            }
            true
        } else if self.len() == 1 {
            other.jeq(&self[0])
        } else if other.len() == 1 {
            self.jeq(&other[0])
        } else {
            false
        }
    }
}

impl JEq<ValueEnum> for Sexpr {
    fn jeq(&self, other: &ValueEnum) -> bool {
        match other {
            ValueEnum::Sexpr(s) => self.jeq(s),
            v => self.singleton_jeq(v)
        }
    }
}

value_judgemental_equality!(Sexpr);

impl JEq for ValId {
    fn jeq(&self, other: &ValId) -> bool {
        self == other || self.data().value.jeq(other)
    }
}

impl JEq<ValId> for ValueEnum {
    fn jeq(&self, other: &ValId) -> bool {
        match self {
            ValueEnum::Sexpr(s) if s.singleton_eq(other) => true,
            v => other.data().value.jeq(v)
        }
    }
}

impl JEq<ValueEnum> for ValId {
    fn jeq(&self, other: &ValueEnum) -> bool { other.jeq(self) }
}

impl JEq for ValueEnum {
    fn jeq(&self, other: &ValueEnum) -> bool {
        match self {
            ValueEnum::Bool(b) => other.jeq(b),
            ValueEnum::BoolTy(b) => other.jeq(b),
            ValueEnum::Lambda(l) => other.jeq(l),
            ValueEnum::Parameter(p) => other.jeq(p),
            ValueEnum::LogicalOp(l) => other.jeq(l),
            ValueEnum::UnitTy(u) => other.jeq(u),
            ValueEnum::Sexpr(s) => other.jeq(s)
        }
    }
}

#[cfg(test)]
mod tests {
    use smallvec::smallvec;
    use super::*;

    #[test]
    fn boolean_judgemental_equality() {
        for i in [false, true].iter() {
            for j in [false, true].iter() {
                assert_eq!(i.jeq(j), i == j);
                assert_eq!(ValueEnum::Bool(*i).jeq(j), i == j);
                assert_eq!(ValueEnum::Bool(*i).jeq(&ValueEnum::Bool(*j)), i == j);
            }
            assert!(!ValueEnum::Bool(*i).jeq(&ValueEnum::UnitTy(Unit)));
            assert!(!Bool.jeq(&ValueEnum::Bool(*i)));
            assert!(!Unit.jeq(&ValueEnum::Bool(*i)));
        }
        assert!(Bool.jeq(&Bool));
    }

    #[test]
    fn basic_sexpr_judgemental_equality() {
        let ts = Sexpr::build(smallvec![ValId::from(true)]).expect("Valid sexpr");
        let fs = Sexpr::build(smallvec![
            ValId::from(true), ValId::from(false), LogicalOp::Binary(Binary::And).into()])
            .expect("Valid sexpr");
        let bsxp = [(ts, true), (fs, false)];
        let and = Sexpr::build(smallvec![LogicalOp::Binary(Binary::And).into()])
            .expect("Valid sexpr");
        for (i, iv) in bsxp.iter() {
            for j in [false, true].iter() {
                assert_eq!(i.singleton_jeq(j), iv == j,
                    "[Singleton] (#{}) == #{} != #{} == #{}", iv, j, iv, j);
                assert_eq!(i.jeq(j), iv == j, "[Value] (#{}) == #{} != #{} == #{}", iv, j, iv, j);
                assert_eq!(i.jeq(&ValueEnum::Bool(*j)), iv == j,
                    "[ValueEnum] (#{}) == #{} != #{} == #{}", iv, j, iv, j);
            }
            for (j, jv) in bsxp.iter() {
                assert_eq!(i.singleton_jeq(j), iv == jv,
                    "[Singleton] (#{}) == (#{}) != #{} == #{}", iv, jv, iv, jv);
                assert_eq!(i.jeq(j), iv == jv,
                    "[Value] (#{}) == (#{}) != #{} == #{}", iv, jv, iv, jv);
            }
            assert!(!i.jeq(&and));
            assert!(!i.jeq(&ValueEnum::UnitTy(Unit)));
            assert!(!Unit.jeq(i));
            assert!(!Bool.jeq(i));
        }
        assert!(and.jeq(&and));
        assert!(LogicalOp::Binary(Binary::And).jeq(&and));
        assert!(Bool.jeq(&Bool));
    }

}