From 32b18e2b6345db6466d773a8255826bbaaa562ee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Tue, 12 May 2020 05:20:48 +0200
Subject: [PATCH] Refactor parsing formulas

---
 Cargo.toml                 |  1 +
 src/error.rs               | 18 ++++++++++++++++++
 src/input/specification.rs | 17 ++++++++---------
 3 files changed, 27 insertions(+), 9 deletions(-)

diff --git a/Cargo.toml b/Cargo.toml
index 4cc43fb..bffbd69 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -7,6 +7,7 @@ edition = "2018"
 [dependencies]
 atty = "0.2"
 foliage = {git = "https://github.com/pluehne/foliage", branch = "parser-new"}
+itertools = "0.9"
 log = "0.4"
 pretty_env_logger = "0.4"
 regex = "1"
diff --git a/src/error.rs b/src/error.rs
index 352f314..6b0efee 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -20,6 +20,7 @@ pub enum Kind
 	UnknownProofDirection(String),
 	UnknownDomainIdentifier(String),
 	VariableNameNotAllowed(String),
+	FormulaNotClosed(std::rc::Rc<foliage::VariableDeclarations>),
 	WriteTPTPProgram,
 	RunVampire,
 	// TODO: rename to something Vampire-specific
@@ -135,6 +136,12 @@ impl Error
 		Self::new(Kind::VariableNameNotAllowed(variable_name))
 	}
 
+	pub(crate) fn new_formula_not_closed(free_variables: std::rc::Rc<foliage::VariableDeclarations>)
+		-> Self
+	{
+		Self::new(Kind::FormulaNotClosed(free_variables))
+	}
+
 	pub(crate) fn new_write_tptp_program<S: Into<Source>>(source: S) -> Self
 	{
 		Self::new(Kind::WriteTPTPProgram).with(source)
@@ -192,6 +199,17 @@ impl std::fmt::Debug for Error
 				"variable name “{}” not allowed (program variables must start with X, Y, or Z and integer variables with I, J, K, L, M, or N)",
 				variable_name),
 			Kind::WriteTPTPProgram => write!(formatter, "error writing TPTP program"),
+			Kind::FormulaNotClosed(free_variable_declarations) =>
+			{
+				let free_variable_names = free_variable_declarations
+					.iter()
+					.map(|variable_declaration| &variable_declaration.name);
+
+				let free_variable_names_output = itertools::join(free_variable_names, ", ");
+
+				write!(formatter, "formula may not contain free variables (free variables in this formula: {})",
+					free_variable_names_output)
+			},
 			Kind::RunVampire => write!(formatter, "could not run Vampire"),
 			Kind::ProveProgram(exit_code, ref stdout, ref stderr) =>
 			{
diff --git a/src/input/specification.rs b/src/input/specification.rs
index 45d58e1..ac91e32 100644
--- a/src/input/specification.rs
+++ b/src/input/specification.rs
@@ -117,39 +117,38 @@ where
 	Ok((open_formula, remaining_input))
 }
 
-fn formula<'i, D>(input: &'i str, declarations: &D)
+fn formula<'i, D>(mut input: &'i str, declarations: &D)
 	-> Result<(foliage::Formula, &'i str), crate::Error>
 where
 	D: foliage::FindOrCreateFunctionDeclaration
 		+ foliage::FindOrCreatePredicateDeclaration
 		+ crate::traits::AssignVariableDeclarationDomain,
 {
-	let (open_formula, input) = open_formula(input, declarations)?;
+	let (open_formula, remaining_input) = open_formula(input, declarations)?;
+
+	input = remaining_input;
 
 	if !open_formula.free_variable_declarations.is_empty()
 	{
-		// TODO: improve
-		panic!("formula may not contain free variables");
+		return Err(crate::Error::new_formula_not_closed(open_formula.free_variable_declarations));
 	}
 
 	Ok((open_formula.formula, input))
 }
 
-fn formula_statement_body<'i>(input: &'i str, problem: &crate::Problem)
+fn formula_statement_body<'i>(mut input: &'i str, problem: &crate::Problem)
 	-> Result<(foliage::Formula, &'i str), crate::Error>
 {
-	let input = input.trim_start();
+	input = input.trim_start();
 
 	let mut input_characters = input.chars();
 
-	let remaining_input = match input_characters.next()
+	input = match input_characters.next()
 	{
 		Some(':') => input_characters.as_str(),
 		_ => return Err(crate::Error::new_expected_colon()),
 	};
 
-	let input = remaining_input;
-
 	formula(input, problem)
 }