use std::collections::{HashMap, HashSet};
use itertools::Itertools;

use enum_map::{Enum, EnumMap};

use crate::item::Item;
use crate::character::Character;

type Time = u64;

#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct Var { index: u64 }

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Value {
    Var(Var),
    Item(Item),
    Character(Character),
    Time(Time),
}
impl From<Var> for Value { fn from(x: Var) -> Self {Value::Var(x)} }
impl From<Item> for Value { fn from(x: Item) -> Self {Value::Item(x)} }
impl From<Character> for Value { fn from(x: Character) -> Self {Value::Character(x)} }
impl From<Time> for Value { fn from(x: Time) -> Self {Value::Time(x)} }
impl TryFrom<Value> for Var {
    type Error = ();
    fn try_from(v: Value) -> Result<Self, Self::Error> {
        if let Value::Var(x) = v { Ok(x) } else { Err(()) }
    }
}
impl TryFrom<Value> for Item {
    type Error = ();
    fn try_from(v: Value) -> Result<Self, Self::Error> {
        if let Value::Item(x) = v { Ok(x) } else { Err(()) }
    }
}
impl TryFrom<Value> for Character {
    type Error = ();
    fn try_from(v: Value) -> Result<Self, Self::Error> {
        if let Value::Character(x) = v { Ok(x) } else { Err(()) }
    }
}
impl TryFrom<Value> for Time {
    type Error = ();
    fn try_from(v: Value) -> Result<Self, Self::Error> {
        if let Value::Time(x) = v { Ok(x) } else { Err(()) }
    }
}

#[derive(Debug, Default)]
pub struct Unification {
    assignment: HashMap<Var, Value>,
}
impl Unification {
    pub fn lookup(&self, v: &Var) -> Option<Value> {
        self.assignment.get(v).cloned()
    }
    pub fn add(&mut self, v: Var, x: impl Into<Value>) -> bool {
        let y = x.into();
        if let Some(old) = self.assignment.get(&v) {
            if let Value::Var(v2) = y {
                self.add(v2, *old)
            } else if let Value::Var(v2) = old {
                self.add(*v2, y)
            } else {
                *old == y
            }
        } else {
            self.assignment.insert(v, y);
            true
        }
    }
    pub fn unify_hole<A, B>(&mut self, h1: &Hole<A>, h2: &Hole<B>) -> bool
    where Value: From<A>, Value: From<B>, A: Copy, B: Copy {
        match (h1, h2) {
            (Hole::Var(v1), Hole::Var(v2)) =>
                self.add(*v1, *v2) && self.add(*v2, *v1),
            (Hole::Val(x1), Hole::Val(x2)) => Value::from(*x1) == Value::from(*x2),
            (Hole::Var(v1), Hole::Val(x2)) => self.add(*v1, *x2),
            (Hole::Val(x1), Hole::Var(v2)) => self.add(*v2, *x1),
        }
    }
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum Hole<T> {
    Var(Var),
    Val(T),
}
impl<T: Clone + TryFrom<Value>> Hole<T> {
    pub fn substitute(&self, u: &Unification) -> Self {
        match self {
            x@Self::Var(v) => if let Some(y) = u.lookup(v) && let Ok(z) = T::try_from(y) {
                Hole::Val(z)
            } else {
                x.clone()
            }
            x => x.clone(),
        }
    }
}

#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Enum)]
pub enum RelationSort {
    HasItem,
    UsedItemAt,
    TimeIs,
    FriendOf,
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
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 sort(&self) -> RelationSort {
        match self {
            Self::HasItem{..} => RelationSort::HasItem,
            Self::UsedItemAt{..} => RelationSort::UsedItemAt,
            Self::TimeIs{..} => RelationSort::TimeIs,
            Self::FriendOf{..} => RelationSort::FriendOf,
        }
    }
    pub fn unify(&self, other: &Self, mut u: Unification) -> Option<Unification> {
        match (self, other) {
            (Self::HasItem(c1, i1), Self::HasItem(c2, i2))
              if u.unify_hole(c1, c2) && u.unify_hole(i1, i2)
              => Some(u),
            (Self::UsedItemAt(c1, i1, t1), Self::UsedItemAt(c2, i2, t2))
              if u.unify_hole(c1, c2) && u.unify_hole(i1, i2) && u.unify_hole(t1, t2)
              => Some(u),
            (Self::TimeIs(t1), Self::TimeIs(t2))
              if u.unify_hole(t1, t2)
              => Some(u),
            (Self::FriendOf(x1, y1), Self::FriendOf(x2, y2))
              if u.unify_hole(x1, x2) && u.unify_hole(y1, y2)
              => Some(u),
            _ => None,
        }
    }
    pub fn substitute(&self, u: &Unification) -> Self {
        match self {
            Self::HasItem(c, i) => Self::HasItem(c.substitute(u), i.substitute(u)),
            Self::UsedItemAt(c, i, t) => Self::UsedItemAt(c.substitute(u), i.substitute(u), t.substitute(u)),
            Self::TimeIs(t) => Self::TimeIs(t.substitute(u)),
            Self::FriendOf(x, y) => Self::FriendOf(x.substitute(u), y.substitute(u)),
        }
    }
}

#[derive(Debug, Clone)]
pub struct Rule {
    pub head: Relation,
    pub body: Vec<Relation>,
}
impl Rule {
    pub fn unify_body(&self, facts: &[&Relation]) -> Option<Unification> {
        if self.body.len() != facts.len() { return None; }
        let mut u = Unification::default();
        for (r1, r2) in self.body.iter().zip(facts) {
            u = r1.unify(r2, u)?;
        }
        Some(u)
    }
}

#[derive(Debug, Default, Clone)]
pub struct Facts {
    facts: EnumMap<RelationSort, HashSet<Relation>>,
}
impl Facts {
    pub fn add(&mut self, f: Relation) -> bool {
        self.facts[f.sort()].insert(f)
    }
    pub fn with_sort(&self, s: RelationSort) -> &HashSet<Relation> {
        &self.facts[s]
    }
}

#[derive(Debug, Default, Clone)]
pub struct Database {
    facts: Facts,
    rules: Vec<Rule>,
}
impl Database {
    pub fn add_fact(&mut self, r: Relation) { self.facts.add(r); }
    pub fn add_rule(&mut self, r: Rule) { self.rules.push(r) }
    fn apply_rule(r: &Rule, facts: &mut Facts) -> bool {
        let found: Vec<Unification> = r.body.iter()
            .map(|r| facts.with_sort(r.sort())).multi_cartesian_product()
            .filter_map(|fs| r.unify_body(&fs))
            .collect();
        let mut changed = false;
        for u in found {
            if facts.add(r.head.substitute(&u)) { changed = true; }
        }
        changed
    }
    pub fn apply_rules_once(&mut self) -> bool {
        let mut changed = false;
        for r in self.rules.iter() {
            if Self::apply_rule(r, &mut self.facts) { changed = true }
        }
        changed
    }
    pub fn apply_rules(&mut self) {
        while self.apply_rules_once() {}
    }
}

#[derive(Debug, Default)]
pub struct Context {
    next_index: u64,
    var_names: HashMap<Var, String>,
}
impl Context {
    pub fn fresh(&mut self) -> Var {
        let ret = Var { index: self.next_index };
        self.next_index += 1;
        ret
    }
    pub fn var(&mut self, nm: &str) -> Var {
        let ret = self.fresh();
        self.var_names.insert(ret, nm.to_owned());
        ret
    }
}