Fix function formatting

By mistake, a function’s name was printed two consecutive times if the
function had more than one argument.

.github/workflows/main.yml

@@ -1,32 +0,0 @@
-name: Rust
-
-on:
-  push:
-    branches: [master]
-  pull_request:
-    branches: [master]
-
-jobs:
-  test:
-    name: Test
-    runs-on: ubuntu-latest
-    strategy:
-      matrix:
-        build: [stable, beta, nightly]
-        include:
-          - build: stable
-            rust: stable
-          - build: beta
-            rust: beta
-          - build: nightly
-            rust: nightly
-
-    steps:
-      - uses: actions/checkout@v2
-      - name: Install Rust (rustup)
-        run: rustup update ${{ matrix.rust }} --no-self-update && rustup default ${{ matrix.rust }}
-        shell: bash
-      - name: Build
-        run: cargo build --verbose
-      - name: Run tests
-        run: cargo test --verbose

Cargo.toml

@@ -11,10 +11,3 @@ keywords = ["logic"]
 categories = ["data-structures", "science"]
 license = "MIT"
 edition = "2018"
-
-[dependencies]
-nom = {version = "5.1", optional = true}
-
-[features]
-default = ["parse"]
-parse = ["nom"]

src/ast.rs

@@ -1,6 +1,5 @@
 // Operators
 
-#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub enum BinaryOperator
 {
 	Add,
@@ -11,7 +10,6 @@ pub enum BinaryOperator
 	Exponentiate,
 }
 
-#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub enum ComparisonOperator
 {
 	Greater,
@@ -22,22 +20,12 @@ pub enum ComparisonOperator
 	Equal,
 }
 
-#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub enum UnaryOperator
 {
 	AbsoluteValue,
 	Negative,
 }
 
-// ImplicationDirection
-
-#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub enum ImplicationDirection
-{
-	LeftToRight,
-	RightToLeft,
-}
-
 // Primitives
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
@@ -127,17 +115,6 @@ impl std::cmp::Ord for VariableDeclaration
 	}
 }
 
-impl std::hash::Hash for VariableDeclaration
-{
-	#[inline(always)]
-	fn hash<H: std::hash::Hasher>(&self, state: &mut H)
-	{
-		let p = self as *const VariableDeclaration;
-
-		p.hash(state);
-	}
-}
-
 impl VariableDeclaration
 {
 	pub fn new(name: String) -> Self
@@ -153,7 +130,6 @@ pub type VariableDeclarations = Vec<std::rc::Rc<VariableDeclaration>>;
 
 // Terms
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct BinaryOperation
 {
 	pub operator: BinaryOperator,
@@ -174,7 +150,6 @@ impl BinaryOperation
 	}
 }
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct Function
 {
 	pub declaration: std::rc::Rc<FunctionDeclaration>,
@@ -183,27 +158,25 @@ pub struct Function
 
 impl Function
 {
-	pub fn new(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
+	pub fn new(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
 	{
 		assert_eq!(declaration.arity, arguments.len(),
 			"function has a different number of arguments then declared");
 
 		Self
 		{
-			declaration,
+			declaration: std::rc::Rc::clone(declaration),
 			arguments,
 		}
 	}
 }
 
-#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub enum SpecialInteger
 {
 	Infimum,
 	Supremum,
 }
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct UnaryOperation
 {
 	pub operator: UnaryOperator,
@@ -222,7 +195,6 @@ impl UnaryOperation
 	}
 }
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct Variable
 {
 	pub declaration: std::rc::Rc<VariableDeclaration>,
@@ -230,18 +202,17 @@ pub struct Variable
 
 impl Variable
 {
-	pub fn new(declaration: std::rc::Rc<VariableDeclaration>) -> Self
+	pub fn new(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
 	{
 		Self
 		{
-			declaration,
+			declaration: std::rc::Rc::clone(declaration),
 		}
 	}
 }
 
 // Formulas
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct Compare
 {
 	pub operator: ComparisonOperator,
@@ -262,7 +233,6 @@ impl Compare
 	}
 }
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct Exists
 {
 	pub parameters: std::rc::Rc<VariableDeclarations>,
@@ -281,7 +251,6 @@ impl Exists
 	}
 }
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct ForAll
 {
 	pub parameters: std::rc::Rc<VariableDeclarations>,
@@ -300,29 +269,42 @@ impl ForAll
 	}
 }
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
+pub struct IfAndOnlyIf
+{
+	pub left: Box<Formula>,
+	pub right: Box<Formula>,
+}
+
+impl IfAndOnlyIf
+{
+	pub fn new(left: Box<Formula>, right: Box<Formula>) -> Self
+	{
+		Self
+		{
+			left,
+			right,
+		}
+	}
+}
+
 pub struct Implies
 {
-	pub direction: ImplicationDirection,
 	pub antecedent: Box<Formula>,
 	pub implication: Box<Formula>,
 }
 
 impl Implies
 {
-	pub fn new(direction: ImplicationDirection, antecedent: Box<Formula>, implication: Box<Formula>)
-		-> Self
+	pub fn new(antecedent: Box<Formula>, implication: Box<Formula>) -> Self
 	{
 		Self
 		{
-			direction,
 			antecedent,
 			implication,
 		}
 	}
 }
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct Predicate
 {
 	pub declaration: std::rc::Rc<PredicateDeclaration>,
@@ -331,14 +313,14 @@ pub struct Predicate
 
 impl Predicate
 {
-	pub fn new(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
+	pub fn new(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
 	{
 		assert_eq!(declaration.arity, arguments.len(),
 			"predicate has a different number of arguments then declared");
 
 		Self
 		{
-			declaration,
+			declaration: std::rc::Rc::clone(declaration),
 			arguments,
 		}
 	}
@@ -346,7 +328,6 @@ impl Predicate
 
 // Variants
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub enum Term
 {
 	BinaryOperation(BinaryOperation),
@@ -398,7 +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: Vec<Box<Term>>)
 		-> Self
 	{
 		Self::Function(Function::new(declaration, arguments))
@@ -459,13 +440,12 @@ impl Term
 		Self::UnaryOperation(UnaryOperation::new(operator, argument))
 	}
 
-	pub fn variable(declaration: std::rc::Rc<VariableDeclaration>) -> Self
+	pub fn variable(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
 	{
 		Self::Variable(Variable::new(declaration))
 	}
 }
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub enum Formula
 {
 	And(Formulas),
@@ -473,7 +453,7 @@ pub enum Formula
 	Compare(Compare),
 	Exists(Exists),
 	ForAll(ForAll),
-	IfAndOnlyIf(Formulas),
+	IfAndOnlyIf(IfAndOnlyIf),
 	Implies(Implies),
 	Not(Box<Formula>),
 	Or(Formulas),
@@ -486,6 +466,8 @@ impl Formula
 {
 	pub fn and(arguments: Formulas) -> Self
 	{
+		assert!(!arguments.is_empty());
+
 		Self::And(arguments)
 	}
 
@@ -501,6 +483,8 @@ impl Formula
 
 	pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
 	{
+		assert!(!parameters.is_empty());
+
 		Self::Exists(Exists::new(parameters, argument))
 	}
 
@@ -516,6 +500,8 @@ impl Formula
 
 	pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
 	{
+		assert!(!parameters.is_empty());
+
 		Self::ForAll(ForAll::new(parameters, argument))
 	}
 
@@ -529,15 +515,14 @@ impl Formula
 		Self::compare(ComparisonOperator::GreaterOrEqual, left, right)
 	}
 
-	pub fn if_and_only_if(arguments: Formulas) -> Self
+	pub fn if_and_only_if(left: Box<Formula>, right: Box<Formula>) -> Self
 	{
-		Self::IfAndOnlyIf(arguments)
+		Self::IfAndOnlyIf(IfAndOnlyIf::new(left, right))
 	}
 
-	pub fn implies(direction: ImplicationDirection, antecedent: Box<Formula>,
-		consequent: Box<Formula>) -> Self
+	pub fn implies(antecedent: Box<Formula>, consequent: Box<Formula>) -> Self
 	{
-		Self::Implies(Implies::new(direction, antecedent, consequent))
+		Self::Implies(Implies::new(antecedent, consequent))
 	}
 
 	pub fn less(left: Box<Term>, right: Box<Term>) -> Self
@@ -562,10 +547,12 @@ impl Formula
 
 	pub fn or(arguments: Formulas) -> Self
 	{
+		assert!(!arguments.is_empty());
+
 		Self::Or(arguments)
 	}
 
-	pub fn predicate(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>)
+	pub fn predicate(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>)
 		-> Self
 	{
 		Self::Predicate(Predicate::new(declaration, arguments))

src/error.rs

@@ -1,69 +0,0 @@
-pub type Source = Box<dyn std::error::Error>;
-
-pub enum Kind
-{
-	Logic(&'static str),
-}
-
-pub struct Error
-{
-	pub kind: Kind,
-	pub source: Option<Source>,
-}
-
-impl Error
-{
-	pub(crate) fn new(kind: Kind) -> Self
-	{
-		Self
-		{
-			kind,
-			source: None,
-		}
-	}
-
-	pub(crate) fn with<S: Into<Source>>(mut self, source: S) -> Self
-	{
-		self.source = Some(source.into());
-		self
-	}
-
-	pub(crate) fn new_logic(description: &'static str) -> Self
-	{
-		Self::new(Kind::Logic(description))
-	}
-}
-
-impl std::fmt::Debug for Error
-{
-	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		match &self.kind
-		{
-			Kind::Logic(ref description) => write!(formatter,
-				"logic error, please report to bug tracker ({})", description),
-		}?;
-
-		Ok(())
-	}
-}
-
-impl std::fmt::Display for Error
-{
-	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(formatter, "{:?}", self)
-	}
-}
-
-impl std::error::Error for Error
-{
-	fn source(&self) -> Option<&(dyn std::error::Error + 'static)>
-	{
-		match &self.source
-		{
-			Some(source) => Some(source.as_ref()),
-			None => None,
-		}
-	}
-}

src/format.rs

@@ -1,2 +1,450 @@
-mod formulas;
-mod terms;
+trait Precedence
+{
+	fn precedence(&self) -> i32;
+}
+
+impl Precedence for crate::Term
+{
+	fn precedence(&self) -> i32
+	{
+		match &self
+		{
+			Self::Boolean(_)
+			| Self::Function(_)
+			| Self::SpecialInteger(_)
+			| Self::Integer(_)
+			| Self::String(_)
+			| Self::Variable(_)
+				=> 0,
+			Self::UnaryOperation(
+				crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..})
+				=> 1,
+			Self::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, ..})
+				=> 2,
+			Self::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, ..})
+			| 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, ..})
+				=> 4,
+			Self::UnaryOperation(
+				crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
+				=> 5,
+		}
+	}
+}
+
+impl Precedence for crate::Formula
+{
+	fn precedence(&self) -> i32
+	{
+		match &self
+		{
+			Self::Predicate(_)
+			| Self::Boolean(_)
+			| Self::Compare(_)
+				=> 0,
+			Self::Exists(_)
+			| Self::ForAll(_)
+				=> 1,
+			Self::Not(_)
+				=> 2,
+			Self::And(_)
+				=> 3,
+			Self::Or(_)
+				=> 4,
+			Self::Implies(_)
+				=> 5,
+			Self::IfAndOnlyIf(_)
+				=> 6,
+		}
+	}
+}
+
+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
+	{
+		write!(format, "{}/{}", &self.name, self.arity)
+	}
+}
+
+impl std::fmt::Display for crate::FunctionDeclaration
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", &self)
+	}
+}
+
+impl std::fmt::Debug for crate::PredicateDeclaration
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{}/{}", &self.name, self.arity)
+	}
+}
+
+impl std::fmt::Display for crate::PredicateDeclaration
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", &self)
+	}
+}
+
+impl std::fmt::Debug for crate::VariableDeclaration
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{}", &self.name)
+	}
+}
+
+impl std::fmt::Display for crate::VariableDeclaration
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", &self)
+	}
+}
+
+struct TermDisplay<'term>
+{
+	parent_precedence: Option<i32>,
+	term: &'term crate::Term,
+}
+
+fn display_term(term: &crate::Term, parent_precedence: Option<i32>) -> TermDisplay
+{
+	TermDisplay
+	{
+		parent_precedence,
+		term,
+	}
+}
+
+impl<'term> std::fmt::Debug for TermDisplay<'term>
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		let precedence = self.term.precedence();
+		let requires_parentheses = match self.parent_precedence
+		{
+			Some(parent_precedence) => precedence > parent_precedence,
+			None => false,
+		};
+		let precedence = Some(precedence);
+
+		if requires_parentheses
+		{
+			write!(format, "(")?;
+		}
+
+		match &self.term
+		{
+			crate::Term::Boolean(true) => write!(format, "true"),
+			crate::Term::Boolean(false) => write!(format, "false"),
+			crate::Term::SpecialInteger(value) => write!(format, "{:?}", value),
+			crate::Term::Integer(value) => write!(format, "{}", value),
+			crate::Term::String(value) => write!(format, "\"{}\"", value),
+			crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration),
+			crate::Term::Function(function) =>
+			{
+				write!(format, "{}", function.declaration.name)?;
+
+				assert!(function.declaration.arity == function.arguments.len(),
+					"number of function arguments differs from declaration (expected {}, got {})",
+					function.declaration.arity, function.arguments.len());
+
+				if !function.arguments.is_empty()
+				{
+					write!(format, "(")?;
+
+					let mut separator = "";
+
+					for argument in &function.arguments
+					{
+						write!(format, "{}{:?}", separator, display_term(&argument, None))?;
+
+						separator = ", ";
+					}
+
+					write!(format, ")")?;
+				}
+
+				Ok(())
+			},
+			crate::Term::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Add, left, right})
+				=> write!(format, "{:?} + {:?}", display_term(left, precedence),
+					display_term(right, precedence)),
+			crate::Term::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, left, right})
+				=> write!(format, "{:?} - {:?}", display_term(left, precedence),
+					display_term(right, precedence)),
+			crate::Term::BinaryOperation(
+				crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, left, right})
+				=> write!(format, "{:?} * {:?}", display_term(left, precedence),
+					display_term(right, precedence)),
+			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})
+				=> write!(format, "|{:?}|", display_term(argument, precedence)),
+		}?;
+
+		if requires_parentheses
+		{
+			write!(format, ")")?;
+		}
+
+		Ok(())
+	}
+}
+
+impl<'term> std::fmt::Display for TermDisplay<'term>
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", self)
+	}
+}
+
+struct FormulaDisplay<'formula>
+{
+	parent_precedence: Option<i32>,
+	formula: &'formula crate::Formula,
+}
+
+fn display_formula(formula: &crate::Formula, parent_precedence: Option<i32>) -> FormulaDisplay
+{
+	FormulaDisplay
+	{
+		parent_precedence,
+		formula,
+	}
+}
+
+impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		let precedence = self.formula.precedence();
+		let requires_parentheses = match self.parent_precedence
+		{
+			Some(parent_precedence) => precedence > parent_precedence,
+			None => false,
+		};
+		let precedence = Some(precedence);
+
+		if requires_parentheses
+		{
+			write!(format, "(")?;
+		}
+
+		match &self.formula
+		{
+			crate::Formula::Exists(exists) =>
+			{
+				assert!(!exists.parameters.is_empty());
+
+				write!(format, "exists")?;
+
+				let mut separator = " ";
+
+				for parameter in exists.parameters.iter()
+				{
+					write!(format, "{}{:?}", separator, parameter)?;
+
+					separator = ", "
+				}
+
+				write!(format, " {:?}", display_formula(&exists.argument, precedence))?;
+			},
+			crate::Formula::ForAll(for_all) =>
+			{
+				assert!(!for_all.parameters.is_empty());
+
+				write!(format, "forall")?;
+
+				let mut separator = " ";
+
+				for parameter in for_all.parameters.iter()
+				{
+					write!(format, "{}{:?}", separator, parameter)?;
+
+					separator = ", "
+				}
+
+				write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
+			},
+			crate::Formula::Not(argument) => write!(format, "not {:?}",
+				display_formula(argument, precedence))?,
+			crate::Formula::And(arguments) =>
+			{
+				let mut separator = "";
+
+				assert!(!arguments.is_empty());
+
+				for argument in arguments
+				{
+					write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
+
+					separator = " and "
+				}
+			},
+			crate::Formula::Or(arguments) =>
+			{
+				let mut separator = "";
+
+				assert!(!arguments.is_empty());
+
+				for argument in arguments
+				{
+					write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
+
+					separator = " or "
+				}
+			},
+			crate::Formula::Implies(crate::Implies{antecedent, implication})
+				=> 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))?,
+			crate::Formula::Compare(
+				crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
+				=> write!(format, "{:?} < {:?}", display_term(left, None),
+					display_term(right, None))?,
+			crate::Formula::Compare(
+				crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
+				=> write!(format, "{:?} <= {:?}", display_term(left, None),
+					display_term(right, None))?,
+			crate::Formula::Compare(
+				crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
+				=> 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) =>
+			{
+				write!(format, "{}", predicate.declaration.name)?;
+
+				if !predicate.arguments.is_empty()
+				{
+					write!(format, "(")?;
+
+					let mut separator = "";
+
+					for argument in &predicate.arguments
+					{
+						write!(format, "{}{:?}", separator, display_term(argument, None))?;
+
+						separator = ", "
+					}
+
+					write!(format, ")")?;
+				}
+			},
+		}
+
+		if requires_parentheses
+		{
+			write!(format, ")")?;
+		}
+
+		Ok(())
+	}
+}
+
+impl<'formula> std::fmt::Display for FormulaDisplay<'formula>
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", self)
+	}
+}
+
+impl std::fmt::Debug for crate::Formula
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", display_formula(&self, None))
+	}
+}
+
+impl std::fmt::Display for crate::Formula
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{}", display_formula(&self, None))
+	}
+}
+
+impl std::fmt::Debug for crate::Term
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", display_term(&self, None))
+	}
+}
+
+impl std::fmt::Display for crate::Term
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{}", display_term(&self, None))
+	}
+}

src/lib.rs

@@ -1,10 +1,4 @@
 mod ast;
-mod error;
 pub mod format;
-#[cfg(feature = "parse")]
-pub mod parse;
-mod utils;
 
 pub use ast::*;
-pub use error::Error;
-pub use utils::VariableDeclarationStack;

src/parse.rs

@@ -1,32 +0,0 @@
-mod formulas;
-mod helpers;
-mod literals;
-mod names;
-mod terms;
-
-pub(crate) use helpers::word_boundary;
-pub(crate) use literals::{boolean, integer, special_integer, string};
-pub(crate) use names::{function_or_predicate_name, variable_name};
-pub use terms::term;
-pub use formulas::formula;
-
-pub struct Declarations
-{
-	function_declarations: std::cell::RefCell<crate::FunctionDeclarations>,
-	predicate_declarations: std::cell::RefCell<crate::PredicateDeclarations>,
-	variable_declaration_stack: std::cell::RefCell<crate::VariableDeclarationStack>,
-}
-
-impl Declarations
-{
-	pub fn new() -> Self
-	{
-		Self
-		{
-			function_declarations: std::cell::RefCell::new(crate::FunctionDeclarations::new()),
-			predicate_declarations: std::cell::RefCell::new(crate::PredicateDeclarations::new()),
-			variable_declaration_stack:
-				std::cell::RefCell::new(crate::VariableDeclarationStack::new()),
-		}
-	}
-}

src/parse/formulas.rs

@@ -1,686 +0,0 @@
-use nom::
-{
-	IResult,
-	branch::alt,
-	bytes::complete::tag,
-	character::complete::multispace0,
-	combinator::{cut, map, map_res},
-	multi::{many1, separated_list},
-	sequence::{delimited, pair, preceded, terminated, tuple},
-};
-
-use super::{Declarations, boolean, word_boundary};
-
-pub fn predicate<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Predicate>
-{
-	map
-	(
-		|i| crate::parse::terms::function_or_predicate(i, d),
-		|(name, arguments)|
-		{
-			let arguments = match arguments
-			{
-				Some(arguments) => arguments,
-				None => vec![],
-			};
-
-			let mut predicate_declarations = d.predicate_declarations.borrow_mut();
-
-			let declaration = match predicate_declarations.iter()
-				.find(|x| x.name == name && x.arity == arguments.len())
-			{
-				Some(declaration) => std::rc::Rc::clone(&declaration),
-				None =>
-				{
-					let declaration = crate::PredicateDeclaration
-					{
-						name: name.to_string(),
-						arity: arguments.len(),
-					};
-					let declaration = std::rc::Rc::new(declaration);
-
-					predicate_declarations.insert(std::rc::Rc::clone(&declaration));
-
-					declaration
-				},
-			};
-
-			crate::Predicate::new(declaration, arguments)
-		},
-	)(i)
-}
-
-fn not<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
-{
-	map
-	(
-		preceded
-		(
-			terminated
-			(
-				tag("not"),
-				multispace0,
-			),
-			|i| formula_precedence_2(i, d),
-		),
-		|x| crate::Formula::not(Box::new(x)),
-	)(i)
-}
-
-fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
-{
-	map_res
-	(
-		separated_list
-		(
-			delimited
-			(
-				multispace0,
-				terminated
-				(
-					tag("and"),
-					word_boundary,
-				),
-				multispace0,
-			),
-			|i| formula_precedence_2(i, d),
-		),
-		|arguments| -> Result<_, (_, _)>
-		{
-			if arguments.len() >= 2
-			{
-				Ok(arguments.into_iter().map(Box::new).collect())
-			}
-			else
-			{
-				Err(nom::error::make_error(i, nom::error::ErrorKind::Many1))
-			}
-		}
-	)(i)
-}
-
-fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
-{
-	map_res
-	(
-		separated_list
-		(
-			delimited
-			(
-				multispace0,
-				terminated
-				(
-					tag("or"),
-					word_boundary,
-				),
-				multispace0,
-			),
-			|i| formula_precedence_3(i, d),
-		),
-		|arguments| -> Result<_, (_, _)>
-		{
-			if arguments.len() >= 2
-			{
-				Ok(arguments.into_iter().map(Box::new).collect())
-			}
-			else
-			{
-				Err(nom::error::make_error(i, nom::error::ErrorKind::Many1))
-			}
-		}
-	)(i)
-}
-
-fn implies_left_to_right<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
-{
-	map
-	(
-		pair
-		(
-			many1
-			(
-				terminated
-				(
-					|i| formula_precedence_4(i, d),
-					delimited
-					(
-						multispace0,
-						tag("->"),
-						multispace0,
-					),
-				)
-			),
-			|i| formula_precedence_4(i, d),
-		),
-		|(arguments, last_argument)| arguments.into_iter().rev().fold(last_argument,
-			|accumulator, argument|
-				crate::Formula::implies(crate::ImplicationDirection::LeftToRight,
-					Box::new(argument), Box::new(accumulator)))
-	)(i)
-}
-
-fn implies_right_to_left<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
-{
-	map
-	(
-		pair
-		(
-			|i| formula_precedence_4(i, d),
-			many1
-			(
-				preceded
-				(
-					delimited
-					(
-						multispace0,
-						tag("<-"),
-						multispace0,
-					),
-					|i| formula_precedence_4(i, d),
-				)
-			),
-		),
-		|(first_argument, arguments)| arguments.into_iter().fold(first_argument,
-			|accumulator, argument|
-				crate::Formula::implies(crate::ImplicationDirection::RightToLeft,
-					Box::new(argument), Box::new(accumulator)))
-	)(i)
-}
-
-fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
-{
-	map_res
-	(
-		separated_list
-		(
-			delimited
-			(
-				multispace0,
-				tag("<->"),
-				multispace0,
-			),
-			|i| formula_precedence_5(i, d),
-		),
-		|arguments| -> Result<_, (_, _)>
-		{
-			if arguments.len() >= 2
-			{
-				Ok(arguments.into_iter().map(Box::new).collect())
-			}
-			else
-			{
-				Err(nom::error::make_error(i, nom::error::ErrorKind::Many1))
-			}
-		}
-	)(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
-{
-	preceded
-	(
-		terminated
-		(
-			tag(keyword),
-			word_boundary,
-		),
-		cut
-		(
-			|i| -> IResult<&'a str, T>
-			{
-				let (i, variable_declarations) =
-					map
-					(
-						delimited
-						(
-							multispace0,
-							separated_list
-							(
-								delimited
-								(
-									multispace0,
-									tag(","),
-									multispace0,
-								),
-								map
-								(
-									crate::parse::terms::variable_declaration,
-									std::rc::Rc::new,
-								),
-							),
-							multispace0,
-						),
-						std::rc::Rc::new,
-					)(i)?;
-
-				if variable_declarations.is_empty()
-				{
-					return Err(nom::Err::Failure((i, nom::error::ErrorKind::Many1)));
-				}
-
-				d.variable_declaration_stack.borrow_mut().push(std::rc::Rc::clone(&variable_declarations));
-
-				let (i, argument) = formula_precedence_0(i, d)?;
-
-				// TODO: report logic errors more appropriately
-				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))))
-			}
-		),
-	)(i)
-}
-
-fn compare<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Compare>
-{
-	map
-	(
-		tuple
-		((
-			|i| crate::parse::term(i, d),
-			delimited
-			(
-				multispace0,
-				alt
-				((
-					map
-					(
-						tag(">"),
-						|_| crate::ComparisonOperator::Greater,
-					),
-					map
-					(
-						tag("<"),
-						|_| crate::ComparisonOperator::Less,
-					),
-					map
-					(
-						tag("<="),
-						|_| crate::ComparisonOperator::LessOrEqual,
-					),
-					map
-					(
-						tag(">="),
-						|_| crate::ComparisonOperator::GreaterOrEqual,
-					),
-					map
-					(
-						tag("!="),
-						|_| crate::ComparisonOperator::NotEqual,
-					),
-					map
-					(
-						tag("="),
-						|_| crate::ComparisonOperator::Equal,
-					),
-				)),
-				multispace0,
-			),
-			|i| crate::parse::term(i, d),
-		)),
-		|(left, operator, right)|
-		{
-			crate::Compare::new(operator, Box::new(left), Box::new(right))
-		}
-	)(i)
-}
-
-fn exists<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Exists>
-{
-	quantified_expression::<crate::Exists, _>(i, d, "exists", crate::Exists::new)
-}
-
-fn for_all<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::ForAll>
-{
-	quantified_expression::<crate::ForAll, _>(i, d, "forall", crate::ForAll::new)
-}
-
-fn formula_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
-{
-	delimited
-	(
-		terminated
-		(
-			tag("("),
-			multispace0,
-		),
-		|i| formula(i, d),
-		preceded
-		(
-			multispace0,
-			tag(")"),
-		),
-	)(i)
-}
-
-fn formula_precedence_0<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
-{
-	alt
-	((
-		map
-		(
-			boolean,
-			crate::Formula::Boolean,
-		),
-		map
-		(
-			|i| predicate(i, d),
-			crate::Formula::Predicate,
-		),
-		map
-		(
-			|i| compare(i, d),
-			crate::Formula::Compare,
-		),
-		|i| formula_parenthesized(i, d),
-	))(i)
-}
-
-fn formula_precedence_1<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
-{
-	alt
-	((
-		map
-		(
-			|i| exists(i, d),
-			crate::Formula::Exists,
-		),
-		map
-		(
-			|i| for_all(i, d),
-			crate::Formula::ForAll,
-		),
-		|i| formula_precedence_0(i, d),
-	))(i)
-}
-
-fn formula_precedence_2<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
-{
-	alt
-	((
-		|i| not(i, d),
-		|i| formula_precedence_1(i, d),
-	))(i)
-}
-
-fn formula_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
-{
-	alt
-	((
-		map
-		(
-			|i| and(i, d),
-			crate::Formula::And,
-		),
-		|i| formula_precedence_2(i, d),
-	))(i)
-}
-
-fn formula_precedence_4<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
-{
-	alt
-	((
-		map
-		(
-			|i| or(i, d),
-			crate::Formula::Or,
-		),
-		|i| formula_precedence_3(i, d),
-	))(i)
-}
-
-fn formula_precedence_5<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
-{
-	alt
-	((
-		|i| implies_left_to_right(i, d),
-		|i| implies_right_to_left(i, d),
-		|i| formula_precedence_4(i, d),
-	))(i)
-}
-
-fn formula_precedence_6<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
-{
-	alt
-	((
-		map
-		(
-			|i| if_and_only_if(i, d),
-			crate::Formula::IfAndOnlyIf,
-		),
-		|i| formula_precedence_5(i, d),
-	))(i)
-}
-
-pub fn formula<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
-{
-	formula_precedence_6(i, d)
-}
-
-#[cfg(test)]
-mod tests
-{
-	use crate::parse::formulas::*;
-	use crate::parse::formulas as original;
-	use crate::{Formula, Term};
-
-	fn formula(i: &str) -> Formula
-	{
-		original::formula(i, &Declarations::new()).unwrap().1
-	}
-
-	fn formula_remainder(i: &str) -> &str
-	{
-		original::formula(i, &Declarations::new()).unwrap().0
-	}
-
-	fn format_formula(i: &str) -> String
-	{
-		format!("{}", formula(i))
-	}
-
-	#[test]
-	fn parse_boolean()
-	{
-		assert_eq!(formula("true"), Formula::true_());
-		assert_eq!(formula("false"), Formula::false_());
-	}
-
-	#[test]
-	fn parse_precedence()
-	{
-		assert_eq!(format_formula("a -> b -> c <-> d -> e -> f"), "a -> b -> c <-> d -> e -> f");
-		assert_eq!(format_formula("(a -> b -> c) <-> (d -> e -> f)"), "a -> b -> c <-> d -> e -> f");
-		assert_eq!(format_formula("a <- b <- c <-> d <- e <- f"), "a <- b <- c <-> d <- e <- f");
-		assert_eq!(format_formula("(a <- b <- c) <-> (d <- e <- f)"), "a <- b <- c <-> d <- e <- f");
-	}
-
-	#[test]
-	fn parse_exists()
-	{
-		let formula_as_exists = |i| match formula(i)
-		{
-			Formula::Exists(exists) => exists,
-			_ => panic!("expected existentially quantified formula"),
-		};
-
-		let as_predicate = |x| match x
-		{
-			Formula::Predicate(arguments) => arguments,
-			_ => panic!("expected predicate"),
-		};
-
-		assert_eq!(format_formula("exists  X , Y , Z  ( p )"), "exists X, Y, Z p");
-		assert_eq!(formula_as_exists("exists  X , Y , Z  ( p )").parameters.len(), 3);
-		assert_eq!(as_predicate(*formula_as_exists("exists  X , Y , Z  ( p )").argument)
-			.declaration.name, "p");
-	}
-
-	#[test]
-	fn parse_and()
-	{
-		let formula_as_and = |i| match formula(i)
-		{
-			Formula::And(arguments) => arguments,
-			_ => panic!("expected conjunction"),
-		};
-
-		let as_predicate = |x| match x
-		{
-			Formula::Predicate(arguments) => arguments,
-			_ => panic!("expected predicate"),
-		};
-
-		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(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");
-		assert_eq!(
-			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());
-
-		// Malformed formulas shouldn’t be accepted
-		assert!(formula("and").is_err());
-		assert!(formula("and p").is_err());
-		assert_eq!(formula_remainder("p and"), " and");
-		assert_eq!(formula_remainder("p andq"), " andq");
-		assert_eq!(formula_remainder("p and q and"), " and");
-		assert_eq!(formula_remainder("p and q andq"), " andq");
-		assert!(formula("(p and) q").is_err());
-		assert_eq!(formula_remainder("p (and q)"), " (and q)");
-	}
-
-	#[test]
-	fn parse_or()
-	{
-		let formula_as_or = |i| match formula(i)
-		{
-			Formula::Or(arguments) => arguments,
-			_ => panic!("expected disjunction"),
-		};
-
-		let as_predicate = |x| match x
-		{
-			Formula::Predicate(arguments) => arguments,
-			_ => panic!("expected predicate"),
-		};
-
-		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(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");
-		assert_eq!(
-			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());
-
-		// Malformed formulas shouldn’t be accepted
-		assert!(formula("or").is_err());
-		assert!(formula("or p").is_err());
-		assert_eq!(formula_remainder("p or"), " or");
-		assert_eq!(formula_remainder("p orq"), " orq");
-		assert_eq!(formula_remainder("p or q or"), " or");
-		assert_eq!(formula_remainder("p or q orq"), " orq");
-		assert!(formula("(p or) q").is_err());
-		assert_eq!(formula_remainder("p (or q)"), " (or q)");
-	}
-
-	#[test]
-	fn parse_implies()
-	{
-		let formula_as_implies = |i| match formula(i)
-		{
-			Formula::Implies(implies) => implies,
-			_ => panic!("expected implication"),
-		};
-
-		let as_predicate = |x| match x
-		{
-			Formula::Predicate(arguments) => arguments,
-			_ => panic!("expected predicate"),
-		};
-
-		assert_eq!(as_predicate(*formula_as_implies("a -> b").antecedent).declaration.name, "a");
-		assert_eq!(as_predicate(*formula_as_implies("a -> b").implication).declaration.name, "b");
-		assert_eq!(formula_as_implies("a -> b").direction,
-			crate::ImplicationDirection::LeftToRight);
-
-		assert_eq!(as_predicate(*formula_as_implies("a <- b").antecedent).declaration.name, "b");
-		assert_eq!(as_predicate(*formula_as_implies("a <- b").implication).declaration.name, "a");
-		assert_eq!(formula_as_implies("a <- b").direction,
-			crate::ImplicationDirection::RightToLeft);
-
-		assert_eq!(format_formula("(a -> b -> c)"), "a -> b -> c");
-		assert_eq!(format_formula("(a -> (b -> c))"), "a -> b -> c");
-		assert_eq!(format_formula("((a -> b) -> c)"), "(a -> b) -> c");
-	}
-
-	#[test]
-	fn parse_predicate()
-	{
-		let predicate = |i| original::predicate(i, &Declarations::new()).unwrap().1;
-		let predicate_remainder = |i| original::predicate(i, &Declarations::new()).unwrap().0;
-
-		assert_eq!(predicate("s").declaration.name, "s");
-		assert_eq!(predicate("s").declaration.arity, 0);
-		assert_eq!(predicate_remainder("s"), "");
-		assert_eq!(predicate("s ( )").declaration.name, "s");
-		assert_eq!(predicate("s ( )").declaration.arity, 0);
-		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(1), Term::integer(2));
-		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");
-		assert_eq!(predicate("s ( ), rest").declaration.arity, 0);
-		assert_eq!(predicate_remainder("s ( ), rest"), ", rest");
-		assert_eq!(predicate("s ( 1 , 2 , 3 ), rest").declaration.name, "s");
-		assert_eq!(predicate("s ( 1 , 2 , 3 ), rest").declaration.arity, 3);
-		assert_eq!(predicate_remainder("s ( 1 , 2 , 3 ), rest"), ", rest");
-	}
-
-	#[test]
-	fn parse_exists_primitive()
-	{
-		assert_eq!(exists("exists X (p(X, Y, X, Y)), rest", &Declarations::new())
-			.map(|(i, x)| (i, x.parameters.len())),
-			Ok((", rest", 1)));
-		assert_eq!(exists("exists X p(X, Y, X, Y), rest", &Declarations::new())
-			.map(|(i, x)| (i, x.parameters.len())),
-			Ok((", rest", 1)));
-		assert!(exists("exists (p(X, Y, X, Y)), rest", &Declarations::new()).is_err());
-		assert!(exists("exists X, rest", &Declarations::new()).is_err());
-		assert!(exists("exists X (), rest", &Declarations::new()).is_err());
-		assert!(exists("exists X (, true), rest", &Declarations::new()).is_err());
-		assert!(exists("exists X (true, ), rest", &Declarations::new()).is_err());
-		assert!(exists("exists X (true false), rest", &Declarations::new()).is_err());
-		assert!(exists("exists X (true), rest", &Declarations::new()).is_ok());
-		assert!(exists("exists X p(X), rest", &Declarations::new()).is_ok());
-	}
-
-	#[test]
-	fn parse_formula()
-	{
-		// TODO: refactor
-		formula("exists X, Y (p(X, Y, X, Y) and X < Y and q(X) <-> r(X)), rest");
-	}
-}

src/parse/helpers.rs

@@ -1,86 +0,0 @@
-use nom::
-{
-	IResult,
-	branch::alt,
-	bytes::complete::take_while_m_n,
-	combinator::{map, peek, rest_len, verify},
-};
-
-fn is_character_word_boundary(c: char) -> bool
-{
-	if c.is_whitespace()
-	{
-		return true;
-	}
-
-	match c
-	{
-		'('
-		| ')'
-		| '>'
-		| '<'
-		| '='
-		| ','
-		| '+'
-		| '-'
-		| '*'
-		| '/'
-		| '%'
-		| '|'
-		| '#'
-			=> true,
-		_ => false,
-	}
-}
-
-pub(crate) fn word_boundary(i: &str) -> IResult<&str, ()>
-{
-	peek
-	(
-		alt
-		((
-			// Accept word boundary characters
-			map
-			(
-				take_while_m_n(1, 1, is_character_word_boundary),
-				|_| (),
-			),
-			// Accept end of file
-			map
-			(
-				verify
-				(
-					rest_len,
-					|rest_length| *rest_length == 0usize,
-				),
-				|_| (),
-			),
-		))
-	)(i)
-}
-
-#[cfg(test)]
-mod tests
-{
-	use crate::parse::*;
-
-	#[test]
-	fn detect_word_boundaries()
-	{
-		assert_eq!(word_boundary(" rest"), Ok((" rest", ())));
-		assert_eq!(word_boundary("(rest"), Ok(("(rest", ())));
-		assert_eq!(word_boundary(")rest"), Ok((")rest", ())));
-		assert_eq!(word_boundary(",rest"), Ok((",rest", ())));
-		assert_eq!(word_boundary("+rest"), Ok(("+rest", ())));
-		assert_eq!(word_boundary("-rest"), Ok(("-rest", ())));
-		assert_eq!(word_boundary("*rest"), Ok(("*rest", ())));
-		assert_eq!(word_boundary("/rest"), Ok(("/rest", ())));
-		assert_eq!(word_boundary("%rest"), Ok(("%rest", ())));
-		assert_eq!(word_boundary("|rest"), Ok(("|rest", ())));
-		assert_eq!(word_boundary("<rest"), Ok(("<rest", ())));
-		assert_eq!(word_boundary(">rest"), Ok((">rest", ())));
-		assert_eq!(word_boundary("=rest"), Ok(("=rest", ())));
-		assert!(word_boundary("0").is_err());
-		assert!(word_boundary("rest").is_err());
-	}
-}

src/parse/literals.rs

@@ -1,249 +0,0 @@
-use nom::
-{
-	IResult,
-	branch::alt,
-	bytes::complete::{escaped_transform, tag},
-	character::complete::{digit1, none_of},
-	combinator::{map, map_res, opt, recognize},
-	sequence::{delimited, pair, terminated},
-};
-
-use super::word_boundary;
-
-fn true_(i: &str) -> IResult<&str, bool>
-{
-	map
-	(
-		terminated
-		(
-			tag("true"),
-			word_boundary,
-		),
-		|_| true,
-	)(i)
-}
-
-fn false_(i: &str) -> IResult<&str, bool>
-{
-	map
-	(
-		terminated
-		(
-			tag("false"),
-			word_boundary,
-		),
-		|_| false,
-	)(i)
-}
-
-pub fn boolean(i: &str) -> IResult<&str, bool>
-{
-	alt
-	((
-		true_,
-		false_,
-	))(i)
-}
-
-pub fn integer(i: &str) -> IResult<&str, i32>
-{
-	map_res
-	(
-		recognize
-		(
-			terminated
-			(
-				pair
-				(
-					opt
-					(
-						alt
-						((
-							tag("-"),
-							tag("+"),
-						))
-					),
-					digit1,
-				),
-				word_boundary,
-			)
-		),
-		std::str::FromStr::from_str,
-	)(i)
-}
-
-fn infimum(i: &str) -> IResult<&str, crate::SpecialInteger>
-{
-	map
-	(
-		terminated
-		(
-			tag("#inf"),
-			word_boundary,
-		),
-		|_| crate::SpecialInteger::Infimum,
-	)(i)
-}
-
-fn supremum(i: &str) -> IResult<&str, crate::SpecialInteger>
-{
-	map
-	(
-		terminated
-		(
-			tag("#sup"),
-			word_boundary,
-		),
-		|_| crate::SpecialInteger::Supremum,
-	)(i)
-}
-
-pub fn special_integer(i: &str) -> IResult<&str, crate::SpecialInteger>
-{
-	alt
-	((
-		infimum,
-		supremum,
-	))(i)
-}
-
-pub fn string(i: &str) -> IResult<&str, String>
-{
-	map
-	(
-		terminated
-		(
-			delimited
-			(
-				tag("\""),
-				escaped_transform
-				(
-					none_of("\"\\"),
-					'\\',
-					alt
-					((
-						tag("\""),
-						tag("\\"),
-						map
-						(
-							tag("n"),
-							|_| "\n",
-						),
-						map
-						(
-							tag("t"),
-							|_| "\t",
-						),
-					)),
-				),
-				tag("\""),
-			),
-			word_boundary,
-		),
-		String::from,
-	)(i)
-}
-
-#[cfg(test)]
-mod tests
-{
-	use crate::SpecialInteger;
-	use crate::parse::*;
-
-	#[test]
-	fn parse_boolean()
-	{
-		assert_eq!(boolean("true"), Ok(("", true)));
-		assert_eq!(boolean("false"), Ok(("", false)));
-		assert_eq!(boolean("true false"), Ok((" false", true)));
-		assert_eq!(boolean("false true"), Ok((" true", false)));
-		assert_eq!(boolean("true,"), Ok((",", true)));
-		assert_eq!(boolean("false,"), Ok((",", false)));
-		assert!(boolean("truefalse").is_err());
-		assert!(boolean("falsetrue").is_err());
-		assert!(boolean("truea").is_err());
-		assert!(boolean("falsea").is_err());
-		assert!(boolean("a").is_err());
-		assert!(boolean("-").is_err());
-		assert!(boolean(" ").is_err());
-	}
-
-	#[test]
-	fn parse_integer()
-	{
-		assert_eq!(integer("0"), Ok(("", 0)));
-		assert_eq!(integer("10000"), Ok(("", 10000)));
-		assert_eq!(integer("+10000"), Ok(("", 10000)));
-		assert_eq!(integer("-10000"), Ok(("", -10000)));
-		assert_eq!(integer("0 42"), Ok((" 42", 0)));
-		assert_eq!(integer("10000 42"), Ok((" 42", 10000)));
-		assert_eq!(integer("+10000 42"), Ok((" 42", 10000)));
-		assert_eq!(integer("-10000 42"), Ok((" 42", -10000)));
-		assert_eq!(integer("10000,"), Ok((",", 10000)));
-		assert_eq!(integer("+10000,"), Ok((",", 10000)));
-		assert_eq!(integer("-10000,"), Ok((",", -10000)));
-		assert!(integer("10000a").is_err());
-		assert!(integer("+10000a").is_err());
-		assert!(integer("-10000a").is_err());
-		assert!(integer("1.5").is_err());
-		assert!(integer("a").is_err());
-		assert!(integer("-").is_err());
-		assert!(integer(" ").is_err());
-	}
-
-	#[test]
-	fn parse_special_integer()
-	{
-		assert_eq!(special_integer("#inf"), Ok(("", SpecialInteger::Infimum)));
-		assert_eq!(special_integer("#sup"), Ok(("", SpecialInteger::Supremum)));
-		assert_eq!(special_integer("#inf #sup"), Ok((" #sup", SpecialInteger::Infimum)));
-		assert_eq!(special_integer("#sup #inf"), Ok((" #inf", SpecialInteger::Supremum)));
-		assert_eq!(special_integer("#inf,"), Ok((",", SpecialInteger::Infimum)));
-		assert_eq!(special_integer("#sup,"), Ok((",", SpecialInteger::Supremum)));
-		assert!(special_integer("#inf0").is_err());
-		assert!(special_integer("#sup0").is_err());
-		assert!(special_integer("#infimum").is_err());
-		assert!(special_integer("#supremum").is_err());
-		assert!(special_integer("inf").is_err());
-		assert!(special_integer("sup").is_err());
-		assert!(special_integer("0").is_err());
-		assert!(special_integer("10000").is_err());
-		assert!(special_integer("-10000").is_err());
-		assert!(special_integer("-").is_err());
-		assert!(special_integer("+").is_err());
-		assert!(special_integer("a").is_err());
-		assert!(special_integer(" ").is_err());
-	}
-
-	#[test]
-	fn parse_string()
-	{
-		assert_eq!(string("\"test 123\""), Ok(("", "test 123".to_string())));
-		assert_eq!(string("\"123 test\""), Ok(("", "123 test".to_string())));
-		assert_eq!(string("\" test 123 \""), Ok(("", " test 123 ".to_string())));
-		assert_eq!(string("\"test 123\" \"rest"), Ok((" \"rest", "test 123".to_string())));
-		assert_eq!(string("\"test 123\", \"rest"), Ok((", \"rest", "test 123".to_string())));
-		assert_eq!(string("\"test\n123\""), Ok(("", "test\n123".to_string())));
-		assert_eq!(string("\"test\\\"123\""), Ok(("", "test\"123".to_string())));
-		assert_eq!(string("\"test\\\"123\\\"\""), Ok(("", "test\"123\"".to_string())));
-		assert_eq!(string("\"\\\"test 123\\\"\""), Ok(("", "\"test 123\"".to_string())));
-		assert_eq!(string("\"test\\\\123\""), Ok(("", "test\\123".to_string())));
-		assert_eq!(string("\"test\\\\123\\\\\""), Ok(("", "test\\123\\".to_string())));
-		assert_eq!(string("\"\\\\test 123\\\\\""), Ok(("", "\\test 123\\".to_string())));
-		assert_eq!(string("\"test\\n123\""), Ok(("", "test\n123".to_string())));
-		assert_eq!(string("\"test\\n123\\n\""), Ok(("", "test\n123\n".to_string())));
-		assert_eq!(string("\"\\ntest 123\\n\""), Ok(("", "\ntest 123\n".to_string())));
-		assert_eq!(string("\"test\\t123\""), Ok(("", "test\t123".to_string())));
-		assert_eq!(string("\"test\\t123\\t\""), Ok(("", "test\t123\t".to_string())));
-		assert_eq!(string("\"\\ttest 123\\t\""), Ok(("", "\ttest 123\t".to_string())));
-		assert_eq!(string("\"test 🙂 123\""), Ok(("", "test 🙂 123".to_string())));
-		assert_eq!(string("\"🙂test 123\""), Ok(("", "🙂test 123".to_string())));
-		assert_eq!(string("\"test 123🙂\""), Ok(("", "test 123🙂".to_string())));
-		assert!(string("\"test 123\"a").is_err());
-		assert!(string("\"test\\i123\"").is_err());
-		assert!(string("\"test").is_err());
-		assert!(string("test").is_err());
-		assert!(string("-").is_err());
-		assert!(string(" ").is_err());
-	}
-}

src/parse/names.rs

@@ -1,159 +0,0 @@
-use nom::
-{
-	IResult,
-	bytes::complete::{take_while, take_while_m_n},
-	combinator::recognize,
-	sequence::{pair, terminated},
-};
-
-use super::word_boundary;
-
-fn is_function_name_character_first(c: char) -> bool
-{
-	c.is_alphabetic() && c.is_lowercase()
-}
-
-fn is_function_name_character_body(c: char) -> bool
-{
-	c.is_alphanumeric() || c == '_'
-}
-
-fn is_variable_name_character_first(c: char) -> bool
-{
-	c.is_alphabetic() && c.is_uppercase()
-}
-
-fn is_variable_name_character_body(c: char) -> bool
-{
-	c.is_alphanumeric() || c == '_'
-}
-
-pub fn function_or_predicate_name(i: &str) -> IResult<&str, &str>
-{
-	let (i, name) =
-		recognize
-		(
-			terminated
-			(
-				pair
-				(
-					take_while_m_n(1, 1, is_function_name_character_first),
-					take_while(is_function_name_character_body),
-				),
-				word_boundary,
-			)
-		)(i)?;
-
-	match name
-	{
-		"and"
-		| "exists"
-		| "false"
-		| "forall"
-		| "not"
-		| "or"
-		| "true"
-			=> Err(nom::Err::Error((i, nom::error::ErrorKind::Verify))),
-		name => Ok((i, name)),
-	}
-}
-
-pub fn variable_name(i: &str) -> IResult<&str, &str>
-{
-	recognize
-	(
-		terminated
-		(
-			pair
-			(
-				take_while_m_n(1, 1, is_variable_name_character_first),
-				take_while(is_variable_name_character_body),
-			),
-			word_boundary,
-		)
-	)(i)
-}
-
-#[cfg(test)]
-mod tests
-{
-	use crate::parse::*;
-
-	#[test]
-	fn parse_function_or_predicate_name()
-	{
-		assert_eq!(function_or_predicate_name("p rest"), Ok((" rest", "p")));
-		assert_eq!(function_or_predicate_name("f rest"), Ok((" rest", "f")));
-		assert_eq!(function_or_predicate_name("p, rest"), Ok((", rest", "p")));
-		assert_eq!(function_or_predicate_name("f, rest"), Ok((", rest", "f")));
-		assert_eq!(function_or_predicate_name("name_123 rest"), Ok((" rest", "name_123")));
-		assert!(function_or_predicate_name("0 rest").is_err());
-		assert!(function_or_predicate_name("123_asd rest").is_err());
-		assert!(function_or_predicate_name("P rest").is_err());
-		assert!(function_or_predicate_name("Predicate_123 rest").is_err());
-		assert!(function_or_predicate_name("_ rest").is_err());
-		assert!(function_or_predicate_name("_predicate_123 rest").is_err());
-		assert!(function_or_predicate_name("(p").is_err());
-		assert!(function_or_predicate_name(")p").is_err());
-		assert!(function_or_predicate_name(">p").is_err());
-		assert!(function_or_predicate_name("<p").is_err());
-		assert!(function_or_predicate_name("=p").is_err());
-		assert!(function_or_predicate_name(",p").is_err());
-		assert!(function_or_predicate_name("+p").is_err());
-		assert!(function_or_predicate_name("-p").is_err());
-		assert!(function_or_predicate_name("*p").is_err());
-		assert!(function_or_predicate_name("/p").is_err());
-		assert!(function_or_predicate_name("%p").is_err());
-		assert!(function_or_predicate_name("|p").is_err());
-		assert!(function_or_predicate_name("#inf").is_err());
-		assert!(function_or_predicate_name("#sup").is_err());
-		assert!(function_or_predicate_name("#p").is_err());
-		assert!(function_or_predicate_name(" ").is_err());
-		// Keywords aren’t valid names
-		assert!(function_or_predicate_name("and rest").is_err());
-		assert!(function_or_predicate_name("exists rest").is_err());
-		assert!(function_or_predicate_name("false rest").is_err());
-		assert!(function_or_predicate_name("forall rest").is_err());
-		assert!(function_or_predicate_name("or rest").is_err());
-		assert!(function_or_predicate_name("not rest").is_err());
-		assert!(function_or_predicate_name("true rest").is_err());
-		// Names that start with keywords are fine though
-		assert!(function_or_predicate_name("anda rest").is_ok());
-		assert!(function_or_predicate_name("existsa rest").is_ok());
-		assert!(function_or_predicate_name("falsea rest").is_ok());
-		assert!(function_or_predicate_name("foralla rest").is_ok());
-		assert!(function_or_predicate_name("ora rest").is_ok());
-		assert!(function_or_predicate_name("nota rest").is_ok());
-		assert!(function_or_predicate_name("truea rest").is_ok());
-	}
-
-	#[test]
-	fn parse_variable_name()
-	{
-		assert_eq!(variable_name("X Rest"), Ok((" Rest", "X")));
-		assert_eq!(variable_name("X, Rest"), Ok((", Rest", "X")));
-		assert_eq!(variable_name("Variable_123 Rest"), Ok((" Rest", "Variable_123")));
-		assert!(variable_name("0 Rest").is_err());
-		assert!(variable_name("123_Asd Rest").is_err());
-		assert!(variable_name("x Rest").is_err());
-		assert!(variable_name("variable_123 Rest").is_err());
-		assert!(variable_name("_ Rest").is_err());
-		assert!(variable_name("_variable_123 Rest").is_err());
-		assert!(variable_name("(X").is_err());
-		assert!(variable_name(")X").is_err());
-		assert!(variable_name(">X").is_err());
-		assert!(variable_name("<X").is_err());
-		assert!(variable_name("=X").is_err());
-		assert!(variable_name(",X").is_err());
-		assert!(variable_name("+X").is_err());
-		assert!(variable_name("-X").is_err());
-		assert!(variable_name("*X").is_err());
-		assert!(variable_name("/X").is_err());
-		assert!(variable_name("%X").is_err());
-		assert!(variable_name("|X").is_err());
-		assert!(variable_name("#inf").is_err());
-		assert!(variable_name("#sup").is_err());
-		assert!(variable_name("#X").is_err());
-		assert!(variable_name(" ").is_err());
-	}
-}

src/parse/terms.rs

@@ -1,856 +0,0 @@
-use nom::
-{
-	IResult,
-	branch::alt,
-	bytes::complete::tag,
-	character::complete::multispace0,
-	combinator::{map, opt},
-	multi::{many1, separated_list},
-	sequence::{delimited, pair, preceded, terminated},
-};
-
-use super::{Declarations, boolean, function_or_predicate_name, integer, special_integer, string,
-	variable_name};
-
-fn negative<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Term>
-{
-	map
-	(
-		preceded
-		(
-			terminated
-			(
-				tag("-"),
-				multispace0,
-			),
-			|i| term_precedence_1(i, d),
-		),
-		|x| match x
-		{
-			crate::Term::Integer(value) => crate::Term::integer(-value),
-			crate::Term::UnaryOperation(
-				crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
-				=> *argument,
-			_ => crate::Term::negative(Box::new(x)),
-		}
-	)(i)
-}
-
-fn absolute_value<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Term>
-{
-	map
-	(
-		delimited
-		(
-			terminated
-			(
-				tag("|"),
-				multispace0,
-			),
-			|i| term(i, d),
-			preceded
-			(
-				multispace0,
-				tag("|"),
-			),
-		),
-		|x| crate::Term::absolute_value(Box::new(x)),
-	)(i)
-}
-
-pub(crate) fn function_or_predicate<'i>(i: &'i str, d: &Declarations)
-	-> IResult<&'i str, (&'i str, Option<Vec<Box<crate::Term>>>)>
-{
-	pair
-	(
-		function_or_predicate_name,
-		opt
-		(
-			delimited
-			(
-				delimited
-				(
-					multispace0,
-					tag("("),
-					multispace0,
-				),
-				separated_list
-				(
-					delimited
-					(
-						multispace0,
-						tag(","),
-						multispace0,
-					),
-					map
-					(
-						|i| term(i, d),
-						Box::new,
-					),
-				),
-				preceded
-				(
-					multispace0,
-					tag(")"),
-				),
-			)
-		),
-	)(i)
-}
-
-pub fn function<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Function>
-{
-	map
-	(
-		|i| function_or_predicate(i, d),
-		|(name, arguments)|
-		{
-			let arguments = match arguments
-			{
-				Some(arguments) => arguments,
-				None => vec![],
-			};
-
-			let mut function_declarations = d.function_declarations.borrow_mut();
-
-			let declaration = match function_declarations.iter()
-				.find(|x| x.name == name && x.arity == arguments.len())
-			{
-				Some(declaration) => std::rc::Rc::clone(&declaration),
-				None =>
-				{
-					let declaration = crate::FunctionDeclaration
-					{
-						name: name.to_string(),
-						arity: arguments.len(),
-					};
-					let declaration = std::rc::Rc::new(declaration);
-
-					function_declarations.insert(std::rc::Rc::clone(&declaration));
-
-					declaration
-				},
-			};
-
-			crate::Function::new(declaration, arguments)
-		},
-	)(i)
-}
-
-pub fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
-{
-	map
-	(
-		variable_name,
-		|name| crate::VariableDeclaration::new(name.to_string())
-	)(i)
-}
-
-pub fn variable<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Variable>
-{
-	map
-	(
-		variable_name,
-		|name|
-		{
-			let mut variable_declaration_stack = d.variable_declaration_stack.borrow_mut();
-
-			let declaration = variable_declaration_stack.find_or_create(name);
-
-			crate::Variable::new(declaration)
-		},
-	)(i)
-}
-
-fn term_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
-{
-	delimited
-	(
-		terminated
-		(
-			tag("("),
-			multispace0,
-		),
-		|i| term(i, d),
-		preceded
-		(
-			multispace0,
-			tag(")"),
-		),
-	)(i)
-}
-
-fn term_precedence_0<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
-{
-	alt
-	((
-		map
-		(
-			boolean,
-			crate::Term::Boolean,
-		),
-		map
-		(
-			special_integer,
-			crate::Term::SpecialInteger,
-		),
-		map
-		(
-			integer,
-			crate::Term::Integer,
-		),
-		map
-		(
-			|i| function(i, d),
-			crate::Term::Function,
-		),
-		map
-		(
-			string,
-			crate::Term::String,
-		),
-		map
-		(
-			|i| variable(i, d),
-			crate::Term::Variable,
-		),
-		|i| absolute_value(i, d),
-		|i| term_parenthesized(i, d),
-	))(i)
-}
-
-fn term_precedence_1<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
-{
-	alt
-	((
-		|i| negative(i, d),
-		|i| term_precedence_0(i, d),
-	))(i)
-}
-
-fn term_precedence_2<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
-{
-	alt
-	((
-		map
-		(
-			pair
-			(
-				many1
-				(
-					terminated
-					(
-						|i| term_precedence_1(i, d),
-						delimited
-						(
-							multispace0,
-							tag("**"),
-							multispace0,
-						),
-					)
-				),
-				|i| term_precedence_1(i, d),
-			),
-			|(arguments, last_argument)| arguments.into_iter().rev().fold(last_argument,
-				|accumulator, argument|
-					crate::Term::exponentiate(Box::new(argument), Box::new(accumulator))),
-		),
-		|i| term_precedence_1(i, d),
-	))(i)
-}
-
-fn term_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
-{
-	alt
-	((
-		map
-		(
-			pair
-			(
-				|i| term_precedence_2(i, d),
-				many1
-				(
-					pair
-					(
-						delimited
-						(
-							multispace0,
-							alt
-							((
-								tag("*"),
-								tag("/"),
-								tag("%"),
-							)),
-							multispace0,
-						),
-						|i| term_precedence_2(i, d),
-					)
-				),
-			),
-			|(first_argument, arguments)| arguments.into_iter().fold(first_argument,
-				|accumulator, (operator, argument)|
-				match operator
-				{
-					"*" => crate::Term::multiply(Box::new(accumulator), Box::new(argument)),
-					"/" => crate::Term::divide(Box::new(accumulator), Box::new(argument)),
-					"%" => crate::Term::modulo(Box::new(accumulator), Box::new(argument)),
-					// TODO: handle appropriately
-					_ => panic!("test"),
-				})
-		),
-		|i| term_precedence_2(i, d),
-	))(i)
-}
-
-fn term_precedence_4<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
-{
-	alt
-	((
-		map
-		(
-			pair
-			(
-				|i| term_precedence_3(i, d),
-				many1
-				(
-					pair
-					(
-						delimited
-						(
-							multispace0,
-							alt
-							((
-								tag("+"),
-								tag("-"),
-							)),
-							multispace0,
-						),
-						|i| term_precedence_3(i, d),
-					)
-				),
-			),
-			|(first_argument, arguments)| arguments.into_iter().fold(first_argument,
-				|accumulator, (operator, argument)|
-				match operator
-				{
-					"+" => crate::Term::add(Box::new(accumulator), Box::new(argument)),
-					"-" => crate::Term::subtract(Box::new(accumulator), Box::new(argument)),
-					// TODO: handle appropriately
-					_ => panic!("test"),
-				})
-		),
-		|i| term_precedence_3(i, d),
-	))(i)
-}
-
-pub fn term<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
-{
-	term_precedence_4(i, d)
-}
-
-#[cfg(test)]
-mod tests
-{
-	use crate::parse::terms::*;
-	use crate::parse::terms as original;
-	use crate::{Term, VariableDeclaration, VariableDeclarationStack};
-
-	fn term(i: &str) -> Term
-	{
-		original::term(i, &Declarations::new()).unwrap().1
-	}
-
-	fn format_term(i: &str) -> String
-	{
-		format!("{}", term(i))
-	}
-
-	#[test]
-	fn parse_parenthesized()
-	{
-		assert_eq!(format_term("(1)"), format_term("1"));
-		assert_eq!(format_term("((1))"), format_term("1"));
-		assert_eq!(format_term("(-1)"), format_term("-1"));
-		assert_eq!(format_term("((-1))"), format_term("-1"));
-		assert_eq!(format_term("(-(1))"), format_term("-1"));
-		assert_eq!(format_term("-((1))"), format_term("-1"));
-		assert_eq!(format_term("(-(-1))"), format_term("1"));
-		assert_eq!(format_term("-((-1))"), format_term("1"));
-		assert_eq!(format_term("-(-(1))"), format_term("1"));
-		assert_eq!(format_term("-(-(-1))"), format_term("-1"));
-		assert_eq!(format_term("(a)"), format_term("a"));
-		assert_eq!(format_term("((a))"), format_term("a"));
-		assert_eq!(format_term("(X)"), format_term("X"));
-		assert_eq!(format_term("((X))"), format_term("X"));
-		assert_eq!(format_term("(\"test\")"), format_term("\"test\""));
-		assert_eq!(format_term("((\"test\"))"), format_term("\"test\""));
-		assert_eq!(format_term("(a ** b)"), format_term("a ** b"));
-		assert_eq!(format_term("(a * b)"), format_term("a * b"));
-		assert_eq!(format_term("(a / b)"), format_term("a / b"));
-		assert_eq!(format_term("(a % b)"), format_term("a % b"));
-		assert_eq!(format_term("(a + b)"), format_term("a + b"));
-		assert_eq!(format_term("(a - b)"), format_term("a - b"));
-		assert_eq!(format_term("((a ** b))"), format_term("a ** b"));
-		assert_eq!(format_term("((a * b))"), format_term("a * b"));
-		assert_eq!(format_term("((a / b))"), format_term("a / b"));
-		assert_eq!(format_term("((a % b))"), format_term("a % b"));
-		assert_eq!(format_term("((a + b))"), format_term("a + b"));
-		assert_eq!(format_term("((a - b))"), format_term("a - b"));
-		assert_eq!(format_term("(f(a, b))"), format_term("f(a, b)"));
-		assert_eq!(format_term("((f(a, b)))"), format_term("f(a, b)"));
-		assert_eq!(format_term("f((a), (b))"), format_term("f(a, b)"));
-		assert_eq!(format_term("f(|-a|)"), format_term("f(|-a|)"));
-		assert_eq!(format_term("f((|-a|))"), format_term("f(|-a|)"));
-		assert_eq!(format_term("f((-a))"), format_term("f(-a)"));
-		assert_eq!(format_term("f(((-a)))"), format_term("f(-a)"));
-		assert_eq!(format_term("f((a ** b))"), format_term("f(a ** b)"));
-		assert_eq!(format_term("f((a * b))"), format_term("f(a * b)"));
-		assert_eq!(format_term("f((a / b))"), format_term("f(a / b)"));
-		assert_eq!(format_term("f((a % b))"), format_term("f(a % b)"));
-		assert_eq!(format_term("f((a + b))"), format_term("f(a + b)"));
-		assert_eq!(format_term("f((a - b))"), format_term("f(a - b)"));
-		assert_eq!(format_term("f(((a ** b)))"), format_term("f(a ** b)"));
-		assert_eq!(format_term("f(((a * b)))"), format_term("f(a * b)"));
-		assert_eq!(format_term("f(((a / b)))"), format_term("f(a / b)"));
-		assert_eq!(format_term("f(((a % b)))"), format_term("f(a % b)"));
-		assert_eq!(format_term("f(((a + b)))"), format_term("f(a + b)"));
-		assert_eq!(format_term("f(((a - b)))"), format_term("f(a - b)"));
-		assert_eq!(format_term("(|a ** b|)"), format_term("|a ** b|"));
-		assert_eq!(format_term("|(a ** b)|"), format_term("|a ** b|"));
-		assert_eq!(format_term("(|(a ** b)|)"), format_term("|a ** b|"));
-		assert_eq!(format_term("(|a * b|)"), format_term("|a * b|"));
-		assert_eq!(format_term("|(a * b)|"), format_term("|a * b|"));
-		assert_eq!(format_term("(|(a * b)|)"), format_term("|a * b|"));
-		assert_eq!(format_term("(|a / b|)"), format_term("|a / b|"));
-		assert_eq!(format_term("|(a / b)|"), format_term("|a / b|"));
-		assert_eq!(format_term("(|(a / b)|)"), format_term("|a / b|"));
-		assert_eq!(format_term("(|a % b|)"), format_term("|a % b|"));
-		assert_eq!(format_term("|(a % b)|"), format_term("|a % b|"));
-		assert_eq!(format_term("(|(a % b)|)"), format_term("|a % b|"));
-	}
-
-	#[test]
-	fn parse_boolean()
-	{
-		assert_eq!(term("true"), Term::true_());
-		assert_eq!(term("false"), Term::false_());
-	}
-
-	#[test]
-	fn parse_integer()
-	{
-		assert_eq!(term("0"), Term::integer(0));
-		assert_eq!(term("10000"), Term::integer(10000));
-		assert_eq!(term("+10000"), Term::integer(10000));
-		assert_eq!(term("-10000"), Term::integer(-10000));
-	}
-
-	#[test]
-	fn parse_special_integer()
-	{
-		assert_eq!(term("#inf"), Term::infimum());
-		assert_eq!(term("#sup"), Term::supremum());
-	}
-
-	#[test]
-	fn parse_string()
-	{
-		// TODO: fix
-		//assert_eq!(term("\"\""), Term::string("".to_string()));
-		assert_eq!(term("\"a\""), Term::string("a".to_string()));
-		assert_eq!(term("\"#\""), Term::string("#".to_string()));
-		assert_eq!(term("\" \""), Term::string(" ".to_string()));
-		assert_eq!(term("\"     \""), Term::string("     ".to_string()));
-		assert_eq!(term("\"test test\""), Term::string("test test".to_string()));
-		assert_eq!(term("\"123 456\""), Term::string("123 456".to_string()));
-		assert_eq!(term("\"-#? -#?\""), Term::string("-#? -#?".to_string()));
-		assert_eq!(term("\"\\ntest\\n123\\n\""), Term::string("\ntest\n123\n".to_string()));
-		assert_eq!(term("\"\\ttest\\t123\\t\""), Term::string("\ttest\t123\t".to_string()));
-		assert_eq!(term("\"\\\\test\\\\123\\\\\""), Term::string("\\test\\123\\".to_string()));
-		assert_eq!(term("\"🙂test🙂123🙂\""), Term::string("🙂test🙂123🙂".to_string()));
-	}
-
-	#[test]
-	fn parse_function()
-	{
-		let term_as_function = |i| match term(i)
-		{
-			Term::Function(function) => function,
-			_ => panic!("expected function"),
-		};
-
-		assert_eq!(term_as_function("s").declaration.name, "s");
-		assert_eq!(term_as_function("s").declaration.arity, 0);
-		assert_eq!(term_as_function("s()").declaration.name, "s");
-		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(2), Term::integer(3));
-	}
-
-	#[test]
-	fn parse_variable()
-	{
-		let term_as_variable = |i| match term(i)
-		{
-			Term::Variable(variable) => variable,
-			_ => panic!("expected variable"),
-		};
-
-		assert_eq!(term_as_variable("X").declaration.name, "X");
-		assert_eq!(term_as_variable("Variable_123").declaration.name, "Variable_123");
-	}
-
-	#[test]
-	fn parse_unary()
-	{
-		assert_eq!(format_term("|a|"), "|a|");
-		assert_eq!(format_term("||a||"), "||a||");
-		assert_eq!(format_term("|a - b|"), "|a - b|");
-		assert_eq!(format_term("|a| - b"), "|a| - b");
-		assert_eq!(format_term("a - |b|"), "a - |b|");
-		assert_eq!(format_term("||a| - b|"), "||a| - b|");
-		assert_eq!(format_term("|a - |b||"), "|a - |b||");
-		assert_eq!(format_term("||a| - |b||"), "||a| - |b||");
-		assert_eq!(format_term("||a| - |b| - |c||"), "||a| - |b| - |c||");
-		assert_eq!(format_term("||a - b| - |c - d||"), "||a - b| - |c - d||");
-		assert_eq!(format_term("-a"), "-a");
-		assert_eq!(format_term("--a"), "a");
-		assert_eq!(format_term("---a"), "-a");
-		assert_eq!(format_term("-(a + b)"), "-(a + b)");
-		assert_eq!(format_term("-|a + b|"), "-|a + b|");
-		assert_eq!(format_term("--|a + b|"), "|a + b|");
-		assert_eq!(format_term("---|a + b|"), "-|a + b|");
-		assert_eq!(term("5"), Term::integer(5));
-		assert_eq!(term("-5"), Term::integer(-5));
-		assert_eq!(term("--5"), Term::integer(5));
-		assert_eq!(term("---5"), Term::integer(-5));
-		assert_eq!(term("0"), Term::integer(0));
-		assert_eq!(term("-0"), Term::integer(0));
-		assert_eq!(term("--0"), Term::integer(0));
-		assert_eq!(term("---0"), Term::integer(0));
-	}
-
-	#[test]
-	fn parse_exponentiate()
-	{
-		assert_eq!(term("1 ** (2 ** (3 ** (4 ** 5)))"), term("1 ** 2 ** 3 ** 4 ** 5"));
-		assert_eq!(format_term("1 ** 2 ** 3 ** 4 ** 5"), "1 ** 2 ** 3 ** 4 ** 5");
-		assert_eq!(term("1 ** (2 ** (3 ** (4 ** 5)))"), term("1 ** 2 ** 3 ** 4 ** 5"));
-		// As exponentiation is right-associative, these parentheses cannot be omitted
-		assert_ne!(term("(((1 ** 2) ** 3) ** 4) ** 5"), term("1 ** 2 ** 3 ** 4 ** 5"));
-		assert_eq!(format_term("(((1 ** 2) ** 3) ** 4) ** 5"), "(((1 ** 2) ** 3) ** 4) ** 5");
-	}
-
-	#[test]
-	fn parse_multiplicative()
-	{
-		assert_eq!(format_term("(a * b) * (c * d)"), "a * b * c * d");
-		assert_eq!(format_term("(a * b) * (c / d)"), "a * b * c / d");
-		assert_eq!(format_term("(a * b) * (c % d)"), "a * b * (c % d)");
-		assert_eq!(format_term("(a / b) * (c * d)"), "a / b * c * d");
-		assert_eq!(format_term("(a / b) * (c / d)"), "a / b * c / d");
-		assert_eq!(format_term("(a / b) * (c % d)"), "a / b * (c % d)");
-		assert_eq!(format_term("(a % b) * (c * d)"), "a % b * c * d");
-		assert_eq!(format_term("(a % b) * (c / d)"), "a % b * c / d");
-		assert_eq!(format_term("(a % b) * (c % d)"), "a % b * (c % d)");
-		assert_eq!(format_term("(a * b) / (c * d)"), "a * b / (c * d)");
-		assert_eq!(format_term("(a * b) / (c / d)"), "a * b / (c / d)");
-		assert_eq!(format_term("(a * b) / (c % d)"), "a * b / (c % d)");
-		assert_eq!(format_term("(a / b) / (c * d)"), "a / b / (c * d)");
-		assert_eq!(format_term("(a / b) / (c / d)"), "a / b / (c / d)");
-		assert_eq!(format_term("(a / b) / (c % d)"), "a / b / (c % d)");
-		assert_eq!(format_term("(a % b) / (c * d)"), "a % b / (c * d)");
-		assert_eq!(format_term("(a % b) / (c / d)"), "a % b / (c / d)");
-		assert_eq!(format_term("(a % b) / (c % d)"), "a % b / (c % d)");
-		assert_eq!(format_term("(a * b) % (c * d)"), "a * b % (c * d)");
-		assert_eq!(format_term("(a * b) % (c / d)"), "a * b % (c / d)");
-		assert_eq!(format_term("(a * b) % (c % d)"), "a * b % (c % d)");
-		assert_eq!(format_term("(a / b) % (c * d)"), "a / b % (c * d)");
-		assert_eq!(format_term("(a / b) % (c / d)"), "a / b % (c / d)");
-		assert_eq!(format_term("(a / b) % (c % d)"), "a / b % (c % d)");
-		assert_eq!(format_term("(a % b) % (c * d)"), "a % b % (c * d)");
-		assert_eq!(format_term("(a % b) % (c / d)"), "a % b % (c / d)");
-		assert_eq!(format_term("(a % b) % (c % d)"), "a % b % (c % d)");
-
-		// TODO: test malformed expressions
-	}
-
-	#[test]
-	fn parse_additive()
-	{
-		assert_eq!(format_term("(a + b) + (c + d)"), "a + b + c + d");
-		assert_eq!(format_term("(a + b) + (c - d)"), "a + b + c - d");
-		assert_eq!(format_term("(a - b) + (c + d)"), "a - b + c + d");
-		assert_eq!(format_term("(a - b) + (c - d)"), "a - b + c - d");
-		assert_eq!(format_term("(a + b) - (c + d)"), "a + b - (c + d)");
-		assert_eq!(format_term("(a + b) - (c - d)"), "a + b - (c - d)");
-		assert_eq!(format_term("(a - b) - (c + d)"), "a - b - (c + d)");
-		assert_eq!(format_term("(a - b) - (c - d)"), "a - b - (c - d)");
-	}
-
-	#[test]
-	fn parse_precedence()
-	{
-		assert_eq!(term("-a + b"), term("(-a) + b"));
-		assert_eq!(term("-a + -b"), term("(-a) + (-b)"));
-		assert_eq!(term("-a + -b"), term("-(a) + -(b)"));
-		assert_eq!(format_term("-(a + b)"), "-(a + b)");
-		assert_eq!(term("-a - b"), term("(-a) - b"));
-		assert_eq!(term("-a - -b"), term("(-a) - (-b)"));
-		assert_eq!(term("-a - -b"), term("-(a) - -(b)"));
-		assert_eq!(term("-a * b"), term("(-a) * b"));
-		assert_eq!(term("-a * -b"), term("(-a) * (-b)"));
-		assert_eq!(term("-a * -b"), term("-(a) * -(b)"));
-		assert_eq!(term("-a / b"), term("(-a) / b"));
-		assert_eq!(term("-a / -b"), term("(-a) / (-b)"));
-		assert_eq!(term("-a / -b"), term("-(a) / -(b)"));
-		assert_eq!(term("-a % b"), term("(-a) % b"));
-		assert_eq!(term("-a % -b"), term("(-a) % (-b)"));
-		assert_eq!(term("-a % -b"), term("-(a) % -(b)"));
-		assert_eq!(term("-a ** b"), term("(-a) ** b"));
-		assert_eq!(term("-a ** -b"), term("(-a) ** (-b)"));
-		assert_eq!(term("-a ** -b"), term("-(a) ** -(b)"));
-		assert_eq!(format_term("-(a + b)"), "-(a + b)");
-		assert_eq!(format_term("-(a + b)"), "-(a + b)");
-		assert_eq!(format_term("-(a + b)"), "-(a + b)");
-		assert_eq!(format_term("-(a + b)"), "-(a + b)");
-		assert_eq!(format_term("-(a + b)"), "-(a + b)");
-		assert_eq!(term("a + (b * c) + d"), term("(a + (b * c)) + d"));
-		assert_eq!(term("a + (b / c) + d"), term("(a + (b / c)) + d"));
-		assert_eq!(term("a + (b % c) + d"), term("(a + (b % c)) + d"));
-		assert_eq!(term("a - (b * c) - d"), term("(a - (b * c)) - d"));
-		assert_eq!(term("a - (b / c) - d"), term("(a - (b / c)) - d"));
-		assert_eq!(term("a - (b % c) - d"), term("(a - (b % c)) - d"));
-		assert_eq!(format_term("(a + b) * (c + d)"), "(a + b) * (c + d)");
-		assert_eq!(format_term("(a + b) / (c + d)"), "(a + b) / (c + d)");
-		assert_eq!(format_term("(a + b) % (c + d)"), "(a + b) % (c + d)");
-		assert_eq!(format_term("(a - b) * (c - d)"), "(a - b) * (c - d)");
-		assert_eq!(format_term("(a - b) / (c - d)"), "(a - b) / (c - d)");
-		assert_eq!(format_term("(a - b) % (c - d)"), "(a - b) % (c - d)");
-		assert_eq!(term("a ** b ** c + d ** e ** f"), term("(a ** b ** c) + (d ** e ** f)"));
-		assert_eq!(term("a ** (b ** c + d) ** e ** f"), term("a ** ((b ** c + d) ** (e ** f))"));
-		assert_eq!(term("a ** b ** (c + d) ** e ** f"), term("a ** (b ** ((c + d) ** (e ** f)))"));
-		assert_eq!(term("a ** b ** (c + d ** e) ** f"), term("a ** (b ** ((c + d ** e) ** f))"));
-		assert_eq!(term("a ** b ** c - d ** e ** f"), term("(a ** b ** c) - (d ** e ** f)"));
-		assert_eq!(term("a ** (b ** c - d) ** e ** f"), term("a ** ((b ** c - d) ** (e ** f))"));
-		assert_eq!(term("a ** b ** (c - d) ** e ** f"), term("a ** (b ** ((c - d) ** (e ** f)))"));
-		assert_eq!(term("a ** b ** (c - d ** e) ** f"), term("a ** (b ** ((c - d ** e) ** f))"));
-		assert_eq!(term("a ** b ** c * d ** e ** f"), term("(a ** b ** c) * (d ** e ** f)"));
-		assert_eq!(term("a ** (b ** c * d) ** e ** f"), term("a ** ((b ** c * d) ** (e ** f))"));
-		assert_eq!(term("a ** b ** (c * d) ** e ** f"), term("a ** (b ** ((c * d) ** (e ** f)))"));
-		assert_eq!(term("a ** b ** (c * d ** e) ** f"), term("a ** (b ** ((c * d ** e) ** f))"));
-		assert_eq!(term("a ** b ** c / d ** e ** f"), term("(a ** b ** c) / (d ** e ** f)"));
-		assert_eq!(term("a ** (b ** c / d) ** e ** f"), term("a ** ((b ** c / d) ** (e ** f))"));
-		assert_eq!(term("a ** b ** (c / d) ** e ** f"), term("a ** (b ** ((c / d) ** (e ** f)))"));
-		assert_eq!(term("a ** b ** (c / d ** e) ** f"), term("a ** (b ** ((c / d ** e) ** f))"));
-		assert_eq!(term("a ** b ** c % d ** e ** f"), term("(a ** b ** c) % (d ** e ** f)"));
-		assert_eq!(term("a ** (b ** c % d) ** e ** f"), term("a ** ((b ** c % d) ** (e ** f))"));
-		assert_eq!(term("a ** b ** (c % d) ** e ** f"), term("a ** (b ** ((c % d) ** (e ** f)))"));
-		assert_eq!(term("a ** b ** (c % d ** e) ** f"), term("a ** (b ** ((c % d ** e) ** f))"));
-	}
-
-	#[test]
-	fn parse_bounds()
-	{
-		let term = |i| original::term(i, &Declarations::new()).unwrap().0;
-
-		assert_eq!(term("1 ** 2 ** 3, rest"), ", rest");
-		assert_eq!(term("1 * 2 * 3, rest"), ", rest");
-		assert_eq!(term("1 / 2 / 3, rest"), ", rest");
-		assert_eq!(term("1 % 2 % 3, rest"), ", rest");
-		assert_eq!(term("1 + 2 + 3, rest"), ", rest");
-		assert_eq!(term("1 - 2 - 3, rest"), ", rest");
-		assert_eq!(term("1, rest"), ", rest");
-		assert_eq!(term("-1, rest"), ", rest");
-		assert_eq!(term("--1, rest"), ", rest");
-		assert_eq!(term("|1|, rest"), ", rest");
-		assert_eq!(term("|1| + |-2|, rest"), ", rest");
-		assert_eq!(term("||-2||, rest"), ", rest");
-		assert_eq!(term("|-|-2||, rest"), ", rest");
-		assert_eq!(term("(1), rest"), ", rest");
-		assert_eq!(term("a, rest"), ", rest");
-		assert_eq!(term("1, rest"), ", rest");
-		assert_eq!(term("true, rest"), ", rest");
-		assert_eq!(term("false, rest"), ", rest");
-		assert_eq!(term("#inf, rest"), ", rest");
-		assert_eq!(term("#sup, rest"), ", rest");
-		assert_eq!(term("f(1, 2), rest"), ", rest");
-		assert_eq!(term("g(1 ** 2, 3 * 4, #inf), rest"), ", rest");
-		assert_eq!(term("\"test\", rest"), ", rest");
-		assert_eq!(term("X, rest"), ", rest");
-		assert_eq!(term("Variable, rest"), ", rest");
-		assert_eq!(term("f(\"test\", Variable), rest"), ", rest");
-	}
-
-	#[test]
-	fn parse_whitespace()
-	{
-		assert_eq!(format_term("(a+b)*(c+d)"), "(a + b) * (c + d)");
-		assert_eq!(format_term("( a + b ) * ( c + d )"), "(a + b) * (c + d)");
-		assert_eq!(format_term("(  a  +  b  )  *  (  c  +  d  )"), "(a + b) * (c + d)");
-		assert_eq!(format_term("(\ta\t+\tb\t)\t*\t(\tc\t+\td\t)"), "(a + b) * (c + d)");
-		assert_eq!(format_term("(\na\n+\nb\n)\n*\n(\nc\n+\nd\n)"), "(a + b) * (c + d)");
-		assert_eq!(format_term("( \t a \t + \t b \t ) \t * \t ( \t c \t + \t d \t )"), "(a + b) * (c + d)");
-		assert_eq!(format_term("( \n a \n + \n b \n ) \n * \n ( \n c \n + \n d \n )"), "(a + b) * (c + d)");
-		assert_eq!(format_term("f(\ta\t+\tb\t,\tc\t+\td\t)"), "f(a + b, c + d)");
-		assert_eq!(format_term("f(\na\n+\nb\n,\nc\n+\nd\n)"), "f(a + b, c + d)");
-		assert_eq!(format_term("f( \t a \t + \t b \t , \t c \t + \t d \t)"), "f(a + b, c + d)");
-		assert_eq!(format_term("f( \n a \n + \n b \n , \n c \n + \n d \n)"), "f(a + b, c + d)");
-		// TODO: test other operators
-	}
-
-	#[test]
-	fn parse_function_primitive()
-	{
-		let function = |i| original::function(i, &Declarations::new()).unwrap().1;
-		let function_remainder = |i| original::function(i, &Declarations::new()).unwrap().0;
-
-		assert_eq!(function("s").declaration.name, "s");
-		assert_eq!(function("s").declaration.arity, 0);
-		assert_eq!(function_remainder("s"), "");
-		assert_eq!(function("s ( )").declaration.name, "s");
-		assert_eq!(function("s ( )").declaration.arity, 0);
-		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(1), Term::integer(2));
-		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);
-		assert_eq!(function_remainder("s ( ), rest"), ", rest");
-		assert_eq!(function("s ( 1 , 2 , 3 ), rest").declaration.name, "s");
-		assert_eq!(function("s ( 1 , 2 , 3 ), rest").declaration.arity, 3);
-		assert_eq!(function_remainder("s ( 1 , 2 , 3 ), rest"), ", rest");
-	}
-
-	#[test]
-	fn parse_variable_declaration()
-	{
-		let variable_declaration = |i| original::variable_declaration(i).unwrap().1;
-		let variable_declaration_remainder = |i| original::variable_declaration(i).unwrap().0;
-
-		assert_eq!(variable_declaration("X Rest").name, "X");
-		assert_eq!(variable_declaration_remainder("X Rest"), " Rest");
-		assert_eq!(variable_declaration("X, Rest").name, "X");
-		assert_eq!(variable_declaration_remainder("X, Rest"), ", Rest");
-		// Variable declarations parsed at different locations should not be considered equal
-		assert_ne!(variable_declaration("X"), variable_declaration("X"));
-		assert_eq!(variable_declaration("Variable_123 Rest").name, "Variable_123");
-		assert_eq!(variable_declaration_remainder("Variable_123 Rest"), " Rest");
-
-		let variable_declaration = original::variable_declaration;
-
-		assert!(variable_declaration("0 Rest").is_err());
-		assert!(variable_declaration("123_Asd Rest").is_err());
-		assert!(variable_declaration("x Rest").is_err());
-		assert!(variable_declaration("variable_123 Rest").is_err());
-		assert!(variable_declaration("_ Rest").is_err());
-		assert!(variable_declaration("_variable_123 Rest").is_err());
-		assert!(variable_declaration(" ").is_err());
-	}
-
-	#[test]
-	fn parse_variable_primitive()
-	{
-		let variable = |i| original::variable(i, &Declarations::new()).unwrap().1;
-		let variable_remainder = |i| original::variable(i, &Declarations::new()).unwrap().0;
-
-		assert_eq!(variable("X Rest").declaration.name, "X");
-		assert_eq!(variable_remainder("X Rest"), " Rest");
-		assert_eq!(variable("X, Rest").declaration.name, "X");
-		assert_eq!(variable_remainder("X, Rest"), ", Rest");
-		assert_eq!(variable("Variable_123 Rest").declaration.name, "Variable_123");
-		assert_eq!(variable_remainder("Variable_123 Rest"), " Rest");
-
-		let variable = |i| original::variable(i, &Declarations::new());
-
-		assert!(variable("0 Rest").is_err());
-		assert!(variable("123_Asd Rest").is_err());
-		assert!(variable("x Rest").is_err());
-		assert!(variable("variable_123 Rest").is_err());
-		assert!(variable("_ Rest").is_err());
-		assert!(variable("_variable_123 Rest").is_err());
-		assert!(variable(" ").is_err());
-
-		let new_variable_declarations = |names: &[&str]| std::rc::Rc::new(names.iter()
-			.map(|name| std::rc::Rc::new(VariableDeclaration::new(name.to_string())))
-			.collect());
-
-		let layer_1 = new_variable_declarations(&["A", "B", "X"]);
-		let layer_2 = new_variable_declarations(&["C", "D", "X"]);
-		let layer_3 = new_variable_declarations(&["E", "F", "Y"]);
-		let layer_4 = new_variable_declarations(&["G", "H", "X"]);
-
-		let variable_declaration_stack = VariableDeclarationStack::new();
-
-		let mut declarations = Declarations::new();
-		declarations.variable_declaration_stack =
-			std::cell::RefCell::new(variable_declaration_stack);
-
-		let variable = |i| original::variable(i, &declarations).unwrap().1;
-		let number_of_free_variable_declarations =
-			|| declarations.variable_declaration_stack.borrow().free_variable_declarations.len();
-
-		let x1 = variable("X");
-		assert_eq!(number_of_free_variable_declarations(), 1);
-		let x2 = variable("X");
-		assert_eq!(number_of_free_variable_declarations(), 1);
-		assert_eq!(x1.declaration, x2.declaration);
-		let y1 = variable("Y");
-		assert_eq!(number_of_free_variable_declarations(), 2);
-		assert_ne!(x1.declaration, y1.declaration);
-		assert_ne!(x2.declaration, y1.declaration);
-
-		declarations.variable_declaration_stack.borrow_mut().push(layer_1);
-
-		let x3 = variable("X");
-		assert_eq!(number_of_free_variable_declarations(), 2);
-		assert_ne!(x1.declaration, x3.declaration);
-		let x4 = variable("X");
-		assert_eq!(number_of_free_variable_declarations(), 2);
-		assert_eq!(x3.declaration, x4.declaration);
-		let a1 = variable("A");
-		assert_eq!(number_of_free_variable_declarations(), 2);
-		assert_ne!(x3.declaration, a1.declaration);
-		let y2 = variable("Y");
-		assert_eq!(number_of_free_variable_declarations(), 2);
-		assert_eq!(y1.declaration, y2.declaration);
-
-		declarations.variable_declaration_stack.borrow_mut().push(layer_2);
-
-		let x5 = variable("X");
-		assert_eq!(number_of_free_variable_declarations(), 2);
-		assert_ne!(x1.declaration, x5.declaration);
-		assert_ne!(x3.declaration, x5.declaration);
-		let x6 = variable("X");
-		assert_eq!(number_of_free_variable_declarations(), 2);
-		assert_eq!(x5.declaration, x6.declaration);
-		let a2 = variable("A");
-		assert_eq!(number_of_free_variable_declarations(), 2);
-		assert_eq!(a1.declaration, a2.declaration);
-
-		declarations.variable_declaration_stack.borrow_mut().push(layer_3);
-
-		let x7 = variable("X");
-		assert_eq!(number_of_free_variable_declarations(), 2);
-		assert_eq!(x5.declaration, x7.declaration);
-		let y3 = variable("Y");
-		assert_eq!(number_of_free_variable_declarations(), 2);
-		assert_ne!(y2.declaration, y3.declaration);
-
-		declarations.variable_declaration_stack.borrow_mut().push(layer_4);
-
-		let x8 = variable("X");
-		assert_eq!(number_of_free_variable_declarations(), 2);
-		assert_ne!(x7.declaration, x8.declaration);
-		let y4 = variable("Y");
-		assert_eq!(number_of_free_variable_declarations(), 2);
-		assert_eq!(y3.declaration, y4.declaration);
-		let _ = variable("I");
-		assert_eq!(number_of_free_variable_declarations(), 3);
-	}
-}

src/utils.rs

@@ -1,72 +0,0 @@
-pub struct VariableDeclarationStack
-{
-	pub free_variable_declarations: crate::VariableDeclarations,
-	bound_variable_declaration_stack: Vec<std::rc::Rc<crate::VariableDeclarations>>,
-}
-
-impl VariableDeclarationStack
-{
-	pub fn new() -> Self
-	{
-		Self
-		{
-			free_variable_declarations: crate::VariableDeclarations::new(),
-			bound_variable_declaration_stack: vec![],
-		}
-	}
-
-	pub fn find(&self, variable_name: &str) -> Option<std::rc::Rc<crate::VariableDeclaration>>
-	{
-		for variable_declarations in self.bound_variable_declaration_stack.iter().rev()
-		{
-			if let Some(variable_declaration) = variable_declarations.iter()
-				.find(|x| x.name == variable_name)
-			{
-				return Some(std::rc::Rc::clone(&variable_declaration));
-			}
-		}
-
-		if let Some(variable_declaration) = self.free_variable_declarations.iter()
-			.find(|x| x.name == variable_name)
-		{
-			return Some(std::rc::Rc::clone(&variable_declaration));
-		}
-
-		None
-	}
-
-	pub fn find_or_create(&mut self, variable_name: &str) -> std::rc::Rc<crate::VariableDeclaration>
-	{
-		if let Some(variable_declaration) = self.find(variable_name)
-		{
-			return variable_declaration;
-		}
-
-		let variable_declaration = crate::VariableDeclaration
-		{
-			name: variable_name.to_owned(),
-		};
-		let variable_declaration = std::rc::Rc::new(variable_declaration);
-
-		self.free_variable_declarations.push(std::rc::Rc::clone(&variable_declaration));
-
-		variable_declaration
-	}
-
-	pub fn is_empty(&self) -> bool
-	{
-		self.free_variable_declarations.is_empty()
-			&& self.bound_variable_declaration_stack.is_empty()
-	}
-
-	pub fn push(&mut self, bound_variable_declarations: std::rc::Rc<crate::VariableDeclarations>)
-	{
-		self.bound_variable_declaration_stack.push(bound_variable_declarations);
-	}
-
-	pub fn pop(&mut self) -> Result<(), crate::Error>
-	{
-		self.bound_variable_declaration_stack.pop().map(|_| ())
-			.ok_or_else(|| crate::Error::new_logic("variable stack not in expected state"))
-	}
-}