Compare commits
82 Commits
parser-new
...
parser-old
Author | SHA1 | Date | |
---|---|---|---|
80980e4e11
|
|||
02cf3f552b
|
|||
80636b447a
|
|||
903993dbec
|
|||
f4f8dbf396
|
|||
680f17bda0
|
|||
f949c0f3f8
|
|||
7b2b292727
|
|||
6c326ddb70
|
|||
9754f933ef
|
|||
351d7cdd19
|
|||
3b7394a43e
|
|||
9a8013f1cb
|
|||
51cbdb313f
|
|||
3bd52845be
|
|||
186ed314d3
|
|||
a8df440fdf
|
|||
d051b84845
|
|||
704fe597a2
|
|||
f3b4cdc399
|
|||
21d4b1d605
|
|||
0c132edc07
|
|||
b6308695f6
|
|||
e0dbb8b75f
|
|||
80d7460ec1
|
|||
33f751781e
|
|||
e4700fc638
|
|||
9e74116a4d
|
|||
5512813cba
|
|||
c11156b2ce
|
|||
cc3265fc72
|
|||
121c858bff
|
|||
881419b8ee
|
|||
dc27ab8aeb
|
|||
c8ca7ba337
|
|||
1968ed83ee
|
|||
d1ab7963b1
|
|||
1a497254a8
|
|||
d57b3b3b62
|
|||
57d568916f
|
|||
e4fe047aba
|
|||
600a6a1b4b
|
|||
8bf9d4bd45
|
|||
f82a20e5f1
|
|||
5c51018ab1
|
|||
23e1854346
|
|||
a3da369346
|
|||
caf957deed
|
|||
1ece0e89ef
|
|||
0fdec430af
|
|||
5ea0a96ec4
|
|||
17d8dbd8ba
|
|||
834e59207f
|
|||
257e02f285
|
|||
2e3707e0af
|
|||
d0263dd1c4
|
|||
a7dd4d2fe9
|
|||
c127bc5eea
|
|||
cb616eba87
|
|||
95677bae34
|
|||
3414e8075c
|
|||
675063e1b8
|
|||
7d78a504b1
|
|||
6f86cd40d7
|
|||
29ea4578e4
|
|||
a1bbae9201
|
|||
1c00e5be16
|
|||
1b89d8900e
|
|||
af1ec8a606
|
|||
2907d10148
|
|||
19e70a90c5
|
|||
385c878597
|
|||
5b98e8a29c
|
|||
3530364ea8
|
|||
deae102405
|
|||
0fc8506164
|
|||
e6a5c20d42
|
|||
d5cd179a2d
|
|||
5ec9331b4c
|
|||
896af02120
|
|||
0c057211ed
|
|||
91918cf645
|
@@ -13,4 +13,8 @@ license = "MIT"
|
||||
edition = "2018"
|
||||
|
||||
[dependencies]
|
||||
log = "0.4"
|
||||
nom = {version = "5.1", optional = true}
|
||||
|
||||
[features]
|
||||
default = ["parse"]
|
||||
parse = ["nom"]
|
||||
|
244
src/ast.rs
244
src/ast.rs
@@ -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
69
src/error.rs
Normal 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,
|
||||
}
|
||||
}
|
||||
}
|
@@ -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;
|
||||
}
|
@@ -1,2 +1,2 @@
|
||||
pub mod formulas;
|
||||
pub mod terms;
|
||||
mod formulas;
|
||||
mod terms;
|
||||
|
@@ -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)
|
||||
}
|
||||
|
@@ -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)
|
||||
}
|
||||
|
13
src/lib.rs
13
src/lib.rs
@@ -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;
|
||||
|
148
src/parse.rs
148
src/parse.rs
@@ -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()),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@@ -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 aren’t 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
86
src/parse/helpers.rs
Normal 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
249
src/parse/literals.rs
Normal 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
159
src/parse/names.rs
Normal 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 aren’t 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());
|
||||
}
|
||||
}
|
1385
src/parse/terms.rs
1385
src/parse/terms.rs
File diff suppressed because it is too large
Load Diff
@@ -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")));
|
||||
}
|
||||
}
|
126
src/utils.rs
126
src/utils.rs
@@ -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"))
|
||||
}
|
||||
}
|
||||
|
Reference in New Issue
Block a user