use super::{Value, Hole, Unification};

use crate::time::*;
use crate::item::*;
use crate::character::*;

use enum_map::Enum;
use strum::EnumDiscriminants;

pub trait Concretizable {
    type Concrete;
    fn concretize(&self) -> Option<Self::Concrete>;
}
impl<A: Clone> Concretizable for Hole<A> {
    type Concrete = A;
    fn concretize(&self) -> Option<Self::Concrete> {
        match self {
            Self::Val(x) => Some(x.clone()),
            _ => None,
        }
    }
}
impl<
    A: Clone,
    B: Clone,
    > Concretizable for (Hole<A>, Hole<B>) {
    type Concrete = (A, B);
    fn concretize(&self) -> Option<Self::Concrete> {
        let a = self.0.concretize()?;
        let b = self.1.concretize()?;
        Some((a, b))
    }
}
impl<
    A: Clone,
    B: Clone,
    C: Clone,
    > Concretizable for (Hole<A>, Hole<B>, Hole<C>) {
        type Concrete = (A, B, C);
    fn concretize(&self) -> Option<Self::Concrete> {
        let a = self.0.concretize()?;
        let b = self.1.concretize()?;
        let c = self.2.concretize()?;
        Some((a, b, c))
    }
}
impl<
    A: Clone,
    B: Clone,
    C: Clone,
    D: Clone,
    > Concretizable for (Hole<A>, Hole<B>, Hole<C>, Hole<D>) {
        type Concrete = (A, B, C, D);
    fn concretize(&self) -> Option<Self::Concrete> {
        let a = self.0.concretize()?;
        let b = self.1.concretize()?;
        let c = self.2.concretize()?;
        let d = self.3.concretize()?;
        Some((a, b, c, d))
    }
}
impl<
    A: Clone,
    B: Clone,
    C: Clone,
    D: Clone,
    E: Clone,
    > Concretizable for (Hole<A>, Hole<B>, Hole<C>, Hole<D>, Hole<E>) {
        type Concrete = (A, B, C, D, E);
    fn concretize(&self) -> Option<Self::Concrete> {
        let a = self.0.concretize()?;
        let b = self.1.concretize()?;
        let c = self.2.concretize()?;
        let d = self.3.concretize()?;
        let e = self.4.concretize()?;
        Some((a, b, c, d, e))
    }
}

pub trait Substitutable {
    fn substitute(&self, u: &Unification) -> Self;
}
impl<A: Clone + TryFrom<Value>> Substitutable for Hole<A> {
    fn substitute(&self, u: &Unification) -> Self {
        match self {
            x@Self::Var(v) => if let Some(y) = u.lookup(v) && let Ok(z) = A::try_from(y) {
                Hole::Val(z)
            } else {
                x.clone()
            }
            x => x.clone(),
        }
    }
}
impl<
    A: Clone + TryFrom<Value>,
    B: Clone + TryFrom<Value>
    > Substitutable for (Hole<A>, Hole<B>) {
    fn substitute(&self, u: &Unification) -> Self {
        let (a, b) = self;
        (a.substitute(u), b.substitute(u))
    }
}
impl<
    A: Clone + TryFrom<Value>,
    B: Clone + TryFrom<Value>,
    C: Clone + TryFrom<Value>,
    > Substitutable for (Hole<A>, Hole<B>, Hole<C>) {
    fn substitute(&self, u: &Unification) -> Self {
        let (a, b, c) = self;
        (a.substitute(u), b.substitute(u), c.substitute(u))
    }
}
impl<
    A: Clone + TryFrom<Value>,
    B: Clone + TryFrom<Value>,
    C: Clone + TryFrom<Value>,
    D: Clone + TryFrom<Value>,
    > Substitutable for (Hole<A>, Hole<B>, Hole<C>, Hole<D>) {
    fn substitute(&self, u: &Unification) -> Self {
        let (a, b, c, d) = self;
        (a.substitute(u), b.substitute(u), c.substitute(u), d.substitute(u))
    }
}
impl<
    A: Clone + TryFrom<Value>,
    B: Clone + TryFrom<Value>,
    C: Clone + TryFrom<Value>,
    D: Clone + TryFrom<Value>,
    E: Clone + TryFrom<Value>,
    > Substitutable for (Hole<A>, Hole<B>, Hole<C>, Hole<D>, Hole<E>) {
    fn substitute(&self, u: &Unification) -> Self {
        let (a, b, c, d, e) = self;
        (a.substitute(u), b.substitute(u), c.substitute(u), d.substitute(u), e.substitute(u))
    }
}

pub trait Unifiable {
    fn unify(&self, other: &Self, u: Unification) -> Option<Unification>;
}
impl<A> Unifiable for Hole<A> where
    Value: From<A>, A: Copy, 
{
    fn unify(&self, other: &Self, mut u: Unification) -> Option<Unification> {
        if u.unify_hole(self, other) {
            Some(u)
        } else { None }
    }
}
impl<A, B> Unifiable for (Hole<A>, Hole<B>) where
    Value: From<A>, A: Copy, 
    Value: From<B>, B: Copy,
{
    fn unify(&self, other: &Self, mut u: Unification) -> Option<Unification> {
        let (a1, b1) = self;
        let (a2, b2) = other;
        if u.unify_hole(a1, a2) && u.unify_hole(b1, b2) {
            Some(u)
        } else { None }
    }
}
impl<A, B, C> Unifiable for (Hole<A>, Hole<B>, Hole<C>) where
    Value: From<A>, A: Copy, 
    Value: From<B>, B: Copy,
    Value: From<C>, C: Copy,
{
    fn unify(&self, other: &Self, mut u: Unification) -> Option<Unification> {
        let (a1, b1, c1) = self;
        let (a2, b2, c2) = other;
        if u.unify_hole(a1, a2) && u.unify_hole(b1, b2) && u.unify_hole(c1, c2) {
            Some(u)
        } else { None }
    }
}
impl<A, B, C, D> Unifiable for (Hole<A>, Hole<B>, Hole<C>, Hole<D>) where
    Value: From<A>, A: Copy, 
    Value: From<B>, B: Copy,
    Value: From<C>, C: Copy,
    Value: From<D>, D: Copy,
{
    fn unify(&self, other: &Self, mut u: Unification) -> Option<Unification> {
        let (a1, b1, c1, d1) = self;
        let (a2, b2, c2, d2) = other;
        if u.unify_hole(a1, a2) && u.unify_hole(b1, b2) && u.unify_hole(c1, c2) && u.unify_hole(d1, d2) {
            Some(u)
        } else { None }
    }
}
impl<A, B, C, D, E> Unifiable for (Hole<A>, Hole<B>, Hole<C>, Hole<D>, Hole<E>) where
    Value: From<A>, A: Copy, 
    Value: From<B>, B: Copy,
    Value: From<C>, C: Copy,
    Value: From<D>, D: Copy,
    Value: From<E>, E: Copy,
{
    fn unify(&self, other: &Self, mut u: Unification) -> Option<Unification> {
        let (a1, b1, c1, d1, e1) = self;
        let (a2, b2, c2, d2, e2) = other;
        if u.unify_hole(a1, a2) && u.unify_hole(b1, b2) && u.unify_hole(c1, c2) && u.unify_hole(d1, d2) && u.unify_hole(e1, e2) {
            Some(u)
        } else { None }
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash, EnumDiscriminants)]
#[strum_discriminants(derive(Enum))]
pub enum Relation {
    HasItem((Hole<Character>, Hole<Item>)),
    UsedItemAt((Hole<Character>, Hole<Item>, Hole<Time>)),
    TimeIs(Hole<Time>),
    FriendOf((Hole<Character>, Hole<Character>)),
}
impl Relation {
    pub fn is_concrete(&self) -> bool {
        match self {
            Self::HasItem(x) => x.concretize().is_some(),
            Self::UsedItemAt(x) => x.concretize().is_some(),
            Self::TimeIs(x) => x.concretize().is_some(),
            Self::FriendOf(x) => x.concretize().is_some(),
        }
    }
}
impl Substitutable for Relation {
    fn substitute(&self, u: &Unification) -> Self {
        match self {
            Self::HasItem(x) => Self::HasItem(x.substitute(u)),
            Self::UsedItemAt(x) => Self::UsedItemAt(x.substitute(u)),
            Self::TimeIs(x) => Self::TimeIs(x.substitute(u)),
            Self::FriendOf(x) => Self::FriendOf(x.substitute(u)),
        }
    }
}
impl Unifiable for Relation {
    fn unify(&self, other: &Self, u: Unification) -> Option<Unification> {
        match (self, other) {
            (Self::HasItem(a), Self::HasItem(b)) => a.unify(b, u),
            (Self::UsedItemAt(a), Self::UsedItemAt(b)) => a.unify(b, u),
            (Self::TimeIs(a), Self::TimeIs(b)) => a.unify(b, u),
            (Self::FriendOf(a), Self::FriendOf(b)) => a.unify(b, u),
            _ => None,
        }
    }
}