From e42fd92d4b5288400fdb7a07284254a9c323601d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Tue, 12 May 2020 05:27:51 +0200
Subject: [PATCH] Add parser support for output statements

---
 examples/example-2.spec    |  1 +
 src/error.rs               |  9 ++++++
 src/input/specification.rs | 58 ++++++++++++++++++++++++++++++++++++++
 src/problem.rs             |  3 ++
 4 files changed, 71 insertions(+)

diff --git a/examples/example-2.spec b/examples/example-2.spec
index f273fba..af1d09e 100644
--- a/examples/example-2.spec
+++ b/examples/example-2.spec
@@ -1,4 +1,5 @@
 input: n -> integer.
+output: q/1.
 
 axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3).
 axiom: (p(0) and forall N (N >= 0 and p(N) -> p(N + 1))) -> (forall N p(N)).
diff --git a/src/error.rs b/src/error.rs
index 6b0efee..0068f56 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -15,6 +15,7 @@ pub enum Kind
 	MissingStatementTerminator,
 	ParseFormula,
 	ExpectedIdentifier,
+	ExpectedPredicateSpecifier,
 	ParsePredicateDeclaration,
 	//ParseConstantDeclaration,
 	UnknownProofDirection(String),
@@ -116,6 +117,11 @@ impl Error
 		Self::new(Kind::ExpectedIdentifier)
 	}
 
+	pub(crate) fn new_expected_predicate_specifier() -> Self
+	{
+		Self::new(Kind::ExpectedPredicateSpecifier)
+	}
+
 	pub(crate) fn new_parse_predicate_declaration() -> Self
 	{
 		Self::new(Kind::ParsePredicateDeclaration)
@@ -187,8 +193,11 @@ impl std::fmt::Debug for Error
 			Kind::UnmatchedParenthesis => write!(formatter, "unmatched parenthesis"),
 			Kind::ParseFormula => write!(formatter, "could not parse formula"),
 			Kind::ExpectedIdentifier => write!(formatter, "expected constant or predicate name"),
+			Kind::ExpectedPredicateSpecifier =>
+				write!(formatter, "expected predicate specifier (examples: p/0, q/2)"),
 			Kind::ParsePredicateDeclaration => write!(formatter,
 				"could not parse predicate declaration"),
+			// TODO: rename to ExpectedStatementTerminator
 			Kind::MissingStatementTerminator => write!(formatter,
 				"statement not terminated with ‘.’ character"),
 			Kind::UnknownProofDirection(ref proof_direction) => write!(formatter,
diff --git a/src/input/specification.rs b/src/input/specification.rs
index ac91e32..95ab38f 100644
--- a/src/input/specification.rs
+++ b/src/input/specification.rs
@@ -306,6 +306,63 @@ fn input_statement_body<'i>(mut input: &'i str, problem: &crate::Problem)
 	expect_statement_terminator(input)
 }
 
+fn output_statement_body<'i>(mut input: &'i str, problem: &crate::Problem)
+	-> Result<&'i str, crate::Error>
+{
+	input = input.trim_start();
+
+	let mut input_characters = input.chars();
+
+	let remaining_input = match input_characters.next()
+	{
+		Some(':') => input_characters.as_str(),
+		_ => return Err(crate::Error::new_expected_colon()),
+	};
+
+	input = remaining_input;
+
+	loop
+	{
+		input = input.trim_start();
+
+		let (constant_or_predicate_name, remaining_input) =
+			foliage::parse::tokens::identifier(input)
+				.ok_or_else(|| crate::Error::new_expected_identifier())?;
+
+		input = remaining_input.trim_start();
+
+		// Only accept output predicate specifiers
+		if let (Some(arity), remaining_input) = predicate_arity_specifier(input)?
+		{
+			input = remaining_input;
+
+			let mut output_predicate_declarations =
+				problem.output_predicate_declarations.borrow_mut();
+
+			use foliage::FindOrCreatePredicateDeclaration as _;
+
+			let predicate_declaration =
+				problem.find_or_create_predicate_declaration(constant_or_predicate_name, arity);
+
+			output_predicate_declarations.insert(predicate_declaration);
+		}
+		else
+		{
+			return Err(crate::Error::new_expected_predicate_specifier());
+		}
+
+		let mut input_characters = input.chars();
+
+		match input_characters.next()
+		{
+			Some(',') => input = input_characters.as_str(),
+			_ => break,
+		}
+	}
+
+	expect_statement_terminator(input)
+}
+
 pub(crate) fn parse_specification(mut input: &str, problem: &crate::Problem)
 	-> Result<(), crate::Error>
 {
@@ -424,6 +481,7 @@ pub(crate) fn parse_specification(mut input: &str, problem: &crate::Problem)
 				continue;
 			},
 			"input" => input = input_statement_body(input, problem)?,
+			"output" => input = output_statement_body(input, problem)?,
 			identifier => return Err(crate::Error::new_unknown_statement(identifier.to_string())),
 		}
 	}
diff --git a/src/problem.rs b/src/problem.rs
index 8ffd863..8567791 100644
--- a/src/problem.rs
+++ b/src/problem.rs
@@ -97,6 +97,7 @@ pub struct Problem
 	pub input_constant_declarations: std::cell::RefCell<foliage::FunctionDeclarations>,
 	pub input_constant_declaration_domains: std::cell::RefCell<InputConstantDeclarationDomains>,
 	pub input_predicate_declarations: std::cell::RefCell<foliage::PredicateDeclarations>,
+	pub output_predicate_declarations: std::cell::RefCell<foliage::PredicateDeclarations>,
 	// TODO: clean up as variable declarations are dropped
 	variable_declaration_domains: std::cell::RefCell<VariableDeclarationDomains>,
 
@@ -120,6 +121,8 @@ impl Problem
 				std::cell::RefCell::new(InputConstantDeclarationDomains::new()),
 			input_predicate_declarations:
 				std::cell::RefCell::new(foliage::PredicateDeclarations::new()),
+			output_predicate_declarations:
+				std::cell::RefCell::new(foliage::PredicateDeclarations::new()),
 			variable_declaration_domains:
 				std::cell::RefCell::new(VariableDeclarationDomains::new()),