From 1a2ffe1b3232d05b1e3e93ac61ffc439c247c3c7 Mon Sep 17 00:00:00 2001 From: elvis Date: Tue, 29 Jul 2025 19:35:25 +0200 Subject: [PATCH] First draft for assertions --- src/rsprocess/assert.rs | 163 ++++++++++++++++++++++++++++++++++ src/rsprocess/grammar.lalrpop | 65 +++++++------- src/rsprocess/mod.rs | 1 + src/rsprocess/structure.rs | 25 ++---- src/rsprocess/translator.rs | 32 +------ 5 files changed, 202 insertions(+), 84 deletions(-) create mode 100644 src/rsprocess/assert.rs diff --git a/src/rsprocess/assert.rs b/src/rsprocess/assert.rs new file mode 100644 index 0000000..fe1d7b5 --- /dev/null +++ b/src/rsprocess/assert.rs @@ -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, Box), + If(Box, Box), + IfElse(Box, Box, Box), + Assignment(AssignmentVar, Box), + Return(Box), + For(Variable, Range, Box), +} + +#[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), + And(Box, Box), + Or(Box, Box), + Xor(Box, Box), + + 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, Box), + Minus(Box, Box), + Times(Box, Box), + Quotient(Box, Box), + Reminder(Box, Box), + Exponential(Box, Box), + Rand(Box, Box), + Min(Box, Box), + Max(Box, Box), + + SetLength(Set), + StrLength(Str), +} + +#[derive(Debug, Clone)] +pub enum Label { + Var(Variable), // should be of type label + Literal(Box), +} + +#[derive(Debug, Clone)] +pub enum Set { + Var(Variable), // should be of type set + Literal(super::structure::RSset), + Append(Box, Element), + Union(Box, Box), + Intersection(Box, Box), + Difference(Box, Box), + SimmetricDifference(Box, Box), + 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, Box), + ArithmeticToString(Box), + BooleanToString(Box), + ElementToString(Element), + CommonSubstring(Box, Box), +} + +#[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, Box), +} diff --git a/src/rsprocess/grammar.lalrpop b/src/rsprocess/grammar.lalrpop index 2fa9593..a46f116 100644 --- a/src/rsprocess/grammar.lalrpop +++ b/src/rsprocess/grammar.lalrpop @@ -4,9 +4,6 @@ use lalrpop_util::ParseError; use crate::rsprocess::structure::{RSset, RSprocess, RSenvironment, - RSassert, - RSassertOp, - RSBHML, RSsystem, RSreaction}; use crate::rsprocess::translator::{Translator, IdType}; @@ -171,43 +168,43 @@ Env_term: (IdType, RSprocess) = { // ----------------------------------------------------------------------------- // AssertParser // ----------------------------------------------------------------------------- -pub Assert: Box = { - => Box::new(f) -}; +// pub Assert: Box = { +// => Box::new(f) +// }; -Formula_Assert: RSassert = { - "-" => RSassert::Not(Box::new(f)), - "(" "^" ")" => - RSassert::Xor(Box::new(f1), Box::new(f2)), - "(" > ")" => RSassert::Or(f), - "(" > ")" => RSassert::And(f), - "inW" => RSassert::Sub(c, RSassertOp::InW), - "inR" => RSassert::Sub(c, RSassertOp::InR), - "inI" => RSassert::Sub(c, RSassertOp::InI), - "inP" => RSassert::Sub(c, RSassertOp::InP), - "?" "inW" => RSassert::NonEmpty(RSassertOp::InW), - "?" "inR" => RSassert::NonEmpty(RSassertOp::InR), - "?" "inI" => RSassert::NonEmpty(RSassertOp::InI), - "?" "inP" => RSassert::NonEmpty(RSassertOp::InP), -}; +// Formula_Assert: RSassert = { +// "-" => RSassert::Not(Box::new(f)), +// "(" "^" ")" => +// RSassert::Xor(Box::new(f1), Box::new(f2)), +// "(" > ")" => RSassert::Or(f), +// "(" > ")" => RSassert::And(f), +// "inW" => RSassert::Sub(c, RSassertOp::InW), +// "inR" => RSassert::Sub(c, RSassertOp::InR), +// "inI" => RSassert::Sub(c, RSassertOp::InI), +// "inP" => RSassert::Sub(c, RSassertOp::InP), +// "?" "inW" => RSassert::NonEmpty(RSassertOp::InW), +// "?" "inR" => RSassert::NonEmpty(RSassertOp::InR), +// "?" "inI" => RSassert::NonEmpty(RSassertOp::InI), +// "?" "inP" => RSassert::NonEmpty(RSassertOp::InP), +// }; // ----------------------------------------------------------------------------- // BHMLParser // ----------------------------------------------------------------------------- -pub BHML: Box = { - => Box::new(g) -}; +// pub BHML: Box = { +// => Box::new(g) +// }; -Formula_BHML: RSBHML = { - "true" => RSBHML::True, - "false" => RSBHML::False, - "(" > ")" => RSBHML::Or(g), - "(" > ")" => RSBHML::And(g), - "<" ">" => - RSBHML::Diamond(Box::new(f), Box::new(g)), - "[" "]" => - RSBHML::Box(Box::new(f), Box::new(g)), -}; +// Formula_BHML: RSBHML = { +// "true" => RSBHML::True, +// "false" => RSBHML::False, +// "(" > ")" => RSBHML::Or(g), +// "(" > ")" => RSBHML::And(g), +// "<" ">" => +// RSBHML::Diamond(Box::new(f), Box::new(g)), +// "[" "]" => +// RSBHML::Box(Box::new(f), Box::new(g)), +// }; // ---------------------------------------------------------------------------- diff --git a/src/rsprocess/mod.rs b/src/rsprocess/mod.rs index 2ad7bc5..ab2f7f0 100644 --- a/src/rsprocess/mod.rs +++ b/src/rsprocess/mod.rs @@ -16,3 +16,4 @@ pub mod presets; pub mod bisimilarity; mod format_helpers; +mod assert; diff --git a/src/rsprocess/structure.rs b/src/rsprocess/structure.rs index cb91b3a..09a2588 100644 --- a/src/rsprocess/structure.rs +++ b/src/rsprocess/structure.rs @@ -593,30 +593,17 @@ impl Hash for RSlabel { } } -// ----------------------------------------------------------------------------- -// RSassertOp -// ----------------------------------------------------------------------------- -#[derive(Clone, Debug)] -pub enum RSassertOp { - InW, - InR, - InI, - InP, -} - // ----------------------------------------------------------------------------- // RSassert // ----------------------------------------------------------------------------- -#[derive(Clone, Debug)] -pub enum RSassert { - Not(Box), - Xor(Box, Box), - Or(Vec), - And(Vec), - Sub(RSset, RSassertOp), - NonEmpty(RSassertOp), + +pub use crate::rsprocess::assert::RSassert; + +pub mod assert { + pub use crate::rsprocess::assert::*; } + // ----------------------------------------------------------------------------- // RSBHML // ----------------------------------------------------------------------------- diff --git a/src/rsprocess/translator.rs b/src/rsprocess/translator.rs index ee0548d..7f2e80e 100644 --- a/src/rsprocess/translator.rs +++ b/src/rsprocess/translator.rs @@ -76,7 +76,7 @@ impl Translator { use super::{ frequency::Frequency, structure::{ - RSBHML, RSassert, RSassertOp, RSchoices, RSenvironment, RSlabel, + RSBHML, RSassert, RSchoices, RSenvironment, RSlabel, RSprocess, RSreaction, RSset, RSsystem, }, }; @@ -360,36 +360,6 @@ fn 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 #[allow(unused_variables)]