First draft for assertions
This commit is contained in:
163
src/rsprocess/assert.rs
Normal file
163
src/rsprocess/assert.rs
Normal file
@ -0,0 +1,163 @@
|
|||||||
|
#![allow(dead_code)]
|
||||||
|
|
||||||
|
type IntegerType = i64;
|
||||||
|
|
||||||
|
#[derive(Debug, Clone)]
|
||||||
|
pub struct RSassert {
|
||||||
|
pub tree: Tree
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone)]
|
||||||
|
pub enum Tree {
|
||||||
|
Concat(Box<Tree>, Box<Tree>),
|
||||||
|
If(Box<Boolean>, Box<Tree>),
|
||||||
|
IfElse(Box<Boolean>, Box<Tree>, Box<Tree>),
|
||||||
|
Assignment(AssignmentVar, Box<Expression>),
|
||||||
|
Return(Box<Expression>),
|
||||||
|
For(Variable, Range, Box<Tree>),
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone)]
|
||||||
|
pub enum Expression {
|
||||||
|
B(Boolean),
|
||||||
|
A(Arithmetic),
|
||||||
|
Lab(Label),
|
||||||
|
Set(Set),
|
||||||
|
El(Element),
|
||||||
|
Str(Str),
|
||||||
|
|
||||||
|
Var(Variable), // for when the type should just be passed through
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone)]
|
||||||
|
pub enum Boolean {
|
||||||
|
Var(Variable), // should be of type boolean
|
||||||
|
True,
|
||||||
|
False,
|
||||||
|
Not(Box<Boolean>),
|
||||||
|
And(Box<Boolean>, Box<Boolean>),
|
||||||
|
Or(Box<Boolean>, Box<Boolean>),
|
||||||
|
Xor(Box<Boolean>, Box<Boolean>),
|
||||||
|
|
||||||
|
Less(Arithmetic, Arithmetic),
|
||||||
|
LessEq(Arithmetic, Arithmetic),
|
||||||
|
More(Arithmetic, Arithmetic),
|
||||||
|
MoreEq(Arithmetic, Arithmetic),
|
||||||
|
Eq(Arithmetic, Arithmetic),
|
||||||
|
NotEq(Arithmetic, Arithmetic),
|
||||||
|
|
||||||
|
LabelEq(Label, Label),
|
||||||
|
LabelNotEq(Label, Label),
|
||||||
|
|
||||||
|
SetSub(Set, Set),
|
||||||
|
SetSubEq(Set, Set),
|
||||||
|
SetSuper(Set, Set),
|
||||||
|
SetSuperEq(Set, Set),
|
||||||
|
SetEq(Set, Set),
|
||||||
|
SetEmpty(Set),
|
||||||
|
|
||||||
|
ElEq(Element, Element),
|
||||||
|
ElNotEq(Element, Element),
|
||||||
|
|
||||||
|
StrEq(Str, Str),
|
||||||
|
StrNotEq(Str, Str),
|
||||||
|
StrSubstring(Str, Str),
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone)]
|
||||||
|
pub enum Arithmetic {
|
||||||
|
Var(Variable), // should be of type arithmetic
|
||||||
|
Integer(IntegerType),
|
||||||
|
Plus(Box<Arithmetic>, Box<Arithmetic>),
|
||||||
|
Minus(Box<Arithmetic>, Box<Arithmetic>),
|
||||||
|
Times(Box<Arithmetic>, Box<Arithmetic>),
|
||||||
|
Quotient(Box<Arithmetic>, Box<Arithmetic>),
|
||||||
|
Reminder(Box<Arithmetic>, Box<Arithmetic>),
|
||||||
|
Exponential(Box<Arithmetic>, Box<Arithmetic>),
|
||||||
|
Rand(Box<Arithmetic>, Box<Arithmetic>),
|
||||||
|
Min(Box<Arithmetic>, Box<Arithmetic>),
|
||||||
|
Max(Box<Arithmetic>, Box<Arithmetic>),
|
||||||
|
|
||||||
|
SetLength(Set),
|
||||||
|
StrLength(Str),
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone)]
|
||||||
|
pub enum Label {
|
||||||
|
Var(Variable), // should be of type label
|
||||||
|
Literal(Box<super::structure::RSlabel>),
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone)]
|
||||||
|
pub enum Set {
|
||||||
|
Var(Variable), // should be of type set
|
||||||
|
Literal(super::structure::RSset),
|
||||||
|
Append(Box<Set>, Element),
|
||||||
|
Union(Box<Set>, Box<Set>),
|
||||||
|
Intersection(Box<Set>, Box<Set>),
|
||||||
|
Difference(Box<Set>, Box<Set>),
|
||||||
|
SimmetricDifference(Box<Set>, Box<Set>),
|
||||||
|
ValueOfLabel(Label, Qualifier),
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone)]
|
||||||
|
pub enum Element {
|
||||||
|
Var(Variable), // should be of type element
|
||||||
|
Literal(super::translator::IdType),
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone)]
|
||||||
|
pub enum Str {
|
||||||
|
Var(Variable), // should be of type string
|
||||||
|
Literal(String),
|
||||||
|
Concat(Box<Str>, Box<Str>),
|
||||||
|
ArithmeticToString(Box<Arithmetic>),
|
||||||
|
BooleanToString(Box<Boolean>),
|
||||||
|
ElementToString(Element),
|
||||||
|
CommonSubstring(Box<Str>, Box<Str>),
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone)]
|
||||||
|
pub enum AssignmentVar {
|
||||||
|
Var(Variable),
|
||||||
|
ValueOfVariable(Variable, QualifierAssignment),
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone)]
|
||||||
|
pub struct Variable {
|
||||||
|
name: String,
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone, Copy)]
|
||||||
|
pub enum QualifierAssignment {
|
||||||
|
Entities,
|
||||||
|
Context,
|
||||||
|
Reactants,
|
||||||
|
ReactantsAbsent,
|
||||||
|
Inhibitors,
|
||||||
|
InhibitorsPresent,
|
||||||
|
Products,
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone, Copy)]
|
||||||
|
pub enum Qualifier {
|
||||||
|
Entities,
|
||||||
|
Context,
|
||||||
|
AvailableEntities,
|
||||||
|
|
||||||
|
Reactants,
|
||||||
|
ReactantsAbsent,
|
||||||
|
AllReactants,
|
||||||
|
|
||||||
|
Inhibitors,
|
||||||
|
InhibitorsPresent,
|
||||||
|
AllInhibitors,
|
||||||
|
|
||||||
|
Products,
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone)]
|
||||||
|
pub enum Range {
|
||||||
|
IterateOverSet(Set),
|
||||||
|
IterateInRange(Box<Arithmetic>, Box<Arithmetic>),
|
||||||
|
}
|
||||||
@ -4,9 +4,6 @@ use lalrpop_util::ParseError;
|
|||||||
use crate::rsprocess::structure::{RSset,
|
use crate::rsprocess::structure::{RSset,
|
||||||
RSprocess,
|
RSprocess,
|
||||||
RSenvironment,
|
RSenvironment,
|
||||||
RSassert,
|
|
||||||
RSassertOp,
|
|
||||||
RSBHML,
|
|
||||||
RSsystem,
|
RSsystem,
|
||||||
RSreaction};
|
RSreaction};
|
||||||
use crate::rsprocess::translator::{Translator, IdType};
|
use crate::rsprocess::translator::{Translator, IdType};
|
||||||
@ -171,43 +168,43 @@ Env_term: (IdType, RSprocess) = {
|
|||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
// AssertParser
|
// AssertParser
|
||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
pub Assert: Box<RSassert> = {
|
// pub Assert: Box<RSassert> = {
|
||||||
<f: Formula_Assert> => Box::new(f)
|
// <f: Formula_Assert> => Box::new(f)
|
||||||
};
|
// };
|
||||||
|
|
||||||
Formula_Assert: RSassert = {
|
// Formula_Assert: RSassert = {
|
||||||
"-" <f: Formula_Assert> => RSassert::Not(Box::new(f)),
|
// "-" <f: Formula_Assert> => RSassert::Not(Box::new(f)),
|
||||||
"(" <f1: Formula_Assert> "^" <f2: Formula_Assert> ")" =>
|
// "(" <f1: Formula_Assert> "^" <f2: Formula_Assert> ")" =>
|
||||||
RSassert::Xor(Box::new(f1), Box::new(f2)),
|
// RSassert::Xor(Box::new(f1), Box::new(f2)),
|
||||||
"(" <f: Separated<Formula_Assert, "\\/">> ")" => RSassert::Or(f),
|
// "(" <f: Separated<Formula_Assert, "\\/">> ")" => RSassert::Or(f),
|
||||||
"(" <f: Separated<Formula_Assert, "/\\">> ")" => RSassert::And(f),
|
// "(" <f: Separated<Formula_Assert, "/\\">> ")" => RSassert::And(f),
|
||||||
<c: Set_of_entities> "inW" => RSassert::Sub(c, RSassertOp::InW),
|
// <c: Set_of_entities> "inW" => RSassert::Sub(c, RSassertOp::InW),
|
||||||
<c: Set_of_entities> "inR" => RSassert::Sub(c, RSassertOp::InR),
|
// <c: Set_of_entities> "inR" => RSassert::Sub(c, RSassertOp::InR),
|
||||||
<c: Set_of_entities> "inI" => RSassert::Sub(c, RSassertOp::InI),
|
// <c: Set_of_entities> "inI" => RSassert::Sub(c, RSassertOp::InI),
|
||||||
<c: Set_of_entities> "inP" => RSassert::Sub(c, RSassertOp::InP),
|
// <c: Set_of_entities> "inP" => RSassert::Sub(c, RSassertOp::InP),
|
||||||
"?" "inW" => RSassert::NonEmpty(RSassertOp::InW),
|
// "?" "inW" => RSassert::NonEmpty(RSassertOp::InW),
|
||||||
"?" "inR" => RSassert::NonEmpty(RSassertOp::InR),
|
// "?" "inR" => RSassert::NonEmpty(RSassertOp::InR),
|
||||||
"?" "inI" => RSassert::NonEmpty(RSassertOp::InI),
|
// "?" "inI" => RSassert::NonEmpty(RSassertOp::InI),
|
||||||
"?" "inP" => RSassert::NonEmpty(RSassertOp::InP),
|
// "?" "inP" => RSassert::NonEmpty(RSassertOp::InP),
|
||||||
};
|
// };
|
||||||
|
|
||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
// BHMLParser
|
// BHMLParser
|
||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
pub BHML: Box<RSBHML> = {
|
// pub BHML: Box<RSBHML> = {
|
||||||
<g: Formula_BHML> => Box::new(g)
|
// <g: Formula_BHML> => Box::new(g)
|
||||||
};
|
// };
|
||||||
|
|
||||||
Formula_BHML: RSBHML = {
|
// Formula_BHML: RSBHML = {
|
||||||
"true" => RSBHML::True,
|
// "true" => RSBHML::True,
|
||||||
"false" => RSBHML::False,
|
// "false" => RSBHML::False,
|
||||||
"(" <g: Separated<Formula_BHML, "\\/">> ")" => RSBHML::Or(g),
|
// "(" <g: Separated<Formula_BHML, "\\/">> ")" => RSBHML::Or(g),
|
||||||
"(" <g: Separated<Formula_BHML, "/\\">> ")" => RSBHML::And(g),
|
// "(" <g: Separated<Formula_BHML, "/\\">> ")" => RSBHML::And(g),
|
||||||
"<" <f: Formula_Assert> ">" <g: Formula_BHML> =>
|
// "<" <f: Formula_Assert> ">" <g: Formula_BHML> =>
|
||||||
RSBHML::Diamond(Box::new(f), Box::new(g)),
|
// RSBHML::Diamond(Box::new(f), Box::new(g)),
|
||||||
"[" <f: Formula_Assert> "]" <g: Formula_BHML> =>
|
// "[" <f: Formula_Assert> "]" <g: Formula_BHML> =>
|
||||||
RSBHML::Box(Box::new(f), Box::new(g)),
|
// RSBHML::Box(Box::new(f), Box::new(g)),
|
||||||
};
|
// };
|
||||||
|
|
||||||
|
|
||||||
// ----------------------------------------------------------------------------
|
// ----------------------------------------------------------------------------
|
||||||
|
|||||||
@ -16,3 +16,4 @@ pub mod presets;
|
|||||||
pub mod bisimilarity;
|
pub mod bisimilarity;
|
||||||
|
|
||||||
mod format_helpers;
|
mod format_helpers;
|
||||||
|
mod assert;
|
||||||
|
|||||||
@ -593,30 +593,17 @@ impl Hash for RSlabel {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// -----------------------------------------------------------------------------
|
|
||||||
// RSassertOp
|
|
||||||
// -----------------------------------------------------------------------------
|
|
||||||
#[derive(Clone, Debug)]
|
|
||||||
pub enum RSassertOp {
|
|
||||||
InW,
|
|
||||||
InR,
|
|
||||||
InI,
|
|
||||||
InP,
|
|
||||||
}
|
|
||||||
|
|
||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
// RSassert
|
// RSassert
|
||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
#[derive(Clone, Debug)]
|
|
||||||
pub enum RSassert {
|
pub use crate::rsprocess::assert::RSassert;
|
||||||
Not(Box<RSassert>),
|
|
||||||
Xor(Box<RSassert>, Box<RSassert>),
|
pub mod assert {
|
||||||
Or(Vec<RSassert>),
|
pub use crate::rsprocess::assert::*;
|
||||||
And(Vec<RSassert>),
|
|
||||||
Sub(RSset, RSassertOp),
|
|
||||||
NonEmpty(RSassertOp),
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
// RSBHML
|
// RSBHML
|
||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
|
|||||||
@ -76,7 +76,7 @@ impl Translator {
|
|||||||
use super::{
|
use super::{
|
||||||
frequency::Frequency,
|
frequency::Frequency,
|
||||||
structure::{
|
structure::{
|
||||||
RSBHML, RSassert, RSassertOp, RSchoices, RSenvironment, RSlabel,
|
RSBHML, RSassert, RSchoices, RSenvironment, RSlabel,
|
||||||
RSprocess, RSreaction, RSset, RSsystem,
|
RSprocess, RSreaction, RSset, RSsystem,
|
||||||
},
|
},
|
||||||
};
|
};
|
||||||
@ -360,36 +360,6 @@ fn print_label(
|
|||||||
|
|
||||||
translator_structure!(RSlabelDisplay, RSlabel, label, print_label);
|
translator_structure!(RSlabelDisplay, RSlabel, label, print_label);
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
// RSassertOp
|
|
||||||
|
|
||||||
fn print_assert_op(
|
|
||||||
f: &mut fmt::Formatter,
|
|
||||||
_translator: &Translator,
|
|
||||||
assert_op: &RSassertOp,
|
|
||||||
) -> fmt::Result {
|
|
||||||
use super::structure::RSassertOp::*;
|
|
||||||
match assert_op {
|
|
||||||
InW => {
|
|
||||||
write!(f, "InW")
|
|
||||||
}
|
|
||||||
InR => {
|
|
||||||
write!(f, "InR")
|
|
||||||
}
|
|
||||||
InI => {
|
|
||||||
write!(f, "InI")
|
|
||||||
}
|
|
||||||
InP => {
|
|
||||||
write!(f, "InP")
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
translator_structure!(RSassertOpDisplay, RSassertOp, assert_op, print_assert_op);
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
// RSassert
|
// RSassert
|
||||||
|
|
||||||
#[allow(unused_variables)]
|
#[allow(unused_variables)]
|
||||||
|
|||||||
Reference in New Issue
Block a user