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,6 +11,3 @@ keywords = ["logic"]
 categories = ["data-structures", "science"]
 license = "MIT"
 edition = "2018"
-
-[dependencies]
-log = "0.4"

src/ast.rs

@@ -1,8 +1,5 @@
-use crate::flavor::{FunctionDeclaration as _, PredicateDeclaration as _};
-
 // Operators
 
-#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub enum BinaryOperator
 {
 	Add,
@@ -13,7 +10,6 @@ pub enum BinaryOperator
 	Exponentiate,
 }
 
-#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub enum ComparisonOperator
 {
 	Greater,
@@ -24,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)]
@@ -61,8 +47,7 @@ impl FunctionDeclaration
 	}
 }
 
-pub type FunctionDeclarations<F> =
-	std::collections::BTreeSet<std::rc::Rc<<F as crate::flavor::Flavor>::FunctionDeclaration>>;
+pub type FunctionDeclarations = std::collections::BTreeSet<std::rc::Rc<FunctionDeclaration>>;
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct PredicateDeclaration
@@ -83,8 +68,7 @@ impl PredicateDeclaration
 	}
 }
 
-pub type PredicateDeclarations<F> =
-	std::collections::BTreeSet<std::rc::Rc<<F as crate::flavor::Flavor>::PredicateDeclaration>>;
+pub type PredicateDeclarations = std::collections::BTreeSet<std::rc::Rc<PredicateDeclaration>>;
 
 pub struct VariableDeclaration
 {
@@ -94,10 +78,10 @@ pub struct VariableDeclaration
 impl std::cmp::PartialEq for VariableDeclaration
 {
 	#[inline(always)]
-	fn eq(&self, other: &Self) -> bool
+	fn eq(&self, other: &VariableDeclaration) -> bool
 	{
-		let l = self as *const Self;
-		let r = other as *const Self;
+		let l = self as *const VariableDeclaration;
+		let r = other as *const VariableDeclaration;
 
 		l.eq(&r)
 	}
@@ -131,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,26 +126,20 @@ impl VariableDeclaration
 	}
 }
 
-pub type VariableDeclarations<F> =
-	Vec<std::rc::Rc<<F as crate::flavor::Flavor>::VariableDeclaration>>;
+pub type VariableDeclarations = Vec<std::rc::Rc<VariableDeclaration>>;
 
 // Terms
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct BinaryOperation<F>
-where
-	F: crate::flavor::Flavor,
+pub struct BinaryOperation
 {
 	pub operator: BinaryOperator,
-	pub left: Box<Term<F>>,
-	pub right: Box<Term<F>>,
+	pub left: Box<Term>,
+	pub right: Box<Term>,
 }
 
-impl<F> BinaryOperation<F>
-where
-	F: crate::flavor::Flavor,
+impl BinaryOperation
 {
-	pub fn new(operator: BinaryOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn new(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self
 		{
@@ -183,53 +150,42 @@ where
 	}
 }
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct Function<F>
-where
-	F: crate::flavor::Flavor,
+pub struct Function
 {
-	pub declaration: std::rc::Rc<F::FunctionDeclaration>,
-	pub arguments: Terms<F>,
+	pub declaration: std::rc::Rc<FunctionDeclaration>,
+	pub arguments: Vec<Box<Term>>,
 }
 
-impl<F> Function<F>
-where
-	F: crate::flavor::Flavor,
+impl Function
 {
-	pub fn new(declaration: std::rc::Rc<F::FunctionDeclaration>, arguments: Terms<F>) -> 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 than declared");
+		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<F>
-where
-	F: crate::flavor::Flavor,
+pub struct UnaryOperation
 {
 	pub operator: UnaryOperator,
-	pub argument: Box<Term<F>>,
+	pub argument: Box<Term>,
 }
 
-impl<F> UnaryOperation<F>
-where
-	F: crate::flavor::Flavor,
+impl UnaryOperation
 {
-	pub fn new(operator: UnaryOperator, argument: Box<Term<F>>) -> Self
+	pub fn new(operator: UnaryOperator, argument: Box<Term>) -> Self
 	{
 		Self
 		{
@@ -239,44 +195,34 @@ where
 	}
 }
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct Variable<F>
-where
-	F: crate::flavor::Flavor,
+pub struct Variable
 {
-	pub declaration: std::rc::Rc<F::VariableDeclaration>,
+	pub declaration: std::rc::Rc<VariableDeclaration>,
 }
 
-impl<F> Variable<F>
-where
-	F: crate::flavor::Flavor,
+impl Variable
 {
-	pub fn new(declaration: std::rc::Rc<F::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<F>
-where
-	F: crate::flavor::Flavor,
+pub struct Compare
 {
 	pub operator: ComparisonOperator,
-	pub left: Box<Term<F>>,
-	pub right: Box<Term<F>>,
+	pub left: Box<Term>,
+	pub right: Box<Term>,
 }
 
-impl<F> Compare<F>
-where
-	F: crate::flavor::Flavor,
+impl Compare
 {
-	pub fn new(operator: ComparisonOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn new(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self
 		{
@@ -287,20 +233,15 @@ where
 	}
 }
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct QuantifiedFormula<F>
-where
-	F: crate::flavor::Flavor,
+pub struct Exists
 {
-	pub parameters: std::rc::Rc<VariableDeclarations<F>>,
-	pub argument: Box<Formula<F>>,
+	pub parameters: std::rc::Rc<VariableDeclarations>,
+	pub argument: Box<Formula>,
 }
 
-impl<F> QuantifiedFormula<F>
-where
-	F: crate::flavor::Flavor,
+impl Exists
 {
-	pub fn new(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
+	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
 	{
 		Self
 		{
@@ -310,54 +251,76 @@ where
 	}
 }
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct Implies<F>
-where
-	F: crate::flavor::Flavor,
+pub struct ForAll
 {
-	pub direction: ImplicationDirection,
-	pub antecedent: Box<Formula<F>>,
-	pub implication: Box<Formula<F>>,
+	pub parameters: std::rc::Rc<VariableDeclarations>,
+	pub argument: Box<Formula>,
 }
 
-impl<F> Implies<F>
-where
-	F: crate::flavor::Flavor,
+impl ForAll
 {
-	pub fn new(direction: ImplicationDirection, antecedent: Box<Formula<F>>,
-		implication: Box<Formula<F>>)
-		-> Self
+	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,
+		}
+	}
+}
+
+pub struct Implies
+{
+	pub antecedent: Box<Formula>,
+	pub implication: Box<Formula>,
+}
+
+impl Implies
+{
+	pub fn new(antecedent: Box<Formula>, implication: Box<Formula>) -> Self
 	{
 		Self
 		{
-			direction,
 			antecedent,
 			implication,
 		}
 	}
 }
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct Predicate<F>
-where
-	F: crate::flavor::Flavor,
+pub struct Predicate
 {
-	pub declaration: std::rc::Rc<F::PredicateDeclaration>,
-	pub arguments: Terms<F>,
+	pub declaration: std::rc::Rc<PredicateDeclaration>,
+	pub arguments: Vec<Box<Term>>,
 }
 
-impl<F> Predicate<F>
-where
-	F: crate::flavor::Flavor,
+impl Predicate
 {
-	pub fn new(declaration: std::rc::Rc<F::PredicateDeclaration>, arguments: Terms<F>) -> 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 than declared");
+		assert_eq!(declaration.arity, arguments.len(),
+			"predicate has a different number of arguments then declared");
 
 		Self
 		{
-			declaration,
+			declaration: std::rc::Rc::clone(declaration),
 			arguments,
 		}
 	}
@@ -365,38 +328,33 @@ where
 
 // Variants
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub enum Term<F>
-where
-	F: crate::flavor::Flavor,
+pub enum Term
 {
-	BinaryOperation(BinaryOperation<F>),
+	BinaryOperation(BinaryOperation),
 	Boolean(bool),
-	Function(Function<F>),
+	Function(Function),
 	Integer(i32),
 	SpecialInteger(SpecialInteger),
 	String(String),
-	UnaryOperation(UnaryOperation<F>),
-	Variable(Variable<F>),
+	UnaryOperation(UnaryOperation),
+	Variable(Variable),
 }
 
-pub type Terms<F> = Vec<Term<F>>;
+pub type Terms = Vec<Box<Term>>;
 
-impl<F> Term<F>
-where
-	F: crate::flavor::Flavor,
+impl Term
 {
-	pub fn absolute_value(argument: Box<Term<F>>) -> Self
+	pub fn absolute_value(argument: Box<Term>) -> Self
 	{
 		Self::unary_operation(UnaryOperator::AbsoluteValue, argument)
 	}
 
-	pub fn add(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn add(left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self::binary_operation(BinaryOperator::Add, left, right)
 	}
 
-	pub fn binary_operation(operator: BinaryOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn binary_operation(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self::BinaryOperation(BinaryOperation::new(operator, left, right))
 	}
@@ -406,12 +364,12 @@ where
 		Self::Boolean(value)
 	}
 
-	pub fn divide(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn divide(left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self::binary_operation(BinaryOperator::Divide, left, right)
 	}
 
-	pub fn exponentiate(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn exponentiate(left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self::binary_operation(BinaryOperator::Exponentiate, left, right)
 	}
@@ -421,7 +379,8 @@ where
 		Self::boolean(false)
 	}
 
-	pub fn function(declaration: std::rc::Rc<F::FunctionDeclaration>, arguments: Terms<F>) -> Self
+	pub fn function(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>)
+		-> Self
 	{
 		Self::Function(Function::new(declaration, arguments))
 	}
@@ -436,17 +395,17 @@ where
 		Self::Integer(value)
 	}
 
-	pub fn modulo(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn modulo(left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self::binary_operation(BinaryOperator::Modulo, left, right)
 	}
 
-	pub fn multiply(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn multiply(left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self::binary_operation(BinaryOperator::Multiply, left, right)
 	}
 
-	pub fn negative(argument: Box<Term<F>>) -> Self
+	pub fn negative(argument: Box<Term>) -> Self
 	{
 		Self::unary_operation(UnaryOperator::Negative, argument)
 	}
@@ -461,7 +420,7 @@ where
 		Self::String(value)
 	}
 
-	pub fn subtract(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn subtract(left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self::binary_operation(BinaryOperator::Subtract, left, right)
 	}
@@ -476,42 +435,39 @@ where
 		Self::boolean(true)
 	}
 
-	pub fn unary_operation(operator: UnaryOperator, argument: Box<Term<F>>) -> Self
+	pub fn unary_operation(operator: UnaryOperator, argument: Box<Term>) -> Self
 	{
 		Self::UnaryOperation(UnaryOperation::new(operator, argument))
 	}
 
-	pub fn variable(declaration: std::rc::Rc<F::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<F>
-where
-	F: crate::flavor::Flavor,
+pub enum Formula
 {
-	And(Formulas<F>),
+	And(Formulas),
 	Boolean(bool),
-	Compare(Compare<F>),
-	Exists(QuantifiedFormula<F>),
-	ForAll(QuantifiedFormula<F>),
-	IfAndOnlyIf(Formulas<F>),
-	Implies(Implies<F>),
-	Not(Box<Formula<F>>),
-	Or(Formulas<F>),
-	Predicate(Predicate<F>),
+	Compare(Compare),
+	Exists(Exists),
+	ForAll(ForAll),
+	IfAndOnlyIf(IfAndOnlyIf),
+	Implies(Implies),
+	Not(Box<Formula>),
+	Or(Formulas),
+	Predicate(Predicate),
 }
 
-pub type Formulas<F> = Vec<Formula<F>>;
+pub type Formulas = Vec<Box<Formula>>;
 
-impl<F> Formula<F>
-where
-	F: crate::flavor::Flavor,
+impl Formula
 {
-	pub fn and(arguments: Formulas<F>) -> Self
+	pub fn and(arguments: Formulas) -> Self
 	{
+		assert!(!arguments.is_empty());
+
 		Self::And(arguments)
 	}
 
@@ -520,17 +476,19 @@ where
 		Self::Boolean(value)
 	}
 
-	pub fn compare(operator: ComparisonOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn compare(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self::Compare(Compare::new(operator, left, right))
 	}
 
-	pub fn exists(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
+	pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
 	{
-		Self::Exists(QuantifiedFormula::new(parameters, argument))
+		assert!(!parameters.is_empty());
+
+		Self::Exists(Exists::new(parameters, argument))
 	}
 
-	pub fn equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self::compare(ComparisonOperator::Equal, left, right)
 	}
@@ -540,58 +498,62 @@ where
 		Self::boolean(false)
 	}
 
-	pub fn for_all(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
+	pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
 	{
-		Self::ForAll(QuantifiedFormula::new(parameters, argument))
+		assert!(!parameters.is_empty());
+
+		Self::ForAll(ForAll::new(parameters, argument))
 	}
 
-	pub fn greater(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn greater(left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self::compare(ComparisonOperator::Greater, left, right)
 	}
 
-	pub fn greater_or_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn greater_or_equal(left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self::compare(ComparisonOperator::GreaterOrEqual, left, right)
 	}
 
-	pub fn if_and_only_if(arguments: Formulas<F>) -> 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<F>>,
-		consequent: Box<Formula<F>>) -> 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<F>>, right: Box<Term<F>>) -> Self
+	pub fn less(left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self::compare(ComparisonOperator::Less, left, right)
 	}
 
-	pub fn less_or_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn less_or_equal(left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self::compare(ComparisonOperator::LessOrEqual, left, right)
 	}
 
-	pub fn not(argument: Box<Formula<F>>) -> Self
+	pub fn not(argument: Box<Formula>) -> Self
 	{
 		Self::Not(argument)
 	}
 
-	pub fn not_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
+	pub fn not_equal(left: Box<Term>, right: Box<Term>) -> Self
 	{
 		Self::compare(ComparisonOperator::NotEqual, left, right)
 	}
 
-	pub fn or(arguments: Formulas<F>) -> Self
+	pub fn or(arguments: Formulas) -> Self
 	{
+		assert!(!arguments.is_empty());
+
 		Self::Or(arguments)
 	}
 
-	pub fn predicate(declaration: std::rc::Rc<F::PredicateDeclaration>, arguments: Terms<F>) -> Self
+	pub fn predicate(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>)
+		-> Self
 	{
 		Self::Predicate(Predicate::new(declaration, arguments))
 	}
@@ -601,11 +563,3 @@ where
 		Self::boolean(true)
 	}
 }
-
-pub struct OpenFormula<F>
-where
-	F: crate::flavor::Flavor,
-{
-	pub free_variable_declarations: std::rc::Rc<VariableDeclarations<F>>,
-	pub formula: Formula<F>,
-}

src/flavor.rs

@@ -1,85 +0,0 @@
-pub trait FunctionDeclaration
-{
-	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
-	fn arity(&self) -> usize;
-	fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool;
-}
-
-impl FunctionDeclaration for crate::FunctionDeclaration
-{
-	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(formatter, "{}", self.name)
-	}
-
-	fn arity(&self) -> usize
-	{
-		self.arity
-	}
-
-	fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool
-	{
-		self.name == other_name && self.arity == other_arity
-	}
-}
-
-pub trait PredicateDeclaration
-{
-	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
-	fn arity(&self) -> usize;
-	fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool;
-}
-
-impl PredicateDeclaration for crate::PredicateDeclaration
-{
-	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(formatter, "{}", self.name)
-	}
-
-	fn arity(&self) -> usize
-	{
-		self.arity
-	}
-
-	fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool
-	{
-		self.name == other_name && self.arity == other_arity
-	}
-}
-
-pub trait VariableDeclaration
-{
-	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
-	fn matches_name(&self, other_name: &str) -> bool;
-}
-
-impl VariableDeclaration for crate::VariableDeclaration
-{
-	fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(formatter, "{}", self.name)
-	}
-
-	fn matches_name(&self, other_name: &str) -> bool
-	{
-		self.name == other_name
-	}
-}
-
-pub trait Flavor
-{
-	type FunctionDeclaration: FunctionDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
-	type PredicateDeclaration:
-		PredicateDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
-	type VariableDeclaration: VariableDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
-}
-
-pub struct DefaultFlavor;
-
-impl Flavor for DefaultFlavor
-{
-	type FunctionDeclaration = crate::FunctionDeclaration;
-	type PredicateDeclaration = crate::PredicateDeclaration;
-	type VariableDeclaration = crate::VariableDeclaration;
-}

src/format.rs

@@ -1,2 +1,450 @@
-pub mod formulas;
-pub 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,11 +1,4 @@
 mod ast;
-pub mod flavor;
-mod format;
-mod parse;
-mod utils;
+pub mod format;
 
 pub use ast::*;
-pub use format::{formulas::FormulaDisplay, terms::TermDisplay};
-pub use flavor::{DefaultFlavor, Flavor};
-pub use utils::*;
-pub use parse::{DefaultParser, Parser};

src/parse.rs

@@ -1,142 +0,0 @@
-pub mod error;
-pub mod formulas;
-pub mod terms;
-pub mod tokens;
-
-pub use error::Error;
-
-use crate::flavor::{FunctionDeclaration as _, PredicateDeclaration as _, VariableDeclaration as _};
-
-pub trait Parser: Sized
-{
-	type Flavor: crate::flavor::Flavor;
-
-	fn find_or_create_function_declaration(&self, name: &str, arity: usize)
-		-> std::rc::Rc<<Self::Flavor as crate::flavor::Flavor>::FunctionDeclaration>;
-
-	fn find_or_create_predicate_declaration(&self, name: &str, arity: usize)
-		-> std::rc::Rc<<Self::Flavor as crate::flavor::Flavor>::PredicateDeclaration>;
-
-	fn new_variable_declaration(name: String)
-		-> <Self::Flavor as crate::flavor::Flavor>::VariableDeclaration;
-
-	fn find_or_create_variable_declaration(
-		variable_declaration_stack_layer: &crate::VariableDeclarationStackLayer<Self::Flavor>,
-		variable_name: &str)
-		-> std::rc::Rc<<Self::Flavor as crate::flavor::Flavor>::VariableDeclaration>
-	{
-		match variable_declaration_stack_layer
-		{
-			crate::VariableDeclarationStackLayer::Free(free_variable_declarations) =>
-			{
-				if let Some(variable_declaration) = free_variable_declarations.borrow().iter()
-					.find(|x| x.matches_name(variable_name))
-				{
-					return std::rc::Rc::clone(&variable_declaration);
-				}
-
-				let variable_declaration = Self::new_variable_declaration(variable_name.to_owned());
-				let variable_declaration = std::rc::Rc::new(variable_declaration);
-
-				free_variable_declarations.borrow_mut()
-					.push(std::rc::Rc::clone(&variable_declaration));
-
-				variable_declaration
-			},
-			crate::VariableDeclarationStackLayer::Bound(bound_variable_declarations) =>
-			{
-				if let Some(variable_declaration) = bound_variable_declarations
-					.variable_declarations.iter()
-					.find(|x| x.matches_name(variable_name))
-				{
-					return std::rc::Rc::clone(&variable_declaration);
-				}
-
-				Self::find_or_create_variable_declaration(bound_variable_declarations.parent,
-					variable_name)
-			},
-		}
-	}
-
-	fn parse_formula(&self, input: &str)
-		-> Result<crate::OpenFormula<Self::Flavor>, crate::parse::Error>
-	{
-		formulas::formula(input, self)
-	}
-}
-
-pub struct DefaultParser
-{
-	function_declarations:
-		std::cell::RefCell<crate::FunctionDeclarations<<Self as Parser>::Flavor>>,
-	predicate_declarations:
-		std::cell::RefCell<crate::PredicateDeclarations<<Self as Parser>::Flavor>>,
-}
-
-impl DefaultParser
-{
-	pub fn new() -> Self
-	{
-		Self
-		{
-			function_declarations: std::cell::RefCell::new(
-				crate::FunctionDeclarations::<<Self as Parser>::Flavor>::new()),
-			predicate_declarations: std::cell::RefCell::new(
-				crate::PredicateDeclarations::<<Self as Parser>::Flavor>::new()),
-		}
-	}
-}
-
-impl Parser for DefaultParser
-{
-	type Flavor = crate::flavor::DefaultFlavor;
-
-	fn new_variable_declaration(name: String)
-		-> <Self::Flavor as crate::flavor::Flavor>::VariableDeclaration
-	{
-		crate::VariableDeclaration
-		{
-			name,
-		}
-	}
-
-	fn find_or_create_function_declaration(&self, name: &str, arity: usize)
-		-> std::rc::Rc<<Self::Flavor as crate::flavor::Flavor>::FunctionDeclaration>
-	{
-		let mut function_declarations = self.function_declarations.borrow_mut();
-
-		match function_declarations.iter().find(|x| x.matches_signature(name, arity))
-		{
-			Some(declaration) => std::rc::Rc::clone(&declaration),
-			None =>
-			{
-				let declaration = crate::FunctionDeclaration::new(name.to_string(), arity);
-				let declaration = std::rc::Rc::new(declaration);
-
-				function_declarations.insert(std::rc::Rc::clone(&declaration));
-
-				declaration
-			},
-		}
-	}
-
-	fn find_or_create_predicate_declaration(&self, name: &str, arity: usize)
-		-> std::rc::Rc<<Self::Flavor as crate::flavor::Flavor>::PredicateDeclaration>
-	{
-		let mut predicate_declarations = self.predicate_declarations.borrow_mut();
-
-		match predicate_declarations.iter().find(|x| x.matches_signature(name, arity))
-		{
-			Some(declaration) => std::rc::Rc::clone(&declaration),
-			None =>
-			{
-				let declaration = crate::PredicateDeclaration::new(name.to_string(), arity);
-				let declaration = std::rc::Rc::new(declaration);
-
-				predicate_declarations.insert(std::rc::Rc::clone(&declaration));
-
-				declaration
-			},
-		}
-	}
-}

src/parse/error.rs

@@ -1,182 +0,0 @@
-pub type Source = Box<dyn std::error::Error>;
-
-pub struct Location
-{
-	start: usize,
-	end: Option<usize>,
-}
-
-impl Location
-{
-	pub fn new(start: usize, end: Option<usize>) -> Self
-	{
-		Self
-		{
-			start,
-			end,
-		}
-	}
-}
-
-pub enum Kind
-{
-	UnmatchedParenthesis,
-	CharacterNotAllowed(char),
-	ParseNumber(String),
-	MixedImplicationDirections(Location),
-	ExpectedVariableDeclaration,
-	UnexpectedToken,
-	EmptyExpression,
-	ExpectedLogicalConnectiveArgument(String),
-	ExpectedTerm,
-	MultipleComparisonOperators(crate::ComparisonOperator, crate::ComparisonOperator),
-}
-
-pub struct Error
-{
-	pub kind: Kind,
-	pub location: Location,
-	pub source: Option<Source>,
-}
-
-impl Error
-{
-	pub(crate) fn new(kind: Kind, location: Location) -> Self
-	{
-		Self
-		{
-			kind,
-			location,
-			source: None,
-		}
-	}
-
-	pub(crate) fn with<S: Into<Source>>(mut self, source: S) -> Self
-	{
-		self.source = Some(source.into());
-		self
-	}
-
-	pub(crate) fn new_unmatched_parenthesis(location: Location) -> Self
-	{
-		Self::new(Kind::UnmatchedParenthesis, location)
-	}
-
-	pub(crate) fn new_character_not_allowed(character: char, location: Location) -> Self
-	{
-		Self::new(Kind::CharacterNotAllowed(character), location)
-	}
-
-	pub(crate) fn new_parse_number<I: Into<String>, S: Into<Source>>(input: I, location: Location,
-		source: S)
-		-> Self
-	{
-		Self::new(Kind::ParseNumber(input.into()), location).with(source)
-	}
-
-	pub(crate) fn new_mixed_implication_directions(location_1: Location, location_2: Location)
-		-> Self
-	{
-		Self::new(Kind::MixedImplicationDirections(location_2), location_1)
-	}
-
-	pub(crate) fn new_expected_variable_declaration(location: Location) -> Self
-	{
-		Self::new(Kind::ExpectedVariableDeclaration, location)
-	}
-
-	pub(crate) fn new_unexpected_token(location: Location) -> Self
-	{
-		Self::new(Kind::UnexpectedToken, location)
-	}
-
-	pub(crate) fn new_empty_expression(location: Location) -> Self
-	{
-		Self::new(Kind::EmptyExpression, location)
-	}
-
-	pub(crate) fn new_expected_logical_connective_argument(logical_connective_name: String,
-		location: Location)
-		-> Self
-	{
-		Self::new(Kind::ExpectedLogicalConnectiveArgument(logical_connective_name), location)
-	}
-
-	pub(crate) fn new_expected_term(location: Location) -> Self
-	{
-		Self::new(Kind::ExpectedTerm, location)
-	}
-
-	pub(crate) fn new_multiple_comparison_operators(
-		comparison_operator_1: crate::ComparisonOperator,
-		comparison_operator_2: crate::ComparisonOperator, location: Location)
-		-> Self
-	{
-		Self::new(Kind::MultipleComparisonOperators(comparison_operator_1, comparison_operator_2),
-			location)
-	}
-}
-
-impl std::fmt::Debug for Error
-{
-	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		if let Some(end) = self.location.end
-		{
-			write!(formatter, "parsing error at {}:{}: ", self.location.start, end)?;
-		}
-		else
-		{
-			write!(formatter, "parsing error at {}: ", self.location.start)?;
-		}
-
-		match &self.kind
-		{
-			Kind::UnmatchedParenthesis => write!(formatter, "unmatched parenthesis")?,
-			Kind::CharacterNotAllowed(character) =>
-				write!(formatter, "character not allowed: ‘{}’", character)?,
-			Kind::ParseNumber(input) => write!(formatter, "could not “{}” as number", input)?,
-			// TODO: print second location properly
-			Kind::MixedImplicationDirections(_location_2) =>
-				write!(formatter, "-> and <- implications may not be mixed within the same scope")?,
-			Kind::ExpectedVariableDeclaration =>
-				write!(formatter, "expected a variable declaration")?,
-			Kind::UnexpectedToken => write!(formatter, "unexpected token")?,
-			Kind::EmptyExpression => write!(formatter, "empty expression")?,
-			Kind::ExpectedLogicalConnectiveArgument(ref logical_connective_name) =>
-				write!(formatter, "this “{}” logical connective is missing an argument",
-					logical_connective_name)?,
-			Kind::ExpectedTerm => write!(formatter, "expected a term")?,
-			Kind::MultipleComparisonOperators(comparison_operator_1, comparison_operator_2) =>
-				write!(formatter, "chained comparisons aren’t supported (found “{:?}” and “{:?}” in the same formula), consider separating them with “and”",
-					comparison_operator_1, comparison_operator_2)?,
-		}
-
-		if let Some(source) = &self.source
-		{
-			write!(formatter, "\nerror source: {}", source)?;
-		}
-
-		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/parse/formulas.rs

@@ -1,564 +0,0 @@
-use super::terms::*;
-use super::tokens::*;
-
-pub fn formula<P>(input: &str, parser: &P)
-	-> Result<crate::OpenFormula<P::Flavor>, crate::parse::Error>
-where
-	P: super::Parser,
-{
-	let variable_declaration_stack = crate::VariableDeclarationStackLayer::free();
-
-	let formula_str = FormulaStr::new(input, parser, &variable_declaration_stack);
-	let formula = formula_str.parse(0)?;
-
-	let free_variable_declarations = match variable_declaration_stack
-	{
-		crate::VariableDeclarationStackLayer::Free(free_variable_declarations) =>
-			std::rc::Rc::new(free_variable_declarations.into_inner()),
-		_ => unreachable!(),
-	};
-
-	Ok(crate::OpenFormula
-	{
-		formula,
-		free_variable_declarations,
-	})
-}
-
-pub(crate) fn predicate_name(identifier: &str) -> Option<(&str, &str)>
-{
-	function_name(identifier)
-}
-
-#[derive(Clone, Copy, Eq, PartialEq)]
-enum LogicalConnective
-{
-	And,
-	IfAndOnlyIf,
-	ImpliesLeftToRight,
-	ImpliesRightToLeft,
-	Or,
-}
-
-impl LogicalConnective
-{
-	fn level(&self) -> usize
-	{
-		match self
-		{
-			Self::And => 1,
-			Self::Or => 2,
-			Self::ImpliesLeftToRight
-			| Self::ImpliesRightToLeft => 3,
-			Self::IfAndOnlyIf => 4,
-		}
-	}
-}
-
-impl std::fmt::Debug for LogicalConnective
-{
-	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		match &self
-		{
-			Self::And => write!(formatter, "and"),
-			Self::IfAndOnlyIf => write!(formatter, "<->"),
-			Self::ImpliesLeftToRight => write!(formatter, "->"),
-			Self::ImpliesRightToLeft => write!(formatter, "<-"),
-			Self::Or => write!(formatter, "or"),
-		}
-	}
-}
-
-struct FormulaStr<'i, 'd, 'p, 'v, P>
-where
-	P: super::Parser,
-{
-	input: &'i str,
-	parser: &'d P,
-	variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, P::Flavor>,
-}
-
-impl<'i, 'd, 'p, 'v, P> FormulaStr<'i, 'd, 'p, 'v, P>
-where
-	P: super::Parser,
-{
-	pub fn new(input: &'i str, parser: &'d P,
-		variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, P::Flavor>)
-		-> Self
-	{
-		Self
-		{
-			input,
-			parser,
-			variable_declaration_stack,
-		}
-	}
-
-	fn logical_connectives(&self) -> Tokens<'i, impl FnMut(Token<'i>) -> Option<LogicalConnective>>
-	{
-		let functor = |token| match token
-		{
-			Token::Identifier("and") => Some(LogicalConnective::And),
-			Token::Identifier("or") => Some(LogicalConnective::Or),
-			Token::Symbol(Symbol::ArrowLeft) => Some(LogicalConnective::ImpliesRightToLeft),
-			Token::Symbol(Symbol::ArrowLeftAndRight) => Some(LogicalConnective::IfAndOnlyIf),
-			Token::Symbol(Symbol::ArrowRight) => Some(LogicalConnective::ImpliesLeftToRight),
-			_ => None,
-		};
-
-		Tokens::new_filter_map(self.input, functor)
-	}
-
-	fn split_at_logical_connective(&self, logical_connective: LogicalConnective)
-		-> TokenSplit<Tokens<'i, impl FnMut(Token<'i>) -> Option<Token<'i>>>>
-	{
-		let predicate = move |token: &_| match token
-		{
-			Token::Identifier("and") => logical_connective == LogicalConnective::And,
-			Token::Identifier("or") => logical_connective == LogicalConnective::Or,
-			Token::Symbol(Symbol::ArrowLeft) =>
-				logical_connective == LogicalConnective::ImpliesRightToLeft,
-			Token::Symbol(Symbol::ArrowLeftAndRight) =>
-				logical_connective == LogicalConnective::IfAndOnlyIf,
-			Token::Symbol(Symbol::ArrowRight) =>
-				logical_connective == LogicalConnective::ImpliesLeftToRight,
-			_ => false,
-		};
-
-		Tokens::new_filter(self.input, predicate).split()
-	}
-
-	pub fn top_level_logical_connective(&self)
-		-> Result<Option<LogicalConnective>, crate::parse::Error>
-	{
-		let mut top_level_logical_connective = None;
-
-		for logical_connective in self.logical_connectives()
-		{
-			let (_, logical_connective) = logical_connective?;
-
-			top_level_logical_connective = match top_level_logical_connective
-			{
-				None => Some(logical_connective),
-				Some(top_level_logical_connective) =>
-				{
-					let implication_directions_are_mixed =
-						logical_connective == LogicalConnective::ImpliesLeftToRight
-							&& top_level_logical_connective == LogicalConnective::ImpliesRightToLeft
-						|| logical_connective == LogicalConnective::ImpliesRightToLeft
-							&& top_level_logical_connective == LogicalConnective::ImpliesLeftToRight;
-
-					if implication_directions_are_mixed
-					{
-						return Err(crate::parse::Error::new_mixed_implication_directions(
-							crate::parse::error::Location::new(0, Some(0)),
-							crate::parse::error::Location::new(0, Some(0))));
-					}
-
-					if logical_connective.level() > top_level_logical_connective.level()
-					{
-						Some(logical_connective)
-					}
-					else
-					{
-						Some(top_level_logical_connective)
-					}
-				},
-			}
-		}
-
-		Ok(top_level_logical_connective)
-	}
-
-	fn comparison_operators(&self) -> Tokens<'i, impl FnMut(Token<'i>)
-		-> Option<crate::ComparisonOperator>>
-	{
-		let functor = |token| match token
-		{
-			Token::Symbol(symbol) => match symbol
-			{
-				Symbol::Greater => Some(crate::ComparisonOperator::Greater),
-				Symbol::GreaterOrEqual => Some(crate::ComparisonOperator::GreaterOrEqual),
-				Symbol::Less => Some(crate::ComparisonOperator::Less),
-				Symbol::LessOrEqual => Some(crate::ComparisonOperator::LessOrEqual),
-				Symbol::Equal => Some(crate::ComparisonOperator::Equal),
-				Symbol::NotEqual => Some(crate::ComparisonOperator::NotEqual),
-				_ => None,
-			},
-			_ => None,
-		};
-
-		Tokens::new_filter_map(self.input, functor)
-	}
-
-	pub fn parse(&self, level: usize) -> Result<crate::Formula<P::Flavor>, crate::parse::Error>
-	{
-		let indentation = "  ".repeat(level);
-		let input = trim_start(self.input);
-
-		log::trace!("{}- parsing formula: {}", indentation, input);
-
-		match input.chars().next()
-		{
-			Some(')') => return Err(crate::parse::Error::new_unmatched_parenthesis(
-				crate::parse::error::Location::new(0, Some(0)))),
-			None => return Err(crate::parse::Error::new_empty_expression(
-				crate::parse::error::Location::new(0, Some(0)))),
-			_ => (),
-		}
-
-		// Parse logical infix connectives
-		if let Some(top_level_logical_connective) = self.top_level_logical_connective()?
-		{
-			log::trace!("{}  parsing “{:?}” logical connective", indentation,
-				top_level_logical_connective);
-
-			// Parse arguments of n-ary logical infix connectives
-			let arguments_n_ary = ||
-			{
-				// TODO: improve error handling if the formulas between the operators are invalid
-				self.split_at_logical_connective(top_level_logical_connective)
-					.map(|argument| FormulaStr::new(argument?, self.parser, self.variable_declaration_stack).parse(level + 1))
-					.collect::<Result<Vec<_>, _>>()
-			};
-
-			match top_level_logical_connective
-			{
-				LogicalConnective::And => return Ok(crate::Formula::and(arguments_n_ary()?)),
-				LogicalConnective::Or => return Ok(crate::Formula::or(arguments_n_ary()?)),
-				LogicalConnective::IfAndOnlyIf =>
-					return Ok(crate::Formula::if_and_only_if(arguments_n_ary()?)),
-				LogicalConnective::ImpliesLeftToRight =>
-					return self.implication_left_to_right(
-						self.split_at_logical_connective(top_level_logical_connective), level + 1),
-				LogicalConnective::ImpliesRightToLeft =>
-				{
-					let mut argument_iterator =
-						self.split_at_logical_connective(top_level_logical_connective);
-					let first_argument = argument_iterator.next().ok_or_else(||
-						crate::parse::Error::new_expected_logical_connective_argument(
-							"right-to-left implication".to_string(),
-							crate::parse::error::Location::new(0, Some(0))))?;
-					let first_argument = FormulaStr::new(first_argument?, self.parser, self.variable_declaration_stack).parse(level + 1)?;
-
-					return argument_iterator.try_fold(first_argument,
-						|accumulator, argument|
-						{
-							let argument = FormulaStr::new(argument?, self.parser, self.variable_declaration_stack).parse(level + 1)?;
-
-							Ok(crate::Formula::implies(crate::ImplicationDirection::RightToLeft,
-								Box::new(argument), Box::new(accumulator)))
-						});
-				},
-			}
-		}
-
-		// Parse quantified formulas
-		if let Some((identifier, input)) = identifier(input)
-		{
-			match identifier
-			{
-				"not" =>
-				{
-					let input = trim_start(input);
-					log::trace!("{}  parsing “not” formula body: {}", indentation, input);
-
-					let argument = FormulaStr::new(input, self.parser, self.variable_declaration_stack).parse(level + 1)?;
-
-					return Ok(crate::Formula::not(Box::new(argument)));
-				},
-				"true" =>
-				{
-					if !input.trim().is_empty()
-					{
-						return Err(crate::parse::Error::new_unexpected_token(
-							crate::parse::error::Location::new(0, Some(0))))
-					}
-
-					return Ok(crate::Formula::true_());
-				},
-				"false" =>
-				{
-					if !input.trim().is_empty()
-					{
-						return Err(crate::parse::Error::new_unexpected_token(
-							crate::parse::error::Location::new(0, Some(0))))
-					}
-
-					return Ok(crate::Formula::false_());
-				},
-				_ => (),
-			}
-
-			let quantifier = match identifier
-			{
-				"exists" => Some(Quantifier::Existential),
-				"forall" => Some(Quantifier::Universal),
-				_ => None,
-			};
-
-			if let Some(quantifier) = quantifier
-			{
-				let input = trim_start(input);
-				log::trace!("{}  parsing “{:?}” formula body: {}", indentation, quantifier, input);
-
-				return self.quantified_formula(input, quantifier, level + 1);
-			}
-		}
-
-		let mut comparison_operators = self.comparison_operators();
-
-		// Parse comparisons
-		if let Some(comparison_operator) = comparison_operators.next()
-		{
-			let (_, comparison_operator) = comparison_operator?;
-
-			// Comparisons with more than one comparison operator aren’t supported
-			if let Some(next_comparison_operator) = comparison_operators.next()
-			{
-				let (_, next_comparison_operator) = next_comparison_operator?;
-
-				return Err(crate::parse::Error::new_multiple_comparison_operators(
-					comparison_operator, next_comparison_operator,
-					crate::parse::error::Location::new(0, Some(0))));
-			}
-
-			log::trace!("{}  parsing “{:?}” comparison: {}", indentation, comparison_operator, input);
-
-			let mut comparison_operator_split = self.comparison_operators().split();
-
-			// There’s exactly one comparison operator in this formula, as we have verified above.
-			// Hence, the split is guaranteed to generate exactly these two elements
-			let input_left = comparison_operator_split.next().unwrap()?;
-			let input_right = comparison_operator_split.next().unwrap()?;
-			assert!(comparison_operator_split.next().is_none());
-
-			let argument_left =
-				TermStr::new(input_left, self.parser, self.variable_declaration_stack)
-					.parse(level + 1)?;
-			let argument_right =
-				TermStr::new(input_right, self.parser, self.variable_declaration_stack)
-					.parse(level + 1)?;
-
-			return Ok(crate::Formula::compare(comparison_operator, Box::new(argument_left),
-				Box::new(argument_right)));
-		}
-
-		// Parse predicates
-		if let Some((predicate_name, input)) = predicate_name(input)
-		{
-			log::trace!("{}  parsing predicate {}", indentation, predicate_name);
-
-			let input = trim_start(input);
-
-			// Parse arguments if there are any
-			let (arguments, input) = match parenthesized_expression(input)?
-			{
-				Some((parenthesized_expression, input)) =>
-				{
-					let functor = |token: &_| *token == Token::Symbol(Symbol::Comma);
-					let arguments = Tokens::new_filter(parenthesized_expression, functor).split()
-						.map(|argument| TermStr::new(argument?, self.parser,
-							self.variable_declaration_stack)
-								.parse(level + 1))
-						.collect::<Result<_, _>>()?;
-
-					(arguments, input)
-				}
-				None => (vec![], input),
-			};
-
-			if !input.trim().is_empty()
-			{
-				return Err(crate::parse::Error::new_unexpected_token(
-					crate::parse::error::Location::new(0, Some(0))))
-			}
-
-			let declaration = self.parser.find_or_create_predicate_declaration(predicate_name,
-				arguments.len());
-			return Ok(crate::Formula::predicate(declaration, arguments));
-		}
-
-		// Parse parenthesized formulas
-		if let Some((parenthesized_expression, input)) = parenthesized_expression(input)?
-		{
-			if !input.trim().is_empty()
-			{
-				return Err(crate::parse::Error::new_unexpected_token(
-					crate::parse::error::Location::new(0, Some(0))));
-			}
-
-			return FormulaStr::new(parenthesized_expression, self.parser, self.variable_declaration_stack).parse(level + 1);
-		}
-
-		Err(crate::parse::Error::new_unexpected_token(
-			crate::parse::error::Location::new(0, Some(0))))
-	}
-
-	// TODO: refactor
-	fn implication_left_to_right_inner<T>(&self, mut argument_iterator: T, level: usize)
-		-> Result<Option<crate::Formula<P::Flavor>>, crate::parse::Error>
-	where
-		T: std::iter::Iterator<Item = Result<&'i str, crate::parse::Error>>
-	{
-		match argument_iterator.next()
-		{
-			Some(argument) =>
-			{
-				// TODO: improve error handling if antecedent cannot be parsed
-				let argument = FormulaStr::new(argument?, self.parser, self.variable_declaration_stack).parse(level)?;
-				match self.implication_left_to_right_inner(argument_iterator, level)?
-				{
-					Some(next_argument) => Ok(Some(crate::Formula::implies(
-						crate::ImplicationDirection::LeftToRight, Box::new(argument),
-						Box::new(next_argument)))),
-					None => Ok(Some(argument)),
-				}
-			},
-			None => Ok(None),
-		}
-	}
-
-	fn implication_left_to_right<T>(&self, mut argument_iterator: T, level: usize)
-		-> Result<crate::Formula<P::Flavor>, crate::parse::Error>
-	where
-		T: std::iter::Iterator<Item = Result<&'i str, crate::parse::Error>>
-	{
-		match argument_iterator.next()
-		{
-			Some(argument) =>
-			{
-				// TODO: improve error handling if antecedent cannot be parsed
-				let argument = FormulaStr::new(argument?, self.parser, self.variable_declaration_stack).parse(level)?;
-				match self.implication_left_to_right_inner(argument_iterator, level)?
-				{
-					Some(next_argument) => Ok(crate::Formula::implies(
-						crate::ImplicationDirection::LeftToRight, Box::new(argument),
-						Box::new(next_argument))),
-					None => Err(crate::parse::Error::new_expected_logical_connective_argument(
-						"left-to-right implication".to_string(),
-						crate::parse::error::Location::new(0, Some(0)))),
-				}
-			},
-			None => Err(crate::parse::Error::new_expected_logical_connective_argument(
-				"left-to-right implication".to_string(),
-				crate::parse::error::Location::new(0, Some(0)))),
-		}
-	}
-
-	// TODO: refactor without input argument
-	fn quantified_formula(&self, input: &str, quantifier: Quantifier, level: usize)
-		-> Result<crate::Formula<P::Flavor>, crate::parse::Error>
-	{
-		let (parameters, input) = match variable_declarations::<P>(input)?
-		{
-			Some(variable_declarations) => variable_declarations,
-			None => return Err(crate::parse::Error::new_expected_variable_declaration(
-				crate::parse::error::Location::new(0, Some(0)))),
-		};
-		let parameters = std::rc::Rc::new(parameters);
-
-		let variable_declaration_stack = crate::VariableDeclarationStackLayer::bound(
-			self.variable_declaration_stack, std::rc::Rc::clone(&parameters));
-
-		let formula_str =
-			FormulaStr::new(input.trim(), self.parser, &variable_declaration_stack);
-		let formula = Box::new(formula_str.parse(level)?);
-
-		let formula = match quantifier
-		{
-			Quantifier::Existential => crate::Formula::exists(parameters, formula),
-			Quantifier::Universal => crate::Formula::for_all(parameters, formula),
-		};
-
-		Ok(formula)
-	}
-}
-
-#[derive(Clone, Copy, Eq, PartialEq)]
-pub(crate) enum Quantifier
-{
-	Existential,
-	Universal,
-}
-
-impl std::fmt::Debug for Quantifier
-{
-	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		match &self
-		{
-			Self::Existential => write!(formatter, "exists"),
-			Self::Universal => write!(formatter, "forall"),
-		}
-	}
-}
-
-#[cfg(test)]
-mod tests
-{
-	use super::*;
-
-	#[test]
-	fn tokenize_formula_logical_connectives()
-	{
-		let parser = crate::parse::DefaultParser::new();
-		let variable_declaration_stack = crate::VariableDeclarationStackLayer::free();
-
-		let formula_str = |input| FormulaStr::new(input, &parser, &variable_declaration_stack);
-
-		let f = formula_str("((forall X exists Y (p(X) -> q(Y)) and false) or p) -> false");
-		assert_eq!(f.top_level_logical_connective().unwrap(),
-			Some(LogicalConnective::ImpliesLeftToRight));
-		let mut i = f.logical_connectives();
-		assert_eq!(i.next().unwrap().unwrap().1, LogicalConnective::ImpliesLeftToRight);
-		assert!(i.next().is_none());
-
-		let f = formula_str("forall X exists Y (p(X) -> q(Y)) and false or p -> false");
-		assert_eq!(f.top_level_logical_connective().unwrap(),
-			Some(LogicalConnective::ImpliesLeftToRight));
-		let mut i = f.logical_connectives();
-		assert_eq!(i.next().unwrap().unwrap().1, LogicalConnective::And);
-		assert_eq!(i.next().unwrap().unwrap().1, LogicalConnective::Or);
-		assert_eq!(i.next().unwrap().unwrap().1, LogicalConnective::ImpliesLeftToRight);
-		assert!(i.next().is_none());
-
-		let f = formula_str("  p -> forall X exists Y (p(X) -> q(Y)) and false or p -> false  ");
-		assert_eq!(f.top_level_logical_connective().unwrap(),
-			Some(LogicalConnective::ImpliesLeftToRight));
-		let mut i = f.split_at_logical_connective(LogicalConnective::ImpliesLeftToRight);
-		assert_eq!(i.next().unwrap().unwrap(), "p");
-		assert_eq!(i.next().unwrap().unwrap(), "forall X exists Y (p(X) -> q(Y)) and false or p");
-		assert_eq!(i.next().unwrap().unwrap(), "false");
-		assert!(i.next().is_none());
-
-		let f = formula_str("  p -> forall X exists Y (p(X) -> q(Y)) and false or p -> false  ");
-		assert_eq!(f.top_level_logical_connective().unwrap(),
-			Some(LogicalConnective::ImpliesLeftToRight));
-		let mut i = f.split_at_logical_connective(LogicalConnective::And);
-		assert_eq!(i.next().unwrap().unwrap(), "p -> forall X exists Y (p(X) -> q(Y))");
-		assert_eq!(i.next().unwrap().unwrap(), "false or p -> false");
-		assert!(i.next().is_none());
-
-		let f = formula_str("  p and forall X exists Y (p(X) -> q(Y)) and false or p or false  ");
-		assert_eq!(f.top_level_logical_connective().unwrap(), Some(LogicalConnective::Or));
-		let mut i = f.split_at_logical_connective(LogicalConnective::Or);
-		assert_eq!(i.next().unwrap().unwrap(), "p and forall X exists Y (p(X) -> q(Y)) and false");
-		assert_eq!(i.next().unwrap().unwrap(), "p");
-		assert_eq!(i.next().unwrap().unwrap(), "false");
-		assert!(i.next().is_none());
-
-		let f = formula_str(" (p and q) ");
-		assert!(f.top_level_logical_connective().unwrap().is_none());
-		let mut i = f.split_at_logical_connective(LogicalConnective::And);
-		assert_eq!(i.next().unwrap().unwrap(), "(p and q)");
-		assert!(i.next().is_none());
-
-		assert!(formula_str(" a -> b -> c ").parse(0).is_ok());
-		assert!(formula_str(" a -> b <- c ").parse(0).is_err());
-
-		assert!(formula_str("  p -> forall X exists Y (p(X) -> q(Y)) and false or p -> false  ")
-			.parse(0).is_ok());
-	}
-}

src/parse/terms.rs

@@ -1,651 +0,0 @@
-use super::tokens::*;
-
-pub(crate) fn function_name(input: &str) -> Option<(&str, &str)>
-{
-	let (identifier, remaining_input) = identifier(input)?;
-
-	if is_keyword(identifier)
-	{
-		return None;
-	}
-
-	let mut characters = identifier.chars();
-
-	while let Some(character) = characters.next()
-	{
-		match character
-		{
-			'_' => continue,
-			_ if character.is_ascii_lowercase() => return Some((identifier, remaining_input)),
-			_ => return None,
-		}
-	}
-
-	None
-}
-
-fn variable_name(input: &str) -> Option<(&str, &str)>
-{
-	let (identifier, remaining_input) = identifier(input)?;
-
-	let mut characters = identifier.chars();
-
-	while let Some(character) = characters.next()
-	{
-		match character
-		{
-			'_' => continue,
-			_ if character.is_ascii_uppercase() => return Some((identifier, remaining_input)),
-			_ => return None,
-		}
-	}
-
-	None
-}
-
-pub fn is_function_name(identifier: &str) -> bool
-{
-	if is_keyword(identifier)
-	{
-		return false;
-	}
-
-	let mut characters = identifier.chars();
-
-	while let Some(character) = characters.next()
-	{
-		match character
-		{
-			'_' => continue,
-			_ if character.is_ascii_lowercase() => return true,
-			_ => return false,
-		}
-	}
-
-	false
-}
-
-fn is_variable_name(identifier: &str) -> bool
-{
-	let mut characters = identifier.chars();
-
-	while let Some(character) = characters.next()
-	{
-		match character
-		{
-			'_' => continue,
-			_ if character.is_ascii_uppercase() => return true,
-			_ => return false,
-		}
-	}
-
-	false
-}
-
-pub(crate) fn variable_declaration<P>(input: &str)
-	-> Option<(<P::Flavor as crate::flavor::Flavor>::VariableDeclaration, &str)>
-where
-	P: crate::parse::Parser,
-{
-	variable_name(input)
-		.map(|(variable_name, remaining_input)|
-			(<P as crate::parse::Parser>::new_variable_declaration(variable_name.to_string()),
-			remaining_input))
-}
-
-pub(crate) fn variable_declarations<P>(input: &str)
-	-> Result<Option<(crate::VariableDeclarations<P::Flavor>, &str)>, crate::parse::Error>
-where
-	P: crate::parse::Parser,
-{
-	let mut variable_declarations = vec![];
-
-	let (first_variable_declaration, mut input) = match variable_declaration::<P>(input)
-	{
-		Some(first_variable_declaration) => first_variable_declaration,
-		None => return Ok(None),
-	};
-
-	variable_declarations.push(std::rc::Rc::new(first_variable_declaration));
-
-	loop
-	{
-		input = trim_start(input);
-
-		input = match symbol(input)
-		{
-			Some((Symbol::Comma, input)) => input,
-			// TODO: detect redeclarations, such as in “exists X, Y, X”
-			_ => return Ok(Some((variable_declarations, input))),
-		};
-
-		input = trim_start(input);
-
-		let (variable_declaration, remaining_input) = match variable_declaration::<P>(input)
-		{
-			Some(variable_declaration) => variable_declaration,
-			None => return Err(crate::parse::Error::new_expected_variable_declaration(
-				crate::parse::error::Location::new(0, Some(0)))),
-		};
-
-		input = remaining_input;
-
-		variable_declarations.push(std::rc::Rc::new(variable_declaration));
-	}
-}
-
-#[derive(Clone, Copy, Eq, PartialEq)]
-pub(crate) enum ArithmeticOperatorClass
-{
-	Exponential,
-	Multiplicative,
-	Additive,
-}
-
-impl ArithmeticOperatorClass
-{
-	fn level(&self) -> usize
-	{
-		match self
-		{
-			Self::Exponential => 1,
-			Self::Multiplicative => 2,
-			Self::Additive => 3,
-		}
-	}
-}
-
-impl std::fmt::Debug for ArithmeticOperatorClass
-{
-	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		match &self
-		{
-			Self::Exponential => write!(formatter, "exponential"),
-			Self::Multiplicative => write!(formatter, "multiplicative"),
-			Self::Additive => write!(formatter, "additive"),
-		}
-	}
-}
-
-pub(crate) struct TermStr<'i, 'd, 'v, 'p, P>
-where
-	P: super::Parser,
-{
-	input: &'i str,
-	parser: &'d P,
-	variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, P::Flavor>,
-}
-
-impl<'i, 'd, 'v, 'p, P> TermStr<'i, 'd, 'v, 'p, P>
-where
-	P: super::Parser,
-{
-	pub fn new(input: &'i str, parser: &'d P,
-		variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, P::Flavor>)
-		-> Self
-	{
-		Self
-		{
-			input,
-			parser,
-			variable_declaration_stack,
-		}
-	}
-
-	fn arithmetic_operator_classes(&self) -> Tokens<'i, impl FnMut(Token<'i>)
-		-> Option<ArithmeticOperatorClass>>
-	{
-		let functor = |token| match token
-		{
-			Token::Symbol(Symbol::Exponentiation) => Some(ArithmeticOperatorClass::Exponential),
-			Token::Symbol(Symbol::Multiplication) => Some(ArithmeticOperatorClass::Multiplicative),
-			Token::Symbol(Symbol::Division) => Some(ArithmeticOperatorClass::Multiplicative),
-			Token::Symbol(Symbol::Percent) => Some(ArithmeticOperatorClass::Multiplicative),
-			Token::Symbol(Symbol::Plus) => Some(ArithmeticOperatorClass::Additive),
-			Token::Symbol(Symbol::Minus) => Some(ArithmeticOperatorClass::Additive),
-			_ => None,
-		};
-
-		// TODO: refactor so that self.input is always set correctly
-		Tokens::new_filter_map(self.input, functor)
-	}
-
-	fn filter_by_arithmetic_operator_class(&self,
-		arithmetic_operator_class: ArithmeticOperatorClass)
-		-> Tokens<'i, impl FnMut(Token<'i>) -> Option<crate::BinaryOperator>>
-	{
-		let functor = move |token| match token
-		{
-			Token::Symbol(Symbol::Exponentiation) =>
-				if arithmetic_operator_class == ArithmeticOperatorClass::Exponential
-				{
-					Some(crate::BinaryOperator::Exponentiate)
-				}
-				else
-				{
-					None
-				},
-			Token::Symbol(Symbol::Multiplication) =>
-				if arithmetic_operator_class == ArithmeticOperatorClass::Multiplicative
-				{
-					Some(crate::BinaryOperator::Multiply)
-				}
-				else
-				{
-					None
-				},
-			Token::Symbol(Symbol::Division) =>
-				if arithmetic_operator_class == ArithmeticOperatorClass::Multiplicative
-				{
-					Some(crate::BinaryOperator::Divide)
-				}
-				else
-				{
-					None
-				},
-			Token::Symbol(Symbol::Percent) =>
-				if arithmetic_operator_class == ArithmeticOperatorClass::Multiplicative
-				{
-					Some(crate::BinaryOperator::Modulo)
-				}
-				else
-				{
-					None
-				},
-			Token::Symbol(Symbol::Plus) =>
-				if arithmetic_operator_class == ArithmeticOperatorClass::Additive
-				{
-					Some(crate::BinaryOperator::Add)
-				}
-				else
-				{
-					None
-				},
-			Token::Symbol(Symbol::Minus) =>
-				if arithmetic_operator_class == ArithmeticOperatorClass::Additive
-				{
-					Some(crate::BinaryOperator::Subtract)
-				}
-				else
-				{
-					None
-				},
-			_ => None,
-		};
-
-		Tokens::new_filter_map(self.input, functor)
-	}
-
-	pub fn top_level_arithmetic_operator_class(&self)
-		-> Result<Option<ArithmeticOperatorClass>, crate::parse::Error>
-	{
-		let mut top_level_arithmetic_operator_class = None;
-
-		for arithmetic_operator_class in self.arithmetic_operator_classes()
-		{
-			let (_, arithmetic_operator_class) = arithmetic_operator_class?;
-
-			top_level_arithmetic_operator_class = match top_level_arithmetic_operator_class
-			{
-				None => Some(arithmetic_operator_class),
-				Some(top_level_arithmetic_operator_class) =>
-				{
-					if arithmetic_operator_class.level()
-						> top_level_arithmetic_operator_class.level()
-					{
-						Some(arithmetic_operator_class)
-					}
-					else
-					{
-						Some(top_level_arithmetic_operator_class)
-					}
-				},
-			}
-		}
-
-		Ok(top_level_arithmetic_operator_class)
-	}
-
-	pub fn parse(&self, level: usize) -> Result<crate::Term<P::Flavor>, crate::parse::Error>
-	{
-		let indentation = "  ".repeat(level);
-		log::trace!("{}- parsing term: {}", indentation, self.input);
-
-		let input = trim_start(self.input);
-
-		match input.chars().next()
-		{
-			Some(')') => return Err(crate::parse::Error::new_unmatched_parenthesis(
-				crate::parse::error::Location::new(0, Some(0)))),
-			// TODO: implement absolute value function
-			Some('|') => unimplemented!(),
-			None => return Err(crate::parse::Error::new_empty_expression(
-				crate::parse::error::Location::new(0, Some(0)))),
-			_ => (),
-		}
-
-		// Parse arithmetic infix operations
-		if let Some(top_level_arithmetic_operator_class) =
-			self.top_level_arithmetic_operator_class()?
-		{
-			log::trace!("{}  parsing {:?} arithmetic term", indentation,
-				top_level_arithmetic_operator_class);
-
-			if top_level_arithmetic_operator_class == ArithmeticOperatorClass::Exponential
-			{
-				return self.exponentiate(
-					self.filter_by_arithmetic_operator_class(top_level_arithmetic_operator_class)
-						.split(), level + 1);
-			}
-
-			// Parse arguments of arithmetic infix operations
-			let mut argument_iterator =
-				self.filter_by_arithmetic_operator_class(top_level_arithmetic_operator_class);
-
-			let (first_argument, first_binary_operator) = argument_iterator.next().ok_or_else(||
-				crate::parse::Error::new_expected_term(
-					crate::parse::error::Location::new(0, Some(0))))??;
-			let first_argument =
-				TermStr::new(first_argument, self.parser, self.variable_declaration_stack)
-					.parse(level + 1)?;
-			// TODO: improve error handling if the terms between the operators are invalid
-
-			let (accumulator, last_binary_operator) =
-				argument_iterator.try_fold((first_argument, first_binary_operator),
-					|(accumulator, binary_operator), argument|
-					{
-						let (argument, next_binary_operator) = argument?;
-						let argument = TermStr::new(argument, self.parser,
-							self.variable_declaration_stack)
-								.parse(level + 1)?;
-						let binary_operation =
-							crate::BinaryOperation::new(binary_operator, Box::new(accumulator),
-								Box::new(argument));
-						let formula = crate::Term::BinaryOperation(binary_operation);
-
-						Ok((formula, next_binary_operator))
-					})?;
-
-			// The last item hasn’t been consumed yet, so it’s safe to unwrap it
-			let last_argument = argument_iterator.remaining_input().unwrap();
-			let last_argument =
-				TermStr::new(last_argument, self.parser, self.variable_declaration_stack)
-					.parse(level + 1)?;
-			let last_binary_operation =
-				crate::BinaryOperation::new(last_binary_operator, Box::new(accumulator),
-					Box::new(last_argument));
-
-			return Ok(crate::Term::BinaryOperation(last_binary_operation));
-		}
-
-		if let Some((number, input)) = number(input)?
-		{
-			if !input.trim().is_empty()
-			{
-				return Err(crate::parse::Error::new_unexpected_token(
-					crate::parse::error::Location::new(0, Some(0))));
-			}
-
-			return Ok(crate::Term::integer(number as i32));
-		}
-
-		if let Some((identifier, input)) = identifier(input)
-		{
-			match identifier
-			{
-				"inf" =>
-				{
-					if !input.trim().is_empty()
-					{
-						return Err(crate::parse::Error::new_unexpected_token(
-							crate::parse::error::Location::new(0, Some(0))))
-					}
-
-					return Ok(crate::Term::infimum());
-				},
-				"sup" =>
-				{
-					if !input.trim().is_empty()
-					{
-						return Err(crate::parse::Error::new_unexpected_token(
-							crate::parse::error::Location::new(0, Some(0))))
-					}
-
-					return Ok(crate::Term::supremum());
-				},
-				"true" =>
-				{
-					if !input.trim().is_empty()
-					{
-						return Err(crate::parse::Error::new_unexpected_token(
-							crate::parse::error::Location::new(0, Some(0))))
-					}
-
-					return Ok(crate::Term::true_());
-				},
-				"false" =>
-				{
-					if !input.trim().is_empty()
-					{
-						return Err(crate::parse::Error::new_unexpected_token(
-							crate::parse::error::Location::new(0, Some(0))))
-					}
-
-					return Ok(crate::Term::false_());
-				},
-				_ if is_variable_name(identifier) =>
-				{
-					if !input.trim().is_empty()
-					{
-						return Err(crate::parse::Error::new_unexpected_token(
-							crate::parse::error::Location::new(0, Some(0))))
-					}
-
-					let declaration = P::find_or_create_variable_declaration(
-						self.variable_declaration_stack, identifier);
-					return Ok(crate::Term::variable(declaration));
-				},
-				_ if is_function_name(identifier) =>
-				{
-					let function_name = identifier;
-					log::trace!("{}  parsing function {}", indentation, function_name);
-
-					let input = trim_start(input);
-
-					// Parse arguments if there are any
-					let (arguments, input) = match parenthesized_expression(input)?
-					{
-						Some((parenthesized_expression, input)) =>
-						{
-							let functor = |token: &_| *token == Token::Symbol(Symbol::Comma);
-							let arguments = Tokens::new_filter(parenthesized_expression, functor).split()
-								.map(|argument| TermStr::new(argument?, self.parser,
-									self.variable_declaration_stack)
-										.parse(level + 1))
-								.collect::<Result<_, _>>()?;
-
-							(arguments, input)
-						}
-						None => (vec![], input),
-					};
-
-					if !input.trim().is_empty()
-					{
-						return Err(crate::parse::Error::new_unexpected_token(
-							crate::parse::error::Location::new(0, Some(0))))
-					}
-
-					let declaration = self.parser.find_or_create_function_declaration(
-						function_name, arguments.len());
-					return Ok(crate::Term::function(declaration, arguments));
-				},
-				_ => (),
-			}
-		}
-
-		// TODO: parse negative value
-
-		// Parse parenthesized terms
-		if let Some((parenthesized_expression, input)) = parenthesized_expression(input)?
-		{
-			if !input.trim().is_empty()
-			{
-				return Err(crate::parse::Error::new_unexpected_token(
-					crate::parse::error::Location::new(0, Some(0))));
-			}
-
-			return TermStr::new(parenthesized_expression, self.parser,
-				self.variable_declaration_stack)
-					.parse(level + 1);
-		}
-
-		Err(crate::parse::Error::new_unexpected_token(
-			crate::parse::error::Location::new(0, Some(0))))
-	}
-
-	// TODO: refactor
-	fn exponentiate_inner<T>(&self, mut argument_iterator: T, level: usize)
-		-> Result<Option<crate::Term<P::Flavor>>, crate::parse::Error>
-	where
-		T: std::iter::Iterator<Item = Result<&'i str, crate::parse::Error>>
-	{
-		match argument_iterator.next()
-		{
-			Some(argument) =>
-			{
-				// TODO: improve error handling if antecedent cannot be parsed
-				let argument =
-					TermStr::new(argument?, self.parser, self.variable_declaration_stack)
-						.parse(level)?;
-				match self.exponentiate_inner(argument_iterator, level)?
-				{
-					Some(next_argument) => Ok(Some(crate::Term::exponentiate(Box::new(argument),
-						Box::new(next_argument)))),
-					None => Ok(Some(argument)),
-				}
-			},
-			None => Ok(None),
-		}
-	}
-
-	fn exponentiate<T>(&self, mut argument_iterator: T, level: usize)
-		-> Result<crate::Term<P::Flavor>, crate::parse::Error>
-	where
-		T: std::iter::Iterator<Item = Result<&'i str, crate::parse::Error>>
-	{
-		match argument_iterator.next()
-		{
-			Some(argument) =>
-			{
-				// TODO: improve error handling if antecedent cannot be parsed
-				let argument =
-					TermStr::new(argument?, self.parser, self.variable_declaration_stack)
-						.parse(level)?;
-				match self.exponentiate_inner(argument_iterator, level)?
-				{
-					Some(next_argument) =>
-						Ok(crate::Term::exponentiate(Box::new(argument), Box::new(next_argument))),
-					None => Err(crate::parse::Error::new_expected_term(
-						crate::parse::error::Location::new(0, Some(0)))),
-				}
-			},
-			None => Err(crate::parse::Error::new_expected_term(
-				crate::parse::error::Location::new(0, Some(0)))),
-		}
-	}
-}
-
-#[cfg(test)]
-mod tests
-{
-	use super::*;
-
-	#[test]
-	fn parse_variable_name()
-	{
-		assert_eq!(variable_name("X").unwrap(), ("X", ""));
-		assert_eq!(variable_name("_X").unwrap(), ("_X", ""));
-		assert_eq!(variable_name("__X").unwrap(), ("__X", ""));
-		assert_eq!(variable_name("Variable").unwrap(), ("Variable", ""));
-		assert_eq!(variable_name("_Variable").unwrap(), ("_Variable", ""));
-		assert_eq!(variable_name("__Variable").unwrap(), ("__Variable", ""));
-		assert_eq!(variable_name("X,").unwrap(), ("X", ","));
-		assert_eq!(variable_name("_X,").unwrap(), ("_X", ","));
-		assert_eq!(variable_name("__X,").unwrap(), ("__X", ","));
-		assert_eq!(variable_name("Variable,").unwrap(), ("Variable", ","));
-		assert_eq!(variable_name("_Variable,").unwrap(), ("_Variable", ","));
-		assert_eq!(variable_name("__Variable,").unwrap(), ("__Variable", ","));
-	}
-
-	#[test]
-	fn parse_variable_declaration()
-	{
-		let variable_declaration =
-			|x| super::variable_declaration::<crate::parse::DefaultParser>(x);
-
-		let v = variable_declaration("X").unwrap();
-		assert_eq!((v.0.name.as_str(), v.1), ("X", ""));
-		let v = variable_declaration("_X").unwrap();
-		assert_eq!((v.0.name.as_str(), v.1), ("_X", ""));
-		let v = variable_declaration("__X").unwrap();
-		assert_eq!((v.0.name.as_str(), v.1), ("__X", ""));
-		let v = variable_declaration("Variable").unwrap();
-		assert_eq!((v.0.name.as_str(), v.1), ("Variable", ""));
-		let v = variable_declaration("_Variable").unwrap();
-		assert_eq!((v.0.name.as_str(), v.1), ("_Variable", ""));
-		let v = variable_declaration("__Variable").unwrap();
-		assert_eq!((v.0.name.as_str(), v.1), ("__Variable", ""));
-		let v = variable_declaration("X,").unwrap();
-		assert_eq!((v.0.name.as_str(), v.1), ("X", ","));
-		let v = variable_declaration("_X,").unwrap();
-		assert_eq!((v.0.name.as_str(), v.1), ("_X", ","));
-		let v = variable_declaration("__X,").unwrap();
-		assert_eq!((v.0.name.as_str(), v.1), ("__X", ","));
-		let v = variable_declaration("Variable,").unwrap();
-		assert_eq!((v.0.name.as_str(), v.1), ("Variable", ","));
-		let v = variable_declaration("_Variable,").unwrap();
-		assert_eq!((v.0.name.as_str(), v.1), ("_Variable", ","));
-		let v = variable_declaration("__Variable,").unwrap();
-		assert_eq!((v.0.name.as_str(), v.1), ("__Variable", ","));
-	}
-
-	#[test]
-	fn parse_variable_declarations()
-	{
-		let variable_declarations =
-			|x| super::variable_declarations::<crate::parse::DefaultParser>(x);
-
-		let v = variable_declarations("X.").unwrap().unwrap();
-		assert_eq!(v.0.len(), 1);
-		assert_eq!(v.0[0].name.as_str(), "X");
-		assert_eq!(v.1, ".");
-
-		let v = variable_declarations("X,Y,Z.").unwrap().unwrap();
-		assert_eq!(v.0.len(), 3);
-		assert_eq!(v.0[0].name.as_str(), "X");
-		assert_eq!(v.0[1].name.as_str(), "Y");
-		assert_eq!(v.0[2].name.as_str(), "Z");
-		assert_eq!(v.1, ".");
-
-		let v = variable_declarations("X, Y, Z.").unwrap().unwrap();
-		assert_eq!(v.0.len(), 3);
-		assert_eq!(v.0[0].name.as_str(), "X");
-		assert_eq!(v.0[1].name.as_str(), "Y");
-		assert_eq!(v.0[2].name.as_str(), "Z");
-		assert_eq!(v.1, ".");
-
-		let v = variable_declarations("X , Y , Z.").unwrap().unwrap();
-		assert_eq!(v.0.len(), 3);
-		assert_eq!(v.0[0].name.as_str(), "X");
-		assert_eq!(v.0[1].name.as_str(), "Y");
-		assert_eq!(v.0[2].name.as_str(), "Z");
-		assert_eq!(v.1, ".");
-
-		assert!(variable_declarations("test").unwrap().is_none());
-		assert!(variable_declarations("X, test").is_err());
-		assert!(variable_declarations("X ,test").is_err());
-		assert!(variable_declarations("X,Y,Z, test").is_err());
-		assert!(variable_declarations("X,Y,Z ,test").is_err());
-	}
-}

src/parse/tokens.rs

@@ -1,641 +0,0 @@
-fn substring_offset(substring: &str, string: &str) -> usize
-{
-	substring.as_ptr() as usize - string.as_ptr() as usize
-}
-
-pub fn trim_start(mut input: &str) -> &str
-{
-	loop
-	{
-		let original_input = input;
-
-		input = input.trim_start();
-
-		let mut input_characters = input.chars();
-
-		if let Some('#') = input_characters.next()
-		{
-			input = input_characters.as_str();
-
-			match (input.find('\n'), input.find('\r'))
-			{
-				(Some(newline_index), Some(carriage_return_index)) =>
-				{
-					let split_index = std::cmp::min(newline_index, carriage_return_index);
-					input = input.split_at(split_index).1;
-				},
-				(Some(split_index), _)
-				| (_, Some(split_index)) => input = input.split_at(split_index).1,
-				_ => input = &input[..input.len()],
-			}
-		}
-
-		if input.is_empty() || input == original_input
-		{
-			break;
-		}
-	}
-
-	input
-}
-
-#[derive(Clone, Copy, Eq, PartialEq)]
-pub(crate) enum Keyword
-{
-	And,
-	Exists,
-	False,
-	ForAll,
-	Infimum,
-	Not,
-	Or,
-	Supremum,
-	True,
-}
-
-impl std::fmt::Debug for Keyword
-{
-	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		match &self
-		{
-			Self::And => write!(formatter, "and"),
-			Self::Exists => write!(formatter, "exists"),
-			Self::False => write!(formatter, "false"),
-			Self::ForAll => write!(formatter, "forall"),
-			Self::Infimum => write!(formatter, "inf"),
-			Self::Not => write!(formatter, "not"),
-			Self::Or => write!(formatter, "or"),
-			Self::Supremum => write!(formatter, "sup"),
-			Self::True => write!(formatter, "true"),
-		}
-	}
-}
-
-#[derive(Clone, Copy, Eq, PartialEq)]
-pub(crate) enum Symbol
-{
-	ArrowLeft,
-	ArrowLeftAndRight,
-	ArrowRight,
-	Comma,
-	Division,
-	Equal,
-	Exponentiation,
-	Greater,
-	GreaterOrEqual,
-	Less,
-	LessOrEqual,
-	Minus,
-	Multiplication,
-	NotEqual,
-	Percent,
-	Plus,
-	VerticalBar,
-}
-
-impl std::fmt::Debug for Symbol
-{
-	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		match &self
-		{
-			Self::ArrowLeft => write!(formatter, "<-"),
-			Self::ArrowLeftAndRight => write!(formatter, "<->"),
-			Self::ArrowRight => write!(formatter, "->"),
-			Self::Comma => write!(formatter, ","),
-			Self::Division => write!(formatter, "/"),
-			Self::Equal => write!(formatter, "="),
-			Self::Exponentiation => write!(formatter, "**"),
-			Self::Greater => write!(formatter, ">"),
-			Self::GreaterOrEqual => write!(formatter, ">="),
-			Self::Less => write!(formatter, "<"),
-			Self::LessOrEqual => write!(formatter, "<="),
-			Self::Minus => write!(formatter, "-"),
-			Self::Multiplication => write!(formatter, "*"),
-			Self::NotEqual => write!(formatter, "!="),
-			Self::Percent => write!(formatter, "%"),
-			Self::Plus => write!(formatter, "+"),
-			Self::VerticalBar => write!(formatter, "|"),
-		}
-	}
-}
-
-#[derive(Clone, Copy, Eq, PartialEq)]
-pub(crate) enum Token<'i>
-{
-	Identifier(&'i str),
-	Number(usize),
-	ParenthesizedExpression(&'i str),
-	Symbol(Symbol),
-}
-
-fn is_identifier_start_character(character: char) -> bool
-{
-	character.is_ascii_alphabetic()
-}
-
-fn is_identifier_body_character(character: char) -> bool
-{
-	match character
-	{
-		'_' => true,
-		_ if character.is_ascii_alphanumeric() => true,
-		_ => false,
-	}
-}
-
-pub fn identifier(input: &str) -> Option<(&str, &str)>
-{
-	let mut characters = input.char_indices();
-
-	let first_character = loop
-	{
-		match characters.next()
-		{
-			Some((_, '_')) => continue,
-			Some((_, character)) => break Some(character),
-			None => break None,
-		}
-	}?;
-
-	if !is_identifier_start_character(first_character)
-	{
-		return None;
-	}
-
-	loop
-	{
-		match characters.next()
-		{
-			None => return Some((input, characters.as_str())),
-			Some((character_index, character)) =>
-			{
-				if !is_identifier_body_character(character)
-				{
-					return Some(input.split_at(character_index));
-				}
-			},
-		}
-	}
-}
-
-pub(crate) fn is_keyword(identifier: &str) -> bool
-{
-	match identifier
-	{
-		"and"
-		| "exists"
-		| "false"
-		| "forall"
-		| "inf"
-		| "not"
-		| "or"
-		| "sup"
-		| "true" => true,
-		_ => false,
-	}
-}
-
-fn number_string(input: &str) -> Option<(&str, &str)>
-{
-	let mut characters = input.char_indices();
-
-	let (_, character) = match characters.next()
-	{
-		Some(characters_next) => characters_next,
-		None => return None,
-	};
-
-	if !character.is_ascii_digit()
-	{
-		return None;
-	}
-
-	loop
-	{
-		match characters.next()
-		{
-			None => return Some((input, characters.as_str())),
-			Some((character_index, character)) =>
-			{
-				if !character.is_ascii_digit()
-				{
-					return Some(input.split_at(character_index));
-				}
-			},
-		}
-	}
-}
-
-pub fn number(input: &str) -> Result<Option<(usize, &str)>, crate::parse::Error>
-{
-	let (number_string, remaining_input) = match number_string(input)
-	{
-		Some(number_string) => number_string,
-		None => return Ok(None),
-	};
-
-	let number = number_string.parse()
-		.map_err(|error| crate::parse::Error::new_parse_number(input,
-			crate::parse::error::Location::new(0, Some(0)), error))?;
-
-	Ok(Some((number, remaining_input)))
-}
-
-pub(crate) fn symbol(input: &str) -> Option<(Symbol, &str)>
-{
-	let mut characters = input.char_indices();
-
-	let (_, character) = match characters.next()
-	{
-		Some(characters_next) => characters_next,
-		None => return None,
-	};
-
-	let remaining_input = characters.as_str();
-
-	match character
-	{
-		',' => Some((Symbol::Comma, remaining_input)),
-		// <->, <-, <=, <
-		'=' => Some((Symbol::Equal, remaining_input)),
-		// !=
-		'!' => match characters.next()
-		{
-			Some((_, '=')) => Some((Symbol::NotEqual, characters.as_str())),
-			_ => None,
-		},
-		'<' => match characters.next()
-		{
-			Some((_, '-')) =>
-			{
-				let remaining_input = characters.as_str();
-
-				match characters.next()
-				{
-					Some((_, '>')) => Some((Symbol::ArrowLeftAndRight, characters.as_str())),
-					_ => Some((Symbol::ArrowLeft, remaining_input)),
-				}
-			},
-			Some((_, '=')) => Some((Symbol::LessOrEqual, characters.as_str())),
-			_ => Some((Symbol::Less, remaining_input)),
-		},
-		// >=, >
-		'>' => match characters.next()
-		{
-			Some((_, '=')) => Some((Symbol::GreaterOrEqual, characters.as_str())),
-			_ => Some((Symbol::Greater, remaining_input)),
-		},
-		'+' => Some((Symbol::Plus, remaining_input)),
-		// ->, -
-		'-' => match characters.next()
-		{
-			Some((_, '>')) => Some((Symbol::ArrowRight, characters.as_str())),
-			_ => Some((Symbol::Minus, remaining_input)),
-		},
-		// **, *
-		'*' => match characters.next()
-		{
-			Some((_, '*')) => Some((Symbol::Exponentiation, characters.as_str())),
-			_ => Some((Symbol::Multiplication, remaining_input)),
-		},
-		'/' => Some((Symbol::Division, remaining_input)),
-		'%' => Some((Symbol::Percent, remaining_input)),
-		'|' => Some((Symbol::VerticalBar, remaining_input)),
-		_ => None,
-	}
-}
-
-pub(crate) fn parenthesized_expression(input: &str)
-	-> Result<Option<(&str, &str)>, crate::parse::Error>
-{
-	let mut characters = input.chars();
-
-	let (first_character, remaining_input) = match characters.next()
-	{
-		Some(first_character) => (first_character, characters.as_str()),
-		None => return Ok(None),
-	};
-
-	if first_character != '('
-	{
-		return Ok(None);
-	}
-
-	let mut characters = remaining_input.char_indices();
-	let mut number_of_open_parentheses = 1;
-
-	while let Some((character_index, character)) = characters.next()
-	{
-		match character
-		{
-			'(' => number_of_open_parentheses += 1,
-			')' => number_of_open_parentheses -= 1,
-			_ => (),
-		}
-
-		if number_of_open_parentheses == 0
-		{
-			let position_of_closing_parenthesis = character_index;
-			let (parenthesized_expression, _) =
-				remaining_input.split_at(position_of_closing_parenthesis);
-			let remaining_input = characters.as_str();
-
-			return Ok(Some((parenthesized_expression, remaining_input)));
-		}
-	}
-
-	Err(crate::parse::Error::new_unmatched_parenthesis(
-		crate::parse::error::Location::new(0, Some(1))))
-}
-
-pub(crate) struct Tokens<'i, F>
-{
-	original_input: &'i str,
-	input: &'i str,
-	previous_index: usize,
-	reached_end_of_stream: bool,
-	functor: F,
-}
-
-impl<'i> Tokens<'i, ()>
-{
-	pub fn new_iter(input: &'i str) -> Tokens<'i, impl FnMut(Token<'i>) -> Option<Token<'i>>>
-	{
-		Tokens::new_filter_map(input, |x| Some(x))
-	}
-
-	pub fn new_filter<P>(input: &'i str, mut predicate: P)
-		-> Tokens<'i, impl FnMut(Token<'i>) -> Option<Token<'i>>>
-	where
-		P: FnMut(&Token<'i>) -> bool,
-	{
-		Tokens::new_filter_map(input,
-			move |x|
-			{
-				if predicate(&x)
-				{
-					Some(x)
-				}
-				else
-				{
-					None
-				}
-			})
-	}
-}
-
-impl<'i, F> Tokens<'i, F>
-{
-	pub fn new_filter_map(input: &'i str, functor: F) -> Self
-	{
-		Self
-		{
-			original_input: input,
-			input,
-			previous_index: 0,
-			reached_end_of_stream: false,
-			functor,
-		}
-	}
-
-	fn next_token(&mut self) -> Option<Result<(usize, usize, Token<'i>), crate::parse::Error>>
-	{
-		self.input = trim_start(self.input);
-		let index_left = substring_offset(self.input, self.original_input);
-
-		let first_character = match self.input.chars().next()
-		{
-			None => return None,
-			Some(first_character) => first_character,
-		};
-
-		if self.input.starts_with(")")
-		{
-			return Some(Err(crate::parse::Error::new_unmatched_parenthesis(
-				crate::parse::error::Location::new(0, Some(1)))));
-		}
-
-		match parenthesized_expression(self.input)
-		{
-			Ok(Some((parenthesized_expression, remaining_input))) =>
-			{
-				self.input = remaining_input;
-				let index_right = substring_offset(self.input, self.original_input);
-
-				return Some(Ok((index_left, index_right,
-					Token::ParenthesizedExpression(parenthesized_expression))));
-			},
-			Ok(None) => (),
-			Err(error) => return Some(Err(error)),
-		}
-
-		match number(self.input)
-		{
-			Ok(Some((number, remaining_input))) =>
-			{
-				self.input = remaining_input;
-				let index_right = substring_offset(self.input, self.original_input);
-
-				return Some(Ok((index_left, index_right, Token::Number(number))));
-			},
-			Ok(None) => (),
-			Err(error) => return Some(Err(error)),
-		}
-
-		if let Some((identifier, remaining_input)) = identifier(self.input)
-		{
-			self.input = remaining_input;
-			let index_right = substring_offset(self.input, self.original_input);
-
-			return Some(Ok((index_left, index_right, Token::Identifier(identifier))));
-		}
-
-		if let Some((symbol, remaining_input)) = symbol(self.input)
-		{
-			self.input = remaining_input;
-			let index_right = substring_offset(self.input, self.original_input);
-
-			return Some(Ok((index_left, index_right, Token::Symbol(symbol))));
-		}
-
-		return Some(Err(crate::parse::Error::new_character_not_allowed(first_character,
-			crate::parse::error::Location::new(0, Some(0)))));
-	}
-
-	pub fn remaining_input(&mut self) -> Option<&'i str>
-	{
-		if self.reached_end_of_stream
-		{
-			return None;
-		}
-
-		let remaining_input = self.original_input[self.previous_index..].trim();
-		self.reached_end_of_stream = true;
-
-		Some(remaining_input)
-	}
-
-	pub fn split(self) -> TokenSplit<Self>
-	{
-		TokenSplit::new(self)
-	}
-}
-
-impl<'i, F, G> std::iter::Iterator for Tokens<'i, F>
-where
-	F: FnMut(Token<'i>) -> Option<G>,
-{
-	type Item = Result<(&'i str, G), crate::parse::Error>;
-
-	fn next(&mut self) -> Option<Self::Item>
-	{
-		if self.previous_index == self.original_input.len()
-		{
-			return None;
-		}
-
-		loop
-		{
-			match self.next_token()
-			{
-				Some(Ok((index_left, index_right, token))) =>
-				{
-					let token = match (self.functor)(token)
-					{
-						None => continue,
-						Some(token) => token,
-					};
-
-					let input_left = self.original_input[self.previous_index..index_left].trim();
-
-					self.previous_index = index_right;
-
-					return Some(Ok((input_left, token)));
-				},
-				Some(Err(error)) => return Some(Err(error)),
-				None => return None,
-			}
-		}
-	}
-}
-
-pub(crate) struct TokenSplit<T>
-{
-	tokens: T,
-}
-
-impl TokenSplit<()>
-{
-	pub fn new<T>(tokens: T) -> TokenSplit<T>
-	{
-		TokenSplit
-		{
-			tokens,
-		}
-	}
-}
-
-impl<'i, F, G> std::iter::Iterator for TokenSplit<Tokens<'i, F>>
-where
-	F: FnMut(Token<'i>) -> Option<G>,
-{
-	type Item = Result<&'i str, crate::parse::Error>;
-
-	fn next(&mut self) -> Option<Self::Item>
-	{
-		match self.tokens.next()
-		{
-			Some(Ok((input_before, _))) => Some(Ok(input_before)),
-			Some(Err(error)) => Some(Err(error)),
-			None => match self.tokens.remaining_input()
-			{
-				Some(remaining_input) => Some(Ok(remaining_input)),
-				None => None,
-			},
-		}
-	}
-}
-
-#[cfg(test)]
-mod tests
-{
-	use super::*;
-
-	#[test]
-	fn tokenize_identifier()
-	{
-		assert_eq!(identifier("test").unwrap(), ("test", ""));
-		assert_eq!(identifier("test2").unwrap(), ("test2", ""));
-		assert_eq!(identifier("Test").unwrap(), ("Test", ""));
-		assert_eq!(identifier("Test2").unwrap(), ("Test2", ""));
-		assert_eq!(identifier("_test").unwrap(), ("_test", ""));
-		assert_eq!(identifier("_test2").unwrap(), ("_test2", ""));
-		assert_eq!(identifier("__test").unwrap(), ("__test", ""));
-		assert_eq!(identifier("__test2").unwrap(), ("__test2", ""));
-		assert_eq!(identifier("test, test").unwrap(), ("test", ", test"));
-		assert_eq!(identifier("test2, test").unwrap(), ("test2", ", test"));
-		assert_eq!(identifier("Test, Test").unwrap(), ("Test", ", Test"));
-		assert_eq!(identifier("Test2, Test").unwrap(), ("Test2", ", Test"));
-		assert_eq!(identifier("_test, _test").unwrap(), ("_test", ", _test"));
-		assert_eq!(identifier("_test2, _test").unwrap(), ("_test2", ", _test"));
-		assert_eq!(identifier("__test, __test").unwrap(), ("__test", ", __test"));
-		assert_eq!(identifier("__test2, __test").unwrap(), ("__test2", ", __test"));
-		assert!(identifier("2test, test").is_none());
-		assert!(identifier("#test, test").is_none());
-		assert!(identifier("$test, test").is_none());
-		assert!(identifier(",test, test").is_none());
-	}
-
-	#[test]
-	fn tokenize_primitives()
-	{
-		assert_eq!(parenthesized_expression("(foo bar baz) test").unwrap(),
-			Some(("foo bar baz", " test")));
-		assert!(parenthesized_expression("( | asd#0231(asd|asd) test").is_err());
-		assert_eq!(parenthesized_expression("( | asd#0231(asd|asd) ) test").unwrap(),
-			Some((" | asd#0231(asd|asd) ", " test")));
-		assert_eq!(parenthesized_expression("( | a)sd#0231(asd|asd)  test").unwrap(),
-			Some((" | a", "sd#0231(asd|asd)  test")));
-
-		assert_eq!(number("1234, ").unwrap(), Some((1234, ", ")));
-		assert_eq!(number("1234.5, ").unwrap(), Some((1234, ".5, ")));
-		assert_eq!(number("-1234, ").unwrap(), None);
-		assert_eq!(number("a1234, ").unwrap(), None);
-
-		assert_eq!(symbol("<-"), Some((Symbol::ArrowLeft, "")));
-		assert_eq!(symbol("<->"), Some((Symbol::ArrowLeftAndRight, "")));
-		assert_eq!(symbol("->"), Some((Symbol::ArrowRight, "")));
-		assert_eq!(symbol(","), Some((Symbol::Comma, "")));
-		assert_eq!(symbol("/"), Some((Symbol::Division, "")));
-		assert_eq!(symbol("="), Some((Symbol::Equal, "")));
-		assert_eq!(symbol("**"), Some((Symbol::Exponentiation, "")));
-		assert_eq!(symbol(">"), Some((Symbol::Greater, "")));
-		assert_eq!(symbol(">="), Some((Symbol::GreaterOrEqual, "")));
-		assert_eq!(symbol("<"), Some((Symbol::Less, "")));
-		assert_eq!(symbol("<="), Some((Symbol::LessOrEqual, "")));
-		assert_eq!(symbol("-"), Some((Symbol::Minus, "")));
-		assert_eq!(symbol("*"), Some((Symbol::Multiplication, "")));
-		assert_eq!(symbol("!="), Some((Symbol::NotEqual, "")));
-		assert_eq!(symbol("+"), Some((Symbol::Plus, "")));
-		assert_eq!(symbol("|"), Some((Symbol::VerticalBar, "")));
-
-		assert_eq!(symbol("<-a"), Some((Symbol::ArrowLeft, "a")));
-		assert_eq!(symbol("<->a"), Some((Symbol::ArrowLeftAndRight, "a")));
-		assert_eq!(symbol("->a"), Some((Symbol::ArrowRight, "a")));
-		assert_eq!(symbol(",a"), Some((Symbol::Comma, "a")));
-		assert_eq!(symbol("/a"), Some((Symbol::Division, "a")));
-		assert_eq!(symbol("=a"), Some((Symbol::Equal, "a")));
-		assert_eq!(symbol("**a"), Some((Symbol::Exponentiation, "a")));
-		assert_eq!(symbol(">a"), Some((Symbol::Greater, "a")));
-		assert_eq!(symbol(">=a"), Some((Symbol::GreaterOrEqual, "a")));
-		assert_eq!(symbol("<a"), Some((Symbol::Less, "a")));
-		assert_eq!(symbol("<=a"), Some((Symbol::LessOrEqual, "a")));
-		assert_eq!(symbol("-a"), Some((Symbol::Minus, "a")));
-		assert_eq!(symbol("*a"), Some((Symbol::Multiplication, "a")));
-		assert_eq!(symbol("!=a"), Some((Symbol::NotEqual, "a")));
-		assert_eq!(symbol("+a"), Some((Symbol::Plus, "a")));
-		assert_eq!(symbol("|a"), Some((Symbol::VerticalBar, "a")));
-	}
-}

src/utils.rs

@@ -1,102 +0,0 @@
-use crate::flavor::VariableDeclaration as _;
-
-pub struct BoundVariableDeclarations<'p, F>
-where
-	F: crate::flavor::Flavor,
-{
-	pub parent: &'p VariableDeclarationStackLayer<'p, F>,
-	pub variable_declarations: std::rc::Rc<crate::VariableDeclarations<F>>,
-}
-
-impl<'p, F> BoundVariableDeclarations<'p, F>
-where
-	F: crate::flavor::Flavor,
-{
-	pub fn new(parent: &'p VariableDeclarationStackLayer<'p, F>,
-		variable_declarations: std::rc::Rc<crate::VariableDeclarations<F>>) -> Self
-	{
-		Self
-		{
-			parent,
-			variable_declarations,
-		}
-	}
-}
-
-pub enum VariableDeclarationStackLayer<'p, F>
-where
-	F: crate::flavor::Flavor,
-{
-	Free(std::cell::RefCell<crate::VariableDeclarations<F>>),
-	Bound(BoundVariableDeclarations<'p, F>),
-}
-
-impl<'p, F> VariableDeclarationStackLayer<'p, F>
-where
-	F: crate::flavor::Flavor,
-{
-	pub fn free() -> Self
-	{
-		Self::Free(std::cell::RefCell::new(vec![]))
-	}
-
-	pub fn bound(parent: &'p VariableDeclarationStackLayer<'p, F>,
-		variable_declarations: std::rc::Rc<crate::VariableDeclarations<F>>) -> Self
-	{
-		Self::Bound(BoundVariableDeclarations::new(parent, variable_declarations))
-	}
-
-	pub fn find(&self, variable_name: &str) -> Option<std::rc::Rc<F::VariableDeclaration>>
-	{
-		match self
-		{
-			VariableDeclarationStackLayer::Free(free_variable_declarations) =>
-			{
-				if let Some(variable_declaration) = free_variable_declarations.borrow().iter()
-					.find(|x| x.matches_name(variable_name))
-				{
-					return Some(std::rc::Rc::clone(&variable_declaration));
-				}
-
-				None
-			},
-			VariableDeclarationStackLayer::Bound(bound_variable_declarations) =>
-			{
-				if let Some(variable_declaration) = bound_variable_declarations
-					.variable_declarations.iter()
-					.find(|x| x.matches_name(variable_name))
-				{
-					return Some(std::rc::Rc::clone(&variable_declaration));
-				}
-
-				bound_variable_declarations.parent.find(variable_name)
-			},
-		}
-	}
-
-	pub fn free_variable_declarations_do_mut<F1, F2>(&self, f: F1) -> F2
-	where
-		F1: Fn(&mut crate::VariableDeclarations<F>) -> F2,
-	{
-		match self
-		{
-			VariableDeclarationStackLayer::Free(free_variable_declarations)
-				=> f(&mut free_variable_declarations.borrow_mut()),
-			VariableDeclarationStackLayer::Bound(bound_variable_declarations)
-				=> bound_variable_declarations.parent.free_variable_declarations_do_mut(f),
-		}
-	}
-
-	pub fn free_variable_declarations_do<F1, F2>(&self, f: F1) -> F2
-	where
-		F1: Fn(&crate::VariableDeclarations<F>) -> F2,
-	{
-		match self
-		{
-			VariableDeclarationStackLayer::Free(free_variable_declarations)
-				=> f(&free_variable_declarations.borrow()),
-			VariableDeclarationStackLayer::Bound(bound_variable_declarations)
-				=> bound_variable_declarations.parent.free_variable_declarations_do(f),
-		}
-	}
-}