diff --git a/src/rsprocess/assert/rsassert.rs b/src/rsprocess/assert/rsassert.rs index 6052a60..5c668a5 100644 --- a/src/rsprocess/assert/rsassert.rs +++ b/src/rsprocess/assert/rsassert.rs @@ -6,6 +6,33 @@ use std::collections::HashMap; // Specific Assert Implementation // ---------------------------------------------------------------------------- +pub mod useful_types_edge_relabeler { + macro_rules! export_types { + ( $( $x:ident ),* ) => { + $( + pub type $x = super::super::dsl::$x; + )* + }; + } + + 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. #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] @@ -15,7 +42,7 @@ pub enum EdgeRelablerInput { } #[derive(Debug, Clone)] -pub enum EdgeRelablerInputValues { +enum EdgeRelablerInputValues { Label(structure::RSlabel), Edge(petgraph::graph::EdgeIndex), } @@ -68,7 +95,6 @@ impl std::fmt::Display for EdgeRelablerInput { } } - impl RSassert { pub fn typecheck(&self) -> Result<(), String> { let mut context = TypeContext::new(); @@ -119,7 +145,9 @@ impl RSassert { } } +// ----------------------------------------------------------------------------- // Implementation for node grouping. +// ----------------------------------------------------------------------------- #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] pub enum NodeRelablerInput { @@ -128,7 +156,7 @@ pub enum NodeRelablerInput { } #[derive(Debug, Clone)] -pub enum NodeRelablerInputValues { +enum NodeRelablerInputValues { Entities(structure::RSset), Node(petgraph::graph::NodeIndex), } diff --git a/src/rsprocess/grammar.lalrpop b/src/rsprocess/grammar.lalrpop index f063697..b3d54fb 100644 --- a/src/rsprocess/grammar.lalrpop +++ b/src/rsprocess/grammar.lalrpop @@ -1,14 +1,14 @@ use std::rc::Rc; use std::str::FromStr; use lalrpop_util::ParseError; -use crate::rsprocess::structure::{RSset, - RSprocess, - RSenvironment, - RSsystem, -// RSlabel, - RSreaction}; -use crate::rsprocess::structure::assert; -use crate::rsprocess::translator::{Translator, IdType}; +use crate::rsprocess::structure::{ RSset, + RSprocess, + RSenvironment, + RSsystem, + RSlabel, + RSreaction }; +use crate::rsprocess::structure::rsassert; +use crate::rsprocess::translator::{ Translator, IdType }; use crate::rsprocess::presets::Instructions; use crate::rsprocess::presets; use crate::rsprocess::graph; @@ -180,176 +180,177 @@ Env_term: (IdType, RSprocess) = { // ----------------------------------------------------------------------------- // AssertParser // ----------------------------------------------------------------------------- -// pub Assert: Box = { -// "label" "{" "}" => -// Box::new(assert::RSassert{tree: f}), -// }; +pub Assert: Box = { + "label" "{" "}" => + Box::new(rsassert::RSassert{tree: f}), +}; -// AssertTree: assert::Tree = { -// ";" => -// assert::Tree::Concat(Box::new(t1), Box::new(t2)), -// => t, -// } +AssertTree: rsassert::Tree = { + ";" => + rsassert::Tree::Concat(Box::new(t1), Box::new(t2)), + => t, +} -// AssertTree2: assert::Tree = { -// "if" -// "then" "{" "}" => -// assert::Tree::If(Box::new(e), Box::new(t)), +AssertTree2: rsassert::Tree = { + "if" + "then" "{" "}" => + rsassert::Tree::If(Box::new(e), Box::new(t)), -// "if" -// "then" "{" "}" -// "else" "{" "}" => -// assert::Tree::IfElse(Box::new(e), Box::new(t1), Box::new(t2)), + "if" + "then" "{" "}" + "else" "{" "}" => + rsassert::Tree::IfElse(Box::new(e), Box::new(t1), Box::new(t2)), -// "let" "=" => -// assert::Tree::Assignment(v, q, Box::new(e)), + "let" "=" => + rsassert::Tree::Assignment(v, q, Box::new(e)), -// "return" => -// assert::Tree::Return(Box::new(e)), + "return" => + rsassert::Tree::Return(Box::new(e)), -// "for" "in" "{" "}" => -// assert::Tree::For(v, r, Box::new(t)), -// } + "for" "in" "{" "}" => + rsassert::Tree::For(v, r, Box::new(t)), +} -// AssertQualifierLet: assert::Qualifier { -// "Entities" => assert::QualifierRestricted::Entities, -// "Context" => assert::QualifierRestricted::Context, -// "Reactants" => assert::QualifierRestricted::Reactants, -// "ReactantsAbsent" => assert::QualifierRestricted::ReactantsAbsent, -// "Inhibitors" => assert::QualifierRestricted::Inhibitors, -// "InhibitorsPresent" => assert::QualifierRestricted::InhibitorsPresent, -// "Products" => assert::QualifierRestricted::Products, -// } +AssertVariable: rsassert::Variable = { + "label" => rsassert::Variable::Special(rsassert::Special::Label), + "edge" => rsassert::Variable::Special(rsassert::Special::Edge), + => rsassert::Variable::Id(v), +} -// AssertAssignmentVar: assert::AssignmentVariable = { -// => assert::AssignmentVariable::Var(v), -// "." => -// assert::AssignmentVariable::QualifiedVar(v, q), -// } -// AssertVariable: assert::Variable = { -// "label" => assert::Variable::Label, -// "edge" => assert::Variable::Edge, -// => assert::Variable::Id(v), -// } +AssertExpression: rsassert::Expression = { + // Unary + => + rsassert::Expression::Unary(unp, Box::new(e)), + "(" ")" => + rsassert::Expression::Unary(uns, Box::new(e)), -// AssertExpression: assert::Expression = { -// => -// assert::Expression::Unary(unp, Box::new(e)), -// "(" ")" => -// assert::Expression::Unary(uns, Box::new(e)), + // binary + "(" ")" => + rsassert::Expression::Binary(b, Box::new(e1), Box::new(e2)), + + "(" "," ")" => + rsassert::Expression::Binary(b, Box::new(e1), Box::new(e2)), -// "(" ")" => -// assert::Expression::Binary(b, Box::new(e1), Box::new(e2)), -// -// "(" "," ")" => -// assert::Expression::Binary(b, Box::new(e1), Box::new(e2)), + "(" ")" => e, + "true" => rsassert::Expression::True, + "false" => rsassert::Expression::False, -// "(" ")" => e, -// "true" => assert::Expression::True, -// "false" => assert::Expression::False, + => rsassert::Expression::Var(v), -// => assert::Expression::Var(v), + // If changing IntegerType in assert.rs, also change from Num to another + // similar parser with different return type + => rsassert::Expression::Integer(i), -// // If changing IntegerType in assert.rs, also change from Num to another -// // similar parser with different return type -// => assert::Expression::Integer(i), + => rsassert::Expression::Label(Box::new(lab)), + => rsassert::Expression::Set(set), + "'" "'" => rsassert::Expression::Element(translator.encode(el)), -// => assert::Expression::Label(Box::new(lab)), -// => assert::Expression::Set(set), -// "'" "'" => assert::Expression::Element(translator.encode(el)), + // strings + PATH => rsassert::Expression::String(<>.trim_end_matches("\"") + .trim_start_matches("\"") + .to_string()), +} -// // strings -// PATH => assert::Expression::String(<>.trim_end_matches("\"") -// .trim_start_matches("\"") -// .to_string()), -// } +AssertRange: rsassert::Range = { + "{" "}" => rsassert::Range::IterateOverSet(Box::new(e)), + "{" ".." "}" => + rsassert::Range::IterateInRange(Box::new(e1), Box::new(e2)), +} -// AssertUnaryPrefix: assert::Unary = { -// "not" => assert::Unary::Not, -// "rand" => assert::Unary::Rand, -// } +AssertUnaryPrefix: rsassert::Unary = { + "not" => rsassert::Unary::Not, + "rand" => rsassert::Unary::Rand, +} -// AssertUnarySuffix: assert::Unary = { -// ".empty" => assert::Unary::Empty, -// ".length" => assert::Unary::Length, -// ".tostr" => assert::Unary::ToStr, -// ".toel" => assert::Unary::ToEl, -// ".source" => assert::Unary::Source, -// ".target" => assert::Unary::Target, -// ".neighbours" => assert::Unary::Neighbours, -// ".system" => assert::Unary::System, -// "." => assert::Unary::QualifierLabel(q), -// "." => assert::Unary::QualifierSystem(q), -// } +AssertUnarySuffix: rsassert::Unary = { + ".empty" => rsassert::Unary::Empty, + ".length" => rsassert::Unary::Length, + ".tostr" => rsassert::Unary::ToStr, + ".toel" => rsassert::Unary::ToEl, -// AssertBinary: assert::Binary = { -// "&&" => 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, -// } + "." => rsassert::Unary::Qualifier(q), +} -// AssertBinaryPrefix: assert::Binary = { -// "substr" => assert::Binary::SubStr, -// "min" => assert::Binary::Min, -// "max" => assert::Binary::Max, -// "commonsubstr" => assert::Binary::CommonSubStr, -// } +AssertQualifierRestricted: rsassert::QualifierRestricted = { + "Entities" => rsassert::QualifierRestricted::Entities, + "Context" => rsassert::QualifierRestricted::Context, + "Reactants" => rsassert::QualifierRestricted::Reactants, + "ReactantsAbsent" => rsassert::QualifierRestricted::ReactantsAbsent, + "Inhibitors" => rsassert::QualifierRestricted::Inhibitors, + "InhibitorsPresent" => rsassert::QualifierRestricted::InhibitorsPresent, + "Products" => rsassert::QualifierRestricted::Products, +} -// AssertQualifierSystem: assert::QualifierSystem = { -// "SystemEntities" => assert::QualifierSystem::Entities, -// "SystemContext" => assert::QualifierSystem::Context, -// } +AssertQualifierLabel: rsassert::QualifierLabel = { + "AvailableEntities" => rsassert::QualifierLabel::AvailableEntities, + "AllReactants" => rsassert::QualifierLabel::AllReactants, + "AllInhibitors" => rsassert::QualifierLabel::AllInhibitors, +} -// AssertQualifierLabel: assert::QualifierLabel = { -// "AvailableEntities" => assert::QualifierLabel::AvailableEntities, -// "AllReactants" => assert::QualifierLabel::AllReactants, -// "AllInhibitors" => assert::QualifierLabel::AllInhibitors, -// => assert::QualifierLabel::Restricted(q), -// } +AssertQualifierSystem: rsassert::QualifierSystem = { + "SystemEntities" => rsassert::QualifierSystem::Entities, + "SystemContext" => rsassert::QualifierSystem::Context, +} -// AssertQualifierRestricted: assert::QualifierRestricted = { -// "Entities" => assert::QualifierRestricted::Entities, -// "Context" => assert::QualifierRestricted::Context, -// "Reactants" => assert::QualifierRestricted::Reactants, -// "ReactantsAbsent" => assert::QualifierRestricted::ReactantsAbsent, -// "Inhibitors" => assert::QualifierRestricted::Inhibitors, -// "InhibitorsPresent" => assert::QualifierRestricted::InhibitorsPresent, -// "Products" => assert::QualifierRestricted::Products, -// } +AssertQualifierEdge: rsassert::QualifierEdge = { + "source" => rsassert::QualifierEdge::Source, + "target" => rsassert::QualifierEdge::Target, +} -// AssertLabel: RSlabel = { -// "[" -// "Entities" ":" "," -// "Context" ":" "," -// "Reactants" ":" "," -// "ReactantsAbsent" ":" "," -// "Inhibitors" ":" "," -// "InhibitorsPresent" ":" "," -// "Products" ":" "," -// "]" => RSlabel::create(e, c, r, r_a, i, i_p, p) -// } +AssertQualifierNode: rsassert::QualifierNode = { + "neighbours" => rsassert::QualifierNode::Neighbours, + "system" => rsassert::QualifierNode::System, +} -// AssertRange: assert::Range = { -// "{" "}" => assert::Range::IterateOverSet(Box::new(e)), -// "{" ".." "}" => -// assert::Range::IterateInRange(Box::new(e1), Box::new(e2)), -// } +AssertQualifier: rsassert::Qualifier = { + => rsassert::Qualifier::System(q), + => rsassert::Qualifier::Label(q), + => rsassert::Qualifier::Restricted(q), + => rsassert::Qualifier::Edge(q), + => 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" ":" "," + "Context" ":" "," + "Reactants" ":" "," + "ReactantsAbsent" ":" "," + "Inhibitors" ":" "," + "InhibitorsPresent" ":" "," + "Products" ":" "," + "]" => RSlabel::create(e, c, r, r_a, i, i_p, p) +} + // ----------------------------------------------------------------------------- // BHMLParser // ----------------------------------------------------------------------------- @@ -738,13 +739,11 @@ Instruction: presets::Instruction = { "Digraph" ">" > => presets::Instruction::Digraph { gso }, // - "Bisimilarity" "(" ")" "relabel" + "Bisimilarity" "(" ")" "relabel" ">" => presets::Instruction::Bisimilarity { system_b: p, - edge_relabeler: Box::new(assert::RSassert { - tree: assert::Tree::Return(Box::new(assert::Expression::True)) - }), + edge_relabeler, so }, } diff --git a/src/rsprocess/structure.rs b/src/rsprocess/structure.rs index 252b3df..090b081 100644 --- a/src/rsprocess/structure.rs +++ b/src/rsprocess/structure.rs @@ -620,13 +620,17 @@ impl Hash for RSlabel { // ----------------------------------------------------------------------------- pub type RSassert = - crate::rsprocess::assert::dsl::RSassert< - crate::rsprocess::assert::rsassert::EdgeRelablerInput>; + crate::rsprocess::assert::rsassert::useful_types_edge_relabeler::RSassert; pub mod assert { 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 // -----------------------------------------------------------------------------