README.md

@@ -1,4 +1,4 @@
-# foliage [![GitHub release](https://img.shields.io/github/release/potassco/foliage.svg?maxAge=3600)](https://github.com/potassco/foliage/releases) [![crates.io](https://img.shields.io/crates/v/foliage.svg?maxAge=3600)](https://crates.io/crates/foliage)
+# foliage [![crates.io](https://img.shields.io/crates/v/foliage.svg?maxAge=3600)](https://crates.io/crates/foliage)
 
 > First-order logic with integer arithmetics in Rust
 

src/ast.rs

@@ -379,7 +379,8 @@ impl Term
 		Self::boolean(false)
 	}
 
-	pub fn function(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
+	pub fn function(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>)
+		-> Self
 	{
 		Self::Function(Function::new(declaration, arguments))
 	}
@@ -551,7 +552,8 @@ impl Formula
 		Self::Or(arguments)
 	}
 
-	pub fn predicate(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
+	pub fn predicate(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>)
+		-> Self
 	{
 		Self::Predicate(Predicate::new(declaration, arguments))
 	}

src/format.rs

@@ -16,18 +16,25 @@ impl Precedence for crate::Term
 			| Self::String(_)
 			| Self::Variable(_)
 				=> 0,
-			Self::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..})
+			Self::UnaryOperation(
+				crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..})
 				=> 1,
-			Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, ..})
+			Self::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, ..})
 				=> 2,
-			Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, ..})
+			Self::BinaryOperation(
-			| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Divide, ..})
+				crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, ..})
-			| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
+			| Self::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Divide, ..})
+			| Self::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
 				=> 3,
 			Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Add, ..})
-			| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, ..})
+			| Self::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, ..})
 				=> 4,
-			Self::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
+			Self::UnaryOperation(
+				crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
 				=> 5,
 		}
 	}
@@ -60,6 +67,26 @@ impl Precedence for crate::Formula
 	}
 }
 
+impl std::fmt::Debug for crate::SpecialInteger
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		match &self
+		{
+			crate::SpecialInteger::Infimum => write!(format, "#inf"),
+			crate::SpecialInteger::Supremum => write!(format, "#sup"),
+		}
+	}
+}
+
+impl std::fmt::Display for crate::SpecialInteger
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", &self)
+	}
+}
+
 impl std::fmt::Debug for crate::FunctionDeclaration
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
@@ -114,8 +141,7 @@ struct TermDisplay<'term>
 	term: &'term crate::Term,
 }
 
-fn display_term<'term>(term: &'term crate::Term, parent_precedence: Option<i32>)
+fn display_term(term: &crate::Term, parent_precedence: Option<i32>) -> TermDisplay
-	-> TermDisplay<'term>
 {
 	TermDisplay
 	{
@@ -145,8 +171,7 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
 		{
 			crate::Term::Boolean(true) => write!(format, "true"),
 			crate::Term::Boolean(false) => write!(format, "false"),
-			crate::Term::SpecialInteger(crate::SpecialInteger::Infimum) => write!(format, "#inf"),
+			crate::Term::SpecialInteger(value) => write!(format, "{:?}", value),
-			crate::Term::SpecialInteger(crate::SpecialInteger::Supremum) => write!(format, "#sup"),
 			crate::Term::Integer(value) => write!(format, "{}", value),
 			crate::Term::String(value) => write!(format, "\"{}\"", value),
 			crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration),
@@ -155,12 +180,12 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
 				write!(format, "{}", function.declaration.name)?;
 
 				assert!(function.declaration.arity == function.arguments.len(),
-					"function has a different number of arguments than declared (expected {}, got {})",
+					"number of function arguments differs from declaration (expected {}, got {})",
 					function.declaration.arity, function.arguments.len());
 
-				if function.arguments.len() > 0
+				if !function.arguments.is_empty()
 				{
-					write!(format, "{}(", function.declaration.name)?;
+					write!(format, "(")?;
 
 					let mut separator = "";
 
@@ -176,21 +201,35 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
 
 				Ok(())
 			},
-			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Add, left, right})
+			crate::Term::BinaryOperation(
-				=> write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)),
+				crate::BinaryOperation{operator: crate::BinaryOperator::Add, left, right})
-			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, left, right})
+				=> write!(format, "{:?} + {:?}", display_term(left, precedence),
-				=> write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)),
+					display_term(right, precedence)),
-			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, left, right})
+			crate::Term::BinaryOperation(
-				=> write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)),
+				crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, left, right})
-			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Divide, left, right})
+				=> write!(format, "{:?} - {:?}", display_term(left, precedence),
-				=> write!(format, "{:?} / {:?}", display_term(left, precedence), display_term(right, precedence)),
+					display_term(right, precedence)),
-			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, left, right})
+			crate::Term::BinaryOperation(
-				=> write!(format, "{:?} % {:?}", display_term(left, precedence), display_term(right, precedence)),
+				crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, left, right})
-			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, left, right})
+				=> write!(format, "{:?} * {:?}", display_term(left, precedence),
-				=> write!(format, "{:?} ** {:?}", display_term(left, precedence), display_term(right, precedence)),
+					display_term(right, precedence)),
-			crate::Term::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
+			crate::Term::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Divide, left, right})
+				=> write!(format, "{:?} / {:?}", display_term(left, precedence),
+					display_term(right, precedence)),
+			crate::Term::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, left, right})
+				=> write!(format, "{:?} % {:?}", display_term(left, precedence),
+					display_term(right, precedence)),
+			crate::Term::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, left, right})
+				=> write!(format, "{:?} ** {:?}", display_term(left, precedence),
+					display_term(right, precedence)),
+			crate::Term::UnaryOperation(
+				crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
 				=> write!(format, "-{:?}", display_term(argument, precedence)),
-			crate::Term::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
+			crate::Term::UnaryOperation(
+				crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
 				=> write!(format, "|{:?}|", display_term(argument, precedence)),
 		}?;
 
@@ -217,8 +256,7 @@ struct FormulaDisplay<'formula>
 	formula: &'formula crate::Formula,
 }
 
-fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedence: Option<i32>)
+fn display_formula(formula: &crate::Formula, parent_precedence: Option<i32>) -> FormulaDisplay
-	-> FormulaDisplay<'formula>
 {
 	FormulaDisplay
 	{
@@ -280,7 +318,8 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 
 				write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
 			},
-			crate::Formula::Not(argument) => write!(format, "not {:?}", display_formula(argument, precedence))?,
+			crate::Formula::Not(argument) => write!(format, "not {:?}",
+				display_formula(argument, precedence))?,
 			crate::Formula::And(arguments) =>
 			{
 				let mut separator = "";
@@ -308,21 +347,35 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 				}
 			},
 			crate::Formula::Implies(crate::Implies{antecedent, implication})
-				=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence), display_formula(implication, precedence))?,
+				=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence),
+					display_formula(implication, precedence))?,
 			crate::Formula::IfAndOnlyIf(crate::IfAndOnlyIf{left, right})
-				=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
+				=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence),
-			crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
+					display_formula(right, precedence))?,
-				=> write!(format, "{:?} < {:?}", display_term(left, None), display_term(right, None))?,
+			crate::Formula::Compare(
-			crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
+				crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
-				=> write!(format, "{:?} <= {:?}", display_term(left, None), display_term(right, None))?,
+				=> write!(format, "{:?} < {:?}", display_term(left, None),
-			crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
+					display_term(right, None))?,
-				=> write!(format, "{:?} > {:?}", display_term(left, None), display_term(right, None))?,
+			crate::Formula::Compare(
-			crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
+				crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
-				=> write!(format, "{:?} >= {:?}", display_term(left, None), display_term(right, None))?,
+				=> write!(format, "{:?} <= {:?}", display_term(left, None),
-			crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
+					display_term(right, None))?,
-				=> write!(format, "{:?} = {:?}", display_term(left, None), display_term(right, None))?,
+			crate::Formula::Compare(
-			crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
+				crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
-				=> write!(format, "{:?} != {:?}", display_term(left, None), display_term(right, None))?,
+				=> write!(format, "{:?} > {:?}", display_term(left, None),
+					display_term(right, None))?,
+			crate::Formula::Compare(
+				crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
+				=> write!(format, "{:?} >= {:?}", display_term(left, None),
+					display_term(right, None))?,
+			crate::Formula::Compare(
+				crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
+				=> write!(format, "{:?} = {:?}", display_term(left, None),
+					display_term(right, None))?,
+			crate::Formula::Compare(
+				crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
+				=> write!(format, "{:?} != {:?}", display_term(left, None),
+					display_term(right, None))?,
 			crate::Formula::Boolean(true) => write!(format, "#true")?,
 			crate::Formula::Boolean(false) => write!(format, "#false")?,
 			crate::Formula::Predicate(predicate) =>