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

use foliage::parse::whitespace0;

pub fn recognize_and_keep<I: Clone + nom::Offset + nom::Slice<std::ops::RangeTo<usize>>, O, E: nom::error::ParseError<I>, F>(parser: F) -> impl Fn(I) -> IResult<I, (I, O), E>
where
	F: Fn(I) -> IResult<I, O, E>,
{
	move |input: I|
	{
		let i = input.clone();
		match parser(i)
		{
			Ok((i, result)) =>
			{
				let index = input.offset(&i);
				Ok((i, (input.slice(..index), result)))
			},
			Err(e) => Err(e),
		}
	}
}

fn formula_statement_kind(i: &str) -> IResult<&str, crate::project::FormulaStatementKind>
{
	delimited
	(
		whitespace0,
		alt
		((
			map
			(
				tag("axiom:"),
				|_| crate::project::FormulaStatementKind::Axiom,
			),
			map
			(
				tag("completion(constraint):"),
				|_| crate::project::FormulaStatementKind::Completion(crate::project::CompletionTarget::Constraint),
			),
			map
			(
				preceded
				(
					tag("completion"),
					delimited
					(
						tag("("),
						pair
						(
							terminated
							(
								foliage::parse::symbolic_identifier,
								tag("/"),
							),
							digit1,
						),
						tag("):"),
					),
				),
				|(name, arity)|
				match arity.parse::<usize>()
				{
					Ok(arity) => crate::project::FormulaStatementKind::Completion(
						crate::project::CompletionTarget::Predicate(foliage::PredicateDeclaration{name, arity})),
					Err(error) => panic!("invalid arity “{}”: {}", arity, error),
				}
			),
			map
			(
				tag("assumption:"),
				|_| crate::project::FormulaStatementKind::Assumption,
			),
			map
			(
				tag("lemma(forward):"),
				|_| crate::project::FormulaStatementKind::Lemma(Some(crate::project::ProofDirection::Forward)),
			),
			map
			(
				tag("lemma(backward):"),
				|_| crate::project::FormulaStatementKind::Lemma(Some(crate::project::ProofDirection::Backward)),
			),
			map
			(
				tag("lemma:"),
				|_| crate::project::FormulaStatementKind::Lemma(None),
			),
			map
			(
				tag("assertion:"),
				|_| crate::project::FormulaStatementKind::Assertion,
			),
		)),
		whitespace0,
	)(i)
}

fn formula_statement(i: &str) -> IResult<&str, (crate::project::FormulaStatementKind, foliage::Formula)>
{
	terminated
	(
		pair
		(
			formula_statement_kind,
			foliage::formula,
		),
		preceded
		(
			whitespace0,
			tag("."),
		),
	)(i)
}

fn input_statement(i: &str) -> IResult<&str, Vec<crate::project::InputSymbol>>
{
	delimited
	(
		whitespace0,
		preceded
		(
			pair
			(
				tag("input:"),
				whitespace0,
			),
			separated_list
			(
				tag(","),
				delimited
				(
					whitespace0,
					alt
					((
						map
						(
							pair
							(
								terminated
								(
									foliage::parse::symbolic_identifier,
									tag("/"),
								),
								digit1,
							),
							|(name, arity)|
							crate::project::InputSymbol::Predicate(
								foliage::PredicateDeclaration
								{
									name: name.to_string(),
									arity: arity.parse::<usize>().expect("invalid arity"),
								})
						),
						map
						(
							pair
							(
								foliage::parse::symbolic_identifier,
								opt
								(
									preceded
									(
										delimited
										(
											whitespace0,
											tag("->"),
											whitespace0,
										),
										tag("integer"),
									),
								),
							),
							|(name, domain)|
							match domain
							{
								None => crate::project::InputSymbol::Constant(
									crate::project::InputConstantDeclaration
									{
										name: name.to_string(),
										domain: foliage::Domain::Program,
									}),
								Some("integer") => crate::project::InputSymbol::Constant(
									crate::project::InputConstantDeclaration
									{
										name: name.to_string(),
										domain: foliage::Domain::Integer,
									}),
								Some(ref unknown_sort) => panic!("unrecognized sort “{}”", unknown_sort),
							}
						),
					)),
					whitespace0,
				)
			)
		),
		preceded
		(
			whitespace0,
			tag("."),
		),
	)(i)
}

pub enum Statement
{
	Formula(crate::project::FormulaStatementKind, foliage::Formula),
	Input(Vec<crate::project::InputSymbol>),
}

fn statement_enclosed_by_whitespace(i: &str)
	-> IResult<&str, (&str, (&str, Statement), &str)>
{
	tuple
	((
		recognize(whitespace0),
		recognize_and_keep
		(
			alt
			((
				map(formula_statement, |(formula_statement_kind, formula)| Statement::Formula(formula_statement_kind, formula)),
				map(input_statement, |input_symbols| Statement::Input(input_symbols)),
			))
		),
		recognize(whitespace0),
	))(i)
}

pub fn project(i: &str) -> IResult<&str, crate::Project>
{
	let mut statement_input = i.clone();
	let mut blocks = Vec::new();
	let mut input_constants = std::collections::HashSet::new();
	let mut input_predicates = std::collections::HashSet::new();

	loop
	{
		let i_ = statement_input.clone();
		match statement_enclosed_by_whitespace(i_)
		{
			Ok((i, (whitespace_before, (statement_original_text, statement), whitespace_after))) =>
			{
				// Iteration must always consume input (to prevent infinite loops)
				if i == statement_input
				{
					return Err(nom::Err::Error(nom::error::ParseError::from_error_kind(statement_input, nom::error::ErrorKind::Many0)));
				}

				if !whitespace_before.is_empty()
				{
					blocks.push(crate::project::Block::Whitespace(whitespace_before.to_string()));
				}

				match statement
				{
					Statement::Formula(formula_statement_kind, formula) =>
					{
						let formula_statement = crate::project::FormulaStatement
						{
							kind: formula_statement_kind,
							original_text: statement_original_text.to_string(),
							formula,
							proven: false,
						};

						blocks.push(crate::project::Block::FormulaStatement(formula_statement));
					},
					Statement::Input(input_symbols) =>
					{
						for input_symbol in input_symbols
						{
							match input_symbol
							{
								crate::project::InputSymbol::Constant(name) =>
								{
									input_constants.insert(name);
								},
								crate::project::InputSymbol::Predicate(declaration) =>
								{
									input_predicates.insert(declaration);
								},
							}
						}

						let input_statement = crate::project::InputStatement
						{
							original_text: statement_original_text.to_string(),
						};

						blocks.push(crate::project::Block::InputStatement(input_statement));
					},
				}

				if !whitespace_after.is_empty()
				{
					blocks.push(crate::project::Block::Whitespace(whitespace_after.to_string()));
				}

				statement_input = i;
			},
			Err(nom::Err::Error(_)) => break,
			Err(e) => return Err(e),
		}
	}

	let i = statement_input;

	// Verify that the whole file has been parsed
	if i != ""
	{
		eprintln!("parsing error at:\n{}", i);
		return Err(nom::Err::Error(nom::error::ParseError::from_error_kind(statement_input, nom::error::ErrorKind::Many0)));
	}

	let project = crate::Project
	{
		blocks,
		input_constants,
		input_predicates,
	};

	Ok((i, project))
}