82 Commits

Author SHA1 Message Date
80980e4e11 Remove redundant indirection 2020-04-10 23:02:14 +02:00
02cf3f552b Remove redundant indirection 2020-04-10 19:40:39 +02:00
80636b447a Simplify representation of quantified formulas 2020-04-10 15:18:50 +02:00
903993dbec Minor clean-up 2020-04-09 16:49:45 +02:00
f4f8dbf396 Minor clean-up 2020-04-09 16:11:59 +02:00
680f17bda0 Refactoring 2020-04-09 16:07:34 +02:00
f949c0f3f8 Refactoring 2020-04-09 16:07:34 +02:00
7b2b292727 Remove unneeded parentheses enum 2020-04-09 16:07:33 +02:00
6c326ddb70 Refactor parenthesis rules for terms 2020-04-09 16:07:33 +02:00
9754f933ef Reorganize term formatter tests 2020-04-09 16:07:33 +02:00
351d7cdd19 Rewrite term formatting tests for clarity 2020-04-09 16:07:33 +02:00
3b7394a43e Support quantified expressions with 0 parameters 2020-04-09 16:07:33 +02:00
9a8013f1cb Support empty n-aries 2020-04-09 16:07:33 +02:00
51cbdb313f Finish testing biconditionals 2020-04-09 16:07:33 +02:00
3bd52845be Reorganize tests 2020-04-09 16:07:33 +02:00
186ed314d3 Rewrite tests for clarity 2020-04-09 16:07:33 +02:00
a8df440fdf Add type annotations 2020-04-09 16:07:33 +02:00
d051b84845 Rewrite tests for clarity 2020-04-09 16:07:33 +02:00
704fe597a2 Rewrite tests for clarity 2020-04-09 16:07:33 +02:00
f3b4cdc399 Experimental method for testing all permutations 2020-04-09 16:07:33 +02:00
21d4b1d605 Test biconditionals 2020-04-09 16:07:32 +02:00
0c132edc07 Continue testing implication 2020-04-09 16:07:32 +02:00
b6308695f6 Fix precedence of implication 2020-04-09 16:07:32 +02:00
e0dbb8b75f Refactor parenthesis requirement check 2020-04-09 16:07:32 +02:00
80d7460ec1 Start testing implications 2020-04-09 16:07:32 +02:00
33f751781e Test disjunction 2020-04-09 16:07:32 +02:00
e4700fc638 Test conjunction 2020-04-09 16:07:32 +02:00
9e74116a4d Clean up tests 2020-04-09 16:07:32 +02:00
5512813cba Clean up tests 2020-04-09 16:07:32 +02:00
c11156b2ce Test quantified formulas 2020-04-09 16:07:32 +02:00
cc3265fc72 Test negation 2020-04-09 16:07:32 +02:00
121c858bff Remove unneeded precedence implementation 2020-04-09 16:07:32 +02:00
881419b8ee Address warnings 2020-04-09 16:07:31 +02:00
dc27ab8aeb Fix 2020-04-09 16:07:31 +02:00
c8ca7ba337 Remove ChildPosition enum 2020-04-09 16:07:31 +02:00
1968ed83ee Refactor precedence rules for formulas 2020-04-09 16:07:31 +02:00
d1ab7963b1 Before larger refactoring 2020-04-09 16:07:31 +02:00
1a497254a8 Add unit tests for precedence-0 formulas and lower 2020-04-09 16:07:31 +02:00
d57b3b3b62 Test remaining formula types 2020-04-09 16:07:31 +02:00
57d568916f Minor formatting 2020-04-09 16:07:31 +02:00
e4fe047aba Start testing formula formatter 2020-04-09 16:07:31 +02:00
600a6a1b4b Refactor precedence rules 2020-04-09 16:07:31 +02:00
8bf9d4bd45 Fix implication formatting 2020-04-09 16:07:31 +02:00
f82a20e5f1 Work in progress 2020-04-09 16:07:31 +02:00
5c51018ab1 Add unit test for function declaration formatting 2020-04-09 16:07:30 +02:00
23e1854346 Test term formatting 2020-04-09 16:07:30 +02:00
a3da369346 Split formatting functionality into two files 2020-04-09 16:07:30 +02:00
caf957deed Fix implication parser and output 2020-04-09 16:07:30 +02:00
1ece0e89ef Add note 2020-04-09 16:07:30 +02:00
0fdec430af Parentheses for stronger checks 2020-04-09 16:07:30 +02:00
5ea0a96ec4 Test disjunction parser 2020-04-09 16:07:30 +02:00
17d8dbd8ba Test conjunction parser 2020-04-09 16:07:30 +02:00
834e59207f Add note 2020-04-09 16:07:30 +02:00
257e02f285 Minor refactoring 2020-04-09 16:07:30 +02:00
2e3707e0af Check that names don’t start with special characters 2020-04-09 16:07:30 +02:00
d0263dd1c4 Add missing word boundary character 2020-04-09 16:07:30 +02:00
a7dd4d2fe9 Disallow reserved keywords as names 2020-04-09 16:07:29 +02:00
c127bc5eea Address clippy warning 2020-04-09 16:07:29 +02:00
cb616eba87 Refactor term parser tests 2020-04-09 16:07:29 +02:00
95677bae34 Fix negation parser 2020-04-09 16:07:29 +02:00
3414e8075c Address warnings 2020-04-09 16:07:29 +02:00
675063e1b8 Move string parser to separate module 2020-04-09 16:07:29 +02:00
7d78a504b1 Move special integer parser to separate module 2020-04-09 16:07:29 +02:00
6f86cd40d7 Move integer parser to separate module 2020-04-09 16:07:29 +02:00
29ea4578e4 Move boolean parser to separate module 2020-04-09 16:07:29 +02:00
a1bbae9201 Finish implementing formula parsing 2020-04-09 16:07:29 +02:00
1c00e5be16 Continue parsing formulas 2020-04-09 16:07:29 +02:00
1b89d8900e Start parsing formulas 2020-04-09 16:07:29 +02:00
af1ec8a606 Fix term parsing and finish tests 2020-04-09 16:07:29 +02:00
2907d10148 Make parse feature the default 2020-04-09 16:07:28 +02:00
19e70a90c5 Test associativity of multiplication 2020-04-09 16:07:28 +02:00
385c878597 Add term parsing test 2020-04-09 16:07:28 +02:00
5b98e8a29c Finish implementing term parsing 2020-04-09 16:07:28 +02:00
3530364ea8 Implement variable parsing 2020-04-09 16:07:28 +02:00
deae102405 Require word boundaries around names 2020-04-09 16:07:28 +02:00
0fc8506164 Implement booleans 2020-04-09 16:07:28 +02:00
e6a5c20d42 Add pipe character to allowed word boundaries 2020-04-09 16:07:28 +02:00
d5cd179a2d Implement strings 2020-04-09 16:07:28 +02:00
5ec9331b4c Implement word boundaries 2020-04-09 16:07:28 +02:00
896af02120 Start parsing terms 2020-04-09 16:07:28 +02:00
0c057211ed Implement name parsing 2020-04-09 16:07:28 +02:00
91918cf645 Start reimplementing parser 2020-04-09 16:07:25 +02:00
17 changed files with 2300 additions and 2555 deletions

View File

@@ -13,4 +13,8 @@ license = "MIT"
edition = "2018"
[dependencies]
log = "0.4"
nom = {version = "5.1", optional = true}
[features]
default = ["parse"]
parse = ["nom"]

View File

@@ -1,5 +1,3 @@
use crate::flavor::{FunctionDeclaration as _, PredicateDeclaration as _};
// Operators
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
@@ -61,8 +59,7 @@ impl FunctionDeclaration
}
}
pub type FunctionDeclarations<F> =
std::collections::BTreeSet<std::rc::Rc<<F as crate::flavor::Flavor>::FunctionDeclaration>>;
pub type FunctionDeclarations = std::collections::BTreeSet<std::rc::Rc<FunctionDeclaration>>;
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct PredicateDeclaration
@@ -83,8 +80,7 @@ impl PredicateDeclaration
}
}
pub type PredicateDeclarations<F> =
std::collections::BTreeSet<std::rc::Rc<<F as crate::flavor::Flavor>::PredicateDeclaration>>;
pub type PredicateDeclarations = std::collections::BTreeSet<std::rc::Rc<PredicateDeclaration>>;
pub struct VariableDeclaration
{
@@ -94,10 +90,10 @@ pub struct VariableDeclaration
impl std::cmp::PartialEq for VariableDeclaration
{
#[inline(always)]
fn eq(&self, other: &Self) -> bool
fn eq(&self, other: &VariableDeclaration) -> bool
{
let l = self as *const Self;
let r = other as *const Self;
let l = self as *const VariableDeclaration;
let r = other as *const VariableDeclaration;
l.eq(&r)
}
@@ -153,26 +149,21 @@ impl VariableDeclaration
}
}
pub type VariableDeclarations<F> =
Vec<std::rc::Rc<<F as crate::flavor::Flavor>::VariableDeclaration>>;
pub type VariableDeclarations = Vec<std::rc::Rc<VariableDeclaration>>;
// Terms
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct BinaryOperation<F>
where
F: crate::flavor::Flavor,
pub struct BinaryOperation
{
pub operator: BinaryOperator,
pub left: Box<Term<F>>,
pub right: Box<Term<F>>,
pub left: Box<Term>,
pub right: Box<Term>,
}
impl<F> BinaryOperation<F>
where
F: crate::flavor::Flavor,
impl BinaryOperation
{
pub fn new(operator: BinaryOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn new(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
{
Self
{
@@ -184,22 +175,18 @@ where
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Function<F>
where
F: crate::flavor::Flavor,
pub struct Function
{
pub declaration: std::rc::Rc<F::FunctionDeclaration>,
pub arguments: Terms<F>,
pub declaration: std::rc::Rc<FunctionDeclaration>,
pub arguments: Terms,
}
impl<F> Function<F>
where
F: crate::flavor::Flavor,
impl Function
{
pub fn new(declaration: std::rc::Rc<F::FunctionDeclaration>, arguments: Terms<F>) -> Self
pub fn new(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Terms) -> Self
{
assert_eq!(declaration.arity(), arguments.len(),
"function has a different number of arguments than declared");
assert_eq!(declaration.arity, arguments.len(),
"function has a different number of arguments then declared");
Self
{
@@ -217,19 +204,15 @@ pub enum SpecialInteger
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct UnaryOperation<F>
where
F: crate::flavor::Flavor,
pub struct UnaryOperation
{
pub operator: UnaryOperator,
pub argument: Box<Term<F>>,
pub argument: Box<Term>,
}
impl<F> UnaryOperation<F>
where
F: crate::flavor::Flavor,
impl UnaryOperation
{
pub fn new(operator: UnaryOperator, argument: Box<Term<F>>) -> Self
pub fn new(operator: UnaryOperator, argument: Box<Term>) -> Self
{
Self
{
@@ -240,18 +223,14 @@ where
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Variable<F>
where
F: crate::flavor::Flavor,
pub struct Variable
{
pub declaration: std::rc::Rc<F::VariableDeclaration>,
pub declaration: std::rc::Rc<VariableDeclaration>,
}
impl<F> Variable<F>
where
F: crate::flavor::Flavor,
impl Variable
{
pub fn new(declaration: std::rc::Rc<F::VariableDeclaration>) -> Self
pub fn new(declaration: std::rc::Rc<VariableDeclaration>) -> Self
{
Self
{
@@ -263,20 +242,16 @@ where
// Formulas
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Compare<F>
where
F: crate::flavor::Flavor,
pub struct Compare
{
pub operator: ComparisonOperator,
pub left: Box<Term<F>>,
pub right: Box<Term<F>>,
pub left: Box<Term>,
pub right: Box<Term>,
}
impl<F> Compare<F>
where
F: crate::flavor::Flavor,
impl Compare
{
pub fn new(operator: ComparisonOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn new(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
{
Self
{
@@ -288,19 +263,15 @@ where
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct QuantifiedFormula<F>
where
F: crate::flavor::Flavor,
pub struct QuantifiedFormula
{
pub parameters: std::rc::Rc<VariableDeclarations<F>>,
pub argument: Box<Formula<F>>,
pub parameters: std::rc::Rc<VariableDeclarations>,
pub argument: Box<Formula>,
}
impl<F> QuantifiedFormula<F>
where
F: crate::flavor::Flavor,
impl QuantifiedFormula
{
pub fn new(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
pub fn new(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
{
Self
{
@@ -311,21 +282,16 @@ where
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Implies<F>
where
F: crate::flavor::Flavor,
pub struct Implies
{
pub direction: ImplicationDirection,
pub antecedent: Box<Formula<F>>,
pub implication: Box<Formula<F>>,
pub antecedent: Box<Formula>,
pub implication: Box<Formula>,
}
impl<F> Implies<F>
where
F: crate::flavor::Flavor,
impl Implies
{
pub fn new(direction: ImplicationDirection, antecedent: Box<Formula<F>>,
implication: Box<Formula<F>>)
pub fn new(direction: ImplicationDirection, antecedent: Box<Formula>, implication: Box<Formula>)
-> Self
{
Self
@@ -338,22 +304,18 @@ where
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub struct Predicate<F>
where
F: crate::flavor::Flavor,
pub struct Predicate
{
pub declaration: std::rc::Rc<F::PredicateDeclaration>,
pub arguments: Terms<F>,
pub declaration: std::rc::Rc<PredicateDeclaration>,
pub arguments: Terms,
}
impl<F> Predicate<F>
where
F: crate::flavor::Flavor,
impl Predicate
{
pub fn new(declaration: std::rc::Rc<F::PredicateDeclaration>, arguments: Terms<F>) -> Self
pub fn new(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Terms) -> Self
{
assert_eq!(declaration.arity(), arguments.len(),
"predicate has a different number of arguments than declared");
assert_eq!(declaration.arity, arguments.len(),
"predicate has a different number of arguments then declared");
Self
{
@@ -366,37 +328,33 @@ where
// Variants
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum Term<F>
where
F: crate::flavor::Flavor,
pub enum Term
{
BinaryOperation(BinaryOperation<F>),
BinaryOperation(BinaryOperation),
Boolean(bool),
Function(Function<F>),
Function(Function),
Integer(i32),
SpecialInteger(SpecialInteger),
String(String),
UnaryOperation(UnaryOperation<F>),
Variable(Variable<F>),
UnaryOperation(UnaryOperation),
Variable(Variable),
}
pub type Terms<F> = Vec<Term<F>>;
pub type Terms = Vec<Term>;
impl<F> Term<F>
where
F: crate::flavor::Flavor,
impl Term
{
pub fn absolute_value(argument: Box<Term<F>>) -> Self
pub fn absolute_value(argument: Box<Term>) -> Self
{
Self::unary_operation(UnaryOperator::AbsoluteValue, argument)
}
pub fn add(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn add(left: Box<Term>, right: Box<Term>) -> Self
{
Self::binary_operation(BinaryOperator::Add, left, right)
}
pub fn binary_operation(operator: BinaryOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn binary_operation(operator: BinaryOperator, left: Box<Term>, right: Box<Term>) -> Self
{
Self::BinaryOperation(BinaryOperation::new(operator, left, right))
}
@@ -406,12 +364,12 @@ where
Self::Boolean(value)
}
pub fn divide(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn divide(left: Box<Term>, right: Box<Term>) -> Self
{
Self::binary_operation(BinaryOperator::Divide, left, right)
}
pub fn exponentiate(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn exponentiate(left: Box<Term>, right: Box<Term>) -> Self
{
Self::binary_operation(BinaryOperator::Exponentiate, left, right)
}
@@ -421,7 +379,7 @@ where
Self::boolean(false)
}
pub fn function(declaration: std::rc::Rc<F::FunctionDeclaration>, arguments: Terms<F>) -> Self
pub fn function(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Terms) -> Self
{
Self::Function(Function::new(declaration, arguments))
}
@@ -436,17 +394,17 @@ where
Self::Integer(value)
}
pub fn modulo(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn modulo(left: Box<Term>, right: Box<Term>) -> Self
{
Self::binary_operation(BinaryOperator::Modulo, left, right)
}
pub fn multiply(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn multiply(left: Box<Term>, right: Box<Term>) -> Self
{
Self::binary_operation(BinaryOperator::Multiply, left, right)
}
pub fn negative(argument: Box<Term<F>>) -> Self
pub fn negative(argument: Box<Term>) -> Self
{
Self::unary_operation(UnaryOperator::Negative, argument)
}
@@ -461,7 +419,7 @@ where
Self::String(value)
}
pub fn subtract(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn subtract(left: Box<Term>, right: Box<Term>) -> Self
{
Self::binary_operation(BinaryOperator::Subtract, left, right)
}
@@ -476,41 +434,37 @@ where
Self::boolean(true)
}
pub fn unary_operation(operator: UnaryOperator, argument: Box<Term<F>>) -> Self
pub fn unary_operation(operator: UnaryOperator, argument: Box<Term>) -> Self
{
Self::UnaryOperation(UnaryOperation::new(operator, argument))
}
pub fn variable(declaration: std::rc::Rc<F::VariableDeclaration>) -> Self
pub fn variable(declaration: std::rc::Rc<VariableDeclaration>) -> Self
{
Self::Variable(Variable::new(declaration))
}
}
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
pub enum Formula<F>
where
F: crate::flavor::Flavor,
pub enum Formula
{
And(Formulas<F>),
And(Formulas),
Boolean(bool),
Compare(Compare<F>),
Exists(QuantifiedFormula<F>),
ForAll(QuantifiedFormula<F>),
IfAndOnlyIf(Formulas<F>),
Implies(Implies<F>),
Not(Box<Formula<F>>),
Or(Formulas<F>),
Predicate(Predicate<F>),
Compare(Compare),
Exists(QuantifiedFormula),
ForAll(QuantifiedFormula),
IfAndOnlyIf(Formulas),
Implies(Implies),
Not(Box<Formula>),
Or(Formulas),
Predicate(Predicate),
}
pub type Formulas<F> = Vec<Formula<F>>;
pub type Formulas = Vec<Formula>;
impl<F> Formula<F>
where
F: crate::flavor::Flavor,
impl Formula
{
pub fn and(arguments: Formulas<F>) -> Self
pub fn and(arguments: Formulas) -> Self
{
Self::And(arguments)
}
@@ -520,17 +474,17 @@ where
Self::Boolean(value)
}
pub fn compare(operator: ComparisonOperator, left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn compare(operator: ComparisonOperator, left: Box<Term>, right: Box<Term>) -> Self
{
Self::Compare(Compare::new(operator, left, right))
}
pub fn exists(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
{
Self::Exists(QuantifiedFormula::new(parameters, argument))
}
pub fn equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn equal(left: Box<Term>, right: Box<Term>) -> Self
{
Self::compare(ComparisonOperator::Equal, left, right)
}
@@ -540,58 +494,58 @@ where
Self::boolean(false)
}
pub fn for_all(parameters: std::rc::Rc<VariableDeclarations<F>>, argument: Box<Formula<F>>) -> Self
pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
{
Self::ForAll(QuantifiedFormula::new(parameters, argument))
}
pub fn greater(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn greater(left: Box<Term>, right: Box<Term>) -> Self
{
Self::compare(ComparisonOperator::Greater, left, right)
}
pub fn greater_or_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn greater_or_equal(left: Box<Term>, right: Box<Term>) -> Self
{
Self::compare(ComparisonOperator::GreaterOrEqual, left, right)
}
pub fn if_and_only_if(arguments: Formulas<F>) -> Self
pub fn if_and_only_if(arguments: Formulas) -> Self
{
Self::IfAndOnlyIf(arguments)
}
pub fn implies(direction: ImplicationDirection, antecedent: Box<Formula<F>>,
consequent: Box<Formula<F>>) -> Self
pub fn implies(direction: ImplicationDirection, antecedent: Box<Formula>,
consequent: Box<Formula>) -> Self
{
Self::Implies(Implies::new(direction, antecedent, consequent))
}
pub fn less(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn less(left: Box<Term>, right: Box<Term>) -> Self
{
Self::compare(ComparisonOperator::Less, left, right)
}
pub fn less_or_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn less_or_equal(left: Box<Term>, right: Box<Term>) -> Self
{
Self::compare(ComparisonOperator::LessOrEqual, left, right)
}
pub fn not(argument: Box<Formula<F>>) -> Self
pub fn not(argument: Box<Formula>) -> Self
{
Self::Not(argument)
}
pub fn not_equal(left: Box<Term<F>>, right: Box<Term<F>>) -> Self
pub fn not_equal(left: Box<Term>, right: Box<Term>) -> Self
{
Self::compare(ComparisonOperator::NotEqual, left, right)
}
pub fn or(arguments: Formulas<F>) -> Self
pub fn or(arguments: Formulas) -> Self
{
Self::Or(arguments)
}
pub fn predicate(declaration: std::rc::Rc<F::PredicateDeclaration>, arguments: Terms<F>) -> Self
pub fn predicate(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Terms) -> Self
{
Self::Predicate(Predicate::new(declaration, arguments))
}
@@ -601,11 +555,3 @@ where
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>,
}

69
src/error.rs Normal file
View File

@@ -0,0 +1,69 @@
pub type Source = Box<dyn std::error::Error>;
pub enum Kind
{
Logic(&'static str),
}
pub struct Error
{
pub kind: Kind,
pub source: Option<Source>,
}
impl Error
{
pub(crate) fn new(kind: Kind) -> Self
{
Self
{
kind,
source: None,
}
}
pub(crate) fn with<S: Into<Source>>(mut self, source: S) -> Self
{
self.source = Some(source.into());
self
}
pub(crate) fn new_logic(description: &'static str) -> Self
{
Self::new(Kind::Logic(description))
}
}
impl std::fmt::Debug for Error
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match &self.kind
{
Kind::Logic(ref description) => write!(formatter,
"logic error, please report to bug tracker ({})", description),
}?;
Ok(())
}
}
impl std::fmt::Display for Error
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", self)
}
}
impl std::error::Error for Error
{
fn source(&self) -> Option<&(dyn std::error::Error + 'static)>
{
match &self.source
{
Some(source) => Some(source.as_ref()),
None => None,
}
}
}

View File

@@ -1,85 +0,0 @@
pub trait FunctionDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
fn arity(&self) -> usize;
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool;
}
impl FunctionDeclaration for crate::FunctionDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{}", self.name)
}
fn arity(&self) -> usize
{
self.arity
}
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool
{
self.name == other_name && self.arity == other_arity
}
}
pub trait PredicateDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
fn arity(&self) -> usize;
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool;
}
impl PredicateDeclaration for crate::PredicateDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{}", self.name)
}
fn arity(&self) -> usize
{
self.arity
}
fn matches_signature(&self, other_name: &str, other_arity: usize) -> bool
{
self.name == other_name && self.arity == other_arity
}
}
pub trait VariableDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result;
fn matches_name(&self, other_name: &str) -> bool;
}
impl VariableDeclaration for crate::VariableDeclaration
{
fn display_name(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{}", self.name)
}
fn matches_name(&self, other_name: &str) -> bool
{
self.name == other_name
}
}
pub trait Flavor
{
type FunctionDeclaration: FunctionDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
type PredicateDeclaration:
PredicateDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
type VariableDeclaration: VariableDeclaration + std::cmp::Eq + std::cmp::Ord + std::hash::Hash;
}
pub struct DefaultFlavor;
impl Flavor for DefaultFlavor
{
type FunctionDeclaration = crate::FunctionDeclaration;
type PredicateDeclaration = crate::PredicateDeclaration;
type VariableDeclaration = crate::VariableDeclaration;
}

View File

@@ -1,2 +1,2 @@
pub mod formulas;
pub mod terms;
mod formulas;
mod terms;

View File

@@ -1,72 +1,48 @@
use crate::flavor::{PredicateDeclaration as _, VariableDeclaration as _};
use super::terms::*;
impl std::fmt::Debug for crate::ComparisonOperator
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
let operator_symbol = match self
{
Self::Less => "<",
Self::LessOrEqual => "<=",
Self::Greater => ">",
Self::GreaterOrEqual => ">=",
Self::Equal => "=",
Self::NotEqual => "!=",
};
write!(formatter, "{}", operator_symbol)
}
}
impl std::fmt::Debug for crate::ImplicationDirection
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
match &self
{
Self::LeftToRight => write!(formatter, "left to right"),
Self::RightToLeft => write!(formatter, "right to left"),
Self::LeftToRight => write!(format, "left to right"),
Self::RightToLeft => write!(format, "right to left"),
}
}
}
impl std::fmt::Debug for crate::PredicateDeclaration
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{}/{}", &self.name, self.arity)
write!(format, "{}/{}", &self.name, self.arity)
}
}
impl std::fmt::Display for crate::PredicateDeclaration
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", &self)
write!(format, "{:?}", &self)
}
}
#[derive(Clone, Copy, Eq, PartialEq)]
pub(crate) enum FormulaPosition
enum FormulaPosition
{
Any,
ImpliesAntecedent,
}
pub struct FormulaDisplay<'formula, F>
where
F: crate::flavor::Flavor,
struct FormulaDisplay<'formula>
{
formula: &'formula crate::Formula<F>,
parent_formula: Option<&'formula crate::Formula<F>>,
formula: &'formula crate::Formula,
parent_formula: Option<&'formula crate::Formula>,
position: FormulaPosition,
//declarations: &'d D,
}
impl<'formula, F> FormulaDisplay<'formula, F>
where
F: crate::flavor::Flavor,
impl<'formula> FormulaDisplay<'formula>
{
fn requires_parentheses(&self) -> bool
{
@@ -136,11 +112,9 @@ where
}
}
pub(crate) fn display_formula<'formula, F>(formula: &'formula crate::Formula<F>,
parent_formula: Option<&'formula crate::Formula<F>>, position: FormulaPosition)
-> FormulaDisplay<'formula, F>
where
F: crate::flavor::Flavor,
fn display_formula<'formula>(formula: &'formula crate::Formula,
parent_formula: Option<&'formula crate::Formula>, position: FormulaPosition)
-> FormulaDisplay<'formula>
{
FormulaDisplay
{
@@ -150,17 +124,15 @@ where
}
}
impl<'formula, F> std::fmt::Debug for FormulaDisplay<'formula, F>
where
F: crate::flavor::Flavor,
impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
let requires_parentheses = self.requires_parentheses();
if requires_parentheses
{
write!(formatter, "(")?;
write!(format, "(")?;
}
match &self.formula
@@ -169,24 +141,23 @@ where
{
if exists.parameters.is_empty()
{
write!(formatter, "{:?}", display_formula::<F>(&exists.argument,
self.parent_formula, self.position))?;
write!(format, "{:?}", display_formula(&exists.argument, self.parent_formula,
self.position))?;
}
else
{
write!(formatter, "exists")?;
write!(format, "exists")?;
let mut separator = " ";
for parameter in exists.parameters.iter()
{
write!(formatter, "{}", separator)?;
parameter.display_name(formatter)?;
write!(format, "{}{:?}", separator, parameter)?;
separator = ", "
}
write!(formatter, " {:?}", display_formula(&exists.argument, Some(self.formula),
write!(format, " {:?}", display_formula(&exists.argument, Some(self.formula),
FormulaPosition::Any))?;
}
},
@@ -194,34 +165,33 @@ where
{
if for_all.parameters.is_empty()
{
write!(formatter, "{:?}", display_formula(&for_all.argument,
self.parent_formula, self.position))?;
write!(format, "{:?}", display_formula(&for_all.argument, self.parent_formula,
self.position))?;
}
else
{
write!(formatter, "forall")?;
write!(format, "forall")?;
let mut separator = " ";
for parameter in for_all.parameters.iter()
{
write!(formatter, "{}", separator)?;
parameter.display_name(formatter)?;
write!(format, "{}{:?}", separator, parameter)?;
separator = ", "
}
write!(formatter, " {:?}", display_formula(&for_all.argument,
Some(self.formula), FormulaPosition::Any))?;
write!(format, " {:?}", display_formula(&for_all.argument, Some(self.formula),
FormulaPosition::Any))?;
}
},
crate::Formula::Not(argument) => write!(formatter, "not {:?}",
crate::Formula::Not(argument) => write!(format, "not {:?}",
display_formula(argument, Some(self.formula), FormulaPosition::Any))?,
crate::Formula::And(arguments) =>
{
if arguments.is_empty()
{
write!(formatter, "true")?;
write!(format, "true")?;
}
else
{
@@ -235,7 +205,7 @@ where
for argument in arguments
{
write!(formatter, "{}{:?}", separator,
write!(format, "{}{:?}", separator,
display_formula(argument, parent_formula, position))?;
separator = " and "
@@ -246,7 +216,7 @@ where
{
if arguments.is_empty()
{
write!(formatter, "false")?;
write!(format, "false")?;
}
else
{
@@ -260,7 +230,7 @@ where
for argument in arguments
{
write!(formatter, "{}{:?}", separator,
write!(format, "{}{:?}", separator,
display_formula(argument, parent_formula, position))?;
separator = " or "
@@ -269,16 +239,16 @@ where
},
crate::Formula::Implies(crate::Implies{direction, antecedent, implication}) =>
{
let format_antecedent = |formatter: &mut std::fmt::Formatter| -> Result<_, _>
let format_antecedent = |format: &mut std::fmt::Formatter| -> Result<_, _>
{
write!(formatter, "{:?}",
write!(format, "{:?}",
display_formula(antecedent, Some(self.formula),
FormulaPosition::ImpliesAntecedent))
};
let format_implication = |formatter: &mut std::fmt::Formatter| -> Result<_, _>
let format_implication = |format: &mut std::fmt::Formatter| -> Result<_, _>
{
write!(formatter, "{:?}",
write!(format, "{:?}",
display_formula(implication, Some(self.formula), FormulaPosition::Any))
};
@@ -286,15 +256,15 @@ where
{
crate::ImplicationDirection::LeftToRight =>
{
format_antecedent(formatter)?;
write!(formatter, " -> ")?;
format_implication(formatter)?;
format_antecedent(format)?;
write!(format, " -> ")?;
format_implication(format)?;
},
crate::ImplicationDirection::RightToLeft =>
{
format_implication(formatter)?;
write!(formatter, " <- ")?;
format_antecedent(formatter)?;
format_implication(format)?;
write!(format, " <- ")?;
format_antecedent(format)?;
},
}
},
@@ -302,7 +272,7 @@ where
{
if arguments.is_empty()
{
write!(formatter, "true")?;
write!(format, "true")?;
}
else
{
@@ -316,7 +286,7 @@ where
for argument in arguments
{
write!(formatter, "{}{:?}", separator,
write!(format, "{}{:?}", separator,
display_formula(argument, parent_formula, position))?;
separator = " <-> "
@@ -335,71 +305,66 @@ where
crate::ComparisonOperator::NotEqual => "!=",
};
write!(formatter, "{:?} {} {:?}",
display_term(&compare.left, None, TermPosition::Any), operator_string,
write!(format, "{:?} {} {:?}",
display_term(&compare.left, None, TermPosition::Any),
operator_string,
display_term(&compare.right, None, TermPosition::Any))?;
},
crate::Formula::Boolean(true) => write!(formatter, "true")?,
crate::Formula::Boolean(false) => write!(formatter, "false")?,
crate::Formula::Boolean(true) => write!(format, "true")?,
crate::Formula::Boolean(false) => write!(format, "false")?,
crate::Formula::Predicate(predicate) =>
{
predicate.declaration.display_name(formatter)?;
write!(format, "{}", predicate.declaration.name)?;
if !predicate.arguments.is_empty()
{
write!(formatter, "(")?;
write!(format, "(")?;
let mut separator = "";
for argument in &predicate.arguments
{
write!(formatter, "{}{:?}", separator, display_term(argument, None,
write!(format, "{}{:?}", separator, display_term(argument, None,
TermPosition::Any))?;
separator = ", "
}
write!(formatter, ")")?;
write!(format, ")")?;
}
},
}
if requires_parentheses
{
write!(formatter, ")")?;
write!(format, ")")?;
}
Ok(())
}
}
impl<'formula, F> std::fmt::Display for FormulaDisplay<'formula, F>
where
F: crate::flavor::Flavor,
impl<'formula> std::fmt::Display for FormulaDisplay<'formula>
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", self)
write!(format, "{:?}", self)
}
}
impl<F> std::fmt::Debug for crate::Formula<F>
where
F: crate::flavor::Flavor,
impl std::fmt::Debug for crate::Formula
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", display_formula(&self, None, FormulaPosition::Any))
write!(format, "{:?}", display_formula(&self, None, FormulaPosition::Any))
}
}
impl<F> std::fmt::Display for crate::Formula<F>
where
F: crate::flavor::Flavor,
impl std::fmt::Display for crate::Formula
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{}", display_formula(&self, None, FormulaPosition::Any))
write!(format, "{}", display_formula(&self, None, FormulaPosition::Any))
}
}
@@ -407,10 +372,7 @@ where
mod tests
{
use crate::*;
use format::terms::tests::*;
type Formula = crate::Formula<flavor::DefaultFlavor>;
type Term = crate::Term<flavor::DefaultFlavor>;
type VariableDeclarations = crate::VariableDeclarations<flavor::DefaultFlavor>;
use crate::format::terms::tests::*;
macro_rules! assert
{
@@ -445,7 +407,7 @@ mod tests
};
}
fn format(formula: Box<Formula>) -> String
fn format(formula: Box<ast::Formula>) -> String
{
format!("{}", formula)
}

View File

@@ -1,38 +1,52 @@
use crate::flavor::{FunctionDeclaration as _, VariableDeclaration as _};
impl std::fmt::Debug for crate::SpecialInteger
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
match &self
{
Self::Infimum => write!(formatter, "#inf"),
Self::Supremum => write!(formatter, "#sup"),
Self::Infimum => write!(format, "#inf"),
Self::Supremum => write!(format, "#sup"),
}
}
}
impl std::fmt::Display for crate::SpecialInteger
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", &self)
write!(format, "{:?}", &self)
}
}
impl std::fmt::Debug for crate::FunctionDeclaration
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{}/{}", &self.name, self.arity)
write!(format, "{}/{}", &self.name, self.arity)
}
}
impl std::fmt::Display for crate::FunctionDeclaration
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", &self)
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)
}
}
@@ -44,18 +58,14 @@ pub(crate) enum TermPosition
Right,
}
pub struct TermDisplay<'term, F>
where
F: crate::flavor::Flavor,
pub(crate) struct TermDisplay<'term>
{
term: &'term crate::Term<F>,
parent_term: Option<&'term crate::Term<F>>,
term: &'term crate::Term,
parent_term: Option<&'term crate::Term>,
position: TermPosition,
}
impl<'term, F> TermDisplay<'term, F>
where
F: crate::flavor::Flavor,
impl<'term> TermDisplay<'term>
{
fn requires_parentheses(&self) -> bool
{
@@ -139,11 +149,9 @@ where
}
}
pub(crate) fn display_term<'term, F>(term: &'term crate::Term<F>,
parent_term: Option<&'term crate::Term<F>>, position: TermPosition)
-> TermDisplay<'term, F>
where
F: crate::flavor::Flavor,
pub(crate) fn display_term<'term>(term: &'term crate::Term, parent_term: Option<&'term crate::Term>,
position: TermPosition)
-> TermDisplay<'term>
{
TermDisplay
{
@@ -153,51 +161,49 @@ where
}
}
impl<'term, F> std::fmt::Debug for TermDisplay<'term, F>
where
F: crate::flavor::Flavor,
impl<'term> std::fmt::Debug for TermDisplay<'term>
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
let requires_parentheses = self.requires_parentheses();
if requires_parentheses
{
write!(formatter, "(")?;
write!(format, "(")?;
}
match &self.term
{
crate::Term::Boolean(true) => write!(formatter, "true")?,
crate::Term::Boolean(false) => write!(formatter, "false")?,
crate::Term::SpecialInteger(value) => write!(formatter, "{:?}", value)?,
crate::Term::Integer(value) => write!(formatter, "{}", value)?,
crate::Term::String(value) => write!(formatter, "\"{}\"",
crate::Term::Boolean(true) => write!(format, "true")?,
crate::Term::Boolean(false) => write!(format, "false")?,
crate::Term::SpecialInteger(value) => write!(format, "{:?}", value)?,
crate::Term::Integer(value) => write!(format, "{}", value)?,
crate::Term::String(value) => write!(format, "\"{}\"",
value.replace("\\", "\\\\").replace("\n", "\\n").replace("\t", "\\t"))?,
crate::Term::Variable(variable) => variable.declaration.display_name(formatter)?,
crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration)?,
crate::Term::Function(function) =>
{
function.declaration.display_name(formatter)?;
write!(format, "{}", function.declaration.name)?;
assert!(function.declaration.arity() == function.arguments.len(),
assert!(function.declaration.arity == function.arguments.len(),
"number of function arguments differs from declaration (expected {}, got {})",
function.declaration.arity(), function.arguments.len());
function.declaration.arity, function.arguments.len());
if !function.arguments.is_empty()
{
write!(formatter, "(")?;
write!(format, "(")?;
let mut separator = "";
for argument in &function.arguments
{
write!(formatter, "{}{:?}", separator,
write!(format, "{}{:?}", separator,
display_term(&argument, Some(self.term), TermPosition::Any))?;
separator = ", ";
}
write!(formatter, ")")?;
write!(format, ")")?;
}
},
crate::Term::BinaryOperation(binary_operation) =>
@@ -212,57 +218,51 @@ where
crate::BinaryOperator::Exponentiate => "**",
};
write!(formatter, "{:?} {} {:?}",
write!(format, "{:?} {} {:?}",
display_term(&binary_operation.left, Some(self.term), TermPosition::Left),
operator_string,
display_term(&binary_operation.right, Some(self.term), TermPosition::Right))?;
},
crate::Term::UnaryOperation(
crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
=> write!(formatter, "-{:?}",
=> write!(format, "-{:?}",
display_term(argument, Some(self.term), TermPosition::Any))?,
crate::Term::UnaryOperation(
crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
=> write!(formatter, "|{:?}|",
=> write!(format, "|{:?}|",
display_term(argument, Some(self.term), TermPosition::Any))?,
}
if requires_parentheses
{
write!(formatter, ")")?;
write!(format, ")")?;
}
Ok(())
}
}
impl<'term, F> std::fmt::Display for TermDisplay<'term, F>
where
F: crate::flavor::Flavor,
impl<'term> std::fmt::Display for TermDisplay<'term>
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", self)
write!(format, "{:?}", self)
}
}
impl<F> std::fmt::Debug for crate::Term<F>
where
F: crate::flavor::Flavor,
impl std::fmt::Debug for crate::Term
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", display_term(&self, None, TermPosition::Any))
write!(format, "{:?}", display_term(&self, None, TermPosition::Any))
}
}
impl<F> std::fmt::Display for crate::Term<F>
where
F: crate::flavor::Flavor,
impl std::fmt::Display for crate::Term
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{}", display_term(&self, None, TermPosition::Any))
write!(format, "{}", display_term(&self, None, TermPosition::Any))
}
}
@@ -270,7 +270,6 @@ where
pub(crate) mod tests
{
use crate::*;
type Term = crate::Term<flavor::DefaultFlavor>;
macro_rules! assert
{
@@ -280,7 +279,7 @@ pub(crate) mod tests
};
}
fn format(term: Box<Term>) -> String
fn format(term: Box<ast::Term>) -> String
{
format!("{}", term)
}

View File

@@ -1,11 +1,10 @@
mod ast;
pub mod flavor;
mod format;
mod parse;
mod error;
pub mod format;
#[cfg(feature = "parse")]
pub mod parse;
mod utils;
pub use ast::*;
pub use format::{formulas::FormulaDisplay, terms::TermDisplay};
pub use flavor::{DefaultFlavor, Flavor};
pub use utils::*;
pub use parse::{DefaultParser, Parser};
pub use error::Error;
pub use utils::VariableDeclarationStack;

View File

@@ -1,142 +1,32 @@
pub mod error;
pub mod formulas;
pub mod terms;
pub mod tokens;
mod formulas;
mod helpers;
mod literals;
mod names;
mod terms;
pub use error::Error;
pub(crate) use helpers::word_boundary;
pub(crate) use literals::{boolean, integer, special_integer, string};
pub(crate) use names::{function_or_predicate_name, variable_name};
pub use terms::term;
pub use formulas::formula;
use crate::flavor::{FunctionDeclaration as _, PredicateDeclaration as _, VariableDeclaration as _};
pub trait Parser: Sized
pub struct Declarations
{
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)
}
function_declarations: std::cell::RefCell<crate::FunctionDeclarations>,
predicate_declarations: std::cell::RefCell<crate::PredicateDeclarations>,
variable_declaration_stack: std::cell::RefCell<crate::VariableDeclarationStack>,
}
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
impl Declarations
{
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
},
function_declarations: std::cell::RefCell::new(crate::FunctionDeclarations::new()),
predicate_declarations: std::cell::RefCell::new(crate::PredicateDeclarations::new()),
variable_declaration_stack:
std::cell::RefCell::new(crate::VariableDeclarationStack::new()),
}
}
}

View File

@@ -1,182 +0,0 @@
pub type Source = Box<dyn std::error::Error>;
pub struct Location
{
start: usize,
end: Option<usize>,
}
impl Location
{
pub fn new(start: usize, end: Option<usize>) -> Self
{
Self
{
start,
end,
}
}
}
pub enum Kind
{
UnmatchedParenthesis,
CharacterNotAllowed(char),
ParseNumber(String),
MixedImplicationDirections(Location),
ExpectedVariableDeclaration,
UnexpectedToken,
EmptyExpression,
ExpectedLogicalConnectiveArgument(String),
ExpectedTerm,
MultipleComparisonOperators(crate::ComparisonOperator, crate::ComparisonOperator),
}
pub struct Error
{
pub kind: Kind,
pub location: Location,
pub source: Option<Source>,
}
impl Error
{
pub(crate) fn new(kind: Kind, location: Location) -> Self
{
Self
{
kind,
location,
source: None,
}
}
pub(crate) fn with<S: Into<Source>>(mut self, source: S) -> Self
{
self.source = Some(source.into());
self
}
pub(crate) fn new_unmatched_parenthesis(location: Location) -> Self
{
Self::new(Kind::UnmatchedParenthesis, location)
}
pub(crate) fn new_character_not_allowed(character: char, location: Location) -> Self
{
Self::new(Kind::CharacterNotAllowed(character), location)
}
pub(crate) fn new_parse_number<I: Into<String>, S: Into<Source>>(input: I, location: Location,
source: S)
-> Self
{
Self::new(Kind::ParseNumber(input.into()), location).with(source)
}
pub(crate) fn new_mixed_implication_directions(location_1: Location, location_2: Location)
-> Self
{
Self::new(Kind::MixedImplicationDirections(location_2), location_1)
}
pub(crate) fn new_expected_variable_declaration(location: Location) -> Self
{
Self::new(Kind::ExpectedVariableDeclaration, location)
}
pub(crate) fn new_unexpected_token(location: Location) -> Self
{
Self::new(Kind::UnexpectedToken, location)
}
pub(crate) fn new_empty_expression(location: Location) -> Self
{
Self::new(Kind::EmptyExpression, location)
}
pub(crate) fn new_expected_logical_connective_argument(logical_connective_name: String,
location: Location)
-> Self
{
Self::new(Kind::ExpectedLogicalConnectiveArgument(logical_connective_name), location)
}
pub(crate) fn new_expected_term(location: Location) -> Self
{
Self::new(Kind::ExpectedTerm, location)
}
pub(crate) fn new_multiple_comparison_operators(
comparison_operator_1: crate::ComparisonOperator,
comparison_operator_2: crate::ComparisonOperator, location: Location)
-> Self
{
Self::new(Kind::MultipleComparisonOperators(comparison_operator_1, comparison_operator_2),
location)
}
}
impl std::fmt::Debug for Error
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
if let Some(end) = self.location.end
{
write!(formatter, "parsing error at {}:{}: ", self.location.start, end)?;
}
else
{
write!(formatter, "parsing error at {}: ", self.location.start)?;
}
match &self.kind
{
Kind::UnmatchedParenthesis => write!(formatter, "unmatched parenthesis")?,
Kind::CharacterNotAllowed(character) =>
write!(formatter, "character not allowed: {}", character)?,
Kind::ParseNumber(input) => write!(formatter, "could not “{}” as number", input)?,
// TODO: print second location properly
Kind::MixedImplicationDirections(_location_2) =>
write!(formatter, "-> and <- implications may not be mixed within the same scope")?,
Kind::ExpectedVariableDeclaration =>
write!(formatter, "expected a variable declaration")?,
Kind::UnexpectedToken => write!(formatter, "unexpected token")?,
Kind::EmptyExpression => write!(formatter, "empty expression")?,
Kind::ExpectedLogicalConnectiveArgument(ref logical_connective_name) =>
write!(formatter, "this “{}” logical connective is missing an argument",
logical_connective_name)?,
Kind::ExpectedTerm => write!(formatter, "expected a term")?,
Kind::MultipleComparisonOperators(comparison_operator_1, comparison_operator_2) =>
write!(formatter, "chained comparisons arent supported (found “{:?}” and “{:?}” in the same formula), consider separating them with “and”",
comparison_operator_1, comparison_operator_2)?,
}
if let Some(source) = &self.source
{
write!(formatter, "\nerror source: {}", source)?;
}
Ok(())
}
}
impl std::fmt::Display for Error
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", self)
}
}
impl std::error::Error for Error
{
fn source(&self) -> Option<&(dyn std::error::Error + 'static)>
{
match &self.source
{
Some(source) => Some(source.as_ref()),
None => None,
}
}
}

File diff suppressed because it is too large Load Diff

86
src/parse/helpers.rs Normal file
View File

@@ -0,0 +1,86 @@
use nom::
{
IResult,
branch::alt,
bytes::complete::take_while_m_n,
combinator::{map, peek, rest_len, verify},
};
fn is_character_word_boundary(c: char) -> bool
{
if c.is_whitespace()
{
return true;
}
match c
{
'('
| ')'
| '>'
| '<'
| '='
| ','
| '+'
| '-'
| '*'
| '/'
| '%'
| '|'
| '#'
=> true,
_ => false,
}
}
pub(crate) fn word_boundary(i: &str) -> IResult<&str, ()>
{
peek
(
alt
((
// Accept word boundary characters
map
(
take_while_m_n(1, 1, is_character_word_boundary),
|_| (),
),
// Accept end of file
map
(
verify
(
rest_len,
|rest_length| *rest_length == 0usize,
),
|_| (),
),
))
)(i)
}
#[cfg(test)]
mod tests
{
use crate::parse::*;
#[test]
fn detect_word_boundaries()
{
assert_eq!(word_boundary(" rest"), Ok((" rest", ())));
assert_eq!(word_boundary("(rest"), Ok(("(rest", ())));
assert_eq!(word_boundary(")rest"), Ok((")rest", ())));
assert_eq!(word_boundary(",rest"), Ok((",rest", ())));
assert_eq!(word_boundary("+rest"), Ok(("+rest", ())));
assert_eq!(word_boundary("-rest"), Ok(("-rest", ())));
assert_eq!(word_boundary("*rest"), Ok(("*rest", ())));
assert_eq!(word_boundary("/rest"), Ok(("/rest", ())));
assert_eq!(word_boundary("%rest"), Ok(("%rest", ())));
assert_eq!(word_boundary("|rest"), Ok(("|rest", ())));
assert_eq!(word_boundary("<rest"), Ok(("<rest", ())));
assert_eq!(word_boundary(">rest"), Ok((">rest", ())));
assert_eq!(word_boundary("=rest"), Ok(("=rest", ())));
assert!(word_boundary("0").is_err());
assert!(word_boundary("rest").is_err());
}
}

249
src/parse/literals.rs Normal file
View File

@@ -0,0 +1,249 @@
use nom::
{
IResult,
branch::alt,
bytes::complete::{escaped_transform, tag},
character::complete::{digit1, none_of},
combinator::{map, map_res, opt, recognize},
sequence::{delimited, pair, terminated},
};
use super::word_boundary;
fn true_(i: &str) -> IResult<&str, bool>
{
map
(
terminated
(
tag("true"),
word_boundary,
),
|_| true,
)(i)
}
fn false_(i: &str) -> IResult<&str, bool>
{
map
(
terminated
(
tag("false"),
word_boundary,
),
|_| false,
)(i)
}
pub fn boolean(i: &str) -> IResult<&str, bool>
{
alt
((
true_,
false_,
))(i)
}
pub fn integer(i: &str) -> IResult<&str, i32>
{
map_res
(
recognize
(
terminated
(
pair
(
opt
(
alt
((
tag("-"),
tag("+"),
))
),
digit1,
),
word_boundary,
)
),
std::str::FromStr::from_str,
)(i)
}
fn infimum(i: &str) -> IResult<&str, crate::SpecialInteger>
{
map
(
terminated
(
tag("#inf"),
word_boundary,
),
|_| crate::SpecialInteger::Infimum,
)(i)
}
fn supremum(i: &str) -> IResult<&str, crate::SpecialInteger>
{
map
(
terminated
(
tag("#sup"),
word_boundary,
),
|_| crate::SpecialInteger::Supremum,
)(i)
}
pub fn special_integer(i: &str) -> IResult<&str, crate::SpecialInteger>
{
alt
((
infimum,
supremum,
))(i)
}
pub fn string(i: &str) -> IResult<&str, String>
{
map
(
terminated
(
delimited
(
tag("\""),
escaped_transform
(
none_of("\"\\"),
'\\',
alt
((
tag("\""),
tag("\\"),
map
(
tag("n"),
|_| "\n",
),
map
(
tag("t"),
|_| "\t",
),
)),
),
tag("\""),
),
word_boundary,
),
String::from,
)(i)
}
#[cfg(test)]
mod tests
{
use crate::SpecialInteger;
use crate::parse::*;
#[test]
fn parse_boolean()
{
assert_eq!(boolean("true"), Ok(("", true)));
assert_eq!(boolean("false"), Ok(("", false)));
assert_eq!(boolean("true false"), Ok((" false", true)));
assert_eq!(boolean("false true"), Ok((" true", false)));
assert_eq!(boolean("true,"), Ok((",", true)));
assert_eq!(boolean("false,"), Ok((",", false)));
assert!(boolean("truefalse").is_err());
assert!(boolean("falsetrue").is_err());
assert!(boolean("truea").is_err());
assert!(boolean("falsea").is_err());
assert!(boolean("a").is_err());
assert!(boolean("-").is_err());
assert!(boolean(" ").is_err());
}
#[test]
fn parse_integer()
{
assert_eq!(integer("0"), Ok(("", 0)));
assert_eq!(integer("10000"), Ok(("", 10000)));
assert_eq!(integer("+10000"), Ok(("", 10000)));
assert_eq!(integer("-10000"), Ok(("", -10000)));
assert_eq!(integer("0 42"), Ok((" 42", 0)));
assert_eq!(integer("10000 42"), Ok((" 42", 10000)));
assert_eq!(integer("+10000 42"), Ok((" 42", 10000)));
assert_eq!(integer("-10000 42"), Ok((" 42", -10000)));
assert_eq!(integer("10000,"), Ok((",", 10000)));
assert_eq!(integer("+10000,"), Ok((",", 10000)));
assert_eq!(integer("-10000,"), Ok((",", -10000)));
assert!(integer("10000a").is_err());
assert!(integer("+10000a").is_err());
assert!(integer("-10000a").is_err());
assert!(integer("1.5").is_err());
assert!(integer("a").is_err());
assert!(integer("-").is_err());
assert!(integer(" ").is_err());
}
#[test]
fn parse_special_integer()
{
assert_eq!(special_integer("#inf"), Ok(("", SpecialInteger::Infimum)));
assert_eq!(special_integer("#sup"), Ok(("", SpecialInteger::Supremum)));
assert_eq!(special_integer("#inf #sup"), Ok((" #sup", SpecialInteger::Infimum)));
assert_eq!(special_integer("#sup #inf"), Ok((" #inf", SpecialInteger::Supremum)));
assert_eq!(special_integer("#inf,"), Ok((",", SpecialInteger::Infimum)));
assert_eq!(special_integer("#sup,"), Ok((",", SpecialInteger::Supremum)));
assert!(special_integer("#inf0").is_err());
assert!(special_integer("#sup0").is_err());
assert!(special_integer("#infimum").is_err());
assert!(special_integer("#supremum").is_err());
assert!(special_integer("inf").is_err());
assert!(special_integer("sup").is_err());
assert!(special_integer("0").is_err());
assert!(special_integer("10000").is_err());
assert!(special_integer("-10000").is_err());
assert!(special_integer("-").is_err());
assert!(special_integer("+").is_err());
assert!(special_integer("a").is_err());
assert!(special_integer(" ").is_err());
}
#[test]
fn parse_string()
{
assert_eq!(string("\"test 123\""), Ok(("", "test 123".to_string())));
assert_eq!(string("\"123 test\""), Ok(("", "123 test".to_string())));
assert_eq!(string("\" test 123 \""), Ok(("", " test 123 ".to_string())));
assert_eq!(string("\"test 123\" \"rest"), Ok((" \"rest", "test 123".to_string())));
assert_eq!(string("\"test 123\", \"rest"), Ok((", \"rest", "test 123".to_string())));
assert_eq!(string("\"test\n123\""), Ok(("", "test\n123".to_string())));
assert_eq!(string("\"test\\\"123\""), Ok(("", "test\"123".to_string())));
assert_eq!(string("\"test\\\"123\\\"\""), Ok(("", "test\"123\"".to_string())));
assert_eq!(string("\"\\\"test 123\\\"\""), Ok(("", "\"test 123\"".to_string())));
assert_eq!(string("\"test\\\\123\""), Ok(("", "test\\123".to_string())));
assert_eq!(string("\"test\\\\123\\\\\""), Ok(("", "test\\123\\".to_string())));
assert_eq!(string("\"\\\\test 123\\\\\""), Ok(("", "\\test 123\\".to_string())));
assert_eq!(string("\"test\\n123\""), Ok(("", "test\n123".to_string())));
assert_eq!(string("\"test\\n123\\n\""), Ok(("", "test\n123\n".to_string())));
assert_eq!(string("\"\\ntest 123\\n\""), Ok(("", "\ntest 123\n".to_string())));
assert_eq!(string("\"test\\t123\""), Ok(("", "test\t123".to_string())));
assert_eq!(string("\"test\\t123\\t\""), Ok(("", "test\t123\t".to_string())));
assert_eq!(string("\"\\ttest 123\\t\""), Ok(("", "\ttest 123\t".to_string())));
assert_eq!(string("\"test 🙂 123\""), Ok(("", "test 🙂 123".to_string())));
assert_eq!(string("\"🙂test 123\""), Ok(("", "🙂test 123".to_string())));
assert_eq!(string("\"test 123🙂\""), Ok(("", "test 123🙂".to_string())));
assert!(string("\"test 123\"a").is_err());
assert!(string("\"test\\i123\"").is_err());
assert!(string("\"test").is_err());
assert!(string("test").is_err());
assert!(string("-").is_err());
assert!(string(" ").is_err());
}
}

159
src/parse/names.rs Normal file
View File

@@ -0,0 +1,159 @@
use nom::
{
IResult,
bytes::complete::{take_while, take_while_m_n},
combinator::recognize,
sequence::{pair, terminated},
};
use super::word_boundary;
fn is_function_name_character_first(c: char) -> bool
{
c.is_alphabetic() && c.is_lowercase()
}
fn is_function_name_character_body(c: char) -> bool
{
c.is_alphanumeric() || c == '_'
}
fn is_variable_name_character_first(c: char) -> bool
{
c.is_alphabetic() && c.is_uppercase()
}
fn is_variable_name_character_body(c: char) -> bool
{
c.is_alphanumeric() || c == '_'
}
pub fn function_or_predicate_name(i: &str) -> IResult<&str, &str>
{
let (i, name) =
recognize
(
terminated
(
pair
(
take_while_m_n(1, 1, is_function_name_character_first),
take_while(is_function_name_character_body),
),
word_boundary,
)
)(i)?;
match name
{
"and"
| "exists"
| "false"
| "forall"
| "not"
| "or"
| "true"
=> Err(nom::Err::Error((i, nom::error::ErrorKind::Verify))),
name => Ok((i, name)),
}
}
pub fn variable_name(i: &str) -> IResult<&str, &str>
{
recognize
(
terminated
(
pair
(
take_while_m_n(1, 1, is_variable_name_character_first),
take_while(is_variable_name_character_body),
),
word_boundary,
)
)(i)
}
#[cfg(test)]
mod tests
{
use crate::parse::*;
#[test]
fn parse_function_or_predicate_name()
{
assert_eq!(function_or_predicate_name("p rest"), Ok((" rest", "p")));
assert_eq!(function_or_predicate_name("f rest"), Ok((" rest", "f")));
assert_eq!(function_or_predicate_name("p, rest"), Ok((", rest", "p")));
assert_eq!(function_or_predicate_name("f, rest"), Ok((", rest", "f")));
assert_eq!(function_or_predicate_name("name_123 rest"), Ok((" rest", "name_123")));
assert!(function_or_predicate_name("0 rest").is_err());
assert!(function_or_predicate_name("123_asd rest").is_err());
assert!(function_or_predicate_name("P rest").is_err());
assert!(function_or_predicate_name("Predicate_123 rest").is_err());
assert!(function_or_predicate_name("_ rest").is_err());
assert!(function_or_predicate_name("_predicate_123 rest").is_err());
assert!(function_or_predicate_name("(p").is_err());
assert!(function_or_predicate_name(")p").is_err());
assert!(function_or_predicate_name(">p").is_err());
assert!(function_or_predicate_name("<p").is_err());
assert!(function_or_predicate_name("=p").is_err());
assert!(function_or_predicate_name(",p").is_err());
assert!(function_or_predicate_name("+p").is_err());
assert!(function_or_predicate_name("-p").is_err());
assert!(function_or_predicate_name("*p").is_err());
assert!(function_or_predicate_name("/p").is_err());
assert!(function_or_predicate_name("%p").is_err());
assert!(function_or_predicate_name("|p").is_err());
assert!(function_or_predicate_name("#inf").is_err());
assert!(function_or_predicate_name("#sup").is_err());
assert!(function_or_predicate_name("#p").is_err());
assert!(function_or_predicate_name(" ").is_err());
// Keywords arent valid names
assert!(function_or_predicate_name("and rest").is_err());
assert!(function_or_predicate_name("exists rest").is_err());
assert!(function_or_predicate_name("false rest").is_err());
assert!(function_or_predicate_name("forall rest").is_err());
assert!(function_or_predicate_name("or rest").is_err());
assert!(function_or_predicate_name("not rest").is_err());
assert!(function_or_predicate_name("true rest").is_err());
// Names that start with keywords are fine though
assert!(function_or_predicate_name("anda rest").is_ok());
assert!(function_or_predicate_name("existsa rest").is_ok());
assert!(function_or_predicate_name("falsea rest").is_ok());
assert!(function_or_predicate_name("foralla rest").is_ok());
assert!(function_or_predicate_name("ora rest").is_ok());
assert!(function_or_predicate_name("nota rest").is_ok());
assert!(function_or_predicate_name("truea rest").is_ok());
}
#[test]
fn parse_variable_name()
{
assert_eq!(variable_name("X Rest"), Ok((" Rest", "X")));
assert_eq!(variable_name("X, Rest"), Ok((", Rest", "X")));
assert_eq!(variable_name("Variable_123 Rest"), Ok((" Rest", "Variable_123")));
assert!(variable_name("0 Rest").is_err());
assert!(variable_name("123_Asd Rest").is_err());
assert!(variable_name("x Rest").is_err());
assert!(variable_name("variable_123 Rest").is_err());
assert!(variable_name("_ Rest").is_err());
assert!(variable_name("_variable_123 Rest").is_err());
assert!(variable_name("(X").is_err());
assert!(variable_name(")X").is_err());
assert!(variable_name(">X").is_err());
assert!(variable_name("<X").is_err());
assert!(variable_name("=X").is_err());
assert!(variable_name(",X").is_err());
assert!(variable_name("+X").is_err());
assert!(variable_name("-X").is_err());
assert!(variable_name("*X").is_err());
assert!(variable_name("/X").is_err());
assert!(variable_name("%X").is_err());
assert!(variable_name("|X").is_err());
assert!(variable_name("#inf").is_err());
assert!(variable_name("#sup").is_err());
assert!(variable_name("#X").is_err());
assert!(variable_name(" ").is_err());
}
}

File diff suppressed because it is too large Load Diff

View File

@@ -1,641 +0,0 @@
fn substring_offset(substring: &str, string: &str) -> usize
{
substring.as_ptr() as usize - string.as_ptr() as usize
}
pub fn trim_start(mut input: &str) -> &str
{
loop
{
let original_input = input;
input = input.trim_start();
let mut input_characters = input.chars();
if let Some('#') = input_characters.next()
{
input = input_characters.as_str();
match (input.find('\n'), input.find('\r'))
{
(Some(newline_index), Some(carriage_return_index)) =>
{
let split_index = std::cmp::min(newline_index, carriage_return_index);
input = input.split_at(split_index).1;
},
(Some(split_index), _)
| (_, Some(split_index)) => input = input.split_at(split_index).1,
_ => input = &input[..input.len()],
}
}
if input.is_empty() || input == original_input
{
break;
}
}
input
}
#[derive(Clone, Copy, Eq, PartialEq)]
pub(crate) enum Keyword
{
And,
Exists,
False,
ForAll,
Infimum,
Not,
Or,
Supremum,
True,
}
impl std::fmt::Debug for Keyword
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match &self
{
Self::And => write!(formatter, "and"),
Self::Exists => write!(formatter, "exists"),
Self::False => write!(formatter, "false"),
Self::ForAll => write!(formatter, "forall"),
Self::Infimum => write!(formatter, "inf"),
Self::Not => write!(formatter, "not"),
Self::Or => write!(formatter, "or"),
Self::Supremum => write!(formatter, "sup"),
Self::True => write!(formatter, "true"),
}
}
}
#[derive(Clone, Copy, Eq, PartialEq)]
pub(crate) enum Symbol
{
ArrowLeft,
ArrowLeftAndRight,
ArrowRight,
Comma,
Division,
Equal,
Exponentiation,
Greater,
GreaterOrEqual,
Less,
LessOrEqual,
Minus,
Multiplication,
NotEqual,
Percent,
Plus,
VerticalBar,
}
impl std::fmt::Debug for Symbol
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match &self
{
Self::ArrowLeft => write!(formatter, "<-"),
Self::ArrowLeftAndRight => write!(formatter, "<->"),
Self::ArrowRight => write!(formatter, "->"),
Self::Comma => write!(formatter, ","),
Self::Division => write!(formatter, "/"),
Self::Equal => write!(formatter, "="),
Self::Exponentiation => write!(formatter, "**"),
Self::Greater => write!(formatter, ">"),
Self::GreaterOrEqual => write!(formatter, ">="),
Self::Less => write!(formatter, "<"),
Self::LessOrEqual => write!(formatter, "<="),
Self::Minus => write!(formatter, "-"),
Self::Multiplication => write!(formatter, "*"),
Self::NotEqual => write!(formatter, "!="),
Self::Percent => write!(formatter, "%"),
Self::Plus => write!(formatter, "+"),
Self::VerticalBar => write!(formatter, "|"),
}
}
}
#[derive(Clone, Copy, Eq, PartialEq)]
pub(crate) enum Token<'i>
{
Identifier(&'i str),
Number(usize),
ParenthesizedExpression(&'i str),
Symbol(Symbol),
}
fn is_identifier_start_character(character: char) -> bool
{
character.is_ascii_alphabetic()
}
fn is_identifier_body_character(character: char) -> bool
{
match character
{
'_' => true,
_ if character.is_ascii_alphanumeric() => true,
_ => false,
}
}
pub fn identifier(input: &str) -> Option<(&str, &str)>
{
let mut characters = input.char_indices();
let first_character = loop
{
match characters.next()
{
Some((_, '_')) => continue,
Some((_, character)) => break Some(character),
None => break None,
}
}?;
if !is_identifier_start_character(first_character)
{
return None;
}
loop
{
match characters.next()
{
None => return Some((input, characters.as_str())),
Some((character_index, character)) =>
{
if !is_identifier_body_character(character)
{
return Some(input.split_at(character_index));
}
},
}
}
}
pub(crate) fn is_keyword(identifier: &str) -> bool
{
match identifier
{
"and"
| "exists"
| "false"
| "forall"
| "inf"
| "not"
| "or"
| "sup"
| "true" => true,
_ => false,
}
}
fn number_string(input: &str) -> Option<(&str, &str)>
{
let mut characters = input.char_indices();
let (_, character) = match characters.next()
{
Some(characters_next) => characters_next,
None => return None,
};
if !character.is_ascii_digit()
{
return None;
}
loop
{
match characters.next()
{
None => return Some((input, characters.as_str())),
Some((character_index, character)) =>
{
if !character.is_ascii_digit()
{
return Some(input.split_at(character_index));
}
},
}
}
}
pub fn number(input: &str) -> Result<Option<(usize, &str)>, crate::parse::Error>
{
let (number_string, remaining_input) = match number_string(input)
{
Some(number_string) => number_string,
None => return Ok(None),
};
let number = number_string.parse()
.map_err(|error| crate::parse::Error::new_parse_number(input,
crate::parse::error::Location::new(0, Some(0)), error))?;
Ok(Some((number, remaining_input)))
}
pub(crate) fn symbol(input: &str) -> Option<(Symbol, &str)>
{
let mut characters = input.char_indices();
let (_, character) = match characters.next()
{
Some(characters_next) => characters_next,
None => return None,
};
let remaining_input = characters.as_str();
match character
{
',' => Some((Symbol::Comma, remaining_input)),
// <->, <-, <=, <
'=' => Some((Symbol::Equal, remaining_input)),
// !=
'!' => match characters.next()
{
Some((_, '=')) => Some((Symbol::NotEqual, characters.as_str())),
_ => None,
},
'<' => match characters.next()
{
Some((_, '-')) =>
{
let remaining_input = characters.as_str();
match characters.next()
{
Some((_, '>')) => Some((Symbol::ArrowLeftAndRight, characters.as_str())),
_ => Some((Symbol::ArrowLeft, remaining_input)),
}
},
Some((_, '=')) => Some((Symbol::LessOrEqual, characters.as_str())),
_ => Some((Symbol::Less, remaining_input)),
},
// >=, >
'>' => match characters.next()
{
Some((_, '=')) => Some((Symbol::GreaterOrEqual, characters.as_str())),
_ => Some((Symbol::Greater, remaining_input)),
},
'+' => Some((Symbol::Plus, remaining_input)),
// ->, -
'-' => match characters.next()
{
Some((_, '>')) => Some((Symbol::ArrowRight, characters.as_str())),
_ => Some((Symbol::Minus, remaining_input)),
},
// **, *
'*' => match characters.next()
{
Some((_, '*')) => Some((Symbol::Exponentiation, characters.as_str())),
_ => Some((Symbol::Multiplication, remaining_input)),
},
'/' => Some((Symbol::Division, remaining_input)),
'%' => Some((Symbol::Percent, remaining_input)),
'|' => Some((Symbol::VerticalBar, remaining_input)),
_ => None,
}
}
pub(crate) fn parenthesized_expression(input: &str)
-> Result<Option<(&str, &str)>, crate::parse::Error>
{
let mut characters = input.chars();
let (first_character, remaining_input) = match characters.next()
{
Some(first_character) => (first_character, characters.as_str()),
None => return Ok(None),
};
if first_character != '('
{
return Ok(None);
}
let mut characters = remaining_input.char_indices();
let mut number_of_open_parentheses = 1;
while let Some((character_index, character)) = characters.next()
{
match character
{
'(' => number_of_open_parentheses += 1,
')' => number_of_open_parentheses -= 1,
_ => (),
}
if number_of_open_parentheses == 0
{
let position_of_closing_parenthesis = character_index;
let (parenthesized_expression, _) =
remaining_input.split_at(position_of_closing_parenthesis);
let remaining_input = characters.as_str();
return Ok(Some((parenthesized_expression, remaining_input)));
}
}
Err(crate::parse::Error::new_unmatched_parenthesis(
crate::parse::error::Location::new(0, Some(1))))
}
pub(crate) struct Tokens<'i, F>
{
original_input: &'i str,
input: &'i str,
previous_index: usize,
reached_end_of_stream: bool,
functor: F,
}
impl<'i> Tokens<'i, ()>
{
pub fn new_iter(input: &'i str) -> Tokens<'i, impl FnMut(Token<'i>) -> Option<Token<'i>>>
{
Tokens::new_filter_map(input, |x| Some(x))
}
pub fn new_filter<P>(input: &'i str, mut predicate: P)
-> Tokens<'i, impl FnMut(Token<'i>) -> Option<Token<'i>>>
where
P: FnMut(&Token<'i>) -> bool,
{
Tokens::new_filter_map(input,
move |x|
{
if predicate(&x)
{
Some(x)
}
else
{
None
}
})
}
}
impl<'i, F> Tokens<'i, F>
{
pub fn new_filter_map(input: &'i str, functor: F) -> Self
{
Self
{
original_input: input,
input,
previous_index: 0,
reached_end_of_stream: false,
functor,
}
}
fn next_token(&mut self) -> Option<Result<(usize, usize, Token<'i>), crate::parse::Error>>
{
self.input = trim_start(self.input);
let index_left = substring_offset(self.input, self.original_input);
let first_character = match self.input.chars().next()
{
None => return None,
Some(first_character) => first_character,
};
if self.input.starts_with(")")
{
return Some(Err(crate::parse::Error::new_unmatched_parenthesis(
crate::parse::error::Location::new(0, Some(1)))));
}
match parenthesized_expression(self.input)
{
Ok(Some((parenthesized_expression, remaining_input))) =>
{
self.input = remaining_input;
let index_right = substring_offset(self.input, self.original_input);
return Some(Ok((index_left, index_right,
Token::ParenthesizedExpression(parenthesized_expression))));
},
Ok(None) => (),
Err(error) => return Some(Err(error)),
}
match number(self.input)
{
Ok(Some((number, remaining_input))) =>
{
self.input = remaining_input;
let index_right = substring_offset(self.input, self.original_input);
return Some(Ok((index_left, index_right, Token::Number(number))));
},
Ok(None) => (),
Err(error) => return Some(Err(error)),
}
if let Some((identifier, remaining_input)) = identifier(self.input)
{
self.input = remaining_input;
let index_right = substring_offset(self.input, self.original_input);
return Some(Ok((index_left, index_right, Token::Identifier(identifier))));
}
if let Some((symbol, remaining_input)) = symbol(self.input)
{
self.input = remaining_input;
let index_right = substring_offset(self.input, self.original_input);
return Some(Ok((index_left, index_right, Token::Symbol(symbol))));
}
return Some(Err(crate::parse::Error::new_character_not_allowed(first_character,
crate::parse::error::Location::new(0, Some(0)))));
}
pub fn remaining_input(&mut self) -> Option<&'i str>
{
if self.reached_end_of_stream
{
return None;
}
let remaining_input = self.original_input[self.previous_index..].trim();
self.reached_end_of_stream = true;
Some(remaining_input)
}
pub fn split(self) -> TokenSplit<Self>
{
TokenSplit::new(self)
}
}
impl<'i, F, G> std::iter::Iterator for Tokens<'i, F>
where
F: FnMut(Token<'i>) -> Option<G>,
{
type Item = Result<(&'i str, G), crate::parse::Error>;
fn next(&mut self) -> Option<Self::Item>
{
if self.previous_index == self.original_input.len()
{
return None;
}
loop
{
match self.next_token()
{
Some(Ok((index_left, index_right, token))) =>
{
let token = match (self.functor)(token)
{
None => continue,
Some(token) => token,
};
let input_left = self.original_input[self.previous_index..index_left].trim();
self.previous_index = index_right;
return Some(Ok((input_left, token)));
},
Some(Err(error)) => return Some(Err(error)),
None => return None,
}
}
}
}
pub(crate) struct TokenSplit<T>
{
tokens: T,
}
impl TokenSplit<()>
{
pub fn new<T>(tokens: T) -> TokenSplit<T>
{
TokenSplit
{
tokens,
}
}
}
impl<'i, F, G> std::iter::Iterator for TokenSplit<Tokens<'i, F>>
where
F: FnMut(Token<'i>) -> Option<G>,
{
type Item = Result<&'i str, crate::parse::Error>;
fn next(&mut self) -> Option<Self::Item>
{
match self.tokens.next()
{
Some(Ok((input_before, _))) => Some(Ok(input_before)),
Some(Err(error)) => Some(Err(error)),
None => match self.tokens.remaining_input()
{
Some(remaining_input) => Some(Ok(remaining_input)),
None => None,
},
}
}
}
#[cfg(test)]
mod tests
{
use super::*;
#[test]
fn tokenize_identifier()
{
assert_eq!(identifier("test").unwrap(), ("test", ""));
assert_eq!(identifier("test2").unwrap(), ("test2", ""));
assert_eq!(identifier("Test").unwrap(), ("Test", ""));
assert_eq!(identifier("Test2").unwrap(), ("Test2", ""));
assert_eq!(identifier("_test").unwrap(), ("_test", ""));
assert_eq!(identifier("_test2").unwrap(), ("_test2", ""));
assert_eq!(identifier("__test").unwrap(), ("__test", ""));
assert_eq!(identifier("__test2").unwrap(), ("__test2", ""));
assert_eq!(identifier("test, test").unwrap(), ("test", ", test"));
assert_eq!(identifier("test2, test").unwrap(), ("test2", ", test"));
assert_eq!(identifier("Test, Test").unwrap(), ("Test", ", Test"));
assert_eq!(identifier("Test2, Test").unwrap(), ("Test2", ", Test"));
assert_eq!(identifier("_test, _test").unwrap(), ("_test", ", _test"));
assert_eq!(identifier("_test2, _test").unwrap(), ("_test2", ", _test"));
assert_eq!(identifier("__test, __test").unwrap(), ("__test", ", __test"));
assert_eq!(identifier("__test2, __test").unwrap(), ("__test2", ", __test"));
assert!(identifier("2test, test").is_none());
assert!(identifier("#test, test").is_none());
assert!(identifier("$test, test").is_none());
assert!(identifier(",test, test").is_none());
}
#[test]
fn tokenize_primitives()
{
assert_eq!(parenthesized_expression("(foo bar baz) test").unwrap(),
Some(("foo bar baz", " test")));
assert!(parenthesized_expression("( | asd#0231(asd|asd) test").is_err());
assert_eq!(parenthesized_expression("( | asd#0231(asd|asd) ) test").unwrap(),
Some((" | asd#0231(asd|asd) ", " test")));
assert_eq!(parenthesized_expression("( | a)sd#0231(asd|asd) test").unwrap(),
Some((" | a", "sd#0231(asd|asd) test")));
assert_eq!(number("1234, ").unwrap(), Some((1234, ", ")));
assert_eq!(number("1234.5, ").unwrap(), Some((1234, ".5, ")));
assert_eq!(number("-1234, ").unwrap(), None);
assert_eq!(number("a1234, ").unwrap(), None);
assert_eq!(symbol("<-"), Some((Symbol::ArrowLeft, "")));
assert_eq!(symbol("<->"), Some((Symbol::ArrowLeftAndRight, "")));
assert_eq!(symbol("->"), Some((Symbol::ArrowRight, "")));
assert_eq!(symbol(","), Some((Symbol::Comma, "")));
assert_eq!(symbol("/"), Some((Symbol::Division, "")));
assert_eq!(symbol("="), Some((Symbol::Equal, "")));
assert_eq!(symbol("**"), Some((Symbol::Exponentiation, "")));
assert_eq!(symbol(">"), Some((Symbol::Greater, "")));
assert_eq!(symbol(">="), Some((Symbol::GreaterOrEqual, "")));
assert_eq!(symbol("<"), Some((Symbol::Less, "")));
assert_eq!(symbol("<="), Some((Symbol::LessOrEqual, "")));
assert_eq!(symbol("-"), Some((Symbol::Minus, "")));
assert_eq!(symbol("*"), Some((Symbol::Multiplication, "")));
assert_eq!(symbol("!="), Some((Symbol::NotEqual, "")));
assert_eq!(symbol("+"), Some((Symbol::Plus, "")));
assert_eq!(symbol("|"), Some((Symbol::VerticalBar, "")));
assert_eq!(symbol("<-a"), Some((Symbol::ArrowLeft, "a")));
assert_eq!(symbol("<->a"), Some((Symbol::ArrowLeftAndRight, "a")));
assert_eq!(symbol("->a"), Some((Symbol::ArrowRight, "a")));
assert_eq!(symbol(",a"), Some((Symbol::Comma, "a")));
assert_eq!(symbol("/a"), Some((Symbol::Division, "a")));
assert_eq!(symbol("=a"), Some((Symbol::Equal, "a")));
assert_eq!(symbol("**a"), Some((Symbol::Exponentiation, "a")));
assert_eq!(symbol(">a"), Some((Symbol::Greater, "a")));
assert_eq!(symbol(">=a"), Some((Symbol::GreaterOrEqual, "a")));
assert_eq!(symbol("<a"), Some((Symbol::Less, "a")));
assert_eq!(symbol("<=a"), Some((Symbol::LessOrEqual, "a")));
assert_eq!(symbol("-a"), Some((Symbol::Minus, "a")));
assert_eq!(symbol("*a"), Some((Symbol::Multiplication, "a")));
assert_eq!(symbol("!=a"), Some((Symbol::NotEqual, "a")));
assert_eq!(symbol("+a"), Some((Symbol::Plus, "a")));
assert_eq!(symbol("|a"), Some((Symbol::VerticalBar, "a")));
}
}

View File

@@ -1,102 +1,72 @@
use crate::flavor::VariableDeclaration as _;
pub struct BoundVariableDeclarations<'p, F>
where
F: crate::flavor::Flavor,
pub struct VariableDeclarationStack
{
pub parent: &'p VariableDeclarationStackLayer<'p, F>,
pub variable_declarations: std::rc::Rc<crate::VariableDeclarations<F>>,
pub free_variable_declarations: crate::VariableDeclarations,
bound_variable_declaration_stack: Vec<std::rc::Rc<crate::VariableDeclarations>>,
}
impl<'p, F> BoundVariableDeclarations<'p, F>
where
F: crate::flavor::Flavor,
impl VariableDeclarationStack
{
pub fn new(parent: &'p VariableDeclarationStackLayer<'p, F>,
variable_declarations: std::rc::Rc<crate::VariableDeclarations<F>>) -> Self
pub fn new() -> Self
{
Self
{
parent,
variable_declarations,
free_variable_declarations: crate::VariableDeclarations::new(),
bound_variable_declaration_stack: vec![],
}
}
}
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
pub fn find(&self, variable_name: &str) -> Option<std::rc::Rc<crate::VariableDeclaration>>
{
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
for variable_declarations in self.bound_variable_declaration_stack.iter().rev()
{
VariableDeclarationStackLayer::Free(free_variable_declarations) =>
if let Some(variable_declaration) = variable_declarations.iter()
.find(|x| x.name == variable_name)
{
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)
},
return Some(std::rc::Rc::clone(&variable_declaration));
}
}
if let Some(variable_declaration) = self.free_variable_declarations.iter()
.find(|x| x.name == variable_name)
{
return Some(std::rc::Rc::clone(&variable_declaration));
}
None
}
pub fn free_variable_declarations_do_mut<F1, F2>(&self, f: F1) -> F2
where
F1: Fn(&mut crate::VariableDeclarations<F>) -> F2,
pub fn find_or_create(&mut self, variable_name: &str) -> std::rc::Rc<crate::VariableDeclaration>
{
match self
if let Some(variable_declaration) = self.find(variable_name)
{
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),
return variable_declaration;
}
let variable_declaration = crate::VariableDeclaration
{
name: variable_name.to_owned(),
};
let variable_declaration = std::rc::Rc::new(variable_declaration);
self.free_variable_declarations.push(std::rc::Rc::clone(&variable_declaration));
variable_declaration
}
pub fn free_variable_declarations_do<F1, F2>(&self, f: F1) -> F2
where
F1: Fn(&crate::VariableDeclarations<F>) -> F2,
pub fn is_empty(&self) -> bool
{
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),
}
self.free_variable_declarations.is_empty()
&& self.bound_variable_declaration_stack.is_empty()
}
pub fn push(&mut self, bound_variable_declarations: std::rc::Rc<crate::VariableDeclarations>)
{
self.bound_variable_declaration_stack.push(bound_variable_declarations);
}
pub fn pop(&mut self) -> Result<(), crate::Error>
{
self.bound_variable_declaration_stack.pop().map(|_| ())
.ok_or_else(|| crate::Error::new_logic("variable stack not in expected state"))
}
}