use nom::
{
	IResult,
	branch::alt,
	bytes::complete::tag,
	character::complete::multispace0,
	combinator::{cut, map, map_res},
	multi::{many1, separated_list},
	sequence::{delimited, pair, preceded, terminated, tuple},
};

use super::{Declarations, boolean, word_boundary};

pub fn predicate<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Predicate>
{
	map
	(
		|i| crate::parse::terms::function_or_predicate(i, d),
		|(name, arguments)|
		{
			let arguments = match arguments
			{
				Some(arguments) => arguments,
				None => vec![],
			};

			let mut predicate_declarations = d.predicate_declarations.borrow_mut();

			let declaration = match predicate_declarations.iter()
				.find(|x| x.name == name && x.arity == arguments.len())
			{
				Some(declaration) => std::rc::Rc::clone(&declaration),
				None =>
				{
					let declaration = crate::PredicateDeclaration
					{
						name: name.to_string(),
						arity: arguments.len(),
					};
					let declaration = std::rc::Rc::new(declaration);

					predicate_declarations.insert(std::rc::Rc::clone(&declaration));

					declaration
				},
			};

			crate::Predicate::new(declaration, arguments)
		},
	)(i)
}

fn not<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
{
	map
	(
		preceded
		(
			terminated
			(
				tag("not"),
				multispace0,
			),
			|i| formula_precedence_2(i, d),
		),
		|x| crate::Formula::not(Box::new(x)),
	)(i)
}

fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
{
	map_res
	(
		separated_list
		(
			delimited
			(
				multispace0,
				terminated
				(
					tag("and"),
					word_boundary,
				),
				multispace0,
			),
			|i| formula_precedence_2(i, d),
		),
		|arguments| -> Result<_, (_, _)>
		{
			if arguments.len() >= 2
			{
				Ok(arguments.into_iter().map(Box::new).collect())
			}
			else
			{
				Err(nom::error::make_error(i, nom::error::ErrorKind::Many1))
			}
		}
	)(i)
}

fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
{
	map_res
	(
		separated_list
		(
			delimited
			(
				multispace0,
				terminated
				(
					tag("or"),
					word_boundary,
				),
				multispace0,
			),
			|i| formula_precedence_3(i, d),
		),
		|arguments| -> Result<_, (_, _)>
		{
			if arguments.len() >= 2
			{
				Ok(arguments.into_iter().map(Box::new).collect())
			}
			else
			{
				Err(nom::error::make_error(i, nom::error::ErrorKind::Many1))
			}
		}
	)(i)
}

fn implication_left_to_right<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
{
	map
	(
		pair
		(
			many1
			(
				terminated
				(
					|i| formula_precedence_4(i, d),
					delimited
					(
						multispace0,
						tag("->"),
						multispace0,
					),
				)
			),
			|i| formula_precedence_4(i, d),
		),
		|(arguments, last_argument)| arguments.into_iter().rev().fold(last_argument,
			|accumulator, argument|
				crate::Formula::implies(crate::ImplicationDirection::LeftToRight,
					Box::new(accumulator), Box::new(argument)))
	)(i)
}

fn implication_right_to_left<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
{
	map
	(
		pair
		(
			|i| formula_precedence_4(i, d),
			many1
			(
				preceded
				(
					delimited
					(
						multispace0,
						tag("<-"),
						multispace0,
					),
					|i| formula_precedence_4(i, d),
				)
			),
		),
		|(first_argument, arguments)| arguments.into_iter().fold(first_argument,
			|accumulator, argument|
				crate::Formula::implies(crate::ImplicationDirection::RightToLeft,
					Box::new(accumulator), Box::new(argument)))
	)(i)
}

fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
{
	map_res
	(
		separated_list
		(
			delimited
			(
				multispace0,
				tag("<->"),
				multispace0,
			),
			|i| formula_precedence_5(i, d),
		),
		|arguments| -> Result<_, (_, _)>
		{
			if arguments.len() >= 2
			{
				Ok(arguments.into_iter().map(Box::new).collect())
			}
			else
			{
				Err(nom::error::make_error(i, nom::error::ErrorKind::Many1))
			}
		}
	)(i)
}

fn quantified_expression<'a, 'b, T, N>(i: &'a str, d: &Declarations, keyword: &'b str,
	new_functor: N)
	-> IResult<&'a str, T>
where
	N: Fn(std::rc::Rc<crate::VariableDeclarations>, Box<crate::Formula>) -> T
{
	preceded
	(
		terminated
		(
			tag(keyword),
			word_boundary,
		),
		cut
		(
			|i| -> IResult<&'a str, T>
			{
				let (i, variable_declarations) =
					map
					(
						delimited
						(
							multispace0,
							separated_list
							(
								delimited
								(
									multispace0,
									tag(","),
									multispace0,
								),
								map
								(
									crate::parse::terms::variable_declaration,
									std::rc::Rc::new,
								),
							),
							multispace0,
						),
						std::rc::Rc::new,
					)(i)?;

				if variable_declarations.is_empty()
				{
					return Err(nom::Err::Failure((i, nom::error::ErrorKind::Many1)));
				}

				d.variable_declaration_stack.borrow_mut().push(std::rc::Rc::clone(&variable_declarations));

				let (i, argument) = formula_parenthesized(i, d)?;

				// TODO: report logic errors more appropriately
				d.variable_declaration_stack.borrow_mut().pop()
					.map_err(|_| nom::Err::Failure((i, nom::error::ErrorKind::Verify)))?;

				Ok((i, new_functor(variable_declarations, Box::new(argument))))
			}
		),
	)(i)
}

fn compare<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Compare>
{
	map
	(
		tuple
		((
			|i| crate::parse::term(i, d),
			delimited
			(
				multispace0,
				alt
				((
					map
					(
						tag(">"),
						|_| crate::ComparisonOperator::Greater,
					),
					map
					(
						tag("<"),
						|_| crate::ComparisonOperator::Less,
					),
					map
					(
						tag("<="),
						|_| crate::ComparisonOperator::LessOrEqual,
					),
					map
					(
						tag(">="),
						|_| crate::ComparisonOperator::GreaterOrEqual,
					),
					map
					(
						tag("!="),
						|_| crate::ComparisonOperator::NotEqual,
					),
					map
					(
						tag("="),
						|_| crate::ComparisonOperator::Equal,
					),
				)),
				multispace0,
			),
			|i| crate::parse::term(i, d),
		)),
		|(left, operator, right)|
		{
			crate::Compare::new(operator, Box::new(left), Box::new(right))
		}
	)(i)
}

fn exists<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Exists>
{
	quantified_expression::<crate::Exists, _>(i, d, "exists", crate::Exists::new)
}

fn for_all<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::ForAll>
{
	quantified_expression::<crate::ForAll, _>(i, d, "forall", crate::ForAll::new)
}

fn formula_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
{
	delimited
	(
		terminated
		(
			tag("("),
			multispace0,
		),
		|i| formula(i, d),
		preceded
		(
			multispace0,
			tag(")"),
		),
	)(i)
}

fn formula_precedence_0<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
{
	alt
	((
		map
		(
			boolean,
			crate::Formula::Boolean,
		),
		map
		(
			|i| predicate(i, d),
			crate::Formula::Predicate,
		),
		map
		(
			|i| compare(i, d),
			crate::Formula::Compare,
		),
		|i| formula_parenthesized(i, d),
	))(i)
}

fn formula_precedence_1<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
{
	alt
	((
		map
		(
			|i| exists(i, d),
			crate::Formula::Exists,
		),
		map
		(
			|i| for_all(i, d),
			crate::Formula::ForAll,
		),
		|i| formula_precedence_0(i, d),
	))(i)
}

fn formula_precedence_2<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
{
	alt
	((
		|i| not(i, d),
		|i| formula_precedence_1(i, d),
	))(i)
}

fn formula_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
{
	alt
	((
		map
		(
			|i| and(i, d),
			crate::Formula::And,
		),
		|i| formula_precedence_2(i, d),
	))(i)
}

fn formula_precedence_4<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
{
	alt
	((
		map
		(
			|i| or(i, d),
			crate::Formula::Or,
		),
		|i| formula_precedence_3(i, d),
	))(i)
}

fn formula_precedence_5<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
{
	alt
	((
		|i| implication_left_to_right(i, d),
		|i| implication_right_to_left(i, d),
		|i| formula_precedence_4(i, d),
	))(i)
}

fn formula_precedence_6<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
{
	alt
	((
		map
		(
			|i| if_and_only_if(i, d),
			crate::Formula::IfAndOnlyIf,
		),
		|i| formula_precedence_5(i, d),
	))(i)
}

pub fn formula<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
{
	formula_precedence_6(i, d)
}

#[cfg(test)]
mod tests
{
	use crate::parse::formulas::*;
	use crate::{Formula, Term};

	/*fn formula(i: &str) -> Formula
	{
		crate::parse::formula(i, &Declarations::new()).unwrap().1
	}

	fn format_formula(i: &str) -> String
	{
		format!("{}", formula(i))
	}

	#[test]
	fn parse_formula_boolean()
	{
		assert_eq!(formula("true"), Formula::true_());
		assert_eq!(formula("false"), Formula::false_());
	}*/

	#[test]
	fn parse_predicate()
	{
		assert_eq!(predicate("s", &Declarations::new())
			.map(|(i, x)| (i, x.declaration.name.clone())),
			Ok(("", "s".to_string())));
		assert_eq!(predicate("s", &Declarations::new())
			.map(|(i, x)| (i, x.declaration.arity)),
			Ok(("", 0)));
		assert_eq!(predicate("s ( )", &Declarations::new())
			.map(|(i, x)| (i, x.declaration.name.clone())),
			Ok(("", "s".to_string())));
		assert_eq!(predicate("s ( )", &Declarations::new())
			.map(|(i, x)| (i, x.declaration.arity)),
			Ok(("", 0)));
		assert_eq!(predicate("s ( 1 , 2 , 3 )", &Declarations::new())
			.map(|(i, x)| (i, x.declaration.name.clone())),
			Ok(("", "s".to_string())));
		assert_eq!(predicate("s ( 1 , 2 , 3 )", &Declarations::new())
			.map(|(i, x)| (i, x.declaration.arity)),
			Ok(("", 3)));
		assert_eq!(predicate("s ( 1 , 2 , 3 )", &Declarations::new())
			.map(|(i, mut x)| (i, x.arguments.remove(0))),
			Ok(("", Box::new(Term::integer(1)))));
		assert_eq!(predicate("s ( 1 , 2 , 3 )", &Declarations::new())
			.map(|(i, mut x)| (i, x.arguments.remove(2))),
			Ok(("", Box::new(Term::integer(3)))));
		assert_eq!(predicate("s ( ), rest", &Declarations::new())
			.map(|(i, x)| (i, x.declaration.name.clone())),
			Ok((", rest", "s".to_string())));
		assert_eq!(predicate("s ( ), rest", &Declarations::new())
			.map(|(i, x)| (i, x.declaration.arity)),
			Ok((", rest", 0)));
		assert_eq!(predicate("s ( 1 , 2 , 3 ), rest", &Declarations::new())
			.map(|(i, x)| (i, x.declaration.name.clone())),
			Ok((", rest", "s".to_string())));
		assert_eq!(predicate("s ( 1 , 2 , 3 ), rest", &Declarations::new())
			.map(|(i, x)| (i, x.declaration.arity)),
			Ok((", rest", 3)));
	}

	#[test]
	fn parse_exists()
	{
		assert_eq!(exists("exists X (p(X, Y, X, Y)), rest", &Declarations::new())
			.map(|(i, x)| (i, x.parameters.len())),
			Ok((", rest", 1)));
		assert!(exists("exists (p(X, Y, X, Y)), rest", &Declarations::new()).is_err());
		assert!(exists("exists X, rest", &Declarations::new()).is_err());
		assert!(exists("exists X (), rest", &Declarations::new()).is_err());
		assert!(exists("exists X (, true), rest", &Declarations::new()).is_err());
		assert!(exists("exists X (true, ), rest", &Declarations::new()).is_err());
		assert!(exists("exists X (true false), rest", &Declarations::new()).is_err());
		assert!(exists("exists X (true), rest", &Declarations::new()).is_ok());
		assert!(exists("exists X p(X), rest", &Declarations::new()).is_err());
	}

	#[test]
	fn parse_formula()
	{
		assert!(formula("exists X, Y (p(X, Y, X, Y) and X < Y and q(X) <-> r(X)), rest", &Declarations::new()).is_ok());
	}
}