from emis_funky_funktions import *

from itertools import combinations, product
from operator import eq
from typing import Collection, FrozenSet, TypeAlias

from ir import Clause, Clause_, IRNeg, IRProp, IRTerm, IRVar, Substitutions, sub_all, unify

KnowledgeBase: TypeAlias = FrozenSet[Clause]
KnowledgeBase_: TypeAlias = Collection[Clause_]
"""
A more general version of `KnowledgeBase`

`KnowledgeBase_` : `KnowledgeBase` :: `Clause_` : `Clause`

A superclass of `KnowledgeBase`
"""

def terms_cancel(t1: IRTerm, t2: IRTerm) -> Option[Substitutions]:
	"""
	Determine if two terms could cancel each other out, given the right substitutions

	That is, is there some set of substitutions such that t1 = ¬t2 or ¬t1 = t2?

	If negation is possible and a substitution exists, that substitution is returned.
	Otherwise, `None` is returned.

	>>> terms_cancel(IRNeg(IRVar('x1')), IRProp('Terezi'))
	Some((Terezi()/x1,))

	>>> terms_cancel(IRProp('Nepeta'), IRVar('x1'))
	Some((¬Nepeta()/x1,))

	>>> terms_cancel(IRProp('ancestor', [IRVar('x1')]), IRVar('x1')) is None
	True
	"""
	match (t1, t2):
		case (IRNeg(a), b) | (b, IRNeg(a)): #type: ignore
			return hush(unify(a, b))
		case (IRVar(_) as x, a) | (a, IRVar(_) as x): #type: ignore
			return hush(unify(x, IRNeg(a)))
	return None

def merge_clauses(c1: Clause_, c2: Clause_) -> KnowledgeBase:
    """
    Produce a list of all possible clauses which resolution could derive from c1 and c2

    For each term in c1 that could cancel with a term in c2 using a substitution, a
    possible clause is produced equal to the union of c1 and c2 with the canceled
    terms removed and the substitution applied.

    >>> merge_clauses(
    ...     [ IRProp('day'), IRNeg(IRProp('night')) ],
    ...     [ IRProp('night') ]
    ... )
    { { day() } }

    >>> merge_clauses(
    ...     [ IRNeg(IRProp('transgender', [IRVar('x1')])), IRProp('powerful', [IRVar('x1')]) ],
    ...     [ IRNeg(IRProp('powerful', [IRVar('x2')])), IRProp('god', [IRVar('x2')]) ]
    ... )
    { { god(*x1), ¬transgender(*x1) } }

    >>> merge_clauses(
    ...     [ IRNeg(IRProp('day')), IRProp('night') ],
    ...     [ IRVar('x2') ]
    ... )
    { { night() }, { ¬day() } }

    If two clauses cannot merge, an empty set is returned

    >>> merge_clauses(
    ...     [ IRProp('day') ],
    ...     [ IRProp('wet') ]
    ... )
    { }
    """
    terms1, terms2 = list(c1), list(c2)
    valid_substitutions = drop_none(
        map_opt(lambda subs: (subs, i1, i2), terms_cancel(t1, t2))
        for ((i1, t1), (i2, t2)) in product(enumerate(terms1), enumerate(terms2))
    )
    return FSet(
        FSet(
            sub_all(subs, term)
            for term in (*terms1[:i1], *terms1[i1 + 1:], *terms2[:i2], *terms2[i2 + 1:])
        )
        for (subs, i1, i2) in valid_substitutions
    )

def derive(clauses: KnowledgeBase_) -> KnowledgeBase:
    """
    All possible clauses which derive in one step of resolution from a knowledge base

    Attempts to merge every possible combination of clauses, in the knowledge base.

    >>> derive([
    ...     [IRNeg(IRProp('animal', [IRProp('Kim')]))],
    ...     [IRNeg(IRProp('dog', [IRVar('x0')])), IRProp('animal', [IRVar('x0')])],
    ...     [IRNeg(IRProp('cat', [IRVar('x1')])), IRProp('animal', [IRVar('x1')])],
    ...     [IRProp('dog', [IRProp('Kim')])],
    ... ]) #doctest: +NORMALIZE_WHITESPACE
    {
        { animal(Kim()) },
        { ¬cat(Kim())   },
        { ¬dog(Kim())   }
    }
    """
    return FSet(
        FSet(clause)
        for (c1, c2) in combinations(clauses, 2)
        for clause in merge_clauses(c1, c2)
    )

def derive2(kb1: KnowledgeBase_, kb2: KnowledgeBase_) -> KnowledgeBase:
    """
    All clauses which derive in one step from the combination of two knowledge bases

    Each resulting clause is the combination of one clause from the left knowledge base
    with exactly one clause from the right knowledge base.  Clauses from the same
    knowledge base will not be combined.

    >>> derive2([
    ...     [IRNeg(IRProp('animal', [IRProp('Kim')]))],
    ...     [IRNeg(IRProp('cat', [IRVar('x1')])), IRProp('animal', [IRVar('x1')])],
    ... ], [
    ...     [IRNeg(IRProp('dog', [IRVar('x0')])), IRProp('animal', [IRVar('x0')])],
    ...     [IRProp('dog', [IRProp('Kim')])],
    ... ])
    { { ¬dog(Kim()) } }
    """
    return FSet(
        FSet(clause)
        for (c1, c2) in product(kb1, kb2)
        for clause in merge_clauses(c1, c2)
    )

is_false: Callable[[Clause_], bool] = c(p(eq, 0), len)
"""
Determines whether a clause is equivalent to false

This is only true for the empty clause.

>>> is_false([])
True

>>> is_false([IRProp('real')])
False
"""

false_clause: Clause = FSet()
"""
The clause which represents the logical condition False

i.e. the empty clause
"""


def next_generation(
    previous_generations: KnowledgeBase_,
    current_generation: KnowledgeBase_,
) -> KnowledgeBase:
	"""
	Advance resolution by one step

	This performs `derive()` on the current generation as well as `derive2()` between the
	current generation and all clauses from previous generations in order to produce a new
	generation, hopefully with new and interesting clauses in it.

	When using the new generation, previous generations should be considered to be the sum
	of all clauses within the two knowledge bases passed to this function.  That is, all
	clauses which were used in the generation of that generation.

	### Example

	Starting from an example knowledge base, we produce a new generation.  Notice that the
	empty list for previous generations indicates that this is the zeroth (original)
	knowledge base.

	>>> next_generation([
	... ], [
	...     [IRNeg(IRProp('animal', [IRProp('Kim')]))],
	...     [IRNeg(IRProp('dog', [IRVar('x0')])), IRProp('animal', [IRVar('x0')])],
	...     [IRNeg(IRProp('cat', [IRVar('x1')])), IRProp('animal', [IRVar('x1')])],
	...     [IRProp('dog', [IRProp('Kim')])],
	... ]) #doctest: +NORMALIZE_WHITESPACE
	{
		{ animal(Kim()) },
		{ ¬cat(Kim())   },
		{ ¬dog(Kim())   }
	}

	Now, we perform the next round of resolution.  All of the terms originally passed into
	the first generation have been moved to the previous generations knowledge base, and
	the current generation contains only the results from the first call.

	>>> next_generation([
	...     [IRNeg(IRProp('animal', [IRProp('Kim')]))],
	...     [IRNeg(IRProp('dog', [IRVar('x0')])), IRProp('animal', [IRVar('x0')])],
	...     [IRNeg(IRProp('cat', [IRVar('x1')])), IRProp('animal', [IRVar('x1')])],
	...     [IRProp('dog', [IRProp('Kim')])],
	... ], [
	...     [IRNeg(IRProp('dog', [IRProp('Kim')]))],
	...     [IRNeg(IRProp('cat', [IRProp('Kim')]))],
	...     [IRProp('animal', [IRProp('Kim')])],
	... ])
	{ { } }

	The return of a knowledge base containing false (ie `[]`) indicates that resolution
	has found a contradiction.  In this case, there are two:  One from ¬dog(Kim) and
	dog(Kim), and one from animal(Kim) and ¬animal(Kim).
	"""
	return fset(*derive(current_generation), *derive2(current_generation, previous_generations))

def derives_false(
	knowledge_base: KnowledgeBase,
	previous_generations: KnowledgeBase = FSet(),
) -> bool:
	"""
	Determine if it is possible to derive false from a given knowledge base.

	Uses any number of generations of resolution via `next_generation()` to find a
	generation which contains the `false_clause`, indicating that the original knowledge
	base (and all subsiquent generations) are contradictory.

	`previous_generations` may be set if the current knowledge base was derived from some
	other series of clauses using `derive()`.

	>>> derives_false(fset(
	...     fset( IRNeg(IRProp('animal', (IRProp('Kim'),)))                              ),
	...     fset( IRNeg(IRProp('dog', (IRVar('x0'),))), IRProp('animal', (IRVar('x0'),)) ),
	...     fset( IRNeg(IRProp('cat', (IRVar('x1'),))), IRProp('animal', (IRVar('x1'),)) ),
	...     fset( IRProp('dog', (IRProp('Kim'),))                                        ),
	... ))
	True

	>>> derives_false(fset(
	...     fset( IRNeg(IRProp('animal', (IRProp('Kim'),)))                              ),
	...     fset( IRNeg(IRProp('dog', (IRVar('x0'),))), IRProp('animal', (IRVar('x0'),)) ),
	...     fset( IRNeg(IRProp('cat', (IRVar('x1'),))), IRProp('animal', (IRVar('x1'),)) ),
	... ))
	False
	"""
	if false_clause in knowledge_base:
		return True
	elif len(knowledge_base) == 0:
		return False
	else:
		return derives_false(
			next_generation(previous_generations, knowledge_base),
			knowledge_base | previous_generations
		)


if __name__ == '__main__':
	import doctest
	doctest.testmod()