From db2f9710ddc26967c67a9668b8b4534eae058f1f Mon Sep 17 00:00:00 2001
From: Emi Simpson <emi@alchemi.dev>
Date: Sun, 5 Mar 2023 21:35:14 -0500
Subject: [PATCH] Add a cancelation checker

---
 resolution.py | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 resolution.py

diff --git a/resolution.py b/resolution.py
new file mode 100644
index 0000000..3a7c79c
--- /dev/null
+++ b/resolution.py
@@ -0,0 +1,32 @@
+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()
\ No newline at end of file