Clarify readme

Variable declarations should only be considered equal if their identity
is equal. In other words, just because two different variable
declarations share the same name, they aren’t automatically equal. This
is to support situations in which nested variable declarations shadow
variable declarations of the same name at a higher level.

.gitignore

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

Cargo.toml

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

@@ -0,0 +1,21 @@
+# 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

@@ -0,0 +1,26 @@
+# foliage [![GitHub release](https://img.shields.io/github/release/potassco/foliage.svg?maxAge=3600)](https://github.com/potassco/foliage/releases) [![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

@@ -1,20 +0,0 @@
-#![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

@@ -1,26 +0,0 @@
-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,76 +1,563 @@
-#[derive(Eq, Hash, PartialEq)]
+// 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)]
 pub struct PredicateDeclaration
 {
 	pub name: String,
 	pub arity: usize,
 }
 
-#[derive(PartialEq)]
+impl PredicateDeclaration
-pub struct Predicate
 {
-	pub declaration: PredicateDeclaration,
+	pub fn new(name: String, arity: usize) -> Self
-	pub arguments: Vec<Term>,
+	{
+		Self
+		{
+			name,
+			arity,
+		}
+	}
 }
 
-#[derive(PartialEq)]
+pub type PredicateDeclarations = std::collections::BTreeSet<std::rc::Rc<PredicateDeclaration>>;
-pub struct Exists
-{
-	pub parameters: Vec<VariableDeclaration>,
-	pub argument: Box<Formula>,
-}
 
-#[derive(PartialEq)]
-pub struct ForAll
-{
-	pub parameters: Vec<VariableDeclaration>,
-	pub argument: Box<Formula>,
-}
-
-#[derive(PartialEq)]
-pub enum Formula
-{
-	Exists(Exists),
-	ForAll(ForAll),
-	Not(Box<Formula>),
-	And(Vec<Box<Formula>>),
-	Or(Vec<Box<Formula>>),
-	Implies(Box<Formula>, Box<Formula>),
-	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),
-}
-
-#[derive(PartialEq)]
-pub enum Domain
-{
-	Program,
-	Integer,
-}
-
-#[derive(PartialEq)]
 pub struct VariableDeclaration
 {
 	pub name: String,
-	pub domain: Domain,
 }
 
-#[derive(PartialEq)]
+impl std::cmp::PartialEq for VariableDeclaration
-pub enum Term
+{
+	#[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,
-	Integer(i64),
+}
-	Symbolic(String),
+
-	String(String),
+pub struct UnaryOperation
-	Variable(VariableDeclaration),
+{
-	Add(Box<Term>, Box<Term>),
+	pub operator: UnaryOperator,
-	Subtract(Box<Term>, Box<Term>),
+	pub argument: Box<Term>,
-	Multiply(Box<Term>, Box<Term>),
+}
-	Negative(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,
+		}
+	}
+}
+
+pub struct Predicate
+{
+	pub declaration: std::rc::Rc<PredicateDeclaration>,
+	pub arguments: Vec<Box<Term>>,
+}
+
+impl Predicate
+{
+	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,
+		}
+	}
+}
+
+// Variants
+
+pub enum Term
+{
+	BinaryOperation(BinaryOperation),
+	Boolean(bool),
+	Function(Function),
+	Integer(i32),
+	SpecialInteger(SpecialInteger),
+	String(String),
+	UnaryOperation(UnaryOperation),
+	Variable(Variable),
+}
+
+pub type Terms = Vec<Box<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: 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))
+	}
+}
+
+pub enum Formula
+{
+	And(Formulas),
+	Boolean(bool),
+	Compare(Compare),
+	Exists(Exists),
+	ForAll(ForAll),
+	IfAndOnlyIf(IfAndOnlyIf),
+	Implies(Implies),
+	Not(Box<Formula>),
+	Or(Formulas),
+	Predicate(Predicate),
+}
+
+pub type Formulas = Vec<Box<Formula>>;
+
+impl Formula
+{
+	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)
+	}
 }

src/format.rs

@@ -1,56 +1,94 @@
-struct TermDisplay<'term>
+trait Precedence
 {
-	parent_precedence: u64,
+	fn precedence(&self) -> i32;
-	term: &'term crate::Term,
 }
 
-struct FormulaDisplay<'formula>
+impl Precedence for crate::Term
 {
-	parent_precedence: u64,
+	fn precedence(&self) -> i32
-	formula: &'formula crate::Formula,
+	{
+		match &self
+		{
+			Self::Boolean(_)
+			| Self::Function(_)
+			| Self::SpecialInteger(_)
+			| Self::Integer(_)
+			| Self::String(_)
+			| Self::Variable(_)
+				=> 0,
+			Self::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..})
+				=> 1,
+			Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, ..})
+				=> 2,
+			Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, ..})
+			| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Divide, ..})
+			| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
+				=> 3,
+			Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Add, ..})
+			| Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, ..})
+				=> 4,
+			Self::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
+				=> 5,
 		}
-
-fn display_term<'term>(term: &'term crate::Term, parent_precedence: u64) -> TermDisplay<'term>
-{
-	TermDisplay
-	{
-		parent_precedence,
-		term,
 	}
 }
 
-fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedence: u64)
+impl Precedence for crate::Formula
-	-> FormulaDisplay<'formula>
 {
-	FormulaDisplay
+	fn precedence(&self) -> i32
 	{
-		parent_precedence,
+		match &self
-		formula,
+		{
+			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,
+		}
 	}
 }
 
-fn term_precedence(term: &crate::Term) -> u64
+impl std::fmt::Debug for crate::FunctionDeclaration
 {
-	match term
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		crate::Term::Infimum | crate::Term::Supremum | crate::Term::Integer(_) | crate::Term::Symbolic(_) | crate::Term::String(_) | crate::Term::Variable(_) => 0,
+		write!(format, "{}/{}", &self.name, self.arity)
-		crate::Term::Negative(_) => 1,
-		crate::Term::Multiply(_, _) => 2,
-		crate::Term::Add(_, _) | crate::Term::Subtract(_, _) => 3,
 	}
 }
 
-fn formula_precedence(formula: &crate::Formula) -> u64
+impl std::fmt::Display for crate::FunctionDeclaration
 {
-	match formula
+	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		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,
+		write!(format, "{:?}", &self)
-		crate::Formula::Exists(_) | crate::Formula::ForAll(_) => 1,
+	}
-		crate::Formula::Not(_) => 2,
+}
-		crate::Formula::And(_) => 3,
+
-		crate::Formula::Or(_) => 4,
+impl std::fmt::Debug for crate::PredicateDeclaration
-		crate::Formula::Implies(_, _) => 5,
+{
-		crate::Formula::Biconditional(_, _) => 6,
+	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)
 	}
 }
 
@@ -58,12 +96,6 @@ impl std::fmt::Debug for crate::VariableDeclaration
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		match &self.domain
-		{
-			crate::Domain::Program => write!(format, "X")?,
-			crate::Domain::Integer => write!(format, "N")?,
-		};
-
 		write!(format, "{}", &self.name)
 	}
 }
@@ -76,30 +108,90 @@ impl std::fmt::Display for crate::VariableDeclaration
 	}
 }
 
+struct TermDisplay<'term>
+{
+	parent_precedence: Option<i32>,
+	term: &'term crate::Term,
+}
+
+fn display_term<'term>(term: &'term crate::Term, parent_precedence: Option<i32>)
+	-> TermDisplay<'term>
+{
+	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 = term_precedence(self.term);
+		let precedence = self.term.precedence();
-		let requires_parentheses = precedence > self.parent_precedence;
+		let requires_parentheses = match self.parent_precedence
+		{
+			Some(parent_precedence) => precedence > parent_precedence,
+			None => false,
+		};
+		let precedence = Some(precedence);
 
 		if requires_parentheses
 		{
 			write!(format, "(")?;
 		}
 
-		match self.term
+		match &self.term
 		{
-			crate::Term::Infimum => write!(format, "#inf"),
+			crate::Term::Boolean(true) => write!(format, "true"),
-			crate::Term::Supremum => write!(format, "#sup"),
+			crate::Term::Boolean(false) => write!(format, "false"),
+			crate::Term::SpecialInteger(crate::SpecialInteger::Infimum) => write!(format, "#inf"),
+			crate::Term::SpecialInteger(crate::SpecialInteger::Supremum) => write!(format, "#sup"),
 			crate::Term::Integer(value) => write!(format, "{}", value),
-			crate::Term::Symbolic(ref value) => write!(format, "{}", value),
+			crate::Term::String(value) => write!(format, "\"{}\"", value),
-			crate::Term::String(ref value) => write!(format, "\"{}\"", value),
+			crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration),
-			crate::Term::Variable(ref declaration) => write!(format, "{:?}", declaration),
+			crate::Term::Function(function) =>
-			crate::Term::Add(ref left, ref right) => write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)),
+			{
-			crate::Term::Subtract(ref left, ref right) => write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)),
+				write!(format, "{}", function.declaration.name)?;
-			crate::Term::Multiply(ref left, ref right) => write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)),
+
-			crate::Term::Negative(ref argument) => write!(format, "-{:?}", display_term(argument, precedence)),
+				assert!(function.declaration.arity == function.arguments.len(),
+					"function has a different number of arguments than declared (expected {}, got {})",
+					function.declaration.arity, function.arguments.len());
+
+				if function.arguments.len() > 0
+				{
+					write!(format, "{}(", function.declaration.name)?;
+
+					let mut separator = "";
+
+					for argument in &function.arguments
+					{
+						write!(format, "{}{:?}", separator, display_term(&argument, None))?;
+
+						separator = ", ";
+					}
+
+					write!(format, ")")?;
+				}
+
+				Ok(())
+			},
+			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Add, left, right})
+				=> write!(format, "{:?} + {:?}", display_term(left, precedence), display_term(right, precedence)),
+			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, left, right})
+				=> write!(format, "{:?} - {:?}", display_term(left, precedence), display_term(right, precedence)),
+			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, left, right})
+				=> write!(format, "{:?} * {:?}", display_term(left, precedence), display_term(right, precedence)),
+			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Divide, left, right})
+				=> write!(format, "{:?} / {:?}", display_term(left, precedence), display_term(right, precedence)),
+			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, left, right})
+				=> write!(format, "{:?} % {:?}", display_term(left, precedence), display_term(right, precedence)),
+			crate::Term::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, left, right})
+				=> write!(format, "{:?} ** {:?}", display_term(left, precedence), display_term(right, precedence)),
+			crate::Term::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
+				=> write!(format, "-{:?}", display_term(argument, precedence)),
+			crate::Term::UnaryOperation(crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
+				=> write!(format, "|{:?}|", display_term(argument, precedence)),
 		}?;
 
 		if requires_parentheses
@@ -119,27 +211,50 @@ impl<'term> std::fmt::Display for TermDisplay<'term>
 	}
 }
 
+struct FormulaDisplay<'formula>
+{
+	parent_precedence: Option<i32>,
+	formula: &'formula crate::Formula,
+}
+
+fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedence: Option<i32>)
+	-> FormulaDisplay<'formula>
+{
+	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 = formula_precedence(self.formula);
+		let precedence = self.formula.precedence();
-		let requires_parentheses = precedence > self.parent_precedence;
+		let requires_parentheses = match self.parent_precedence
+		{
+			Some(parent_precedence) => precedence > parent_precedence,
+			None => false,
+		};
+		let precedence = Some(precedence);
 
 		if requires_parentheses
 		{
 			write!(format, "(")?;
 		}
 
-		match self.formula
+		match &self.formula
 		{
-			crate::Formula::Exists(ref exists) =>
+			crate::Formula::Exists(exists) =>
 			{
+				assert!(!exists.parameters.is_empty());
+
 				write!(format, "exists")?;
 
 				let mut separator = " ";
 
-				for parameter in &exists.parameters
+				for parameter in exists.parameters.iter()
 				{
 					write!(format, "{}{:?}", separator, parameter)?;
 
@@ -148,13 +263,15 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 
 				write!(format, " {:?}", display_formula(&exists.argument, precedence))?;
 			},
-			crate::Formula::ForAll(ref for_all) =>
+			crate::Formula::ForAll(for_all) =>
 			{
+				assert!(!for_all.parameters.is_empty());
+
 				write!(format, "forall")?;
 
 				let mut separator = " ";
 
-				for parameter in &for_all.parameters
+				for parameter in for_all.parameters.iter()
 				{
 					write!(format, "{}{:?}", separator, parameter)?;
 
@@ -163,11 +280,13 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 
 				write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
 			},
-			crate::Formula::Not(ref argument) => write!(format, "not {:?}", display_formula(argument, precedence))?,
+			crate::Formula::Not(argument) => write!(format, "not {:?}", display_formula(argument, precedence))?,
-			crate::Formula::And(ref arguments) =>
+			crate::Formula::And(arguments) =>
 			{
 				let mut separator = "";
 
+				assert!(!arguments.is_empty());
+
 				for argument in arguments
 				{
 					write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
@@ -175,10 +294,12 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 					separator = " and "
 				}
 			},
-			crate::Formula::Or(ref arguments) =>
+			crate::Formula::Or(arguments) =>
 			{
 				let mut separator = "";
 
+				assert!(!arguments.is_empty());
+
 				for argument in arguments
 				{
 					write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
@@ -186,21 +307,25 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 					separator = " or "
 				}
 			},
-			crate::Formula::Implies(ref left, ref right) => write!(format, "{:?} -> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
+			crate::Formula::Implies(crate::Implies{antecedent, implication})
-			crate::Formula::Biconditional(ref left, ref right) => write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
+				=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence), display_formula(implication, precedence))?,
-			crate::Formula::Less(ref left, ref right) => write!(format, "{:?} < {:?}", display_term(left, 1000), display_term(right, 1000))?,
+			crate::Formula::IfAndOnlyIf(crate::IfAndOnlyIf{left, right})
-			crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "{:?} <= {:?}", display_term(left, 1000), display_term(right, 1000))?,
+				=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence), display_formula(right, precedence))?,
-			crate::Formula::Greater(ref left, ref right) => write!(format, "{:?} > {:?}", display_term(left, 1000), display_term(right, 1000))?,
+			crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
-			crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "{:?} >= {:?}", display_term(left, 1000), display_term(right, 1000))?,
+				=> write!(format, "{:?} < {:?}", display_term(left, None), display_term(right, None))?,
-			crate::Formula::Equal(ref left, ref right) => write!(format, "{:?} = {:?}", display_term(left, 1000), display_term(right, 1000))?,
+			crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
-			crate::Formula::NotEqual(ref left, ref right) => write!(format, "{:?} != {:?}", display_term(left, 1000), display_term(right, 1000))?,
+				=> write!(format, "{:?} <= {:?}", display_term(left, None), display_term(right, None))?,
-			crate::Formula::Boolean(value) =>
+			crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
-				match value
+				=> write!(format, "{:?} > {:?}", display_term(left, None), display_term(right, None))?,
-				{
+			crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
-					true => write!(format, "#true")?,
+				=> write!(format, "{:?} >= {:?}", display_term(left, None), display_term(right, None))?,
-					false => write!(format, "#false")?,
+			crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
-				},
+				=> write!(format, "{:?} = {:?}", display_term(left, None), display_term(right, None))?,
-			crate::Formula::Predicate(ref predicate) =>
+			crate::Formula::Compare(crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
+				=> write!(format, "{:?} != {:?}", display_term(left, None), display_term(right, None))?,
+			crate::Formula::Boolean(true) => write!(format, "#true")?,
+			crate::Formula::Boolean(false) => write!(format, "#false")?,
+			crate::Formula::Predicate(predicate) =>
 			{
 				write!(format, "{}", predicate.declaration.name)?;
 
@@ -212,7 +337,7 @@ impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
 
 					for argument in &predicate.arguments
 					{
-						write!(format, "{}{:?}", separator, display_term(argument, 1000))?;
+						write!(format, "{}{:?}", separator, display_term(argument, None))?;
 
 						separator = ", "
 					}
@@ -243,7 +368,7 @@ impl std::fmt::Debug for crate::Formula
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{:?}", display_formula(&self, 1000))
+		write!(format, "{:?}", display_formula(&self, None))
 	}
 }
 
@@ -251,7 +376,7 @@ impl std::fmt::Display for crate::Formula
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{}", display_formula(&self, 1000))
+		write!(format, "{}", display_formula(&self, None))
 	}
 }
 
@@ -259,7 +384,7 @@ impl std::fmt::Debug for crate::Term
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{:?}", display_term(&self, 1000))
+		write!(format, "{:?}", display_term(&self, None))
 	}
 }
 
@@ -267,6 +392,6 @@ impl std::fmt::Display for crate::Term
 {
 	fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
 	{
-		write!(format, "{}", display_term(&self, 1000))
+		write!(format, "{}", display_term(&self, None))
 	}
 }

src/lib.rs

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