Compare commits
87 Commits
Author | SHA1 | Date | |
---|---|---|---|
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 | |||
fd6ba4a005 | |||
153f77621e | |||
551c35ed75 | |||
549f127729 | |||
a304ec9a75 | |||
a82b4080c8 | |||
90f7be2f33 | |||
a127a053b2 |
32
.github/workflows/main.yml
vendored
Normal file
32
.github/workflows/main.yml
vendored
Normal file
@ -0,0 +1,32 @@
|
||||
name: Rust
|
||||
|
||||
on:
|
||||
push:
|
||||
branches: [master]
|
||||
pull_request:
|
||||
branches: [master]
|
||||
|
||||
jobs:
|
||||
test:
|
||||
name: Test
|
||||
runs-on: ubuntu-latest
|
||||
strategy:
|
||||
matrix:
|
||||
build: [stable, beta, nightly]
|
||||
include:
|
||||
- build: stable
|
||||
rust: stable
|
||||
- build: beta
|
||||
rust: beta
|
||||
- build: nightly
|
||||
rust: nightly
|
||||
|
||||
steps:
|
||||
- uses: actions/checkout@v2
|
||||
- name: Install Rust (rustup)
|
||||
run: rustup update ${{ matrix.rust }} --no-self-update && rustup default ${{ matrix.rust }}
|
||||
shell: bash
|
||||
- name: Build
|
||||
run: cargo build --verbose
|
||||
- name: Run tests
|
||||
run: cargo test --verbose
|
@ -11,3 +11,10 @@ keywords = ["logic"]
|
||||
categories = ["data-structures", "science"]
|
||||
license = "MIT"
|
||||
edition = "2018"
|
||||
|
||||
[dependencies]
|
||||
nom = {version = "5.1", optional = true}
|
||||
|
||||
[features]
|
||||
default = ["parse"]
|
||||
parse = ["nom"]
|
||||
|
95
src/ast.rs
95
src/ast.rs
@ -1,5 +1,6 @@
|
||||
// Operators
|
||||
|
||||
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub enum BinaryOperator
|
||||
{
|
||||
Add,
|
||||
@ -10,6 +11,7 @@ pub enum BinaryOperator
|
||||
Exponentiate,
|
||||
}
|
||||
|
||||
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub enum ComparisonOperator
|
||||
{
|
||||
Greater,
|
||||
@ -20,12 +22,22 @@ pub enum ComparisonOperator
|
||||
Equal,
|
||||
}
|
||||
|
||||
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub enum UnaryOperator
|
||||
{
|
||||
AbsoluteValue,
|
||||
Negative,
|
||||
}
|
||||
|
||||
// ImplicationDirection
|
||||
|
||||
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub enum ImplicationDirection
|
||||
{
|
||||
LeftToRight,
|
||||
RightToLeft,
|
||||
}
|
||||
|
||||
// Primitives
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
@ -115,6 +127,17 @@ impl std::cmp::Ord for VariableDeclaration
|
||||
}
|
||||
}
|
||||
|
||||
impl std::hash::Hash for VariableDeclaration
|
||||
{
|
||||
#[inline(always)]
|
||||
fn hash<H: std::hash::Hasher>(&self, state: &mut H)
|
||||
{
|
||||
let p = self as *const VariableDeclaration;
|
||||
|
||||
p.hash(state);
|
||||
}
|
||||
}
|
||||
|
||||
impl VariableDeclaration
|
||||
{
|
||||
pub fn new(name: String) -> Self
|
||||
@ -130,6 +153,7 @@ pub type VariableDeclarations = Vec<std::rc::Rc<VariableDeclaration>>;
|
||||
|
||||
// Terms
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub struct BinaryOperation
|
||||
{
|
||||
pub operator: BinaryOperator,
|
||||
@ -150,6 +174,7 @@ impl BinaryOperation
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub struct Function
|
||||
{
|
||||
pub declaration: std::rc::Rc<FunctionDeclaration>,
|
||||
@ -158,25 +183,27 @@ pub struct Function
|
||||
|
||||
impl Function
|
||||
{
|
||||
pub fn new(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
|
||||
pub fn new(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>) -> Self
|
||||
{
|
||||
assert_eq!(declaration.arity, arguments.len(),
|
||||
"function has a different number of arguments then declared");
|
||||
|
||||
Self
|
||||
{
|
||||
declaration: std::rc::Rc::clone(declaration),
|
||||
declaration,
|
||||
arguments,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, Copy, Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub enum SpecialInteger
|
||||
{
|
||||
Infimum,
|
||||
Supremum,
|
||||
}
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub struct UnaryOperation
|
||||
{
|
||||
pub operator: UnaryOperator,
|
||||
@ -195,6 +222,7 @@ impl UnaryOperation
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub struct Variable
|
||||
{
|
||||
pub declaration: std::rc::Rc<VariableDeclaration>,
|
||||
@ -202,17 +230,18 @@ pub struct Variable
|
||||
|
||||
impl Variable
|
||||
{
|
||||
pub fn new(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
|
||||
pub fn new(declaration: std::rc::Rc<VariableDeclaration>) -> Self
|
||||
{
|
||||
Self
|
||||
{
|
||||
declaration: std::rc::Rc::clone(declaration),
|
||||
declaration,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Formulas
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub struct Compare
|
||||
{
|
||||
pub operator: ComparisonOperator,
|
||||
@ -233,6 +262,7 @@ impl Compare
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub struct Exists
|
||||
{
|
||||
pub parameters: std::rc::Rc<VariableDeclarations>,
|
||||
@ -251,6 +281,7 @@ impl Exists
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub struct ForAll
|
||||
{
|
||||
pub parameters: std::rc::Rc<VariableDeclarations>,
|
||||
@ -269,42 +300,29 @@ impl ForAll
|
||||
}
|
||||
}
|
||||
|
||||
pub struct IfAndOnlyIf
|
||||
{
|
||||
pub left: Box<Formula>,
|
||||
pub right: Box<Formula>,
|
||||
}
|
||||
|
||||
impl IfAndOnlyIf
|
||||
{
|
||||
pub fn new(left: Box<Formula>, right: Box<Formula>) -> Self
|
||||
{
|
||||
Self
|
||||
{
|
||||
left,
|
||||
right,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub struct Implies
|
||||
{
|
||||
pub direction: ImplicationDirection,
|
||||
pub antecedent: Box<Formula>,
|
||||
pub implication: Box<Formula>,
|
||||
}
|
||||
|
||||
impl Implies
|
||||
{
|
||||
pub fn new(antecedent: Box<Formula>, implication: Box<Formula>) -> Self
|
||||
pub fn new(direction: ImplicationDirection, antecedent: Box<Formula>, implication: Box<Formula>)
|
||||
-> Self
|
||||
{
|
||||
Self
|
||||
{
|
||||
direction,
|
||||
antecedent,
|
||||
implication,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub struct Predicate
|
||||
{
|
||||
pub declaration: std::rc::Rc<PredicateDeclaration>,
|
||||
@ -313,14 +331,14 @@ pub struct Predicate
|
||||
|
||||
impl Predicate
|
||||
{
|
||||
pub fn new(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
|
||||
pub fn new(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>) -> Self
|
||||
{
|
||||
assert_eq!(declaration.arity, arguments.len(),
|
||||
"predicate has a different number of arguments then declared");
|
||||
|
||||
Self
|
||||
{
|
||||
declaration: std::rc::Rc::clone(declaration),
|
||||
declaration,
|
||||
arguments,
|
||||
}
|
||||
}
|
||||
@ -328,6 +346,7 @@ impl Predicate
|
||||
|
||||
// Variants
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub enum Term
|
||||
{
|
||||
BinaryOperation(BinaryOperation),
|
||||
@ -379,7 +398,7 @@ impl Term
|
||||
Self::boolean(false)
|
||||
}
|
||||
|
||||
pub fn function(declaration: &std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>)
|
||||
pub fn function(declaration: std::rc::Rc<FunctionDeclaration>, arguments: Vec<Box<Term>>)
|
||||
-> Self
|
||||
{
|
||||
Self::Function(Function::new(declaration, arguments))
|
||||
@ -440,12 +459,13 @@ impl Term
|
||||
Self::UnaryOperation(UnaryOperation::new(operator, argument))
|
||||
}
|
||||
|
||||
pub fn variable(declaration: &std::rc::Rc<VariableDeclaration>) -> Self
|
||||
pub fn variable(declaration: std::rc::Rc<VariableDeclaration>) -> Self
|
||||
{
|
||||
Self::Variable(Variable::new(declaration))
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Eq, Hash, Ord, PartialEq, PartialOrd)]
|
||||
pub enum Formula
|
||||
{
|
||||
And(Formulas),
|
||||
@ -453,7 +473,7 @@ pub enum Formula
|
||||
Compare(Compare),
|
||||
Exists(Exists),
|
||||
ForAll(ForAll),
|
||||
IfAndOnlyIf(IfAndOnlyIf),
|
||||
IfAndOnlyIf(Formulas),
|
||||
Implies(Implies),
|
||||
Not(Box<Formula>),
|
||||
Or(Formulas),
|
||||
@ -466,8 +486,6 @@ impl Formula
|
||||
{
|
||||
pub fn and(arguments: Formulas) -> Self
|
||||
{
|
||||
assert!(!arguments.is_empty());
|
||||
|
||||
Self::And(arguments)
|
||||
}
|
||||
|
||||
@ -483,8 +501,6 @@ impl Formula
|
||||
|
||||
pub fn exists(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
|
||||
{
|
||||
assert!(!parameters.is_empty());
|
||||
|
||||
Self::Exists(Exists::new(parameters, argument))
|
||||
}
|
||||
|
||||
@ -500,8 +516,6 @@ impl Formula
|
||||
|
||||
pub fn for_all(parameters: std::rc::Rc<VariableDeclarations>, argument: Box<Formula>) -> Self
|
||||
{
|
||||
assert!(!parameters.is_empty());
|
||||
|
||||
Self::ForAll(ForAll::new(parameters, argument))
|
||||
}
|
||||
|
||||
@ -515,14 +529,15 @@ impl Formula
|
||||
Self::compare(ComparisonOperator::GreaterOrEqual, left, right)
|
||||
}
|
||||
|
||||
pub fn if_and_only_if(left: Box<Formula>, right: Box<Formula>) -> Self
|
||||
pub fn if_and_only_if(arguments: Formulas) -> Self
|
||||
{
|
||||
Self::IfAndOnlyIf(IfAndOnlyIf::new(left, right))
|
||||
Self::IfAndOnlyIf(arguments)
|
||||
}
|
||||
|
||||
pub fn implies(antecedent: Box<Formula>, consequent: Box<Formula>) -> Self
|
||||
pub fn implies(direction: ImplicationDirection, antecedent: Box<Formula>,
|
||||
consequent: Box<Formula>) -> Self
|
||||
{
|
||||
Self::Implies(Implies::new(antecedent, consequent))
|
||||
Self::Implies(Implies::new(direction, antecedent, consequent))
|
||||
}
|
||||
|
||||
pub fn less(left: Box<Term>, right: Box<Term>) -> Self
|
||||
@ -547,12 +562,10 @@ impl Formula
|
||||
|
||||
pub fn or(arguments: Formulas) -> Self
|
||||
{
|
||||
assert!(!arguments.is_empty());
|
||||
|
||||
Self::Or(arguments)
|
||||
}
|
||||
|
||||
pub fn predicate(declaration: &std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>)
|
||||
pub fn predicate(declaration: std::rc::Rc<PredicateDeclaration>, arguments: Vec<Box<Term>>)
|
||||
-> Self
|
||||
{
|
||||
Self::Predicate(Predicate::new(declaration, arguments))
|
||||
|
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,
|
||||
}
|
||||
}
|
||||
}
|
452
src/format.rs
452
src/format.rs
@ -1,450 +1,2 @@
|
||||
trait Precedence
|
||||
{
|
||||
fn precedence(&self) -> i32;
|
||||
}
|
||||
|
||||
impl Precedence for crate::Term
|
||||
{
|
||||
fn precedence(&self) -> i32
|
||||
{
|
||||
match &self
|
||||
{
|
||||
Self::Boolean(_)
|
||||
| Self::Function(_)
|
||||
| Self::SpecialInteger(_)
|
||||
| Self::Integer(_)
|
||||
| Self::String(_)
|
||||
| Self::Variable(_)
|
||||
=> 0,
|
||||
Self::UnaryOperation(
|
||||
crate::UnaryOperation{operator: crate::UnaryOperator::Negative, ..})
|
||||
=> 1,
|
||||
Self::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, ..})
|
||||
=> 2,
|
||||
Self::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, ..})
|
||||
| Self::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Divide, ..})
|
||||
| Self::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, ..})
|
||||
=> 3,
|
||||
Self::BinaryOperation(crate::BinaryOperation{operator: crate::BinaryOperator::Add, ..})
|
||||
| Self::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, ..})
|
||||
=> 4,
|
||||
Self::UnaryOperation(
|
||||
crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, ..})
|
||||
=> 5,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Precedence for crate::Formula
|
||||
{
|
||||
fn precedence(&self) -> i32
|
||||
{
|
||||
match &self
|
||||
{
|
||||
Self::Predicate(_)
|
||||
| Self::Boolean(_)
|
||||
| Self::Compare(_)
|
||||
=> 0,
|
||||
Self::Exists(_)
|
||||
| Self::ForAll(_)
|
||||
=> 1,
|
||||
Self::Not(_)
|
||||
=> 2,
|
||||
Self::And(_)
|
||||
=> 3,
|
||||
Self::Or(_)
|
||||
=> 4,
|
||||
Self::Implies(_)
|
||||
=> 5,
|
||||
Self::IfAndOnlyIf(_)
|
||||
=> 6,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Debug for crate::SpecialInteger
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
match &self
|
||||
{
|
||||
crate::SpecialInteger::Infimum => write!(format, "#inf"),
|
||||
crate::SpecialInteger::Supremum => write!(format, "#sup"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Display for crate::SpecialInteger
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{:?}", &self)
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Debug for crate::FunctionDeclaration
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{}/{}", &self.name, self.arity)
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Display for crate::FunctionDeclaration
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{:?}", &self)
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Debug for crate::PredicateDeclaration
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{}/{}", &self.name, self.arity)
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Display for crate::PredicateDeclaration
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{:?}", &self)
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Debug for crate::VariableDeclaration
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{}", &self.name)
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Display for crate::VariableDeclaration
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{:?}", &self)
|
||||
}
|
||||
}
|
||||
|
||||
struct TermDisplay<'term>
|
||||
{
|
||||
parent_precedence: Option<i32>,
|
||||
term: &'term crate::Term,
|
||||
}
|
||||
|
||||
fn display_term(term: &crate::Term, parent_precedence: Option<i32>) -> TermDisplay
|
||||
{
|
||||
TermDisplay
|
||||
{
|
||||
parent_precedence,
|
||||
term,
|
||||
}
|
||||
}
|
||||
|
||||
impl<'term> std::fmt::Debug for TermDisplay<'term>
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
let precedence = self.term.precedence();
|
||||
let requires_parentheses = match self.parent_precedence
|
||||
{
|
||||
Some(parent_precedence) => precedence > parent_precedence,
|
||||
None => false,
|
||||
};
|
||||
let precedence = Some(precedence);
|
||||
|
||||
if requires_parentheses
|
||||
{
|
||||
write!(format, "(")?;
|
||||
}
|
||||
|
||||
match &self.term
|
||||
{
|
||||
crate::Term::Boolean(true) => write!(format, "true"),
|
||||
crate::Term::Boolean(false) => write!(format, "false"),
|
||||
crate::Term::SpecialInteger(value) => write!(format, "{:?}", value),
|
||||
crate::Term::Integer(value) => write!(format, "{}", value),
|
||||
crate::Term::String(value) => write!(format, "\"{}\"", value),
|
||||
crate::Term::Variable(variable) => write!(format, "{:?}", variable.declaration),
|
||||
crate::Term::Function(function) =>
|
||||
{
|
||||
write!(format, "{}", function.declaration.name)?;
|
||||
|
||||
assert!(function.declaration.arity == function.arguments.len(),
|
||||
"number of function arguments differs from declaration (expected {}, got {})",
|
||||
function.declaration.arity, function.arguments.len());
|
||||
|
||||
if !function.arguments.is_empty()
|
||||
{
|
||||
write!(format, "(")?;
|
||||
|
||||
let mut separator = "";
|
||||
|
||||
for argument in &function.arguments
|
||||
{
|
||||
write!(format, "{}{:?}", separator, display_term(&argument, None))?;
|
||||
|
||||
separator = ", ";
|
||||
}
|
||||
|
||||
write!(format, ")")?;
|
||||
}
|
||||
|
||||
Ok(())
|
||||
},
|
||||
crate::Term::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Add, left, right})
|
||||
=> write!(format, "{:?} + {:?}", display_term(left, precedence),
|
||||
display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Subtract, left, right})
|
||||
=> write!(format, "{:?} - {:?}", display_term(left, precedence),
|
||||
display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Multiply, left, right})
|
||||
=> write!(format, "{:?} * {:?}", display_term(left, precedence),
|
||||
display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Divide, left, right})
|
||||
=> write!(format, "{:?} / {:?}", display_term(left, precedence),
|
||||
display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Modulo, left, right})
|
||||
=> write!(format, "{:?} % {:?}", display_term(left, precedence),
|
||||
display_term(right, precedence)),
|
||||
crate::Term::BinaryOperation(
|
||||
crate::BinaryOperation{operator: crate::BinaryOperator::Exponentiate, left, right})
|
||||
=> write!(format, "{:?} ** {:?}", display_term(left, precedence),
|
||||
display_term(right, precedence)),
|
||||
crate::Term::UnaryOperation(
|
||||
crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
|
||||
=> write!(format, "-{:?}", display_term(argument, precedence)),
|
||||
crate::Term::UnaryOperation(
|
||||
crate::UnaryOperation{operator: crate::UnaryOperator::AbsoluteValue, argument})
|
||||
=> write!(format, "|{:?}|", display_term(argument, precedence)),
|
||||
}?;
|
||||
|
||||
if requires_parentheses
|
||||
{
|
||||
write!(format, ")")?;
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl<'term> std::fmt::Display for TermDisplay<'term>
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{:?}", self)
|
||||
}
|
||||
}
|
||||
|
||||
struct FormulaDisplay<'formula>
|
||||
{
|
||||
parent_precedence: Option<i32>,
|
||||
formula: &'formula crate::Formula,
|
||||
}
|
||||
|
||||
fn display_formula(formula: &crate::Formula, parent_precedence: Option<i32>) -> FormulaDisplay
|
||||
{
|
||||
FormulaDisplay
|
||||
{
|
||||
parent_precedence,
|
||||
formula,
|
||||
}
|
||||
}
|
||||
|
||||
impl<'formula> std::fmt::Debug for FormulaDisplay<'formula>
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
let precedence = self.formula.precedence();
|
||||
let requires_parentheses = match self.parent_precedence
|
||||
{
|
||||
Some(parent_precedence) => precedence > parent_precedence,
|
||||
None => false,
|
||||
};
|
||||
let precedence = Some(precedence);
|
||||
|
||||
if requires_parentheses
|
||||
{
|
||||
write!(format, "(")?;
|
||||
}
|
||||
|
||||
match &self.formula
|
||||
{
|
||||
crate::Formula::Exists(exists) =>
|
||||
{
|
||||
assert!(!exists.parameters.is_empty());
|
||||
|
||||
write!(format, "exists")?;
|
||||
|
||||
let mut separator = " ";
|
||||
|
||||
for parameter in exists.parameters.iter()
|
||||
{
|
||||
write!(format, "{}{:?}", separator, parameter)?;
|
||||
|
||||
separator = ", "
|
||||
}
|
||||
|
||||
write!(format, " {:?}", display_formula(&exists.argument, precedence))?;
|
||||
},
|
||||
crate::Formula::ForAll(for_all) =>
|
||||
{
|
||||
assert!(!for_all.parameters.is_empty());
|
||||
|
||||
write!(format, "forall")?;
|
||||
|
||||
let mut separator = " ";
|
||||
|
||||
for parameter in for_all.parameters.iter()
|
||||
{
|
||||
write!(format, "{}{:?}", separator, parameter)?;
|
||||
|
||||
separator = ", "
|
||||
}
|
||||
|
||||
write!(format, " {:?}", display_formula(&for_all.argument, precedence))?;
|
||||
},
|
||||
crate::Formula::Not(argument) => write!(format, "not {:?}",
|
||||
display_formula(argument, precedence))?,
|
||||
crate::Formula::And(arguments) =>
|
||||
{
|
||||
let mut separator = "";
|
||||
|
||||
assert!(!arguments.is_empty());
|
||||
|
||||
for argument in arguments
|
||||
{
|
||||
write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
|
||||
|
||||
separator = " and "
|
||||
}
|
||||
},
|
||||
crate::Formula::Or(arguments) =>
|
||||
{
|
||||
let mut separator = "";
|
||||
|
||||
assert!(!arguments.is_empty());
|
||||
|
||||
for argument in arguments
|
||||
{
|
||||
write!(format, "{}{:?}", separator, display_formula(argument, precedence))?;
|
||||
|
||||
separator = " or "
|
||||
}
|
||||
},
|
||||
crate::Formula::Implies(crate::Implies{antecedent, implication})
|
||||
=> write!(format, "{:?} -> {:?}", display_formula(antecedent, precedence),
|
||||
display_formula(implication, precedence))?,
|
||||
crate::Formula::IfAndOnlyIf(crate::IfAndOnlyIf{left, right})
|
||||
=> write!(format, "{:?} <-> {:?}", display_formula(left, precedence),
|
||||
display_formula(right, precedence))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::Less, left, right})
|
||||
=> write!(format, "{:?} < {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::LessOrEqual, left, right})
|
||||
=> write!(format, "{:?} <= {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::Greater, left, right})
|
||||
=> write!(format, "{:?} > {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::GreaterOrEqual, left, right})
|
||||
=> write!(format, "{:?} >= {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::Equal, left, right})
|
||||
=> write!(format, "{:?} = {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Compare(
|
||||
crate::Compare{operator: crate::ComparisonOperator::NotEqual, left, right})
|
||||
=> write!(format, "{:?} != {:?}", display_term(left, None),
|
||||
display_term(right, None))?,
|
||||
crate::Formula::Boolean(true) => write!(format, "#true")?,
|
||||
crate::Formula::Boolean(false) => write!(format, "#false")?,
|
||||
crate::Formula::Predicate(predicate) =>
|
||||
{
|
||||
write!(format, "{}", predicate.declaration.name)?;
|
||||
|
||||
if !predicate.arguments.is_empty()
|
||||
{
|
||||
write!(format, "(")?;
|
||||
|
||||
let mut separator = "";
|
||||
|
||||
for argument in &predicate.arguments
|
||||
{
|
||||
write!(format, "{}{:?}", separator, display_term(argument, None))?;
|
||||
|
||||
separator = ", "
|
||||
}
|
||||
|
||||
write!(format, ")")?;
|
||||
}
|
||||
},
|
||||
}
|
||||
|
||||
if requires_parentheses
|
||||
{
|
||||
write!(format, ")")?;
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl<'formula> std::fmt::Display for FormulaDisplay<'formula>
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{:?}", self)
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Debug for crate::Formula
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{:?}", display_formula(&self, None))
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Display for crate::Formula
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{}", display_formula(&self, None))
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Debug for crate::Term
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{:?}", display_term(&self, None))
|
||||
}
|
||||
}
|
||||
|
||||
impl std::fmt::Display for crate::Term
|
||||
{
|
||||
fn fmt(&self, format: &mut std::fmt::Formatter) -> std::fmt::Result
|
||||
{
|
||||
write!(format, "{}", display_term(&self, None))
|
||||
}
|
||||
}
|
||||
mod formulas;
|
||||
mod terms;
|
||||
|
1236
src/format/formulas.rs
Normal file
1236
src/format/formulas.rs
Normal file
File diff suppressed because it is too large
Load Diff
1088
src/format/terms.rs
Normal file
1088
src/format/terms.rs
Normal file
File diff suppressed because it is too large
Load Diff
@ -1,4 +1,10 @@
|
||||
mod ast;
|
||||
mod error;
|
||||
pub mod format;
|
||||
#[cfg(feature = "parse")]
|
||||
pub mod parse;
|
||||
mod utils;
|
||||
|
||||
pub use ast::*;
|
||||
pub use error::Error;
|
||||
pub use utils::VariableDeclarationStack;
|
||||
|
32
src/parse.rs
Normal file
32
src/parse.rs
Normal file
@ -0,0 +1,32 @@
|
||||
mod formulas;
|
||||
mod helpers;
|
||||
mod literals;
|
||||
mod names;
|
||||
mod terms;
|
||||
|
||||
pub(crate) use helpers::word_boundary;
|
||||
pub(crate) use literals::{boolean, integer, special_integer, string};
|
||||
pub(crate) use names::{function_or_predicate_name, variable_name};
|
||||
pub use terms::term;
|
||||
pub use formulas::formula;
|
||||
|
||||
pub struct Declarations
|
||||
{
|
||||
function_declarations: std::cell::RefCell<crate::FunctionDeclarations>,
|
||||
predicate_declarations: std::cell::RefCell<crate::PredicateDeclarations>,
|
||||
variable_declaration_stack: std::cell::RefCell<crate::VariableDeclarationStack>,
|
||||
}
|
||||
|
||||
impl Declarations
|
||||
{
|
||||
pub fn new() -> Self
|
||||
{
|
||||
Self
|
||||
{
|
||||
function_declarations: std::cell::RefCell::new(crate::FunctionDeclarations::new()),
|
||||
predicate_declarations: std::cell::RefCell::new(crate::PredicateDeclarations::new()),
|
||||
variable_declaration_stack:
|
||||
std::cell::RefCell::new(crate::VariableDeclarationStack::new()),
|
||||
}
|
||||
}
|
||||
}
|
686
src/parse/formulas.rs
Normal file
686
src/parse/formulas.rs
Normal file
@ -0,0 +1,686 @@
|
||||
use nom::
|
||||
{
|
||||
IResult,
|
||||
branch::alt,
|
||||
bytes::complete::tag,
|
||||
character::complete::multispace0,
|
||||
combinator::{cut, map, map_res},
|
||||
multi::{many1, separated_list},
|
||||
sequence::{delimited, pair, preceded, terminated, tuple},
|
||||
};
|
||||
|
||||
use super::{Declarations, boolean, word_boundary};
|
||||
|
||||
pub fn predicate<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Predicate>
|
||||
{
|
||||
map
|
||||
(
|
||||
|i| crate::parse::terms::function_or_predicate(i, d),
|
||||
|(name, arguments)|
|
||||
{
|
||||
let arguments = match arguments
|
||||
{
|
||||
Some(arguments) => arguments,
|
||||
None => vec![],
|
||||
};
|
||||
|
||||
let mut predicate_declarations = d.predicate_declarations.borrow_mut();
|
||||
|
||||
let declaration = match predicate_declarations.iter()
|
||||
.find(|x| x.name == name && x.arity == arguments.len())
|
||||
{
|
||||
Some(declaration) => std::rc::Rc::clone(&declaration),
|
||||
None =>
|
||||
{
|
||||
let declaration = crate::PredicateDeclaration
|
||||
{
|
||||
name: name.to_string(),
|
||||
arity: arguments.len(),
|
||||
};
|
||||
let declaration = std::rc::Rc::new(declaration);
|
||||
|
||||
predicate_declarations.insert(std::rc::Rc::clone(&declaration));
|
||||
|
||||
declaration
|
||||
},
|
||||
};
|
||||
|
||||
crate::Predicate::new(declaration, arguments)
|
||||
},
|
||||
)(i)
|
||||
}
|
||||
|
||||
fn not<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
|
||||
{
|
||||
map
|
||||
(
|
||||
preceded
|
||||
(
|
||||
terminated
|
||||
(
|
||||
tag("not"),
|
||||
multispace0,
|
||||
),
|
||||
|i| formula_precedence_2(i, d),
|
||||
),
|
||||
|x| crate::Formula::not(Box::new(x)),
|
||||
)(i)
|
||||
}
|
||||
|
||||
fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
|
||||
{
|
||||
map_res
|
||||
(
|
||||
separated_list
|
||||
(
|
||||
delimited
|
||||
(
|
||||
multispace0,
|
||||
terminated
|
||||
(
|
||||
tag("and"),
|
||||
word_boundary,
|
||||
),
|
||||
multispace0,
|
||||
),
|
||||
|i| formula_precedence_2(i, d),
|
||||
),
|
||||
|arguments| -> Result<_, (_, _)>
|
||||
{
|
||||
if arguments.len() >= 2
|
||||
{
|
||||
Ok(arguments.into_iter().map(Box::new).collect())
|
||||
}
|
||||
else
|
||||
{
|
||||
Err(nom::error::make_error(i, nom::error::ErrorKind::Many1))
|
||||
}
|
||||
}
|
||||
)(i)
|
||||
}
|
||||
|
||||
fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
|
||||
{
|
||||
map_res
|
||||
(
|
||||
separated_list
|
||||
(
|
||||
delimited
|
||||
(
|
||||
multispace0,
|
||||
terminated
|
||||
(
|
||||
tag("or"),
|
||||
word_boundary,
|
||||
),
|
||||
multispace0,
|
||||
),
|
||||
|i| formula_precedence_3(i, d),
|
||||
),
|
||||
|arguments| -> Result<_, (_, _)>
|
||||
{
|
||||
if arguments.len() >= 2
|
||||
{
|
||||
Ok(arguments.into_iter().map(Box::new).collect())
|
||||
}
|
||||
else
|
||||
{
|
||||
Err(nom::error::make_error(i, nom::error::ErrorKind::Many1))
|
||||
}
|
||||
}
|
||||
)(i)
|
||||
}
|
||||
|
||||
fn implies_left_to_right<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
|
||||
{
|
||||
map
|
||||
(
|
||||
pair
|
||||
(
|
||||
many1
|
||||
(
|
||||
terminated
|
||||
(
|
||||
|i| formula_precedence_4(i, d),
|
||||
delimited
|
||||
(
|
||||
multispace0,
|
||||
tag("->"),
|
||||
multispace0,
|
||||
),
|
||||
)
|
||||
),
|
||||
|i| formula_precedence_4(i, d),
|
||||
),
|
||||
|(arguments, last_argument)| arguments.into_iter().rev().fold(last_argument,
|
||||
|accumulator, argument|
|
||||
crate::Formula::implies(crate::ImplicationDirection::LeftToRight,
|
||||
Box::new(argument), Box::new(accumulator)))
|
||||
)(i)
|
||||
}
|
||||
|
||||
fn implies_right_to_left<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
|
||||
{
|
||||
map
|
||||
(
|
||||
pair
|
||||
(
|
||||
|i| formula_precedence_4(i, d),
|
||||
many1
|
||||
(
|
||||
preceded
|
||||
(
|
||||
delimited
|
||||
(
|
||||
multispace0,
|
||||
tag("<-"),
|
||||
multispace0,
|
||||
),
|
||||
|i| formula_precedence_4(i, d),
|
||||
)
|
||||
),
|
||||
),
|
||||
|(first_argument, arguments)| arguments.into_iter().fold(first_argument,
|
||||
|accumulator, argument|
|
||||
crate::Formula::implies(crate::ImplicationDirection::RightToLeft,
|
||||
Box::new(argument), Box::new(accumulator)))
|
||||
)(i)
|
||||
}
|
||||
|
||||
fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, Vec<Box<crate::Formula>>>
|
||||
{
|
||||
map_res
|
||||
(
|
||||
separated_list
|
||||
(
|
||||
delimited
|
||||
(
|
||||
multispace0,
|
||||
tag("<->"),
|
||||
multispace0,
|
||||
),
|
||||
|i| formula_precedence_5(i, d),
|
||||
),
|
||||
|arguments| -> Result<_, (_, _)>
|
||||
{
|
||||
if arguments.len() >= 2
|
||||
{
|
||||
Ok(arguments.into_iter().map(Box::new).collect())
|
||||
}
|
||||
else
|
||||
{
|
||||
Err(nom::error::make_error(i, nom::error::ErrorKind::Many1))
|
||||
}
|
||||
}
|
||||
)(i)
|
||||
}
|
||||
|
||||
fn quantified_expression<'a, 'b, T, N>(i: &'a str, d: &Declarations, keyword: &'b str,
|
||||
new_functor: N)
|
||||
-> IResult<&'a str, T>
|
||||
where
|
||||
N: Fn(std::rc::Rc<crate::VariableDeclarations>, Box<crate::Formula>) -> T
|
||||
{
|
||||
preceded
|
||||
(
|
||||
terminated
|
||||
(
|
||||
tag(keyword),
|
||||
word_boundary,
|
||||
),
|
||||
cut
|
||||
(
|
||||
|i| -> IResult<&'a str, T>
|
||||
{
|
||||
let (i, variable_declarations) =
|
||||
map
|
||||
(
|
||||
delimited
|
||||
(
|
||||
multispace0,
|
||||
separated_list
|
||||
(
|
||||
delimited
|
||||
(
|
||||
multispace0,
|
||||
tag(","),
|
||||
multispace0,
|
||||
),
|
||||
map
|
||||
(
|
||||
crate::parse::terms::variable_declaration,
|
||||
std::rc::Rc::new,
|
||||
),
|
||||
),
|
||||
multispace0,
|
||||
),
|
||||
std::rc::Rc::new,
|
||||
)(i)?;
|
||||
|
||||
if variable_declarations.is_empty()
|
||||
{
|
||||
return Err(nom::Err::Failure((i, nom::error::ErrorKind::Many1)));
|
||||
}
|
||||
|
||||
d.variable_declaration_stack.borrow_mut().push(std::rc::Rc::clone(&variable_declarations));
|
||||
|
||||
let (i, argument) = formula_precedence_0(i, d)?;
|
||||
|
||||
// TODO: report logic errors more appropriately
|
||||
d.variable_declaration_stack.borrow_mut().pop()
|
||||
.map_err(|_| nom::Err::Failure((i, nom::error::ErrorKind::Verify)))?;
|
||||
|
||||
Ok((i, new_functor(variable_declarations, Box::new(argument))))
|
||||
}
|
||||
),
|
||||
)(i)
|
||||
}
|
||||
|
||||
fn compare<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Compare>
|
||||
{
|
||||
map
|
||||
(
|
||||
tuple
|
||||
((
|
||||
|i| crate::parse::term(i, d),
|
||||
delimited
|
||||
(
|
||||
multispace0,
|
||||
alt
|
||||
((
|
||||
map
|
||||
(
|
||||
tag(">"),
|
||||
|_| crate::ComparisonOperator::Greater,
|
||||
),
|
||||
map
|
||||
(
|
||||
tag("<"),
|
||||
|_| crate::ComparisonOperator::Less,
|
||||
),
|
||||
map
|
||||
(
|
||||
tag("<="),
|
||||
|_| crate::ComparisonOperator::LessOrEqual,
|
||||
),
|
||||
map
|
||||
(
|
||||
tag(">="),
|
||||
|_| crate::ComparisonOperator::GreaterOrEqual,
|
||||
),
|
||||
map
|
||||
(
|
||||
tag("!="),
|
||||
|_| crate::ComparisonOperator::NotEqual,
|
||||
),
|
||||
map
|
||||
(
|
||||
tag("="),
|
||||
|_| crate::ComparisonOperator::Equal,
|
||||
),
|
||||
)),
|
||||
multispace0,
|
||||
),
|
||||
|i| crate::parse::term(i, d),
|
||||
)),
|
||||
|(left, operator, right)|
|
||||
{
|
||||
crate::Compare::new(operator, Box::new(left), Box::new(right))
|
||||
}
|
||||
)(i)
|
||||
}
|
||||
|
||||
fn exists<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Exists>
|
||||
{
|
||||
quantified_expression::<crate::Exists, _>(i, d, "exists", crate::Exists::new)
|
||||
}
|
||||
|
||||
fn for_all<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::ForAll>
|
||||
{
|
||||
quantified_expression::<crate::ForAll, _>(i, d, "forall", crate::ForAll::new)
|
||||
}
|
||||
|
||||
fn formula_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
|
||||
{
|
||||
delimited
|
||||
(
|
||||
terminated
|
||||
(
|
||||
tag("("),
|
||||
multispace0,
|
||||
),
|
||||
|i| formula(i, d),
|
||||
preceded
|
||||
(
|
||||
multispace0,
|
||||
tag(")"),
|
||||
),
|
||||
)(i)
|
||||
}
|
||||
|
||||
fn formula_precedence_0<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
|
||||
{
|
||||
alt
|
||||
((
|
||||
map
|
||||
(
|
||||
boolean,
|
||||
crate::Formula::Boolean,
|
||||
),
|
||||
map
|
||||
(
|
||||
|i| predicate(i, d),
|
||||
crate::Formula::Predicate,
|
||||
),
|
||||
map
|
||||
(
|
||||
|i| compare(i, d),
|
||||
crate::Formula::Compare,
|
||||
),
|
||||
|i| formula_parenthesized(i, d),
|
||||
))(i)
|
||||
}
|
||||
|
||||
fn formula_precedence_1<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
|
||||
{
|
||||
alt
|
||||
((
|
||||
map
|
||||
(
|
||||
|i| exists(i, d),
|
||||
crate::Formula::Exists,
|
||||
),
|
||||
map
|
||||
(
|
||||
|i| for_all(i, d),
|
||||
crate::Formula::ForAll,
|
||||
),
|
||||
|i| formula_precedence_0(i, d),
|
||||
))(i)
|
||||
}
|
||||
|
||||
fn formula_precedence_2<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
|
||||
{
|
||||
alt
|
||||
((
|
||||
|i| not(i, d),
|
||||
|i| formula_precedence_1(i, d),
|
||||
))(i)
|
||||
}
|
||||
|
||||
fn formula_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
|
||||
{
|
||||
alt
|
||||
((
|
||||
map
|
||||
(
|
||||
|i| and(i, d),
|
||||
crate::Formula::And,
|
||||
),
|
||||
|i| formula_precedence_2(i, d),
|
||||
))(i)
|
||||
}
|
||||
|
||||
fn formula_precedence_4<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
|
||||
{
|
||||
alt
|
||||
((
|
||||
map
|
||||
(
|
||||
|i| or(i, d),
|
||||
crate::Formula::Or,
|
||||
),
|
||||
|i| formula_precedence_3(i, d),
|
||||
))(i)
|
||||
}
|
||||
|
||||
fn formula_precedence_5<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
|
||||
{
|
||||
alt
|
||||
((
|
||||
|i| implies_left_to_right(i, d),
|
||||
|i| implies_right_to_left(i, d),
|
||||
|i| formula_precedence_4(i, d),
|
||||
))(i)
|
||||
}
|
||||
|
||||
fn formula_precedence_6<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
|
||||
{
|
||||
alt
|
||||
((
|
||||
map
|
||||
(
|
||||
|i| if_and_only_if(i, d),
|
||||
crate::Formula::IfAndOnlyIf,
|
||||
),
|
||||
|i| formula_precedence_5(i, d),
|
||||
))(i)
|
||||
}
|
||||
|
||||
pub fn formula<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
|
||||
{
|
||||
formula_precedence_6(i, d)
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests
|
||||
{
|
||||
use crate::parse::formulas::*;
|
||||
use crate::parse::formulas as original;
|
||||
use crate::{Formula, Term};
|
||||
|
||||
fn formula(i: &str) -> Formula
|
||||
{
|
||||
original::formula(i, &Declarations::new()).unwrap().1
|
||||
}
|
||||
|
||||
fn formula_remainder(i: &str) -> &str
|
||||
{
|
||||
original::formula(i, &Declarations::new()).unwrap().0
|
||||
}
|
||||
|
||||
fn format_formula(i: &str) -> String
|
||||
{
|
||||
format!("{}", formula(i))
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_boolean()
|
||||
{
|
||||
assert_eq!(formula("true"), Formula::true_());
|
||||
assert_eq!(formula("false"), Formula::false_());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_precedence()
|
||||
{
|
||||
assert_eq!(format_formula("a -> b -> c <-> d -> e -> f"), "a -> b -> c <-> d -> e -> f");
|
||||
assert_eq!(format_formula("(a -> b -> c) <-> (d -> e -> f)"), "a -> b -> c <-> d -> e -> f");
|
||||
assert_eq!(format_formula("a <- b <- c <-> d <- e <- f"), "a <- b <- c <-> d <- e <- f");
|
||||
assert_eq!(format_formula("(a <- b <- c) <-> (d <- e <- f)"), "a <- b <- c <-> d <- e <- f");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_exists()
|
||||
{
|
||||
let formula_as_exists = |i| match formula(i)
|
||||
{
|
||||
Formula::Exists(exists) => exists,
|
||||
_ => panic!("expected existentially quantified formula"),
|
||||
};
|
||||
|
||||
let as_predicate = |x| match x
|
||||
{
|
||||
Formula::Predicate(arguments) => arguments,
|
||||
_ => panic!("expected predicate"),
|
||||
};
|
||||
|
||||
assert_eq!(format_formula("exists X , Y , Z ( p )"), "exists X, Y, Z p");
|
||||
assert_eq!(formula_as_exists("exists X , Y , Z ( p )").parameters.len(), 3);
|
||||
assert_eq!(as_predicate(*formula_as_exists("exists X , Y , Z ( p )").argument)
|
||||
.declaration.name, "p");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_and()
|
||||
{
|
||||
let formula_as_and = |i| match formula(i)
|
||||
{
|
||||
Formula::And(arguments) => arguments,
|
||||
_ => panic!("expected conjunction"),
|
||||
};
|
||||
|
||||
let as_predicate = |x| match x
|
||||
{
|
||||
Formula::Predicate(arguments) => arguments,
|
||||
_ => panic!("expected predicate"),
|
||||
};
|
||||
|
||||
assert_eq!(format_formula("(true and false)"), "true and false");
|
||||
assert_eq!(formula_as_and("(true and false)").len(), 2);
|
||||
assert_eq!(*formula_as_and("(true and false)").remove(0), Formula::true_());
|
||||
assert_eq!(*formula_as_and("(true and false)").remove(1), Formula::false_());
|
||||
// The order of elements is retained
|
||||
assert_ne!(formula("(true and false)"), formula("false and true"));
|
||||
assert_eq!(format_formula("(p and q and r and s)"), "p and q and r and s");
|
||||
assert_eq!(
|
||||
as_predicate(*formula_as_and("(p and q and r and s)").remove(0)).declaration.name, "p");
|
||||
assert_eq!(
|
||||
as_predicate(*formula_as_and("(p and q and r and s)").remove(3)).declaration.name, "s");
|
||||
|
||||
let formula = |i| original::formula(i, &Declarations::new());
|
||||
|
||||
// Malformed formulas shouldn’t be accepted
|
||||
assert!(formula("and").is_err());
|
||||
assert!(formula("and p").is_err());
|
||||
assert_eq!(formula_remainder("p and"), " and");
|
||||
assert_eq!(formula_remainder("p andq"), " andq");
|
||||
assert_eq!(formula_remainder("p and q and"), " and");
|
||||
assert_eq!(formula_remainder("p and q andq"), " andq");
|
||||
assert!(formula("(p and) q").is_err());
|
||||
assert_eq!(formula_remainder("p (and q)"), " (and q)");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_or()
|
||||
{
|
||||
let formula_as_or = |i| match formula(i)
|
||||
{
|
||||
Formula::Or(arguments) => arguments,
|
||||
_ => panic!("expected disjunction"),
|
||||
};
|
||||
|
||||
let as_predicate = |x| match x
|
||||
{
|
||||
Formula::Predicate(arguments) => arguments,
|
||||
_ => panic!("expected predicate"),
|
||||
};
|
||||
|
||||
assert_eq!(format_formula("(true or false)"), "true or false");
|
||||
assert_eq!(formula_as_or("(true or false)").len(), 2);
|
||||
assert_eq!(*formula_as_or("(true or false)").remove(0), Formula::true_());
|
||||
assert_eq!(*formula_as_or("(true or false)").remove(1), Formula::false_());
|
||||
// The order of elements is retained
|
||||
assert_ne!(formula("(true or false)"), formula("false or true)"));
|
||||
assert_eq!(format_formula("(p or q or r or s)"), "p or q or r or s");
|
||||
assert_eq!(
|
||||
as_predicate(*formula_as_or("(p or q or r or s)").remove(0)).declaration.name, "p");
|
||||
assert_eq!(
|
||||
as_predicate(*formula_as_or("(p or q or r or s)").remove(3)).declaration.name, "s");
|
||||
|
||||
let formula = |i| original::formula(i, &Declarations::new());
|
||||
|
||||
// Malformed formulas shouldn’t be accepted
|
||||
assert!(formula("or").is_err());
|
||||
assert!(formula("or p").is_err());
|
||||
assert_eq!(formula_remainder("p or"), " or");
|
||||
assert_eq!(formula_remainder("p orq"), " orq");
|
||||
assert_eq!(formula_remainder("p or q or"), " or");
|
||||
assert_eq!(formula_remainder("p or q orq"), " orq");
|
||||
assert!(formula("(p or) q").is_err());
|
||||
assert_eq!(formula_remainder("p (or q)"), " (or q)");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_implies()
|
||||
{
|
||||
let formula_as_implies = |i| match formula(i)
|
||||
{
|
||||
Formula::Implies(implies) => implies,
|
||||
_ => panic!("expected implication"),
|
||||
};
|
||||
|
||||
let as_predicate = |x| match x
|
||||
{
|
||||
Formula::Predicate(arguments) => arguments,
|
||||
_ => panic!("expected predicate"),
|
||||
};
|
||||
|
||||
assert_eq!(as_predicate(*formula_as_implies("a -> b").antecedent).declaration.name, "a");
|
||||
assert_eq!(as_predicate(*formula_as_implies("a -> b").implication).declaration.name, "b");
|
||||
assert_eq!(formula_as_implies("a -> b").direction,
|
||||
crate::ImplicationDirection::LeftToRight);
|
||||
|
||||
assert_eq!(as_predicate(*formula_as_implies("a <- b").antecedent).declaration.name, "b");
|
||||
assert_eq!(as_predicate(*formula_as_implies("a <- b").implication).declaration.name, "a");
|
||||
assert_eq!(formula_as_implies("a <- b").direction,
|
||||
crate::ImplicationDirection::RightToLeft);
|
||||
|
||||
assert_eq!(format_formula("(a -> b -> c)"), "a -> b -> c");
|
||||
assert_eq!(format_formula("(a -> (b -> c))"), "a -> b -> c");
|
||||
assert_eq!(format_formula("((a -> b) -> c)"), "(a -> b) -> c");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_predicate()
|
||||
{
|
||||
let predicate = |i| original::predicate(i, &Declarations::new()).unwrap().1;
|
||||
let predicate_remainder = |i| original::predicate(i, &Declarations::new()).unwrap().0;
|
||||
|
||||
assert_eq!(predicate("s").declaration.name, "s");
|
||||
assert_eq!(predicate("s").declaration.arity, 0);
|
||||
assert_eq!(predicate_remainder("s"), "");
|
||||
assert_eq!(predicate("s ( )").declaration.name, "s");
|
||||
assert_eq!(predicate("s ( )").declaration.arity, 0);
|
||||
assert_eq!(predicate_remainder("s ( )"), "");
|
||||
assert_eq!(predicate("s ( 1 , 2 , 3 )").declaration.name, "s");
|
||||
assert_eq!(predicate("s ( 1 , 2 , 3 )").declaration.arity, 3);
|
||||
assert_eq!(*predicate("s ( 1 , 2 , 3 )").arguments.remove(0), Term::integer(1));
|
||||
assert_eq!(*predicate("s ( 1 , 2 , 3 )").arguments.remove(1), Term::integer(2));
|
||||
assert_eq!(*predicate("s ( 1 , 2 , 3 )").arguments.remove(2), Term::integer(3));
|
||||
assert_eq!(predicate_remainder("s ( 1 , 2 , 3 )"), "");
|
||||
assert_eq!(predicate_remainder("s ( 1 , 2 , 3 )"), "");
|
||||
assert_eq!(predicate("s ( ), rest").declaration.name, "s");
|
||||
assert_eq!(predicate("s ( ), rest").declaration.arity, 0);
|
||||
assert_eq!(predicate_remainder("s ( ), rest"), ", rest");
|
||||
assert_eq!(predicate("s ( 1 , 2 , 3 ), rest").declaration.name, "s");
|
||||
assert_eq!(predicate("s ( 1 , 2 , 3 ), rest").declaration.arity, 3);
|
||||
assert_eq!(predicate_remainder("s ( 1 , 2 , 3 ), rest"), ", rest");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_exists_primitive()
|
||||
{
|
||||
assert_eq!(exists("exists X (p(X, Y, X, Y)), rest", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.parameters.len())),
|
||||
Ok((", rest", 1)));
|
||||
assert_eq!(exists("exists X p(X, Y, X, Y), rest", &Declarations::new())
|
||||
.map(|(i, x)| (i, x.parameters.len())),
|
||||
Ok((", rest", 1)));
|
||||
assert!(exists("exists (p(X, Y, X, Y)), rest", &Declarations::new()).is_err());
|
||||
assert!(exists("exists X, rest", &Declarations::new()).is_err());
|
||||
assert!(exists("exists X (), rest", &Declarations::new()).is_err());
|
||||
assert!(exists("exists X (, true), rest", &Declarations::new()).is_err());
|
||||
assert!(exists("exists X (true, ), rest", &Declarations::new()).is_err());
|
||||
assert!(exists("exists X (true false), rest", &Declarations::new()).is_err());
|
||||
assert!(exists("exists X (true), rest", &Declarations::new()).is_ok());
|
||||
assert!(exists("exists X p(X), rest", &Declarations::new()).is_ok());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_formula()
|
||||
{
|
||||
// TODO: refactor
|
||||
formula("exists X, Y (p(X, Y, X, Y) and X < Y and q(X) <-> r(X)), rest");
|
||||
}
|
||||
}
|
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());
|
||||
}
|
||||
}
|
856
src/parse/terms.rs
Normal file
856
src/parse/terms.rs
Normal file
@ -0,0 +1,856 @@
|
||||
use nom::
|
||||
{
|
||||
IResult,
|
||||
branch::alt,
|
||||
bytes::complete::tag,
|
||||
character::complete::multispace0,
|
||||
combinator::{map, opt},
|
||||
multi::{many1, separated_list},
|
||||
sequence::{delimited, pair, preceded, terminated},
|
||||
};
|
||||
|
||||
use super::{Declarations, boolean, function_or_predicate_name, integer, special_integer, string,
|
||||
variable_name};
|
||||
|
||||
fn negative<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Term>
|
||||
{
|
||||
map
|
||||
(
|
||||
preceded
|
||||
(
|
||||
terminated
|
||||
(
|
||||
tag("-"),
|
||||
multispace0,
|
||||
),
|
||||
|i| term_precedence_1(i, d),
|
||||
),
|
||||
|x| match x
|
||||
{
|
||||
crate::Term::Integer(value) => crate::Term::integer(-value),
|
||||
crate::Term::UnaryOperation(
|
||||
crate::UnaryOperation{operator: crate::UnaryOperator::Negative, argument})
|
||||
=> *argument,
|
||||
_ => crate::Term::negative(Box::new(x)),
|
||||
}
|
||||
)(i)
|
||||
}
|
||||
|
||||
fn absolute_value<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Term>
|
||||
{
|
||||
map
|
||||
(
|
||||
delimited
|
||||
(
|
||||
terminated
|
||||
(
|
||||
tag("|"),
|
||||
multispace0,
|
||||
),
|
||||
|i| term(i, d),
|
||||
preceded
|
||||
(
|
||||
multispace0,
|
||||
tag("|"),
|
||||
),
|
||||
),
|
||||
|x| crate::Term::absolute_value(Box::new(x)),
|
||||
)(i)
|
||||
}
|
||||
|
||||
pub(crate) fn function_or_predicate<'i>(i: &'i str, d: &Declarations)
|
||||
-> IResult<&'i str, (&'i str, Option<Vec<Box<crate::Term>>>)>
|
||||
{
|
||||
pair
|
||||
(
|
||||
function_or_predicate_name,
|
||||
opt
|
||||
(
|
||||
delimited
|
||||
(
|
||||
delimited
|
||||
(
|
||||
multispace0,
|
||||
tag("("),
|
||||
multispace0,
|
||||
),
|
||||
separated_list
|
||||
(
|
||||
delimited
|
||||
(
|
||||
multispace0,
|
||||
tag(","),
|
||||
multispace0,
|
||||
),
|
||||
map
|
||||
(
|
||||
|i| term(i, d),
|
||||
Box::new,
|
||||
),
|
||||
),
|
||||
preceded
|
||||
(
|
||||
multispace0,
|
||||
tag(")"),
|
||||
),
|
||||
)
|
||||
),
|
||||
)(i)
|
||||
}
|
||||
|
||||
pub fn function<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Function>
|
||||
{
|
||||
map
|
||||
(
|
||||
|i| function_or_predicate(i, d),
|
||||
|(name, arguments)|
|
||||
{
|
||||
let arguments = match arguments
|
||||
{
|
||||
Some(arguments) => arguments,
|
||||
None => vec![],
|
||||
};
|
||||
|
||||
let mut function_declarations = d.function_declarations.borrow_mut();
|
||||
|
||||
let declaration = match function_declarations.iter()
|
||||
.find(|x| x.name == name && x.arity == arguments.len())
|
||||
{
|
||||
Some(declaration) => std::rc::Rc::clone(&declaration),
|
||||
None =>
|
||||
{
|
||||
let declaration = crate::FunctionDeclaration
|
||||
{
|
||||
name: name.to_string(),
|
||||
arity: arguments.len(),
|
||||
};
|
||||
let declaration = std::rc::Rc::new(declaration);
|
||||
|
||||
function_declarations.insert(std::rc::Rc::clone(&declaration));
|
||||
|
||||
declaration
|
||||
},
|
||||
};
|
||||
|
||||
crate::Function::new(declaration, arguments)
|
||||
},
|
||||
)(i)
|
||||
}
|
||||
|
||||
pub fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDeclaration>
|
||||
{
|
||||
map
|
||||
(
|
||||
variable_name,
|
||||
|name| crate::VariableDeclaration::new(name.to_string())
|
||||
)(i)
|
||||
}
|
||||
|
||||
pub fn variable<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Variable>
|
||||
{
|
||||
map
|
||||
(
|
||||
variable_name,
|
||||
|name|
|
||||
{
|
||||
let mut variable_declaration_stack = d.variable_declaration_stack.borrow_mut();
|
||||
|
||||
let declaration = variable_declaration_stack.find_or_create(name);
|
||||
|
||||
crate::Variable::new(declaration)
|
||||
},
|
||||
)(i)
|
||||
}
|
||||
|
||||
fn term_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
||||
{
|
||||
delimited
|
||||
(
|
||||
terminated
|
||||
(
|
||||
tag("("),
|
||||
multispace0,
|
||||
),
|
||||
|i| term(i, d),
|
||||
preceded
|
||||
(
|
||||
multispace0,
|
||||
tag(")"),
|
||||
),
|
||||
)(i)
|
||||
}
|
||||
|
||||
fn term_precedence_0<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
||||
{
|
||||
alt
|
||||
((
|
||||
map
|
||||
(
|
||||
boolean,
|
||||
crate::Term::Boolean,
|
||||
),
|
||||
map
|
||||
(
|
||||
special_integer,
|
||||
crate::Term::SpecialInteger,
|
||||
),
|
||||
map
|
||||
(
|
||||
integer,
|
||||
crate::Term::Integer,
|
||||
),
|
||||
map
|
||||
(
|
||||
|i| function(i, d),
|
||||
crate::Term::Function,
|
||||
),
|
||||
map
|
||||
(
|
||||
string,
|
||||
crate::Term::String,
|
||||
),
|
||||
map
|
||||
(
|
||||
|i| variable(i, d),
|
||||
crate::Term::Variable,
|
||||
),
|
||||
|i| absolute_value(i, d),
|
||||
|i| term_parenthesized(i, d),
|
||||
))(i)
|
||||
}
|
||||
|
||||
fn term_precedence_1<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
||||
{
|
||||
alt
|
||||
((
|
||||
|i| negative(i, d),
|
||||
|i| term_precedence_0(i, d),
|
||||
))(i)
|
||||
}
|
||||
|
||||
fn term_precedence_2<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
||||
{
|
||||
alt
|
||||
((
|
||||
map
|
||||
(
|
||||
pair
|
||||
(
|
||||
many1
|
||||
(
|
||||
terminated
|
||||
(
|
||||
|i| term_precedence_1(i, d),
|
||||
delimited
|
||||
(
|
||||
multispace0,
|
||||
tag("**"),
|
||||
multispace0,
|
||||
),
|
||||
)
|
||||
),
|
||||
|i| term_precedence_1(i, d),
|
||||
),
|
||||
|(arguments, last_argument)| arguments.into_iter().rev().fold(last_argument,
|
||||
|accumulator, argument|
|
||||
crate::Term::exponentiate(Box::new(argument), Box::new(accumulator))),
|
||||
),
|
||||
|i| term_precedence_1(i, d),
|
||||
))(i)
|
||||
}
|
||||
|
||||
fn term_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
||||
{
|
||||
alt
|
||||
((
|
||||
map
|
||||
(
|
||||
pair
|
||||
(
|
||||
|i| term_precedence_2(i, d),
|
||||
many1
|
||||
(
|
||||
pair
|
||||
(
|
||||
delimited
|
||||
(
|
||||
multispace0,
|
||||
alt
|
||||
((
|
||||
tag("*"),
|
||||
tag("/"),
|
||||
tag("%"),
|
||||
)),
|
||||
multispace0,
|
||||
),
|
||||
|i| term_precedence_2(i, d),
|
||||
)
|
||||
),
|
||||
),
|
||||
|(first_argument, arguments)| arguments.into_iter().fold(first_argument,
|
||||
|accumulator, (operator, argument)|
|
||||
match operator
|
||||
{
|
||||
"*" => crate::Term::multiply(Box::new(accumulator), Box::new(argument)),
|
||||
"/" => crate::Term::divide(Box::new(accumulator), Box::new(argument)),
|
||||
"%" => crate::Term::modulo(Box::new(accumulator), Box::new(argument)),
|
||||
// TODO: handle appropriately
|
||||
_ => panic!("test"),
|
||||
})
|
||||
),
|
||||
|i| term_precedence_2(i, d),
|
||||
))(i)
|
||||
}
|
||||
|
||||
fn term_precedence_4<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
||||
{
|
||||
alt
|
||||
((
|
||||
map
|
||||
(
|
||||
pair
|
||||
(
|
||||
|i| term_precedence_3(i, d),
|
||||
many1
|
||||
(
|
||||
pair
|
||||
(
|
||||
delimited
|
||||
(
|
||||
multispace0,
|
||||
alt
|
||||
((
|
||||
tag("+"),
|
||||
tag("-"),
|
||||
)),
|
||||
multispace0,
|
||||
),
|
||||
|i| term_precedence_3(i, d),
|
||||
)
|
||||
),
|
||||
),
|
||||
|(first_argument, arguments)| arguments.into_iter().fold(first_argument,
|
||||
|accumulator, (operator, argument)|
|
||||
match operator
|
||||
{
|
||||
"+" => crate::Term::add(Box::new(accumulator), Box::new(argument)),
|
||||
"-" => crate::Term::subtract(Box::new(accumulator), Box::new(argument)),
|
||||
// TODO: handle appropriately
|
||||
_ => panic!("test"),
|
||||
})
|
||||
),
|
||||
|i| term_precedence_3(i, d),
|
||||
))(i)
|
||||
}
|
||||
|
||||
pub fn term<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
|
||||
{
|
||||
term_precedence_4(i, d)
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests
|
||||
{
|
||||
use crate::parse::terms::*;
|
||||
use crate::parse::terms as original;
|
||||
use crate::{Term, VariableDeclaration, VariableDeclarationStack};
|
||||
|
||||
fn term(i: &str) -> Term
|
||||
{
|
||||
original::term(i, &Declarations::new()).unwrap().1
|
||||
}
|
||||
|
||||
fn format_term(i: &str) -> String
|
||||
{
|
||||
format!("{}", term(i))
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_parenthesized()
|
||||
{
|
||||
assert_eq!(format_term("(1)"), format_term("1"));
|
||||
assert_eq!(format_term("((1))"), format_term("1"));
|
||||
assert_eq!(format_term("(-1)"), format_term("-1"));
|
||||
assert_eq!(format_term("((-1))"), format_term("-1"));
|
||||
assert_eq!(format_term("(-(1))"), format_term("-1"));
|
||||
assert_eq!(format_term("-((1))"), format_term("-1"));
|
||||
assert_eq!(format_term("(-(-1))"), format_term("1"));
|
||||
assert_eq!(format_term("-((-1))"), format_term("1"));
|
||||
assert_eq!(format_term("-(-(1))"), format_term("1"));
|
||||
assert_eq!(format_term("-(-(-1))"), format_term("-1"));
|
||||
assert_eq!(format_term("(a)"), format_term("a"));
|
||||
assert_eq!(format_term("((a))"), format_term("a"));
|
||||
assert_eq!(format_term("(X)"), format_term("X"));
|
||||
assert_eq!(format_term("((X))"), format_term("X"));
|
||||
assert_eq!(format_term("(\"test\")"), format_term("\"test\""));
|
||||
assert_eq!(format_term("((\"test\"))"), format_term("\"test\""));
|
||||
assert_eq!(format_term("(a ** b)"), format_term("a ** b"));
|
||||
assert_eq!(format_term("(a * b)"), format_term("a * b"));
|
||||
assert_eq!(format_term("(a / b)"), format_term("a / b"));
|
||||
assert_eq!(format_term("(a % b)"), format_term("a % b"));
|
||||
assert_eq!(format_term("(a + b)"), format_term("a + b"));
|
||||
assert_eq!(format_term("(a - b)"), format_term("a - b"));
|
||||
assert_eq!(format_term("((a ** b))"), format_term("a ** b"));
|
||||
assert_eq!(format_term("((a * b))"), format_term("a * b"));
|
||||
assert_eq!(format_term("((a / b))"), format_term("a / b"));
|
||||
assert_eq!(format_term("((a % b))"), format_term("a % b"));
|
||||
assert_eq!(format_term("((a + b))"), format_term("a + b"));
|
||||
assert_eq!(format_term("((a - b))"), format_term("a - b"));
|
||||
assert_eq!(format_term("(f(a, b))"), format_term("f(a, b)"));
|
||||
assert_eq!(format_term("((f(a, b)))"), format_term("f(a, b)"));
|
||||
assert_eq!(format_term("f((a), (b))"), format_term("f(a, b)"));
|
||||
assert_eq!(format_term("f(|-a|)"), format_term("f(|-a|)"));
|
||||
assert_eq!(format_term("f((|-a|))"), format_term("f(|-a|)"));
|
||||
assert_eq!(format_term("f((-a))"), format_term("f(-a)"));
|
||||
assert_eq!(format_term("f(((-a)))"), format_term("f(-a)"));
|
||||
assert_eq!(format_term("f((a ** b))"), format_term("f(a ** b)"));
|
||||
assert_eq!(format_term("f((a * b))"), format_term("f(a * b)"));
|
||||
assert_eq!(format_term("f((a / b))"), format_term("f(a / b)"));
|
||||
assert_eq!(format_term("f((a % b))"), format_term("f(a % b)"));
|
||||
assert_eq!(format_term("f((a + b))"), format_term("f(a + b)"));
|
||||
assert_eq!(format_term("f((a - b))"), format_term("f(a - b)"));
|
||||
assert_eq!(format_term("f(((a ** b)))"), format_term("f(a ** b)"));
|
||||
assert_eq!(format_term("f(((a * b)))"), format_term("f(a * b)"));
|
||||
assert_eq!(format_term("f(((a / b)))"), format_term("f(a / b)"));
|
||||
assert_eq!(format_term("f(((a % b)))"), format_term("f(a % b)"));
|
||||
assert_eq!(format_term("f(((a + b)))"), format_term("f(a + b)"));
|
||||
assert_eq!(format_term("f(((a - b)))"), format_term("f(a - b)"));
|
||||
assert_eq!(format_term("(|a ** b|)"), format_term("|a ** b|"));
|
||||
assert_eq!(format_term("|(a ** b)|"), format_term("|a ** b|"));
|
||||
assert_eq!(format_term("(|(a ** b)|)"), format_term("|a ** b|"));
|
||||
assert_eq!(format_term("(|a * b|)"), format_term("|a * b|"));
|
||||
assert_eq!(format_term("|(a * b)|"), format_term("|a * b|"));
|
||||
assert_eq!(format_term("(|(a * b)|)"), format_term("|a * b|"));
|
||||
assert_eq!(format_term("(|a / b|)"), format_term("|a / b|"));
|
||||
assert_eq!(format_term("|(a / b)|"), format_term("|a / b|"));
|
||||
assert_eq!(format_term("(|(a / b)|)"), format_term("|a / b|"));
|
||||
assert_eq!(format_term("(|a % b|)"), format_term("|a % b|"));
|
||||
assert_eq!(format_term("|(a % b)|"), format_term("|a % b|"));
|
||||
assert_eq!(format_term("(|(a % b)|)"), format_term("|a % b|"));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_boolean()
|
||||
{
|
||||
assert_eq!(term("true"), Term::true_());
|
||||
assert_eq!(term("false"), Term::false_());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_integer()
|
||||
{
|
||||
assert_eq!(term("0"), Term::integer(0));
|
||||
assert_eq!(term("10000"), Term::integer(10000));
|
||||
assert_eq!(term("+10000"), Term::integer(10000));
|
||||
assert_eq!(term("-10000"), Term::integer(-10000));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_special_integer()
|
||||
{
|
||||
assert_eq!(term("#inf"), Term::infimum());
|
||||
assert_eq!(term("#sup"), Term::supremum());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_string()
|
||||
{
|
||||
// TODO: fix
|
||||
//assert_eq!(term("\"\""), Term::string("".to_string()));
|
||||
assert_eq!(term("\"a\""), Term::string("a".to_string()));
|
||||
assert_eq!(term("\"#\""), Term::string("#".to_string()));
|
||||
assert_eq!(term("\" \""), Term::string(" ".to_string()));
|
||||
assert_eq!(term("\" \""), Term::string(" ".to_string()));
|
||||
assert_eq!(term("\"test test\""), Term::string("test test".to_string()));
|
||||
assert_eq!(term("\"123 456\""), Term::string("123 456".to_string()));
|
||||
assert_eq!(term("\"-#? -#?\""), Term::string("-#? -#?".to_string()));
|
||||
assert_eq!(term("\"\\ntest\\n123\\n\""), Term::string("\ntest\n123\n".to_string()));
|
||||
assert_eq!(term("\"\\ttest\\t123\\t\""), Term::string("\ttest\t123\t".to_string()));
|
||||
assert_eq!(term("\"\\\\test\\\\123\\\\\""), Term::string("\\test\\123\\".to_string()));
|
||||
assert_eq!(term("\"🙂test🙂123🙂\""), Term::string("🙂test🙂123🙂".to_string()));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_function()
|
||||
{
|
||||
let term_as_function = |i| match term(i)
|
||||
{
|
||||
Term::Function(function) => function,
|
||||
_ => panic!("expected function"),
|
||||
};
|
||||
|
||||
assert_eq!(term_as_function("s").declaration.name, "s");
|
||||
assert_eq!(term_as_function("s").declaration.arity, 0);
|
||||
assert_eq!(term_as_function("s()").declaration.name, "s");
|
||||
assert_eq!(term_as_function("s").declaration.arity, 0);
|
||||
assert_eq!(term_as_function("s(1, 2, 3)").declaration.name, "s");
|
||||
assert_eq!(term_as_function("s(1, 2, 3)").declaration.arity, 3);
|
||||
assert_eq!(*term_as_function("s(1, 2, 3)").arguments.remove(0), Term::integer(1));
|
||||
assert_eq!(*term_as_function("s(1, 2, 3)").arguments.remove(2), Term::integer(3));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_variable()
|
||||
{
|
||||
let term_as_variable = |i| match term(i)
|
||||
{
|
||||
Term::Variable(variable) => variable,
|
||||
_ => panic!("expected variable"),
|
||||
};
|
||||
|
||||
assert_eq!(term_as_variable("X").declaration.name, "X");
|
||||
assert_eq!(term_as_variable("Variable_123").declaration.name, "Variable_123");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_unary()
|
||||
{
|
||||
assert_eq!(format_term("|a|"), "|a|");
|
||||
assert_eq!(format_term("||a||"), "||a||");
|
||||
assert_eq!(format_term("|a - b|"), "|a - b|");
|
||||
assert_eq!(format_term("|a| - b"), "|a| - b");
|
||||
assert_eq!(format_term("a - |b|"), "a - |b|");
|
||||
assert_eq!(format_term("||a| - b|"), "||a| - b|");
|
||||
assert_eq!(format_term("|a - |b||"), "|a - |b||");
|
||||
assert_eq!(format_term("||a| - |b||"), "||a| - |b||");
|
||||
assert_eq!(format_term("||a| - |b| - |c||"), "||a| - |b| - |c||");
|
||||
assert_eq!(format_term("||a - b| - |c - d||"), "||a - b| - |c - d||");
|
||||
assert_eq!(format_term("-a"), "-a");
|
||||
assert_eq!(format_term("--a"), "a");
|
||||
assert_eq!(format_term("---a"), "-a");
|
||||
assert_eq!(format_term("-(a + b)"), "-(a + b)");
|
||||
assert_eq!(format_term("-|a + b|"), "-|a + b|");
|
||||
assert_eq!(format_term("--|a + b|"), "|a + b|");
|
||||
assert_eq!(format_term("---|a + b|"), "-|a + b|");
|
||||
assert_eq!(term("5"), Term::integer(5));
|
||||
assert_eq!(term("-5"), Term::integer(-5));
|
||||
assert_eq!(term("--5"), Term::integer(5));
|
||||
assert_eq!(term("---5"), Term::integer(-5));
|
||||
assert_eq!(term("0"), Term::integer(0));
|
||||
assert_eq!(term("-0"), Term::integer(0));
|
||||
assert_eq!(term("--0"), Term::integer(0));
|
||||
assert_eq!(term("---0"), Term::integer(0));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_exponentiate()
|
||||
{
|
||||
assert_eq!(term("1 ** (2 ** (3 ** (4 ** 5)))"), term("1 ** 2 ** 3 ** 4 ** 5"));
|
||||
assert_eq!(format_term("1 ** 2 ** 3 ** 4 ** 5"), "1 ** 2 ** 3 ** 4 ** 5");
|
||||
assert_eq!(term("1 ** (2 ** (3 ** (4 ** 5)))"), term("1 ** 2 ** 3 ** 4 ** 5"));
|
||||
// As exponentiation is right-associative, these parentheses cannot be omitted
|
||||
assert_ne!(term("(((1 ** 2) ** 3) ** 4) ** 5"), term("1 ** 2 ** 3 ** 4 ** 5"));
|
||||
assert_eq!(format_term("(((1 ** 2) ** 3) ** 4) ** 5"), "(((1 ** 2) ** 3) ** 4) ** 5");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_multiplicative()
|
||||
{
|
||||
assert_eq!(format_term("(a * b) * (c * d)"), "a * b * c * d");
|
||||
assert_eq!(format_term("(a * b) * (c / d)"), "a * b * c / d");
|
||||
assert_eq!(format_term("(a * b) * (c % d)"), "a * b * (c % d)");
|
||||
assert_eq!(format_term("(a / b) * (c * d)"), "a / b * c * d");
|
||||
assert_eq!(format_term("(a / b) * (c / d)"), "a / b * c / d");
|
||||
assert_eq!(format_term("(a / b) * (c % d)"), "a / b * (c % d)");
|
||||
assert_eq!(format_term("(a % b) * (c * d)"), "a % b * c * d");
|
||||
assert_eq!(format_term("(a % b) * (c / d)"), "a % b * c / d");
|
||||
assert_eq!(format_term("(a % b) * (c % d)"), "a % b * (c % d)");
|
||||
assert_eq!(format_term("(a * b) / (c * d)"), "a * b / (c * d)");
|
||||
assert_eq!(format_term("(a * b) / (c / d)"), "a * b / (c / d)");
|
||||
assert_eq!(format_term("(a * b) / (c % d)"), "a * b / (c % d)");
|
||||
assert_eq!(format_term("(a / b) / (c * d)"), "a / b / (c * d)");
|
||||
assert_eq!(format_term("(a / b) / (c / d)"), "a / b / (c / d)");
|
||||
assert_eq!(format_term("(a / b) / (c % d)"), "a / b / (c % d)");
|
||||
assert_eq!(format_term("(a % b) / (c * d)"), "a % b / (c * d)");
|
||||
assert_eq!(format_term("(a % b) / (c / d)"), "a % b / (c / d)");
|
||||
assert_eq!(format_term("(a % b) / (c % d)"), "a % b / (c % d)");
|
||||
assert_eq!(format_term("(a * b) % (c * d)"), "a * b % (c * d)");
|
||||
assert_eq!(format_term("(a * b) % (c / d)"), "a * b % (c / d)");
|
||||
assert_eq!(format_term("(a * b) % (c % d)"), "a * b % (c % d)");
|
||||
assert_eq!(format_term("(a / b) % (c * d)"), "a / b % (c * d)");
|
||||
assert_eq!(format_term("(a / b) % (c / d)"), "a / b % (c / d)");
|
||||
assert_eq!(format_term("(a / b) % (c % d)"), "a / b % (c % d)");
|
||||
assert_eq!(format_term("(a % b) % (c * d)"), "a % b % (c * d)");
|
||||
assert_eq!(format_term("(a % b) % (c / d)"), "a % b % (c / d)");
|
||||
assert_eq!(format_term("(a % b) % (c % d)"), "a % b % (c % d)");
|
||||
|
||||
// TODO: test malformed expressions
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_additive()
|
||||
{
|
||||
assert_eq!(format_term("(a + b) + (c + d)"), "a + b + c + d");
|
||||
assert_eq!(format_term("(a + b) + (c - d)"), "a + b + c - d");
|
||||
assert_eq!(format_term("(a - b) + (c + d)"), "a - b + c + d");
|
||||
assert_eq!(format_term("(a - b) + (c - d)"), "a - b + c - d");
|
||||
assert_eq!(format_term("(a + b) - (c + d)"), "a + b - (c + d)");
|
||||
assert_eq!(format_term("(a + b) - (c - d)"), "a + b - (c - d)");
|
||||
assert_eq!(format_term("(a - b) - (c + d)"), "a - b - (c + d)");
|
||||
assert_eq!(format_term("(a - b) - (c - d)"), "a - b - (c - d)");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_precedence()
|
||||
{
|
||||
assert_eq!(term("-a + b"), term("(-a) + b"));
|
||||
assert_eq!(term("-a + -b"), term("(-a) + (-b)"));
|
||||
assert_eq!(term("-a + -b"), term("-(a) + -(b)"));
|
||||
assert_eq!(format_term("-(a + b)"), "-(a + b)");
|
||||
assert_eq!(term("-a - b"), term("(-a) - b"));
|
||||
assert_eq!(term("-a - -b"), term("(-a) - (-b)"));
|
||||
assert_eq!(term("-a - -b"), term("-(a) - -(b)"));
|
||||
assert_eq!(term("-a * b"), term("(-a) * b"));
|
||||
assert_eq!(term("-a * -b"), term("(-a) * (-b)"));
|
||||
assert_eq!(term("-a * -b"), term("-(a) * -(b)"));
|
||||
assert_eq!(term("-a / b"), term("(-a) / b"));
|
||||
assert_eq!(term("-a / -b"), term("(-a) / (-b)"));
|
||||
assert_eq!(term("-a / -b"), term("-(a) / -(b)"));
|
||||
assert_eq!(term("-a % b"), term("(-a) % b"));
|
||||
assert_eq!(term("-a % -b"), term("(-a) % (-b)"));
|
||||
assert_eq!(term("-a % -b"), term("-(a) % -(b)"));
|
||||
assert_eq!(term("-a ** b"), term("(-a) ** b"));
|
||||
assert_eq!(term("-a ** -b"), term("(-a) ** (-b)"));
|
||||
assert_eq!(term("-a ** -b"), term("-(a) ** -(b)"));
|
||||
assert_eq!(format_term("-(a + b)"), "-(a + b)");
|
||||
assert_eq!(format_term("-(a + b)"), "-(a + b)");
|
||||
assert_eq!(format_term("-(a + b)"), "-(a + b)");
|
||||
assert_eq!(format_term("-(a + b)"), "-(a + b)");
|
||||
assert_eq!(format_term("-(a + b)"), "-(a + b)");
|
||||
assert_eq!(term("a + (b * c) + d"), term("(a + (b * c)) + d"));
|
||||
assert_eq!(term("a + (b / c) + d"), term("(a + (b / c)) + d"));
|
||||
assert_eq!(term("a + (b % c) + d"), term("(a + (b % c)) + d"));
|
||||
assert_eq!(term("a - (b * c) - d"), term("(a - (b * c)) - d"));
|
||||
assert_eq!(term("a - (b / c) - d"), term("(a - (b / c)) - d"));
|
||||
assert_eq!(term("a - (b % c) - d"), term("(a - (b % c)) - d"));
|
||||
assert_eq!(format_term("(a + b) * (c + d)"), "(a + b) * (c + d)");
|
||||
assert_eq!(format_term("(a + b) / (c + d)"), "(a + b) / (c + d)");
|
||||
assert_eq!(format_term("(a + b) % (c + d)"), "(a + b) % (c + d)");
|
||||
assert_eq!(format_term("(a - b) * (c - d)"), "(a - b) * (c - d)");
|
||||
assert_eq!(format_term("(a - b) / (c - d)"), "(a - b) / (c - d)");
|
||||
assert_eq!(format_term("(a - b) % (c - d)"), "(a - b) % (c - d)");
|
||||
assert_eq!(term("a ** b ** c + d ** e ** f"), term("(a ** b ** c) + (d ** e ** f)"));
|
||||
assert_eq!(term("a ** (b ** c + d) ** e ** f"), term("a ** ((b ** c + d) ** (e ** f))"));
|
||||
assert_eq!(term("a ** b ** (c + d) ** e ** f"), term("a ** (b ** ((c + d) ** (e ** f)))"));
|
||||
assert_eq!(term("a ** b ** (c + d ** e) ** f"), term("a ** (b ** ((c + d ** e) ** f))"));
|
||||
assert_eq!(term("a ** b ** c - d ** e ** f"), term("(a ** b ** c) - (d ** e ** f)"));
|
||||
assert_eq!(term("a ** (b ** c - d) ** e ** f"), term("a ** ((b ** c - d) ** (e ** f))"));
|
||||
assert_eq!(term("a ** b ** (c - d) ** e ** f"), term("a ** (b ** ((c - d) ** (e ** f)))"));
|
||||
assert_eq!(term("a ** b ** (c - d ** e) ** f"), term("a ** (b ** ((c - d ** e) ** f))"));
|
||||
assert_eq!(term("a ** b ** c * d ** e ** f"), term("(a ** b ** c) * (d ** e ** f)"));
|
||||
assert_eq!(term("a ** (b ** c * d) ** e ** f"), term("a ** ((b ** c * d) ** (e ** f))"));
|
||||
assert_eq!(term("a ** b ** (c * d) ** e ** f"), term("a ** (b ** ((c * d) ** (e ** f)))"));
|
||||
assert_eq!(term("a ** b ** (c * d ** e) ** f"), term("a ** (b ** ((c * d ** e) ** f))"));
|
||||
assert_eq!(term("a ** b ** c / d ** e ** f"), term("(a ** b ** c) / (d ** e ** f)"));
|
||||
assert_eq!(term("a ** (b ** c / d) ** e ** f"), term("a ** ((b ** c / d) ** (e ** f))"));
|
||||
assert_eq!(term("a ** b ** (c / d) ** e ** f"), term("a ** (b ** ((c / d) ** (e ** f)))"));
|
||||
assert_eq!(term("a ** b ** (c / d ** e) ** f"), term("a ** (b ** ((c / d ** e) ** f))"));
|
||||
assert_eq!(term("a ** b ** c % d ** e ** f"), term("(a ** b ** c) % (d ** e ** f)"));
|
||||
assert_eq!(term("a ** (b ** c % d) ** e ** f"), term("a ** ((b ** c % d) ** (e ** f))"));
|
||||
assert_eq!(term("a ** b ** (c % d) ** e ** f"), term("a ** (b ** ((c % d) ** (e ** f)))"));
|
||||
assert_eq!(term("a ** b ** (c % d ** e) ** f"), term("a ** (b ** ((c % d ** e) ** f))"));
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_bounds()
|
||||
{
|
||||
let term = |i| original::term(i, &Declarations::new()).unwrap().0;
|
||||
|
||||
assert_eq!(term("1 ** 2 ** 3, rest"), ", rest");
|
||||
assert_eq!(term("1 * 2 * 3, rest"), ", rest");
|
||||
assert_eq!(term("1 / 2 / 3, rest"), ", rest");
|
||||
assert_eq!(term("1 % 2 % 3, rest"), ", rest");
|
||||
assert_eq!(term("1 + 2 + 3, rest"), ", rest");
|
||||
assert_eq!(term("1 - 2 - 3, rest"), ", rest");
|
||||
assert_eq!(term("1, rest"), ", rest");
|
||||
assert_eq!(term("-1, rest"), ", rest");
|
||||
assert_eq!(term("--1, rest"), ", rest");
|
||||
assert_eq!(term("|1|, rest"), ", rest");
|
||||
assert_eq!(term("|1| + |-2|, rest"), ", rest");
|
||||
assert_eq!(term("||-2||, rest"), ", rest");
|
||||
assert_eq!(term("|-|-2||, rest"), ", rest");
|
||||
assert_eq!(term("(1), rest"), ", rest");
|
||||
assert_eq!(term("a, rest"), ", rest");
|
||||
assert_eq!(term("1, rest"), ", rest");
|
||||
assert_eq!(term("true, rest"), ", rest");
|
||||
assert_eq!(term("false, rest"), ", rest");
|
||||
assert_eq!(term("#inf, rest"), ", rest");
|
||||
assert_eq!(term("#sup, rest"), ", rest");
|
||||
assert_eq!(term("f(1, 2), rest"), ", rest");
|
||||
assert_eq!(term("g(1 ** 2, 3 * 4, #inf), rest"), ", rest");
|
||||
assert_eq!(term("\"test\", rest"), ", rest");
|
||||
assert_eq!(term("X, rest"), ", rest");
|
||||
assert_eq!(term("Variable, rest"), ", rest");
|
||||
assert_eq!(term("f(\"test\", Variable), rest"), ", rest");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_whitespace()
|
||||
{
|
||||
assert_eq!(format_term("(a+b)*(c+d)"), "(a + b) * (c + d)");
|
||||
assert_eq!(format_term("( a + b ) * ( c + d )"), "(a + b) * (c + d)");
|
||||
assert_eq!(format_term("( a + b ) * ( c + d )"), "(a + b) * (c + d)");
|
||||
assert_eq!(format_term("(\ta\t+\tb\t)\t*\t(\tc\t+\td\t)"), "(a + b) * (c + d)");
|
||||
assert_eq!(format_term("(\na\n+\nb\n)\n*\n(\nc\n+\nd\n)"), "(a + b) * (c + d)");
|
||||
assert_eq!(format_term("( \t a \t + \t b \t ) \t * \t ( \t c \t + \t d \t )"), "(a + b) * (c + d)");
|
||||
assert_eq!(format_term("( \n a \n + \n b \n ) \n * \n ( \n c \n + \n d \n )"), "(a + b) * (c + d)");
|
||||
assert_eq!(format_term("f(\ta\t+\tb\t,\tc\t+\td\t)"), "f(a + b, c + d)");
|
||||
assert_eq!(format_term("f(\na\n+\nb\n,\nc\n+\nd\n)"), "f(a + b, c + d)");
|
||||
assert_eq!(format_term("f( \t a \t + \t b \t , \t c \t + \t d \t)"), "f(a + b, c + d)");
|
||||
assert_eq!(format_term("f( \n a \n + \n b \n , \n c \n + \n d \n)"), "f(a + b, c + d)");
|
||||
// TODO: test other operators
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_function_primitive()
|
||||
{
|
||||
let function = |i| original::function(i, &Declarations::new()).unwrap().1;
|
||||
let function_remainder = |i| original::function(i, &Declarations::new()).unwrap().0;
|
||||
|
||||
assert_eq!(function("s").declaration.name, "s");
|
||||
assert_eq!(function("s").declaration.arity, 0);
|
||||
assert_eq!(function_remainder("s"), "");
|
||||
assert_eq!(function("s ( )").declaration.name, "s");
|
||||
assert_eq!(function("s ( )").declaration.arity, 0);
|
||||
assert_eq!(function_remainder("s ( )"), "");
|
||||
assert_eq!(function("s ( 1 , 2 , 3 )").declaration.name, "s");
|
||||
assert_eq!(function("s ( 1 , 2 , 3 )").declaration.arity, 3);
|
||||
assert_eq!(*function("s ( 1 , 2 , 3 )").arguments.remove(0), Term::integer(1));
|
||||
assert_eq!(*function("s ( 1 , 2 , 3 )").arguments.remove(1), Term::integer(2));
|
||||
assert_eq!(*function("s ( 1 , 2 , 3 )").arguments.remove(2), Term::integer(3));
|
||||
assert_eq!(function_remainder("s ( 1 , 2 , 3 )"), "");
|
||||
assert_eq!(function("s ( ), rest").declaration.name, "s");
|
||||
assert_eq!(function("s ( ), rest").declaration.arity, 0);
|
||||
assert_eq!(function_remainder("s ( ), rest"), ", rest");
|
||||
assert_eq!(function("s ( 1 , 2 , 3 ), rest").declaration.name, "s");
|
||||
assert_eq!(function("s ( 1 , 2 , 3 ), rest").declaration.arity, 3);
|
||||
assert_eq!(function_remainder("s ( 1 , 2 , 3 ), rest"), ", rest");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_variable_declaration()
|
||||
{
|
||||
let variable_declaration = |i| original::variable_declaration(i).unwrap().1;
|
||||
let variable_declaration_remainder = |i| original::variable_declaration(i).unwrap().0;
|
||||
|
||||
assert_eq!(variable_declaration("X Rest").name, "X");
|
||||
assert_eq!(variable_declaration_remainder("X Rest"), " Rest");
|
||||
assert_eq!(variable_declaration("X, Rest").name, "X");
|
||||
assert_eq!(variable_declaration_remainder("X, Rest"), ", Rest");
|
||||
// Variable declarations parsed at different locations should not be considered equal
|
||||
assert_ne!(variable_declaration("X"), variable_declaration("X"));
|
||||
assert_eq!(variable_declaration("Variable_123 Rest").name, "Variable_123");
|
||||
assert_eq!(variable_declaration_remainder("Variable_123 Rest"), " Rest");
|
||||
|
||||
let variable_declaration = original::variable_declaration;
|
||||
|
||||
assert!(variable_declaration("0 Rest").is_err());
|
||||
assert!(variable_declaration("123_Asd Rest").is_err());
|
||||
assert!(variable_declaration("x Rest").is_err());
|
||||
assert!(variable_declaration("variable_123 Rest").is_err());
|
||||
assert!(variable_declaration("_ Rest").is_err());
|
||||
assert!(variable_declaration("_variable_123 Rest").is_err());
|
||||
assert!(variable_declaration(" ").is_err());
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn parse_variable_primitive()
|
||||
{
|
||||
let variable = |i| original::variable(i, &Declarations::new()).unwrap().1;
|
||||
let variable_remainder = |i| original::variable(i, &Declarations::new()).unwrap().0;
|
||||
|
||||
assert_eq!(variable("X Rest").declaration.name, "X");
|
||||
assert_eq!(variable_remainder("X Rest"), " Rest");
|
||||
assert_eq!(variable("X, Rest").declaration.name, "X");
|
||||
assert_eq!(variable_remainder("X, Rest"), ", Rest");
|
||||
assert_eq!(variable("Variable_123 Rest").declaration.name, "Variable_123");
|
||||
assert_eq!(variable_remainder("Variable_123 Rest"), " Rest");
|
||||
|
||||
let variable = |i| original::variable(i, &Declarations::new());
|
||||
|
||||
assert!(variable("0 Rest").is_err());
|
||||
assert!(variable("123_Asd Rest").is_err());
|
||||
assert!(variable("x Rest").is_err());
|
||||
assert!(variable("variable_123 Rest").is_err());
|
||||
assert!(variable("_ Rest").is_err());
|
||||
assert!(variable("_variable_123 Rest").is_err());
|
||||
assert!(variable(" ").is_err());
|
||||
|
||||
let new_variable_declarations = |names: &[&str]| std::rc::Rc::new(names.iter()
|
||||
.map(|name| std::rc::Rc::new(VariableDeclaration::new(name.to_string())))
|
||||
.collect());
|
||||
|
||||
let layer_1 = new_variable_declarations(&["A", "B", "X"]);
|
||||
let layer_2 = new_variable_declarations(&["C", "D", "X"]);
|
||||
let layer_3 = new_variable_declarations(&["E", "F", "Y"]);
|
||||
let layer_4 = new_variable_declarations(&["G", "H", "X"]);
|
||||
|
||||
let variable_declaration_stack = VariableDeclarationStack::new();
|
||||
|
||||
let mut declarations = Declarations::new();
|
||||
declarations.variable_declaration_stack =
|
||||
std::cell::RefCell::new(variable_declaration_stack);
|
||||
|
||||
let variable = |i| original::variable(i, &declarations).unwrap().1;
|
||||
let number_of_free_variable_declarations =
|
||||
|| declarations.variable_declaration_stack.borrow().free_variable_declarations.len();
|
||||
|
||||
let x1 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 1);
|
||||
let x2 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 1);
|
||||
assert_eq!(x1.declaration, x2.declaration);
|
||||
let y1 = variable("Y");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_ne!(x1.declaration, y1.declaration);
|
||||
assert_ne!(x2.declaration, y1.declaration);
|
||||
|
||||
declarations.variable_declaration_stack.borrow_mut().push(layer_1);
|
||||
|
||||
let x3 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_ne!(x1.declaration, x3.declaration);
|
||||
let x4 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_eq!(x3.declaration, x4.declaration);
|
||||
let a1 = variable("A");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_ne!(x3.declaration, a1.declaration);
|
||||
let y2 = variable("Y");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_eq!(y1.declaration, y2.declaration);
|
||||
|
||||
declarations.variable_declaration_stack.borrow_mut().push(layer_2);
|
||||
|
||||
let x5 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_ne!(x1.declaration, x5.declaration);
|
||||
assert_ne!(x3.declaration, x5.declaration);
|
||||
let x6 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_eq!(x5.declaration, x6.declaration);
|
||||
let a2 = variable("A");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_eq!(a1.declaration, a2.declaration);
|
||||
|
||||
declarations.variable_declaration_stack.borrow_mut().push(layer_3);
|
||||
|
||||
let x7 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_eq!(x5.declaration, x7.declaration);
|
||||
let y3 = variable("Y");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_ne!(y2.declaration, y3.declaration);
|
||||
|
||||
declarations.variable_declaration_stack.borrow_mut().push(layer_4);
|
||||
|
||||
let x8 = variable("X");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_ne!(x7.declaration, x8.declaration);
|
||||
let y4 = variable("Y");
|
||||
assert_eq!(number_of_free_variable_declarations(), 2);
|
||||
assert_eq!(y3.declaration, y4.declaration);
|
||||
let _ = variable("I");
|
||||
assert_eq!(number_of_free_variable_declarations(), 3);
|
||||
}
|
||||
}
|
72
src/utils.rs
Normal file
72
src/utils.rs
Normal file
@ -0,0 +1,72 @@
|
||||
pub struct VariableDeclarationStack
|
||||
{
|
||||
pub free_variable_declarations: crate::VariableDeclarations,
|
||||
bound_variable_declaration_stack: Vec<std::rc::Rc<crate::VariableDeclarations>>,
|
||||
}
|
||||
|
||||
impl VariableDeclarationStack
|
||||
{
|
||||
pub fn new() -> Self
|
||||
{
|
||||
Self
|
||||
{
|
||||
free_variable_declarations: crate::VariableDeclarations::new(),
|
||||
bound_variable_declaration_stack: vec![],
|
||||
}
|
||||
}
|
||||
|
||||
pub fn find(&self, variable_name: &str) -> Option<std::rc::Rc<crate::VariableDeclaration>>
|
||||
{
|
||||
for variable_declarations in self.bound_variable_declaration_stack.iter().rev()
|
||||
{
|
||||
if let Some(variable_declaration) = variable_declarations.iter()
|
||||
.find(|x| x.name == 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 find_or_create(&mut self, variable_name: &str) -> std::rc::Rc<crate::VariableDeclaration>
|
||||
{
|
||||
if let Some(variable_declaration) = self.find(variable_name)
|
||||
{
|
||||
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 is_empty(&self) -> bool
|
||||
{
|
||||
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"))
|
||||
}
|
||||
}
|
Loading…
Reference in New Issue
Block a user