use super::*;

impl super::Precedence for crate::Formula
{
	fn precedence_level(&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::ImplicationDirection
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		match &self
		{
			Self::LeftToRight => write!(format, "left to right"),
			Self::RightToLeft => write!(format, "right to left"),
		}
	}
}

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

struct FormulaDisplay<'formula>
{
	parentheses: Parentheses,
	formula: &'formula crate::Formula,
}

fn display_formula(formula: &crate::Formula, parentheses: Parentheses) -> FormulaDisplay
{
	FormulaDisplay
	{
		parentheses,
		formula,
	}
}

impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		let precedence_level = self.formula.precedence_level();
		let requires_parentheses = match self.parentheses
		{
			Parentheses::None => false,
			Parentheses::PrecedenceBased(parent_precedence_level)
				=> precedence_level > parent_precedence_level,
			Parentheses::Required => true,
		};
		let parentheses = Parentheses::PrecedenceBased(precedence_level);

		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, parentheses))?;
			},
			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, parentheses))?;
			},
			crate::Formula::Not(argument) => write!(format, "not {:?}",
				display_formula(argument, parentheses))?,
			crate::Formula::And(arguments) =>
			{
				let mut separator = "";

				assert!(!arguments.is_empty());

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

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

				assert!(!arguments.is_empty());

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

					separator = " or "
				}
			},
			crate::Formula::Implies(crate::Implies{direction, antecedent, implication}) =>
			{
				let antecedent_parentheses = match **antecedent
				{
					// Implication is right-associative and thus requires parentheses when nested on
					// the antecedent side
					crate::Formula::Implies(_) => Parentheses::Required,
					_ => parentheses,
				};

				let implication_parentheses = match **antecedent
				{
					// Implication is right-associative and thus doesn’t require parentheses when
					// nested on the implication side with the same implication direction
					crate::Formula::Implies(crate::Implies{direction: nested_direction, ..})
						if nested_direction == *direction => Parentheses::None,
					// If the nested implication is in the other direction, parentheses are needed
					crate::Formula::Implies(_) => Parentheses::Required,
					_ => parentheses,
				};

				let format_antecedent = |format: &mut std::fmt::Formatter| -> Result<_, _>
				{
					write!(format, "{:?}", display_formula(antecedent, antecedent_parentheses))
				};

				let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _>
				{
					write!(format, "{:?}", display_formula(implication, implication_parentheses))
				};

				match direction
				{
					crate::ImplicationDirection::LeftToRight =>
					{
						format_antecedent(format)?;
						write!(format, " -> ")?;
						format_implication(format)?;
					},
					crate::ImplicationDirection::RightToLeft =>
					{
						format_implication(format)?;
						write!(format, " <- ")?;
						format_antecedent(format)?;
					},
				}
			},
			crate::Formula::IfAndOnlyIf(arguments) =>
			{
				let mut separator = "";

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

					separator = " <-> ";
				}
			},
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
				=> write!(format, "{:?} < {:?}", display_term(left, Parentheses::None),
					display_term(right, Parentheses::None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
				=> write!(format, "{:?} <= {:?}", display_term(left, Parentheses::None),
					display_term(right, Parentheses::None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
				=> write!(format, "{:?} > {:?}", display_term(left, Parentheses::None),
					display_term(right, Parentheses::None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
				=> write!(format, "{:?} >= {:?}", display_term(left, Parentheses::None),
					display_term(right, Parentheses::None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
				=> write!(format, "{:?} = {:?}", display_term(left, Parentheses::None),
					display_term(right, Parentheses::None))?,
			crate::Formula::Compare(
				crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
				=> write!(format, "{:?} != {:?}", display_term(left, Parentheses::None),
					display_term(right, Parentheses::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, Parentheses::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, Parentheses::None))
	}
}

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

#[cfg(test)]
mod tests
{
	use crate::*;

	fn format(formula: &ast::Formula) -> String
	{
		format!("{}", formula)
	}

	#[test]
	fn compare()
	{
		let ad = std::rc::Rc::new(FunctionDeclaration::new("a".to_string(), 0));
		let bd = std::rc::Rc::new(FunctionDeclaration::new("b".to_string(), 0));

		let a = || Box::new(Term::function(std::rc::Rc::clone(&ad), vec![]));
		let b = || Box::new(Term::function(std::rc::Rc::clone(&bd), vec![]));

		assert_eq!(format(&Formula::greater(a(), b())), "a > b");
		assert_eq!(format(&Formula::less(a(), b())), "a < b");
		assert_eq!(format(&Formula::less_or_equal(a(), b())), "a <= b");
		assert_eq!(format(&Formula::greater_or_equal(a(), b())), "a >= b");
		assert_eq!(format(&Formula::equal(a(), b())), "a = b");
		assert_eq!(format(&Formula::not_equal(a(), b())), "a != b");
	}
}