elvis/ReactionSystems
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Parser for assert

Browse Source
This commit is contained in:
elvis
2025-08-18 20:39:43 +02:00
parent eb94964677
commit 331635981a
3 changed files with 191 additions and 160 deletions
Download Patch File Download Diff File Expand all files Collapse all files

34
src/rsprocess/assert/rsassert.rs
View File

@ -6,6 +6,33 @@ use std::collections::HashMap;
// Specific Assert Implementation // Specific Assert Implementation
// ---------------------------------------------------------------------------- // ----------------------------------------------------------------------------
pub mod useful_types_edge_relabeler {
macro_rules! export_types {
( $( $x:ident ),* ) => {
$(
pub type $x = super::super::dsl::$x<super::EdgeRelablerInput>;
)*
};
}
macro_rules! export_types_no_parameter {
( $( $x:ident ),* ) => {
$(
pub type $x = super::super::dsl::$x;
)*
};
}
export_types!(RSassert, Tree, Variable, Expression, Range);
export_types_no_parameter!(Unary, QualifierRestricted, QualifierLabel,
QualifierSystem, QualifierEdge, QualifierNode,
Qualifier, Binary, AssertReturnValue);
pub type Special = super::EdgeRelablerInput;
}
// Implementation for graph labeling in bisimulation. // Implementation for graph labeling in bisimulation.
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
@ -15,7 +42,7 @@ pub enum EdgeRelablerInput {
} }
#[derive(Debug, Clone)] #[derive(Debug, Clone)]
pub enum EdgeRelablerInputValues { enum EdgeRelablerInputValues {
Label(structure::RSlabel), Label(structure::RSlabel),
Edge(petgraph::graph::EdgeIndex), Edge(petgraph::graph::EdgeIndex),
} }
@ -68,7 +95,6 @@ impl std::fmt::Display for EdgeRelablerInput {
} }
} }
impl RSassert<EdgeRelablerInput> { impl RSassert<EdgeRelablerInput> {
pub fn typecheck(&self) -> Result<(), String> { pub fn typecheck(&self) -> Result<(), String> {
let mut context = TypeContext::new(); let mut context = TypeContext::new();
@ -119,7 +145,9 @@ impl RSassert<EdgeRelablerInput> {
} }
} }
// -----------------------------------------------------------------------------
// Implementation for node grouping. // Implementation for node grouping.
// -----------------------------------------------------------------------------
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
pub enum NodeRelablerInput { pub enum NodeRelablerInput {
@ -128,7 +156,7 @@ pub enum NodeRelablerInput {
} }
#[derive(Debug, Clone)] #[derive(Debug, Clone)]
pub enum NodeRelablerInputValues { enum NodeRelablerInputValues {
Entities(structure::RSset), Entities(structure::RSset),
Node(petgraph::graph::NodeIndex), Node(petgraph::graph::NodeIndex),
} }

297
src/rsprocess/grammar.lalrpop
View File

@ -5,9 +5,9 @@ use crate::rsprocess::structure::{RSset,
RSprocess, RSprocess,
RSenvironment, RSenvironment,
RSsystem, RSsystem,
// RSlabel, RSlabel,
RSreaction }; RSreaction };
use crate::rsprocess::structure::assert; use crate::rsprocess::structure::rsassert;
use crate::rsprocess::translator::{ Translator, IdType }; use crate::rsprocess::translator::{ Translator, IdType };
use crate::rsprocess::presets::Instructions; use crate::rsprocess::presets::Instructions;
use crate::rsprocess::presets; use crate::rsprocess::presets;
@ -180,176 +180,177 @@ Env_term: (IdType, RSprocess) = {
// ----------------------------------------------------------------------------- // -----------------------------------------------------------------------------
// AssertParser // AssertParser
// ----------------------------------------------------------------------------- // -----------------------------------------------------------------------------
// pub Assert: Box<assert::RSassert> = { pub Assert: Box<rsassert::RSassert> = {
// "label" "{" <f: AssertTree> "}" => "label" "{" <f: AssertTree> "}" =>
// Box::new(assert::RSassert{tree: f}), Box::new(rsassert::RSassert{tree: f}),
// }; };
// AssertTree: assert::Tree = { AssertTree: rsassert::Tree = {
// <t1: AssertTree2> ";" <t2: AssertTree> => <t1: AssertTree2> ";" <t2: AssertTree> =>
// assert::Tree::Concat(Box::new(t1), Box::new(t2)), rsassert::Tree::Concat(Box::new(t1), Box::new(t2)),
// <t: AssertTree2> => t, <t: AssertTree2> => t,
// } }
// AssertTree2: assert::Tree = { AssertTree2: rsassert::Tree = {
// "if" <e: AssertExpression> "if" <e: AssertExpression>
// "then" "{" <t: AssertTree> "}" => "then" "{" <t: AssertTree> "}" =>
// assert::Tree::If(Box::new(e), Box::new(t)), rsassert::Tree::If(Box::new(e), Box::new(t)),
// "if" <e: AssertExpression> "if" <e: AssertExpression>
// "then" "{" <t1: AssertTree> "}" "then" "{" <t1: AssertTree> "}"
// "else" "{" <t2: AssertTree> "}" => "else" "{" <t2: AssertTree> "}" =>
// assert::Tree::IfElse(Box::new(e), Box::new(t1), Box::new(t2)), rsassert::Tree::IfElse(Box::new(e), Box::new(t1), Box::new(t2)),
// "let" <v: AssertVariable> <q: AssertQualifierLet?> "=" <e: AssertExpression> => "let" <v: AssertVariable> <q: AssertQualifier?> "=" <e: AssertExpression> =>
// assert::Tree::Assignment(v, q, Box::new(e)), rsassert::Tree::Assignment(v, q, Box::new(e)),
// "return" <e: AssertExpression> => "return" <e: AssertExpression> =>
// assert::Tree::Return(Box::new(e)), rsassert::Tree::Return(Box::new(e)),
// "for" <v: AssertVariable> "in" <r: AssertRange> "{" <t: AssertTree> "}" => "for" <v: AssertVariable> "in" <r: AssertRange> "{" <t: AssertTree> "}" =>
// assert::Tree::For(v, r, Box::new(t)), rsassert::Tree::For(v, r, Box::new(t)),
// } }
// AssertQualifierLet: assert::Qualifier { AssertVariable: rsassert::Variable = {
// "Entities" => assert::QualifierRestricted::Entities, "label" => rsassert::Variable::Special(rsassert::Special::Label),
// "Context" => assert::QualifierRestricted::Context, "edge" => rsassert::Variable::Special(rsassert::Special::Edge),
// "Reactants" => assert::QualifierRestricted::Reactants, <v: Literal> => rsassert::Variable::Id(v),
// "ReactantsAbsent" => assert::QualifierRestricted::ReactantsAbsent, }
// "Inhibitors" => assert::QualifierRestricted::Inhibitors,
// "InhibitorsPresent" => assert::QualifierRestricted::InhibitorsPresent,
// "Products" => assert::QualifierRestricted::Products,
// }
// AssertAssignmentVar: assert::AssignmentVariable = {
// <v: AssertVariable> => assert::AssignmentVariable::Var(v),
// <v: AssertVariable> "." <q: AssertQualifierRestricted> =>
// assert::AssignmentVariable::QualifiedVar(v, q),
// }
// AssertVariable: assert::Variable = { AssertExpression: rsassert::Expression = {
// "label" => assert::Variable::Label, // Unary
// "edge" => assert::Variable::Edge, <unp: AssertUnaryPrefix> <e: AssertExpression> =>
// <v: Literal> => assert::Variable::Id(v), rsassert::Expression::Unary(unp, Box::new(e)),
// } "(" <e: AssertExpression> ")" <uns: AssertUnarySuffix> =>
rsassert::Expression::Unary(uns, Box::new(e)),
// AssertExpression: assert::Expression = { // binary
// <unp: AssertUnaryPrefix> <e: AssertExpression> => "(" <e1: AssertExpression> <b: AssertBinary> <e2: AssertExpression> ")" =>
// assert::Expression::Unary(unp, Box::new(e)), rsassert::Expression::Binary(b, Box::new(e1), Box::new(e2)),
// "(" <e: AssertExpression> ")" <uns: AssertUnarySuffix> => <b: AssertBinaryPrefix>
// assert::Expression::Unary(uns, Box::new(e)), "(" <e1: AssertExpression> "," <e2: AssertExpression> ")" =>
rsassert::Expression::Binary(b, Box::new(e1), Box::new(e2)),
// "(" <e1: AssertExpression> <b: AssertBinary> <e2: AssertExpression> ")" => "(" <e: AssertExpression> ")" => e,
// assert::Expression::Binary(b, Box::new(e1), Box::new(e2)), "true" => rsassert::Expression::True,
// <b: AssertBinaryPrefix> "false" => rsassert::Expression::False,
// "(" <e1: AssertExpression> "," <e2: AssertExpression> ")" =>
// assert::Expression::Binary(b, Box::new(e1), Box::new(e2)),
// "(" <e: AssertExpression> ")" => e, <v: AssertVariable> => rsassert::Expression::Var(v),
// "true" => assert::Expression::True,
// "false" => assert::Expression::False,
// <v: AssertAssignmentVar> => assert::Expression::Var(v), // If changing IntegerType in assert.rs, also change from Num to another
// similar parser with different return type
<i: Num> => rsassert::Expression::Integer(i),
// // If changing IntegerType in assert.rs, also change from Num to another <lab: AssertLabel> => rsassert::Expression::Label(Box::new(lab)),
// // similar parser with different return type <set: Set_of_entities> => rsassert::Expression::Set(set),
// <i: Num> => assert::Expression::Integer(i), "'" <el: Literal> "'" => rsassert::Expression::Element(translator.encode(el)),
// <lab: AssertLabel> => assert::Expression::Label(Box::new(lab)), // strings
// <set: Set_of_entities> => assert::Expression::Set(set), PATH => rsassert::Expression::String(<>.trim_end_matches("\"")
// "'" <el: Literal> "'" => assert::Expression::Element(translator.encode(el)), .trim_start_matches("\"")
.to_string()),
}
// // strings AssertRange: rsassert::Range = {
// PATH => assert::Expression::String(<>.trim_end_matches("\"") "{" <e: AssertExpression> "}" => rsassert::Range::IterateOverSet(Box::new(e)),
// .trim_start_matches("\"") "{" <e1: AssertExpression> ".." <e2: AssertExpression> "}" =>
// .to_string()), rsassert::Range::IterateInRange(Box::new(e1), Box::new(e2)),
// } }
// AssertUnaryPrefix: assert::Unary = { AssertUnaryPrefix: rsassert::Unary = {
// "not" => assert::Unary::Not, "not" => rsassert::Unary::Not,
// "rand" => assert::Unary::Rand, "rand" => rsassert::Unary::Rand,
// } }
// AssertUnarySuffix: assert::Unary = { AssertUnarySuffix: rsassert::Unary = {
// ".empty" => assert::Unary::Empty, ".empty" => rsassert::Unary::Empty,
// ".length" => assert::Unary::Length, ".length" => rsassert::Unary::Length,
// ".tostr" => assert::Unary::ToStr, ".tostr" => rsassert::Unary::ToStr,
// ".toel" => assert::Unary::ToEl, ".toel" => rsassert::Unary::ToEl,
// ".source" => assert::Unary::Source,
// ".target" => assert::Unary::Target,
// ".neighbours" => assert::Unary::Neighbours,
// ".system" => assert::Unary::System,
// "." <q: AssertQualifierLabel> => assert::Unary::QualifierLabel(q),
// "." <q: AssertQualifierSystem> => assert::Unary::QualifierSystem(q),
// }
// AssertBinary: assert::Binary = { "." <q: AssertQualifier> => rsassert::Unary::Qualifier(q),
// "&&" => assert::Binary::And, }
// "||" => assert::Binary::Or,
// "^^" => assert::Binary::Xor,
// "<" => assert::Binary::Less,
// "<=" => assert::Binary::LessEq,
// ">" => assert::Binary::More,
// ">=" => assert::Binary::MoreEq,
// "==" => assert::Binary::Eq,
// "!=" => assert::Binary::NotEq,
// "+" => assert::Binary::Plus,
// "-" => assert::Binary::Minus,
// "*" => assert::Binary::Times,
// "^" => assert::Binary::Exponential,
// "/" => assert::Binary::Quotient,
// "%" => assert::Binary::Reminder,
// "::" => assert::Binary::Concat,
// }
// AssertBinaryPrefix: assert::Binary = { AssertQualifierRestricted: rsassert::QualifierRestricted = {
// "substr" => assert::Binary::SubStr, "Entities" => rsassert::QualifierRestricted::Entities,
// "min" => assert::Binary::Min, "Context" => rsassert::QualifierRestricted::Context,
// "max" => assert::Binary::Max, "Reactants" => rsassert::QualifierRestricted::Reactants,
// "commonsubstr" => assert::Binary::CommonSubStr, "ReactantsAbsent" => rsassert::QualifierRestricted::ReactantsAbsent,
// } "Inhibitors" => rsassert::QualifierRestricted::Inhibitors,
"InhibitorsPresent" => rsassert::QualifierRestricted::InhibitorsPresent,
"Products" => rsassert::QualifierRestricted::Products,
}
// AssertQualifierSystem: assert::QualifierSystem = { AssertQualifierLabel: rsassert::QualifierLabel = {
// "SystemEntities" => assert::QualifierSystem::Entities, "AvailableEntities" => rsassert::QualifierLabel::AvailableEntities,
// "SystemContext" => assert::QualifierSystem::Context, "AllReactants" => rsassert::QualifierLabel::AllReactants,
// } "AllInhibitors" => rsassert::QualifierLabel::AllInhibitors,
}
// AssertQualifierLabel: assert::QualifierLabel = { AssertQualifierSystem: rsassert::QualifierSystem = {
// "AvailableEntities" => assert::QualifierLabel::AvailableEntities, "SystemEntities" => rsassert::QualifierSystem::Entities,
// "AllReactants" => assert::QualifierLabel::AllReactants, "SystemContext" => rsassert::QualifierSystem::Context,
// "AllInhibitors" => assert::QualifierLabel::AllInhibitors, }
// <q: AssertQualifierRestricted> => assert::QualifierLabel::Restricted(q),
// }
// AssertQualifierRestricted: assert::QualifierRestricted = { AssertQualifierEdge: rsassert::QualifierEdge = {
// "Entities" => assert::QualifierRestricted::Entities, "source" => rsassert::QualifierEdge::Source,
// "Context" => assert::QualifierRestricted::Context, "target" => rsassert::QualifierEdge::Target,
// "Reactants" => assert::QualifierRestricted::Reactants, }
// "ReactantsAbsent" => assert::QualifierRestricted::ReactantsAbsent,
// "Inhibitors" => assert::QualifierRestricted::Inhibitors,
// "InhibitorsPresent" => assert::QualifierRestricted::InhibitorsPresent,
// "Products" => assert::QualifierRestricted::Products,
// }
// AssertLabel: RSlabel = { AssertQualifierNode: rsassert::QualifierNode = {
// "[" "neighbours" => rsassert::QualifierNode::Neighbours,
// "Entities" ":" <e: Set_of_entities> "," "system" => rsassert::QualifierNode::System,
// "Context" ":" <c: Set_of_entities> "," }
// "Reactants" ":" <r: Set_of_entities> ","
// "ReactantsAbsent" ":" <r_a: Set_of_entities> ","
// "Inhibitors" ":" <i: Set_of_entities> ","
// "InhibitorsPresent" ":" <i_p: Set_of_entities> ","
// "Products" ":" <p: Set_of_entities> ","
// "]" => RSlabel::create(e, c, r, r_a, i, i_p, p)
// }
// AssertRange: assert::Range = { AssertQualifier: rsassert::Qualifier = {
// "{" <e: AssertExpression> "}" => assert::Range::IterateOverSet(Box::new(e)), <q: AssertQualifierSystem> => rsassert::Qualifier::System(q),
// "{" <e1: AssertExpression> ".." <e2: AssertExpression> "}" => <q: AssertQualifierLabel> => rsassert::Qualifier::Label(q),
// assert::Range::IterateInRange(Box::new(e1), Box::new(e2)), <q: AssertQualifierRestricted> => rsassert::Qualifier::Restricted(q),
// } <q: AssertQualifierEdge> => rsassert::Qualifier::Edge(q),
<q: AssertQualifierNode> => rsassert::Qualifier::Node(q),
}
AssertBinary: rsassert::Binary = {
"&&" => rsassert::Binary::And,
"||" => rsassert::Binary::Or,
"^^" => rsassert::Binary::Xor,
"<" => rsassert::Binary::Less,
"<=" => rsassert::Binary::LessEq,
">" => rsassert::Binary::More,
">=" => rsassert::Binary::MoreEq,
"==" => rsassert::Binary::Eq,
"!=" => rsassert::Binary::NotEq,
"+" => rsassert::Binary::Plus,
"-" => rsassert::Binary::Minus,
"*" => rsassert::Binary::Times,
"^" => rsassert::Binary::Exponential,
"/" => rsassert::Binary::Quotient,
"%" => rsassert::Binary::Reminder,
"::" => rsassert::Binary::Concat,
}
AssertBinaryPrefix: rsassert::Binary = {
"substr" => rsassert::Binary::SubStr,
"min" => rsassert::Binary::Min,
"max" => rsassert::Binary::Max,
"commonsubstr" => rsassert::Binary::CommonSubStr,
}
AssertLabel: RSlabel = {
"["
"Entities" ":" <e: Set_of_entities> ","
"Context" ":" <c: Set_of_entities> ","
"Reactants" ":" <r: Set_of_entities> ","
"ReactantsAbsent" ":" <r_a: Set_of_entities> ","
"Inhibitors" ":" <i: Set_of_entities> ","
"InhibitorsPresent" ":" <i_p: Set_of_entities> ","
"Products" ":" <p: Set_of_entities> ","
"]" => RSlabel::create(e, c, r, r_a, i, i_p, p)
}
// ----------------------------------------------------------------------------- // -----------------------------------------------------------------------------
// BHMLParser // BHMLParser
// ----------------------------------------------------------------------------- // -----------------------------------------------------------------------------
@ -738,13 +739,11 @@ Instruction: presets::Instruction = {
"Digraph" ">" <gso: Separated_Or<GraphSaveOptions, "|">> => "Digraph" ">" <gso: Separated_Or<GraphSaveOptions, "|">> =>
presets::Instruction::Digraph { gso }, presets::Instruction::Digraph { gso },
// <edge_relabeler: Assert> // <edge_relabeler: Assert>
"Bisimilarity" "(" <p: Path> ")" "relabel" "Bisimilarity" "(" <p: Path> ")" "relabel" <edge_relabeler: Assert>
">" <so: SaveOptions> => ">" <so: SaveOptions> =>
presets::Instruction::Bisimilarity { presets::Instruction::Bisimilarity {
system_b: p, system_b: p,
edge_relabeler: Box::new(assert::RSassert { edge_relabeler,
tree: assert::Tree::Return(Box::new(assert::Expression::True))
}),
so so
}, },
} }

8
src/rsprocess/structure.rs
View File

@ -620,13 +620,17 @@ impl Hash for RSlabel {
// ----------------------------------------------------------------------------- // -----------------------------------------------------------------------------
pub type RSassert = pub type RSassert =
crate::rsprocess::assert::dsl::RSassert< crate::rsprocess::assert::rsassert::useful_types_edge_relabeler::RSassert;
crate::rsprocess::assert::rsassert::EdgeRelablerInput>;
pub mod assert { pub mod assert {
pub use crate::rsprocess::assert::dsl::*; pub use crate::rsprocess::assert::dsl::*;
} }
/// Export of useful values from submodule of submodule
pub mod rsassert {
pub use crate::rsprocess::assert::rsassert::useful_types_edge_relabeler::*;
}
// ----------------------------------------------------------------------------- // -----------------------------------------------------------------------------
// RSBHML // RSBHML
// ----------------------------------------------------------------------------- // -----------------------------------------------------------------------------