Remove redundant indirection

src/ast.rs

@@ -178,12 +178,12 @@ impl BinaryOperation
 pub struct Function
 {
 	pub declaration: std::rc::Rc<FunctionDeclaration>,
-	pub arguments: Vec<Box<Term>>,
+	pub arguments: Terms,
 }
 
 impl Function
 {
-	pub fn new(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
+	pub fn new(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Terms) -> Self
 	{
 		assert_eq!(declaration.arity, arguments.len(),
 			"function has a different number of arguments then declared");
@@ -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
+impl QuantifiedFormula
-{
-	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
 {
 	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
 	{
@@ -326,12 +307,12 @@ impl Implies
 pub struct Predicate
 {
 	pub declaration: std::rc::Rc<PredicateDeclaration>,
-	pub arguments: Vec<Box<Term>>,
+	pub arguments: Terms,
 }
 
 impl Predicate
 {
-	pub fn new(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
+	pub fn new(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Terms) -> Self
 	{
 		assert_eq!(declaration.arity, arguments.len(),
 			"predicate has a different number of arguments then declared");
@@ -359,7 +340,7 @@ pub enum Term
 	Variable(Variable),
 }
 
-pub type Terms = Vec<Box<Term>>;
+pub type Terms = Vec<Term>;
 
 impl Term
 {
@@ -398,8 +379,7 @@ impl Term
 		Self::boolean(false)
 	}
 
-	pub fn function(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>)
+	pub fn function(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Terms) -> Self
-		-> Self
 	{
 		Self::Function(Function::new(declaration, arguments))
 	}
@@ -471,8 +451,8 @@ pub enum Formula
 	And(Formulas),
 	Boolean(bool),
 	Compare(Compare),
-	Exists(Exists),
+	Exists(QuantifiedFormula),
-	ForAll(ForAll),
+	ForAll(QuantifiedFormula),
 	IfAndOnlyIf(Formulas),
 	Implies(Implies),
 	Not(Box<Formula>),
@@ -480,7 +460,7 @@ pub enum Formula
 	Predicate(Predicate),
 }
 
-pub type Formulas = Vec<Box<Formula>>;
+pub type Formulas = Vec<Formula>;
 
 impl Formula
 {
@@ -501,7 +481,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 +496,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
@@ -565,8 +545,7 @@ impl Formula
 		Self::Or(arguments)
 	}
 
-	pub fn predicate(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>)
+	pub fn predicate(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Terms) -> Self
-		-> Self
 	{
 		Self::Predicate(Predicate::new(declaration, arguments))
 	}

src/format/formulas.rs

@@ -412,9 +412,9 @@ mod tests
 		format!("{}", formula)
 	}
 
-	fn and(arguments: Formulas) -> Box<Formula>
+	fn and(arguments: Vec<Box<Formula>>) -> Box<Formula>
 	{
-		Box::new(Formula::and(arguments))
+		Box::new(Formula::and(arguments.into_iter().map(|x| *x).collect()))
 	}
 
 	fn equal(left: Box<Term>, right: Box<Term>) -> Box<Formula>
@@ -447,9 +447,9 @@ mod tests
 		Box::new(Formula::greater_or_equal(left, right))
 	}
 
-	fn if_and_only_if(arguments: Formulas) -> Box<Formula>
+	fn if_and_only_if(arguments: Vec<Box<Formula>>) -> Box<Formula>
 	{
-		Box::new(Formula::if_and_only_if(arguments))
+		Box::new(Formula::if_and_only_if(arguments.into_iter().map(|x| *x).collect()))
 	}
 
 	fn implies(direction: ImplicationDirection, antecedent: Box<Formula>, implication: Box<Formula>)
@@ -478,14 +478,15 @@ mod tests
 		Box::new(Formula::not_equal(left, right))
 	}
 
-	fn or(arguments: Formulas) -> Box<Formula>
+	fn or(arguments: Vec<Box<Formula>>) -> Box<Formula>
 	{
-		Box::new(Formula::or(arguments))
+		Box::new(Formula::or(arguments.into_iter().map(|x| *x).collect()))
 	}
 
-	fn predicate(name: &str, arguments: Terms) -> Box<Formula>
+	fn predicate(name: &str, arguments: Vec<Box<Term>>) -> Box<Formula>
 	{
-		Box::new(Formula::predicate(predicate_declaration(name, arguments.len()), arguments))
+		Box::new(Formula::predicate(predicate_declaration(name, arguments.len()),
+			arguments.into_iter().map(|x| *x).collect()))
 	}
 
 	fn predicate_declaration(name: &str, arity: usize) -> std::rc::Rc<PredicateDeclaration>
@@ -578,22 +579,22 @@ mod tests
 		predicate("r", vec![])
 	}
 
-	fn pqr() -> Formulas
+	fn pqr() -> Vec<Box<Formula>>
 	{
 		vec![p(), q(), r()]
 	}
 
-	fn p1q1r1() -> Formulas
+	fn p1q1r1() -> Vec<Box<Formula>>
 	{
 		vec![p1(), q1(), predicate("r1", vec![])]
 	}
 
-	fn p2q2r2() -> Formulas
+	fn p2q2r2() -> Vec<Box<Formula>>
 	{
 		vec![p2(), q2(), predicate("r2", vec![])]
 	}
 
-	fn p3q3r3() -> Formulas
+	fn p3q3r3() -> Vec<Box<Formula>>
 	{
 		vec![p3(), q3(), predicate("r3", vec![])]
 	}

src/format/terms.rs

@@ -316,7 +316,8 @@ pub(crate) mod tests
 
 	pub(crate) fn function(name: &str, arguments: Vec<Box<Term>>) -> Box<Term>
 	{
-		Box::new(Term::function(function_declaration(name, arguments.len()), arguments))
+		Box::new(Term::function(function_declaration(name, arguments.len()),
+			arguments.into_iter().map(|x| *x).collect()))
 	}
 
 	pub(crate) fn function_declaration(name: &str, arity: usize) -> std::rc::Rc<FunctionDeclaration>
@@ -404,17 +405,17 @@ pub(crate) mod tests
 		constant("e")
 	}
 
-	pub(crate) fn abc() -> Terms
+	pub(crate) fn abc() -> Vec<Box<Term>>
 	{
 		vec![a(), b(), c()]
 	}
 
-	pub(crate) fn a1b1c1() -> Terms
+	pub(crate) fn a1b1c1() -> Vec<Box<Term>>
 	{
 		vec![constant("a1"), constant("b1"), constant("c1")]
 	}
 
-	pub(crate) fn a2b2c2() -> Terms
+	pub(crate) fn a2b2c2() -> Vec<Box<Term>>
 	{
 		vec![constant("a2"), constant("b2"), constant("c2")]
 	}
@@ -434,7 +435,7 @@ pub(crate) mod tests
 		variable("Z")
 	}
 
-	pub(crate) fn xyz() -> Terms
+	pub(crate) fn xyz() -> Vec<Box<Term>>
 	{
 		vec![x(), y(), z()]
 	}

src/parse/formulas.rs

@@ -67,7 +67,7 @@ fn not<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
 	)(i)
 }
 
-fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
+fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formulas>
 {
 	map_res
 	(
@@ -89,7 +89,7 @@ fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Form
 		{
 			if arguments.len() >= 2
 			{
-				Ok(arguments.into_iter().map(Box::new).collect())
+				Ok(arguments.into_iter().collect())
 			}
 			else
 			{
@@ -99,7 +99,7 @@ fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Form
 	)(i)
 }
 
-fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
+fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formulas>
 {
 	map_res
 	(
@@ -121,7 +121,7 @@ fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formu
 		{
 			if arguments.len() >= 2
 			{
-				Ok(arguments.into_iter().map(Box::new).collect())
+				Ok(arguments.into_iter().collect())
 			}
 			else
 			{
@@ -187,7 +187,7 @@ fn implies_right_to_left<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, c
 	)(i)
 }
 
-fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
+fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formulas>
 {
 	map_res
 	(
@@ -205,7 +205,7 @@ fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<
 		{
 			if arguments.len() >= 2
 			{
-				Ok(arguments.into_iter().map(Box::new).collect())
+				Ok(arguments.into_iter().collect())
 			}
 			else
 			{
@@ -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,
+fn quantified_formula<'a, 'b>(i: &'a str, d: &Declarations, keyword: &'b str)
-	new_functor: N)
+	-> IResult<&'a str, crate::QuantifiedFormula>
-	-> IResult<&'a str, T>
-where
-	N: Fn(std::rc::Rc<crate::VariableDeclarations>, Box<crate::Formula>) -> T
 {
 	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>
@@ -538,15 +535,15 @@ mod tests
 
 		assert_eq!(format_formula("(true  and  false)"), "true and false");
 		assert_eq!(formula_as_and("(true and false)").len(), 2);
-		assert_eq!(*formula_as_and("(true and false)").remove(0), Formula::true_());
+		assert_eq!(formula_as_and("(true and false)").remove(0), Formula::true_());
-		assert_eq!(*formula_as_and("(true and false)").remove(1), Formula::false_());
+		assert_eq!(formula_as_and("(true and false)").remove(1), Formula::false_());
 		// The order of elements is retained
 		assert_ne!(formula("(true and false)"), formula("false and true"));
 		assert_eq!(format_formula("(p  and  q  and  r  and  s)"), "p and q and r and s");
 		assert_eq!(
-			as_predicate(*formula_as_and("(p and q and r and s)").remove(0)).declaration.name, "p");
+			as_predicate(formula_as_and("(p and q and r and s)").remove(0)).declaration.name, "p");
 		assert_eq!(
-			as_predicate(*formula_as_and("(p and q and r and s)").remove(3)).declaration.name, "s");
+			as_predicate(formula_as_and("(p and q and r and s)").remove(3)).declaration.name, "s");
 
 		let formula = |i| original::formula(i, &Declarations::new());
 
@@ -578,15 +575,15 @@ mod tests
 
 		assert_eq!(format_formula("(true  or  false)"), "true or false");
 		assert_eq!(formula_as_or("(true or false)").len(), 2);
-		assert_eq!(*formula_as_or("(true or false)").remove(0), Formula::true_());
+		assert_eq!(formula_as_or("(true or false)").remove(0), Formula::true_());
-		assert_eq!(*formula_as_or("(true or false)").remove(1), Formula::false_());
+		assert_eq!(formula_as_or("(true or false)").remove(1), Formula::false_());
 		// The order of elements is retained
 		assert_ne!(formula("(true or false)"), formula("false or true)"));
 		assert_eq!(format_formula("(p  or  q  or  r  or  s)"), "p or q or r or s");
 		assert_eq!(
-			as_predicate(*formula_as_or("(p or q or r or s)").remove(0)).declaration.name, "p");
+			as_predicate(formula_as_or("(p or q or r or s)").remove(0)).declaration.name, "p");
 		assert_eq!(
-			as_predicate(*formula_as_or("(p or q or r or s)").remove(3)).declaration.name, "s");
+			as_predicate(formula_as_or("(p or q or r or s)").remove(3)).declaration.name, "s");
 
 		let formula = |i| original::formula(i, &Declarations::new());
 
@@ -645,9 +642,9 @@ mod tests
 		assert_eq!(predicate_remainder("s ( )"), "");
 		assert_eq!(predicate("s ( 1 , 2 , 3 )").declaration.name, "s");
 		assert_eq!(predicate("s ( 1 , 2 , 3 )").declaration.arity, 3);
-		assert_eq!(*predicate("s ( 1 , 2 , 3 )").arguments.remove(0), Term::integer(1));
+		assert_eq!(predicate("s ( 1 , 2 , 3 )").arguments.remove(0), Term::integer(1));
-		assert_eq!(*predicate("s ( 1 , 2 , 3 )").arguments.remove(1), Term::integer(2));
+		assert_eq!(predicate("s ( 1 , 2 , 3 )").arguments.remove(1), Term::integer(2));
-		assert_eq!(*predicate("s ( 1 , 2 , 3 )").arguments.remove(2), Term::integer(3));
+		assert_eq!(predicate("s ( 1 , 2 , 3 )").arguments.remove(2), Term::integer(3));
 		assert_eq!(predicate_remainder("s ( 1 , 2 , 3 )"), "");
 		assert_eq!(predicate_remainder("s ( 1 , 2 , 3 )"), "");
 		assert_eq!(predicate("s ( ), rest").declaration.name, "s");

src/parse/terms.rs

@@ -59,7 +59,7 @@ fn absolute_value<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::T
 }
 
 pub(crate) fn function_or_predicate<'i>(i: &'i str, d: &Declarations)
-	-> IResult<&'i str, (&'i str, Option<Vec<Box<crate::Term>>>)>
+	-> IResult<&'i str, (&'i str, Option<crate::Terms>)>
 {
 	pair
 	(
@@ -82,11 +82,7 @@ pub(crate) fn function_or_predicate<'i>(i: &'i str, d: &Declarations)
 						tag(","),
 						multispace0,
 					),
-					map
+					|i| term(i, d),
-					(
-						|i| term(i, d),
-						Box::new,
-					),
 				),
 				preceded
 				(
@@ -485,8 +481,8 @@ mod tests
 		assert_eq!(term_as_function("s").declaration.arity, 0);
 		assert_eq!(term_as_function("s(1, 2, 3)").declaration.name, "s");
 		assert_eq!(term_as_function("s(1, 2, 3)").declaration.arity, 3);
-		assert_eq!(*term_as_function("s(1, 2, 3)").arguments.remove(0), Term::integer(1));
+		assert_eq!(term_as_function("s(1, 2, 3)").arguments.remove(0), Term::integer(1));
-		assert_eq!(*term_as_function("s(1, 2, 3)").arguments.remove(2), Term::integer(3));
+		assert_eq!(term_as_function("s(1, 2, 3)").arguments.remove(2), Term::integer(3));
 	}
 
 	#[test]
@@ -715,9 +711,9 @@ mod tests
 		assert_eq!(function_remainder("s ( )"), "");
 		assert_eq!(function("s ( 1 , 2 , 3 )").declaration.name, "s");
 		assert_eq!(function("s ( 1 , 2 , 3 )").declaration.arity, 3);
-		assert_eq!(*function("s ( 1 , 2 , 3 )").arguments.remove(0), Term::integer(1));
+		assert_eq!(function("s ( 1 , 2 , 3 )").arguments.remove(0), Term::integer(1));
-		assert_eq!(*function("s ( 1 , 2 , 3 )").arguments.remove(1), Term::integer(2));
+		assert_eq!(function("s ( 1 , 2 , 3 )").arguments.remove(1), Term::integer(2));
-		assert_eq!(*function("s ( 1 , 2 , 3 )").arguments.remove(2), Term::integer(3));
+		assert_eq!(function("s ( 1 , 2 , 3 )").arguments.remove(2), Term::integer(3));
 		assert_eq!(function_remainder("s ( 1 , 2 , 3 )"), "");
 		assert_eq!(function("s ( ), rest").declaration.name, "s");
 		assert_eq!(function("s ( ), rest").declaration.arity, 0);