from typing import Any, TypeVar

import act4e_interfaces as I
from act4e_interfaces import FiniteRelation

from .relations_representation import MyFiniteRelation

E1 = TypeVar("E1")
E2 = TypeVar("E2")
E3 = TypeVar("E3")
E = TypeVar("E")

A = TypeVar("A")
B = TypeVar("B")


class SolFiniteRelationProperties(I.FiniteRelationProperties):
    def is_surjective(self, fr: I.FiniteRelation[Any, Any]) -> bool:
        # for all y in B there is an x in A s.t. x R y
        # converse: there is a y in B s.t. for all x in A there is no x R y
        for y in fr.target().elements():
            there_is_one = any([fr.holds(x, y) for x in fr.source().elements()])
            if not there_is_one:
                return False
        return True

    def is_defined_everywhere(self, fr: I.FiniteRelation[Any, Any]) -> bool:
        # for all x in A there is a y in B s.t. x R y
        # converse: there is an x in A s.t. for all y in B there is no x R y
        for x in fr.source().elements():
            there_is_one = any([fr.holds(x, y) for y in fr.target().elements()])
            if not there_is_one:
                return False
        return True

    def is_injective(self, fr: I.FiniteRelation[Any, Any]) -> bool:
        # x R y and z R y implies z = x
        # converse: there is a z neq y such that x R y and z R y
        image = []
        for y in fr.target().elements():
            for x in fr.source().elements():
                if fr.holds(x, y):
                    if y in image:
                        return False
                    image.append(y)
        return True

    def is_single_valued(self, fr: I.FiniteRelation[Any, Any]) -> bool:
        # x R y and x R u imply y = u
        # converse: there is an y neq u such that x R y and x R u
        domain = []
        for x in fr.source().elements():
            for y in fr.target().elements():
                if fr.holds(x, y):
                    if x in domain:
                        return False
                    domain.append(x)
        return True


class SolFiniteRelationOperations(I.FiniteRelationOperations):
    def transpose(self, fr: I.FiniteRelation[A, B]) -> I.FiniteRelation[B, A]:
        raise NotImplementedError()

    def as_relation(self, f: I.FiniteMap[A, B]) -> I.FiniteRelation[A, B]:
        raise NotImplementedError()


class SolFiniteEndorelationProperties(I.FiniteEndorelationProperties):
    def is_reflexive(self, fr: I.FiniteRelation[Any, Any]) -> bool:
        raise NotImplementedError()

    def is_irreflexive(self, fr: I.FiniteRelation[Any, Any]) -> bool:
        raise NotImplementedError()

    def is_transitive(self, fr: I.FiniteRelation[Any, Any]) -> bool:
        raise NotImplementedError()

    def is_symmetric(self, fr: I.FiniteRelation[Any, Any]) -> bool:
        raise NotImplementedError()

    def is_antisymmetric(self, fr: I.FiniteRelation[Any, Any]) -> bool:
        raise NotImplementedError()

    def is_asymmetric(self, fr: I.FiniteRelation[Any, Any]) -> bool:
        raise NotImplementedError()


class SolFiniteEndorelationOperations(I.FiniteEndorelationOperations):
    def transitive_closure(self, fr: I.FiniteRelation[E, E]) -> I.FiniteRelation[E, E]:
        raise NotImplementedError()


class SolFiniteRelationCompose(I.FiniteRelationCompose):
    def compose(self, fr1: FiniteRelation[E1, E2], fr2: FiniteRelation[E2, E3]) -> I.FiniteRelation[E1, E3]:
        values = []
        # Yeah O(n^3), i really should do this better
        for a in fr1.source().elements():
            for b in fr1.target().elements():
                for c in fr2.target().elements():
                    if fr1.holds(a, b) and fr2.holds(b, c):
                        values.append([a, c])

        return MyFiniteRelation(fr1.source(), fr2.target(), values)