trait Precedence
{
	fn precedence(&self) -> i32;
}

impl Precedence for crate::Term
{
	fn precedence(&self) -> i32
	{
		match &self
		{
			Self::Boolean(_)
			| Self::Function(_)
			| Self::SpecialInteger(_)
			| Self::Integer(_)
			| Self::String(_)
			| Self::Variable(_)
			| Self::UnaryOperation(
				crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
				=> 0,
			Self::UnaryOperation(
				crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..})
				=> 1,
			Self::BinaryOperation(
				crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, ..})
				=> 2,
			Self::BinaryOperation(
				crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, ..})
			| Self::BinaryOperation(
				crate::BinaryOperation{operator: crate::BinaryOperator::Divide, ..})
			| Self::BinaryOperation(
				crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
				=> 3,
			Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Add, ..})
			| Self::BinaryOperation(
				crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, ..})
				=> 4,
		}
	}
}

impl Precedence for crate::Formula
{
	fn precedence(&self) -> i32
	{
		match &self
		{
			Self::Predicate(_)
			| Self::Boolean(_)
			| Self::Compare(_)
				=> 0,
			Self::Exists(_)
			| Self::ForAll(_)
				=> 1,
			Self::Not(_)
				=> 2,
			Self::And(_)
				=> 3,
			Self::Or(_)
				=> 4,
			Self::Implies(_)
				=> 5,
			Self::IfAndOnlyIf(_)
				=> 6,
		}
	}
}

impl std::fmt::Debug for crate::SpecialInteger
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		match &self
		{
			Self::Infimum => write!(format, "#inf"),
			Self::Supremum => write!(format, "#sup"),
		}
	}
}

impl std::fmt::Display for crate::SpecialInteger
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{:?}", &self)
	}
}

impl std::fmt::Debug for crate::FunctionDeclaration
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{}/{}", &self.name, self.arity)
	}
}

impl std::fmt::Display for crate::FunctionDeclaration
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{:?}", &self)
	}
}

impl std::fmt::Debug for crate::PredicateDeclaration
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{}/{}", &self.name, self.arity)
	}
}

impl std::fmt::Display for crate::PredicateDeclaration
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{:?}", &self)
	}
}

impl std::fmt::Debug for crate::VariableDeclaration
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{}", &self.name)
	}
}

impl std::fmt::Display for crate::VariableDeclaration
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{:?}", &self)
	}
}

struct TermDisplay<'term>
{
	parent_precedence: Option<i32>,
	term: &'term crate::Term,
}

fn display_term(term: &crate::Term, parent_precedence: Option<i32>) -> TermDisplay
{
	TermDisplay
	{
		parent_precedence,
		term,
	}
}

impl<'term> std::fmt::Debug for TermDisplay<'term>
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		let precedence = self.term.precedence();
		let requires_parentheses = match self.parent_precedence
		{
			Some(parent_precedence) => precedence > parent_precedence,
			None => false,
		};

		if requires_parentheses
		{
			write!(format, "(")?;
		}

		match &self.term
		{
			crate::Term::Boolean(true) => write!(format, "true"),
			crate::Term::Boolean(false) => write!(format, "false"),
			crate::Term::SpecialInteger(value) => write!(format, "{:?}", value),
			crate::Term::Integer(value) => write!(format, "{}", value),
			crate::Term::String(value) => write!(format, "\"{}\"", value),
			crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration),
			crate::Term::Function(function) =>
			{
				write!(format, "{}", function.declaration.name)?;

				assert!(function.declaration.arity == function.arguments.len(),
					"number of function arguments differs from declaration (expected {}, got {})",
					function.declaration.arity, function.arguments.len());

				if !function.arguments.is_empty()
				{
					write!(format, "(")?;

					let mut separator = "";

					for argument in &function.arguments
					{
						write!(format, "{}{:?}", separator, display_term(&argument, None))?;

						separator = ", ";
					}

					write!(format, ")")?;
				}

				Ok(())
			},
			crate::Term::BinaryOperation(binary_operation) =>
			{
				let operator_string = match binary_operation.operator
				{
					crate::BinaryOperator::Add => "+",
					crate::BinaryOperator::Subtract => "-",
					crate::BinaryOperator::Multiply => "*",
					crate::BinaryOperator::Divide => "/",
					crate::BinaryOperator::Modulo => "%",
					crate::BinaryOperator::Exponentiate => "**",
				};

				let left_requires_parentheses = binary_operation.left.precedence() == precedence
					// Exponentiation is right-associative and thus requires parentheses when
					// nested on the left side
					&& binary_operation.operator == crate::BinaryOperator::Exponentiate;

				// The subtraction, division, and modulo operators require parentheses around the
				// right argument even if it has the same precedence
				let operator_requires_right_priority = match binary_operation.operator
				{
					crate::BinaryOperator::Subtract
					| crate::BinaryOperator::Divide
					| crate::BinaryOperator::Modulo
						=> true,
					_ => false,
				};

				// Additionally, modulo operations nested to the right of another multiplicative
				// operation always require parentheses
				let right_requires_priority = match *binary_operation.right
				{
					crate::Term::BinaryOperation(
						crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
						=> true,
					_ => false,
				};

				let right_requires_parentheses = binary_operation.right.precedence() == precedence
					&& (operator_requires_right_priority || right_requires_priority);

				if left_requires_parentheses
				{
					write!(format, "(")?;
				}

				write!(format, "{:?}", display_term(&binary_operation.left, Some(precedence)))?;

				if left_requires_parentheses
				{
					write!(format, ")")?;
				}

				write!(format, " {} ", operator_string)?;

				if right_requires_parentheses
				{
					write!(format, "(")?;
				}

				write!(format, "{:?}", display_term(&binary_operation.right, Some(precedence)))?;

				if right_requires_parentheses
				{
					write!(format, ")")?;
				}

				Ok(())
			},
			crate::Term::UnaryOperation(
				crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
				=> write!(format, "-{:?}", display_term(argument, Some(precedence))),
			crate::Term::UnaryOperation(
				crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
				=> write!(format, "|{:?}|", display_term(argument, None)),
		}?;

		if requires_parentheses
		{
			write!(format, ")")?;
		}

		Ok(())
	}
}

impl<'term> std::fmt::Display for TermDisplay<'term>
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{:?}", self)
	}
}

struct FormulaDisplay<'formula>
{
	parent_precedence: Option<i32>,
	formula: &'formula crate::Formula,
}

fn display_formula(formula: &crate::Formula, parent_precedence: Option<i32>) -> FormulaDisplay
{
	FormulaDisplay
	{
		parent_precedence,
		formula,
	}
}

impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		let precedence = self.formula.precedence();
		let requires_parentheses = match self.parent_precedence
		{
			Some(parent_precedence) => precedence > parent_precedence,
			None => false,
		};
		let precedence = Some(precedence);

		if requires_parentheses
		{
			write!(format, "(")?;
		}

		match &self.formula
		{
			crate::Formula::Exists(exists) =>
			{
				assert!(!exists.parameters.is_empty());

				write!(format, "exists")?;

				let mut separator = " ";

				for parameter in exists.parameters.iter()
				{
					write!(format, "{}{:?}", separator, parameter)?;

					separator = ", "
				}

				write!(format, " {:?}", display_formula(&exists.argument, precedence))?;
			},
			crate::Formula::ForAll(for_all) =>
			{
				assert!(!for_all.parameters.is_empty());

				write!(format, "forall")?;

				let mut separator = " ";

				for parameter in for_all.parameters.iter()
				{
					write!(format, "{}{:?}", separator, parameter)?;

					separator = ", "
				}

				write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
			},
			crate::Formula::Not(argument) => write!(format, "not {:?}",
				display_formula(argument, precedence))?,
			crate::Formula::And(arguments) =>
			{
				let mut separator = "";

				assert!(!arguments.is_empty());

				for argument in arguments
				{
					write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;

					separator = " and "
				}
			},
			crate::Formula::Or(arguments) =>
			{
				let mut separator = "";

				assert!(!arguments.is_empty());

				for argument in arguments
				{
					write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;

					separator = " or "
				}
			},
			crate::Formula::Implies(crate::Implies{direction, antecedent, implication}) =>
			{
				let operator_symbol = match direction
				{
					crate::ImplicationDirection::LeftToRight => "->",
					crate::ImplicationDirection::RightToLeft => "<-",
				};

				write!(format, "{:?} {} {:?}", display_formula(antecedent, precedence),
					operator_symbol, display_formula(implication, precedence))?;
			},
			crate::Formula::IfAndOnlyIf(arguments) =>
			{
				let mut separator = "";

				for argument in arguments
				{
					write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;

					separator = " <-> ";
				}
			},
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
				=> write!(format, "{:?} < {:?}", display_term(left, None),
					display_term(right, None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
				=> write!(format, "{:?} <= {:?}", display_term(left, None),
					display_term(right, None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
				=> write!(format, "{:?} > {:?}", display_term(left, None),
					display_term(right, None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
				=> write!(format, "{:?} >= {:?}", display_term(left, None),
					display_term(right, None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
				=> write!(format, "{:?} = {:?}", display_term(left, None),
					display_term(right, None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
				=> write!(format, "{:?} != {:?}", display_term(left, None),
					display_term(right, None))?,
			crate::Formula::Boolean(true) => write!(format, "true")?,
			crate::Formula::Boolean(false) => write!(format, "false")?,
			crate::Formula::Predicate(predicate) =>
			{
				write!(format, "{}", predicate.declaration.name)?;

				if !predicate.arguments.is_empty()
				{
					write!(format, "(")?;

					let mut separator = "";

					for argument in &predicate.arguments
					{
						write!(format, "{}{:?}", separator, display_term(argument, None))?;

						separator = ", "
					}

					write!(format, ")")?;
				}
			},
		}

		if requires_parentheses
		{
			write!(format, ")")?;
		}

		Ok(())
	}
}

impl<'formula> std::fmt::Display for FormulaDisplay<'formula>
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{:?}", self)
	}
}

impl std::fmt::Debug for crate::Formula
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{:?}", display_formula(&self, None))
	}
}

impl std::fmt::Display for crate::Formula
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{}", display_formula(&self, None))
	}
}

impl std::fmt::Debug for crate::Term
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{:?}", display_term(&self, None))
	}
}

impl std::fmt::Display for crate::Term
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{}", display_term(&self, None))
	}
}