from emis_funky_funktions import *

from ir import IRNeg, IRProp, IRTerm, IRVar, Substitutions, unify, unify_clauses

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

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