Compare commits

...

90 Commits

Author SHA1 Message Date
Patrick Lühne 80980e4e11
Remove redundant indirection 3 years ago
Patrick Lühne 02cf3f552b
Remove redundant indirection 3 years ago
Patrick Lühne 80636b447a
Simplify representation of quantified formulas 3 years ago
Patrick Lühne 903993dbec
Minor clean-up 3 years ago
Patrick Lühne f4f8dbf396
Minor clean-up 3 years ago
Patrick Lühne 680f17bda0
Refactoring 3 years ago
Patrick Lühne f949c0f3f8
Refactoring 3 years ago
Patrick Lühne 7b2b292727
Remove unneeded parentheses enum 3 years ago
Patrick Lühne 6c326ddb70
Refactor parenthesis rules for terms 3 years ago
Patrick Lühne 9754f933ef
Reorganize term formatter tests 3 years ago
Patrick Lühne 351d7cdd19
Rewrite term formatting tests for clarity 3 years ago
Patrick Lühne 3b7394a43e
Support quantified expressions with 0 parameters 3 years ago
Patrick Lühne 9a8013f1cb
Support empty n-aries 3 years ago
Patrick Lühne 51cbdb313f
Finish testing biconditionals 3 years ago
Patrick Lühne 3bd52845be
Reorganize tests 3 years ago
Patrick Lühne 186ed314d3
Rewrite tests for clarity 3 years ago
Patrick Lühne a8df440fdf
Add type annotations 3 years ago
Patrick Lühne d051b84845
Rewrite tests for clarity 3 years ago
Patrick Lühne 704fe597a2
Rewrite tests for clarity 3 years ago
Patrick Lühne f3b4cdc399
Experimental method for testing all permutations 3 years ago
Patrick Lühne 21d4b1d605
Test biconditionals 3 years ago
Patrick Lühne 0c132edc07
Continue testing implication 3 years ago
Patrick Lühne b6308695f6
Fix precedence of implication 3 years ago
Patrick Lühne e0dbb8b75f
Refactor parenthesis requirement check 3 years ago
Patrick Lühne 80d7460ec1
Start testing implications 3 years ago
Patrick Lühne 33f751781e
Test disjunction 3 years ago
Patrick Lühne e4700fc638
Test conjunction 3 years ago
Patrick Lühne 9e74116a4d
Clean up tests 3 years ago
Patrick Lühne 5512813cba
Clean up tests 3 years ago
Patrick Lühne c11156b2ce
Test quantified formulas 3 years ago
Patrick Lühne cc3265fc72
Test negation 3 years ago
Patrick Lühne 121c858bff
Remove unneeded precedence implementation 3 years ago
Patrick Lühne 881419b8ee
Address warnings 3 years ago
Patrick Lühne dc27ab8aeb
Fix 3 years ago
Patrick Lühne c8ca7ba337
Remove ChildPosition enum 3 years ago
Patrick Lühne 1968ed83ee
Refactor precedence rules for formulas 3 years ago
Patrick Lühne d1ab7963b1
Before larger refactoring 3 years ago
Patrick Lühne 1a497254a8
Add unit tests for precedence-0 formulas and lower 3 years ago
Patrick Lühne d57b3b3b62
Test remaining formula types 3 years ago
Patrick Lühne 57d568916f
Minor formatting 3 years ago
Patrick Lühne e4fe047aba
Start testing formula formatter 3 years ago
Patrick Lühne 600a6a1b4b
Refactor precedence rules 3 years ago
Patrick Lühne 8bf9d4bd45
Fix implication formatting 3 years ago
Patrick Lühne f82a20e5f1
Work in progress 3 years ago
Patrick Lühne 5c51018ab1
Add unit test for function declaration formatting 3 years ago
Patrick Lühne 23e1854346
Test term formatting 3 years ago
Patrick Lühne a3da369346
Split formatting functionality into two files 3 years ago
Patrick Lühne caf957deed
Fix implication parser and output 3 years ago
Patrick Lühne 1ece0e89ef
Add note 3 years ago
Patrick Lühne 0fdec430af
Parentheses for stronger checks 3 years ago
Patrick Lühne 5ea0a96ec4
Test disjunction parser 3 years ago
Patrick Lühne 17d8dbd8ba
Test conjunction parser 3 years ago
Patrick Lühne 834e59207f
Add note 3 years ago
Patrick Lühne 257e02f285
Minor refactoring 3 years ago
Patrick Lühne 2e3707e0af
Check that names don’t start with special characters 3 years ago
Patrick Lühne d0263dd1c4
Add missing word boundary character 3 years ago
Patrick Lühne a7dd4d2fe9
Disallow reserved keywords as names 3 years ago
Patrick Lühne c127bc5eea
Address clippy warning 3 years ago
Patrick Lühne cb616eba87
Refactor term parser tests 3 years ago
Patrick Lühne 95677bae34
Fix negation parser 3 years ago
Patrick Lühne 3414e8075c
Address warnings 3 years ago
Patrick Lühne 675063e1b8
Move string parser to separate module 3 years ago
Patrick Lühne 7d78a504b1
Move special integer parser to separate module 3 years ago
Patrick Lühne 6f86cd40d7
Move integer parser to separate module 3 years ago
Patrick Lühne 29ea4578e4
Move boolean parser to separate module 3 years ago
Patrick Lühne a1bbae9201
Finish implementing formula parsing 3 years ago
Patrick Lühne 1c00e5be16
Continue parsing formulas 3 years ago
Patrick Lühne 1b89d8900e
Start parsing formulas 3 years ago
Patrick Lühne af1ec8a606
Fix term parsing and finish tests 3 years ago
Patrick Lühne 2907d10148
Make parse feature the default 3 years ago
Patrick Lühne 19e70a90c5
Test associativity of multiplication 3 years ago
Patrick Lühne 385c878597
Add term parsing test 3 years ago
Patrick Lühne 5b98e8a29c
Finish implementing term parsing 3 years ago
Patrick Lühne 3530364ea8
Implement variable parsing 3 years ago
Patrick Lühne deae102405
Require word boundaries around names 3 years ago
Patrick Lühne 0fc8506164
Implement booleans 3 years ago
Patrick Lühne e6a5c20d42
Add pipe character to allowed word boundaries 3 years ago
Patrick Lühne d5cd179a2d
Implement strings 3 years ago
Patrick Lühne 5ec9331b4c
Implement word boundaries 3 years ago
Patrick Lühne 896af02120
Start parsing terms 3 years ago
Patrick Lühne 0c057211ed
Implement name parsing 3 years ago
Patrick Lühne 91918cf645
Start reimplementing parser 3 years ago
Patrick Lühne fd6ba4a005
Test crate with GitHub Actions 3 years ago
Patrick Lühne 153f77621e
Fix precedence of absolute value operation 3 years ago
Patrick Lühne 551c35ed75
Fix formatting of binary operations 3 years ago
Patrick Lühne 549f127729
Derive simple enums from basic traits 3 years ago
Patrick Lühne a304ec9a75
Fix output of Booleans in formulas 3 years ago
Patrick Lühne a82b4080c8
Fix function formatting 3 years ago
Patrick Lühne 90f7be2f33
Minor refactoring for clarity 3 years ago
Patrick Lühne a127a053b2
Support formatting special integers separately 3 years ago
  1. 32
      .github/workflows/main.yml
  2. 7
      Cargo.toml
  3. 134
      src/ast.rs
  4. 69
      src/error.rs
  5. 433
      src/format.rs
  6. 1237
      src/format/formulas.rs
  7. 1089
      src/format/terms.rs
  8. 6
      src/lib.rs
  9. 32
      src/parse.rs
  10. 683
      src/parse/formulas.rs
  11. 86
      src/parse/helpers.rs
  12. 249
      src/parse/literals.rs
  13. 159
      src/parse/names.rs
  14. 852
      src/parse/terms.rs
  15. 72
      src/utils.rs

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

@ -11,3 +11,10 @@ keywords = ["logic"]
categories = ["data-structures", "science"]
license = "MIT"
edition = "2018"
[dependencies]
nom = {version = "5.1", optional = true}
[features]
default = ["parse"]
parse = ["nom"]

@ -1,5 +1,6 @@
// Operators
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum BinaryOperator
{
Add,
@ -10,6 +11,7 @@ pub enum BinaryOperator
Exponentiate,
}
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum ComparisonOperator
{
Greater,
@ -20,12 +22,22 @@ pub enum ComparisonOperator
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)]
@ -115,6 +127,17 @@ impl std::cmp::Ord for VariableDeclaration
}
}
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
@ -130,6 +153,7 @@ pub type VariableDeclarations = Vec<std::rc::Rc<VariableDeclaration>>;
// Terms
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct BinaryOperation
{
pub operator: BinaryOperator,
@ -150,33 +174,36 @@ impl BinaryOperation
}
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Function
{
pub declaration: std::rc::Rc<FunctionDeclaration>,
pub arguments: Vec<Box<Term>>,
pub arguments: Terms,
}
impl Function
{
pub fn new(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
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: std::rc::Rc::clone(declaration),
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,
@ -195,6 +222,7 @@ impl UnaryOperation
}
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Variable
{
pub declaration: std::rc::Rc<VariableDeclaration>,
@ -202,17 +230,18 @@ pub struct Variable
impl Variable
{
pub fn new(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
pub fn new(declaration: std::rc::Rc<VariableDeclaration>) -> Self
{
Self
{
declaration: std::rc::Rc::clone(declaration),
declaration,
}
}
}
// Formulas
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Compare
{
pub operator: ComparisonOperator,
@ -233,31 +262,14 @@ impl Compare
}
}
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
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct QuantifiedFormula
{
pub parameters: std::rc::Rc<VariableDeclarations>,
pub argument: Box<Formula>,
}
impl ForAll
impl QuantifiedFormula
{
pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
{
@ -269,58 +281,45 @@ impl ForAll
}
}
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,
}
}
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Implies
{
pub direction: ImplicationDirection,
pub antecedent: Box<Formula>,
pub implication: Box<Formula>,
}
impl Implies
{
pub fn new(antecedent: Box<Formula>, implication: Box<Formula>) -> Self
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: Vec<Box<Term>>,
pub arguments: Terms,
}
impl Predicate
{
pub fn new(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
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: std::rc::Rc::clone(declaration),
declaration,
arguments,
}
}
@ -328,6 +327,7 @@ impl Predicate
// Variants
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum Term
{
BinaryOperation(BinaryOperation),
@ -340,7 +340,7 @@ pub enum Term
Variable(Variable),
}
pub type Terms = Vec<Box<Term>>;
pub type Terms = Vec<Term>;
impl Term
{
@ -379,8 +379,7 @@ impl Term
Self::boolean(false)
}
pub fn function(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>)
-> Self
pub fn function(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Terms) -> Self
{
Self::Function(Function::new(declaration, arguments))
}
@ -440,34 +439,33 @@ impl Term
Self::UnaryOperation(UnaryOperation::new(operator, argument))
}
pub fn variable(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
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),
Boolean(bool),
Compare(Compare),
Exists(Exists),
ForAll(ForAll),
IfAndOnlyIf(IfAndOnlyIf),
Exists(QuantifiedFormula),
ForAll(QuantifiedFormula),
IfAndOnlyIf(Formulas),
Implies(Implies),
Not(Box<Formula>),
Or(Formulas),
Predicate(Predicate),
}
pub type Formulas = Vec<Box<Formula>>;
pub type Formulas = Vec<Formula>;
impl Formula
{
pub fn and(arguments: Formulas) -> Self
{
assert!(!arguments.is_empty());
Self::And(arguments)
}
@ -483,9 +481,7 @@ impl Formula
pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
{
assert!(!parameters.is_empty());
Self::Exists(Exists::new(parameters, argument))
Self::Exists(QuantifiedFormula::new(parameters, argument))
}
pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
@ -500,9 +496,7 @@ impl Formula
pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
{
assert!(!parameters.is_empty());
Self::ForAll(ForAll::new(parameters, argument))
Self::ForAll(QuantifiedFormula::new(parameters, argument))
}
pub fn greater(left: Box<Term>, right: Box<Term>) -> Self
@ -515,14 +509,15 @@ impl Formula
Self::compare(ComparisonOperator::GreaterOrEqual, left, right)
}
pub fn if_and_only_if(left: Box<Formula>, right: Box<Formula>) -> Self
pub fn if_and_only_if(arguments: Formulas) -> Self
{
Self::IfAndOnlyIf(IfAndOnlyIf::new(left, right))
Self::IfAndOnlyIf(arguments)
}
pub fn implies(antecedent: Box<Formula>, consequent: Box<Formula>) -> Self
pub fn implies(direction: ImplicationDirection, antecedent: Box<Formula>,
consequent: Box<Formula>) -> Self
{
Self::Implies(Implies::new(antecedent, consequent))
Self::Implies(Implies::new(direction, antecedent, consequent))
}
pub fn less(left: Box<Term>, right: Box<Term>) -> Self
@ -547,13 +542,10 @@ impl Formula
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
pub fn predicate(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Terms) -> Self
{
Self::Predicate(Predicate::new(declaration, arguments))
}

@ -0,0 +1,69 @@
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,
}
}
}

@ -1,431 +1,2 @@
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<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);
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<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);
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))
}
}
mod formulas;
mod terms;

File diff suppressed because it is too large Load Diff

File diff suppressed because it is too large Load Diff

@ -1,4 +1,10 @@
mod ast;
mod error;
pub mod format;
#[cfg(feature = "parse")]
pub mod parse;
mod utils;
pub use ast::*;
pub use error::Error;
pub use utils::VariableDeclarationStack;

@ -0,0 +1,32 @@
mod formulas;
mod helpers;
mod literals;
mod names;
mod terms;
pub(crate) use helpers::word_boundary;
pub(crate) use literals::{boolean, integer, special_integer, string};
pub(crate) use names::{function_or_predicate_name, variable_name};
pub use terms::term;
pub use formulas::formula;
pub struct Declarations
{
function_declarations: std::cell::RefCell<crate::FunctionDeclarations>,
predicate_declarations: std::cell::RefCell<crate::PredicateDeclarations>,
variable_declaration_stack: std::cell::RefCell<crate::VariableDeclarationStack>,
}
impl Declarations
{
pub fn new() -> Self
{
Self
{
function_declarations: std::cell::RefCell::new(crate::FunctionDeclarations::new()),
predicate_declarations: std::cell::RefCell::new(crate::PredicateDeclarations::new()),
variable_declaration_stack:
std::cell::RefCell::new(crate::VariableDeclarationStack::new()),
}
}
}

@ -0,0 +1,683 @@
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
{</