From 80636b447ad7545525f8c6fbac545921fc478add Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Fri, 10 Apr 2020 15:18:50 +0200
Subject: [PATCH] Simplify representation of quantified formulas

---
 src/ast.rs            | 31 ++++++-------------------------
 src/parse/formulas.rs | 19 ++++++++-----------
 2 files changed, 14 insertions(+), 36 deletions(-)

diff --git a/src/ast.rs b/src/ast.rs
index 2067cfe..87b91ce 100644
--- a/src/ast.rs
+++ b/src/ast.rs
@@ -263,32 +263,13 @@ impl Compare
 }
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct Exists
+pub struct QuantifiedFormula
 {
 	pub parameters: std::rc::Rc<VariableDeclarations>,
 	pub argument: Box<Formula>,
 }
 
-impl Exists
-{
-	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
-	{
-		Self
-		{
-			parameters,
-			argument,
-		}
-	}
-}
-
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct ForAll
-{
-	pub parameters: std::rc::Rc<VariableDeclarations>,
-	pub argument: Box<Formula>,
-}
-
-impl ForAll
+impl QuantifiedFormula
 {
 	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
 	{
@@ -471,8 +452,8 @@ pub enum Formula
 	And(Formulas),
 	Boolean(bool),
 	Compare(Compare),
-	Exists(Exists),
-	ForAll(ForAll),
+	Exists(QuantifiedFormula),
+	ForAll(QuantifiedFormula),
 	IfAndOnlyIf(Formulas),
 	Implies(Implies),
 	Not(Box<Formula>),
@@ -501,7 +482,7 @@ impl Formula
 
 	pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
 	{
-		Self::Exists(Exists::new(parameters, argument))
+		Self::Exists(QuantifiedFormula::new(parameters, argument))
 	}
 
 	pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
@@ -516,7 +497,7 @@ impl Formula
 
 	pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
 	{
-		Self::ForAll(ForAll::new(parameters, argument))
+		Self::ForAll(QuantifiedFormula::new(parameters, argument))
 	}
 
 	pub fn greater(left: Box<Term>, right: Box<Term>) -> Self
diff --git a/src/parse/formulas.rs b/src/parse/formulas.rs
index 65e0927..a7da5cd 100644
--- a/src/parse/formulas.rs
+++ b/src/parse/formulas.rs
@@ -215,11 +215,8 @@ fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<
 	)(i)
 }
 
-fn quantified_expression<'a, 'b, T, N>(i: &'a str, d: &Declarations, keyword: &'b str,
-	new_functor: N)
-	-> IResult<&'a str, T>
-where
-	N: Fn(std::rc::Rc<crate::VariableDeclarations>, Box<crate::Formula>) -> T
+fn quantified_formula<'a, 'b>(i: &'a str, d: &Declarations, keyword: &'b str)
+	-> IResult<&'a str, crate::QuantifiedFormula>
 {
 	preceded
 	(
@@ -230,7 +227,7 @@ where
 		),
 		cut
 		(
-			|i| -> IResult<&'a str, T>
+			|i|
 			{
 				let (i, variable_declarations) =
 					map
@@ -270,7 +267,7 @@ where
 				d.variable_declaration_stack.borrow_mut().pop()
 					.map_err(|_| nom::Err::Failure((i, nom::error::ErrorKind::Verify)))?;
 
-				Ok((i, new_functor(variable_declarations, Box::new(argument))))
+				Ok((i, crate::QuantifiedFormula::new(variable_declarations, Box::new(argument))))
 			}
 		),
 	)(i)
@@ -330,14 +327,14 @@ fn compare<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Compare>
 	)(i)
 }
 
-fn exists<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Exists>
+fn exists<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::QuantifiedFormula>
 {
-	quantified_expression::<crate::Exists, _>(i, d, "exists", crate::Exists::new)
+	quantified_formula(i, d, "exists")
 }
 
-fn for_all<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::ForAll>
+fn for_all<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::QuantifiedFormula>
 {
-	quantified_expression::<crate::ForAll, _>(i, d, "forall", crate::ForAll::new)
+	quantified_formula(i, d, "forall")
 }
 
 fn formula_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>