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.replacement}/{self.variable}'

@dataclass(frozen=True)
class IRProp:
	"""
	Represents a proposition or object for resolution

	Can have any number of arguments, each of which should be a `IRTerm`.  Note that no
	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]' = 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)
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)
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()