use nom::
{
	IResult,
	branch::alt,
	bytes::complete::{escaped_transform, tag},
	character::complete::{digit1, multispace0, none_of},
	combinator::{map, map_res, opt, recognize},
	multi::separated_list,
	sequence::{delimited, pair, preceded, terminated},
};

use super::{Declarations, function_or_predicate_name, word_boundary, variable_name};

fn true_(i: &str) -> IResult<&str, crate::Term>
{
	map
	(
		terminated
		(
			tag("true"),
			word_boundary,
		),
		|_| crate::Term::true_(),
	)(i)
}

fn false_(i: &str) -> IResult<&str, crate::Term>
{
	map
	(
		terminated
		(
			tag("false"),
			word_boundary,
		),
		|_| crate::Term::false_(),
	)(i)
}

pub fn boolean(i: &str) -> IResult<&str, crate::Term>
{
	alt
	((
		true_,
		false_,
	))(i)
}

pub fn integer(i: &str) -> IResult<&str, crate::Term>
{
	map
	(
		map_res
		(
			recognize
			(
				terminated
				(
					pair
					(
						opt
						(
							alt
							((
								tag("-"),
								tag("+"),
							))
						),
						digit1,
					),
					word_boundary,
				)
			),
			std::str::FromStr::from_str,
		),
		crate::Term::integer,
	)(i)
}

fn infimum(i: &str) -> IResult<&str, crate::Term>
{
	map
	(
		terminated
		(
			tag("#inf"),
			word_boundary,
		),
		|_| crate::Term::infimum(),
	)(i)
}

fn supremum(i: &str) -> IResult<&str, crate::Term>
{
	map
	(
		terminated
		(
			tag("#sup"),
			word_boundary,
		),
		|_| crate::Term::supremum(),
	)(i)
}

pub fn special_integer(i: &str) -> IResult<&str, crate::Term>
{
	alt
	((
		infimum,
		supremum,
	))(i)
}

pub fn string(i: &str) -> IResult<&str, crate::Term>
{
	map
	(
		terminated
		(
			delimited
			(
				tag("\""),
				escaped_transform
				(
					none_of("\"\\"),
					'\\',
					alt
					((
						tag("\""),
						tag("\\"),
						map
						(
							tag("n"),
							|_| "\n",
						),
						map
						(
							tag("t"),
							|_| "\t",
						),
					)),
				),
				tag("\""),
			),
			word_boundary,
		),
		crate::Term::string,
	)(i)
}

fn function_or_predicate<'i>(i: &'i str, declarations: &Declarations)
	-> IResult<&'i str, (&'i str, Option<Vec<Box<crate::Term>>>)>
{
	pair
	(
		function_or_predicate_name,
		opt
		(
			delimited
			(
				delimited
				(
					multispace0,
					tag("("),
					multispace0,
				),
				separated_list
				(
					delimited
					(
						multispace0,
						tag(","),
						multispace0,
					),
					// TODO: fix
					map
					(
						integer,
						Box::new,
					),
				),
				preceded
				(
					multispace0,
					tag(")"),
				),
			)
		),
	)(i)
}

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

			let mut function_declarations = declarations.function_declarations.borrow_mut();

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

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

					declaration
				},
			};

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

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

			let mut predicate_declarations = declarations.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)
}

pub fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
{
	map
	(
		variable_name,
		|name| crate::VariableDeclaration::new(name.to_string())
	)(i)
}

pub fn variable<'i>(i: &'i str, declarations: &Declarations) -> IResult<&'i str, crate::Variable>
{
	map
	(
		variable_name,
		|name|
		{
			let mut variable_declaration_stack =
				declarations.variable_declaration_stack.borrow_mut();

			let declaration = variable_declaration_stack.find_or_create(name);

			crate::Variable::new(declaration)
		},
	)(i)
}

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

	#[test]
	fn parse_boolean()
	{
		assert_eq!(boolean("true"), Ok(("", Term::true_())));
		assert_eq!(boolean("false"), Ok(("", Term::false_())));
		assert_eq!(boolean("true false"), Ok((" false", Term::true_())));
		assert_eq!(boolean("false true"), Ok((" true", Term::false_())));
		assert_eq!(boolean("true,"), Ok((",", Term::true_())));
		assert_eq!(boolean("false,"), Ok((",", Term::false_())));
		assert!(boolean("truefalse").is_err());
		assert!(boolean("falsetrue").is_err());
		assert!(boolean("truea").is_err());
		assert!(boolean("falsea").is_err());
		assert!(boolean("a").is_err());
		assert!(boolean("-").is_err());
		assert!(boolean(" ").is_err());
	}

	#[test]
	fn parse_integer()
	{
		assert_eq!(integer("0"), Ok(("", Term::integer(0))));
		assert_eq!(integer("10000"), Ok(("", Term::integer(10000))));
		assert_eq!(integer("+10000"), Ok(("", Term::integer(10000))));
		assert_eq!(integer("-10000"), Ok(("", Term::integer(-10000))));
		assert_eq!(integer("0 42"), Ok((" 42", Term::integer(0))));
		assert_eq!(integer("10000 42"), Ok((" 42", Term::integer(10000))));
		assert_eq!(integer("+10000 42"), Ok((" 42", Term::integer(10000))));
		assert_eq!(integer("-10000 42"), Ok((" 42", Term::integer(-10000))));
		assert_eq!(integer("10000,"), Ok((",", Term::integer(10000))));
		assert_eq!(integer("+10000,"), Ok((",", Term::integer(10000))));
		assert_eq!(integer("-10000,"), Ok((",", Term::integer(-10000))));
		assert!(integer("10000a").is_err());
		assert!(integer("+10000a").is_err());
		assert!(integer("-10000a").is_err());
		assert!(integer("1.5").is_err());
		assert!(integer("a").is_err());
		assert!(integer("-").is_err());
		assert!(integer(" ").is_err());
	}

	#[test]
	fn parse_special_integer()
	{
		assert_eq!(special_integer("#inf"), Ok(("", Term::infimum())));
		assert_eq!(special_integer("#sup"), Ok(("", Term::supremum())));
		assert_eq!(special_integer("#inf #sup"), Ok((" #sup", Term::infimum())));
		assert_eq!(special_integer("#sup #inf"), Ok((" #inf", Term::supremum())));
		assert_eq!(special_integer("#inf,"), Ok((",", Term::infimum())));
		assert_eq!(special_integer("#sup,"), Ok((",", Term::supremum())));
		assert!(special_integer("#inf0").is_err());
		assert!(special_integer("#sup0").is_err());
		assert!(special_integer("#infimum").is_err());
		assert!(special_integer("#supremum").is_err());
		assert!(special_integer("inf").is_err());
		assert!(special_integer("sup").is_err());
		assert!(special_integer("0").is_err());
		assert!(special_integer("10000").is_err());
		assert!(special_integer("-10000").is_err());
		assert!(special_integer("-").is_err());
		assert!(special_integer("+").is_err());
		assert!(special_integer("a").is_err());
		assert!(special_integer(" ").is_err());
	}

	#[test]
	fn parse_string()
	{
		assert_eq!(string("\"test 123\""), Ok(("", Term::string("test 123".to_string()))));
		assert_eq!(string("\"123 test\""), Ok(("", Term::string("123 test".to_string()))));
		assert_eq!(string("\" test 123 \""), Ok(("", Term::string(" test 123 ".to_string()))));
		assert_eq!(string("\"test 123\" \"rest"), Ok((" \"rest", Term::string("test 123".to_string()))));
		assert_eq!(string("\"test 123\", \"rest"), Ok((", \"rest", Term::string("test 123".to_string()))));
		assert_eq!(string("\"test\n123\""), Ok(("", Term::string("test\n123".to_string()))));
		assert_eq!(string("\"test\\\"123\""), Ok(("", Term::string("test\"123".to_string()))));
		assert_eq!(string("\"test\\\"123\\\"\""), Ok(("", Term::string("test\"123\"".to_string()))));
		assert_eq!(string("\"\\\"test 123\\\"\""), Ok(("", Term::string("\"test 123\"".to_string()))));
		assert_eq!(string("\"test\\\\123\""), Ok(("", Term::string("test\\123".to_string()))));
		assert_eq!(string("\"test\\\\123\\\\\""), Ok(("", Term::string("test\\123\\".to_string()))));
		assert_eq!(string("\"\\\\test 123\\\\\""), Ok(("", Term::string("\\test 123\\".to_string()))));
		assert_eq!(string("\"test\\n123\""), Ok(("", Term::string("test\n123".to_string()))));
		assert_eq!(string("\"test\\n123\\n\""), Ok(("", Term::string("test\n123\n".to_string()))));
		assert_eq!(string("\"\\ntest 123\\n\""), Ok(("", Term::string("\ntest 123\n".to_string()))));
		assert_eq!(string("\"test\\t123\""), Ok(("", Term::string("test\t123".to_string()))));
		assert_eq!(string("\"test\\t123\\t\""), Ok(("", Term::string("test\t123\t".to_string()))));
		assert_eq!(string("\"\\ttest 123\\t\""), Ok(("", Term::string("\ttest 123\t".to_string()))));
		assert_eq!(string("\"test 🙂 123\""), Ok(("", Term::string("test 🙂 123".to_string()))));
		assert!(string("\"test 123\"a").is_err());
		assert!(string("\"test\\i123\"").is_err());
		assert!(string("\"test").is_err());
		assert!(string("test").is_err());
		assert!(string("-").is_err());
		assert!(string(" ").is_err());
	}

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

	#[test]
	fn parse_variable_declaration()
	{
		assert_eq!(variable_declaration("X Rest")
			.map(|(i, x)| (i, x.name.clone())), Ok((" Rest", "X".to_string())));
		assert_eq!(variable_declaration("X, Rest")
			.map(|(i, x)| (i, x.name.clone())), Ok((", Rest", "X".to_string())));
		// Variable declarations parsed at different locations should not be considered equal
		assert_ne!(variable_declaration("X"), variable_declaration("X"));
		assert_eq!(variable_declaration("Variable_123 Rest")
			.map(|(i, x)| (i, x.name.clone())), Ok((" Rest", "Variable_123".to_string())));
		assert!(variable_declaration("0 Rest").is_err());
		assert!(variable_declaration("123_Asd Rest").is_err());
		assert!(variable_declaration("x Rest").is_err());
		assert!(variable_declaration("variable_123 Rest").is_err());
		assert!(variable_declaration("_ Rest").is_err());
		assert!(variable_declaration("_variable_123 Rest").is_err());
		assert!(variable_declaration(" ").is_err());
	}

	#[test]
	fn parse_variable()
	{
		assert_eq!(variable("X Rest", &Declarations::new())
			.map(|(i, x)| (i, x.declaration.name.clone())), Ok((" Rest", "X".to_string())));
		assert_eq!(variable("X, Rest", &Declarations::new())
			.map(|(i, x)| (i, x.declaration.name.clone())), Ok((", Rest", "X".to_string())));
		assert_eq!(variable("Variable_123 Rest", &Declarations::new())
			.map(|(i, x)| (i, x.declaration.name.clone())),
			Ok((" Rest", "Variable_123".to_string())));
		assert!(variable("0 Rest", &Declarations::new()).is_err());
		assert!(variable("123_Asd Rest", &Declarations::new()).is_err());
		assert!(variable("x Rest", &Declarations::new()).is_err());
		assert!(variable("variable_123 Rest", &Declarations::new()).is_err());
		assert!(variable("_ Rest", &Declarations::new()).is_err());
		assert!(variable("_variable_123 Rest", &Declarations::new()).is_err());
		assert!(variable(" ", &Declarations::new()).is_err());

		let new_variable_declarations = |names: &[&str]| std::rc::Rc::new(names.iter()
			.map(|name| std::rc::Rc::new(crate::VariableDeclaration::new(name.to_string())))
			.collect());

		let layer_1 = new_variable_declarations(&["A", "B", "X"]);
		let layer_2 = new_variable_declarations(&["C", "D", "X"]);
		let layer_3 = new_variable_declarations(&["E", "F", "Y"]);
		let layer_4 = new_variable_declarations(&["G", "H", "X"]);

		let variable_declaration_stack = crate::VariableDeclarationStack::new();

		let mut declarations = Declarations::new();
		declarations.variable_declaration_stack =
			std::cell::RefCell::new(variable_declaration_stack);

		let (_, x1) = variable("X", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 1);
		let (_, x2) = variable("X", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 1);
		assert_eq!(x1.declaration, x2.declaration);
		let (_, y1) = variable("Y", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 2);
		assert_ne!(x1.declaration, y1.declaration);
		assert_ne!(x2.declaration, y1.declaration);

		declarations.variable_declaration_stack.borrow_mut().push(layer_1);

		let (_, x3) = variable("X", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 2);
		assert_ne!(x1.declaration, x3.declaration);
		let (_, x4) = variable("X", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 2);
		assert_eq!(x3.declaration, x4.declaration);
		let (_, a1) = variable("A", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 2);
		assert_ne!(x3.declaration, a1.declaration);
		let (_, y2) = variable("Y", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 2);
		assert_eq!(y1.declaration, y2.declaration);

		declarations.variable_declaration_stack.borrow_mut().push(layer_2);

		let (_, x5) = variable("X", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 2);
		assert_ne!(x1.declaration, x5.declaration);
		assert_ne!(x3.declaration, x5.declaration);
		let (_, x6) = variable("X", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 2);
		assert_eq!(x5.declaration, x6.declaration);
		let (_, a2) = variable("A", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 2);
		assert_eq!(a1.declaration, a2.declaration);

		declarations.variable_declaration_stack.borrow_mut().push(layer_3);

		let (_, x7) = variable("X", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 2);
		assert_eq!(x5.declaration, x7.declaration);
		let (_, y3) = variable("Y", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 2);
		assert_ne!(y2.declaration, y3.declaration);

		declarations.variable_declaration_stack.borrow_mut().push(layer_4);

		let (_, x8) = variable("X", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 2);
		assert_ne!(x7.declaration, x8.declaration);
		let (_, y4) = variable("Y", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 2);
		assert_eq!(y3.declaration, y4.declaration);
		let _ = variable("I", &declarations).unwrap();
		assert_eq!(declarations.variable_declaration_stack.borrow()
			.free_variable_declarations.len(), 3);
	}
}