From 8d3edb1ea801bb6506d237799729aff567c3bd02 Mon Sep 17 00:00:00 2001
From: Emi Simpson <emi@alchemi.dev>
Date: Sun, 5 Mar 2023 20:54:48 -0500
Subject: [PATCH] Add a notation of cantions

---
 ir.py | 87 ++++++++++++++++++++++++++++++++++++++++-------------------
 1 file changed, 60 insertions(+), 27 deletions(-)

diff --git a/ir.py b/ir.py
index 0cfc300..7c1b950 100644
--- a/ir.py
+++ b/ir.py
@@ -83,6 +83,14 @@ class IRProp:
 		return repr(self)
 	def __repr__(self) -> str:
 		return f'{self.name}({",".join(str(arg) for arg in self.arguments)})'
+	def __contains__(self, var: str) -> bool:
+		"""
+		Test if a variable with a given name exists in this term
+
+		>>> 'x1' in IRProp('friends', [IRProp('John'), IRProp('mother_of', [IRVar('x1')])])
+		True
+		"""
+		return any(var in term for term in self.arguments)
 
 @dataclass(frozen=True)
 class IRVar:
@@ -111,6 +119,17 @@ class IRVar:
 		return repr(self)
 	def __repr__(self) -> str:
 		return f'*{self.name}'
+	def __contains__(self, var: str) -> bool:
+		"""
+		Test if a variable with a given name exists in this term
+
+		>>> 'x1' in IRVar('x1')
+		True
+
+		>>> 'x1' in IRVar('x2')
+		False
+		"""
+		return var == self.name
 
 @dataclass(frozen=True)
 class IRNeg:
@@ -137,6 +156,14 @@ class IRNeg:
 		return repr(self)
 	def __repr__(self) -> str:
 		return f'¬{self.inner}'
+	def __contains__(self, var: str) -> bool:
+		"""
+		Test if a variable with a given name exists in this term
+
+		>>> 'x1' in IRNeg(IRProp('round', [IRVar('x1')]))
+		True
+		"""
+		return var in self.inner
 
 IRTerm: TypeAlias = IRVar | IRProp | IRNeg
 Clause: TypeAlias = Sequence[IRTerm]
@@ -155,37 +182,43 @@ kismesis(Karkat(), Karkat())
 """
 
 def unify(t1: IRTerm, t2: IRTerm) -> Result[Substitutions, UnificationError]:
-    """
-    Attempt to find a substitution that unifies two terms
+	"""
+	Attempt to find a substitution that unifies two terms
 
-    If successful, the returned substitutions will cause both term to be equal, when
-    applied to both.
+	If successful, the returned substitutions will cause both term to be equal, when
+	applied to both.
 
-    If this method fails, then the pair of subterms which caused the unification to fail
-    are returned.
+	If this method fails, then the pair of subterms which caused the unification to fail
+	are returned.
 
-    >>> unify(
-    ...     IRProp('imaginary', [IRProp('Rufio')]),
-    ...     IRProp('imaginary', [IRVar('x1')])
-    ... )
-    Ok((Rufio()/x1,))
+	>>> unify(
+	...		IRProp('imaginary', [IRProp('Rufio')]),
+	...		IRProp('imaginary', [IRVar('x1')])
+	... )
+	Ok((Rufio()/x1,))
 
-    >>> unify(
-    ...     IRProp('dating', [IRProp('Jade'), IRVar('x1')]),
-    ...     IRProp('dating', [IRVar('x1'), IRProp('John')])
-    ... )
-    Err(UnificationMismatch(term1=Jade(), term2=John()))
-    """
-    match (t1, t2):
-        case (IRVar(v1), IRVar(v2)) if v1 == v2:
-            return Ok(tuple())
-        case (IRVar(v), t_other) | (t_other, IRVar(v)):#type:ignore #TODO if v not in t_other:
-            return Ok((Subst(v, t_other),))
-        case (IRProp(n1, a1), IRProp(n2, a2)) if n1 == n2 and len(a1) == len(a2):
-            return unify_clauses(a1, a2)
-        case (IRNeg(i1), IRNeg(i2)):
-            return unify(i1, i2)
-    return Err(UnificationMismatch(t1, t2))
+	>>> unify(
+	...		IRProp('dating', [IRProp('Jade'), IRVar('x1')]),
+	...		IRProp('dating', [IRVar('x1'), IRProp('John')])
+	... )
+	Err(UnificationMismatch(term1=Jade(), term2=John()))
+
+	>>> unify(
+	...		IRProp('mother_of', [IRVar('x1')]),
+	...		IRVar('x1')
+	... )
+	Err(UnificationMismatch(term1=mother_of(*x1), term2=*x1))
+	"""
+	match (t1, t2):
+		case (IRVar(v1), IRVar(v2)) if v1 == v2:
+			return Ok(tuple())
+		case (IRVar(v), t_other) | (t_other, IRVar(v)) if v not in t_other: #type: ignore
+			return Ok((Subst(v, t_other),))
+		case (IRProp(n1, a1), IRProp(n2, a2)) if n1 == n2 and len(a1) == len(a2):
+			return unify_clauses(a1, a2)
+		case (IRNeg(i1), IRNeg(i2)):
+			return unify(i1, i2)
+	return Err(UnificationMismatch(t1, t2))
 
 def unify_clauses(c1: Clause, c2: Clause) -> Result[Substitutions, UnificationError]:
     """