import fol


class Kb:
    def __init__(self):
        self.base = []
        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)

            s = fol.unify(clause, other)
            # same = s is not None
            if same:
                return True
        return False

    def tell(self, request):
        req = self.make_f(request)
        self.check_request(req)
        self.base.append(req)

    def ask(self, request):
        while True:
            n = len(self.base)
            self.update()
            if n == len(self.base):
                break

        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 = []
            self.solve(rule, self.conds(rule), self.facts, solution, solutions)
            for sol in solutions:
                concl = conclusion.subst(sol)

                if not self.exists(concl) and concl.depth() < 4:
                    self.base.append([concl])
                    return

    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()