Remove redundant indirection

Cargo.toml

@@ -11,3 +11,10 @@ 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,6 @@
 // Operators
 
-#[derive(Clone, Copy, Eq, PartialEq)]
+#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub enum BinaryOperator
 {
 	Add,
@@ -11,7 +11,7 @@ pub enum BinaryOperator
 	Exponentiate,
 }
 
-#[derive(Clone, Copy, Eq, PartialEq)]
+#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub enum ComparisonOperator
 {
 	Greater,
@@ -22,13 +22,22 @@ pub enum ComparisonOperator
 	Equal,
 }
 
-#[derive(Clone, Copy, Eq, PartialEq)]
+#[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)]
@@ -118,6 +127,17 @@ 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
@@ -133,6 +153,7 @@ pub type VariableDeclarations = Vec<std::rc::Rc<VariableDeclaration>>;
 
 // Terms
 
+#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct BinaryOperation
 {
 	pub operator: BinaryOperator,
@@ -153,34 +174,36 @@ impl BinaryOperation
 	}
 }
 
+#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct Function
 {
 	pub declaration: std::rc::Rc<FunctionDeclaration>,
-	pub arguments: Vec<Box<Term>>,
+	pub arguments: Terms,
 }
 
 impl Function
 {
-	pub fn new(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
+	pub fn new(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Terms) -> Self
 	{
 		assert_eq!(declaration.arity, arguments.len(),
 			"function has a different number of arguments then declared");
 
 		Self
 		{
-			declaration: std::rc::Rc::clone(declaration),
+			declaration,
 			arguments,
 		}
 	}
 }
 
-#[derive(Clone, Copy, Eq, PartialEq)]
+#[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,
@@ -199,6 +222,7 @@ impl UnaryOperation
 	}
 }
 
+#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct Variable
 {
 	pub declaration: std::rc::Rc<VariableDeclaration>,
@@ -206,17 +230,18 @@ 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: std::rc::Rc::clone(declaration),
+			declaration,
 		}
 	}
 }
 
 // Formulas
 
+#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct Compare
 {
 	pub operator: ComparisonOperator,
@@ -237,13 +262,14 @@ impl Compare
 	}
 }
 
-pub struct Exists
+#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
+pub struct QuantifiedFormula
 {
 	pub parameters: std::rc::Rc<VariableDeclarations>,
 	pub argument: Box<Formula>,
 }
 
-impl Exists
+impl QuantifiedFormula
 {
 	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
 	{
@@ -255,76 +281,45 @@ impl Exists
 	}
 }
 
-pub struct ForAll
-{
-	pub parameters: std::rc::Rc<VariableDeclarations>,
-	pub argument: Box<Formula>,
-}
-
-impl ForAll
-{
-	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
-	{
-		Self
-		{
-			parameters,
-			argument,
-		}
-	}
-}
-
-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,
-		}
-	}
-}
-
+#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct Implies
 {
+	pub direction: ImplicationDirection,
 	pub antecedent: Box<Formula>,
 	pub implication: Box<Formula>,
 }
 
 impl Implies
 {
-	pub fn new(antecedent: Box<Formula>, implication: Box<Formula>) -> Self
+	pub fn new(direction: ImplicationDirection, 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>,
-	pub arguments: Vec<Box<Term>>,
+	pub arguments: Terms,
 }
 
 impl Predicate
 {
-	pub fn new(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
+	pub fn new(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Terms) -> Self
 	{
 		assert_eq!(declaration.arity, arguments.len(),
 			"predicate has a different number of arguments then declared");
 
 		Self
 		{
-			declaration: std::rc::Rc::clone(declaration),
+			declaration,
 			arguments,
 		}
 	}
@@ -332,6 +327,7 @@ impl Predicate
 
 // Variants
 
+#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub enum Term
 {
 	BinaryOperation(BinaryOperation),
@@ -344,7 +340,7 @@ pub enum Term
 	Variable(Variable),
 }
 
-pub type Terms = Vec<Box<Term>>;
+pub type Terms = Vec<Term>;
 
 impl Term
 {
@@ -383,8 +379,7 @@ 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: Terms) -> Self
 	{
 		Self::Function(Function::new(declaration, arguments))
 	}
@@ -444,34 +439,33 @@ 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),
 	Boolean(bool),
 	Compare(Compare),
-	Exists(Exists),
-	ForAll(ForAll),
-	IfAndOnlyIf(IfAndOnlyIf),
+	Exists(QuantifiedFormula),
+	ForAll(QuantifiedFormula),
+	IfAndOnlyIf(Formulas),
 	Implies(Implies),
 	Not(Box<Formula>),
 	Or(Formulas),
 	Predicate(Predicate),
 }
 
-pub type Formulas = Vec<Box<Formula>>;
+pub type Formulas = Vec<Formula>;
 
 impl Formula
 {
 	pub fn and(arguments: Formulas) -> Self
 	{
-		assert!(!arguments.is_empty());
-
 		Self::And(arguments)
 	}
 
@@ -487,9 +481,7 @@ impl Formula
 
 	pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
 	{
-		assert!(!parameters.is_empty());
-
-		Self::Exists(Exists::new(parameters, argument))
+		Self::Exists(QuantifiedFormula::new(parameters, argument))
 	}
 
 	pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
@@ -504,9 +496,7 @@ 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))
+		Self::ForAll(QuantifiedFormula::new(parameters, argument))
 	}
 
 	pub fn greater(left: Box<Term>, right: Box<Term>) -> Self
@@ -519,14 +509,15 @@ impl Formula
 		Self::compare(ComparisonOperator::GreaterOrEqual, left, right)
 	}
 
-	pub fn if_and_only_if(left: Box<Formula>, right: Box<Formula>) -> Self
+	pub fn if_and_only_if(arguments: Formulas) -> Self
 	{
-		Self::IfAndOnlyIf(IfAndOnlyIf::new(left, right))
+		Self::IfAndOnlyIf(arguments)
 	}
 
-	pub fn implies(antecedent: Box<Formula>, consequent: Box<Formula>) -> Self
+	pub fn implies(direction: ImplicationDirection, antecedent: Box<Formula>,
+		consequent: Box<Formula>) -> Self
 	{
-		Self::Implies(Implies::new(antecedent, consequent))
+		Self::Implies(Implies::new(direction, antecedent, consequent))
 	}
 
 	pub fn less(left: Box<Term>, right: Box<Term>) -> Self
@@ -551,13 +542,10 @@ 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>>)
-		-> Self
+	pub fn predicate(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Terms) -> Self
 	{
 		Self::Predicate(Predicate::new(declaration, arguments))
 	}

src/error.rs

@@ -0,0 +1,69 @@
+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,493 +1,2 @@
-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(_)
-			| Self::UnaryOperation(
-				crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
-				=> 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,
-		}
-	}
-}
-
-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
-		{
-			Self::Infimum => write!(format, "#inf"),
-			Self::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,
-		};
-
-		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(binary_operation) =>
-			{
-				let operator_string = match binary_operation.operator
-				{
-					crate::BinaryOperator::Add => "+",
-					crate::BinaryOperator::Subtract => "-",
-					crate::BinaryOperator::Multiply => "*",
-					crate::BinaryOperator::Divide => "/",
-					crate::BinaryOperator::Modulo => "%",
-					crate::BinaryOperator::Exponentiate => "**",
-				};
-
-				let left_requires_parentheses = binary_operation.left.precedence() == precedence
-					// Exponentiation is right-associative and thus requires parentheses when
-					// nested on the left side
-					&& binary_operation.operator == crate::BinaryOperator::Exponentiate;
-
-				// The subtraction, division, and modulo operators require parentheses around the
-				// right argument even if it has the same precedence
-				let operator_requires_right_priority = match binary_operation.operator
-				{
-					crate::BinaryOperator::Subtract
-					| crate::BinaryOperator::Divide
-					| crate::BinaryOperator::Modulo
-						=> true,
-					_ => false,
-				};
-
-				// Additionally, modulo operations nested to the right of another multiplicative
-				// operation always require parentheses
-				let right_requires_priority = match *binary_operation.right
-				{
-					crate::Term::BinaryOperation(
-						crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
-						=> true,
-					_ => false,
-				};
-
-				let right_requires_parentheses = binary_operation.right.precedence() == precedence
-					&& (operator_requires_right_priority || right_requires_priority);
-
-				if left_requires_parentheses
-				{
-					write!(format, "(")?;
-				}
-
-				write!(format, "{:?}", display_term(&binary_operation.left, Some(precedence)))?;
-
-				if left_requires_parentheses
-				{
-					write!(format, ")")?;
-				}
-
-				write!(format, " {} ", operator_string)?;
-
-				if right_requires_parentheses
-				{
-					write!(format, "(")?;
-				}
-
-				write!(format, "{:?}", display_term(&binary_operation.right, Some(precedence)))?;
-
-				if right_requires_parentheses
-				{
-					write!(format, ")")?;
-				}
-
-				Ok(())
-			},
-			crate::Term::UnaryOperation(
-				crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
-				=> write!(format, "-{:?}", display_term(argument, Some(precedence))),
-			crate::Term::UnaryOperation(
-				crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
-				=> write!(format, "|{:?}|", display_term(argument, None)),
-		}?;
-
-		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))
-	}
-}
+mod formulas;
+mod terms;

src/lib.rs

@@ -1,4 +1,10 @@
 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

@@ -0,0 +1,32 @@
+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

@@ -0,0 +1,683 @@
+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, crate::Formulas>
+{
+	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().collect())
+			}
+			else
+			{
+				Err(nom::error::make_error(i, nom::error::ErrorKind::Many1))
+			}
+		}
+	)(i)
+}
+
+fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formulas>
+{
+	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().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, crate::Formulas>
+{
+	map_res
+	(
+		separated_list
+		(
+			delimited
+			(
+				multispace0,
+				tag("<->"),
+				multispace0,
+			),
+			|i| formula_precedence_5(i, d),
+		),
+		|arguments| -> Result<_, (_, _)>
+		{
+			if arguments.len() >= 2
+			{
+				Ok(arguments.into_iter().collect())
+			}
+			else
+			{
+				Err(nom::error::make_error(i, nom::error::ErrorKind::Many1))
+			}
+		}
+	)(i)
+}
+
+fn quantified_formula<'a, 'b>(i: &'a str, d: &Declarations, keyword: &'b str)
+	-> IResult<&'a str, crate::QuantifiedFormula>
+{
+	preceded
+	(
+		terminated
+		(
+			tag(keyword),
+			word_boundary,
+		),
+		cut
+		(
+			|i|
+			{
+				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, crate::QuantifiedFormula::new(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::QuantifiedFormula>
+{
+	quantified_formula(i, d, "exists")
+}
+
+fn for_all<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::QuantifiedFormula>
+{
+	quantified_formula(i, d, "forall")
+}
+
+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

@@ -0,0 +1,86 @@
+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

@@ -0,0 +1,249 @@
+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

@@ -0,0 +1,159 @@
+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

@@ -0,0 +1,852 @@
+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<crate::Terms>)>
+{
+	pair
+	(
+		function_or_predicate_name,
+		opt
+		(
+			delimited
+			(
+				delimited
+				(
+					multispace0,
+					tag("("),
+					multispace0,
+				),
+				separated_list
+				(
+					delimited
+					(
+						multispace0,
+						tag(","),
+						multispace0,
+					),
+					|i| term(i, d),
+				),
+				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

@@ -0,0 +1,72 @@
+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"))
+	}
+}