Make inner types customizable

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
 {
@@ -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 left: Box<Term<F>>,
-	pub right: Box<Term>,
+	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,17 +184,21 @@ 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 declaration: std::rc::Rc<F::FunctionDeclaration>,
-	pub arguments: Terms,
+	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(),
+		assert_eq!(declaration.arity(), arguments.len(),
 			"function has a different number of arguments then 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 left: Box<Term<F>>,
-	pub right: Box<Term>,
+	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 parameters: std::rc::Rc<VariableDeclarations<F>>,
-	pub argument: Box<Formula>,
+	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 antecedent: Box<Formula<F>>,
-	pub implication: Box<Formula>,
+	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,17 +338,21 @@ 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 declaration: std::rc::Rc<F::PredicateDeclaration>,
-	pub arguments: Terms,
+	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(),
+		assert_eq!(declaration.arity(), arguments.len(),
 			"predicate has a different number of arguments then 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),
+	UnaryOperation(UnaryOperation<F>),
-	Variable(Variable),
+	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),
+	Compare(Compare<F>),
-	Exists(QuantifiedFormula),
+	Exists(QuantifiedFormula<F>),
-	ForAll(QuantifiedFormula),
+	ForAll(QuantifiedFormula<F>),
-	IfAndOnlyIf(Formulas),
+	IfAndOnlyIf(Formulas<F>),
-	Implies(Implies),
+	Implies(Implies<F>),
-	Not(Box<Formula>),
+	Not(Box<Formula<F>>),
-	Or(Formulas),
+	Or(Formulas<F>),
-	Predicate(Predicate),
+	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>,
+	pub fn implies(direction: ImplicationDirection, antecedent: Box<Formula<F>>,
-		consequent: Box<Formula>) -> Self
+		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))
 	}
@@ -556,8 +602,10 @@ impl Formula
 	}
 }
 
-pub struct OpenFormula
+pub struct OpenFormula<F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub free_variable_declarations: std::rc::Rc<VariableDeclarations>,
+	pub free_variable_declarations: std::rc::Rc<VariableDeclarations<F>>,
-	pub formula: Formula,
+	pub formula: Formula<F>,
 }

src/flavor.rs

@@ -0,0 +1,100 @@
+pub trait FunctionDeclaration
+{
+	fn new(name: String, arity: usize) -> Self;
+
+	fn name(&self) -> &str;
+	fn arity(&self) -> usize;
+}
+
+impl FunctionDeclaration for crate::FunctionDeclaration
+{
+	fn new(name: String, arity: usize) -> Self
+	{
+		Self
+		{
+			name,
+			arity,
+		}
+	}
+
+	fn name(&self) -> &str
+	{
+		&self.name
+	}
+
+	fn arity(&self) -> usize
+	{
+		self.arity
+	}
+}
+
+pub trait PredicateDeclaration
+{
+	fn new(name: String, arity: usize) -> Self;
+
+	fn name(&self) -> &str;
+	fn arity(&self) -> usize;
+}
+
+impl PredicateDeclaration for crate::PredicateDeclaration
+{
+	fn new(name: String, arity: usize) -> Self
+	{
+		Self
+		{
+			name,
+			arity,
+		}
+	}
+
+	fn name(&self) -> &str
+	{
+		&self.name
+	}
+
+	fn arity(&self) -> usize
+	{
+		self.arity
+	}
+}
+
+pub trait VariableDeclaration
+{
+	fn new(name: String) -> Self;
+
+	fn name(&self) -> &str;
+}
+
+impl VariableDeclaration for crate::VariableDeclaration
+{
+	fn new(name: String) -> Self
+	{
+		Self
+		{
+			name
+		}
+	}
+
+	fn name(&self) -> &str
+	{
+		&self.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
+		+ std::fmt::Display;
+}
+
+pub struct DefaultFlavor;
+
+impl Flavor for DefaultFlavor
+{
+	type FunctionDeclaration = crate::FunctionDeclaration;
+	type PredicateDeclaration = crate::PredicateDeclaration;
+	type VariableDeclaration = crate::VariableDeclaration;
+}

src/format.rs

@@ -1,37 +1,2 @@
 pub mod formulas;
 pub mod terms;
-
-pub trait Format
-{
-	fn display_variable_declaration(&self, formatter: &mut std::fmt::Formatter,
-		variable_declaration: &std::rc::Rc<crate::VariableDeclaration>)
-		-> std::fmt::Result;
-}
-
-pub struct DefaultFormat;
-
-impl Format for DefaultFormat
-{
-	fn display_variable_declaration(&self, formatter: &mut std::fmt::Formatter,
-		variable_declaration: &std::rc::Rc<crate::VariableDeclaration>)
-		-> std::fmt::Result
-	{
-		write!(formatter, "{:?}", variable_declaration)
-	}
-}
-
-pub fn display_term<'term, 'format, F>(term: &'term crate::Term, format: &'format F)
-	-> terms::TermDisplay<'term, 'format, F>
-where
-	F: Format,
-{
-	terms::display_term(term, None, terms::TermPosition::Any, format)
-}
-
-pub fn display_formula<'formula, 'format, F>(formula: &'formula crate::Formula, format: &'format F)
-	-> formulas::FormulaDisplay<'formula, 'format, F>
-where
-	F: Format,
-{
-	formulas::display_formula(formula, None, formulas::FormulaPosition::Any, format)
-}

src/format/formulas.rs

@@ -1,3 +1,4 @@
+use crate::flavor::PredicateDeclaration as _;
 use super::terms::*;
 
 impl std::fmt::Debug for crate::ComparisonOperator
@@ -53,19 +54,19 @@ pub(crate) enum FormulaPosition
 	ImpliesAntecedent,
 }
 
-pub struct FormulaDisplay<'formula, 'format, F>
+pub struct FormulaDisplay<'formula, F>
 where
-	F: super::Format,
+	F: crate::flavor::Flavor,
 {
-	formula: &'formula crate::Formula,
+	formula: &'formula crate::Formula<F>,
-	parent_formula: Option<&'formula crate::Formula>,
+	parent_formula: Option<&'formula crate::Formula<F>>,
 	position: FormulaPosition,
-	format: &'format F,
+	//declarations: &'d D,
 }
 
-impl<'formula, 'format, F> FormulaDisplay<'formula, 'format, F>
+impl<'formula, F> FormulaDisplay<'formula, F>
 where
-	F: super::Format,
+	F: crate::flavor::Flavor,
 {
 	fn requires_parentheses(&self) -> bool
 	{
@@ -135,24 +136,23 @@ where
 	}
 }
 
-pub(crate) fn display_formula<'formula, 'format, F>(formula: &'formula crate::Formula,
+pub(crate) fn display_formula<'formula, F>(formula: &'formula crate::Formula<F>,
-	parent_formula: Option<&'formula crate::Formula>, position: FormulaPosition, format: &'format F)
+	parent_formula: Option<&'formula crate::Formula<F>>, position: FormulaPosition)
-	-> FormulaDisplay<'formula, 'format, F>
+	-> FormulaDisplay<'formula, F>
 where
-	F: super::Format,
+	F: crate::flavor::Flavor,
 {
 	FormulaDisplay
 	{
 		formula,
 		parent_formula,
 		position,
-		format,
 	}
 }
 
-impl<'formula, 'format, F> std::fmt::Debug for FormulaDisplay<'formula, 'format, F>
+impl<'formula, F> std::fmt::Debug for FormulaDisplay<'formula, F>
 where
-	F: super::Format,
+	F: crate::flavor::Flavor,
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
@@ -169,8 +169,8 @@ where
 			{
 				if exists.parameters.is_empty()
 				{
-					write!(formatter, "{:?}", display_formula(&exists.argument, self.parent_formula,
+					write!(formatter, "{:?}", display_formula::<F>(&exists.argument,
-						self.position, self.format))?;
+						self.parent_formula, self.position))?;
 				}
 				else
 				{
@@ -180,14 +180,13 @@ where
 
 					for parameter in exists.parameters.iter()
 					{
-						write!(formatter, "{}", separator)?;
+						write!(formatter, "{}{}", separator, parameter)?;
-						self.format.display_variable_declaration(formatter, &parameter)?;
 
 						separator = ", "
 					}
 
 					write!(formatter, " {:?}", display_formula(&exists.argument, Some(self.formula),
-						FormulaPosition::Any, self.format))?;
+						FormulaPosition::Any))?;
 				}
 			},
 			crate::Formula::ForAll(for_all) =>
@@ -195,7 +194,7 @@ where
 				if for_all.parameters.is_empty()
 				{
 					write!(formatter, "{:?}", display_formula(&for_all.argument,
-						self.parent_formula, self.position, self.format))?;
+						self.parent_formula, self.position))?;
 				}
 				else
 				{
@@ -205,18 +204,17 @@ where
 
 					for parameter in for_all.parameters.iter()
 					{
-						write!(formatter, "{}", separator)?;
+						write!(formatter, "{}{}", separator, parameter)?;
-						self.format.display_variable_declaration(formatter, &parameter)?;
 
 						separator = ", "
 					}
 
 					write!(formatter, " {:?}", display_formula(&for_all.argument,
-						Some(self.formula), FormulaPosition::Any, self.format))?;
+						Some(self.formula), FormulaPosition::Any))?;
 				}
 			},
 			crate::Formula::Not(argument) => write!(formatter, "not {:?}",
-				display_formula(argument, Some(self.formula), FormulaPosition::Any, self.format))?,
+				display_formula(argument, Some(self.formula), FormulaPosition::Any))?,
 			crate::Formula::And(arguments) =>
 			{
 				if arguments.is_empty()
@@ -236,7 +234,7 @@ where
 					for argument in arguments
 					{
 						write!(formatter, "{}{:?}", separator,
-							display_formula(argument, parent_formula, position, self.format))?;
+							display_formula(argument, parent_formula, position))?;
 
 						separator = " and "
 					}
@@ -261,7 +259,7 @@ where
 					for argument in arguments
 					{
 						write!(formatter, "{}{:?}", separator,
-							display_formula(argument, parent_formula, position, self.format))?;
+							display_formula(argument, parent_formula, position))?;
 
 						separator = " or "
 					}
@@ -273,14 +271,13 @@ where
 				{
 					write!(formatter, "{:?}",
 						display_formula(antecedent, Some(self.formula),
-							FormulaPosition::ImpliesAntecedent, self.format))
+							FormulaPosition::ImpliesAntecedent))
 				};
 
 				let format_implication = |formatter: &mut std::fmt::Formatter| -> Result<_, _>
 				{
 					write!(formatter, "{:?}",
-						display_formula(implication, Some(self.formula), FormulaPosition::Any,
+						display_formula(implication, Some(self.formula), FormulaPosition::Any))
-							self.format))
 				};
 
 				match direction
@@ -318,7 +315,7 @@ where
 					for argument in arguments
 					{
 						write!(formatter, "{}{:?}", separator,
-							display_formula(argument, parent_formula, position, self.format))?;
+							display_formula(argument, parent_formula, position))?;
 
 						separator = " <-> "
 					}
@@ -337,15 +334,14 @@ where
 				};
 
 				write!(formatter, "{:?} {} {:?}",
-					display_term(&compare.left, None, TermPosition::Any, self.format),
+					display_term(&compare.left, None, TermPosition::Any), operator_string,
-					operator_string,
+					display_term(&compare.right, None, TermPosition::Any))?;
-					display_term(&compare.right, None, TermPosition::Any, self.format))?;
 			},
 			crate::Formula::Boolean(true) => write!(formatter, "true")?,
 			crate::Formula::Boolean(false) => write!(formatter, "false")?,
 			crate::Formula::Predicate(predicate) =>
 			{
-				write!(formatter, "{}", predicate.declaration.name)?;
+				write!(formatter, "{}", predicate.declaration.name())?;
 
 				if !predicate.arguments.is_empty()
 				{
@@ -356,7 +352,7 @@ where
 					for argument in &predicate.arguments
 					{
 						write!(formatter, "{}{:?}", separator, display_term(argument, None,
-							TermPosition::Any, self.format))?;
+							TermPosition::Any))?;
 
 						separator = ", "
 					}
@@ -375,9 +371,9 @@ where
 	}
 }
 
-impl<'formula, 'format, F> std::fmt::Display for FormulaDisplay<'formula, 'format, F>
+impl<'formula, F> std::fmt::Display for FormulaDisplay<'formula, F>
 where
-	F: super::Format,
+	F: crate::flavor::Flavor,
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
@@ -385,21 +381,23 @@ where
 	}
 }
 
-impl std::fmt::Debug for crate::Formula
+impl<F> std::fmt::Debug for crate::Formula<F>
+where
+	F: crate::flavor::Flavor,
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(formatter, "{:?}", display_formula(&self, None, FormulaPosition::Any,
+		write!(formatter, "{:?}", display_formula(&self, None, FormulaPosition::Any))
-			&super::DefaultFormat))
 	}
 }
 
-impl std::fmt::Display for crate::Formula
+impl<F> std::fmt::Display for crate::Formula<F>
+where
+	F: crate::flavor::Flavor,
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(formatter, "{}", display_formula(&self, None, FormulaPosition::Any,
+		write!(formatter, "{}", display_formula(&self, None, FormulaPosition::Any))
-			&super::DefaultFormat))
 	}
 }
 
@@ -407,7 +405,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
 	{
@@ -442,7 +443,7 @@ mod tests
 		};
 	}
 
-	fn format(formula: Box<ast::Formula>) -> String
+	fn format(formula: Box<Formula>) -> String
 	{
 		format!("{}", formula)
 	}

src/format/terms.rs

@@ -1,3 +1,5 @@
+use crate::flavor::FunctionDeclaration as _;
+
 impl std::fmt::Debug for crate::SpecialInteger
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
@@ -58,19 +60,18 @@ pub(crate) enum TermPosition
 	Right,
 }
 
-pub struct TermDisplay<'term, 'format, F>
+pub struct TermDisplay<'term, F>
 where
-	F: super::Format,
+	F: crate::flavor::Flavor,
 {
-	term: &'term crate::Term,
+	term: &'term crate::Term<F>,
-	parent_term: Option<&'term crate::Term>,
+	parent_term: Option<&'term crate::Term<F>>,
 	position: TermPosition,
-	format: &'format F,
 }
 
-impl<'term, 'format, F> TermDisplay<'term, 'format, F>
+impl<'term, F> TermDisplay<'term, F>
 where
-	F: super::Format,
+	F: crate::flavor::Flavor,
 {
 	fn requires_parentheses(&self) -> bool
 	{
@@ -154,24 +155,23 @@ where
 	}
 }
 
-pub(crate) fn display_term<'term, 'format, F>(term: &'term crate::Term,
+pub(crate) fn display_term<'term, F>(term: &'term crate::Term<F>,
-	parent_term: Option<&'term crate::Term>, position: TermPosition, format: &'format F)
+	parent_term: Option<&'term crate::Term<F>>, position: TermPosition)
-	-> TermDisplay<'term, 'format, F>
+	-> TermDisplay<'term, F>
 where
-	F: super::Format,
+	F: crate::flavor::Flavor,
 {
 	TermDisplay
 	{
 		term,
 		parent_term,
 		position,
-		format,
 	}
 }
 
-impl<'term, 'format, F> std::fmt::Debug for TermDisplay<'term, 'format, F>
+impl<'term, F> std::fmt::Debug for TermDisplay<'term, F>
 where
-	F: super::Format,
+	F: crate::flavor::Flavor,
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
@@ -190,15 +190,14 @@ where
 			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) =>
+			crate::Term::Variable(variable) => write!(formatter, "{}", variable.declaration)?,
-				self.format.display_variable_declaration(formatter, &variable.declaration)?,
 			crate::Term::Function(function) =>
 			{
-				write!(formatter, "{}", function.declaration.name)?;
+				write!(formatter, "{}", function.declaration.name())?;
 
-				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()
 				{
@@ -209,8 +208,7 @@ where
 					for argument in &function.arguments
 					{
 						write!(formatter, "{}{:?}", separator,
-							display_term(&argument, Some(self.term), TermPosition::Any,
+							display_term(&argument, Some(self.term), TermPosition::Any))?;
-								self.format))?;
 
 						separator = ", ";
 					}
@@ -231,20 +229,18 @@ where
 				};
 
 				write!(formatter, "{:?} {} {:?}",
-					display_term(&binary_operation.left, Some(self.term), TermPosition::Left,
+					display_term(&binary_operation.left, Some(self.term), TermPosition::Left),
-						self.format),
 					operator_string,
-					display_term(&binary_operation.right, Some(self.term), TermPosition::Right,
+					display_term(&binary_operation.right, Some(self.term), TermPosition::Right))?;
-						self.format))?;
 			},
 			crate::Term::UnaryOperation(
 				crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
 				=> write!(formatter, "-{:?}",
-					display_term(argument, Some(self.term), TermPosition::Any, self.format))?,
+					display_term(argument, Some(self.term), TermPosition::Any))?,
 			crate::Term::UnaryOperation(
 				crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
 				=> write!(formatter, "|{:?}|",
-					display_term(argument, Some(self.term), TermPosition::Any, self.format))?,
+					display_term(argument, Some(self.term), TermPosition::Any))?,
 		}
 
 		if requires_parentheses
@@ -256,9 +252,9 @@ where
 	}
 }
 
-impl<'term, 'format, F> std::fmt::Display for TermDisplay<'term, 'format, F>
+impl<'term, F> std::fmt::Display for TermDisplay<'term, F>
 where
-	F: super::Format,
+	F: crate::flavor::Flavor,
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
@@ -266,20 +262,23 @@ where
 	}
 }
 
-impl std::fmt::Debug for crate::Term
+impl<F> std::fmt::Debug for crate::Term<F>
+where
+	F: crate::flavor::Flavor,
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(formatter, "{:?}", display_term(&self, None, TermPosition::Any,
+		write!(formatter, "{:?}", display_term(&self, None, TermPosition::Any))
-			&super::DefaultFormat))
 	}
 }
 
-impl std::fmt::Display for crate::Term
+impl<F> std::fmt::Display for crate::Term<F>
+where
+	F: crate::flavor::Flavor,
 {
 	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(formatter, "{}", display_term(&self, None, TermPosition::Any, &super::DefaultFormat))
+		write!(formatter, "{}", display_term(&self, None, TermPosition::Any))
 	}
 }
 
@@ -287,6 +286,7 @@ impl std::fmt::Display for crate::Term
 pub(crate) mod tests
 {
 	use crate::*;
+	type Term = crate::Term<flavor::DefaultFlavor>;
 
 	macro_rules! assert
 	{
@@ -296,7 +296,7 @@ pub(crate) mod tests
 		};
 	}
 
-	fn format(term: Box<ast::Term>) -> String
+	fn format(term: Box<Term>) -> String
 	{
 		format!("{}", term)
 	}

src/lib.rs

@@ -1,4 +1,5 @@
 mod ast;
+pub mod flavor;
 pub mod format;
 pub mod parse;
 mod utils;

src/parse/formulas.rs

@@ -1,9 +1,11 @@
 use super::terms::*;
 use super::tokens::*;
 
-pub fn formula<D>(input: &str, declarations: &D) -> Result<crate::OpenFormula, crate::parse::Error>
+pub fn formula<D, F>(input: &str, declarations: &D)
+	-> Result<crate::OpenFormula<F>, crate::parse::Error>
 where
-	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration,
+	F: crate::flavor::Flavor,
+	D: crate::FindOrCreateFunctionDeclaration<F> + crate::FindOrCreatePredicateDeclaration<F>,
 {
 	let variable_declaration_stack = crate::VariableDeclarationStackLayer::free();
 
@@ -69,19 +71,22 @@ impl std::fmt::Debug for LogicalConnective
 	}
 }
 
-struct FormulaStr<'i, 'd, 'p, 'v, D>
+struct FormulaStr<'i, 'd, 'p, 'v, F, D>
+where
+	F: crate::flavor::Flavor,
 {
 	input: &'i str,
 	declarations: &'d D,
-	variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p>,
+	variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, F>,
 }
 
-impl<'i, 'd, 'p, 'v, D> FormulaStr<'i, 'd, 'p, 'v, D>
+impl<'i, 'd, 'p, 'v, F, D> FormulaStr<'i, 'd, 'p, 'v, F, D>
 where
-	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration,
+	F: crate::flavor::Flavor,
+	D: crate::FindOrCreateFunctionDeclaration<F> + crate::FindOrCreatePredicateDeclaration<F>,
 {
 	pub fn new(input: &'i str, declarations: &'d D,
-		variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p>)
+		variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, F>)
 		-> Self
 	{
 		Self
@@ -189,7 +194,7 @@ where
 		Tokens::new_filter_map(self.input, functor)
 	}
 
-	pub fn parse(&self, level: usize) -> Result<crate::Formula, crate::parse::Error>
+	pub fn parse(&self, level: usize) -> Result<crate::Formula<F>, crate::parse::Error>
 	{
 		let indentation = "  ".repeat(level);
 		let input = trim_start(self.input);
@@ -395,7 +400,7 @@ where
 
 	// TODO: refactor
 	fn implication_left_to_right_inner<T>(&self, mut argument_iterator: T, level: usize)
-		-> Result<Option<crate::Formula>, crate::parse::Error>
+		-> Result<Option<crate::Formula<F>>, crate::parse::Error>
 	where
 		T: std::iter::Iterator<Item = Result<&'i str, crate::parse::Error>>
 	{
@@ -418,7 +423,7 @@ where
 	}
 
 	fn implication_left_to_right<T>(&self, mut argument_iterator: T, level: usize)
-		-> Result<crate::Formula, crate::parse::Error>
+		-> Result<crate::Formula<F>, crate::parse::Error>
 	where
 		T: std::iter::Iterator<Item = Result<&'i str, crate::parse::Error>>
 	{
@@ -446,9 +451,9 @@ where
 
 	// TODO: refactor without input argument
 	fn quantified_formula(&self, input: &str, quantifier: Quantifier, level: usize)
-		-> Result<crate::Formula, crate::parse::Error>
+		-> Result<crate::Formula<F>, crate::parse::Error>
 	{
-		let (parameters, input) = match variable_declarations(input)?
+		let (parameters, input) = match variable_declarations::<F>(input)?
 		{
 			Some(variable_declarations) => variable_declarations,
 			None => return Err(crate::parse::Error::new_expected_variable_declaration(
@@ -500,7 +505,7 @@ mod tests
 	#[test]
 	fn tokenize_formula_logical_connectives()
 	{
-		let declarations = crate::Declarations::new();
+		let declarations = crate::Declarations::<crate::flavor::DefaultFlavor>::new();
 		let variable_declaration_stack = crate::VariableDeclarationStackLayer::free();
 
 		let formula_str = |input| FormulaStr::new(input, &declarations,

src/parse/terms.rs

@@ -1,3 +1,4 @@
+use crate::flavor::VariableDeclaration as _;
 use super::tokens::*;
 
 pub(crate) fn function_name(input: &str) -> Option<(&str, &str)>
@@ -82,19 +83,23 @@ fn is_variable_name(identifier: &str) -> bool
 	false
 }
 
-pub(crate) fn variable_declaration(input: &str) -> Option<(crate::VariableDeclaration, &str)>
+pub(crate) fn variable_declaration<F>(input: &str) -> Option<(F::VariableDeclaration, &str)>
+where
+	F: crate::flavor::Flavor,
 {
 	variable_name(input)
 		.map(|(variable_name, remaining_input)|
-			(crate::VariableDeclaration::new(variable_name.to_string()), remaining_input))
+			(F::VariableDeclaration::new(variable_name.to_string()), remaining_input))
 }
 
-pub(crate) fn variable_declarations(input: &str)
+pub(crate) fn variable_declarations<F>(input: &str)
-	-> Result<Option<(crate::VariableDeclarations, &str)>, crate::parse::Error>
+	-> Result<Option<(crate::VariableDeclarations<F>, &str)>, crate::parse::Error>
+where
+	F: crate::flavor::Flavor,
 {
 	let mut variable_declarations = vec![];
 
-	let (first_variable_declaration, mut input) = match variable_declaration(input)
+	let (first_variable_declaration, mut input) = match variable_declaration::<F>(input)
 	{
 		Some(first_variable_declaration) => first_variable_declaration,
 		None => return Ok(None),
@@ -115,7 +120,7 @@ pub(crate) fn variable_declarations(input: &str)
 
 		input = trim_start(input);
 
-		let (variable_declaration, remaining_input) = match variable_declaration(input)
+		let (variable_declaration, remaining_input) = match variable_declaration::<F>(input)
 		{
 			Some(variable_declaration) => variable_declaration,
 			None => return Err(crate::parse::Error::new_expected_variable_declaration(
@@ -162,19 +167,22 @@ impl std::fmt::Debug for ArithmeticOperatorClass
 	}
 }
 
-pub(crate) struct TermStr<'i, 'd, 'v, 'p, D>
+pub(crate) struct TermStr<'i, 'd, 'v, 'p, F, D>
+where
+	F: crate::flavor::Flavor,
 {
 	input: &'i str,
 	declarations: &'d D,
-	variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p>,
+	variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, F>,
 }
 
-impl<'i, 'd, 'v, 'p, D> TermStr<'i, 'd, 'v, 'p, D>
+impl<'i, 'd, 'v, 'p, F, D> TermStr<'i, 'd, 'v, 'p, F, D>
 where
-	D: crate::FindOrCreateFunctionDeclaration + crate::FindOrCreatePredicateDeclaration,
+	F: crate::flavor::Flavor,
+	D: crate::FindOrCreateFunctionDeclaration<F> + crate::FindOrCreatePredicateDeclaration<F>,
 {
 	pub fn new(input: &'i str, declarations: &'d D,
-		variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p>)
+		variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, F>)
 		-> Self
 	{
 		Self
@@ -299,7 +307,7 @@ where
 		Ok(top_level_arithmetic_operator_class)
 	}
 
-	pub fn parse(&self, level: usize) -> Result<crate::Term, crate::parse::Error>
+	pub fn parse(&self, level: usize) -> Result<crate::Term<F>, crate::parse::Error>
 	{
 		let indentation = "  ".repeat(level);
 		log::trace!("{}- parsing term: {}", indentation, self.input);
@@ -497,7 +505,7 @@ where
 
 	// TODO: refactor
 	fn exponentiate_inner<T>(&self, mut argument_iterator: T, level: usize)
-		-> Result<Option<crate::Term>, crate::parse::Error>
+		-> Result<Option<crate::Term<F>>, crate::parse::Error>
 	where
 		T: std::iter::Iterator<Item = Result<&'i str, crate::parse::Error>>
 	{
@@ -521,7 +529,7 @@ where
 	}
 
 	fn exponentiate<T>(&self, mut argument_iterator: T, level: usize)
-		-> Result<crate::Term, crate::parse::Error>
+		-> Result<crate::Term<F>, crate::parse::Error>
 	where
 		T: std::iter::Iterator<Item = Result<&'i str, crate::parse::Error>>
 	{
@@ -572,6 +580,9 @@ mod tests
 	#[test]
 	fn parse_variable_declaration()
 	{
+		let variable_declaration =
+			|x| super::variable_declaration::<crate::flavor::DefaultFlavor>(x);
+
 		let v = variable_declaration("X").unwrap();
 		assert_eq!((v.0.name.as_str(), v.1), ("X", ""));
 		let v = variable_declaration("_X").unwrap();
@@ -601,6 +612,9 @@ mod tests
 	#[test]
 	fn parse_variable_declarations()
 	{
+		let variable_declarations =
+			|x| super::variable_declarations::<crate::flavor::DefaultFlavor>(x);
+
 		let v = variable_declarations("X.").unwrap().unwrap();
 		assert_eq!(v.0.len(), 1);
 		assert_eq!(v.0[0].name.as_str(), "X");

src/utils.rs

@@ -1,25 +1,36 @@
-pub trait FindOrCreateFunctionDeclaration
+use crate::flavor::{FunctionDeclaration as _, PredicateDeclaration as _, VariableDeclaration as _};
+
+// Group with implementations
+pub trait FindOrCreateFunctionDeclaration<F>
+where
+	F: crate::flavor::Flavor,
 {
 	fn find_or_create_function_declaration(&self, name: &str, arity: usize)
-		-> std::rc::Rc<crate::FunctionDeclaration>;
+		-> std::rc::Rc<F::FunctionDeclaration>;
 }
 
-pub trait FindOrCreatePredicateDeclaration
+pub trait FindOrCreatePredicateDeclaration<F>
+where
+	F: crate::flavor::Flavor,
 {
 	fn find_or_create_predicate_declaration(&self, name: &str, arity: usize)
-		-> std::rc::Rc<crate::PredicateDeclaration>;
+		-> std::rc::Rc<F::PredicateDeclaration>;
 }
 
-pub struct BoundVariableDeclarations<'p>
+pub struct BoundVariableDeclarations<'p, F>
+where
+	F: crate::flavor::Flavor,
 {
-	parent: &'p VariableDeclarationStackLayer<'p>,
+	parent: &'p VariableDeclarationStackLayer<'p, F>,
-	variable_declarations: std::rc::Rc<crate::VariableDeclarations>,
+	variable_declarations: std::rc::Rc<crate::VariableDeclarations<F>>,
 }
 
-impl<'p> BoundVariableDeclarations<'p>
+impl<'p, F> BoundVariableDeclarations<'p, F>
+where
+	F: crate::flavor::Flavor,
 {
-	pub fn new(parent: &'p VariableDeclarationStackLayer<'p>,
+	pub fn new(parent: &'p VariableDeclarationStackLayer<'p, F>,
-		variable_declarations: std::rc::Rc<crate::VariableDeclarations>) -> Self
+		variable_declarations: std::rc::Rc<crate::VariableDeclarations<F>>) -> Self
 	{
 		Self
 		{
@@ -29,33 +40,37 @@ impl<'p> BoundVariableDeclarations<'p>
 	}
 }
 
-pub enum VariableDeclarationStackLayer<'p>
+pub enum VariableDeclarationStackLayer<'p, F>
+where
+	F: crate::flavor::Flavor,
 {
-	Free(std::cell::RefCell<crate::VariableDeclarations>),
+	Free(std::cell::RefCell<crate::VariableDeclarations<F>>),
-	Bound(BoundVariableDeclarations<'p>),
+	Bound(BoundVariableDeclarations<'p, F>),
 }
 
-impl<'p> VariableDeclarationStackLayer<'p>
+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>,
+	pub fn bound(parent: &'p VariableDeclarationStackLayer<'p, F>,
-		variable_declarations: std::rc::Rc<crate::VariableDeclarations>) -> Self
+		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<crate::VariableDeclaration>>
+	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.name == variable_name)
+					.find(|x| x.name() == variable_name)
 				{
 					return Some(std::rc::Rc::clone(&variable_declaration));
 				}
@@ -66,7 +81,7 @@ impl<'p> VariableDeclarationStackLayer<'p>
 			{
 				if let Some(variable_declaration) = bound_variable_declarations
 					.variable_declarations.iter()
-					.find(|x| x.name == variable_name)
+					.find(|x| x.name() == variable_name)
 				{
 					return Some(std::rc::Rc::clone(&variable_declaration));
 				}
@@ -76,22 +91,19 @@ impl<'p> VariableDeclarationStackLayer<'p>
 		}
 	}
 
-	pub fn find_or_create(&self, variable_name: &str) -> std::rc::Rc<crate::VariableDeclaration>
+	pub fn find_or_create(&self, variable_name: &str) -> 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.name == variable_name)
+					.find(|x| x.name() == variable_name)
 				{
 					return std::rc::Rc::clone(&variable_declaration);
 				}
 
-				let variable_declaration = crate::VariableDeclaration
+				let variable_declaration = F::VariableDeclaration::new(variable_name.to_owned());
-				{
-					name: variable_name.to_owned(),
-				};
 				let variable_declaration = std::rc::Rc::new(variable_declaration);
 
 				free_variable_declarations.borrow_mut()
@@ -103,7 +115,7 @@ impl<'p> VariableDeclarationStackLayer<'p>
 			{
 				if let Some(variable_declaration) = bound_variable_declarations
 					.variable_declarations.iter()
-					.find(|x| x.name == variable_name)
+					.find(|x| x.name() == variable_name)
 				{
 					return std::rc::Rc::clone(&variable_declaration);
 				}
@@ -113,9 +125,9 @@ impl<'p> VariableDeclarationStackLayer<'p>
 		}
 	}
 
-	pub fn free_variable_declarations_do_mut<F, G>(&self, f: F) -> G
+	pub fn free_variable_declarations_do_mut<F1, F2>(&self, f: F1) -> F2
 	where
-		F: Fn(&mut crate::VariableDeclarations) -> G
+		F1: Fn(&mut crate::VariableDeclarations<F>) -> F2,
 	{
 		match self
 		{
@@ -126,9 +138,9 @@ impl<'p> VariableDeclarationStackLayer<'p>
 		}
 	}
 
-	pub fn free_variable_declarations_do<F, G>(&self, f: F) -> G
+	pub fn free_variable_declarations_do<F1, F2>(&self, f: F1) -> F2
 	where
-		F: Fn(&crate::VariableDeclarations) -> G
+		F1: Fn(&crate::VariableDeclarations<F>) -> F2,
 	{
 		match self
 		{
@@ -140,41 +152,44 @@ impl<'p> VariableDeclarationStackLayer<'p>
 	}
 }
 
-pub struct Declarations
+pub struct Declarations<F>
+where
+	F: crate::flavor::Flavor,
 {
-	function_declarations: std::cell::RefCell<crate::FunctionDeclarations>,
+	function_declarations: std::cell::RefCell<crate::FunctionDeclarations<F>>,
-	predicate_declarations: std::cell::RefCell<crate::PredicateDeclarations>,
+	predicate_declarations: std::cell::RefCell<crate::PredicateDeclarations<F>>,
 }
 
-impl Declarations
+impl<F> Declarations<F>
+where
+	F: crate::flavor::Flavor,
 {
 	pub fn new() -> Self
 	{
 		Self
 		{
-			function_declarations: std::cell::RefCell::new(crate::FunctionDeclarations::new()),
+			function_declarations: std::cell::RefCell::new(crate::FunctionDeclarations::<F>::new()),
-			predicate_declarations: std::cell::RefCell::new(crate::PredicateDeclarations::new()),
+			predicate_declarations:
+				std::cell::RefCell::new(crate::PredicateDeclarations::<F>::new()),
 		}
 	}
 }
 
-impl FindOrCreateFunctionDeclaration for Declarations
+impl<F> FindOrCreateFunctionDeclaration<F> for Declarations<F>
+where
+	F: crate::flavor::Flavor,
 {
 	fn find_or_create_function_declaration(&self, name: &str, arity: usize)
-		-> std::rc::Rc<crate::FunctionDeclaration>
+		-> std::rc::Rc<F::FunctionDeclaration>
 	{
 		let mut function_declarations = self.function_declarations.borrow_mut();
 
-		match function_declarations.iter().find(|x| x.name == name && x.arity == arity)
+		match function_declarations.iter().find(|x| x.name() == name && x.arity() == arity)
 		{
 			Some(declaration) => std::rc::Rc::clone(&declaration),
 			None =>
 			{
-				let declaration = crate::FunctionDeclaration
+				let declaration = F::FunctionDeclaration::new(name.to_string(), arity);
-				{
-					name: name.to_string(),
-					arity,
-				};
 				let declaration = std::rc::Rc::new(declaration);
 
 				function_declarations.insert(std::rc::Rc::clone(&declaration));
@@ -185,23 +200,21 @@ impl FindOrCreateFunctionDeclaration for Declarations
 	}
 }
 
-impl FindOrCreatePredicateDeclaration for Declarations
+impl<F> FindOrCreatePredicateDeclaration<F> for Declarations<F>
+where
+	F: crate::flavor::Flavor,
 {
 	fn find_or_create_predicate_declaration(&self, name: &str, arity: usize)
-		-> std::rc::Rc<crate::PredicateDeclaration>
+		-> std::rc::Rc<F::PredicateDeclaration>
 	{
 		let mut predicate_declarations = self.predicate_declarations.borrow_mut();
 
-		match predicate_declarations.iter().find(|x| x.name == name && x.arity == arity)
+		match predicate_declarations.iter().find(|x| x.name() == name && x.arity() == arity)
 		{
 			Some(declaration) => std::rc::Rc::clone(&declaration),
 			None =>
 			{
-				let declaration = crate::PredicateDeclaration
+				let declaration = F::PredicateDeclaration::new(name.to_string(), arity);
-				{
-					name: name.to_string(),
-					arity,
-				};
 				let declaration = std::rc::Rc::new(declaration);
 
 				predicate_declarations.insert(std::rc::Rc::clone(&declaration));