commit a446aed011bff4ee61b43c6a21421d3e17f512ae Author: Patrick Lühne Date: Wed Feb 5 03:17:28 2020 +0100 Initial commit This provides an abstract syntax tree for first-order logic with integer arithmetics. Initially, the following types of formulas are supported: - Booleans values (true and false) - predicates - negated formulas - comparisons of terms (<, ≤, >, ≥, =, ≠) - implications and biconditionals - conjunctions and disjunctions of formulas - existentially and universally quantified formulas In addition, these types of terms are provided: - 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) diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..b1c7301 --- /dev/null +++ b/.gitignore @@ -0,0 +1,3 @@ +/Cargo.lock +/target +**/*.rs.bk diff --git a/Cargo.toml b/Cargo.toml new file mode 100644 index 0000000..694d191 --- /dev/null +++ b/Cargo.toml @@ -0,0 +1,13 @@ +[package] +name = "foliage" +version = "0.1.0" +authors = ["Patrick Lühne "] +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" diff --git a/LICENSE.md b/LICENSE.md new file mode 100644 index 0000000..f6bc205 --- /dev/null +++ b/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. diff --git a/README.md b/README.md new file mode 100644 index 0000000..55ca534 --- /dev/null +++ b/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) diff --git a/src/ast.rs b/src/ast.rs new file mode 100644 index 0000000..4bf9b4d --- /dev/null +++ b/src/ast.rs @@ -0,0 +1,565 @@ +// 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>; + +#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] +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>; + +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 + { + 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>; + +// Terms + +pub struct BinaryOperation +{ + pub operator: BinaryOperator, + pub left: Box, + pub right: Box, +} + +impl BinaryOperation +{ + pub fn new(operator: BinaryOperator, left: Box, right: Box) -> Self + { + Self + { + operator, + left, + right, + } + } +} + +pub struct Function +{ + pub declaration: std::rc::Rc, + pub arguments: Vec>, +} + +impl Function +{ + pub fn new(declaration: &std::rc::Rc, arguments: Vec>) -> 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, +} + +impl UnaryOperation +{ + pub fn new(operator: UnaryOperator, argument: Box) -> Self + { + Self + { + operator, + argument, + } + } +} + +pub struct Variable +{ + pub declaration: std::rc::Rc, +} + +impl Variable +{ + pub fn new(declaration: &std::rc::Rc) -> Self + { + Self + { + declaration: std::rc::Rc::clone(declaration), + } + } +} + +// Formulas + +pub struct Compare +{ + pub operator: ComparisonOperator, + pub left: Box, + pub right: Box, +} + +impl Compare +{ + pub fn new(operator: ComparisonOperator, left: Box, right: Box) -> Self + { + Self + { + operator, + left, + right, + } + } +} + +pub struct Exists +{ + pub parameters: std::rc::Rc, + pub argument: Box, +} + +impl Exists +{ + pub fn new(parameters: std::rc::Rc, argument: Box) -> Self + { + Self + { + parameters, + argument, + } + } +} + +pub struct ForAll +{ + pub parameters: std::rc::Rc, + pub argument: Box, +} + +impl ForAll +{ + pub fn new(parameters: std::rc::Rc, argument: Box) -> Self + { + Self + { + parameters, + argument, + } + } +} + +pub struct IfAndOnlyIf +{ + pub left: Box, + pub right: Box, +} + +impl IfAndOnlyIf +{ + pub fn new(left: Box, right: Box) -> Self + { + Self + { + left, + right, + } + } +} + +pub struct Implies +{ + pub antecedent: Box, + pub implication: Box, +} + +impl Implies +{ + pub fn new(antecedent: Box, implication: Box) -> Self + { + Self + { + antecedent, + implication, + } + } +} + +pub struct Predicate +{ + pub declaration: std::rc::Rc, + pub arguments: Vec>, +} + +impl Predicate +{ + pub fn new(declaration: &std::rc::Rc, arguments: Vec>) -> 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>; + +impl Term +{ + pub fn absolute_value(argument: Box) -> Self + { + Self::unary_operation(UnaryOperator::AbsoluteValue, argument) + } + + pub fn add(left: Box, right: Box) -> Self + { + Self::binary_operation(BinaryOperator::Add, left, right) + } + + pub fn binary_operation(operator: BinaryOperator, left: Box, right: Box) -> Self + { + Self::BinaryOperation(BinaryOperation::new(operator, left, right)) + } + + pub fn boolean(value: bool) -> Self + { + Self::Boolean(value) + } + + pub fn divide(left: Box, right: Box) -> Self + { + Self::binary_operation(BinaryOperator::Divide, left, right) + } + + pub fn exponentiate(left: Box, right: Box) -> Self + { + Self::binary_operation(BinaryOperator::Exponentiate, left, right) + } + + pub fn false_() -> Self + { + Self::boolean(false) + } + + pub fn function(declaration: &std::rc::Rc, arguments: Vec>) + -> 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, right: Box) -> Self + { + Self::binary_operation(BinaryOperator::Modulo, left, right) + } + + pub fn multiply(left: Box, right: Box) -> Self + { + Self::binary_operation(BinaryOperator::Multiply, left, right) + } + + pub fn negative(argument: Box) -> 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, right: Box) -> 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) -> Self + { + Self::UnaryOperation(UnaryOperation::new(operator, argument)) + } + + pub fn variable(declaration: &std::rc::Rc) -> 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), + Or(Formulas), + Predicate(Predicate), +} + +pub type Formulas = Vec>; + +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, right: Box) -> Self + { + Self::Compare(Compare::new(operator, left, right)) + } + + pub fn exists(parameters: std::rc::Rc, argument: Box) -> Self + { + assert!(!parameters.is_empty()); + + Self::Exists(Exists::new(parameters, argument)) + } + + pub fn equal(left: Box, right: Box) -> Self + { + Self::compare(ComparisonOperator::Equal, left, right) + } + + pub fn false_() -> Self + { + Self::boolean(false) + } + + pub fn for_all(parameters: std::rc::Rc, argument: Box) -> Self + { + assert!(!parameters.is_empty()); + + Self::ForAll(ForAll::new(parameters, argument)) + } + + pub fn greater(left: Box, right: Box) -> Self + { + Self::compare(ComparisonOperator::Greater, left, right) + } + + pub fn greater_or_equal(left: Box, right: Box) -> Self + { + Self::compare(ComparisonOperator::GreaterOrEqual, left, right) + } + + pub fn if_and_only_if(left: Box, right: Box) -> Self + { + Self::IfAndOnlyIf(IfAndOnlyIf::new(left, right)) + } + + pub fn implies(antecedent: Box, consequent: Box) -> Self + { + Self::Implies(Implies::new(antecedent, consequent)) + } + + pub fn less(left: Box, right: Box) -> Self + { + Self::compare(ComparisonOperator::Less, left, right) + } + + pub fn less_or_equal(left: Box, right: Box) -> Self + { + Self::compare(ComparisonOperator::LessOrEqual, left, right) + } + + pub fn not(argument: Box) -> Self + { + Self::Not(argument) + } + + pub fn not_equal(left: Box, right: Box) -> 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, arguments: Vec>) + -> Self + { + Self::Predicate(Predicate::new(declaration, arguments)) + } + + pub fn true_() -> Self + { + Self::boolean(true) + } +} diff --git a/src/format.rs b/src/format.rs new file mode 100644 index 0000000..49a7a6f --- /dev/null +++ b/src/format.rs @@ -0,0 +1,433 @@ +trait Precedence +{ + fn precedence(&self) -> i32; +} + +impl Precedence for crate::Term +{ + fn precedence(&self) -> i32 + { + 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, + } + } +} + +impl Precedence for crate::Formula +{ + fn precedence(&self) -> i32 + { + match &self + { + 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, + } + } +} + +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) + } +} + +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) + } +} + +struct TermDisplay<'term> +{ + parent_precedence: Option, + term: &'term crate::Term, +} + +fn display_term<'term>(term: &'term crate::Term, parent_precedence: Option) + -> 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 = self.term.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 + { + crate::Term::Boolean(true) => write!(format, "true"), + 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::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.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 + { + 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) + } +} + +struct FormulaDisplay<'formula> +{ + parent_precedence: Option, + formula: &'formula crate::Formula, +} + +fn display_formula<'formula>(formula: &'formula crate::Formula, parent_precedence: Option) + -> 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 = self.formula.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 + { + crate::Formula::Exists(exists) => + { + assert!(!exists.parameters.is_empty()); + + write!(format, "exists")?; + + let mut separator = " "; + + for parameter in exists.parameters.iter() + { + write!(format, "{}{:?}", separator, parameter)?; + + separator = ", " + } + + write!(format, " {:?}", display_formula(&exists.argument, precedence))?; + }, + crate::Formula::ForAll(for_all) => + { + assert!(!for_all.parameters.is_empty()); + + write!(format, "forall")?; + + let mut separator = " "; + + for parameter in for_all.parameters.iter() + { + write!(format, "{}{:?}", separator, parameter)?; + + separator = ", " + } + + write!(format, " {:?}", display_formula(&for_all.argument, precedence))?; + }, + crate::Formula::Not(argument) => write!(format, "not {:?}", + display_formula(argument, precedence))?, + crate::Formula::And(arguments) => + { + let mut separator = ""; + + assert!(!arguments.is_empty()); + + for argument in arguments + { + write!(format, "{}{:?}", separator, display_formula(argument, precedence))?; + + separator = " and " + } + }, + crate::Formula::Or(arguments) => + { + let mut separator = ""; + + assert!(!arguments.is_empty()); + + for argument in arguments + { + write!(format, "{}{:?}", separator, display_formula(argument, precedence))?; + + 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) => + { + 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)) + } +} diff --git a/src/lib.rs b/src/lib.rs new file mode 100644 index 0000000..b5f6020 --- /dev/null +++ b/src/lib.rs @@ -0,0 +1,4 @@ +mod ast; +pub mod format; + +pub use ast::*;