from dataclasses import dataclass
from typing import Sequence, TypeAlias

@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]'
	def __str__(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 __str__(self) -> str:
		return f'*{self.name}'

@dataclass(frozen=True)
class IRNeg:
	"""
	A negated proposition
	"""
	inner: 'IRTerm'
	def __str__(self) -> str:
		return f'¬{self.inner}'

IRTerm: TypeAlias = IRVar | IRProp | IRNeg