pub trait DisplayTPTP<'a, DisplayType>
	where DisplayType: 'a + std::fmt::Debug + std::fmt::Display
{
	fn display_tptp(&'a self) -> DisplayType;
}

fn is_arithmetic_term(term: &foliage::Term) -> bool
{
	match term
	{
		foliage::Term::Infimum => false,
		foliage::Term::Supremum => false,
		foliage::Term::Integer(_) => true,
		foliage::Term::Symbolic(_) => false,
		foliage::Term::String(_) => false,
		foliage::Term::Variable(ref declaration) => match declaration.domain
		{
			foliage::Domain::Program => false,
			foliage::Domain::Integer => true,
		},
		foliage::Term::Add(ref left, ref right) => is_arithmetic_term(left) && is_arithmetic_term(right),
		foliage::Term::Subtract(ref left, ref right) => is_arithmetic_term(left) && is_arithmetic_term(right),
		foliage::Term::Multiply(ref left, ref right) => is_arithmetic_term(left) && is_arithmetic_term(right),
		foliage::Term::Negative(ref argument) => is_arithmetic_term(argument),
	}
}

fn collect_predicate_declarations_in_formula<'a>(
	predicate_declarations: &mut std::collections::HashSet<&'a foliage::PredicateDeclaration>, formula: &'a foliage::Formula)
{
	match formula
	{
		foliage::Formula::Exists(ref exists) => collect_predicate_declarations_in_formula(predicate_declarations, &exists.argument),
		foliage::Formula::ForAll(ref for_all) => collect_predicate_declarations_in_formula(predicate_declarations, &for_all.argument),
		foliage::Formula::Not(ref argument) => collect_predicate_declarations_in_formula(predicate_declarations, argument),
		foliage::Formula::And(ref arguments) =>
			for argument in arguments
			{
				collect_predicate_declarations_in_formula(predicate_declarations, argument);
			},
		foliage::Formula::Or(ref arguments) =>
			for argument in arguments
			{
				collect_predicate_declarations_in_formula(predicate_declarations, argument);
			},
		foliage::Formula::Implies(ref left, ref right) =>
		{
			collect_predicate_declarations_in_formula(predicate_declarations, left);
			collect_predicate_declarations_in_formula(predicate_declarations, right);
		},
		foliage::Formula::Biconditional(ref left, ref right) =>
		{
			collect_predicate_declarations_in_formula(predicate_declarations, left);
			collect_predicate_declarations_in_formula(predicate_declarations, right);
		},
		foliage::Formula::Less(_, _) => (),
		foliage::Formula::LessOrEqual(_, _) => (),
		foliage::Formula::Greater(_, _) => (),
		foliage::Formula::GreaterOrEqual(_, _) => (),
		foliage::Formula::Equal(_, _) => (),
		foliage::Formula::NotEqual(_, _) => (),
		foliage::Formula::Boolean(_) => (),
		foliage::Formula::Predicate(ref predicate) =>
		{
			predicate_declarations.insert(&predicate.declaration);
		},
	}
}

fn collect_predicate_declarations_in_project<'a>(project: &'a crate::Project)
	-> std::collections::HashSet<&'a foliage::PredicateDeclaration>
{
	let mut predicate_declarations = std::collections::HashSet::new();

	let formulas = project.blocks.iter()
		.filter_map(
			|block|
				match block
				{
					crate::project::Block::Whitespace(_) => None,
					crate::project::Block::Statement(ref statement) =>
						match statement.kind
						{
							crate::project::StatementKind::Axiom => Some(&statement.formula),
							_ => None,
						}
				});

	for formula in formulas
	{
		collect_predicate_declarations_in_formula(&mut predicate_declarations, formula);
	}

	predicate_declarations
}

fn collect_symbolic_constants_in_term<'a>(
	symbolic_constants: &mut std::collections::HashSet<&'a str>, term: &'a foliage::Term)
{
	match term
	{
		foliage::Term::Infimum => (),
		foliage::Term::Supremum => (),
		foliage::Term::Integer(_) => (),
		foliage::Term::Symbolic(ref name) =>
		{
			symbolic_constants.insert(name);
		},
		foliage::Term::String(_) => (),
		foliage::Term::Variable(_) => (),
		foliage::Term::Add(ref left, ref right) =>
		{
			collect_symbolic_constants_in_term(symbolic_constants, left);
			collect_symbolic_constants_in_term(symbolic_constants, right);
		},
		foliage::Term::Subtract(ref left, ref right) =>
		{
			collect_symbolic_constants_in_term(symbolic_constants, left);
			collect_symbolic_constants_in_term(symbolic_constants, right);
		},
		foliage::Term::Multiply(ref left, ref right) =>
		{
			collect_symbolic_constants_in_term(symbolic_constants, left);
			collect_symbolic_constants_in_term(symbolic_constants, right);
		},
		foliage::Term::Negative(ref argument) =>
		{
			collect_symbolic_constants_in_term(symbolic_constants, argument);
		},
	}
}

fn collect_symbolic_constants_in_formula<'a>(
	symbolic_constants: &mut std::collections::HashSet<&'a str>, formula: &'a foliage::Formula)
{
	match formula
	{
		foliage::Formula::Exists(ref exists) => collect_symbolic_constants_in_formula(symbolic_constants, &exists.argument),
		foliage::Formula::ForAll(ref for_all) => collect_symbolic_constants_in_formula(symbolic_constants, &for_all.argument),
		foliage::Formula::Not(ref argument) => collect_symbolic_constants_in_formula(symbolic_constants, argument),
		foliage::Formula::And(ref arguments) =>
			for argument in arguments
			{
				collect_symbolic_constants_in_formula(symbolic_constants, argument);
			},
		foliage::Formula::Or(ref arguments) =>
			for argument in arguments
			{
				collect_symbolic_constants_in_formula(symbolic_constants, argument);
			},
		foliage::Formula::Implies(ref left, ref right) =>
		{
			collect_symbolic_constants_in_formula(symbolic_constants, left);
			collect_symbolic_constants_in_formula(symbolic_constants, right);
		},
		foliage::Formula::Biconditional(ref left, ref right) =>
		{
			collect_symbolic_constants_in_formula(symbolic_constants, left);
			collect_symbolic_constants_in_formula(symbolic_constants, right);
		},
		foliage::Formula::Less(ref left, ref right) =>
		{
			collect_symbolic_constants_in_term(symbolic_constants, left);
			collect_symbolic_constants_in_term(symbolic_constants, right);
		},
		foliage::Formula::LessOrEqual(ref left, ref right) =>
		{
			collect_symbolic_constants_in_term(symbolic_constants, left);
			collect_symbolic_constants_in_term(symbolic_constants, right);
		},
		foliage::Formula::Greater(ref left, ref right) =>
		{
			collect_symbolic_constants_in_term(symbolic_constants, left);
			collect_symbolic_constants_in_term(symbolic_constants, right);
		},
		foliage::Formula::GreaterOrEqual(ref left, ref right) =>
		{
			collect_symbolic_constants_in_term(symbolic_constants, left);
			collect_symbolic_constants_in_term(symbolic_constants, right);
		},
		foliage::Formula::Equal(ref left, ref right) =>
		{
			collect_symbolic_constants_in_term(symbolic_constants, left);
			collect_symbolic_constants_in_term(symbolic_constants, right);
		},
		foliage::Formula::NotEqual(ref left, ref right) =>
		{
			collect_symbolic_constants_in_term(symbolic_constants, left);
			collect_symbolic_constants_in_term(symbolic_constants, right);
		},
		foliage::Formula::Boolean(_) => (),
		foliage::Formula::Predicate(ref predicate) =>
		{
			for argument in &predicate.arguments
			{
				collect_symbolic_constants_in_term(symbolic_constants, &argument);
			}
		},
	}
}

fn collect_symbolic_constants_in_project<'a>(project: &'a crate::Project)
	-> std::collections::HashSet<&'a str>
{
	let mut symbolic_constants = std::collections::HashSet::new();

	// TODO: avoid code duplication
	let formulas = project.blocks.iter()
		.filter_map(
			|block|
				match block
				{
					crate::project::Block::Whitespace(_) => None,
					crate::project::Block::Statement(ref statement) =>
						match statement.kind
						{
							crate::project::StatementKind::Axiom => Some(&statement.formula),
							_ => None,
						}
				});

	for formula in formulas
	{
		collect_symbolic_constants_in_formula(&mut symbolic_constants, formula);
	}

	symbolic_constants
}

struct VariableDeclarationDisplay<'a>(&'a foliage::VariableDeclaration);
struct PredicateDeclarationDisplay<'a>(&'a foliage::PredicateDeclaration);
struct TermDisplay<'a>(&'a foliage::Term);
struct FormulaDisplay<'a>(&'a foliage::Formula);
struct StatementKindDisplay<'a>(&'a crate::project::StatementKind);
pub struct ProjectDisplay<'a, 'input>
{
	project: &'a crate::project::Project<'input>,
	conjecture: &'a crate::project::Statement<'input>,
}

impl<'a> DisplayTPTP<'a, VariableDeclarationDisplay<'a>> for foliage::VariableDeclaration
{
	fn display_tptp(&'a self) -> VariableDeclarationDisplay<'a>
	{
		VariableDeclarationDisplay(self)
	}
}

impl<'a> DisplayTPTP<'a, PredicateDeclarationDisplay<'a>> for foliage::PredicateDeclaration
{
	fn display_tptp(&'a self) -> PredicateDeclarationDisplay<'a>
	{
		PredicateDeclarationDisplay(self)
	}
}

impl<'a> DisplayTPTP<'a, TermDisplay<'a>> for foliage::Term
{
	fn display_tptp(&'a self) -> TermDisplay<'a>
	{
		TermDisplay(self)
	}
}

impl<'a> DisplayTPTP<'a, FormulaDisplay<'a>> for foliage::Formula
{
	fn display_tptp(&'a self) -> FormulaDisplay<'a>
	{
		FormulaDisplay(self)
	}
}

impl<'a> DisplayTPTP<'a, StatementKindDisplay<'a>> for crate::project::StatementKind
{
	fn display_tptp(&'a self) -> StatementKindDisplay<'a>
	{
		StatementKindDisplay(self)
	}
}

pub fn display_project_with_conjecture_tptp<'a, 'input>(project: &'a crate::Project<'input>,
	conjecture: &'a crate::project::Statement<'input>) -> ProjectDisplay<'a, 'input>
{
	ProjectDisplay
	{
		project,
		conjecture,
	}
}

impl<'a> std::fmt::Debug for VariableDeclarationDisplay<'a>
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		match &self.0.domain
		{
			foliage::Domain::Program => write!(format, "X{}: object", self.0.name),
			foliage::Domain::Integer => write!(format, "N{}: $int", self.0.name),
		}
	}
}

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

impl<'a> std::fmt::Debug for PredicateDeclarationDisplay<'a>
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		write!(format, "{}: (", self.0.name)?;

		let mut separator = "";

		for _ in 0..self.0.arity
		{
			write!(format, "{}object", separator)?;
			separator = " * "
		}

		write!(format, ") > $o")
	}
}

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

impl<'a> std::fmt::Debug for TermDisplay<'a>
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		match self.0
		{
			foliage::Term::Infimum => write!(format, "c__infimum__"),
			foliage::Term::Supremum => write!(format, "c__supremum__"),
			foliage::Term::Integer(value) => write!(format, "{}", value),
			foliage::Term::Symbolic(ref value) => write!(format, "{}", value),
			foliage::Term::String(ref value) => write!(format, "\"{}\"", value),
			foliage::Term::Variable(ref declaration) => match declaration.domain
			{
				foliage::Domain::Program => write!(format, "X{}", declaration.name),
				foliage::Domain::Integer => write!(format, "N{}", declaration.name),
			},
			foliage::Term::Add(ref left, ref right) => write!(format, "$sum({:?}, {:?})", (&**left).display_tptp(), right.display_tptp()),
			foliage::Term::Subtract(ref left, ref right) => write!(format, "$difference({:?}, {:?})", left.display_tptp(), right.display_tptp()),
			foliage::Term::Multiply(ref left, ref right) => write!(format, "$product({:?}, {:?})", left.display_tptp(), right.display_tptp()),
			foliage::Term::Negative(ref argument) => write!(format, "$uminus({:?})", argument.display_tptp()),
		}
	}
}

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

impl<'a> std::fmt::Debug for FormulaDisplay<'a>
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		#[derive(Eq, PartialEq)]
		enum Notation
		{
			Prefix,
			Infix,
		}

		let mut display_comparison = |notation, operator_identifier: &str, operator_identifier_fallback, left, right| -> Result<(), std::fmt::Error>
		{
			write!(format, "(")?;

			let mut notation = notation;
			let mut operator_identifier = operator_identifier;

			let left_is_arithmetic_term = is_arithmetic_term(left);
			let right_is_arithmetic_term = is_arithmetic_term(right);

			if let Some(operator_identifier_fallback) = operator_identifier_fallback
			{
				if !left_is_arithmetic_term || !right_is_arithmetic_term
				{
					notation = Notation::Prefix;
					operator_identifier = operator_identifier_fallback;
				}
			}

			if notation == Notation::Prefix
			{
				write!(format, "{}(", operator_identifier)?;
			}

			if left_is_arithmetic_term && !right_is_arithmetic_term
			{
				write!(format, "f__integer__({})", left.display_tptp())?;
			}
			else
			{
				write!(format, "{}", left.display_tptp())?;
			}

			match notation
			{
				Notation::Prefix => write!(format, ", ")?,
				Notation::Infix => write!(format, " {} ", operator_identifier)?,
			}

			if right_is_arithmetic_term && !left_is_arithmetic_term
			{
				write!(format, "f__integer__({})", right.display_tptp())?;
			}
			else
			{
				write!(format, "{}", right.display_tptp())?;
			}

			if notation == Notation::Prefix
			{
				write!(format, ")")?;
			}

			write!(format, ")")
		};

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

				let mut separator = "";

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

					separator = ", "
				}

				write!(format, "]: ({:?})", exists.argument.display_tptp())
			},
			foliage::Formula::ForAll(ref for_all) =>
			{
				write!(format, "![")?;

				let mut separator = "";

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

					separator = ", "
				}

				write!(format, "]: ({:?})", for_all.argument.display_tptp())
			},
			foliage::Formula::Not(ref argument) => write!(format, "~({:?})", argument.display_tptp()),
			foliage::Formula::And(ref arguments) =>
			{
				write!(format, "(")?;

				let mut separator = "";

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

					separator = " & "
				}

				write!(format, ")")
			},
			foliage::Formula::Or(ref arguments) =>
			{
				write!(format, "(")?;

				let mut separator = "";

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

					separator = " | "
				}

				write!(format, ")")
			},
			foliage::Formula::Implies(ref left, ref right) => write!(format, "({:?} => {:?})", left.display_tptp(), right.display_tptp()),
			foliage::Formula::Biconditional(ref left, ref right) => write!(format, "({:?} <=> {:?})", left.display_tptp(), right.display_tptp()),
			foliage::Formula::Less(ref left, ref right) => display_comparison(Notation::Prefix, "$less", Some("p__less__"), left, right),
			foliage::Formula::LessOrEqual(ref left, ref right) => display_comparison(Notation::Prefix, "$lesseq", Some("p__less_equal__"), left, right),
			foliage::Formula::Greater(ref left, ref right) => display_comparison(Notation::Prefix, "$greater", Some("p__greater__"), left, right),
			foliage::Formula::GreaterOrEqual(ref left, ref right) => display_comparison(Notation::Prefix, "$greatereq", Some("p__greater_equal__"), left, right),
			foliage::Formula::Equal(ref left, ref right) => display_comparison(Notation::Infix, "=", None, left, right),
			foliage::Formula::NotEqual(ref left, ref right) => display_comparison(Notation::Infix, "!=", None, left, right),
			foliage::Formula::Boolean(value) =>
				match value
				{
					true => write!(format, "$true"),
					false => write!(format, "$false"),
				},
			foliage::Formula::Predicate(ref predicate) =>
			{
				write!(format, "{}", predicate.declaration.name)?;

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

					let mut separator = "";

					for argument in &predicate.arguments
					{
						let argument_is_arithmetic_term = is_arithmetic_term(argument);

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

						write!(format, "{}{:?}", separator, argument.display_tptp())?;

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

						separator = ", "
					}

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

				Ok(())
			},
		}
	}
}

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

impl<'a> std::fmt::Debug for StatementKindDisplay<'a>
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		match &self.0
		{
			crate::project::StatementKind::Axiom => write!(format, "axiom, axiom"),
			crate::project::StatementKind::Lemma => write!(format, "lemma, conjecture"),
			crate::project::StatementKind::Conjecture => write!(format, "conjecture, conjecture"),
		}
	}
}

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

impl<'a, 'input> std::fmt::Debug for ProjectDisplay<'a, 'input>
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		let write_title = |format: &mut std::fmt::Formatter, line_separator, title_identifier|
		{
			write!(format, "{}{}", line_separator, "%".repeat(80))?;
			write!(format, "\n% {}", title_identifier)?;
			write!(format, "\n{}", "%".repeat(80))
		};

		write_title(format, "", "anthem types")?;

		let tptp_preamble_anthem_types = include_str!("tptp_preamble_anthem_types.tptp").trim_end();
		write!(format, "\n{}", tptp_preamble_anthem_types)?;

		write_title(format, "\n\n", "anthem axioms")?;

		let tptp_preamble_anthem_axioms = include_str!("tptp_preamble_anthem_axioms.tptp").trim_end();
		write!(format, "\n{}", tptp_preamble_anthem_axioms)?;

		let predicate_declarations = collect_predicate_declarations_in_project(self.project);
		let symbolic_constants = collect_symbolic_constants_in_project(self.project);

		if !predicate_declarations.is_empty() || !symbolic_constants.is_empty()
		{
			write_title(format, "\n\n", "types")?;

			for predicate_declaration in predicate_declarations
			{
				write!(format, "\ntff(type, type, {:?}).", predicate_declaration.display_tptp())?;
			}

			for symbolic_constant in symbolic_constants
			{
				write!(format, "\ntff(type, type, {}: object).", symbolic_constant)?;
			}
		}

		let axioms = self.project.blocks.iter()
			.filter_map(
				|block|
				match block
				{
					crate::project::Block::Whitespace(_) => None,
					crate::project::Block::Statement(ref statement) =>
						match statement.kind
						{
							crate::project::StatementKind::Axiom => Some(statement),
							_ => None,
						}
				});

		for axiom in axioms
		{
			write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Axiom.display_tptp(), axiom.formula.display_tptp())?;
		}

		match self.conjecture.kind
		{
			crate::project::StatementKind::Lemma =>
			{
				write_title(format, "\n\n", "lemma")?;

				write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Lemma.display_tptp(), self.conjecture.formula.display_tptp())?;

				Ok(())
			},
			crate::project::StatementKind::Conjecture =>
			{
				write_title(format, "\n\n", "conjecture")?;

				write!(format, "\ntff({:?}, {:?}).", crate::project::StatementKind::Conjecture.display_tptp(), self.conjecture.formula.display_tptp())?;

				Ok(())
			},
			crate::project::StatementKind::Axiom => panic!("unexpected axiom"),
		}
	}
}

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