enum ProofResult
{
	ProofNotFound,
	Refutation,
	Satisfiable,
}

fn reset_proof_results<'a>(project: &'a mut ask_dracula::Project)
{
	for block in &mut project.blocks
	{
		match block
		{
			ask_dracula::project::Block::Whitespace(_) => (),
			ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) => formula_statement.proven = false,
		}
	}
}

fn run_vampire<I, S>(input: &str, arguments: Option<I>)
	-> Result<(ProofResult, Option<f32>), ask_dracula::Error>
	where I: IntoIterator<Item = S>, S: AsRef<std::ffi::OsStr>
{
	let mut vampire = std::process::Command::new("vampire");

	let vampire = match arguments
	{
		Some(arguments) => vampire.args(arguments),
		None => &mut vampire,
	};

	//eprintln!("{}", input);

	let mut vampire = vampire
		.stdin(std::process::Stdio::piped())
		.stdout(std::process::Stdio::piped())
		.stderr(std::process::Stdio::piped())
		.spawn()
		.map_err(|error| ask_dracula::Error::new_run_vampire(error))?;

	{
		use std::io::Write;

		let vampire_stdin = vampire.stdin.as_mut().unwrap();
		vampire_stdin.write_all(input.as_bytes())
			.map_err(|error| ask_dracula::Error::new_run_vampire(error))?;
	}

	let output = vampire.wait_with_output()
		.map_err(|error| ask_dracula::Error::new_run_vampire(error))?;

	let stdout = std::str::from_utf8(&output.stdout)
		.map_err(|error| ask_dracula::Error::new_run_vampire(error))?;

	let stderr = std::str::from_utf8(&output.stderr)
		.map_err(|error| ask_dracula::Error::new_run_vampire(error))?;

	if !output.status.success()
	{
		let proof_not_found_regex = regex::Regex::new(r"% \(\d+\)Proof not found in time").unwrap();

		if proof_not_found_regex.is_match(stdout)
		{
			return Ok((ProofResult::ProofNotFound, None));
		}

		return Err(ask_dracula::Error::new_run_vampire(
			format!("Vampire returned unsuccessful exit code ({})\n\n======== stdout ========\n{}\n\n======== stderr ========\n{}", output.status, std::str::from_utf8(&output.stdout).unwrap_or("(not valid UTF-8)").trim(), std::str::from_utf8(&output.stderr).unwrap_or("(not valid UTF-8)").trim())));
	}

	let proof_time_regex = regex::Regex::new(r"% \(\d+\)Success in time (\d+(?:\.\d+)?) s").unwrap();

	let proof_time = proof_time_regex.captures(stdout)
		.map(|captures| captures.get(1).unwrap().as_str().parse::<f32>().ok())
		.unwrap_or(None);

	let refutation_regex = regex::Regex::new(r"% \(\d+\)Termination reason: Refutation").unwrap();

	if refutation_regex.is_match(stdout)
	{
		return Ok((ProofResult::Refutation, proof_time));
	}

	Err(ask_dracula::Error::new_interpret_vampire_output(stdout.to_string(), stderr.to_string()))
}

fn main() -> Result<(), Box<dyn std::error::Error>>
{
	let matches = clap::App::new("Ask Dracula: Using Vampire as an interactive theorem prover")
		.arg(clap::Arg::with_name("file").takes_value(true).required(true))
		.arg(clap::Arg::with_name("proof-direction").long("proof-direction").takes_value(true).default_value("forward"))
		.arg(clap::Arg::with_name("vampire_arguments").multiple(true))
		.after_help("example: ask_dracula <project file> -- --mode casc --cores 8")
		.get_matches();

	let file = matches.value_of("file").unwrap().to_string();
	let file_path = std::path::Path::new(&file);

	let file_content = std::fs::read_to_string(&file_path)?;
	let (_, mut project) = ask_dracula::parse::project(&file_content)
		.map_err(|_| "couldn’t parse input file")?;

	let proof_directions = match matches.value_of("proof-direction").unwrap()
	{
		"forward" => vec![ask_dracula::project::ProofDirection::Forward],
		"backward" => vec![ask_dracula::project::ProofDirection::Backward],
		"both" => vec![ask_dracula::project::ProofDirection::Forward, ask_dracula::project::ProofDirection::Backward],
		proof_direction => panic!("unrecognized proof direction “{}”", proof_direction),
	};

	let mut section_separator = "";
	let mut was_proof_attempted = false;

	for proof_direction in proof_directions
	{
		println!("{}performing {} proof", section_separator, proof_direction);

		section_separator = "\n";

		reset_proof_results(&mut project);

		loop
		{
			let conjecture = project.blocks.iter()
				.filter_map
				(
					|block|
					match block
					{
						ask_dracula::project::Block::Whitespace(_) => None,
						ask_dracula::project::Block::FormulaStatement(ref formula_statement) => Some(formula_statement),
					}
				)
				.find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_lemma(&formula_statement, proof_direction));

			let conjecture = match conjecture
			{
				Some(conjecture) => Some(conjecture),
				None => project.blocks.iter()
					.filter_map
					(
						|block|
						match block
						{
							ask_dracula::project::Block::Whitespace(_) => None,
							ask_dracula::project::Block::FormulaStatement(ref formula_statement) => Some(formula_statement),
						}
					)
					.find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_theorem(&formula_statement, proof_direction)),
			};

			let conjecture = match conjecture
			{
				Some(ref conjecture) => conjecture,
				None => break,
			};

			was_proof_attempted = true;

			eprintln!("verifying {}: {}", &conjecture.kind, conjecture.formula);

			let tptp_content = format!("{}", ask_dracula::format_tptp::display_project_with_conjecture_tptp(&project, conjecture, proof_direction));

			let (vampire_result, proof_time)
				= run_vampire(&tptp_content, matches.values_of("vampire_arguments").map(|value| value))?;

			match vampire_result
			{
				ProofResult::ProofNotFound =>
				{
					println!("proof not found");
					return Ok(());
				},
				ProofResult::Refutation =>
				{
					if let Some(proof_time) = proof_time
					{
						println!("{} proven in {} seconds", &conjecture.kind, proof_time);
					}
					else
					{
						println!("assertion proven");
					}

					// TODO: refactor
					let conjecture = project.blocks.iter_mut()
						.filter_map
						(
							|block|
							match block
							{
								ask_dracula::project::Block::Whitespace(_) => None,
								ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) => Some(formula_statement),
							}
						)
						.find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_lemma(&formula_statement, proof_direction));

					let mut conjecture = match conjecture
					{
						Some(conjecture) => Some(conjecture),
						None => project.blocks.iter_mut()
							.filter_map
							(
								|block|
								match block
								{
									ask_dracula::project::Block::Whitespace(_) => None,
									ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) => Some(formula_statement),
								}
							)
							.find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_theorem(&formula_statement, proof_direction)),
					}.unwrap();

					conjecture.proven = true;
				},
				ProofResult::Satisfiable =>
				{
					println!("assertion disproven");
					return Ok(());
				},
			}
		}
	}

	match was_proof_attempted
	{
		true => println!("finished all proofs"),
		false => println!("nothing to verify, exiting"),
	}

	Ok(())
}