Compare commits

...

64 Commits

Author SHA1 Message Date
Patrick Lühne 79d6643598
Remove unneeded trait methods 2020-07-07 09:56:14 +02:00
Patrick Lühne c6f2cdc6e1
Improve public interface 2020-07-07 08:38:28 +02:00
Patrick Lühne 66b5499005
Experimental refactoring 2020-07-07 08:15:52 +02:00
Patrick Lühne 742379934f
Remove unused trait implementations 2020-05-21 23:26:57 +02:00
Patrick Lühne a0fefe9b6a
Improve interface for declaration types 2020-05-21 23:19:18 +02:00
Patrick Lühne 036544d3c7
Minor refactoring 2020-05-19 19:06:16 +02:00
Patrick Lühne c7d79e7b07
Make inner types customizable 2020-05-19 15:39:20 +02:00
Patrick Lühne 170cde6a82
Fix parsing right-to-left implication 2020-05-18 06:00:41 +02:00
Patrick Lühne 0216f90929
Add support for comments 2020-05-12 05:55:23 +02:00
Patrick Lühne ae46634d67
Rename ClosedFormula to OpenFormula 2020-05-11 03:52:36 +02:00
Patrick Lühne 75e97a5c07
Use log crate rather than println 2020-05-05 19:43:41 +02:00
Patrick Lühne dd208ffeeb
Expose number parser 2020-05-04 20:29:07 +02:00
Patrick Lühne bdd5d0e583
Expose identifier parser 2020-05-04 18:07:39 +02:00
Patrick Lühne 82e98e5ec0
Look up functions 2020-05-04 16:56:03 +02:00
Patrick Lühne 1b4c400bfb
Look up variables 2020-05-04 16:55:21 +02:00
Patrick Lühne f8918628fa
Pass declarations to term parser 2020-05-04 16:53:42 +02:00
Patrick Lühne 555f983285
Look up predicates 2020-05-04 16:48:35 +02:00
Patrick Lühne 56885dc290
Pass declarations to formula parser 2020-05-04 16:40:59 +02:00
Patrick Lühne 30c28c2bc4
Fix unit tests 2020-05-03 18:05:45 +02:00
Patrick Lühne 8d474fa489
Finish dirty first pass over parser 2020-04-28 05:21:58 +02:00
Patrick Lühne 66ac57c5b8
Work in progress 2020-04-28 03:18:05 +02:00
Patrick Lühne 0fb2be4897
Minor refactoring 2020-04-28 02:39:58 +02:00
Patrick Lühne 80aafb2359
Implement right-to-left implication 2020-04-28 02:36:53 +02:00
Patrick Lühne a2268ab85b
Minor renaming 2020-04-28 02:36:47 +02:00
Patrick Lühne 451b887019
Minor renaming 2020-04-28 02:36:38 +02:00
Patrick Lühne a12acae633
Refactoring 2020-04-28 02:36:02 +02:00
Patrick Lühne 35937d7930
Clean-up 2020-04-28 02:35:46 +02:00
Patrick Lühne 31805fa9d8
Clean-up 2020-04-28 02:16:15 +02:00
Patrick Lühne a6edd2e9cc
Clean-up 2020-04-28 02:14:27 +02:00
Patrick Lühne 834194d40a
Work in progress 2020-04-28 02:02:20 +02:00
Patrick Lühne 15d0d2b76c
Work in progress 2020-04-27 19:36:12 +02:00
Patrick Lühne ff17c60cd1
Start rewriting parser 2020-04-22 20:01:29 +02:00
Patrick Lühne b516396977
Fix parsing nested quantified formulas 2020-04-20 02:57:32 +02:00
Patrick Lühne 987e02f478
Allow period character as word boundary 2020-04-20 02:51:46 +02:00
Patrick Lühne ba385868cb
Fix parsing precedence of left implication vs. less-than comparison 2020-04-20 02:40:13 +02:00
Patrick Lühne 04e2d61583
Fix order of operators 2020-04-19 23:05:12 +02:00
Patrick Lühne 395c029ca9
Expose function/predicate name parser 2020-04-18 02:32:12 +02:00
Patrick Lühne c927fe4628
Expose Declarations type 2020-04-18 01:07:12 +02:00
Patrick Lühne 2b3add562f
Update nom to 6.0.0-alpha1 2020-04-17 18:22:50 +02:00
Patrick Lühne 0d5971cad7
Retrieve declarations using traits and not objects 2020-04-17 04:06:22 +02:00
Patrick Lühne 0e78e4ea57
Minor refactoring 2020-04-17 03:30:32 +02:00
Patrick Lühne 63c1931e30
Expose functions to access free and manipulate variable declarations 2020-04-17 03:18:25 +02:00
Patrick Lühne 8a9a7b9132
Remove unneeded indirection 2020-04-17 03:13:18 +02:00
Patrick Lühne abbc047dda
Replace variable declaration stack with recursive layer implementation 2020-04-17 02:53:23 +02:00
Patrick Lühne 62b9e2da04
Make variable declaration stack safer with guards 2020-04-17 01:40:19 +02:00
Patrick Lühne fa6f27beb4
Start reimplementing parser
Implement name parsing

Start parsing terms

Implement word boundaries

Implement strings

Add pipe character to allowed word boundaries

Implement booleans

Require word boundaries around names

Implement variable parsing

Finish implementing term parsing

Add term parsing test

Test associativity of multiplication

Make parse feature the default

Fix term parsing and finish tests

Start parsing formulas

Continue parsing formulas

Finish implementing formula parsing

Move boolean parser to separate module

Move integer parser to separate module

Move special integer parser to separate module

Move string parser to separate module

Address warnings

Fix negation parser

Refactor term parser tests

Address clippy warning

Disallow reserved keywords as names

Add missing word boundary character

Check that names don’t start with special characters

Minor refactoring

Add note

Test conjunction parser

Test disjunction parser

Parentheses for stronger checks

Add note

Fix implication parser and output

Split formatting functionality into two files

Test term formatting

Add unit test for function declaration formatting

Work in progress

Fix implication formatting

Refactor precedence rules

Start testing formula formatter

Minor formatting

Test remaining formula types

Add unit tests for precedence-0 formulas and lower

Before larger refactoring

Refactor precedence rules for formulas

Remove ChildPosition enum

Fix

Address warnings

Remove unneeded precedence implementation

Test negation

Test quantified formulas

Clean up tests

Clean up tests

Test conjunction

Test disjunction

Start testing implications

Refactor parenthesis requirement check

Fix precedence of implication

Continue testing implication

Test biconditionals

Experimental method for testing all permutations

Rewrite tests for clarity

Rewrite tests for clarity

Add type annotations

Rewrite tests for clarity

Reorganize tests

Finish testing biconditionals

Support empty n-aries

Support quantified expressions with 0 parameters

Rewrite term formatting tests for clarity

Reorganize term formatter tests

Refactor parenthesis rules for terms

Remove unneeded parentheses enum

Refactoring

Refactoring

Minor clean-up

Minor clean-up

Simplify representation of quantified formulas

Remove redundant indirection

Remove redundant indirection
2020-04-17 01:40:16 +02:00
Patrick Lühne 1e34d726e1
Export formatting implementation functionality 2020-04-14 01:15:02 +02:00
Patrick Lühne 1e610a77fe
Make variable formatting customizable
This introduces a Format trait, which can be implemented to customize
the appearance of variable declarations right now. The Format trait will
be extended with further customization options in the future.
2020-04-14 01:15:02 +02:00
Patrick Lühne 9216bbbe31
Rename formatter variables
These formatter objects were just named “format,” but there’s no need
to abbreviate that. This renames all occurrences to “formatter” for
clarity.
2020-04-13 23:07:54 +02:00
Patrick Lühne d67e530fec
Rewrite formula and term formatting
The rules for determining required parentheses as opposed to parentheses
that can be omitted are more complicated than just showing parentheses
whenever a child expression has lower precedence than its parent. This
necessitated a rewrite.

This new implementation determines whether an expression requires to be
parenthesized with individual rules for each type of expression, which
may or may not depend on the type of the parent expression and the
position of a child within its parent expression. For example,
implication is defined to be right-associative, which means that the
parentheses in the formula

    (F -> G) -> H

cannot be ommitted. When determining whether the subformula (F -> G)
needs to be parenthesized, the new algorithm notices that the subformula
is contained as the antecedent of another implication and concludes that
parentheses are required.

Furthermore, this adds extensive unit tests for both formula and term
formatting. The general idea is to test all types of expressions
individually and, in addition to that, all combinations of parent and
child expression types.

Unit testing made it clear that the formatting of empty and 1-ary
conjunctions, disjunctions, and biconditionals needs to be well-defined
even though these types of formulas may be unconventional. The same
applies to existentially and universally quantified formulas where the
list of parameters is empty. Now, empty conjunctions and biconditionals
are rendered like true Booleans, empty disjunctions like false Booleans,
and 1-ary conjunctions, disjunctions, biconditionals, as well as
quantified expressions with empty parameter lists as their singleton
argument.

The latter formulas can be considered neutral intermediates. That is,
they should not affect whether their singleton arguments are
parenthesized or not. To account for that, all unit tests covering
combinations of formulas are tested with any of those five neutral
intermediates additionally.
2020-04-13 23:07:54 +02:00
Patrick Lühne 8e32b58c99
Remove unneeded indirection from vector types
The type aliases for vectors of formulas and terms were defined as
vectors of boxed formulas and terms, respectively. This is an
unnecessary indirection, so store the formulas and terms directly.
2020-04-13 22:16:01 +02:00
Patrick Lühne 2fa592576b
Take reference-counted arguments by value
These reference-counted arguments were taken by reference, which made it
necessary to clone them. If a reference-counted object is created for the
sole purpose of being passed to one of these methods, it would be cloned
unnecessarily. This changes the signatures to take these arguments by
value, shifting the responsibility of cloning the reference-counted
objects to the users of these methods.
2020-04-13 22:09:43 +02:00
Patrick Lühne 7d22e47ba1
Represent quantified formulas consistently
Existential and universal quantification used redundant data
representations, while they actually share the same structure. This
unifies both into a single QuantifiedFormula type.
2020-04-13 22:05:09 +02:00
Patrick Lühne 7566fdaa29
Support n-ary biconditionals
For convenience, support biconditionals with more than one argument.
An n-ary “if and only if” statement

    F_1 <-> F_2 <-> ... <-> F_n

is to be interpreted as

    F_1 <-> F_2 and F2 <-> F3 and ... and F_(n - 1) <-> F_n
2020-04-13 21:59:25 +02:00
Patrick Lühne 855fd9abcf
Support right-to-left implications
As right-to-left implications are common in answer set programming, this
adds support for using implications in both directions.
2020-04-13 21:44:02 +02:00
Patrick Lühne 5bbb09eef8
Split formatting utils into separate files
For clarity, this moves the formatting functionality related to formulas
and terms into two separate files.
2020-04-09 22:09:15 +02:00
Patrick Lühne fd6ba4a005
Test crate with GitHub Actions
This adds a GitHub Actions workflow to test this crate with the Rust
stable, beta, and nightly toolchains.
2020-04-09 15:34:49 +02:00
Patrick Lühne 153f77621e
Fix precedence of absolute value operation
As the absolute value operation has its own type of parentheses, it
never needs to take precedence over other terms in order to be displayed
correctly. To avoid extraneous parentheses around absolute value
operations, set its precedence level to 0.
2020-03-30 06:42:54 +02:00
Patrick Lühne 551c35ed75
Fix formatting of binary operations
The precedence rules of binary operations are a bit trickier than
expected. The fact that a parent and a child term have the same
precedence level doesn’t automatically mean that parentheses can be
omitted. This is the case, for example, with

    a - (b + c)

While addition and subtraction have the same precedence level, the
parenthesis cannot be omitted. In general, this happens on the right-
hand side of the subtraction, division, and modulo operators if the
right-hand side has the same precedence level.

This patch fixes the output of binary operations accordingly.
2020-03-30 06:37:21 +02:00
Patrick Lühne 549f127729
Derive simple enums from basic traits
This adds derive statements from Copy, Clone, PartialEq, and Eq to the
operator enums as well as SpecialInteger.
2020-03-30 06:37:21 +02:00
Patrick Lühne a304ec9a75
Fix output of Booleans in formulas
Booleans are supposed to be formatted without a leading hash sign in
both terms and formulas. By mistake, the formula formatter added leading
hash signs though.
2020-03-30 06:37:21 +02:00
Patrick Lühne a82b4080c8
Fix function formatting
By mistake, a function’s name was printed two consecutive times if the
function had more than one argument.
2020-03-30 06:37:21 +02:00
Patrick Lühne 90f7be2f33
Minor refactoring for clarity 2020-03-30 06:37:21 +02:00
Patrick Lühne a127a053b2
Support formatting special integers separately
This adds Debug and Display trait implementations for the SpecialInteger
enum to make it possible to format its values without having to wrap it
in a Term variant.
2020-03-30 06:37:21 +02:00
14 changed files with 4970 additions and 579 deletions

32
.github/workflows/main.yml vendored Normal file
View File

@ -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

View File

@ -11,3 +11,6 @@ keywords = ["logic"]
categories = ["data-structures", "science"] categories = ["data-structures", "science"]
license = "MIT" license = "MIT"
edition = "2018" edition = "2018"
[dependencies]
log = "0.4"

View File

@ -1,5 +1,8 @@
use crate::flavor::{FunctionDeclaration as _, PredicateDeclaration as _};
// Operators // Operators
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum BinaryOperator pub enum BinaryOperator
{ {
Add, Add,
@ -10,6 +13,7 @@ pub enum BinaryOperator
Exponentiate, Exponentiate,
} }
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum ComparisonOperator pub enum ComparisonOperator
{ {
Greater, Greater,
@ -20,12 +24,22 @@ pub enum ComparisonOperator
Equal, Equal,
} }
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum UnaryOperator pub enum UnaryOperator
{ {
AbsoluteValue, AbsoluteValue,
Negative, Negative,
} }
// ImplicationDirection
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum ImplicationDirection
{
LeftToRight,
RightToLeft,
}
// Primitives // Primitives
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)] #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
@ -47,7 +61,8 @@ impl FunctionDeclaration
} }
} }
pub type FunctionDeclarations = std::collections::BTreeSet<std::rc::Rc<FunctionDeclaration>>; 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, Ord, PartialEq, PartialOrd)]
pub struct PredicateDeclaration pub struct PredicateDeclaration
@ -68,7 +83,8 @@ impl PredicateDeclaration
} }
} }
pub type PredicateDeclarations = std::collections::BTreeSet<std::rc::Rc<PredicateDeclaration>>; pub type PredicateDeclarations<F> =
std::collections::BTreeSet<std::rc::Rc<<F as crate::flavor::Flavor>::PredicateDeclaration>>;
pub struct VariableDeclaration pub struct VariableDeclaration
{ {
@ -78,10 +94,10 @@ pub struct VariableDeclaration
impl std::cmp::PartialEq for VariableDeclaration impl std::cmp::PartialEq for VariableDeclaration
{ {
#[inline(always)] #[inline(always)]
fn eq(&self, other: &VariableDeclaration) -> bool fn eq(&self, other: &Self) -> bool
{ {
let l = self as *const VariableDeclaration; let l = self as *const Self;
let r = other as *const VariableDeclaration; let r = other as *const Self;
l.eq(&r) l.eq(&r)
} }
@ -115,6 +131,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 impl VariableDeclaration
{ {
pub fn new(name: String) -> Self pub fn new(name: String) -> Self
@ -126,20 +153,26 @@ impl VariableDeclaration
} }
} }
pub type VariableDeclarations = Vec<std::rc::Rc<VariableDeclaration>>; pub type VariableDeclarations<F> =
Vec<std::rc::Rc<<F as crate::flavor::Flavor>::VariableDeclaration>>;
// Terms // Terms
pub struct BinaryOperation #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct BinaryOperation<F>
where
F: crate::flavor::Flavor,
{ {
pub operator: BinaryOperator, pub operator: BinaryOperator,
pub left: Box<Term>, pub left: Box<Term<F>>,
pub right: Box<Term>, pub right: Box<Term<F>>,
} }
impl BinaryOperation impl<F> BinaryOperation<F>
where
F: crate::flavor::Flavor,
{ {
pub fn new(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self pub fn new(operator: BinaryOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self Self
{ {
@ -150,42 +183,53 @@ impl BinaryOperation
} }
} }
pub struct Function #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Function<F>
where
F: crate::flavor::Flavor,
{ {
pub declaration: std::rc::Rc<FunctionDeclaration>, pub declaration: std::rc::Rc<F::FunctionDeclaration>,
pub arguments: Vec<Box<Term>>, pub arguments: Terms<F>,
} }
impl Function impl<F> Function<F>
where
F: crate::flavor::Flavor,
{ {
pub fn new(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self pub fn new(declaration: std::rc::Rc<F::FunctionDeclaration>, arguments: Terms<F>) -> Self
{ {
assert_eq!(declaration.arity, arguments.len(), assert_eq!(declaration.arity(), arguments.len(),
"function has a different number of arguments then declared"); "function has a different number of arguments than declared");
Self Self
{ {
declaration: std::rc::Rc::clone(declaration), declaration,
arguments, arguments,
} }
} }
} }
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum SpecialInteger pub enum SpecialInteger
{ {
Infimum, Infimum,
Supremum, Supremum,
} }
pub struct UnaryOperation #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct UnaryOperation<F>
where
F: crate::flavor::Flavor,
{ {
pub operator: UnaryOperator, pub operator: UnaryOperator,
pub argument: Box<Term>, pub argument: Box<Term<F>>,
} }
impl UnaryOperation impl<F> UnaryOperation<F>
where
F: crate::flavor::Flavor,
{ {
pub fn new(operator: UnaryOperator, argument: Box<Term>) -> Self pub fn new(operator: UnaryOperator, argument: Box<Term<F>>) -> Self
{ {
Self Self
{ {
@ -195,34 +239,44 @@ impl UnaryOperation
} }
} }
pub struct Variable #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Variable<F>
where
F: crate::flavor::Flavor,
{ {
pub declaration: std::rc::Rc<VariableDeclaration>, pub declaration: std::rc::Rc<F::VariableDeclaration>,
} }
impl Variable impl<F> Variable<F>
where
F: crate::flavor::Flavor,
{ {
pub fn new(declaration: &std::rc::Rc<VariableDeclaration>) -> Self pub fn new(declaration: std::rc::Rc<F::VariableDeclaration>) -> Self
{ {
Self Self
{ {
declaration: std::rc::Rc::clone(declaration), declaration,
} }
} }
} }
// Formulas // Formulas
pub struct Compare #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Compare<F>
where
F: crate::flavor::Flavor,
{ {
pub operator: ComparisonOperator, pub operator: ComparisonOperator,
pub left: Box<Term>, pub left: Box<Term<F>>,
pub right: Box<Term>, pub right: Box<Term<F>>,
} }
impl Compare impl<F> Compare<F>
where
F: crate::flavor::Flavor,
{ {
pub fn new(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self pub fn new(operator: ComparisonOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self Self
{ {
@ -233,15 +287,20 @@ impl Compare
} }
} }
pub struct Exists #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct QuantifiedFormula<F>
where
F: crate::flavor::Flavor,
{ {
pub parameters: std::rc::Rc<VariableDeclarations>, pub parameters: std::rc::Rc<VariableDeclarations<F>>,
pub argument: Box<Formula>, pub argument: Box<Formula<F>>,
} }
impl Exists impl<F> QuantifiedFormula<F>
where
F: crate::flavor::Flavor,
{ {
pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self pub fn new(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
{ {
Self Self
{ {
@ -251,76 +310,54 @@ impl Exists
} }
} }
pub struct ForAll #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Implies<F>
where
F: crate::flavor::Flavor,
{ {
pub parameters: std::rc::Rc<VariableDeclarations>, pub direction: ImplicationDirection,
pub argument: Box<Formula>, pub antecedent: Box<Formula<F>>,
pub implication: Box<Formula<F>>,
} }
impl ForAll impl<F> Implies<F>
where
F: crate::flavor::Flavor,
{ {
pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self pub fn new(direction: ImplicationDirection, antecedent: Box<Formula<F>>,
{ implication: Box<Formula<F>>)
Self -> Self
{
parameters,
argument,
}
}
}
pub struct IfAndOnlyIf
{
pub left: Box<Formula>,
pub right: Box<Formula>,
}
impl IfAndOnlyIf
{
pub fn new(left: Box<Formula>, right: Box<Formula>) -> Self
{
Self
{
left,
right,
}
}
}
pub struct Implies
{
pub antecedent: Box<Formula>,
pub implication: Box<Formula>,
}
impl Implies
{
pub fn new(antecedent: Box<Formula>, implication: Box<Formula>) -> Self
{ {
Self Self
{ {
direction,
antecedent, antecedent,
implication, implication,
} }
} }
} }
pub struct Predicate #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Predicate<F>
where
F: crate::flavor::Flavor,
{ {
pub declaration: std::rc::Rc<PredicateDeclaration>, pub declaration: std::rc::Rc<F::PredicateDeclaration>,
pub arguments: Vec<Box<Term>>, pub arguments: Terms<F>,
} }
impl Predicate impl<F> Predicate<F>
where
F: crate::flavor::Flavor,
{ {
pub fn new(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self pub fn new(declaration: std::rc::Rc<F::PredicateDeclaration>, arguments: Terms<F>) -> Self
{ {
assert_eq!(declaration.arity, arguments.len(), assert_eq!(declaration.arity(), arguments.len(),
"predicate has a different number of arguments then declared"); "predicate has a different number of arguments than declared");
Self Self
{ {
declaration: std::rc::Rc::clone(declaration), declaration,
arguments, arguments,
} }
} }
@ -328,33 +365,38 @@ impl Predicate
// Variants // Variants
pub enum Term #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum Term<F>
where
F: crate::flavor::Flavor,
{ {
BinaryOperation(BinaryOperation), BinaryOperation(BinaryOperation<F>),
Boolean(bool), Boolean(bool),
Function(Function), Function(Function<F>),
Integer(i32), Integer(i32),
SpecialInteger(SpecialInteger), SpecialInteger(SpecialInteger),
String(String), String(String),
UnaryOperation(UnaryOperation), UnaryOperation(UnaryOperation<F>),
Variable(Variable), Variable(Variable<F>),
} }
pub type Terms = Vec<Box<Term>>; pub type Terms<F> = Vec<Term<F>>;
impl Term impl<F> Term<F>
where
F: crate::flavor::Flavor,
{ {
pub fn absolute_value(argument: Box<Term>) -> Self pub fn absolute_value(argument: Box<Term<F>>) -> Self
{ {
Self::unary_operation(UnaryOperator::AbsoluteValue, argument) Self::unary_operation(UnaryOperator::AbsoluteValue, argument)
} }
pub fn add(left: Box<Term>, right: Box<Term>) -> Self pub fn add(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self::binary_operation(BinaryOperator::Add, left, right) Self::binary_operation(BinaryOperator::Add, left, right)
} }
pub fn binary_operation(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self pub fn binary_operation(operator: BinaryOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self::BinaryOperation(BinaryOperation::new(operator, left, right)) Self::BinaryOperation(BinaryOperation::new(operator, left, right))
} }
@ -364,12 +406,12 @@ impl Term
Self::Boolean(value) Self::Boolean(value)
} }
pub fn divide(left: Box<Term>, right: Box<Term>) -> Self pub fn divide(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self::binary_operation(BinaryOperator::Divide, left, right) Self::binary_operation(BinaryOperator::Divide, left, right)
} }
pub fn exponentiate(left: Box<Term>, right: Box<Term>) -> Self pub fn exponentiate(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self::binary_operation(BinaryOperator::Exponentiate, left, right) Self::binary_operation(BinaryOperator::Exponentiate, left, right)
} }
@ -379,8 +421,7 @@ impl Term
Self::boolean(false) Self::boolean(false)
} }
pub fn function(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) pub fn function(declaration: std::rc::Rc<F::FunctionDeclaration>, arguments: Terms<F>) -> Self
-> Self
{ {
Self::Function(Function::new(declaration, arguments)) Self::Function(Function::new(declaration, arguments))
} }
@ -395,17 +436,17 @@ impl Term
Self::Integer(value) Self::Integer(value)
} }
pub fn modulo(left: Box<Term>, right: Box<Term>) -> Self pub fn modulo(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self::binary_operation(BinaryOperator::Modulo, left, right) Self::binary_operation(BinaryOperator::Modulo, left, right)
} }
pub fn multiply(left: Box<Term>, right: Box<Term>) -> Self pub fn multiply(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self::binary_operation(BinaryOperator::Multiply, left, right) Self::binary_operation(BinaryOperator::Multiply, left, right)
} }
pub fn negative(argument: Box<Term>) -> Self pub fn negative(argument: Box<Term<F>>) -> Self
{ {
Self::unary_operation(UnaryOperator::Negative, argument) Self::unary_operation(UnaryOperator::Negative, argument)
} }
@ -420,7 +461,7 @@ impl Term
Self::String(value) Self::String(value)
} }
pub fn subtract(left: Box<Term>, right: Box<Term>) -> Self pub fn subtract(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self::binary_operation(BinaryOperator::Subtract, left, right) Self::binary_operation(BinaryOperator::Subtract, left, right)
} }
@ -435,39 +476,42 @@ impl Term
Self::boolean(true) Self::boolean(true)
} }
pub fn unary_operation(operator: UnaryOperator, argument: Box<Term>) -> Self pub fn unary_operation(operator: UnaryOperator, argument: Box<Term<F>>) -> Self
{ {
Self::UnaryOperation(UnaryOperation::new(operator, argument)) Self::UnaryOperation(UnaryOperation::new(operator, argument))
} }
pub fn variable(declaration: &std::rc::Rc<VariableDeclaration>) -> Self pub fn variable(declaration: std::rc::Rc<F::VariableDeclaration>) -> Self
{ {
Self::Variable(Variable::new(declaration)) Self::Variable(Variable::new(declaration))
} }
} }
pub enum Formula #[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum Formula<F>
where
F: crate::flavor::Flavor,
{ {
And(Formulas), And(Formulas<F>),
Boolean(bool), Boolean(bool),
Compare(Compare), Compare(Compare<F>),
Exists(Exists), Exists(QuantifiedFormula<F>),
ForAll(ForAll), ForAll(QuantifiedFormula<F>),
IfAndOnlyIf(IfAndOnlyIf), IfAndOnlyIf(Formulas<F>),
Implies(Implies), Implies(Implies<F>),
Not(Box<Formula>), Not(Box<Formula<F>>),
Or(Formulas), Or(Formulas<F>),
Predicate(Predicate), Predicate(Predicate<F>),
} }
pub type Formulas = Vec<Box<Formula>>; pub type Formulas<F> = Vec<Formula<F>>;
impl Formula impl<F> Formula<F>
where
F: crate::flavor::Flavor,
{ {
pub fn and(arguments: Formulas) -> Self pub fn and(arguments: Formulas<F>) -> Self
{ {
assert!(!arguments.is_empty());
Self::And(arguments) Self::And(arguments)
} }
@ -476,19 +520,17 @@ impl Formula
Self::Boolean(value) Self::Boolean(value)
} }
pub fn compare(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self pub fn compare(operator: ComparisonOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self::Compare(Compare::new(operator, left, right)) Self::Compare(Compare::new(operator, left, right))
} }
pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self pub fn exists(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
{ {
assert!(!parameters.is_empty()); Self::Exists(QuantifiedFormula::new(parameters, argument))
Self::Exists(Exists::new(parameters, argument))
} }
pub fn equal(left: Box<Term>, right: Box<Term>) -> Self pub fn equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self::compare(ComparisonOperator::Equal, left, right) Self::compare(ComparisonOperator::Equal, left, right)
} }
@ -498,62 +540,58 @@ impl Formula
Self::boolean(false) Self::boolean(false)
} }
pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self pub fn for_all(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
{ {
assert!(!parameters.is_empty()); Self::ForAll(QuantifiedFormula::new(parameters, argument))
Self::ForAll(ForAll::new(parameters, argument))
} }
pub fn greater(left: Box<Term>, right: Box<Term>) -> Self pub fn greater(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self::compare(ComparisonOperator::Greater, left, right) Self::compare(ComparisonOperator::Greater, left, right)
} }
pub fn greater_or_equal(left: Box<Term>, right: Box<Term>) -> Self pub fn greater_or_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self::compare(ComparisonOperator::GreaterOrEqual, left, right) 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<F>) -> 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<F>>,
consequent: Box<Formula<F>>) -> Self
{ {
Self::Implies(Implies::new(antecedent, consequent)) Self::Implies(Implies::new(direction, antecedent, consequent))
} }
pub fn less(left: Box<Term>, right: Box<Term>) -> Self pub fn less(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self::compare(ComparisonOperator::Less, left, right) Self::compare(ComparisonOperator::Less, left, right)
} }
pub fn less_or_equal(left: Box<Term>, right: Box<Term>) -> Self pub fn less_or_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self::compare(ComparisonOperator::LessOrEqual, left, right) Self::compare(ComparisonOperator::LessOrEqual, left, right)
} }
pub fn not(argument: Box<Formula>) -> Self pub fn not(argument: Box<Formula<F>>) -> Self
{ {
Self::Not(argument) Self::Not(argument)
} }
pub fn not_equal(left: Box<Term>, right: Box<Term>) -> Self pub fn not_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
{ {
Self::compare(ComparisonOperator::NotEqual, left, right) Self::compare(ComparisonOperator::NotEqual, left, right)
} }
pub fn or(arguments: Formulas) -> Self pub fn or(arguments: Formulas<F>) -> Self
{ {
assert!(!arguments.is_empty());
Self::Or(arguments) Self::Or(arguments)
} }
pub fn predicate(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) pub fn predicate(declaration: std::rc::Rc<F::PredicateDeclaration>, arguments: Terms<F>) -> Self
-> Self
{ {
Self::Predicate(Predicate::new(declaration, arguments)) Self::Predicate(Predicate::new(declaration, arguments))
} }
@ -563,3 +601,11 @@ impl Formula
Self::boolean(true) 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>,
}

85
src/flavor.rs Normal file
View File

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

View File

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

1275
src/format/formulas.rs Normal file

File diff suppressed because it is too large Load Diff

1090
src/format/terms.rs Normal file

File diff suppressed because it is too large Load Diff

View File

@ -1,4 +1,11 @@
mod ast; mod ast;
pub mod format; pub mod flavor;
mod format;
mod parse;
mod utils;
pub use ast::*; pub use ast::*;
pub use format::{formulas::FormulaDisplay, terms::TermDisplay};
pub use flavor::{DefaultFlavor, Flavor};
pub use utils::*;
pub use parse::{DefaultParser, Parser};

142
src/parse.rs Normal file
View File

@ -0,0 +1,142 @@
pub mod error;
pub mod formulas;
pub mod terms;
pub mod tokens;
pub use error::Error;
use crate::flavor::{FunctionDeclaration as _, PredicateDeclaration as _, VariableDeclaration as _};
pub trait Parser: Sized
{
type Flavor: crate::flavor::Flavor;
fn find_or_create_function_declaration(&self, name: &str, arity: usize)
-> std::rc::Rc<<Self::Flavor as crate::flavor::Flavor>::FunctionDeclaration>;
fn find_or_create_predicate_declaration(&self, name: &str, arity: usize)
-> std::rc::Rc<<Self::Flavor as crate::flavor::Flavor>::PredicateDeclaration>;
fn new_variable_declaration(name: String)
-> <Self::Flavor as crate::flavor::Flavor>::VariableDeclaration;
fn find_or_create_variable_declaration(
variable_declaration_stack_layer: &crate::VariableDeclarationStackLayer<Self::Flavor>,
variable_name: &str)
-> std::rc::Rc<<Self::Flavor as crate::flavor::Flavor>::VariableDeclaration>
{
match variable_declaration_stack_layer
{
crate::VariableDeclarationStackLayer::Free(free_variable_declarations) =>
{
if let Some(variable_declaration) = free_variable_declarations.borrow().iter()
.find(|x| x.matches_name(variable_name))
{
return std::rc::Rc::clone(&variable_declaration);
}
let variable_declaration = Self::new_variable_declaration(variable_name.to_owned());
let variable_declaration = std::rc::Rc::new(variable_declaration);
free_variable_declarations.borrow_mut()
.push(std::rc::Rc::clone(&variable_declaration));
variable_declaration
},
crate::VariableDeclarationStackLayer::Bound(bound_variable_declarations) =>
{
if let Some(variable_declaration) = bound_variable_declarations
.variable_declarations.iter()
.find(|x| x.matches_name(variable_name))
{
return std::rc::Rc::clone(&variable_declaration);
}
Self::find_or_create_variable_declaration(bound_variable_declarations.parent,
variable_name)
},
}
}
fn parse_formula(&self, input: &str)
-> Result<crate::OpenFormula<Self::Flavor>, crate::parse::Error>
{
formulas::formula(input, self)
}
}
pub struct DefaultParser
{
function_declarations:
std::cell::RefCell<crate::FunctionDeclarations<<Self as Parser>::Flavor>>,
predicate_declarations:
std::cell::RefCell<crate::PredicateDeclarations<<Self as Parser>::Flavor>>,
}
impl DefaultParser
{
pub fn new() -> Self
{
Self
{
function_declarations: std::cell::RefCell::new(
crate::FunctionDeclarations::<<Self as Parser>::Flavor>::new()),
predicate_declarations: std::cell::RefCell::new(
crate::PredicateDeclarations::<<Self as Parser>::Flavor>::new()),
}
}
}
impl Parser for DefaultParser
{
type Flavor = crate::flavor::DefaultFlavor;
fn new_variable_declaration(name: String)
-> <Self::Flavor as crate::flavor::Flavor>::VariableDeclaration
{
crate::VariableDeclaration
{
name,
}
}
fn find_or_create_function_declaration(&self, name: &str, arity: usize)
-> std::rc::Rc<<Self::Flavor as crate::flavor::Flavor>::FunctionDeclaration>
{
let mut function_declarations = self.function_declarations.borrow_mut();
match function_declarations.iter().find(|x| x.matches_signature(name, arity))
{
Some(declaration) => std::rc::Rc::clone(&declaration),
None =>
{
let declaration = crate::FunctionDeclaration::new(name.to_string(), arity);
let declaration = std::rc::Rc::new(declaration);
function_declarations.insert(std::rc::Rc::clone(&declaration));
declaration
},
}
}
fn find_or_create_predicate_declaration(&self, name: &str, arity: usize)
-> std::rc::Rc<<Self::Flavor as crate::flavor::Flavor>::PredicateDeclaration>
{
let mut predicate_declarations = self.predicate_declarations.borrow_mut();
match predicate_declarations.iter().find(|x| x.matches_signature(name, arity))
{
Some(declaration) => std::rc::Rc::clone(&declaration),
None =>
{
let declaration = crate::PredicateDeclaration::new(name.to_string(), arity);
let declaration = std::rc::Rc::new(declaration);
predicate_declarations.insert(std::rc::Rc::clone(&declaration));
declaration
},
}
}
}

182
src/parse/error.rs Normal file
View File

@ -0,0 +1,182 @@
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
src/parse/formulas.rs Normal file
View File

@ -0,0 +1,564 @@
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
src/parse/terms.rs Normal file
View File

@ -0,0 +1,651 @@
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
src/parse/tokens.rs Normal file
View File

@ -0,0 +1,641 @@
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
src/utils.rs Normal file
View File

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