13 Commits
19 changed files with 1519 additions and 5392 deletions
-32
View File
@@ -1,32 +0,0 @@
name: Rust
on:
push:
branches: [master]
pull_request:
branches: [master]
jobs:
test:
name: Test
runs-on: ubuntu-latest
strategy:
matrix:
build: [stable, beta, nightly]
include:
- build: stable
rust: stable
- build: beta
rust: beta
- build: nightly
rust: nightly
steps:
- uses: actions/checkout@v2
- name: Install Rust (rustup)
run: rustup update ${{ matrix.rust }} --no-self-update && rustup default ${{ matrix.rust }}
shell: bash
- name: Build
run: cargo build --verbose
- name: Run tests
run: cargo test --verbose
+1 -1
View File
@@ -1,3 +1,3 @@
/Cargo.lock
/target
**/*.rs.bk
Cargo.lock
+1 -9
View File
@@ -2,15 +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]
log = "0.4"
nom = "5.0"
-21
View File
@@ -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.
-26
View File
@@ -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)
+20
View File
@@ -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, "");
});
}
}
+26
View File
@@ -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(())
}
+56 -591
View File
@@ -1,611 +1,76 @@
use crate::flavor::{FunctionDeclaration as _, PredicateDeclaration as _};
// Operators
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum BinaryOperator
{
Add,
Subtract,
Multiply,
Divide,
Modulo,
Exponentiate,
}
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum ComparisonOperator
{
Greater,
Less,
LessOrEqual,
GreaterOrEqual,
NotEqual,
Equal,
}
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum UnaryOperator
{
AbsoluteValue,
Negative,
}
// ImplicationDirection
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum ImplicationDirection
{
LeftToRight,
RightToLeft,
}
// Primitives
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct FunctionDeclaration
{
pub name: String,
pub arity: usize,
}
impl FunctionDeclaration
{
pub fn new(name: String, arity: usize) -> Self
{
Self
{
name,
arity,
}
}
}
pub type FunctionDeclarations<F> =
std::collections::BTreeSet<std::rc::Rc<<F as crate::flavor::Flavor>::FunctionDeclaration>>;
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
#[derive(Eq, Hash, PartialEq)]
pub struct PredicateDeclaration
{
pub name: String,
pub arity: usize,
}
impl PredicateDeclaration
#[derive(PartialEq)]
pub struct Predicate
{
pub fn new(name: String, arity: usize) -> Self
{
Self
{
name,
arity,
}
}
pub declaration: PredicateDeclaration,
pub arguments: Vec<Term>,
}
pub type PredicateDeclarations<F> =
std::collections::BTreeSet<std::rc::Rc<<F as crate::flavor::Flavor>::PredicateDeclaration>>;
#[derive(PartialEq)]
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,
}
impl std::cmp::PartialEq for VariableDeclaration
{
#[inline(always)]
fn eq(&self, other: &Self) -> bool
{
let l = self as *const Self;
let r = other as *const Self;
l.eq(&r)
}
}
impl std::cmp::Eq for VariableDeclaration
{
}
impl std::cmp::PartialOrd for VariableDeclaration
{
#[inline(always)]
fn partial_cmp(&self, other: &VariableDeclaration) -> Option<std::cmp::Ordering>
{
let l = self as *const VariableDeclaration;
let r = other as *const VariableDeclaration;
l.partial_cmp(&r)
}
}
impl std::cmp::Ord for VariableDeclaration
{
#[inline(always)]
fn cmp(&self, other: &VariableDeclaration) -> std::cmp::Ordering
{
let l = self as *const VariableDeclaration;
let r = other as *const VariableDeclaration;
l.cmp(&r)
}
}
impl std::hash::Hash for VariableDeclaration
{
#[inline(always)]
fn hash<H: std::hash::Hasher>(&self, state: &mut H)
{
let p = self as *const VariableDeclaration;
p.hash(state);
}
}
impl VariableDeclaration
{
pub fn new(name: String) -> Self
{
Self
{
name,
}
}
}
pub type VariableDeclarations<F> =
Vec<std::rc::Rc<<F as crate::flavor::Flavor>::VariableDeclaration>>;
// Terms
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct BinaryOperation<F>
where
F: crate::flavor::Flavor,
{
pub operator: BinaryOperator,
pub left: Box<Term<F>>,
pub right: Box<Term<F>>,
}
impl<F> BinaryOperation<F>
where
F: crate::flavor::Flavor,
{
pub fn new(operator: BinaryOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self
{
operator,
left,
right,
}
}
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Function<F>
where
F: crate::flavor::Flavor,
{
pub declaration: std::rc::Rc<F::FunctionDeclaration>,
pub arguments: Terms<F>,
}
impl<F> Function<F>
where
F: crate::flavor::Flavor,
{
pub fn new(declaration: std::rc::Rc<F::FunctionDeclaration>, arguments: Terms<F>) -> Self
{
assert_eq!(declaration.arity(), arguments.len(),
"function has a different number of arguments than declared");
Self
{
declaration,
arguments,
}
}
}
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum SpecialInteger
#[derive(PartialEq)]
pub enum Term
{
Infimum,
Supremum,
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct UnaryOperation<F>
where
F: crate::flavor::Flavor,
{
pub operator: UnaryOperator,
pub argument: Box<Term<F>>,
}
impl<F> UnaryOperation<F>
where
F: crate::flavor::Flavor,
{
pub fn new(operator: UnaryOperator, argument: Box<Term<F>>) -> Self
{
Self
{
operator,
argument,
}
}
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Variable<F>
where
F: crate::flavor::Flavor,
{
pub declaration: std::rc::Rc<F::VariableDeclaration>,
}
impl<F> Variable<F>
where
F: crate::flavor::Flavor,
{
pub fn new(declaration: std::rc::Rc<F::VariableDeclaration>) -> Self
{
Self
{
declaration,
}
}
}
// Formulas
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Compare<F>
where
F: crate::flavor::Flavor,
{
pub operator: ComparisonOperator,
pub left: Box<Term<F>>,
pub right: Box<Term<F>>,
}
impl<F> Compare<F>
where
F: crate::flavor::Flavor,
{
pub fn new(operator: ComparisonOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self
{
operator,
left,
right,
}
}
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct QuantifiedFormula<F>
where
F: crate::flavor::Flavor,
{
pub parameters: std::rc::Rc<VariableDeclarations<F>>,
pub argument: Box<Formula<F>>,
}
impl<F> QuantifiedFormula<F>
where
F: crate::flavor::Flavor,
{
pub fn new(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
{
Self
{
parameters,
argument,
}
}
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Implies<F>
where
F: crate::flavor::Flavor,
{
pub direction: ImplicationDirection,
pub antecedent: Box<Formula<F>>,
pub implication: Box<Formula<F>>,
}
impl<F> Implies<F>
where
F: crate::flavor::Flavor,
{
pub fn new(direction: ImplicationDirection, antecedent: Box<Formula<F>>,
implication: Box<Formula<F>>)
-> Self
{
Self
{
direction,
antecedent,
implication,
}
}
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Predicate<F>
where
F: crate::flavor::Flavor,
{
pub declaration: std::rc::Rc<F::PredicateDeclaration>,
pub arguments: Terms<F>,
}
impl<F> Predicate<F>
where
F: crate::flavor::Flavor,
{
pub fn new(declaration: std::rc::Rc<F::PredicateDeclaration>, arguments: Terms<F>) -> Self
{
assert_eq!(declaration.arity(), arguments.len(),
"predicate has a different number of arguments than declared");
Self
{
declaration,
arguments,
}
}
}
// Variants
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum Term<F>
where
F: crate::flavor::Flavor,
{
BinaryOperation(BinaryOperation<F>),
Boolean(bool),
Function(Function<F>),
Integer(i32),
SpecialInteger(SpecialInteger),
Integer(i64),
Symbolic(String),
String(String),
UnaryOperation(UnaryOperation<F>),
Variable(Variable<F>),
}
pub type Terms<F> = Vec<Term<F>>;
impl<F> Term<F>
where
F: crate::flavor::Flavor,
{
pub fn absolute_value(argument: Box<Term<F>>) -> Self
{
Self::unary_operation(UnaryOperator::AbsoluteValue, argument)
}
pub fn add(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::binary_operation(BinaryOperator::Add, left, right)
}
pub fn binary_operation(operator: BinaryOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::BinaryOperation(BinaryOperation::new(operator, left, right))
}
pub fn boolean(value: bool) -> Self
{
Self::Boolean(value)
}
pub fn divide(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::binary_operation(BinaryOperator::Divide, left, right)
}
pub fn exponentiate(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::binary_operation(BinaryOperator::Exponentiate, left, right)
}
pub fn false_() -> Self
{
Self::boolean(false)
}
pub fn function(declaration: std::rc::Rc<F::FunctionDeclaration>, arguments: Terms<F>) -> 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<F>>, right: Box<Term<F>>) -> Self
{
Self::binary_operation(BinaryOperator::Modulo, left, right)
}
pub fn multiply(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::binary_operation(BinaryOperator::Multiply, left, right)
}
pub fn negative(argument: Box<Term<F>>) -> 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<F>>, right: Box<Term<F>>) -> 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<F>>) -> Self
{
Self::UnaryOperation(UnaryOperation::new(operator, argument))
}
pub fn variable(declaration: std::rc::Rc<F::VariableDeclaration>) -> Self
{
Self::Variable(Variable::new(declaration))
}
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum Formula<F>
where
F: crate::flavor::Flavor,
{
And(Formulas<F>),
Boolean(bool),
Compare(Compare<F>),
Exists(QuantifiedFormula<F>),
ForAll(QuantifiedFormula<F>),
IfAndOnlyIf(Formulas<F>),
Implies(Implies<F>),
Not(Box<Formula<F>>),
Or(Formulas<F>),
Predicate(Predicate<F>),
}
pub type Formulas<F> = Vec<Formula<F>>;
impl<F> Formula<F>
where
F: crate::flavor::Flavor,
{
pub fn and(arguments: Formulas<F>) -> Self
{
Self::And(arguments)
}
pub fn boolean(value: bool) -> Self
{
Self::Boolean(value)
}
pub fn compare(operator: ComparisonOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::Compare(Compare::new(operator, left, right))
}
pub fn exists(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
{
Self::Exists(QuantifiedFormula::new(parameters, argument))
}
pub fn equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::compare(ComparisonOperator::Equal, left, right)
}
pub fn false_() -> Self
{
Self::boolean(false)
}
pub fn for_all(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
{
Self::ForAll(QuantifiedFormula::new(parameters, argument))
}
pub fn greater(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::compare(ComparisonOperator::Greater, left, right)
}
pub fn greater_or_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::compare(ComparisonOperator::GreaterOrEqual, left, right)
}
pub fn if_and_only_if(arguments: Formulas<F>) -> Self
{
Self::IfAndOnlyIf(arguments)
}
pub fn implies(direction: ImplicationDirection, antecedent: Box<Formula<F>>,
consequent: Box<Formula<F>>) -> Self
{
Self::Implies(Implies::new(direction, antecedent, consequent))
}
pub fn less(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::compare(ComparisonOperator::Less, left, right)
}
pub fn less_or_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::compare(ComparisonOperator::LessOrEqual, left, right)
}
pub fn not(argument: Box<Formula<F>>) -> Self
{
Self::Not(argument)
}
pub fn not_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{
Self::compare(ComparisonOperator::NotEqual, left, right)
}
pub fn or(arguments: Formulas<F>) -> Self
{
Self::Or(arguments)
}
pub fn predicate(declaration: std::rc::Rc<F::PredicateDeclaration>, arguments: Terms<F>) -> Self
{
Self::Predicate(Predicate::new(declaration, arguments))
}
pub fn true_() -> Self
{
Self::boolean(true)
}
}
pub struct OpenFormula<F>
where
F: crate::flavor::Flavor,
{
pub free_variable_declarations: std::rc::Rc<VariableDeclarations<F>>,
pub formula: Formula<F>,
Variable(VariableDeclaration),
Add(Box<Term>, Box<Term>),
Subtract(Box<Term>, Box<Term>),
Multiply(Box<Term>, Box<Term>),
Negative(Box<Term>),
}
-85
View File
@@ -1,85 +0,0 @@
pub trait FunctionDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
fn arity(&self) -> usize;
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool;
}
impl FunctionDeclaration for crate::FunctionDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{}", self.name)
}
fn arity(&self) -> usize
{
self.arity
}
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool
{
self.name == other_name && self.arity == other_arity
}
}
pub trait PredicateDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
fn arity(&self) -> usize;
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool;
}
impl PredicateDeclaration for crate::PredicateDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{}", self.name)
}
fn arity(&self) -> usize
{
self.arity
}
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool
{
self.name == other_name && self.arity == other_arity
}
}
pub trait VariableDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
fn matches_name(&self, other_name: &str) -> bool;
}
impl VariableDeclaration for crate::VariableDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{}", self.name)
}
fn matches_name(&self, other_name: &str) -> bool
{
self.name == other_name
}
}
pub trait Flavor
{
type FunctionDeclaration: FunctionDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
type PredicateDeclaration:
PredicateDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
type VariableDeclaration: VariableDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
}
pub struct DefaultFlavor;
impl Flavor for DefaultFlavor
{
type FunctionDeclaration = crate::FunctionDeclaration;
type PredicateDeclaration = crate::PredicateDeclaration;
type VariableDeclaration = crate::VariableDeclaration;
}
+315 -2
View File
@@ -1,2 +1,315 @@
pub mod formulas;
pub mod terms;
struct TermDisplay<'parent>
{
parent: Option<&'parent crate::Term>,
term: &'parent crate::Term,
}
struct FormulaDisplay<'parent>
{
parent: Option<&'parent crate::Formula>,
formula: &'parent crate::Formula,
}
fn display_term<'parent>(term: &'parent crate::Term, parent: Option<&'parent crate::Term>) -> TermDisplay<'parent>
{
TermDisplay
{
parent,
term,
}
}
fn display_formula<'parent>(formula: &'parent crate::Formula, parent: Option<&'parent crate::Formula>)
-> FormulaDisplay<'parent>
{
FormulaDisplay
{
parent,
formula,
}
}
fn term_precedence(term: &crate::Term) -> u64
{
match term
{
crate::Term::Infimum | crate::Term::Supremum | crate::Term::Integer(_) | crate::Term::Symbolic(_) | crate::Term::String(_) | crate::Term::Variable(_) => 0,
crate::Term::Negative(_) => 1,
crate::Term::Multiply(_, _) => 2,
crate::Term::Add(_, _) | crate::Term::Subtract(_, _) => 3,
}
}
fn term_requires_parentheses(child: &crate::Term, parent: Option<&crate::Term>) -> bool
{
match parent
{
None => false,
Some(parent) =>
{
let child_precedence = term_precedence(child);
let parent_precedence = term_precedence(parent);
if child_precedence != parent_precedence
{
return child_precedence > parent_precedence;
}
// Subtraction isnt associative, so handle them separately
// TODO: only do this for right-hand side of subtractions
match parent
{
crate::Term::Subtract(_, _) => true,
_ => false,
}
},
}
}
fn formula_precedence(formula: &crate::Formula) -> u64
{
match formula
{
crate::Formula::Predicate(_) | crate::Formula::Boolean(_) | crate::Formula::Less(_, _) | crate::Formula::LessOrEqual(_, _) | crate::Formula::Greater(_, _) | crate::Formula::GreaterOrEqual(_, _) | crate::Formula::Equal(_, _) | crate::Formula::NotEqual(_, _) => 0,
crate::Formula::Exists(_) | crate::Formula::ForAll(_) => 1,
crate::Formula::Not(_) => 2,
crate::Formula::And(_) => 3,
crate::Formula::Or(_) => 4,
crate::Formula::Implies(_, _) => 5,
crate::Formula::Biconditional(_, _) => 6,
}
}
fn formula_requires_parentheses(child: &crate::Formula, parent: Option<&crate::Formula>) -> bool
{
match parent
{
None => false,
Some(parent) =>
{
let child_precedence = formula_precedence(child);
let parent_precedence = formula_precedence(parent);
if child_precedence != parent_precedence
{
return child_precedence > parent_precedence;
}
// Implications arent associative, so handle them separately
match parent
{
crate::Formula::Implies(_, _) => true,
_ => false,
}
},
}
}
impl std::fmt::Debug for crate::VariableDeclaration
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{}", &self.name)
}
}
impl std::fmt::Display for crate::VariableDeclaration
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{:?}", &self)
}
}
impl<'term> std::fmt::Debug for TermDisplay<'term>
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
let requires_parentheses = term_requires_parentheses(self.term, self.parent);
if requires_parentheses
{
write!(format, "(")?;
}
match self.term
{
crate::Term::Infimum => write!(format, "#inf"),
crate::Term::Supremum => write!(format, "#sup"),
crate::Term::Integer(value) => write!(format, "{}", value),
crate::Term::Symbolic(ref value) => write!(format, "{}", value),
crate::Term::String(ref value) => write!(format, "\"{}\"", value),
crate::Term::Variable(ref declaration) => write!(format, "{:?}", declaration),
crate::Term::Add(ref left, ref right) => write!(format, "{:?} + {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))),
crate::Term::Subtract(ref left, ref right) => write!(format, "{:?} - {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))),
crate::Term::Multiply(ref left, ref right) => write!(format, "{:?} * {:?}", display_term(left, Some(self.term)), display_term(right, Some(self.term))),
crate::Term::Negative(ref argument) => write!(format, "-{:?}", display_term(argument, Some(self.term))),
}?;
if requires_parentheses
{
write!(format, ")")?;
}
Ok(())
}
}
impl<'term> std::fmt::Display for TermDisplay<'term>
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{:?}", self)
}
}
impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
let requires_parentheses = formula_requires_parentheses(self.formula, self.parent);
if requires_parentheses
{
write!(format, "(")?;
}
match self.formula
{
crate::Formula::Exists(ref exists) =>
{
write!(format, "exists")?;
let mut separator = " ";
for parameter in &exists.parameters
{
write!(format, "{}{:?}", separator, parameter)?;
separator = ", "
}
write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula)))?;
},
crate::Formula::ForAll(ref for_all) =>
{
write!(format, "forall")?;
let mut separator = " ";
for parameter in &for_all.parameters
{
write!(format, "{}{:?}", separator, parameter)?;
separator = ", "
}
write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula)))?;
},
crate::Formula::Not(ref argument) => write!(format, "not {:?}", display_formula(argument, Some(self.formula)))?,
crate::Formula::And(ref arguments) =>
{
let mut separator = "";
for argument in arguments
{
write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?;
separator = " and "
}
},
crate::Formula::Or(ref arguments) =>
{
let mut separator = "";
for argument in arguments
{
write!(format, "{}{:?}", separator, display_formula(argument, Some(self.formula)))?;
separator = " or "
}
},
crate::Formula::Implies(ref left, ref right) => write!(format, "{:?} -> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
crate::Formula::Biconditional(ref left, ref right) => write!(format, "{:?} <-> {:?}", display_formula(left, Some(self.formula)), display_formula(right, Some(self.formula)))?,
crate::Formula::Less(ref left, ref right) => write!(format, "{:?} < {:?}", display_term(left, None), display_term(right, None))?,
crate::Formula::LessOrEqual(ref left, ref right) => write!(format, "{:?} <= {:?}", display_term(left, None), display_term(right, None))?,
crate::Formula::Greater(ref left, ref right) => write!(format, "{:?} > {:?}", display_term(left, None), display_term(right, None))?,
crate::Formula::GreaterOrEqual(ref left, ref right) => write!(format, "{:?} >= {:?}", display_term(left, None), display_term(right, None))?,
crate::Formula::Equal(ref left, ref right) => write!(format, "{:?} = {:?}", display_term(left, None), display_term(right, None))?,
crate::Formula::NotEqual(ref left, ref right) => write!(format, "{:?} != {:?}", display_term(left, None), display_term(right, None))?,
crate::Formula::Boolean(value) =>
match value
{
true => write!(format, "#true")?,
false => write!(format, "#false")?,
},
crate::Formula::Predicate(ref predicate) =>
{
write!(format, "{}", predicate.declaration.name)?;
if !predicate.arguments.is_empty()
{
write!(format, "(")?;
let mut separator = "";
for argument in &predicate.arguments
{
write!(format, "{}{:?}", separator, display_term(argument, None))?;
separator = ", "
}
write!(format, ")")?;
}
},
}
if requires_parentheses
{
write!(format, ")")?;
}
Ok(())
}
}
impl<'formula> std::fmt::Display for FormulaDisplay<'formula>
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{:?}", self)
}
}
impl std::fmt::Debug for crate::Formula
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{:?}", display_formula(&self, None))
}
}
impl std::fmt::Display for crate::Formula
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{}", display_formula(&self, None))
}
}
impl std::fmt::Debug for crate::Term
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{:?}", display_term(&self, None))
}
}
impl std::fmt::Display for crate::Term
{
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(format, "{}", display_term(&self, None))
}
}
File diff suppressed because it is too large Load Diff
-1090
View File
File diff suppressed because it is too large Load Diff
+4 -9
View File
@@ -1,11 +1,6 @@
mod ast;
pub mod flavor;
mod format;
mod parse;
mod utils;
pub mod format;
pub mod parse;
pub use ast::*;
pub use format::{formulas::FormulaDisplay, terms::TermDisplay};
pub use flavor::{DefaultFlavor, Flavor};
pub use utils::*;
pub use parse::{DefaultParser, Parser};
pub use ast::{Domain, Exists, Formula, ForAll, Predicate, PredicateDeclaration, VariableDeclaration, Term};
pub use parse::{formula, formulas, term};
+1096 -111
View File
File diff suppressed because it is too large Load Diff
-182
View File
@@ -1,182 +0,0 @@
pub type Source = Box<dyn std::error::Error>;
pub struct Location
{
start: usize,
end: Option<usize>,
}
impl Location
{
pub fn new(start: usize, end: Option<usize>) -> Self
{
Self
{
start,
end,
}
}
}
pub enum Kind
{
UnmatchedParenthesis,
CharacterNotAllowed(char),
ParseNumber(String),
MixedImplicationDirections(Location),
ExpectedVariableDeclaration,
UnexpectedToken,
EmptyExpression,
ExpectedLogicalConnectiveArgument(String),
ExpectedTerm,
MultipleComparisonOperators(crate::ComparisonOperator, crate::ComparisonOperator),
}
pub struct Error
{
pub kind: Kind,
pub location: Location,
pub source: Option<Source>,
}
impl Error
{
pub(crate) fn new(kind: Kind, location: Location) -> Self
{
Self
{
kind,
location,
source: None,
}
}
pub(crate) fn with<S: Into<Source>>(mut self, source: S) -> Self
{
self.source = Some(source.into());
self
}
pub(crate) fn new_unmatched_parenthesis(location: Location) -> Self
{
Self::new(Kind::UnmatchedParenthesis, location)
}
pub(crate) fn new_character_not_allowed(character: char, location: Location) -> Self
{
Self::new(Kind::CharacterNotAllowed(character), location)
}
pub(crate) fn new_parse_number<I: Into<String>, S: Into<Source>>(input: I, location: Location,
source: S)
-> Self
{
Self::new(Kind::ParseNumber(input.into()), location).with(source)
}
pub(crate) fn new_mixed_implication_directions(location_1: Location, location_2: Location)
-> Self
{
Self::new(Kind::MixedImplicationDirections(location_2), location_1)
}
pub(crate) fn new_expected_variable_declaration(location: Location) -> Self
{
Self::new(Kind::ExpectedVariableDeclaration, location)
}
pub(crate) fn new_unexpected_token(location: Location) -> Self
{
Self::new(Kind::UnexpectedToken, location)
}
pub(crate) fn new_empty_expression(location: Location) -> Self
{
Self::new(Kind::EmptyExpression, location)
}
pub(crate) fn new_expected_logical_connective_argument(logical_connective_name: String,
location: Location)
-> Self
{
Self::new(Kind::ExpectedLogicalConnectiveArgument(logical_connective_name), location)
}
pub(crate) fn new_expected_term(location: Location) -> Self
{
Self::new(Kind::ExpectedTerm, location)
}
pub(crate) fn new_multiple_comparison_operators(
comparison_operator_1: crate::ComparisonOperator,
comparison_operator_2: crate::ComparisonOperator, location: Location)
-> Self
{
Self::new(Kind::MultipleComparisonOperators(comparison_operator_1, comparison_operator_2),
location)
}
}
impl std::fmt::Debug for Error
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
if let Some(end) = self.location.end
{
write!(formatter, "parsing error at {}:{}: ", self.location.start, end)?;
}
else
{
write!(formatter, "parsing error at {}: ", self.location.start)?;
}
match &self.kind
{
Kind::UnmatchedParenthesis => write!(formatter, "unmatched parenthesis")?,
Kind::CharacterNotAllowed(character) =>
write!(formatter, "character not allowed: {}", character)?,
Kind::ParseNumber(input) => write!(formatter, "could not “{}” as number", input)?,
// TODO: print second location properly
Kind::MixedImplicationDirections(_location_2) =>
write!(formatter, "-> and <- implications may not be mixed within the same scope")?,
Kind::ExpectedVariableDeclaration =>
write!(formatter, "expected a variable declaration")?,
Kind::UnexpectedToken => write!(formatter, "unexpected token")?,
Kind::EmptyExpression => write!(formatter, "empty expression")?,
Kind::ExpectedLogicalConnectiveArgument(ref logical_connective_name) =>
write!(formatter, "this “{}” logical connective is missing an argument",
logical_connective_name)?,
Kind::ExpectedTerm => write!(formatter, "expected a term")?,
Kind::MultipleComparisonOperators(comparison_operator_1, comparison_operator_2) =>
write!(formatter, "chained comparisons arent supported (found “{:?}” and “{:?}” in the same formula), consider separating them with “and”",
comparison_operator_1, comparison_operator_2)?,
}
if let Some(source) = &self.source
{
write!(formatter, "\nerror source: {}", source)?;
}
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,
}
}
}
-564
View File
@@ -1,564 +0,0 @@
use super::terms::*;
use super::tokens::*;
pub fn formula<P>(input: &str, parser: &P)
-> Result<crate::OpenFormula<P::Flavor>, crate::parse::Error>
where
P: super::Parser,
{
let variable_declaration_stack = crate::VariableDeclarationStackLayer::free();
let formula_str = FormulaStr::new(input, parser, &variable_declaration_stack);
let formula = formula_str.parse(0)?;
let free_variable_declarations = match variable_declaration_stack
{
crate::VariableDeclarationStackLayer::Free(free_variable_declarations) =>
std::rc::Rc::new(free_variable_declarations.into_inner()),
_ => unreachable!(),
};
Ok(crate::OpenFormula
{
formula,
free_variable_declarations,
})
}
pub(crate) fn predicate_name(identifier: &str) -> Option<(&str, &str)>
{
function_name(identifier)
}
#[derive(Clone, Copy, Eq, PartialEq)]
enum LogicalConnective
{
And,
IfAndOnlyIf,
ImpliesLeftToRight,
ImpliesRightToLeft,
Or,
}
impl LogicalConnective
{
fn level(&self) -> usize
{
match self
{
Self::And => 1,
Self::Or => 2,
Self::ImpliesLeftToRight
| Self::ImpliesRightToLeft => 3,
Self::IfAndOnlyIf => 4,
}
}
}
impl std::fmt::Debug for LogicalConnective
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match &self
{
Self::And => write!(formatter, "and"),
Self::IfAndOnlyIf => write!(formatter, "<->"),
Self::ImpliesLeftToRight => write!(formatter, "->"),
Self::ImpliesRightToLeft => write!(formatter, "<-"),
Self::Or => write!(formatter, "or"),
}
}
}
struct FormulaStr<'i, 'd, 'p, 'v, P>
where
P: super::Parser,
{
input: &'i str,
parser: &'d P,
variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, P::Flavor>,
}
impl<'i, 'd, 'p, 'v, P> FormulaStr<'i, 'd, 'p, 'v, P>
where
P: super::Parser,
{
pub fn new(input: &'i str, parser: &'d P,
variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, P::Flavor>)
-> Self
{
Self
{
input,
parser,
variable_declaration_stack,
}
}
fn logical_connectives(&self) -> Tokens<'i, impl FnMut(Token<'i>) -> Option<LogicalConnective>>
{
let functor = |token| match token
{
Token::Identifier("and") => Some(LogicalConnective::And),
Token::Identifier("or") => Some(LogicalConnective::Or),
Token::Symbol(Symbol::ArrowLeft) => Some(LogicalConnective::ImpliesRightToLeft),
Token::Symbol(Symbol::ArrowLeftAndRight) => Some(LogicalConnective::IfAndOnlyIf),
Token::Symbol(Symbol::ArrowRight) => Some(LogicalConnective::ImpliesLeftToRight),
_ => None,
};
Tokens::new_filter_map(self.input, functor)
}
fn split_at_logical_connective(&self, logical_connective: LogicalConnective)
-> TokenSplit<Tokens<'i, impl FnMut(Token<'i>) -> Option<Token<'i>>>>
{
let predicate = move |token: &_| match token
{
Token::Identifier("and") => logical_connective == LogicalConnective::And,
Token::Identifier("or") => logical_connective == LogicalConnective::Or,
Token::Symbol(Symbol::ArrowLeft) =>
logical_connective == LogicalConnective::ImpliesRightToLeft,
Token::Symbol(Symbol::ArrowLeftAndRight) =>
logical_connective == LogicalConnective::IfAndOnlyIf,
Token::Symbol(Symbol::ArrowRight) =>
logical_connective == LogicalConnective::ImpliesLeftToRight,
_ => false,
};
Tokens::new_filter(self.input, predicate).split()
}
pub fn top_level_logical_connective(&self)
-> Result<Option<LogicalConnective>, crate::parse::Error>
{
let mut top_level_logical_connective = None;
for logical_connective in self.logical_connectives()
{
let (_, logical_connective) = logical_connective?;
top_level_logical_connective = match top_level_logical_connective
{
None => Some(logical_connective),
Some(top_level_logical_connective) =>
{
let implication_directions_are_mixed =
logical_connective == LogicalConnective::ImpliesLeftToRight
&& top_level_logical_connective == LogicalConnective::ImpliesRightToLeft
|| logical_connective == LogicalConnective::ImpliesRightToLeft
&& top_level_logical_connective == LogicalConnective::ImpliesLeftToRight;
if implication_directions_are_mixed
{
return Err(crate::parse::Error::new_mixed_implication_directions(
crate::parse::error::Location::new(0, Some(0)),
crate::parse::error::Location::new(0, Some(0))));
}
if logical_connective.level() > top_level_logical_connective.level()
{
Some(logical_connective)
}
else
{
Some(top_level_logical_connective)
}
},
}
}
Ok(top_level_logical_connective)
}
fn comparison_operators(&self) -> Tokens<'i, impl FnMut(Token<'i>)
-> Option<crate::ComparisonOperator>>
{
let functor = |token| match token
{
Token::Symbol(symbol) => match symbol
{
Symbol::Greater => Some(crate::ComparisonOperator::Greater),
Symbol::GreaterOrEqual => Some(crate::ComparisonOperator::GreaterOrEqual),
Symbol::Less => Some(crate::ComparisonOperator::Less),
Symbol::LessOrEqual => Some(crate::ComparisonOperator::LessOrEqual),
Symbol::Equal => Some(crate::ComparisonOperator::Equal),
Symbol::NotEqual => Some(crate::ComparisonOperator::NotEqual),
_ => None,
},
_ => None,
};
Tokens::new_filter_map(self.input, functor)
}
pub fn parse(&self, level: usize) -> Result<crate::Formula<P::Flavor>, crate::parse::Error>
{
let indentation = " ".repeat(level);
let input = trim_start(self.input);
log::trace!("{}- parsing formula: {}", indentation, input);
match input.chars().next()
{
Some(')') => return Err(crate::parse::Error::new_unmatched_parenthesis(
crate::parse::error::Location::new(0, Some(0)))),
None => return Err(crate::parse::Error::new_empty_expression(
crate::parse::error::Location::new(0, Some(0)))),
_ => (),
}
// Parse logical infix connectives
if let Some(top_level_logical_connective) = self.top_level_logical_connective()?
{
log::trace!("{} parsing “{:?}” logical connective", indentation,
top_level_logical_connective);
// Parse arguments of n-ary logical infix connectives
let arguments_n_ary = ||
{
// TODO: improve error handling if the formulas between the operators are invalid
self.split_at_logical_connective(top_level_logical_connective)
.map(|argument| FormulaStr::new(argument?, self.parser, self.variable_declaration_stack).parse(level + 1))
.collect::<Result<Vec<_>, _>>()
};
match top_level_logical_connective
{
LogicalConnective::And => return Ok(crate::Formula::and(arguments_n_ary()?)),
LogicalConnective::Or => return Ok(crate::Formula::or(arguments_n_ary()?)),
LogicalConnective::IfAndOnlyIf =>
return Ok(crate::Formula::if_and_only_if(arguments_n_ary()?)),
LogicalConnective::ImpliesLeftToRight =>
return self.implication_left_to_right(
self.split_at_logical_connective(top_level_logical_connective), level + 1),
LogicalConnective::ImpliesRightToLeft =>
{
let mut argument_iterator =
self.split_at_logical_connective(top_level_logical_connective);
let first_argument = argument_iterator.next().ok_or_else(||
crate::parse::Error::new_expected_logical_connective_argument(
"right-to-left implication".to_string(),
crate::parse::error::Location::new(0, Some(0))))?;
let first_argument = FormulaStr::new(first_argument?, self.parser, self.variable_declaration_stack).parse(level + 1)?;
return argument_iterator.try_fold(first_argument,
|accumulator, argument|
{
let argument = FormulaStr::new(argument?, self.parser, self.variable_declaration_stack).parse(level + 1)?;
Ok(crate::Formula::implies(crate::ImplicationDirection::RightToLeft,
Box::new(argument), Box::new(accumulator)))
});
},
}
}
// Parse quantified formulas
if let Some((identifier, input)) = identifier(input)
{
match identifier
{
"not" =>
{
let input = trim_start(input);
log::trace!("{} parsing “not” formula body: {}", indentation, input);
let argument = FormulaStr::new(input, self.parser, self.variable_declaration_stack).parse(level + 1)?;
return Ok(crate::Formula::not(Box::new(argument)));
},
"true" =>
{
if !input.trim().is_empty()
{
return Err(crate::parse::Error::new_unexpected_token(
crate::parse::error::Location::new(0, Some(0))))
}
return Ok(crate::Formula::true_());
},
"false" =>
{
if !input.trim().is_empty()
{
return Err(crate::parse::Error::new_unexpected_token(
crate::parse::error::Location::new(0, Some(0))))
}
return Ok(crate::Formula::false_());
},
_ => (),
}
let quantifier = match identifier
{
"exists" => Some(Quantifier::Existential),
"forall" => Some(Quantifier::Universal),
_ => None,
};
if let Some(quantifier) = quantifier
{
let input = trim_start(input);
log::trace!("{} parsing “{:?}” formula body: {}", indentation, quantifier, input);
return self.quantified_formula(input, quantifier, level + 1);
}
}
let mut comparison_operators = self.comparison_operators();
// Parse comparisons
if let Some(comparison_operator) = comparison_operators.next()
{
let (_, comparison_operator) = comparison_operator?;
// Comparisons with more than one comparison operator arent supported
if let Some(next_comparison_operator) = comparison_operators.next()
{
let (_, next_comparison_operator) = next_comparison_operator?;
return Err(crate::parse::Error::new_multiple_comparison_operators(
comparison_operator, next_comparison_operator,
crate::parse::error::Location::new(0, Some(0))));
}
log::trace!("{} parsing “{:?}” comparison: {}", indentation, comparison_operator, input);
let mut comparison_operator_split = self.comparison_operators().split();
// Theres exactly one comparison operator in this formula, as we have verified above.
// Hence, the split is guaranteed to generate exactly these two elements
let input_left = comparison_operator_split.next().unwrap()?;
let input_right = comparison_operator_split.next().unwrap()?;
assert!(comparison_operator_split.next().is_none());
let argument_left =
TermStr::new(input_left, self.parser, self.variable_declaration_stack)
.parse(level + 1)?;
let argument_right =
TermStr::new(input_right, self.parser, self.variable_declaration_stack)
.parse(level + 1)?;
return Ok(crate::Formula::compare(comparison_operator, Box::new(argument_left),
Box::new(argument_right)));
}
// Parse predicates
if let Some((predicate_name, input)) = predicate_name(input)
{
log::trace!("{} parsing predicate {}", indentation, predicate_name);
let input = trim_start(input);
// Parse arguments if there are any
let (arguments, input) = match parenthesized_expression(input)?
{
Some((parenthesized_expression, input)) =>
{
let functor = |token: &_| *token == Token::Symbol(Symbol::Comma);
let arguments = Tokens::new_filter(parenthesized_expression, functor).split()
.map(|argument| TermStr::new(argument?, self.parser,
self.variable_declaration_stack)
.parse(level + 1))
.collect::<Result<_, _>>()?;
(arguments, input)
}
None => (vec![], input),
};
if !input.trim().is_empty()
{
return Err(crate::parse::Error::new_unexpected_token(
crate::parse::error::Location::new(0, Some(0))))
}
let declaration = self.parser.find_or_create_predicate_declaration(predicate_name,
arguments.len());
return Ok(crate::Formula::predicate(declaration, arguments));
}
// Parse parenthesized formulas
if let Some((parenthesized_expression, input)) = parenthesized_expression(input)?
{
if !input.trim().is_empty()
{
return Err(crate::parse::Error::new_unexpected_token(
crate::parse::error::Location::new(0, Some(0))));
}
return FormulaStr::new(parenthesized_expression, self.parser, self.variable_declaration_stack).parse(level + 1);
}
Err(crate::parse::Error::new_unexpected_token(
crate::parse::error::Location::new(0, Some(0))))
}
// TODO: refactor
fn implication_left_to_right_inner<T>(&self, mut argument_iterator: T, level: usize)
-> Result<Option<crate::Formula<P::Flavor>>, crate::parse::Error>
where
T: std::iter::Iterator<Item = Result<&'i str, crate::parse::Error>>
{
match argument_iterator.next()
{
Some(argument) =>
{
// TODO: improve error handling if antecedent cannot be parsed
let argument = FormulaStr::new(argument?, self.parser, self.variable_declaration_stack).parse(level)?;
match self.implication_left_to_right_inner(argument_iterator, level)?
{
Some(next_argument) => Ok(Some(crate::Formula::implies(
crate::ImplicationDirection::LeftToRight, Box::new(argument),
Box::new(next_argument)))),
None => Ok(Some(argument)),
}
},
None => Ok(None),
}
}
fn implication_left_to_right<T>(&self, mut argument_iterator: T, level: usize)
-> Result<crate::Formula<P::Flavor>, crate::parse::Error>
where
T: std::iter::Iterator<Item = Result<&'i str, crate::parse::Error>>
{
match argument_iterator.next()
{
Some(argument) =>
{
// TODO: improve error handling if antecedent cannot be parsed
let argument = FormulaStr::new(argument?, self.parser, self.variable_declaration_stack).parse(level)?;
match self.implication_left_to_right_inner(argument_iterator, level)?
{
Some(next_argument) => Ok(crate::Formula::implies(
crate::ImplicationDirection::LeftToRight, Box::new(argument),
Box::new(next_argument))),
None => Err(crate::parse::Error::new_expected_logical_connective_argument(
"left-to-right implication".to_string(),
crate::parse::error::Location::new(0, Some(0)))),
}
},
None => Err(crate::parse::Error::new_expected_logical_connective_argument(
"left-to-right implication".to_string(),
crate::parse::error::Location::new(0, Some(0)))),
}
}
// TODO: refactor without input argument
fn quantified_formula(&self, input: &str, quantifier: Quantifier, level: usize)
-> Result<crate::Formula<P::Flavor>, crate::parse::Error>
{
let (parameters, input) = match variable_declarations::<P>(input)?
{
Some(variable_declarations) => variable_declarations,
None => return Err(crate::parse::Error::new_expected_variable_declaration(
crate::parse::error::Location::new(0, Some(0)))),
};
let parameters = std::rc::Rc::new(parameters);
let variable_declaration_stack = crate::VariableDeclarationStackLayer::bound(
self.variable_declaration_stack, std::rc::Rc::clone(&parameters));
let formula_str =
FormulaStr::new(input.trim(), self.parser, &variable_declaration_stack);
let formula = Box::new(formula_str.parse(level)?);
let formula = match quantifier
{
Quantifier::Existential => crate::Formula::exists(parameters, formula),
Quantifier::Universal => crate::Formula::for_all(parameters, formula),
};
Ok(formula)
}
}
#[derive(Clone, Copy, Eq, PartialEq)]
pub(crate) enum Quantifier
{
Existential,
Universal,
}
impl std::fmt::Debug for Quantifier
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match &self
{
Self::Existential => write!(formatter, "exists"),
Self::Universal => write!(formatter, "forall"),
}
}
}
#[cfg(test)]
mod tests
{
use super::*;
#[test]
fn tokenize_formula_logical_connectives()
{
let parser = crate::parse::DefaultParser::new();
let variable_declaration_stack = crate::VariableDeclarationStackLayer::free();
let formula_str = |input| FormulaStr::new(input, &parser, &variable_declaration_stack);
let f = formula_str("((forall X exists Y (p(X) -> q(Y)) and false) or p) -> false");
assert_eq!(f.top_level_logical_connective().unwrap(),
Some(LogicalConnective::ImpliesLeftToRight));
let mut i = f.logical_connectives();
assert_eq!(i.next().unwrap().unwrap().1, LogicalConnective::ImpliesLeftToRight);
assert!(i.next().is_none());
let f = formula_str("forall X exists Y (p(X) -> q(Y)) and false or p -> false");
assert_eq!(f.top_level_logical_connective().unwrap(),
Some(LogicalConnective::ImpliesLeftToRight));
let mut i = f.logical_connectives();
assert_eq!(i.next().unwrap().unwrap().1, LogicalConnective::And);
assert_eq!(i.next().unwrap().unwrap().1, LogicalConnective::Or);
assert_eq!(i.next().unwrap().unwrap().1, LogicalConnective::ImpliesLeftToRight);
assert!(i.next().is_none());
let f = formula_str(" p -> forall X exists Y (p(X) -> q(Y)) and false or p -> false ");
assert_eq!(f.top_level_logical_connective().unwrap(),
Some(LogicalConnective::ImpliesLeftToRight));
let mut i = f.split_at_logical_connective(LogicalConnective::ImpliesLeftToRight);
assert_eq!(i.next().unwrap().unwrap(), "p");
assert_eq!(i.next().unwrap().unwrap(), "forall X exists Y (p(X) -> q(Y)) and false or p");
assert_eq!(i.next().unwrap().unwrap(), "false");
assert!(i.next().is_none());
let f = formula_str(" p -> forall X exists Y (p(X) -> q(Y)) and false or p -> false ");
assert_eq!(f.top_level_logical_connective().unwrap(),
Some(LogicalConnective::ImpliesLeftToRight));
let mut i = f.split_at_logical_connective(LogicalConnective::And);
assert_eq!(i.next().unwrap().unwrap(), "p -> forall X exists Y (p(X) -> q(Y))");
assert_eq!(i.next().unwrap().unwrap(), "false or p -> false");
assert!(i.next().is_none());
let f = formula_str(" p and forall X exists Y (p(X) -> q(Y)) and false or p or false ");
assert_eq!(f.top_level_logical_connective().unwrap(), Some(LogicalConnective::Or));
let mut i = f.split_at_logical_connective(LogicalConnective::Or);
assert_eq!(i.next().unwrap().unwrap(), "p and forall X exists Y (p(X) -> q(Y)) and false");
assert_eq!(i.next().unwrap().unwrap(), "p");
assert_eq!(i.next().unwrap().unwrap(), "false");
assert!(i.next().is_none());
let f = formula_str(" (p and q) ");
assert!(f.top_level_logical_connective().unwrap().is_none());
let mut i = f.split_at_logical_connective(LogicalConnective::And);
assert_eq!(i.next().unwrap().unwrap(), "(p and q)");
assert!(i.next().is_none());
assert!(formula_str(" a -> b -> c ").parse(0).is_ok());
assert!(formula_str(" a -> b <- c ").parse(0).is_err());
assert!(formula_str(" p -> forall X exists Y (p(X) -> q(Y)) and false or p -> false ")
.parse(0).is_ok());
}
}
-651
View File
@@ -1,651 +0,0 @@
use super::tokens::*;
pub(crate) fn function_name(input: &str) -> Option<(&str, &str)>
{
let (identifier, remaining_input) = identifier(input)?;
if is_keyword(identifier)
{
return None;
}
let mut characters = identifier.chars();
while let Some(character) = characters.next()
{
match character
{
'_' => continue,
_ if character.is_ascii_lowercase() => return Some((identifier, remaining_input)),
_ => return None,
}
}
None
}
fn variable_name(input: &str) -> Option<(&str, &str)>
{
let (identifier, remaining_input) = identifier(input)?;
let mut characters = identifier.chars();
while let Some(character) = characters.next()
{
match character
{
'_' => continue,
_ if character.is_ascii_uppercase() => return Some((identifier, remaining_input)),
_ => return None,
}
}
None
}
pub fn is_function_name(identifier: &str) -> bool
{
if is_keyword(identifier)
{
return false;
}
let mut characters = identifier.chars();
while let Some(character) = characters.next()
{
match character
{
'_' => continue,
_ if character.is_ascii_lowercase() => return true,
_ => return false,
}
}
false
}
fn is_variable_name(identifier: &str) -> bool
{
let mut characters = identifier.chars();
while let Some(character) = characters.next()
{
match character
{
'_' => continue,
_ if character.is_ascii_uppercase() => return true,
_ => return false,
}
}
false
}
pub(crate) fn variable_declaration<P>(input: &str)
-> Option<(<P::Flavor as crate::flavor::Flavor>::VariableDeclaration, &str)>
where
P: crate::parse::Parser,
{
variable_name(input)
.map(|(variable_name, remaining_input)|
(<P as crate::parse::Parser>::new_variable_declaration(variable_name.to_string()),
remaining_input))
}
pub(crate) fn variable_declarations<P>(input: &str)
-> Result<Option<(crate::VariableDeclarations<P::Flavor>, &str)>, crate::parse::Error>
where
P: crate::parse::Parser,
{
let mut variable_declarations = vec![];
let (first_variable_declaration, mut input) = match variable_declaration::<P>(input)
{
Some(first_variable_declaration) => first_variable_declaration,
None => return Ok(None),
};
variable_declarations.push(std::rc::Rc::new(first_variable_declaration));
loop
{
input = trim_start(input);
input = match symbol(input)
{
Some((Symbol::Comma, input)) => input,
// TODO: detect redeclarations, such as in “exists X, Y, X”
_ => return Ok(Some((variable_declarations, input))),
};
input = trim_start(input);
let (variable_declaration, remaining_input) = match variable_declaration::<P>(input)
{
Some(variable_declaration) => variable_declaration,
None => return Err(crate::parse::Error::new_expected_variable_declaration(
crate::parse::error::Location::new(0, Some(0)))),
};
input = remaining_input;
variable_declarations.push(std::rc::Rc::new(variable_declaration));
}
}
#[derive(Clone, Copy, Eq, PartialEq)]
pub(crate) enum ArithmeticOperatorClass
{
Exponential,
Multiplicative,
Additive,
}
impl ArithmeticOperatorClass
{
fn level(&self) -> usize
{
match self
{
Self::Exponential => 1,
Self::Multiplicative => 2,
Self::Additive => 3,
}
}
}
impl std::fmt::Debug for ArithmeticOperatorClass
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match &self
{
Self::Exponential => write!(formatter, "exponential"),
Self::Multiplicative => write!(formatter, "multiplicative"),
Self::Additive => write!(formatter, "additive"),
}
}
}
pub(crate) struct TermStr<'i, 'd, 'v, 'p, P>
where
P: super::Parser,
{
input: &'i str,
parser: &'d P,
variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, P::Flavor>,
}
impl<'i, 'd, 'v, 'p, P> TermStr<'i, 'd, 'v, 'p, P>
where
P: super::Parser,
{
pub fn new(input: &'i str, parser: &'d P,
variable_declaration_stack: &'v crate::VariableDeclarationStackLayer<'p, P::Flavor>)
-> Self
{
Self
{
input,
parser,
variable_declaration_stack,
}
}
fn arithmetic_operator_classes(&self) -> Tokens<'i, impl FnMut(Token<'i>)
-> Option<ArithmeticOperatorClass>>
{
let functor = |token| match token
{
Token::Symbol(Symbol::Exponentiation) => Some(ArithmeticOperatorClass::Exponential),
Token::Symbol(Symbol::Multiplication) => Some(ArithmeticOperatorClass::Multiplicative),
Token::Symbol(Symbol::Division) => Some(ArithmeticOperatorClass::Multiplicative),
Token::Symbol(Symbol::Percent) => Some(ArithmeticOperatorClass::Multiplicative),
Token::Symbol(Symbol::Plus) => Some(ArithmeticOperatorClass::Additive),
Token::Symbol(Symbol::Minus) => Some(ArithmeticOperatorClass::Additive),
_ => None,
};
// TODO: refactor so that self.input is always set correctly
Tokens::new_filter_map(self.input, functor)
}
fn filter_by_arithmetic_operator_class(&self,
arithmetic_operator_class: ArithmeticOperatorClass)
-> Tokens<'i, impl FnMut(Token<'i>) -> Option<crate::BinaryOperator>>
{
let functor = move |token| match token
{
Token::Symbol(Symbol::Exponentiation) =>
if arithmetic_operator_class == ArithmeticOperatorClass::Exponential
{
Some(crate::BinaryOperator::Exponentiate)
}
else
{
None
},
Token::Symbol(Symbol::Multiplication) =>
if arithmetic_operator_class == ArithmeticOperatorClass::Multiplicative
{
Some(crate::BinaryOperator::Multiply)
}
else
{
None
},
Token::Symbol(Symbol::Division) =>
if arithmetic_operator_class == ArithmeticOperatorClass::Multiplicative
{
Some(crate::BinaryOperator::Divide)
}
else
{
None
},
Token::Symbol(Symbol::Percent) =>
if arithmetic_operator_class == ArithmeticOperatorClass::Multiplicative
{
Some(crate::BinaryOperator::Modulo)
}
else
{
None
},
Token::Symbol(Symbol::Plus) =>
if arithmetic_operator_class == ArithmeticOperatorClass::Additive
{
Some(crate::BinaryOperator::Add)
}
else
{
None
},
Token::Symbol(Symbol::Minus) =>
if arithmetic_operator_class == ArithmeticOperatorClass::Additive
{
Some(crate::BinaryOperator::Subtract)
}
else
{
None
},
_ => None,
};
Tokens::new_filter_map(self.input, functor)
}
pub fn top_level_arithmetic_operator_class(&self)
-> Result<Option<ArithmeticOperatorClass>, crate::parse::Error>
{
let mut top_level_arithmetic_operator_class = None;
for arithmetic_operator_class in self.arithmetic_operator_classes()
{
let (_, arithmetic_operator_class) = arithmetic_operator_class?;
top_level_arithmetic_operator_class = match top_level_arithmetic_operator_class
{
None => Some(arithmetic_operator_class),
Some(top_level_arithmetic_operator_class) =>
{
if arithmetic_operator_class.level()
> top_level_arithmetic_operator_class.level()
{
Some(arithmetic_operator_class)
}
else
{
Some(top_level_arithmetic_operator_class)
}
},
}
}
Ok(top_level_arithmetic_operator_class)
}
pub fn parse(&self, level: usize) -> Result<crate::Term<P::Flavor>, crate::parse::Error>
{
let indentation = " ".repeat(level);
log::trace!("{}- parsing term: {}", indentation, self.input);
let input = trim_start(self.input);
match input.chars().next()
{
Some(')') => return Err(crate::parse::Error::new_unmatched_parenthesis(
crate::parse::error::Location::new(0, Some(0)))),
// TODO: implement absolute value function
Some('|') => unimplemented!(),
None => return Err(crate::parse::Error::new_empty_expression(
crate::parse::error::Location::new(0, Some(0)))),
_ => (),
}
// Parse arithmetic infix operations
if let Some(top_level_arithmetic_operator_class) =
self.top_level_arithmetic_operator_class()?
{
log::trace!("{} parsing {:?} arithmetic term", indentation,
top_level_arithmetic_operator_class);
if top_level_arithmetic_operator_class == ArithmeticOperatorClass::Exponential
{
return self.exponentiate(
self.filter_by_arithmetic_operator_class(top_level_arithmetic_operator_class)
.split(), level + 1);
}
// Parse arguments of arithmetic infix operations
let mut argument_iterator =
self.filter_by_arithmetic_operator_class(top_level_arithmetic_operator_class);
let (first_argument, first_binary_operator) = argument_iterator.next().ok_or_else(||
crate::parse::Error::new_expected_term(
crate::parse::error::Location::new(0, Some(0))))??;
let first_argument =
TermStr::new(first_argument, self.parser, self.variable_declaration_stack)
.parse(level + 1)?;
// TODO: improve error handling if the terms between the operators are invalid
let (accumulator, last_binary_operator) =
argument_iterator.try_fold((first_argument, first_binary_operator),
|(accumulator, binary_operator), argument|
{
let (argument, next_binary_operator) = argument?;
let argument = TermStr::new(argument, self.parser,
self.variable_declaration_stack)
.parse(level + 1)?;
let binary_operation =
crate::BinaryOperation::new(binary_operator, Box::new(accumulator),
Box::new(argument));
let formula = crate::Term::BinaryOperation(binary_operation);
Ok((formula, next_binary_operator))
})?;
// The last item hasnt been consumed yet, so its safe to unwrap it
let last_argument = argument_iterator.remaining_input().unwrap();
let last_argument =
TermStr::new(last_argument, self.parser, self.variable_declaration_stack)
.parse(level + 1)?;
let last_binary_operation =
crate::BinaryOperation::new(last_binary_operator, Box::new(accumulator),
Box::new(last_argument));
return Ok(crate::Term::BinaryOperation(last_binary_operation));
}
if let Some((number, input)) = number(input)?
{
if !input.trim().is_empty()
{
return Err(crate::parse::Error::new_unexpected_token(
crate::parse::error::Location::new(0, Some(0))));
}
return Ok(crate::Term::integer(number as i32));
}
if let Some((identifier, input)) = identifier(input)
{
match identifier
{
"inf" =>
{
if !input.trim().is_empty()
{
return Err(crate::parse::Error::new_unexpected_token(
crate::parse::error::Location::new(0, Some(0))))
}
return Ok(crate::Term::infimum());
},
"sup" =>
{
if !input.trim().is_empty()
{
return Err(crate::parse::Error::new_unexpected_token(
crate::parse::error::Location::new(0, Some(0))))
}
return Ok(crate::Term::supremum());
},
"true" =>
{
if !input.trim().is_empty()
{
return Err(crate::parse::Error::new_unexpected_token(
crate::parse::error::Location::new(0, Some(0))))
}
return Ok(crate::Term::true_());
},
"false" =>
{
if !input.trim().is_empty()
{
return Err(crate::parse::Error::new_unexpected_token(
crate::parse::error::Location::new(0, Some(0))))
}
return Ok(crate::Term::false_());
},
_ if is_variable_name(identifier) =>
{
if !input.trim().is_empty()
{
return Err(crate::parse::Error::new_unexpected_token(
crate::parse::error::Location::new(0, Some(0))))
}
let declaration = P::find_or_create_variable_declaration(
self.variable_declaration_stack, identifier);
return Ok(crate::Term::variable(declaration));
},
_ if is_function_name(identifier) =>
{
let function_name = identifier;
log::trace!("{} parsing function {}", indentation, function_name);
let input = trim_start(input);
// Parse arguments if there are any
let (arguments, input) = match parenthesized_expression(input)?
{
Some((parenthesized_expression, input)) =>
{
let functor = |token: &_| *token == Token::Symbol(Symbol::Comma);
let arguments = Tokens::new_filter(parenthesized_expression, functor).split()
.map(|argument| TermStr::new(argument?, self.parser,
self.variable_declaration_stack)
.parse(level + 1))
.collect::<Result<_, _>>()?;
(arguments, input)
}
None => (vec![], input),
};
if !input.trim().is_empty()
{
return Err(crate::parse::Error::new_unexpected_token(
crate::parse::error::Location::new(0, Some(0))))
}
let declaration = self.parser.find_or_create_function_declaration(
function_name, arguments.len());
return Ok(crate::Term::function(declaration, arguments));
},
_ => (),
}
}
// TODO: parse negative value
// Parse parenthesized terms
if let Some((parenthesized_expression, input)) = parenthesized_expression(input)?
{
if !input.trim().is_empty()
{
return Err(crate::parse::Error::new_unexpected_token(
crate::parse::error::Location::new(0, Some(0))));
}
return TermStr::new(parenthesized_expression, self.parser,
self.variable_declaration_stack)
.parse(level + 1);
}
Err(crate::parse::Error::new_unexpected_token(
crate::parse::error::Location::new(0, Some(0))))
}
// TODO: refactor
fn exponentiate_inner<T>(&self, mut argument_iterator: T, level: usize)
-> Result<Option<crate::Term<P::Flavor>>, crate::parse::Error>
where
T: std::iter::Iterator<Item = Result<&'i str, crate::parse::Error>>
{
match argument_iterator.next()
{
Some(argument) =>
{
// TODO: improve error handling if antecedent cannot be parsed
let argument =
TermStr::new(argument?, self.parser, self.variable_declaration_stack)
.parse(level)?;
match self.exponentiate_inner(argument_iterator, level)?
{
Some(next_argument) => Ok(Some(crate::Term::exponentiate(Box::new(argument),
Box::new(next_argument)))),
None => Ok(Some(argument)),
}
},
None => Ok(None),
}
}
fn exponentiate<T>(&self, mut argument_iterator: T, level: usize)
-> Result<crate::Term<P::Flavor>, crate::parse::Error>
where
T: std::iter::Iterator<Item = Result<&'i str, crate::parse::Error>>
{
match argument_iterator.next()
{
Some(argument) =>
{
// TODO: improve error handling if antecedent cannot be parsed
let argument =
TermStr::new(argument?, self.parser, self.variable_declaration_stack)
.parse(level)?;
match self.exponentiate_inner(argument_iterator, level)?
{
Some(next_argument) =>
Ok(crate::Term::exponentiate(Box::new(argument), Box::new(next_argument))),
None => Err(crate::parse::Error::new_expected_term(
crate::parse::error::Location::new(0, Some(0)))),
}
},
None => Err(crate::parse::Error::new_expected_term(
crate::parse::error::Location::new(0, Some(0)))),
}
}
}
#[cfg(test)]
mod tests
{
use super::*;
#[test]
fn parse_variable_name()
{
assert_eq!(variable_name("X").unwrap(), ("X", ""));
assert_eq!(variable_name("_X").unwrap(), ("_X", ""));
assert_eq!(variable_name("__X").unwrap(), ("__X", ""));
assert_eq!(variable_name("Variable").unwrap(), ("Variable", ""));
assert_eq!(variable_name("_Variable").unwrap(), ("_Variable", ""));
assert_eq!(variable_name("__Variable").unwrap(), ("__Variable", ""));
assert_eq!(variable_name("X,").unwrap(), ("X", ","));
assert_eq!(variable_name("_X,").unwrap(), ("_X", ","));
assert_eq!(variable_name("__X,").unwrap(), ("__X", ","));
assert_eq!(variable_name("Variable,").unwrap(), ("Variable", ","));
assert_eq!(variable_name("_Variable,").unwrap(), ("_Variable", ","));
assert_eq!(variable_name("__Variable,").unwrap(), ("__Variable", ","));
}
#[test]
fn parse_variable_declaration()
{
let variable_declaration =
|x| super::variable_declaration::<crate::parse::DefaultParser>(x);
let v = variable_declaration("X").unwrap();
assert_eq!((v.0.name.as_str(), v.1), ("X", ""));
let v = variable_declaration("_X").unwrap();
assert_eq!((v.0.name.as_str(), v.1), ("_X", ""));
let v = variable_declaration("__X").unwrap();
assert_eq!((v.0.name.as_str(), v.1), ("__X", ""));
let v = variable_declaration("Variable").unwrap();
assert_eq!((v.0.name.as_str(), v.1), ("Variable", ""));
let v = variable_declaration("_Variable").unwrap();
assert_eq!((v.0.name.as_str(), v.1), ("_Variable", ""));
let v = variable_declaration("__Variable").unwrap();
assert_eq!((v.0.name.as_str(), v.1), ("__Variable", ""));
let v = variable_declaration("X,").unwrap();
assert_eq!((v.0.name.as_str(), v.1), ("X", ","));
let v = variable_declaration("_X,").unwrap();
assert_eq!((v.0.name.as_str(), v.1), ("_X", ","));
let v = variable_declaration("__X,").unwrap();
assert_eq!((v.0.name.as_str(), v.1), ("__X", ","));
let v = variable_declaration("Variable,").unwrap();
assert_eq!((v.0.name.as_str(), v.1), ("Variable", ","));
let v = variable_declaration("_Variable,").unwrap();
assert_eq!((v.0.name.as_str(), v.1), ("_Variable", ","));
let v = variable_declaration("__Variable,").unwrap();
assert_eq!((v.0.name.as_str(), v.1), ("__Variable", ","));
}
#[test]
fn parse_variable_declarations()
{
let variable_declarations =
|x| super::variable_declarations::<crate::parse::DefaultParser>(x);
let v = variable_declarations("X.").unwrap().unwrap();
assert_eq!(v.0.len(), 1);
assert_eq!(v.0[0].name.as_str(), "X");
assert_eq!(v.1, ".");
let v = variable_declarations("X,Y,Z.").unwrap().unwrap();
assert_eq!(v.0.len(), 3);
assert_eq!(v.0[0].name.as_str(), "X");
assert_eq!(v.0[1].name.as_str(), "Y");
assert_eq!(v.0[2].name.as_str(), "Z");
assert_eq!(v.1, ".");
let v = variable_declarations("X, Y, Z.").unwrap().unwrap();
assert_eq!(v.0.len(), 3);
assert_eq!(v.0[0].name.as_str(), "X");
assert_eq!(v.0[1].name.as_str(), "Y");
assert_eq!(v.0[2].name.as_str(), "Z");
assert_eq!(v.1, ".");
let v = variable_declarations("X , Y , Z.").unwrap().unwrap();
assert_eq!(v.0.len(), 3);
assert_eq!(v.0[0].name.as_str(), "X");
assert_eq!(v.0[1].name.as_str(), "Y");
assert_eq!(v.0[2].name.as_str(), "Z");
assert_eq!(v.1, ".");
assert!(variable_declarations("test").unwrap().is_none());
assert!(variable_declarations("X, test").is_err());
assert!(variable_declarations("X ,test").is_err());
assert!(variable_declarations("X,Y,Z, test").is_err());
assert!(variable_declarations("X,Y,Z ,test").is_err());
}
}
-641
View File
@@ -1,641 +0,0 @@
fn substring_offset(substring: &str, string: &str) -> usize
{
substring.as_ptr() as usize - string.as_ptr() as usize
}
pub fn trim_start(mut input: &str) -> &str
{
loop
{
let original_input = input;
input = input.trim_start();
let mut input_characters = input.chars();
if let Some('#') = input_characters.next()
{
input = input_characters.as_str();
match (input.find('\n'), input.find('\r'))
{
(Some(newline_index), Some(carriage_return_index)) =>
{
let split_index = std::cmp::min(newline_index, carriage_return_index);
input = input.split_at(split_index).1;
},
(Some(split_index), _)
| (_, Some(split_index)) => input = input.split_at(split_index).1,
_ => input = &input[..input.len()],
}
}
if input.is_empty() || input == original_input
{
break;
}
}
input
}
#[derive(Clone, Copy, Eq, PartialEq)]
pub(crate) enum Keyword
{
And,
Exists,
False,
ForAll,
Infimum,
Not,
Or,
Supremum,
True,
}
impl std::fmt::Debug for Keyword
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match &self
{
Self::And => write!(formatter, "and"),
Self::Exists => write!(formatter, "exists"),
Self::False => write!(formatter, "false"),
Self::ForAll => write!(formatter, "forall"),
Self::Infimum => write!(formatter, "inf"),
Self::Not => write!(formatter, "not"),
Self::Or => write!(formatter, "or"),
Self::Supremum => write!(formatter, "sup"),
Self::True => write!(formatter, "true"),
}
}
}
#[derive(Clone, Copy, Eq, PartialEq)]
pub(crate) enum Symbol
{
ArrowLeft,
ArrowLeftAndRight,
ArrowRight,
Comma,
Division,
Equal,
Exponentiation,
Greater,
GreaterOrEqual,
Less,
LessOrEqual,
Minus,
Multiplication,
NotEqual,
Percent,
Plus,
VerticalBar,
}
impl std::fmt::Debug for Symbol
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match &self
{
Self::ArrowLeft => write!(formatter, "<-"),
Self::ArrowLeftAndRight => write!(formatter, "<->"),
Self::ArrowRight => write!(formatter, "->"),
Self::Comma => write!(formatter, ","),
Self::Division => write!(formatter, "/"),
Self::Equal => write!(formatter, "="),
Self::Exponentiation => write!(formatter, "**"),
Self::Greater => write!(formatter, ">"),
Self::GreaterOrEqual => write!(formatter, ">="),
Self::Less => write!(formatter, "<"),
Self::LessOrEqual => write!(formatter, "<="),
Self::Minus => write!(formatter, "-"),
Self::Multiplication => write!(formatter, "*"),
Self::NotEqual => write!(formatter, "!="),
Self::Percent => write!(formatter, "%"),
Self::Plus => write!(formatter, "+"),
Self::VerticalBar => write!(formatter, "|"),
}
}
}
#[derive(Clone, Copy, Eq, PartialEq)]
pub(crate) enum Token<'i>
{
Identifier(&'i str),
Number(usize),
ParenthesizedExpression(&'i str),
Symbol(Symbol),
}
fn is_identifier_start_character(character: char) -> bool
{
character.is_ascii_alphabetic()
}
fn is_identifier_body_character(character: char) -> bool
{
match character
{
'_' => true,
_ if character.is_ascii_alphanumeric() => true,
_ => false,
}
}
pub fn identifier(input: &str) -> Option<(&str, &str)>
{
let mut characters = input.char_indices();
let first_character = loop
{
match characters.next()
{
Some((_, '_')) => continue,
Some((_, character)) => break Some(character),
None => break None,
}
}?;
if !is_identifier_start_character(first_character)
{
return None;
}
loop
{
match characters.next()
{
None => return Some((input, characters.as_str())),
Some((character_index, character)) =>
{
if !is_identifier_body_character(character)
{
return Some(input.split_at(character_index));
}
},
}
}
}
pub(crate) fn is_keyword(identifier: &str) -> bool
{
match identifier
{
"and"
| "exists"
| "false"
| "forall"
| "inf"
| "not"
| "or"
| "sup"
| "true" => true,
_ => false,
}
}
fn number_string(input: &str) -> Option<(&str, &str)>
{
let mut characters = input.char_indices();
let (_, character) = match characters.next()
{
Some(characters_next) => characters_next,
None => return None,
};
if !character.is_ascii_digit()
{
return None;
}
loop
{
match characters.next()
{
None => return Some((input, characters.as_str())),
Some((character_index, character)) =>
{
if !character.is_ascii_digit()
{
return Some(input.split_at(character_index));
}
},
}
}
}
pub fn number(input: &str) -> Result<Option<(usize, &str)>, crate::parse::Error>
{
let (number_string, remaining_input) = match number_string(input)
{
Some(number_string) => number_string,
None => return Ok(None),
};
let number = number_string.parse()
.map_err(|error| crate::parse::Error::new_parse_number(input,
crate::parse::error::Location::new(0, Some(0)), error))?;
Ok(Some((number, remaining_input)))
}
pub(crate) fn symbol(input: &str) -> Option<(Symbol, &str)>
{
let mut characters = input.char_indices();
let (_, character) = match characters.next()
{
Some(characters_next) => characters_next,
None => return None,
};
let remaining_input = characters.as_str();
match character
{
',' => Some((Symbol::Comma, remaining_input)),
// <->, <-, <=, <
'=' => Some((Symbol::Equal, remaining_input)),
// !=
'!' => match characters.next()
{
Some((_, '=')) => Some((Symbol::NotEqual, characters.as_str())),
_ => None,
},
'<' => match characters.next()
{
Some((_, '-')) =>
{
let remaining_input = characters.as_str();
match characters.next()
{
Some((_, '>')) => Some((Symbol::ArrowLeftAndRight, characters.as_str())),
_ => Some((Symbol::ArrowLeft, remaining_input)),
}
},
Some((_, '=')) => Some((Symbol::LessOrEqual, characters.as_str())),
_ => Some((Symbol::Less, remaining_input)),
},
// >=, >
'>' => match characters.next()
{
Some((_, '=')) => Some((Symbol::GreaterOrEqual, characters.as_str())),
_ => Some((Symbol::Greater, remaining_input)),
},
'+' => Some((Symbol::Plus, remaining_input)),
// ->, -
'-' => match characters.next()
{
Some((_, '>')) => Some((Symbol::ArrowRight, characters.as_str())),
_ => Some((Symbol::Minus, remaining_input)),
},
// **, *
'*' => match characters.next()
{
Some((_, '*')) => Some((Symbol::Exponentiation, characters.as_str())),
_ => Some((Symbol::Multiplication, remaining_input)),
},
'/' => Some((Symbol::Division, remaining_input)),
'%' => Some((Symbol::Percent, remaining_input)),
'|' => Some((Symbol::VerticalBar, remaining_input)),
_ => None,
}
}
pub(crate) fn parenthesized_expression(input: &str)
-> Result<Option<(&str, &str)>, crate::parse::Error>
{
let mut characters = input.chars();
let (first_character, remaining_input) = match characters.next()
{
Some(first_character) => (first_character, characters.as_str()),
None => return Ok(None),
};
if first_character != '('
{
return Ok(None);
}
let mut characters = remaining_input.char_indices();
let mut number_of_open_parentheses = 1;
while let Some((character_index, character)) = characters.next()
{
match character
{
'(' => number_of_open_parentheses += 1,
')' => number_of_open_parentheses -= 1,
_ => (),
}
if number_of_open_parentheses == 0
{
let position_of_closing_parenthesis = character_index;
let (parenthesized_expression, _) =
remaining_input.split_at(position_of_closing_parenthesis);
let remaining_input = characters.as_str();
return Ok(Some((parenthesized_expression, remaining_input)));
}
}
Err(crate::parse::Error::new_unmatched_parenthesis(
crate::parse::error::Location::new(0, Some(1))))
}
pub(crate) struct Tokens<'i, F>
{
original_input: &'i str,
input: &'i str,
previous_index: usize,
reached_end_of_stream: bool,
functor: F,
}
impl<'i> Tokens<'i, ()>
{
pub fn new_iter(input: &'i str) -> Tokens<'i, impl FnMut(Token<'i>) -> Option<Token<'i>>>
{
Tokens::new_filter_map(input, |x| Some(x))
}
pub fn new_filter<P>(input: &'i str, mut predicate: P)
-> Tokens<'i, impl FnMut(Token<'i>) -> Option<Token<'i>>>
where
P: FnMut(&Token<'i>) -> bool,
{
Tokens::new_filter_map(input,
move |x|
{
if predicate(&x)
{
Some(x)
}
else
{
None
}
})
}
}
impl<'i, F> Tokens<'i, F>
{
pub fn new_filter_map(input: &'i str, functor: F) -> Self
{
Self
{
original_input: input,
input,
previous_index: 0,
reached_end_of_stream: false,
functor,
}
}
fn next_token(&mut self) -> Option<Result<(usize, usize, Token<'i>), crate::parse::Error>>
{
self.input = trim_start(self.input);
let index_left = substring_offset(self.input, self.original_input);
let first_character = match self.input.chars().next()
{
None => return None,
Some(first_character) => first_character,
};
if self.input.starts_with(")")
{
return Some(Err(crate::parse::Error::new_unmatched_parenthesis(
crate::parse::error::Location::new(0, Some(1)))));
}
match parenthesized_expression(self.input)
{
Ok(Some((parenthesized_expression, remaining_input))) =>
{
self.input = remaining_input;
let index_right = substring_offset(self.input, self.original_input);
return Some(Ok((index_left, index_right,
Token::ParenthesizedExpression(parenthesized_expression))));
},
Ok(None) => (),
Err(error) => return Some(Err(error)),
}
match number(self.input)
{
Ok(Some((number, remaining_input))) =>
{
self.input = remaining_input;
let index_right = substring_offset(self.input, self.original_input);
return Some(Ok((index_left, index_right, Token::Number(number))));
},
Ok(None) => (),
Err(error) => return Some(Err(error)),
}
if let Some((identifier, remaining_input)) = identifier(self.input)
{
self.input = remaining_input;
let index_right = substring_offset(self.input, self.original_input);
return Some(Ok((index_left, index_right, Token::Identifier(identifier))));
}
if let Some((symbol, remaining_input)) = symbol(self.input)
{
self.input = remaining_input;
let index_right = substring_offset(self.input, self.original_input);
return Some(Ok((index_left, index_right, Token::Symbol(symbol))));
}
return Some(Err(crate::parse::Error::new_character_not_allowed(first_character,
crate::parse::error::Location::new(0, Some(0)))));
}
pub fn remaining_input(&mut self) -> Option<&'i str>
{
if self.reached_end_of_stream
{
return None;
}
let remaining_input = self.original_input[self.previous_index..].trim();
self.reached_end_of_stream = true;
Some(remaining_input)
}
pub fn split(self) -> TokenSplit<Self>
{
TokenSplit::new(self)
}
}
impl<'i, F, G> std::iter::Iterator for Tokens<'i, F>
where
F: FnMut(Token<'i>) -> Option<G>,
{
type Item = Result<(&'i str, G), crate::parse::Error>;
fn next(&mut self) -> Option<Self::Item>
{
if self.previous_index == self.original_input.len()
{
return None;
}
loop
{
match self.next_token()
{
Some(Ok((index_left, index_right, token))) =>
{
let token = match (self.functor)(token)
{
None => continue,
Some(token) => token,
};
let input_left = self.original_input[self.previous_index..index_left].trim();
self.previous_index = index_right;
return Some(Ok((input_left, token)));
},
Some(Err(error)) => return Some(Err(error)),
None => return None,
}
}
}
}
pub(crate) struct TokenSplit<T>
{
tokens: T,
}
impl TokenSplit<()>
{
pub fn new<T>(tokens: T) -> TokenSplit<T>
{
TokenSplit
{
tokens,
}
}
}
impl<'i, F, G> std::iter::Iterator for TokenSplit<Tokens<'i, F>>
where
F: FnMut(Token<'i>) -> Option<G>,
{
type Item = Result<&'i str, crate::parse::Error>;
fn next(&mut self) -> Option<Self::Item>
{
match self.tokens.next()
{
Some(Ok((input_before, _))) => Some(Ok(input_before)),
Some(Err(error)) => Some(Err(error)),
None => match self.tokens.remaining_input()
{
Some(remaining_input) => Some(Ok(remaining_input)),
None => None,
},
}
}
}
#[cfg(test)]
mod tests
{
use super::*;
#[test]
fn tokenize_identifier()
{
assert_eq!(identifier("test").unwrap(), ("test", ""));
assert_eq!(identifier("test2").unwrap(), ("test2", ""));
assert_eq!(identifier("Test").unwrap(), ("Test", ""));
assert_eq!(identifier("Test2").unwrap(), ("Test2", ""));
assert_eq!(identifier("_test").unwrap(), ("_test", ""));
assert_eq!(identifier("_test2").unwrap(), ("_test2", ""));
assert_eq!(identifier("__test").unwrap(), ("__test", ""));
assert_eq!(identifier("__test2").unwrap(), ("__test2", ""));
assert_eq!(identifier("test, test").unwrap(), ("test", ", test"));
assert_eq!(identifier("test2, test").unwrap(), ("test2", ", test"));
assert_eq!(identifier("Test, Test").unwrap(), ("Test", ", Test"));
assert_eq!(identifier("Test2, Test").unwrap(), ("Test2", ", Test"));
assert_eq!(identifier("_test, _test").unwrap(), ("_test", ", _test"));
assert_eq!(identifier("_test2, _test").unwrap(), ("_test2", ", _test"));
assert_eq!(identifier("__test, __test").unwrap(), ("__test", ", __test"));
assert_eq!(identifier("__test2, __test").unwrap(), ("__test2", ", __test"));
assert!(identifier("2test, test").is_none());
assert!(identifier("#test, test").is_none());
assert!(identifier("$test, test").is_none());
assert!(identifier(",test, test").is_none());
}
#[test]
fn tokenize_primitives()
{
assert_eq!(parenthesized_expression("(foo bar baz) test").unwrap(),
Some(("foo bar baz", " test")));
assert!(parenthesized_expression("( | asd#0231(asd|asd) test").is_err());
assert_eq!(parenthesized_expression("( | asd#0231(asd|asd) ) test").unwrap(),
Some((" | asd#0231(asd|asd) ", " test")));
assert_eq!(parenthesized_expression("( | a)sd#0231(asd|asd) test").unwrap(),
Some((" | a", "sd#0231(asd|asd) test")));
assert_eq!(number("1234, ").unwrap(), Some((1234, ", ")));
assert_eq!(number("1234.5, ").unwrap(), Some((1234, ".5, ")));
assert_eq!(number("-1234, ").unwrap(), None);
assert_eq!(number("a1234, ").unwrap(), None);
assert_eq!(symbol("<-"), Some((Symbol::ArrowLeft, "")));
assert_eq!(symbol("<->"), Some((Symbol::ArrowLeftAndRight, "")));
assert_eq!(symbol("->"), Some((Symbol::ArrowRight, "")));
assert_eq!(symbol(","), Some((Symbol::Comma, "")));
assert_eq!(symbol("/"), Some((Symbol::Division, "")));
assert_eq!(symbol("="), Some((Symbol::Equal, "")));
assert_eq!(symbol("**"), Some((Symbol::Exponentiation, "")));
assert_eq!(symbol(">"), Some((Symbol::Greater, "")));
assert_eq!(symbol(">="), Some((Symbol::GreaterOrEqual, "")));
assert_eq!(symbol("<"), Some((Symbol::Less, "")));
assert_eq!(symbol("<="), Some((Symbol::LessOrEqual, "")));
assert_eq!(symbol("-"), Some((Symbol::Minus, "")));
assert_eq!(symbol("*"), Some((Symbol::Multiplication, "")));
assert_eq!(symbol("!="), Some((Symbol::NotEqual, "")));
assert_eq!(symbol("+"), Some((Symbol::Plus, "")));
assert_eq!(symbol("|"), Some((Symbol::VerticalBar, "")));
assert_eq!(symbol("<-a"), Some((Symbol::ArrowLeft, "a")));
assert_eq!(symbol("<->a"), Some((Symbol::ArrowLeftAndRight, "a")));
assert_eq!(symbol("->a"), Some((Symbol::ArrowRight, "a")));
assert_eq!(symbol(",a"), Some((Symbol::Comma, "a")));
assert_eq!(symbol("/a"), Some((Symbol::Division, "a")));
assert_eq!(symbol("=a"), Some((Symbol::Equal, "a")));
assert_eq!(symbol("**a"), Some((Symbol::Exponentiation, "a")));
assert_eq!(symbol(">a"), Some((Symbol::Greater, "a")));
assert_eq!(symbol(">=a"), Some((Symbol::GreaterOrEqual, "a")));
assert_eq!(symbol("<a"), Some((Symbol::Less, "a")));
assert_eq!(symbol("<=a"), Some((Symbol::LessOrEqual, "a")));
assert_eq!(symbol("-a"), Some((Symbol::Minus, "a")));
assert_eq!(symbol("*a"), Some((Symbol::Multiplication, "a")));
assert_eq!(symbol("!=a"), Some((Symbol::NotEqual, "a")));
assert_eq!(symbol("+a"), Some((Symbol::Plus, "a")));
assert_eq!(symbol("|a"), Some((Symbol::VerticalBar, "a")));
}
}
-102
View File
@@ -1,102 +0,0 @@
use crate::flavor::VariableDeclaration as _;
pub struct BoundVariableDeclarations<'p, F>
where
F: crate::flavor::Flavor,
{
pub parent: &'p VariableDeclarationStackLayer<'p, F>,
pub variable_declarations: std::rc::Rc<crate::VariableDeclarations<F>>,
}
impl<'p, F> BoundVariableDeclarations<'p, F>
where
F: crate::flavor::Flavor,
{
pub fn new(parent: &'p VariableDeclarationStackLayer<'p, F>,
variable_declarations: std::rc::Rc<crate::VariableDeclarations<F>>) -> Self
{
Self
{
parent,
variable_declarations,
}
}
}
pub enum VariableDeclarationStackLayer<'p, F>
where
F: crate::flavor::Flavor,
{
Free(std::cell::RefCell<crate::VariableDeclarations<F>>),
Bound(BoundVariableDeclarations<'p, F>),
}
impl<'p, F> VariableDeclarationStackLayer<'p, F>
where
F: crate::flavor::Flavor,
{
pub fn free() -> Self
{
Self::Free(std::cell::RefCell::new(vec![]))
}
pub fn bound(parent: &'p VariableDeclarationStackLayer<'p, F>,
variable_declarations: std::rc::Rc<crate::VariableDeclarations<F>>) -> Self
{
Self::Bound(BoundVariableDeclarations::new(parent, variable_declarations))
}
pub fn find(&self, variable_name: &str) -> Option<std::rc::Rc<F::VariableDeclaration>>
{
match self
{
VariableDeclarationStackLayer::Free(free_variable_declarations) =>
{
if let Some(variable_declaration) = free_variable_declarations.borrow().iter()
.find(|x| x.matches_name(variable_name))
{
return Some(std::rc::Rc::clone(&variable_declaration));
}
None
},
VariableDeclarationStackLayer::Bound(bound_variable_declarations) =>
{
if let Some(variable_declaration) = bound_variable_declarations
.variable_declarations.iter()
.find(|x| x.matches_name(variable_name))
{
return Some(std::rc::Rc::clone(&variable_declaration));
}
bound_variable_declarations.parent.find(variable_name)
},
}
}
pub fn free_variable_declarations_do_mut<F1, F2>(&self, f: F1) -> F2
where
F1: Fn(&mut crate::VariableDeclarations<F>) -> F2,
{
match self
{
VariableDeclarationStackLayer::Free(free_variable_declarations)
=> f(&mut free_variable_declarations.borrow_mut()),
VariableDeclarationStackLayer::Bound(bound_variable_declarations)
=> bound_variable_declarations.parent.free_variable_declarations_do_mut(f),
}
}
pub fn free_variable_declarations_do<F1, F2>(&self, f: F1) -> F2
where
F1: Fn(&crate::VariableDeclarations<F>) -> F2,
{
match self
{
VariableDeclarationStackLayer::Free(free_variable_declarations)
=> f(&free_variable_declarations.borrow()),
VariableDeclarationStackLayer::Bound(bound_variable_declarations)
=> bound_variable_declarations.parent.free_variable_declarations_do(f),
}
}
}