use nom::
{
	IResult,
	bytes::complete::{take_while, take_while1, take_while_m_n, is_not},
	character::is_alphanumeric,
	character::complete::{digit1, multispace0},
	sequence::{preceded, delimited, pair},
	combinator::{map, map_res},
	multi::{many0, separated_list},
	branch::alt,
	bytes::complete::tag,
};

#[derive(PartialEq)]
pub struct PredicateDeclaration
{
	name: String,
	arity: usize,
}

#[derive(PartialEq)]
pub struct Predicate
{
	declaration: PredicateDeclaration,
	arguments: Vec<Term>,
}

#[derive(PartialEq)]
pub struct Exists
{
	parameters: Vec<VariableDeclaration>,
	argument: Box<Formula>,
}

#[derive(PartialEq)]
pub struct ForAll
{
	parameters: Vec<VariableDeclaration>,
	argument: Box<Formula>,
}

#[derive(PartialEq)]
pub enum Formula
{
	Exists(Exists),
	ForAll(ForAll),
	Not(Box<Formula>),
	And(Vec<Box<Formula>>),
	Or(Vec<Box<Formula>>),
	Implies(Box<Formula>, Box<Formula>),
	Biconditional(Box<Formula>, Box<Formula>),
	Less(Term, Term),
	LessOrEqual(Term, Term),
	Greater(Term, Term),
	GreaterOrEqual(Term, Term),
	Equal(Term, Term),
	NotEqual(Term, Term),
	Boolean(bool),
	Predicate(Predicate),
}

#[derive(PartialEq)]
pub enum Domain
{
	Program,
	Integer,
}

#[derive(PartialEq)]
pub struct VariableDeclaration
{
	name: String,
	domain: Domain,
}

#[derive(PartialEq)]
pub enum Term
{
	Infimum,
	Supremum,
	Integer(i64),
	Symbolic(String),
	String(String),
	Variable(VariableDeclaration),
	Add(Box<Term>, Box<Term>),
	Subtract(Box<Term>, Box<Term>),
	Multiply(Box<Term>, Box<Term>),
	Negative(Box<Term>),
}

pub enum TermOperator
{
	Add,
	Subtract,
	Multiply,
}

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

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

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

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

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

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

impl std::fmt::Debug for Term
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		match *self
		{
			Term::Infimum => write!(format, "#inf"),
			Term::Supremum => write!(format, "#sup"),
			Term::Integer(value) => write!(format, "{}", value),
			Term::Symbolic(ref value) => write!(format, "{}", value),
			Term::String(ref value) => write!(format, "\"{}\"", value),
			Term::Variable(ref declaration) => write!(format, "{:?}", declaration),
			Term::Add(ref left, ref right) => write!(format, "({:?} + {:?})", left, right),
			Term::Subtract(ref left, ref right) => write!(format, "({:?} - {:?})", left, right),
			Term::Multiply(ref left, ref right) => write!(format, "({:?} * {:?})", left, right),
			Term::Negative(ref argument) => write!(format, "-({:?})", argument),
		}
	}
}

impl std::fmt::Display for Term
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		match *self
		{
			Term::Infimum => write!(format, "#inf"),
			Term::Supremum => write!(format, "#sup"),
			Term::Integer(value) => write!(format, "{}", value),
			Term::Symbolic(ref value) => write!(format, "{}", value),
			Term::String(ref value) => write!(format, "\"{}\"", value),
			Term::Variable(ref declaration) => write!(format, "{}", declaration),
			Term::Add(ref left, ref right) => write!(format, "({} + {})", left, right),
			Term::Subtract(ref left, ref right) => write!(format, "({} - {})", left, right),
			Term::Multiply(ref left, ref right) => write!(format, "({} * {})", left, right),
			Term::Negative(ref argument) => write!(format, "-({})", argument),
		}
	}
}

impl std::fmt::Debug for Formula
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		match *self
		{
			Formula::Exists(ref exists) =>
			{
				write!(format, "exists")?;

				let mut separator = " ";

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

					separator = ", "
				}

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

				let mut separator = " ";

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

					separator = ", "
				}

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

				let mut separator = "";

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

					separator = " and "
				}

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

				let mut separator = "";

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

					separator = " or "
				}

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

						separator = ", "
					}

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

				Ok(())
			},
		}
	}
}

impl std::fmt::Display for Formula
{
	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
	{
		match *self
		{
			Formula::Exists(ref exists) =>
			{
				write!(format, "exists")?;

				let mut separator = " ";

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

					separator = ", "
				}

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

				let mut separator = " ";

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

					separator = ", "
				}

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

				let mut separator = "";

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

					separator = " and "
				}

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

				let mut separator = "";

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

					separator = " or "
				}

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

						separator = ", "
					}

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

				Ok(())
			},
		}
	}
}

fn infimum(i: &str) -> IResult<&str, Term>
{
	map
	(
		delimited(multispace0, tag("#inf"), multispace0),
		|_| Term::Infimum
	)(i)
}

fn supremum(i: &str) -> IResult<&str, Term>
{
	map
	(
		delimited(multispace0, tag("#sup"), multispace0),
		|_| Term::Supremum
	)(i)
}

fn integer(i: &str) -> IResult<&str, Term>
{
	map
	(
		map_res
		(
			delimited(multispace0, digit1, multispace0),
			std::str::FromStr::from_str
		),
		Term::Integer
	)(i)
}

fn is_lowercase_alphanumeric(c: char) -> bool
{
	c.is_alphanumeric() && c.is_lowercase()
}

fn symbolic_identifier(i: &str) -> IResult<&str, String>
{
	map
	(
		pair
		(
			take_while_m_n(1, 1, is_lowercase_alphanumeric),
			take_while(char::is_alphanumeric)
		),
		|(s0, s1)| format!("{}{}", s0, s1)
	)(i)
}

fn symbolic(i: &str) -> IResult<&str, Term>
{
	map
	(
		delimited(multispace0, symbolic_identifier, multispace0),
		Term::Symbolic
	)(i)
}

fn string(i: &str) -> IResult<&str, Term>
{
	map
	(
		delimited
		(
			multispace0,
			delimited
			(
				tag("\""),
				is_not("\""),
				tag("\""),
			),
			multispace0
		),
		|s: &str| Term::String(s.to_string())
	)(i)
}

fn program_variable_identifier(i: &str) -> IResult<&str, String>
{
	map
	(
		delimited
		(
			multispace0,
			preceded
			(
				tag("X"),
				take_while1(char::is_alphanumeric)
			),
			multispace0
		),
		|s: &str| s.to_string()
	)(i)
}

fn integer_variable_identifier(i: &str) -> IResult<&str, String>
{
	map
	(
		delimited
		(
			multispace0,
			preceded
			(
				tag("N"),
				take_while1(char::is_alphanumeric)
			),
			multispace0
		),
		|s: &str| s.to_string()
	)(i)
}

fn program_variable_declaration(i: &str) -> IResult<&str, VariableDeclaration>
{
	map
	(
		program_variable_identifier,
		|s| VariableDeclaration{name: s, domain: Domain::Program}
	)(i)
}

fn integer_variable_declaration(i: &str) -> IResult<&str, VariableDeclaration>
{
	map
	(
		integer_variable_identifier,
		|s| VariableDeclaration{name: s, domain: Domain::Integer}
	)(i)
}

fn variable_declaration(i: &str) -> IResult<&str, VariableDeclaration>
{
	alt
	((
		program_variable_declaration,
		integer_variable_declaration
	))(i)
}

fn program_variable(i: &str) -> IResult<&str, Term>
{
	map
	(
		program_variable_identifier,
		|s| Term::Variable(VariableDeclaration{name: s, domain: Domain::Program})
	)(i)
}

fn integer_variable(i: &str) -> IResult<&str, Term>
{
	map
	(
		integer_variable_identifier,
		|s| Term::Variable(VariableDeclaration{name: s, domain: Domain::Integer})
	)(i)
}

fn variable(i: &str) -> IResult<&str, Term>
{
	alt
	((
		program_variable,
		integer_variable
	))(i)
}

fn predicate_0_ary(i: &str) -> IResult<&str, Formula>
{
	map
	(
		delimited(multispace0, symbolic_identifier, multispace0),
		|name| Formula::Predicate(
			Predicate
			{
				declaration:
					PredicateDeclaration
					{
						name: name,
						arity: 0,
					},
				arguments: vec![],
			})
	)(i)
}

fn predicate_n_ary(i: &str) -> IResult<&str, Formula>
{
	map
	(
		pair
		(
			delimited(multispace0, symbolic_identifier, multispace0),
			delimited
			(
				tag("("),
				separated_list(tag(","), term),
				tag(")")
			)
		),
		|(name, arguments)| Formula::Predicate(
				Predicate
				{
					declaration:
						PredicateDeclaration
						{
							name: name,
							arity: arguments.len(),
						},
					arguments: arguments,
				})
	)(i)
}

fn predicate(i: &str) -> IResult<&str, Formula>
{
	alt
	((
		predicate_n_ary,
		predicate_0_ary
	))(i)
}

fn boolean(i: &str) -> IResult<&str, Formula>
{
	map
	(
		delimited
		(
			multispace0,
			alt
			((
				map(tag("#true"), |_| true),
				map(tag("#false"), |_| false)
			)),
			multispace0
		),
		|value| Formula::Boolean(value)
	)(i)
}






fn term_parenthesized(i: &str) -> IResult<&str, Term>
{
	delimited
	(
		multispace0,
		delimited
		(
			tag("("),
			term,
			tag(")")
		),
		multispace0
	)(i)
}

fn fold_terms(initial: Term, remainder: Vec<(TermOperator, Term)>) -> Term
{
	remainder.into_iter().fold(initial,
		|accumulator, pair|
		{
			let (term_operator, term) = pair;

			match term_operator
			{
				TermOperator::Add => Term::Add(Box::new(accumulator), Box::new(term)),
				TermOperator::Subtract => Term::Subtract(Box::new(accumulator), Box::new(term)),
				TermOperator::Multiply => Term::Multiply(Box::new(accumulator), Box::new(term)),
			}
		})
}

fn term_precedence_0(i: &str) -> IResult<&str, Term>
{
	alt
	((
		infimum,
		supremum,
		integer,
		symbolic,
		string,
		variable,
		term_parenthesized
	))(i)
}

fn term_precedence_1(i: &str) -> IResult<&str, Term>
{
	alt
	((
		map
		(
			delimited
			(
				multispace0,
				preceded(tag("-"), term_precedence_0),
				multispace0
			),
			|term| Term::Negative(Box::new(term))
		),
		term_precedence_0
	))(i)
}

fn term_precedence_2(i: &str) -> IResult<&str, Term>
{
	let (i, initial) = term_precedence_1(i)?;
	let (i, remainder) =
		many0
		(
			|i|
			{
				let (i, term) = preceded(tag("*"), term_precedence_1)(i)?;
				Ok((i, (TermOperator::Multiply, term)))
			}
		)(i)?;

	Ok((i, fold_terms(initial, remainder)))
}

fn term_precedence_3(i: &str) -> IResult<&str, Term>
{
	let (i, initial) = term_precedence_2(i)?;
	let (i, remainder) =
		many0
		(
			alt
			((
				|i|
				{
					let (i, term) = preceded(tag("+"), term_precedence_2)(i)?;
					Ok((i, (TermOperator::Add, term)))
				},
				|i|
				{
					let (i, term) = preceded(tag("-"), term_precedence_2)(i)?;
					Ok((i, (TermOperator::Subtract, term)))
				}
			))
		)(i)?;

	Ok((i, fold_terms(initial, remainder)))
}

fn term(i: &str) -> IResult<&str, Term>
{
	term_precedence_3(i)
}

#[cfg(test)]
mod tests
{
	#[test]
	fn parse_integer()
	{
		assert_eq!(crate::integer("12345"), Ok(("", crate::Term::Integer(12345))));
	}

	#[test]
	fn parse_variable_declaration()
	{
		assert_eq!(crate::variable_declaration("X5"), Ok(("", crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()})));
		assert_eq!(crate::variable_declaration("NX3"), Ok(("", crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()})));
	}

	#[test]
	fn parse_variable()
	{
		assert_eq!(crate::variable("X5"), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "5".to_string()}))));
		assert_eq!(crate::variable("NX3"), Ok(("", crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Integer, name: "X3".to_string()}))));
	}

	#[test]
	fn parse_string()
	{
		assert_eq!(crate::string(" \"foobar\" "), Ok(("", crate::Term::String("foobar".to_string()))));
	}

	#[test]
	fn parse_boolean()
	{
		assert_eq!(crate::boolean(" #true "), Ok(("", crate::Formula::Boolean(true))));
		assert_eq!(crate::boolean(" #false "), Ok(("", crate::Formula::Boolean(false))));
	}

	#[test]
	fn parse_term()
	{
		assert_eq!(crate::term(" 5 + 3"), Ok(("",
			crate::Term::Add
			(
				Box::new(crate::Term::Integer(5)),
				Box::new(crate::Term::Integer(3)),
			))));

		assert_eq!(crate::term(" -5"), Ok(("",
				crate::Term::Negative
				(
					Box::new(crate::Term::Integer(5))
				)
			)));

		assert_eq!(crate::term(" 5+3 * -(9+ 1)  + 2 "), Ok(("",
			crate::Term::Add
			(
				Box::new(crate::Term::Add
				(
					Box::new(crate::Term::Integer(5)),
					Box::new(crate::Term::Multiply
					(
						Box::new(crate::Term::Integer(3)),
						Box::new(crate::Term::Negative
						(
							Box::new(crate::Term::Add
							(
								Box::new(crate::Term::Integer(9)),
								Box::new(crate::Term::Integer(1)),
							))
						)),
					)),
				)),
				Box::new(crate::Term::Integer(2)),
			))));

		assert_eq!(crate::term(" 5 + a "), Ok(("",
			crate::Term::Add
			(
				Box::new(crate::Term::Integer(5)),
				Box::new(crate::Term::Symbolic("a".to_string())),
			))));

		assert_eq!(crate::term(" 5 + #sup "), Ok(("",
			crate::Term::Add
			(
				Box::new(crate::Term::Integer(5)),
				Box::new(crate::Term::Supremum),
			))));

		assert_eq!(crate::term(" 5 + #inf "), Ok(("",
			crate::Term::Add
			(
				Box::new(crate::Term::Integer(5)),
				Box::new(crate::Term::Infimum),
			))));

		assert_eq!(crate::term(" 5 + \" text \" "), Ok(("",
			crate::Term::Add
			(
				Box::new(crate::Term::Integer(5)),
				Box::new(crate::Term::String(" text ".to_string())),
			))));

		assert_eq!(crate::term(" 5 + X1 "), Ok(("",
			crate::Term::Add
			(
				Box::new(crate::Term::Integer(5)),
				Box::new(crate::Term::Variable(crate::VariableDeclaration{domain: crate::Domain::Program, name: "1".to_string()})),
			))));
	}

	#[test]
	fn parse_predicate()
	{
		assert_eq!(crate::predicate("p"), Ok(("", crate::Formula::Predicate(crate::Predicate{declaration: crate::PredicateDeclaration{name: "p".to_string(), arity: 0}, arguments: vec![]}))));

		assert_eq!(crate::predicate_n_ary("p(5, 6, 7)"), Ok(("",
			crate::Formula::Predicate
			(
				crate::Predicate
				{
					declaration:
						crate::PredicateDeclaration
						{
							name: "p".to_string(),
							arity: 3,
						},
					arguments:
						vec!
						[
							crate::Term::Integer(5),
							crate::Term::Integer(6),
							crate::Term::Integer(7),
						]
				}
			))));

		assert_eq!(crate::predicate("p(1, 3+4*5+6, \"test\")"), Ok(("",
			crate::Formula::Predicate
			(
				crate::Predicate
				{
					declaration:
						crate::PredicateDeclaration
						{
							name: "p".to_string(),
							arity: 3,
						},
					arguments:
						vec!
						[
							crate::Term::Integer(1),
							crate::Term::Add
							(
								Box::new(crate::Term::Add
								(
									Box::new(crate::Term::Integer(3)),
									Box::new(crate::Term::Multiply
									(
										Box::new(crate::Term::Integer(4)),
										Box::new(crate::Term::Integer(5)),
									)),
								)),
								Box::new(crate::Term::Integer(6)),
							),
							crate::Term::String("test".to_string()),
						]
				}
			))));
	}
}