Support hashing domains

.github/workflows/main.yml

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

.gitignore

@@ -1,3 +1,3 @@
-/Cargo.lock
 /target
 **/*.rs.bk
+Cargo.lock

Cargo.toml

@@ -2,19 +2,7 @@
 name = "foliage"
 version = "0.1.0"
 authors = ["Patrick Lühne <patrick@luehne.de>"]
-description = "Abstract syntax tree for first-order logic with integer arithmetics"
-documentation = "https://github.com/potassco/foliage"
-homepage = "https://github.com/potassco/foliage"
-repository = "https://github.com/potassco/foliage"
-readme = "README.md"
-keywords = ["logic"]
-categories = ["data-structures", "science"]
-license = "MIT"
 edition = "2018"
 
 [dependencies]
-nom = {version = "5.1", optional = true}
+nom = "5.0"
-
-[features]
-default = ["parse"]
-parse = ["nom"]

LICENSE.md

@@ -1,21 +0,0 @@
-# The MIT License (MIT)
-
-Copyright © 2020 Patrick Lühne
-
-Permission is hereby granted, free of charge, to any person obtaining a copy
-of this software and associated documentation files (the "Software"), to deal
-in the Software without restriction, including without limitation the rights
-to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all
-copies or substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-SOFTWARE.

README.md

@@ -1,26 +0,0 @@
-# foliage [![crates.io](https://img.shields.io/crates/v/foliage.svg?maxAge=3600)](https://crates.io/crates/foliage)
-
-> First-order logic with integer arithmetics in Rust
-
-This Rust crate provides an abstract syntax tree for first-order formulas with integer arithmetics.
-
-## Supported Formulas
-
-- Booleans values (`true` and `false`)
-- predicates
-- negated formulas
-- comparisons of terms (<, ≤, >, ≥, =, ≠)
-- implications and biconditionals
-- conjunctions and disjunctions of formulas
-- existentially and universally quantified formulas
-
-## Supported Terms
-
-- Boolean values (`true` and `false`)
-- integers
-- strings
-- special integers (infimum and supremum)
-- symbolic functions
-- variables
-- binary operations (addition, subtraction, multiplication, division, modulo, exponentiation)
-- unary operations (absolute value, numeric negation)

benches/test.rs

@@ -0,0 +1,20 @@
+#![feature(test)]
+
+extern crate test;
+
+#[cfg(test)]
+mod tests
+{
+	#[bench]
+	fn anthem_example_2(b: &mut test::Bencher)
+	{
+		let formulas = "forall XV1 (p(XV1) <-> (exists XU1 (exists X1, X2 (X1 = XU1 and exists N1, N2, N3 (N1 = 0 and N2 = n and N1 <= N3 and N3 <= N2 and X2 = N3) and X1 = X2) and exists X3, X4 (exists N4, N5 (X3 = (N4 * N5) and N4 = XU1 and N5 = XU1) and X4 = n and X3 <= X4) and XV1 = XU1)))
+forall XV2 (q(XV2) <-> (exists XU2 (exists X5 (X5 = XU2 and p(X5)) and exists X6 (exists N6, N7 (X6 = (N6 + N7) and N6 = XU2 and N7 = 1) and not p(X6)) and XV2 = XU2)))";
+
+		b.iter(||
+		{
+			let (i, _) = foliage::formulas(formulas).unwrap();
+			assert_eq!(i, "");
+		});
+	}
+}

examples/test.rs

@@ -0,0 +1,26 @@
+fn main() -> Result<(), Box<dyn std::error::Error>>
+{
+	let formulas = "forall XV1 (p(XV1) <-> (exists XU1 (exists X1, X2 (X1 = XU1 and exists N1, N2, N3 (N1 = 0 and N2 = n and N1 <= N3 and N3 <= N2 and X2 = N3) and X1 = X2) and exists X3, X4 (exists N4, N5 (X3 = (N4 * N5) and N4 = XU1 and N5 = XU1) and X4 = n and X3 <= X4) and XV1 = XU1)))
+forall XV2 (q(XV2) <-> (exists XU2 (exists X5 (X5 = XU2 and p(X5)) and exists X6 (exists N6, N7 (X6 = (N6 + N7) and N6 = XU2 and N7 = 1) and not p(X6)) and XV2 = XU2)))";
+
+	let (i, formulas) = foliage::formulas(formulas).unwrap();
+	assert_eq!(i, "");
+
+	for formula in formulas
+	{
+		println!("{}", formula);
+	}
+
+	let formulas = "forall XV1 (p(XV1) <-> exists XU1 (exists X1, X2 (X1 = XU1 and exists N1, N2, N3 (N1 = 0 and N2 = n and N1 <= N3 and N3 <= N2 and X2 = N3) and X1 = X2) and exists X3, X4 (exists N4, N5 (X3 = N4 * N5 and N4 = XU1 and N5 = XU1) and X4 = n and X3 <= X4) and XV1 = XU1))
+forall XV2 (q(XV2) <-> exists XU2 (exists X5 (X5 = XU2 and p(X5)) and exists X6 (exists N6, N7 (X6 = N6 + N7 and N6 = XU2 and N7 = 1) and not p(X6)) and XV2 = XU2))";
+
+	let (i, formulas) = foliage::formulas(formulas).unwrap();
+	assert_eq!(i, "");
+
+	for formula in formulas
+	{
+		println!("{}", formula);
+	}
+
+	Ok(())
+}

src/ast.rs

@@ -1,557 +1,83 @@
-// Operators
+#[derive(Eq, Hash, PartialEq)]
-
-#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub enum BinaryOperator
-{
-	Add,
-	Subtract,
-	Multiply,
-	Divide,
-	Modulo,
-	Exponentiate,
-}
-
-#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub enum ComparisonOperator
-{
-	Greater,
-	Less,
-	LessOrEqual,
-	GreaterOrEqual,
-	NotEqual,
-	Equal,
-}
-
-#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub enum UnaryOperator
-{
-	AbsoluteValue,
-	Negative,
-}
-
-// ImplicationDirection
-
-#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub enum ImplicationDirection
-{
-	LeftToRight,
-	RightToLeft,
-}
-
-// Primitives
-
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct FunctionDeclaration
-{
-	pub name: String,
-	pub arity: usize,
-}
-
-impl FunctionDeclaration
-{
-	pub fn new(name: String, arity: usize) -> Self
-	{
-		Self
-		{
-			name,
-			arity,
-		}
-	}
-}
-
-pub type FunctionDeclarations = std::collections::BTreeSet<std::rc::Rc<FunctionDeclaration>>;
-
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub struct PredicateDeclaration
 {
 	pub name: String,
 	pub arity: usize,
 }
 
-impl PredicateDeclaration
+#[derive(PartialEq)]
+pub struct Predicate
 {
-	pub fn new(name: String, arity: usize) -> Self
+	pub declaration: PredicateDeclaration,
-	{
+	pub arguments: Vec<Term>,
-		Self
-		{
-			name,
-			arity,
-		}
-	}
 }
 
-pub type PredicateDeclarations = std::collections::BTreeSet<std::rc::Rc<PredicateDeclaration>>;
+#[derive(PartialEq)]
-
+pub struct Exists
-pub struct VariableDeclaration
 {
-	pub name: String,
+	pub parameters: Vec<VariableDeclaration>,
-}
-
-impl std::cmp::PartialEq for VariableDeclaration
-{
-	#[inline(always)]
-	fn eq(&self, other: &VariableDeclaration) -> bool
-	{
-		let l = self as *const VariableDeclaration;
-		let r = other as *const VariableDeclaration;
-
-		l.eq(&r)
-	}
-}
-
-impl std::cmp::Eq for VariableDeclaration
-{
-}
-
-impl std::cmp::PartialOrd for VariableDeclaration
-{
-	#[inline(always)]
-	fn partial_cmp(&self, other: &VariableDeclaration) -> Option<std::cmp::Ordering>
-	{
-		let l = self as *const VariableDeclaration;
-		let r = other as *const VariableDeclaration;
-
-		l.partial_cmp(&r)
-	}
-}
-
-impl std::cmp::Ord for VariableDeclaration
-{
-	#[inline(always)]
-	fn cmp(&self, other: &VariableDeclaration) -> std::cmp::Ordering
-	{
-		let l = self as *const VariableDeclaration;
-		let r = other as *const VariableDeclaration;
-
-		l.cmp(&r)
-	}
-}
-
-impl std::hash::Hash for VariableDeclaration
-{
-	#[inline(always)]
-	fn hash<H: std::hash::Hasher>(&self, state: &mut H)
-	{
-		let p = self as *const VariableDeclaration;
-
-		p.hash(state);
-	}
-}
-
-impl VariableDeclaration
-{
-	pub fn new(name: String) -> Self
-	{
-		Self
-		{
-			name,
-		}
-	}
-}
-
-pub type VariableDeclarations = Vec<std::rc::Rc<VariableDeclaration>>;
-
-// Terms
-
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct BinaryOperation
-{
-	pub operator: BinaryOperator,
-	pub left: Box<Term>,
-	pub right: Box<Term>,
-}
-
-impl BinaryOperation
-{
-	pub fn new(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self
-		{
-			operator,
-			left,
-			right,
-		}
-	}
-}
-
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct Function
-{
-	pub declaration: std::rc::Rc<FunctionDeclaration>,
-	pub arguments: Terms,
-}
-
-impl Function
-{
-	pub fn new(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Terms) -> Self
-	{
-		assert_eq!(declaration.arity, arguments.len(),
-			"function has a different number of arguments then declared");
-
-		Self
-		{
-			declaration,
-			arguments,
-		}
-	}
-}
-
-#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub enum SpecialInteger
-{
-	Infimum,
-	Supremum,
-}
-
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct UnaryOperation
-{
-	pub operator: UnaryOperator,
-	pub argument: Box<Term>,
-}
-
-impl UnaryOperation
-{
-	pub fn new(operator: UnaryOperator, argument: Box<Term>) -> Self
-	{
-		Self
-		{
-			operator,
-			argument,
-		}
-	}
-}
-
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct Variable
-{
-	pub declaration: std::rc::Rc<VariableDeclaration>,
-}
-
-impl Variable
-{
-	pub fn new(declaration: std::rc::Rc<VariableDeclaration>) -> Self
-	{
-		Self
-		{
-			declaration,
-		}
-	}
-}
-
-// Formulas
-
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct Compare
-{
-	pub operator: ComparisonOperator,
-	pub left: Box<Term>,
-	pub right: Box<Term>,
-}
-
-impl Compare
-{
-	pub fn new(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self
-		{
-			operator,
-			left,
-			right,
-		}
-	}
-}
-
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct QuantifiedFormula
-{
-	pub parameters: std::rc::Rc<VariableDeclarations>,
 	pub argument: Box<Formula>,
 }
 
-impl QuantifiedFormula
+#[derive(PartialEq)]
+pub struct ForAll
 {
-	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
+	pub parameters: Vec<VariableDeclaration>,
-	{
+	pub argument: Box<Formula>,
-		Self
-		{
-			parameters,
-			argument,
-		}
-	}
 }
 
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
+#[derive(PartialEq)]
-pub struct Implies
+pub enum ImplicationDirection
 {
-	pub direction: ImplicationDirection,
+	LeftToRight,
-	pub antecedent: Box<Formula>,
+	RightToLeft,
-	pub implication: Box<Formula>,
 }
 
-impl Implies
+#[derive(PartialEq)]
-{
-	pub fn new(direction: ImplicationDirection, antecedent: Box<Formula>, implication: Box<Formula>)
-		-> Self
-	{
-		Self
-		{
-			direction,
-			antecedent,
-			implication,
-		}
-	}
-}
-
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub struct Predicate
-{
-	pub declaration: std::rc::Rc<PredicateDeclaration>,
-	pub arguments: Terms,
-}
-
-impl Predicate
-{
-	pub fn new(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Terms) -> Self
-	{
-		assert_eq!(declaration.arity, arguments.len(),
-			"predicate has a different number of arguments then declared");
-
-		Self
-		{
-			declaration,
-			arguments,
-		}
-	}
-}
-
-// Variants
-
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
-pub enum Term
-{
-	BinaryOperation(BinaryOperation),
-	Boolean(bool),
-	Function(Function),
-	Integer(i32),
-	SpecialInteger(SpecialInteger),
-	String(String),
-	UnaryOperation(UnaryOperation),
-	Variable(Variable),
-}
-
-pub type Terms = Vec<Term>;
-
-impl Term
-{
-	pub fn absolute_value(argument: Box<Term>) -> Self
-	{
-		Self::unary_operation(UnaryOperator::AbsoluteValue, argument)
-	}
-
-	pub fn add(left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self::binary_operation(BinaryOperator::Add, left, right)
-	}
-
-	pub fn binary_operation(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self::BinaryOperation(BinaryOperation::new(operator, left, right))
-	}
-
-	pub fn boolean(value: bool) -> Self
-	{
-		Self::Boolean(value)
-	}
-
-	pub fn divide(left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self::binary_operation(BinaryOperator::Divide, left, right)
-	}
-
-	pub fn exponentiate(left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self::binary_operation(BinaryOperator::Exponentiate, left, right)
-	}
-
-	pub fn false_() -> Self
-	{
-		Self::boolean(false)
-	}
-
-	pub fn function(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Terms) -> Self
-	{
-		Self::Function(Function::new(declaration, arguments))
-	}
-
-	pub fn infimum() -> Self
-	{
-		Self::special_integer(SpecialInteger::Infimum)
-	}
-
-	pub fn integer(value: i32) -> Self
-	{
-		Self::Integer(value)
-	}
-
-	pub fn modulo(left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self::binary_operation(BinaryOperator::Modulo, left, right)
-	}
-
-	pub fn multiply(left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self::binary_operation(BinaryOperator::Multiply, left, right)
-	}
-
-	pub fn negative(argument: Box<Term>) -> Self
-	{
-		Self::unary_operation(UnaryOperator::Negative, argument)
-	}
-
-	pub fn special_integer(value: SpecialInteger) -> Self
-	{
-		Self::SpecialInteger(value)
-	}
-
-	pub fn string(value: String) -> Self
-	{
-		Self::String(value)
-	}
-
-	pub fn subtract(left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self::binary_operation(BinaryOperator::Subtract, left, right)
-	}
-
-	pub fn supremum() -> Self
-	{
-		Self::special_integer(SpecialInteger::Supremum)
-	}
-
-	pub fn true_() -> Self
-	{
-		Self::boolean(true)
-	}
-
-	pub fn unary_operation(operator: UnaryOperator, argument: Box<Term>) -> Self
-	{
-		Self::UnaryOperation(UnaryOperation::new(operator, argument))
-	}
-
-	pub fn variable(declaration: std::rc::Rc<VariableDeclaration>) -> Self
-	{
-		Self::Variable(Variable::new(declaration))
-	}
-}
-
-#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
 pub enum Formula
 {
-	And(Formulas),
+	Exists(Exists),
-	Boolean(bool),
+	ForAll(ForAll),
-	Compare(Compare),
-	Exists(QuantifiedFormula),
-	ForAll(QuantifiedFormula),
-	IfAndOnlyIf(Formulas),
-	Implies(Implies),
 	Not(Box<Formula>),
-	Or(Formulas),
+	And(Vec<Box<Formula>>),
+	Or(Vec<Box<Formula>>),
+	Implies(Box<Formula>, Box<Formula>, ImplicationDirection),
+	Biconditional(Box<Formula>, Box<Formula>),
+	Less(Term, Term),
+	LessOrEqual(Term, Term),
+	Greater(Term, Term),
+	GreaterOrEqual(Term, Term),
+	Equal(Term, Term),
+	NotEqual(Term, Term),
+	Boolean(bool),
 	Predicate(Predicate),
 }
 
-pub type Formulas = Vec<Formula>;
+#[derive(Eq, Hash, PartialEq)]
-
+pub enum Domain
-impl Formula
 {
-	pub fn and(arguments: Formulas) -> Self
+	Program,
-	{
+	Integer,
-		Self::And(arguments)
+}
-	}
+
-
+#[derive(PartialEq)]
-	pub fn boolean(value: bool) -> Self
+pub struct VariableDeclaration
-	{
+{
-		Self::Boolean(value)
+	pub name: String,
-	}
+	pub domain: Domain,
-
+}
-	pub fn compare(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
+
-	{
+#[derive(PartialEq)]
-		Self::Compare(Compare::new(operator, left, right))
+pub enum Term
-	}
+{
-
+	Infimum,
-	pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
+	Supremum,
-	{
+	Integer(i64),
-		Self::Exists(QuantifiedFormula::new(parameters, argument))
+	Symbolic(String),
-	}
+	String(String),
-
+	Variable(VariableDeclaration),
-	pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
+	Add(Box<Term>, Box<Term>),
-	{
+	Subtract(Box<Term>, Box<Term>),
-		Self::compare(ComparisonOperator::Equal, left, right)
+	Multiply(Box<Term>, Box<Term>),
-	}
+	Negative(Box<Term>),
-
-	pub fn false_() -> Self
-	{
-		Self::boolean(false)
-	}
-
-	pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
-	{
-		Self::ForAll(QuantifiedFormula::new(parameters, argument))
-	}
-
-	pub fn greater(left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self::compare(ComparisonOperator::Greater, left, right)
-	}
-
-	pub fn greater_or_equal(left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self::compare(ComparisonOperator::GreaterOrEqual, left, right)
-	}
-
-	pub fn if_and_only_if(arguments: Formulas) -> Self
-	{
-		Self::IfAndOnlyIf(arguments)
-	}
-
-	pub fn implies(direction: ImplicationDirection, antecedent: Box<Formula>,
-		consequent: Box<Formula>) -> Self
-	{
-		Self::Implies(Implies::new(direction, antecedent, consequent))
-	}
-
-	pub fn less(left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self::compare(ComparisonOperator::Less, left, right)
-	}
-
-	pub fn less_or_equal(left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self::compare(ComparisonOperator::LessOrEqual, left, right)
-	}
-
-	pub fn not(argument: Box<Formula>) -> Self
-	{
-		Self::Not(argument)
-	}
-
-	pub fn not_equal(left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self::compare(ComparisonOperator::NotEqual, left, right)
-	}
-
-	pub fn or(arguments: Formulas) -> Self
-	{
-		Self::Or(arguments)
-	}
-
-	pub fn predicate(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Terms) -> Self
-	{
-		Self::Predicate(Predicate::new(declaration, arguments))
-	}
-
-	pub fn true_() -> Self
-	{
-		Self::boolean(true)
-	}
 }

src/error.rs

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

src/format.rs

@@ -1,2 +1,319 @@
-mod formulas;
+struct TermDisplay<'parent>
-mod terms;
+{
+	parent: Option<&'parent crate::Term>,
+	term: &'parent crate::Term,
+}
+
+struct FormulaDisplay<'parent>
+{
+	parent: Option<&'parent crate::Formula>,
+	formula: &'parent crate::Formula,
+}
+
+fn display_term<'parent>(term: &'parent crate::Term, parent: Option<&'parent crate::Term>) -> TermDisplay<'parent>
+{
+	TermDisplay
+	{
+		parent,
+		term,
+	}
+}
+
+fn display_formula<'parent>(formula: &'parent crate::Formula, parent: Option<&'parent crate::Formula>)
+	-> FormulaDisplay<'parent>
+{
+	FormulaDisplay
+	{
+		parent,
+		formula,
+	}
+}
+
+fn term_precedence(term: &crate::Term) -> u64
+{
+	match term
+	{
+		crate::Term::Infimum | crate::Term::Supremum | crate::Term::Integer(_) | crate::Term::Symbolic(_) | crate::Term::String(_) | crate::Term::Variable(_) => 0,
+		crate::Term::Negative(_) => 1,
+		crate::Term::Multiply(_, _) => 2,
+		crate::Term::Add(_, _) | crate::Term::Subtract(_, _) => 3,
+	}
+}
+
+fn term_requires_parentheses(child: &crate::Term, parent: Option<&crate::Term>) -> bool
+{
+	match parent
+	{
+		None => false,
+		Some(parent) =>
+		{
+			let child_precedence = term_precedence(child);
+			let parent_precedence = term_precedence(parent);
+
+			if child_precedence != parent_precedence
+			{
+				return child_precedence > parent_precedence;
+			}
+
+			// Subtraction isn’t associative, so handle them separately
+			// TODO: only do this for right-hand side of subtractions
+			match parent
+			{
+				crate::Term::Subtract(_, _) => true,
+				_ => false,
+			}
+		},
+	}
+}
+
+fn formula_precedence(formula: &crate::Formula) -> u64
+{
+	match formula
+	{
+		crate::Formula::Predicate(_) | crate::Formula::Boolean(_) | crate::Formula::Less(_, _) | crate::Formula::LessOrEqual(_, _) | crate::Formula::Greater(_, _) | crate::Formula::GreaterOrEqual(_, _) | crate::Formula::Equal(_, _) | crate::Formula::NotEqual(_, _) => 0,
+		crate::Formula::Exists(_) | crate::Formula::ForAll(_) => 1,
+		crate::Formula::Not(_) => 2,
+		crate::Formula::And(_) => 3,
+		crate::Formula::Or(_) => 4,
+		crate::Formula::Implies(_, _, _) => 5,
+		crate::Formula::Biconditional(_, _) => 6,
+	}
+}
+
+fn formula_requires_parentheses(child: &crate::Formula, parent: Option<&crate::Formula>) -> bool
+{
+	match parent
+	{
+		None => false,
+		Some(parent) =>
+		{
+			let child_precedence = formula_precedence(child);
+			let parent_precedence = formula_precedence(parent);
+
+			if child_precedence != parent_precedence
+			{
+				return child_precedence > parent_precedence;
+			}
+
+			// Implications aren’t associative, so handle them separately
+			match parent
+			{
+				crate::Formula::Implies(_, _, _) => true,
+				_ => false,
+			}
+		},
+	}
+}
+
+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)
+	}
+}
+
+impl<'term> std::fmt::Debug for TermDisplay<'term>
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		let requires_parentheses = term_requires_parentheses(self.term, self.parent);
+
+		if requires_parentheses
+		{
+			write!(format, "(")?;
+		}
+
+		match self.term
+		{
+			crate::Term::Infimum => write!(format, "#inf"),
+			crate::Term::Supremum => write!(format, "#sup"),
+			crate::Term::Integer(value) => write!(format, "{}", value),
+			crate::Term::Symbolic(ref value) => write!(format, "{}", value),
+			crate::Term::String(ref value) => write!(format, "\"{}\"", value),
+			crate::Term::Variable(ref declaration) => write!(format, "{:?}", declaration),
+			crate::Term::Add(ref left, ref right) => write!(format, "{:?} + {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))),
+			crate::Term::Subtract(ref left, ref right) => write!(format, "{:?} - {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))),
+			crate::Term::Multiply(ref left, ref right) => write!(format, "{:?} * {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))),
+			crate::Term::Negative(ref argument) => write!(format, "-{:?}", display_term(argument, Some(self.term))),
+		}?;
+
+		if requires_parentheses
+		{
+			write!(format, ")")?;
+		}
+
+		Ok(())
+	}
+}
+
+impl<'term> std::fmt::Display for TermDisplay<'term>
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", self)
+	}
+}
+
+impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		let requires_parentheses = formula_requires_parentheses(self.formula, self.parent);
+
+		if requires_parentheses
+		{
+			write!(format, "(")?;
+		}
+
+		match self.formula
+		{
+			crate::Formula::Exists(ref exists) =>
+			{
+				write!(format, "exists")?;
+
+				let mut separator = " ";
+
+				for parameter in &exists.parameters
+				{
+					write!(format, "{}{:?}", separator, parameter)?;
+
+					separator = ", "
+				}
+
+				write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula)))?;
+			},
+			crate::Formula::ForAll(ref for_all) =>
+			{
+				write!(format, "forall")?;
+
+				let mut separator = " ";
+
+				for parameter in &for_all.parameters
+				{
+					write!(format, "{}{:?}", separator, parameter)?;
+
+					separator = ", "
+				}
+
+				write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula)))?;
+			},
+			crate::Formula::Not(ref argument) => write!(format, "not {:?}", display_formula(argument, Some(self.formula)))?,
+			crate::Formula::And(ref arguments) =>
+			{
+				let mut separator = "";
+
+				for argument in arguments
+				{
+					write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?;
+
+					separator = " and "
+				}
+			},
+			crate::Formula::Or(ref arguments) =>
+			{
+				let mut separator = "";
+
+				for argument in arguments
+				{
+					write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?;
+
+					separator = " or "
+				}
+			},
+			crate::Formula::Implies(ref left, ref right, implication_direction) => match implication_direction
+			{
+				crate::ImplicationDirection::LeftToRight => write!(format, "{:?} -> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
+				crate::ImplicationDirection::RightToLeft => write!(format, "{:?} <- {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
+			},
+			crate::Formula::Biconditional(ref left, ref right) => write!(format, "{:?} <-> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
+			crate::Formula::Less(ref left, ref right) => write!(format, "{:?} < {:?}", display_term(left, None), display_term(right, None))?,
+			crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "{:?} <= {:?}", display_term(left, None), display_term(right, None))?,
+			crate::Formula::Greater(ref left, ref right) => write!(format, "{:?} > {:?}", display_term(left, None), display_term(right, None))?,
+			crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "{:?} >= {:?}", display_term(left, None), display_term(right, None))?,
+			crate::Formula::Equal(ref left, ref right) => write!(format, "{:?} = {:?}", display_term(left, None), display_term(right, None))?,
+			crate::Formula::NotEqual(ref left, ref right) => write!(format, "{:?} != {:?}", display_term(left, None), display_term(right, None))?,
+			crate::Formula::Boolean(value) =>
+				match value
+				{
+					true => write!(format, "#true")?,
+					false => write!(format, "#false")?,
+				},
+			crate::Formula::Predicate(ref predicate) =>
+			{
+				write!(format, "{}", predicate.declaration.name)?;
+
+				if !predicate.arguments.is_empty()
+				{
+					write!(format, "(")?;
+
+					let mut separator = "";
+
+					for argument in &predicate.arguments
+					{
+						write!(format, "{}{:?}", separator, display_term(argument, None))?;
+
+						separator = ", "
+					}
+
+					write!(format, ")")?;
+				}
+			},
+		}
+
+		if requires_parentheses
+		{
+			write!(format, ")")?;
+		}
+
+		Ok(())
+	}
+}
+
+impl<'formula> std::fmt::Display for FormulaDisplay<'formula>
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", self)
+	}
+}
+
+impl std::fmt::Debug for crate::Formula
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", display_formula(&self, None))
+	}
+}
+
+impl std::fmt::Display for crate::Formula
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{}", display_formula(&self, None))
+	}
+}
+
+impl std::fmt::Debug for crate::Term
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{:?}", display_term(&self, None))
+	}
+}
+
+impl std::fmt::Display for crate::Term
+{
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
+	{
+		write!(format, "{}", display_term(&self, None))
+	}
+}

src/lib.rs

@@ -1,10 +1,6 @@
 mod ast;
-mod error;
 pub mod format;
-#[cfg(feature = "parse")]
 pub mod parse;
-mod utils;
 
-pub use ast::*;
+pub use ast::{Domain, Exists, Formula, ForAll, ImplicationDirection, Predicate, PredicateDeclaration, VariableDeclaration, Term};
-pub use error::Error;
+pub use parse::{formula, formulas, term};
-pub use utils::VariableDeclarationStack;

src/parse/formulas.rs

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

src/parse/helpers.rs

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

src/parse/literals.rs

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

src/parse/names.rs

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

src/parse/terms.rs

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

src/utils.rs

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