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

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

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

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

fn term_precedence(term: &crate::Term) -> u64
{
	match term
	{
		crate::Term::Infimum | crate::Term::Supremum | crate::Term::Integer(_) | crate::Term::Symbolic(_) | crate::Term::String(_) | crate::Term::Variable(_) => 0,
		crate::Term::Negative(_) => 1,
		crate::Term::Multiply(_, _) => 2,
		crate::Term::Add(_, _) | crate::Term::Subtract(_, _) => 3,
	}
}

fn formula_precedence(formula: &crate::Formula) -> u64
{
	match formula
	{
		crate::Formula::Predicate(_) | crate::Formula::Boolean(_) | crate::Formula::Less(_, _) | crate::Formula::LessOrEqual(_, _) | crate::Formula::Greater(_, _) | crate::Formula::GreaterOrEqual(_, _) | crate::Formula::Equal(_, _) | crate::Formula::NotEqual(_, _) => 0,
		crate::Formula::Exists(_) | crate::Formula::ForAll(_) => 1,
		crate::Formula::Not(_) => 2,
		crate::Formula::And(_) => 3,
		crate::Formula::Or(_) => 4,
		crate::Formula::Implies(_, _) => 5,
		crate::Formula::Biconditional(_, _) => 6,
	}
}

impl std::fmt::Debug for crate::VariableDeclaration
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		match &self.domain
		{
			crate::Domain::Program => write!(format, "X")?,
			crate::Domain::Integer => write!(format, "N")?,
		};

		write!(format, "{}", &self.name)
	}
}

impl std::fmt::Display for crate::VariableDeclaration
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		match &self.domain
		{
			crate::Domain::Program => write!(format, "X")?,
			crate::Domain::Integer => write!(format, "N")?,
		};

		write!(format, "{}", &self.name)
	}
}

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

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

		match self.term
		{
			crate::Term::Infimum => write!(format, "#inf"),
			crate::Term::Supremum => write!(format, "#sup"),
			crate::Term::Integer(value) => write!(format, "{}", value),
			crate::Term::Symbolic(ref value) => write!(format, "{}", value),
			crate::Term::String(ref value) => write!(format, "\"{}\"", value),
			crate::Term::Variable(ref declaration) => write!(format, "{:?}", declaration),
			crate::Term::Add(ref left, ref right) => write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)),
			crate::Term::Subtract(ref left, ref right) => write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)),
			crate::Term::Multiply(ref left, ref right) => write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)),
			crate::Term::Negative(ref argument) => write!(format, "-{:?}", display_term(argument, precedence)),
		}?;

		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)
	}
}

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

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

		match self.formula
		{
			crate::Formula::Exists(ref exists) =>
			{
				write!(format, "exists")?;

				let mut separator = " ";

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

					separator = ", "
				}

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

				let mut separator = " ";

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

					separator = ", "
				}

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

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

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

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

					separator = " or "
				}
			},
			crate::Formula::Implies(ref left, ref right) => write!(format, "{:?} -> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
			crate::Formula::Biconditional(ref left, ref right) => write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
			crate::Formula::Less(ref left, ref right) => write!(format, "{:?} < {:?}", display_term(left, 1000), display_term(right, 1000))?,
			crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "{:?} <= {:?}", display_term(left, 1000), display_term(right, 1000))?,
			crate::Formula::Greater(ref left, ref right) => write!(format, "{:?} > {:?}", display_term(left, 1000), display_term(right, 1000))?,
			crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "{:?} >= {:?}", display_term(left, 1000), display_term(right, 1000))?,
			crate::Formula::Equal(ref left, ref right) => write!(format, "{:?} = {:?}", display_term(left, 1000), display_term(right, 1000))?,
			crate::Formula::NotEqual(ref left, ref right) => write!(format, "{:?} != {:?}", display_term(left, 1000), display_term(right, 1000))?,
			crate::Formula::Boolean(value) =>
				match value
				{
					true => write!(format, "#true")?,
					false => write!(format, "#false")?,
				},
			crate::Formula::Predicate(ref 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, 1000))?;

						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, 1000))
	}
}

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

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

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