Implement substitution

ir.py

@@ -1,6 +1,24 @@
 from dataclasses import dataclass
 from typing import Sequence, TypeAlias
 
+@dataclass(frozen=True)
+class Subst:
+	"""
+	A substitution which may be performed on a term.
+
+	Only variables may be substituted, but they may be substituted with any term.  That
+	is, `x1/Chris` is valid, but `Chris/x1` is not.
+
+	It is strongly recommended to avoid recursive substitutions, that is, substitutions
+	which contain the variable they are replacing
+	"""
+	variable: str
+	replacement: 'IRTerm'
+	def __str__(self) -> str:
+		return repr(self)
+	def __repr__(self) -> str:
+		return f'{self.variable}/{self.replacement}'
+
 @dataclass(frozen=True)
 class IRProp:
 	"""
@@ -10,12 +28,32 @@ class IRProp:
 	distinction is made between predicates (n-arity, logical statements), functions
 	(positive-arity functions over objects), and constants (stand-ins for objects)
 	"""
+
 	name: str
 	"""
 	The identifier of this thing, including its location in the source
 	"""
-	arguments: 'Sequence[IRTerm]'
+
+	arguments: 'Sequence[IRTerm]' = tuple()
+
+	def subst(self, subst: Subst) -> 'IRTerm':
+		"""
+		Perform substitution on a proposition
+
+		Returns the same proposition, but with any instances of the variable named in the
+		substitution replaced with the contents of the substitution.
+
+		>>> original = IRProp('angry', (IRVar('x1'),))
+		>>> original
+		angry(*x1)
+
+		>>> original.subst(Subst('x1', IRProp('Alex')))
+		angry(Alex())
+		"""
+		return IRProp(self.name, [arg.subst(subst) for arg in self.arguments])
 	def __str__(self) -> str:
+		return repr(self)
+	def __repr__(self) -> str:
 		return f'{self.name}({",".join(str(arg) for arg in self.arguments)})'
 
 @dataclass(frozen=True)
@@ -24,7 +62,26 @@ class IRVar:
 	A variable which may be substituted for any other term
 	"""
 	name: str
+	def subst(self, subst: Subst) -> 'IRTerm':
+		"""
+		Perform substitution on a proposition
+
+		Returns the same proposition, but with any instances of the variable named in the
+		substitution replaced with the contents of the substitution.
+
+		>>> IRVar('x1').subst(Subst('x1', IRProp('Alex')))
+		Alex()
+
+		>>> IRVar('x1').subst(Subst('x2', IRProp('Alex')))
+		*x1
+		"""
+		if self.name == subst.variable:
+			return subst.replacement
+		else:
+			return self
 	def __str__(self) -> str:
+		return repr(self)
+	def __repr__(self) -> str:
 		return f'*{self.name}'
 
 @dataclass(frozen=True)
@@ -33,7 +90,28 @@ class IRNeg:
 	A negated proposition
 	"""
 	inner: 'IRTerm'
+	def subst(self, subst: Subst) -> 'IRTerm':
+		"""
+		Perform substitution on a proposition
+
+		Returns the same proposition, but with any instances of the variable named in the
+		substitution replaced with the contents of the substitution.
+
+		>>> original = IRNeg(IRProp('happy', [IRVar('x1')]))
+		>>> original
+		¬happy(*x1)
+
+		>>> original.subst(Subst('x1', IRProp('parent', [IRProp('Susie')])))
+		¬happy(parent(Susie()))
+		"""
+		return IRNeg(self.inner.subst(subst))
 	def __str__(self) -> str:
+		return repr(self)
+	def __repr__(self) -> str:
 		return f'¬{self.inner}'
 
 IRTerm: TypeAlias = IRVar | IRProp | IRNeg
+
+if __name__ == '__main__':
+	import doctest
+	doctest.testmod()