.gitignore

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

Cargo.toml

@@ -2,12 +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 = "5.0"

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,565 +1,83 @@
-// Operators
-
-pub enum BinaryOperator
-{
-	Add,
-	Subtract,
-	Multiply,
-	Divide,
-	Modulo,
-	Exponentiate,
-}
-
-pub enum ComparisonOperator
-{
-	Greater,
-	Less,
-	LessOrEqual,
-	GreaterOrEqual,
-	NotEqual,
-	Equal,
-}
-
-pub enum UnaryOperator
-{
-	AbsoluteValue,
-	Negative,
-}
-
-// 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)]
+#[derive(Eq, Hash, PartialEq)]
 pub struct PredicateDeclaration
 {
 	pub name: String,
 	pub arity: usize,
 }
 
-impl PredicateDeclaration
-{
-	pub fn new(name: String, arity: usize) -> Self
-	{
-		Self
-		{
-			name,
-			arity,
-		}
-	}
-}
-
-pub type PredicateDeclarations = std::collections::BTreeSet<std::rc::Rc<PredicateDeclaration>>;
-
-pub struct VariableDeclaration
-{
-	pub name: String,
-}
-
-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 VariableDeclaration
-{
-	pub fn new(name: String) -> Self
-	{
-		Self
-		{
-			name,
-		}
-	}
-}
-
-pub type VariableDeclarations = Vec<std::rc::Rc<VariableDeclaration>>;
-
-// Terms
-
-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,
-		}
-	}
-}
-
-pub struct Function
-{
-	pub declaration: std::rc::Rc<FunctionDeclaration>,
-	pub arguments: Vec<Box<Term>>,
-}
-
-impl Function
-{
-	pub fn new(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
-	{
-		assert_eq!(declaration.arity, arguments.len(),
-			"function has a different number of arguments then declared");
-
-		Self
-		{
-			declaration: std::rc::Rc::clone(declaration),
-			arguments,
-		}
-	}
-}
-
-pub enum SpecialInteger
-{
-	Infimum,
-	Supremum,
-}
-
-pub struct UnaryOperation
-{
-	pub operator: UnaryOperator,
-	pub argument: Box<Term>,
-}
-
-impl UnaryOperation
-{
-	pub fn new(operator: UnaryOperator, argument: Box<Term>) -> Self
-	{
-		Self
-		{
-			operator,
-			argument,
-		}
-	}
-}
-
-pub struct Variable
-{
-	pub declaration: std::rc::Rc<VariableDeclaration>,
-}
-
-impl Variable
-{
-	pub fn new(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
-	{
-		Self
-		{
-			declaration: std::rc::Rc::clone(declaration),
-		}
-	}
-}
-
-// Formulas
-
-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,
-		}
-	}
-}
-
-pub struct Exists
-{
-	pub parameters: std::rc::Rc<VariableDeclarations>,
-	pub argument: Box<Formula>,
-}
-
-impl Exists
-{
-	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
-	{
-		Self
-		{
-			parameters,
-			argument,
-		}
-	}
-}
-
-pub struct ForAll
-{
-	pub parameters: std::rc::Rc<VariableDeclarations>,
-	pub argument: Box<Formula>,
-}
-
-impl ForAll
-{
-	pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
-	{
-		Self
-		{
-			parameters,
-			argument,
-		}
-	}
-}
-
-pub struct IfAndOnlyIf
-{
-	pub left: Box<Formula>,
-	pub right: Box<Formula>,
-}
-
-impl IfAndOnlyIf
-{
-	pub fn new(left: Box<Formula>, right: Box<Formula>) -> Self
-	{
-		Self
-		{
-			left,
-			right,
-		}
-	}
-}
-
-pub struct Implies
-{
-	pub antecedent: Box<Formula>,
-	pub implication: Box<Formula>,
-}
-
-impl Implies
-{
-	pub fn new(antecedent: Box<Formula>, implication: Box<Formula>) -> Self
-	{
-		Self
-		{
-			antecedent,
-			implication,
-		}
-	}
-}
-
+#[derive(PartialEq)]
 pub struct Predicate
 {
-	pub declaration: std::rc::Rc<PredicateDeclaration>,
-	pub arguments: Vec<Box<Term>>,
+	pub declaration: PredicateDeclaration,
+	pub arguments: Vec<Term>,
 }
 
-impl Predicate
+#[derive(PartialEq)]
+pub struct Exists
 {
-	pub fn new(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
-	{
-		assert_eq!(declaration.arity, arguments.len(),
-			"predicate has a different number of arguments then declared");
-
-		Self
-		{
-			declaration: std::rc::Rc::clone(declaration),
-			arguments,
-		}
-	}
+	pub parameters: Vec<VariableDeclaration>,
+	pub argument: Box<Formula>,
 }
 
-// Variants
-
-pub enum Term
+#[derive(PartialEq)]
+pub struct ForAll
 {
-	BinaryOperation(BinaryOperation),
-	Boolean(bool),
-	Function(Function),
-	Integer(i32),
-	SpecialInteger(SpecialInteger),
-	String(String),
-	UnaryOperation(UnaryOperation),
-	Variable(Variable),
+	pub parameters: Vec<VariableDeclaration>,
+	pub argument: Box<Formula>,
 }
 
-pub type Terms = Vec<Box<Term>>;
-
-impl Term
+#[derive(PartialEq)]
+pub enum ImplicationDirection
 {
-	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: Vec<Box<Term>>)
-		-> 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))
-	}
+	LeftToRight,
+	RightToLeft,
 }
 
+#[derive(PartialEq)]
 pub enum Formula
 {
-	And(Formulas),
-	Boolean(bool),
-	Compare(Compare),
 	Exists(Exists),
 	ForAll(ForAll),
-	IfAndOnlyIf(IfAndOnlyIf),
-	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<Box<Formula>>;
-
-impl Formula
+#[derive(Eq, Hash, PartialEq)]
+pub enum Domain
 {
-	pub fn and(arguments: Formulas) -> Self
-	{
-		assert!(!arguments.is_empty());
-
-		Self::And(arguments)
-	}
-
-	pub fn boolean(value: bool) -> Self
-	{
-		Self::Boolean(value)
-	}
-
-	pub fn compare(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self::Compare(Compare::new(operator, left, right))
-	}
-
-	pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
-	{
-		assert!(!parameters.is_empty());
-
-		Self::Exists(Exists::new(parameters, argument))
-	}
-
-	pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
-	{
-		Self::compare(ComparisonOperator::Equal, left, right)
-	}
-
-	pub fn false_() -> Self
-	{
-		Self::boolean(false)
-	}
-
-	pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
-	{
-		assert!(!parameters.is_empty());
-
-		Self::ForAll(ForAll::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(left: Box<Formula>, right: Box<Formula>) -> Self
-	{
-		Self::IfAndOnlyIf(IfAndOnlyIf::new(left, right))
-	}
-
-	pub fn implies(antecedent: Box<Formula>, consequent: Box<Formula>) -> Self
-	{
-		Self::Implies(Implies::new(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
-	{
-		assert!(!arguments.is_empty());
-
-		Self::Or(arguments)
-	}
-
-	pub fn predicate(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>)
-		-> Self
-	{
-		Self::Predicate(Predicate::new(declaration, arguments))
-	}
-
-	pub fn true_() -> Self
-	{
-		Self::boolean(true)
-	}
+	Program,
+	Integer,
+}
+
+#[derive(PartialEq)]
+pub struct VariableDeclaration
+{
+	pub name: String,
+	pub domain: Domain,
+}
+
+#[derive(PartialEq)]
+pub enum Term
+{
+	Infimum,
+	Supremum,
+	Integer(i64),
+	Symbolic(String),
+	String(String),
+	Variable(VariableDeclaration),
+	Add(Box<Term>, Box<Term>),
+	Subtract(Box<Term>, Box<Term>),
+	Multiply(Box<Term>, Box<Term>),
+	Negative(Box<Term>),
 }

src/format.rs

@@ -1,121 +1,107 @@
-trait Precedence
+struct TermDisplay<'parent>
 {
-	fn precedence(&self) -> i32;
+	parent: Option<&'parent crate::Term>,
+	term: &'parent crate::Term,
 }
 
-impl Precedence for crate::Term
+struct FormulaDisplay<'parent>
 {
-	fn precedence(&self) -> i32
+	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
 	{
-		match &self
+		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) =>
 		{
-			Self::Boolean(_)
-			| Self::Function(_)
-			| Self::SpecialInteger(_)
-			| Self::Integer(_)
-			| Self::String(_)
-			| Self::Variable(_)
-				=> 0,
-			Self::UnaryOperation(
-				crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..})
-				=> 1,
-			Self::BinaryOperation(
-				crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, ..})
-				=> 2,
-			Self::BinaryOperation(
-				crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, ..})
-			| Self::BinaryOperation(
-				crate::BinaryOperation{operator: crate::BinaryOperator::Divide, ..})
-			| Self::BinaryOperation(
-				crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
-				=> 3,
-			Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Add, ..})
-			| Self::BinaryOperation(
-				crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, ..})
-				=> 4,
-			Self::UnaryOperation(
-				crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
-				=> 5,
-		}
+			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,
+			}
+		},
 	}
 }
 
-impl Precedence for crate::Formula
+fn formula_precedence(formula: &crate::Formula) -> u64
 {
-	fn precedence(&self) -> i32
+	match formula
 	{
-		match &self
+		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) =>
 		{
-			Self::Predicate(_)
-			| Self::Boolean(_)
-			| Self::Compare(_)
-				=> 0,
-			Self::Exists(_)
-			| Self::ForAll(_)
-				=> 1,
-			Self::Not(_)
-				=> 2,
-			Self::And(_)
-				=> 3,
-			Self::Or(_)
-				=> 4,
-			Self::Implies(_)
-				=> 5,
-			Self::IfAndOnlyIf(_)
-				=> 6,
-		}
-	}
-}
+			let child_precedence = formula_precedence(child);
+			let parent_precedence = formula_precedence(parent);
 
-impl std::fmt::Debug for crate::SpecialInteger
-{
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		match &self
-		{
-			crate::SpecialInteger::Infimum => write!(format, "#inf"),
-			crate::SpecialInteger::Supremum => write!(format, "#sup"),
-		}
-	}
-}
+			if child_precedence != parent_precedence
+			{
+				return child_precedence > parent_precedence;
+			}
 
-impl std::fmt::Display for crate::SpecialInteger
-{
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(format, "{:?}", &self)
-	}
-}
-
-impl std::fmt::Debug for crate::FunctionDeclaration
-{
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(format, "{}/{}", &self.name, self.arity)
-	}
-}
-
-impl std::fmt::Display for crate::FunctionDeclaration
-{
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(format, "{:?}", &self)
-	}
-}
-
-impl std::fmt::Debug for crate::PredicateDeclaration
-{
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(format, "{}/{}", &self.name, self.arity)
-	}
-}
-
-impl std::fmt::Display for crate::PredicateDeclaration
-{
-	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(format, "{:?}", &self)
+			// Implications aren’t associative, so handle them separately
+			match parent
+			{
+				crate::Formula::Implies(_, _, _) => true,
+				_ => false,
+			}
+		},
 	}
 }
 
@@ -135,102 +121,29 @@ impl std::fmt::Display for crate::VariableDeclaration
 	}
 }
 
-struct TermDisplay<'term>
-{
-	parent_precedence: Option<i32>,
-	term: &'term crate::Term,
-}
-
-fn display_term(term: &crate::Term, parent_precedence: Option<i32>) -> TermDisplay
-{
-	TermDisplay
-	{
-		parent_precedence,
-		term,
-	}
-}
-
 impl<'term> std::fmt::Debug for TermDisplay<'term>
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		let precedence = self.term.precedence();
-		let requires_parentheses = match self.parent_precedence
-		{
-			Some(parent_precedence) => precedence > parent_precedence,
-			None => false,
-		};
-		let precedence = Some(precedence);
+		let requires_parentheses = term_requires_parentheses(self.term, self.parent);
 
 		if requires_parentheses
 		{
 			write!(format, "(")?;
 		}
 
-		match &self.term
+		match self.term
 		{
-			crate::Term::Boolean(true) => write!(format, "true"),
-			crate::Term::Boolean(false) => write!(format, "false"),
-			crate::Term::SpecialInteger(value) => write!(format, "{:?}", value),
+			crate::Term::Infimum => write!(format, "#inf"),
+			crate::Term::Supremum => write!(format, "#sup"),
 			crate::Term::Integer(value) => write!(format, "{}", value),
-			crate::Term::String(value) => write!(format, "\"{}\"", value),
-			crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration),
-			crate::Term::Function(function) =>
-			{
-				write!(format, "{}", function.declaration.name)?;
-
-				assert!(function.declaration.arity == function.arguments.len(),
-					"number of function arguments differs from declaration (expected {}, got {})",
-					function.declaration.arity, function.arguments.len());
-
-				if !function.arguments.is_empty()
-				{
-					write!(format, "(")?;
-
-					let mut separator = "";
-
-					for argument in &function.arguments
-					{
-						write!(format, "{}{:?}", separator, display_term(&argument, None))?;
-
-						separator = ", ";
-					}
-
-					write!(format, ")")?;
-				}
-
-				Ok(())
-			},
-			crate::Term::BinaryOperation(
-				crate::BinaryOperation{operator: crate::BinaryOperator::Add, left, right})
-				=> write!(format, "{:?} + {:?}", display_term(left, precedence),
-					display_term(right, precedence)),
-			crate::Term::BinaryOperation(
-				crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, left, right})
-				=> write!(format, "{:?} - {:?}", display_term(left, precedence),
-					display_term(right, precedence)),
-			crate::Term::BinaryOperation(
-				crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, left, right})
-				=> write!(format, "{:?} * {:?}", display_term(left, precedence),
-					display_term(right, precedence)),
-			crate::Term::BinaryOperation(
-				crate::BinaryOperation{operator: crate::BinaryOperator::Divide, left, right})
-				=> write!(format, "{:?} / {:?}", display_term(left, precedence),
-					display_term(right, precedence)),
-			crate::Term::BinaryOperation(
-				crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, left, right})
-				=> write!(format, "{:?} % {:?}", display_term(left, precedence),
-					display_term(right, precedence)),
-			crate::Term::BinaryOperation(
-				crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, left, right})
-				=> write!(format, "{:?} ** {:?}", display_term(left, precedence),
-					display_term(right, precedence)),
-			crate::Term::UnaryOperation(
-				crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
-				=> write!(format, "-{:?}", display_term(argument, precedence)),
-			crate::Term::UnaryOperation(
-				crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
-				=> write!(format, "|{:?}|", display_term(argument, precedence)),
+			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
@@ -250,135 +163,91 @@ impl<'term> std::fmt::Display for TermDisplay<'term>
 	}
 }
 
-struct FormulaDisplay<'formula>
-{
-	parent_precedence: Option<i32>,
-	formula: &'formula crate::Formula,
-}
-
-fn display_formula(formula: &crate::Formula, parent_precedence: Option<i32>) -> FormulaDisplay
-{
-	FormulaDisplay
-	{
-		parent_precedence,
-		formula,
-	}
-}
-
 impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		let precedence = self.formula.precedence();
-		let requires_parentheses = match self.parent_precedence
-		{
-			Some(parent_precedence) => precedence > parent_precedence,
-			None => false,
-		};
-		let precedence = Some(precedence);
+		let requires_parentheses = formula_requires_parentheses(self.formula, self.parent);
 
 		if requires_parentheses
 		{
 			write!(format, "(")?;
 		}
 
-		match &self.formula
+		match self.formula
 		{
-			crate::Formula::Exists(exists) =>
+			crate::Formula::Exists(ref exists) =>
 			{
-				assert!(!exists.parameters.is_empty());
-
 				write!(format, "exists")?;
 
 				let mut separator = " ";
 
-				for parameter in exists.parameters.iter()
+				for parameter in &exists.parameters
 				{
 					write!(format, "{}{:?}", separator, parameter)?;
 
 					separator = ", "
 				}
 
-				write!(format, " {:?}", display_formula(&exists.argument, precedence))?;
+				write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula)))?;
 			},
-			crate::Formula::ForAll(for_all) =>
+			crate::Formula::ForAll(ref for_all) =>
 			{
-				assert!(!for_all.parameters.is_empty());
-
 				write!(format, "forall")?;
 
 				let mut separator = " ";
 
-				for parameter in for_all.parameters.iter()
+				for parameter in &for_all.parameters
 				{
 					write!(format, "{}{:?}", separator, parameter)?;
 
 					separator = ", "
 				}
 
-				write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
+				write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula)))?;
 			},
-			crate::Formula::Not(argument) => write!(format, "not {:?}",
-				display_formula(argument, precedence))?,
-			crate::Formula::And(arguments) =>
+			crate::Formula::Not(ref argument) => write!(format, "not {:?}", display_formula(argument, Some(self.formula)))?,
+			crate::Formula::And(ref arguments) =>
 			{
 				let mut separator = "";
 
-				assert!(!arguments.is_empty());
-
 				for argument in arguments
 				{
-					write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
+					write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?;
 
 					separator = " and "
 				}
 			},
-			crate::Formula::Or(arguments) =>
+			crate::Formula::Or(ref arguments) =>
 			{
 				let mut separator = "";
 
-				assert!(!arguments.is_empty());
-
 				for argument in arguments
 				{
-					write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
+					write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?;
 
 					separator = " or "
 				}
 			},
-			crate::Formula::Implies(crate::Implies{antecedent, implication})
-				=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence),
-					display_formula(implication, precedence))?,
-			crate::Formula::IfAndOnlyIf(crate::IfAndOnlyIf{left, right})
-				=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence),
-					display_formula(right, precedence))?,
-			crate::Formula::Compare(
-				crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
-				=> write!(format, "{:?} < {:?}", display_term(left, None),
-					display_term(right, None))?,
-			crate::Formula::Compare(
-				crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
-				=> write!(format, "{:?} <= {:?}", display_term(left, None),
-					display_term(right, None))?,
-			crate::Formula::Compare(
-				crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
-				=> write!(format, "{:?} > {:?}", display_term(left, None),
-					display_term(right, None))?,
-			crate::Formula::Compare(
-				crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
-				=> write!(format, "{:?} >= {:?}", display_term(left, None),
-					display_term(right, None))?,
-			crate::Formula::Compare(
-				crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
-				=> write!(format, "{:?} = {:?}", display_term(left, None),
-					display_term(right, None))?,
-			crate::Formula::Compare(
-				crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
-				=> write!(format, "{:?} != {:?}", display_term(left, None),
-					display_term(right, None))?,
-			crate::Formula::Boolean(true) => write!(format, "#true")?,
-			crate::Formula::Boolean(false) => write!(format, "#false")?,
-			crate::Formula::Predicate(predicate) =>
+			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)?;
 

src/lib.rs

@@ -1,4 +1,6 @@
 mod ast;
 pub mod format;
+pub mod parse;
 
-pub use ast::*;
+pub use ast::{Domain, Exists, Formula, ForAll, ImplicationDirection, Predicate, PredicateDeclaration, VariableDeclaration, Term};
+pub use parse::{formula, formulas, term};