import fol


class Kb:
    def __init__(self):
        self.base = []

        self.prev = []
        self.current = []

        self.indexes = {}
        self.counter = fol.cnf.Counter()

    def make_f(self, h):
        f = h
        if type(f) is str:
            f = fol.p(f)
        self.counter.begin()
        f = fol.cnf.cnf(f, self.counter)

        if f.name == 'OR':
            f = f.list_of('OR')
        else:
            f = [f]

        return f

    def make_req(self, h):
        f = h
        if type(f) is str:
            f = fol.p(f)

        if f.name == 'OR':
            f = f.list_of('OR')
        else:
            f = [f]

        return f

    def check_request(self, request):
        for r in request:
            if r.name not in ['NOT', 'PRED']:
                raise Exception(f'invalid statement {repr(r)}')

    def conds(self, statement):
        result = []
        for f in statement:
            if f.name == 'NOT':
                result.append(f.children[0])
        return result

    def conclusion(self, statement):
        for f in statement:
            if f.name != 'NOT':
                return f
        return None

    @property
    def rules(self):
        res = []
        for r in self.base:
            if len(r) > 1:
                res.append(r)
        return res

    @property
    def facts(self):
        res = []
        for r in self.base:
            if len(r) == 1:
                res.append(r[0])
        return res

    def exists(self, f):
        for g in self.base:
            if self.clause_equals([f], g):
                return True
        return False

    def clause_equals(self, left, right):
        if len(left) != len(right):
            return False

        for element in left:
            if not self.clause_in(element, right):
                return False

        for element in right:
            if not self.clause_in(element, left):
                return False

        return True

    def clause_in(self, clause, lst):
        for other in lst:
            same = clause.equals(other)
            if same:
                return True
        return False

    def add_req(self, req):
        if len(req) == 1:
            preds = []
            for r in req:
                preds.extend(r.find_by_name('PRED'))

            for p in preds:
                if p.value in self.indexes.keys():
                    self.indexes[p.value].append(req)
                else:
                    self.indexes[p.value] = [req]
        self.check_request(req)
        self.base.append(req)
        self.current.append(req)

    def tell(self, request):
        req = self.make_f(request)
        self.add_req(req)

    def generate(self):
        while True:
            self.update()
            self.prev = [c for c in self.current]
            self.current = []
            if len(self.prev) == 0:
                break

    def ask(self, request):
        self.generate()
        req = self.make_req(request)
        results = []

        for f in self.base:
            s = fol.unify(f, req)
            if s is not None:
                ok = True
                for k in s.keys():
                    if len(s[k].find_by_name('VAR')) > 0:
                        ok = False
                if ok:
                    results.append(s)

        return results

    def update(self):
        for rule in self.rules:
            conclusion = self.conclusion(rule)
            solution = []
            solutions = []

            preds = []
            for cond in self.conds(rule):
                preds.append(cond.value)
            facts = []
            for p in preds:
                if p in self.indexes.keys():
                    facts.extend(self.indexes[p])

            facts = [f[0] for f in facts]

            rules = self.conds(rule)

            if not self.is_rule_needed(rules, self.prev):
                continue

            self.solve(rule, rules, facts, solution, solutions)

            for sol in solutions:
                concl = conclusion.subst(sol)
                if concl.depth() < 8 and not self.exists(concl):
                    self.add_req([concl])
                    return

    def is_rule_needed(self, rule, prev):
        for f in prev:
            for r in rule:
                s = fol.unify(r, f[0])
                if s is not None:
                    return True
        return False

    def merge_substs(self, substs):
        res = {}
        for s in substs:
            for k in s.keys():
                if k in res.keys() and not res[k].equals(s[k]):
                    return None
                res[k] = s[k]
        return res

    def solve(self, rule, conds, facts, solution, solutions):
        if len(conds) == 0:
            substs = []

            for sol in solution:
                s = fol.unify(sol[0], sol[1])
                if s is not None:
                    substs.append(s)

            s = self.merge_substs(substs)

            if s is not None:
                solutions.append(s)
            return

        for cond in conds:
            for fact in facts:
                solution.append((cond, fact))

                self.solve(
                    rule,
                    [c for c in conds if c != cond],
                    [f for f in facts if f != fact],
                    solution,
                    solutions
                )

                solution.pop()