Remove unneeded trait methods

Implement name parsing

Start parsing terms

Implement word boundaries

Implement strings

Add pipe character to allowed word boundaries

Implement booleans

Require word boundaries around names

Implement variable parsing

Finish implementing term parsing

Add term parsing test

Test associativity of multiplication

Make parse feature the default

Fix term parsing and finish tests

Start parsing formulas

Continue parsing formulas

Finish implementing formula parsing

Move boolean parser to separate module

Move integer parser to separate module

Move special integer parser to separate module

Move string parser to separate module

Address warnings

Fix negation parser

Refactor term parser tests

Address clippy warning

Disallow reserved keywords as names

Add missing word boundary character

Check that names don’t start with special characters

Minor refactoring

Add note

Test conjunction parser

Test disjunction parser

Parentheses for stronger checks

Add note

Fix implication parser and output

Split formatting functionality into two files

Test term formatting

Add unit test for function declaration formatting

Work in progress

Fix implication formatting

Refactor precedence rules

Start testing formula formatter

Minor formatting

Test remaining formula types

Add unit tests for precedence-0 formulas and lower

Before larger refactoring

Refactor precedence rules for formulas

Remove ChildPosition enum

Fix

Address warnings

Remove unneeded precedence implementation

Test negation

Test quantified formulas

Clean up tests

Clean up tests

Test conjunction

Test disjunction

Start testing implications

Refactor parenthesis requirement check

Fix precedence of implication

Continue testing implication

Test biconditionals

Experimental method for testing all permutations

Rewrite tests for clarity

Rewrite tests for clarity

Add type annotations

Rewrite tests for clarity

Reorganize tests

Finish testing biconditionals

Support empty n-aries

Support quantified expressions with 0 parameters

Rewrite term formatting tests for clarity

Reorganize term formatter tests

Refactor parenthesis rules for terms

Remove unneeded parentheses enum

Refactoring

Refactoring

Minor clean-up

Minor clean-up

Simplify representation of quantified formulas

Remove redundant indirection

Remove redundant indirection

Cargo.toml

@@ -13,8 +13,4 @@ license = "MIT"
 edition = "2018"
 
 [dependencies]
-nom = {version = "5.1", optional = true}
-
-[features]
-default = ["parse"]
-parse = ["nom"]
+log = "0.4"

src/ast.rs

@@ -1,3 +1,5 @@
+use crate::flavor::{FunctionDeclaration as _, PredicateDeclaration as _};
+
 // Operators
 
 #[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
@@ -59,7 +61,8 @@ impl FunctionDeclaration
 	}
 }
 
-pub type FunctionDeclarations = std::collections::BTreeSet<std::rc::Rc<FunctionDeclaration>>;
+pub type FunctionDeclarations<F> =
+	std::collections::BTreeSet<std::rc::Rc<<F as crate::flavor::Flavor>::FunctionDeclaration>>;
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct PredicateDeclaration
@@ -80,7 +83,8 @@ impl PredicateDeclaration
 	}
 }
 
-pub type PredicateDeclarations = std::collections::BTreeSet<std::rc::Rc<PredicateDeclaration>>;
+pub type PredicateDeclarations<F> =
+	std::collections::BTreeSet<std::rc::Rc<<F as crate::flavor::Flavor>::PredicateDeclaration>>;
 
 pub struct VariableDeclaration
 {
@@ -90,10 +94,10 @@ pub struct VariableDeclaration
 impl std::cmp::PartialEq for VariableDeclaration
 {
 	#[inline(always)]
-	fn eq(&self, other: &VariableDeclaration) -> bool
+	fn eq(&self, other: &Self) -> bool
 	{
-		let l = self as *const VariableDeclaration;
-		let r = other as *const VariableDeclaration;
+		let l = self as *const Self;
+		let r = other as *const Self;
 
 		l.eq(&r)
 	}
@@ -149,21 +153,26 @@ impl VariableDeclaration
 	}
 }
 
-pub type VariableDeclarations = Vec<std::rc::Rc<VariableDeclaration>>;
+pub type VariableDeclarations<F> =
+	Vec<std::rc::Rc<<F as crate::flavor::Flavor>::VariableDeclaration>>;
 
 // Terms
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct BinaryOperation
+pub struct BinaryOperation<F>
+where
+	F: crate::flavor::Flavor,
 {
 	pub operator: BinaryOperator,
-	pub left: Box<Term>,
-	pub right: Box<Term>,
+	pub left: Box<Term<F>>,
+	pub right: Box<Term<F>>,
 }
 
-impl BinaryOperation
+impl<F> BinaryOperation<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub fn new(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
+	pub fn new(operator: BinaryOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self
 		{
@@ -175,18 +184,22 @@ impl BinaryOperation
 }
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct Function
+pub struct Function<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub declaration: std::rc::Rc<FunctionDeclaration>,
-	pub arguments: Terms,
+	pub declaration: std::rc::Rc<F::FunctionDeclaration>,
+	pub arguments: Terms<F>,
 }
 
-impl Function
+impl<F> Function<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub fn new(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Terms) -> Self
+	pub fn new(declaration: std::rc::Rc<F::FunctionDeclaration>, arguments: Terms<F>) -> Self
 	{
-		assert_eq!(declaration.arity, arguments.len(),
-			"function has a different number of arguments then declared");
+		assert_eq!(declaration.arity(), arguments.len(),
+			"function has a different number of arguments than declared");
 
 		Self
 		{
@@ -204,15 +217,19 @@ pub enum SpecialInteger
 }
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct UnaryOperation
+pub struct UnaryOperation<F>
+where
+	F: crate::flavor::Flavor,
 {
 	pub operator: UnaryOperator,
-	pub argument: Box<Term>,
+	pub argument: Box<Term<F>>,
 }
 
-impl UnaryOperation
+impl<F> UnaryOperation<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub fn new(operator: UnaryOperator, argument: Box<Term>) -> Self
+	pub fn new(operator: UnaryOperator, argument: Box<Term<F>>) -> Self
 	{
 		Self
 		{
@@ -223,14 +240,18 @@ impl UnaryOperation
 }
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct Variable
+pub struct Variable<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub declaration: std::rc::Rc<VariableDeclaration>,
+	pub declaration: std::rc::Rc<F::VariableDeclaration>,
 }
 
-impl Variable
+impl<F> Variable<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub fn new(declaration: std::rc::Rc<VariableDeclaration>) -> Self
+	pub fn new(declaration: std::rc::Rc<F::VariableDeclaration>) -> Self
 	{
 		Self
 		{
@@ -242,16 +263,20 @@ impl Variable
 // Formulas
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct Compare
+pub struct Compare<F>
+where
+	F: crate::flavor::Flavor,
 {
 	pub operator: ComparisonOperator,
-	pub left: Box<Term>,
-	pub right: Box<Term>,
+	pub left: Box<Term<F>>,
+	pub right: Box<Term<F>>,
 }
 
-impl Compare
+impl<F> Compare<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub fn new(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
+	pub fn new(operator: ComparisonOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self
 		{
@@ -263,15 +288,19 @@ impl Compare
 }
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct QuantifiedFormula
+pub struct QuantifiedFormula<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub parameters: std::rc::Rc<VariableDeclarations>,
-	pub argument: Box<Formula>,
+	pub parameters: std::rc::Rc<VariableDeclarations<F>>,
+	pub argument: Box<Formula<F>>,
 }
 
-impl QuantifiedFormula
+impl<F> QuantifiedFormula<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
+	pub fn new(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
 	{
 		Self
 		{
@@ -282,16 +311,21 @@ impl QuantifiedFormula
 }
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct Implies
+pub struct Implies<F>
+where
+	F: crate::flavor::Flavor,
 {
 	pub direction: ImplicationDirection,
-	pub antecedent: Box<Formula>,
-	pub implication: Box<Formula>,
+	pub antecedent: Box<Formula<F>>,
+	pub implication: Box<Formula<F>>,
 }
 
-impl Implies
+impl<F> Implies<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub fn new(direction: ImplicationDirection, antecedent: Box<Formula>, implication: Box<Formula>)
+	pub fn new(direction: ImplicationDirection, antecedent: Box<Formula<F>>,
+		implication: Box<Formula<F>>)
 		-> Self
 	{
 		Self
@@ -304,18 +338,22 @@ impl Implies
 }
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct Predicate
+pub struct Predicate<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub declaration: std::rc::Rc<PredicateDeclaration>,
-	pub arguments: Terms,
+	pub declaration: std::rc::Rc<F::PredicateDeclaration>,
+	pub arguments: Terms<F>,
 }
 
-impl Predicate
+impl<F> Predicate<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub fn new(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Terms) -> Self
+	pub fn new(declaration: std::rc::Rc<F::PredicateDeclaration>, arguments: Terms<F>) -> Self
 	{
-		assert_eq!(declaration.arity, arguments.len(),
-			"predicate has a different number of arguments then declared");
+		assert_eq!(declaration.arity(), arguments.len(),
+			"predicate has a different number of arguments than declared");
 
 		Self
 		{
@@ -328,33 +366,37 @@ impl Predicate
 // Variants
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub enum Term
+pub enum Term<F>
+where
+	F: crate::flavor::Flavor,
 {
-	BinaryOperation(BinaryOperation),
+	BinaryOperation(BinaryOperation<F>),
 	Boolean(bool),
-	Function(Function),
+	Function(Function<F>),
 	Integer(i32),
 	SpecialInteger(SpecialInteger),
 	String(String),
-	UnaryOperation(UnaryOperation),
-	Variable(Variable),
+	UnaryOperation(UnaryOperation<F>),
+	Variable(Variable<F>),
 }
 
-pub type Terms = Vec<Term>;
+pub type Terms<F> = Vec<Term<F>>;
 
-impl Term
+impl<F> Term<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub fn absolute_value(argument: Box<Term>) -> Self
+	pub fn absolute_value(argument: Box<Term<F>>) -> Self
 	{
 		Self::unary_operation(UnaryOperator::AbsoluteValue, argument)
 	}
 
-	pub fn add(left: Box<Term>, right: Box<Term>) -> Self
+	pub fn add(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self::binary_operation(BinaryOperator::Add, left, right)
 	}
 
-	pub fn binary_operation(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
+	pub fn binary_operation(operator: BinaryOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self::BinaryOperation(BinaryOperation::new(operator, left, right))
 	}
@@ -364,12 +406,12 @@ impl Term
 		Self::Boolean(value)
 	}
 
-	pub fn divide(left: Box<Term>, right: Box<Term>) -> Self
+	pub fn divide(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self::binary_operation(BinaryOperator::Divide, left, right)
 	}
 
-	pub fn exponentiate(left: Box<Term>, right: Box<Term>) -> Self
+	pub fn exponentiate(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self::binary_operation(BinaryOperator::Exponentiate, left, right)
 	}
@@ -379,7 +421,7 @@ impl Term
 		Self::boolean(false)
 	}
 
-	pub fn function(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Terms) -> Self
+	pub fn function(declaration: std::rc::Rc<F::FunctionDeclaration>, arguments: Terms<F>) -> Self
 	{
 		Self::Function(Function::new(declaration, arguments))
 	}
@@ -394,17 +436,17 @@ impl Term
 		Self::Integer(value)
 	}
 
-	pub fn modulo(left: Box<Term>, right: Box<Term>) -> Self
+	pub fn modulo(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self::binary_operation(BinaryOperator::Modulo, left, right)
 	}
 
-	pub fn multiply(left: Box<Term>, right: Box<Term>) -> Self
+	pub fn multiply(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self::binary_operation(BinaryOperator::Multiply, left, right)
 	}
 
-	pub fn negative(argument: Box<Term>) -> Self
+	pub fn negative(argument: Box<Term<F>>) -> Self
 	{
 		Self::unary_operation(UnaryOperator::Negative, argument)
 	}
@@ -419,7 +461,7 @@ impl Term
 		Self::String(value)
 	}
 
-	pub fn subtract(left: Box<Term>, right: Box<Term>) -> Self
+	pub fn subtract(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self::binary_operation(BinaryOperator::Subtract, left, right)
 	}
@@ -434,37 +476,41 @@ impl Term
 		Self::boolean(true)
 	}
 
-	pub fn unary_operation(operator: UnaryOperator, argument: Box<Term>) -> Self
+	pub fn unary_operation(operator: UnaryOperator, argument: Box<Term<F>>) -> Self
 	{
 		Self::UnaryOperation(UnaryOperation::new(operator, argument))
 	}
 
-	pub fn variable(declaration: std::rc::Rc<VariableDeclaration>) -> Self
+	pub fn variable(declaration: std::rc::Rc<F::VariableDeclaration>) -> Self
 	{
 		Self::Variable(Variable::new(declaration))
 	}
 }
 
 #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub enum Formula
+pub enum Formula<F>
+where
+	F: crate::flavor::Flavor,
 {
-	And(Formulas),
+	And(Formulas<F>),
 	Boolean(bool),
-	Compare(Compare),
-	Exists(QuantifiedFormula),
-	ForAll(QuantifiedFormula),
-	IfAndOnlyIf(Formulas),
-	Implies(Implies),
-	Not(Box<Formula>),
-	Or(Formulas),
-	Predicate(Predicate),
+	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>),
 }
 
-pub type Formulas = Vec<Formula>;
+pub type Formulas<F> = Vec<Formula<F>>;
 
-impl Formula
+impl<F> Formula<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub fn and(arguments: Formulas) -> Self
+	pub fn and(arguments: Formulas<F>) -> Self
 	{
 		Self::And(arguments)
 	}
@@ -474,17 +520,17 @@ impl Formula
 		Self::Boolean(value)
 	}
 
-	pub fn compare(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
+	pub fn compare(operator: ComparisonOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self::Compare(Compare::new(operator, left, right))
 	}
 
-	pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
+	pub fn exists(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
 	{
 		Self::Exists(QuantifiedFormula::new(parameters, argument))
 	}
 
-	pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
+	pub fn equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self::compare(ComparisonOperator::Equal, left, right)
 	}
@@ -494,58 +540,58 @@ impl Formula
 		Self::boolean(false)
 	}
 
-	pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
+	pub fn for_all(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
 	{
 		Self::ForAll(QuantifiedFormula::new(parameters, argument))
 	}
 
-	pub fn greater(left: Box<Term>, right: Box<Term>) -> Self
+	pub fn greater(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self::compare(ComparisonOperator::Greater, left, right)
 	}
 
-	pub fn greater_or_equal(left: Box<Term>, right: Box<Term>) -> Self
+	pub fn greater_or_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self::compare(ComparisonOperator::GreaterOrEqual, left, right)
 	}
 
-	pub fn if_and_only_if(arguments: Formulas) -> Self
+	pub fn if_and_only_if(arguments: Formulas<F>) -> Self
 	{
 		Self::IfAndOnlyIf(arguments)
 	}
 
-	pub fn implies(direction: ImplicationDirection, antecedent: Box<Formula>,
-		consequent: Box<Formula>) -> Self
+	pub fn implies(direction: ImplicationDirection, antecedent: Box<Formula<F>>,
+		consequent: Box<Formula<F>>) -> Self
 	{
 		Self::Implies(Implies::new(direction, antecedent, consequent))
 	}
 
-	pub fn less(left: Box<Term>, right: Box<Term>) -> Self
+	pub fn less(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self::compare(ComparisonOperator::Less, left, right)
 	}
 
-	pub fn less_or_equal(left: Box<Term>, right: Box<Term>) -> Self
+	pub fn less_or_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self::compare(ComparisonOperator::LessOrEqual, left, right)
 	}
 
-	pub fn not(argument: Box<Formula>) -> Self
+	pub fn not(argument: Box<Formula<F>>) -> Self
 	{
 		Self::Not(argument)
 	}
 
-	pub fn not_equal(left: Box<Term>, right: Box<Term>) -> Self
+	pub fn not_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
 	{
 		Self::compare(ComparisonOperator::NotEqual, left, right)
 	}
 
-	pub fn or(arguments: Formulas) -> Self
+	pub fn or(arguments: Formulas<F>) -> Self
 	{
 		Self::Or(arguments)
 	}
 
-	pub fn predicate(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Terms) -> Self
+	pub fn predicate(declaration: std::rc::Rc<F::PredicateDeclaration>, arguments: Terms<F>) -> Self
 	{
 		Self::Predicate(Predicate::new(declaration, arguments))
 	}
@@ -555,3 +601,11 @@ impl Formula
 		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/error.rs

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

src/flavor.rs

@@ -0,0 +1,85 @@
+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,2 @@
-mod formulas;
-mod terms;
+pub mod formulas;
+pub mod terms;

src/format/formulas.rs

@@ -1,48 +1,72 @@
+use crate::flavor::{PredicateDeclaration as _, VariableDeclaration as _};
 use super::terms::*;
 
+impl std::fmt::Debug for crate::ComparisonOperator
+{
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		let operator_symbol = match self
+		{
+			Self::Less => "<",
+			Self::LessOrEqual => "<=",
+			Self::Greater => ">",
+			Self::GreaterOrEqual => ">=",
+			Self::Equal => "=",
+			Self::NotEqual => "!=",
+		};
+
+		write!(formatter, "{}", operator_symbol)
+	}
+}
+
 impl std::fmt::Debug for crate::ImplicationDirection
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
 		match &self
 		{
-			Self::LeftToRight => write!(format, "left to right"),
-			Self::RightToLeft => write!(format, "right to left"),
+			Self::LeftToRight => write!(formatter, "left to right"),
+			Self::RightToLeft => write!(formatter, "right to left"),
 		}
 	}
 }
 
 impl std::fmt::Debug for crate::PredicateDeclaration
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{}/{}", &self.name, self.arity)
+		write!(formatter, "{}/{}", &self.name, self.arity)
 	}
 }
 
 impl std::fmt::Display for crate::PredicateDeclaration
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{:?}", &self)
+		write!(formatter, "{:?}", &self)
 	}
 }
 
 #[derive(Clone, Copy, Eq, PartialEq)]
-enum FormulaPosition
+pub(crate) enum FormulaPosition
 {
 	Any,
 	ImpliesAntecedent,
 }
 
-struct FormulaDisplay<'formula>
+pub struct FormulaDisplay<'formula, F>
+where
+	F: crate::flavor::Flavor,
 {
-	formula: &'formula crate::Formula,
-	parent_formula: Option<&'formula crate::Formula>,
+	formula: &'formula crate::Formula<F>,
+	parent_formula: Option<&'formula crate::Formula<F>>,
 	position: FormulaPosition,
+	//declarations: &'d D,
 }
 
-impl<'formula> FormulaDisplay<'formula>
+impl<'formula, F> FormulaDisplay<'formula, F>
+where
+	F: crate::flavor::Flavor,
 {
 	fn requires_parentheses(&self) -> bool
 	{
@@ -112,9 +136,11 @@ impl<'formula> FormulaDisplay<'formula>
 	}
 }
 
-fn display_formula<'formula>(formula: &'formula crate::Formula,
-	parent_formula: Option<&'formula crate::Formula>, position: FormulaPosition)
-	-> FormulaDisplay<'formula>
+pub(crate) fn display_formula<'formula, F>(formula: &'formula crate::Formula<F>,
+	parent_formula: Option<&'formula crate::Formula<F>>, position: FormulaPosition)
+	-> FormulaDisplay<'formula, F>
+where
+	F: crate::flavor::Flavor,
 {
 	FormulaDisplay
 	{
@@ -124,15 +150,17 @@ fn display_formula<'formula>(formula: &'formula crate::Formula,
 	}
 }
 
-impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
+impl<'formula, F> std::fmt::Debug for FormulaDisplay<'formula, F>
+where
+	F: crate::flavor::Flavor,
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
 		let requires_parentheses = self.requires_parentheses();
 
 		if requires_parentheses
 		{
-			write!(format, "(")?;
+			write!(formatter, "(")?;
 		}
 
 		match &self.formula
@@ -141,23 +169,24 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 			{
 				if exists.parameters.is_empty()
 				{
-					write!(format, "{:?}", display_formula(&exists.argument, self.parent_formula,
-						self.position))?;
+					write!(formatter, "{:?}", display_formula::<F>(&exists.argument,
+						self.parent_formula, self.position))?;
 				}
 				else
 				{
-					write!(format, "exists")?;
+					write!(formatter, "exists")?;
 
 					let mut separator = " ";
 
 					for parameter in exists.parameters.iter()
 					{
-						write!(format, "{}{:?}", separator, parameter)?;
+						write!(formatter, "{}", separator)?;
+						parameter.display_name(formatter)?;
 
 						separator = ", "
 					}
 
-					write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula),
+					write!(formatter, " {:?}", display_formula(&exists.argument, Some(self.formula),
 						FormulaPosition::Any))?;
 				}
 			},
@@ -165,33 +194,34 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 			{
 				if for_all.parameters.is_empty()
 				{
-					write!(format, "{:?}", display_formula(&for_all.argument, self.parent_formula,
-						self.position))?;
+					write!(formatter, "{:?}", display_formula(&for_all.argument,
+						self.parent_formula, self.position))?;
 				}
 				else
 				{
-					write!(format, "forall")?;
+					write!(formatter, "forall")?;
 
 					let mut separator = " ";
 
 					for parameter in for_all.parameters.iter()
 					{
-						write!(format, "{}{:?}", separator, parameter)?;
+						write!(formatter, "{}", separator)?;
+						parameter.display_name(formatter)?;
 
 						separator = ", "
 					}
 
-					write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula),
-						FormulaPosition::Any))?;
+					write!(formatter, " {:?}", display_formula(&for_all.argument,
+						Some(self.formula), FormulaPosition::Any))?;
 				}
 			},
-			crate::Formula::Not(argument) => write!(format, "not {:?}",
+			crate::Formula::Not(argument) => write!(formatter, "not {:?}",
 				display_formula(argument, Some(self.formula), FormulaPosition::Any))?,
 			crate::Formula::And(arguments) =>
 			{
 				if arguments.is_empty()
 				{
-					write!(format, "true")?;
+					write!(formatter, "true")?;
 				}
 				else
 				{
@@ -205,7 +235,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 
 					for argument in arguments
 					{
-						write!(format, "{}{:?}", separator,
+						write!(formatter, "{}{:?}", separator,
 							display_formula(argument, parent_formula, position))?;
 
 						separator = " and "
@@ -216,7 +246,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 			{
 				if arguments.is_empty()
 				{
-					write!(format, "false")?;
+					write!(formatter, "false")?;
 				}
 				else
 				{
@@ -230,7 +260,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 
 					for argument in arguments
 					{
-						write!(format, "{}{:?}", separator,
+						write!(formatter, "{}{:?}", separator,
 							display_formula(argument, parent_formula, position))?;
 
 						separator = " or "
@@ -239,16 +269,16 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 			},
 			crate::Formula::Implies(crate::Implies{direction, antecedent, implication}) =>
 			{
-				let format_antecedent = |format: &mut std::fmt::Formatter| -> Result<_, _>
+				let format_antecedent = |formatter: &mut std::fmt::Formatter| -> Result<_, _>
 				{
-					write!(format, "{:?}",
+					write!(formatter, "{:?}",
 						display_formula(antecedent, Some(self.formula),
 							FormulaPosition::ImpliesAntecedent))
 				};
 
-				let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _>
+				let format_implication = |formatter: &mut std::fmt::Formatter| -> Result<_, _>
 				{
-					write!(format, "{:?}",
+					write!(formatter, "{:?}",
 						display_formula(implication, Some(self.formula), FormulaPosition::Any))
 				};
 
@@ -256,15 +286,15 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 				{
 					crate::ImplicationDirection::LeftToRight =>
 					{
-						format_antecedent(format)?;
-						write!(format, " -> ")?;
-						format_implication(format)?;
+						format_antecedent(formatter)?;
+						write!(formatter, " -> ")?;
+						format_implication(formatter)?;
 					},
 					crate::ImplicationDirection::RightToLeft =>
 					{
-						format_implication(format)?;
-						write!(format, " <- ")?;
-						format_antecedent(format)?;
+						format_implication(formatter)?;
+						write!(formatter, " <- ")?;
+						format_antecedent(formatter)?;
 					},
 				}
 			},
@@ -272,7 +302,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 			{
 				if arguments.is_empty()
 				{
-					write!(format, "true")?;
+					write!(formatter, "true")?;
 				}
 				else
 				{
@@ -286,7 +316,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 
 					for argument in arguments
 					{
-						write!(format, "{}{:?}", separator,
+						write!(formatter, "{}{:?}", separator,
 							display_formula(argument, parent_formula, position))?;
 
 						separator = " <-> "
@@ -305,66 +335,71 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 					crate::ComparisonOperator::NotEqual => "!=",
 				};
 
-				write!(format, "{:?} {} {:?}",
-					display_term(&compare.left, None, TermPosition::Any),
-					operator_string,
+				write!(formatter, "{:?} {} {:?}",
+					display_term(&compare.left, None, TermPosition::Any), operator_string,
 					display_term(&compare.right, None, TermPosition::Any))?;
 			},
-			crate::Formula::Boolean(true) => write!(format, "true")?,
-			crate::Formula::Boolean(false) => write!(format, "false")?,
+			crate::Formula::Boolean(true) => write!(formatter, "true")?,
+			crate::Formula::Boolean(false) => write!(formatter, "false")?,
 			crate::Formula::Predicate(predicate) =>
 			{
-				write!(format, "{}", predicate.declaration.name)?;
+				predicate.declaration.display_name(formatter)?;
 
 				if !predicate.arguments.is_empty()
 				{
-					write!(format, "(")?;
+					write!(formatter, "(")?;
 
 					let mut separator = "";
 
 					for argument in &predicate.arguments
 					{
-						write!(format, "{}{:?}", separator, display_term(argument, None,
+						write!(formatter, "{}{:?}", separator, display_term(argument, None,
 							TermPosition::Any))?;
 
 						separator = ", "
 					}
 
-					write!(format, ")")?;
+					write!(formatter, ")")?;
 				}
 			},
 		}
 
 		if requires_parentheses
 		{
-			write!(format, ")")?;
+			write!(formatter, ")")?;
 		}
 
 		Ok(())
 	}
 }
 
-impl<'formula> std::fmt::Display for FormulaDisplay<'formula>
+impl<'formula, F> std::fmt::Display for FormulaDisplay<'formula, F>
+where
+	F: crate::flavor::Flavor,
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{:?}", self)
+		write!(formatter, "{:?}", self)
 	}
 }
 
-impl std::fmt::Debug for crate::Formula
+impl<F> std::fmt::Debug for crate::Formula<F>
+where
+	F: crate::flavor::Flavor,
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{:?}", display_formula(&self, None, FormulaPosition::Any))
+		write!(formatter, "{:?}", display_formula(&self, None, FormulaPosition::Any))
 	}
 }
 
-impl std::fmt::Display for crate::Formula
+impl<F> std::fmt::Display for crate::Formula<F>
+where
+	F: crate::flavor::Flavor,
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{}", display_formula(&self, None, FormulaPosition::Any))
+		write!(formatter, "{}", display_formula(&self, None, FormulaPosition::Any))
 	}
 }
 
@@ -372,7 +407,10 @@ impl std::fmt::Display for crate::Formula
 mod tests
 {
 	use crate::*;
-	use crate::format::terms::tests::*;
+	use format::terms::tests::*;
+	type Formula = crate::Formula<flavor::DefaultFlavor>;
+	type Term = crate::Term<flavor::DefaultFlavor>;
+	type VariableDeclarations = crate::VariableDeclarations<flavor::DefaultFlavor>;
 
 	macro_rules! assert
 	{
@@ -407,7 +445,7 @@ mod tests
 		};
 	}
 
-	fn format(formula: Box<ast::Formula>) -> String
+	fn format(formula: Box<Formula>) -> String
 	{
 		format!("{}", formula)
 	}

src/format/terms.rs

@@ -1,52 +1,38 @@
+use crate::flavor::{FunctionDeclaration as _, VariableDeclaration as _};
+
 impl std::fmt::Debug for crate::SpecialInteger
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
 		match &self
 		{
-			Self::Infimum => write!(format, "#inf"),
-			Self::Supremum => write!(format, "#sup"),
+			Self::Infimum => write!(formatter, "#inf"),
+			Self::Supremum => write!(formatter, "#sup"),
 		}
 	}
 }
 
 impl std::fmt::Display for crate::SpecialInteger
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{:?}", &self)
+		write!(formatter, "{:?}", &self)
 	}
 }
 
 impl std::fmt::Debug for crate::FunctionDeclaration
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{}/{}", &self.name, self.arity)
+		write!(formatter, "{}/{}", &self.name, self.arity)
 	}
 }
 
 impl std::fmt::Display for crate::FunctionDeclaration
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &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)
+		write!(formatter, "{:?}", &self)
 	}
 }
 
@@ -58,14 +44,18 @@ pub(crate) enum TermPosition
 	Right,
 }
 
-pub(crate) struct TermDisplay<'term>
+pub struct TermDisplay<'term, F>
+where
+	F: crate::flavor::Flavor,
 {
-	term: &'term crate::Term,
-	parent_term: Option<&'term crate::Term>,
+	term: &'term crate::Term<F>,
+	parent_term: Option<&'term crate::Term<F>>,
 	position: TermPosition,
 }
 
-impl<'term> TermDisplay<'term>
+impl<'term, F> TermDisplay<'term, F>
+where
+	F: crate::flavor::Flavor,
 {
 	fn requires_parentheses(&self) -> bool
 	{
@@ -149,9 +139,11 @@ impl<'term> TermDisplay<'term>
 	}
 }
 
-pub(crate) fn display_term<'term>(term: &'term crate::Term,	parent_term: Option<&'term crate::Term>,
-	position: TermPosition)
-	-> TermDisplay<'term>
+pub(crate) fn display_term<'term, F>(term: &'term crate::Term<F>,
+	parent_term: Option<&'term crate::Term<F>>, position: TermPosition)
+	-> TermDisplay<'term, F>
+where
+	F: crate::flavor::Flavor,
 {
 	TermDisplay
 	{
@@ -161,49 +153,51 @@ pub(crate) fn display_term<'term>(term: &'term crate::Term,	parent_term: Option<
 	}
 }
 
-impl<'term> std::fmt::Debug for TermDisplay<'term>
+impl<'term, F> std::fmt::Debug for TermDisplay<'term, F>
+where
+	F: crate::flavor::Flavor,
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
 		let requires_parentheses = self.requires_parentheses();
 
 		if requires_parentheses
 		{
-			write!(format, "(")?;
+			write!(formatter, "(")?;
 		}
 
 		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, "\"{}\"",
+			crate::Term::Boolean(true) => write!(formatter, "true")?,
+			crate::Term::Boolean(false) => write!(formatter, "false")?,
+			crate::Term::SpecialInteger(value) => write!(formatter, "{:?}", value)?,
+			crate::Term::Integer(value) => write!(formatter, "{}", value)?,
+			crate::Term::String(value) => write!(formatter, "\"{}\"",
 				value.replace("\\", "\\\\").replace("\n", "\\n").replace("\t", "\\t"))?,
-			crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration)?,
+			crate::Term::Variable(variable) => variable.declaration.display_name(formatter)?,
 			crate::Term::Function(function) =>
 			{
-				write!(format, "{}", function.declaration.name)?;
+				function.declaration.display_name(formatter)?;
 
-				assert!(function.declaration.arity == function.arguments.len(),
+				assert!(function.declaration.arity() == function.arguments.len(),
 					"number of function arguments differs from declaration (expected {}, got {})",
-					function.declaration.arity, function.arguments.len());
+					function.declaration.arity(), function.arguments.len());
 
 				if !function.arguments.is_empty()
 				{
-					write!(format, "(")?;
+					write!(formatter, "(")?;
 
 					let mut separator = "";
 
 					for argument in &function.arguments
 					{
-						write!(format, "{}{:?}", separator,
+						write!(formatter, "{}{:?}", separator,
 							display_term(&argument, Some(self.term), TermPosition::Any))?;
 
 						separator = ", ";
 					}
 
-					write!(format, ")")?;
+					write!(formatter, ")")?;
 				}
 			},
 			crate::Term::BinaryOperation(binary_operation) =>
@@ -218,51 +212,57 @@ impl<'term> std::fmt::Debug for TermDisplay<'term>
 					crate::BinaryOperator::Exponentiate => "**",
 				};
 
-				write!(format, "{:?} {} {:?}",
+				write!(formatter, "{:?} {} {:?}",
 					display_term(&binary_operation.left, Some(self.term), TermPosition::Left),
 					operator_string,
 					display_term(&binary_operation.right, Some(self.term), TermPosition::Right))?;
 			},
 			crate::Term::UnaryOperation(
 				crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
-				=> write!(format, "-{:?}",
+				=> write!(formatter, "-{:?}",
 					display_term(argument, Some(self.term), TermPosition::Any))?,
 			crate::Term::UnaryOperation(
 				crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
-				=> write!(format, "|{:?}|",
+				=> write!(formatter, "|{:?}|",
 					display_term(argument, Some(self.term), TermPosition::Any))?,
 		}
 
 		if requires_parentheses
 		{
-			write!(format, ")")?;
+			write!(formatter, ")")?;
 		}
 
 		Ok(())
 	}
 }
 
-impl<'term> std::fmt::Display for TermDisplay<'term>
+impl<'term, F> std::fmt::Display for TermDisplay<'term, F>
+where
+	F: crate::flavor::Flavor,
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{:?}", self)
+		write!(formatter, "{:?}", self)
 	}
 }
 
-impl std::fmt::Debug for crate::Term
+impl<F> std::fmt::Debug for crate::Term<F>
+where
+	F: crate::flavor::Flavor,
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{:?}", display_term(&self, None, TermPosition::Any))
+		write!(formatter, "{:?}", display_term(&self, None, TermPosition::Any))
 	}
 }
 
-impl std::fmt::Display for crate::Term
+impl<F> std::fmt::Display for crate::Term<F>
+where
+	F: crate::flavor::Flavor,
 {
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{}", display_term(&self, None, TermPosition::Any))
+		write!(formatter, "{}", display_term(&self, None, TermPosition::Any))
 	}
 }
 
@@ -270,6 +270,7 @@ impl std::fmt::Display for crate::Term
 pub(crate) mod tests
 {
 	use crate::*;
+	type Term = crate::Term<flavor::DefaultFlavor>;
 
 	macro_rules! assert
 	{
@@ -279,7 +280,7 @@ pub(crate) mod tests
 		};
 	}
 
-	fn format(term: Box<ast::Term>) -> String
+	fn format(term: Box<Term>) -> String
 	{
 		format!("{}", term)
 	}

src/lib.rs

@@ -1,10 +1,11 @@
 mod ast;
-mod error;
-pub mod format;
-#[cfg(feature = "parse")]
-pub mod parse;
+pub mod flavor;
+mod format;
+mod parse;
 mod utils;
 
 pub use ast::*;
-pub use error::Error;
-pub use utils::VariableDeclarationStack;
+pub use format::{formulas::FormulaDisplay, terms::TermDisplay};
+pub use flavor::{DefaultFlavor, Flavor};
+pub use utils::*;
+pub use parse::{DefaultParser, Parser};

src/parse.rs

@@ -1,32 +1,142 @@
-mod formulas;
-mod helpers;
-mod literals;
-mod names;
-mod terms;
+pub mod error;
+pub mod formulas;
+pub mod terms;
+pub mod tokens;
 
-pub(crate) use helpers::word_boundary;
-pub(crate) use literals::{boolean, integer, special_integer, string};
-pub(crate) use names::{function_or_predicate_name, variable_name};
-pub use terms::term;
-pub use formulas::formula;
+pub use error::Error;
 
-pub struct Declarations
+use crate::flavor::{FunctionDeclaration as _, PredicateDeclaration as _, VariableDeclaration as _};
+
+pub trait Parser: Sized
 {
-	function_declarations: std::cell::RefCell<crate::FunctionDeclarations>,
-	predicate_declarations: std::cell::RefCell<crate::PredicateDeclarations>,
-	variable_declaration_stack: std::cell::RefCell<crate::VariableDeclarationStack>,
+	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)
+	}
 }
 
-impl Declarations
+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::new()),
-			predicate_declarations: std::cell::RefCell::new(crate::PredicateDeclarations::new()),
-			variable_declaration_stack:
-				std::cell::RefCell::new(crate::VariableDeclarationStack::new()),
+			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

@@ -0,0 +1,182 @@
+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/helpers.rs

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

src/parse/literals.rs

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

src/parse/names.rs

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

src/parse/tokens.rs

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