diff --git a/src/rsprocess/assert.rs b/src/rsprocess/assert.rs index 88afd07..717c470 100644 --- a/src/rsprocess/assert.rs +++ b/src/rsprocess/assert.rs @@ -4,29 +4,40 @@ type IntegerType = i64; #[derive(Debug, Clone)] -pub struct RSassert { - pub tree: Tree +pub struct RSassert { + pub tree: Tree } #[derive(Debug, Clone)] -pub enum Tree { - Concat(Box, Box), - If(Box, Box), - IfElse(Box, Box, Box), - Assignment(Variable, Option, Box), - Return(Box), - For(Variable, Range, Box), +pub enum Tree { + Concat(Box>, Box>), + If(Box>, Box>), + IfElse(Box>, Box>, Box>), + Assignment(Variable, Option, Box>), + Return(Box>), + For(Variable, Range, Box>), } #[derive(Debug, Clone, PartialEq, Eq, Hash)] -pub enum Variable { +pub enum Variable { Id(String), - Label, // special label that is the input of the function - Edge, // special edge that is the input of the function + Special(S) +} + +trait SpecialVariables: Display + std::fmt::Debug + Sized + Eq + Copy + + std::hash::Hash +{ + fn type_of(&self) -> AssertionTypes; + fn type_qualified(&self, q: &Qualifier) -> Result; + fn new_context(input: HashMap) + -> HashMap; + fn correct_type(&self, other: &AssertReturnValue) -> bool; + // fn correct_type_qualified(&self, q: &Qualifier, other: &AssertReturnValue) + // -> bool; } #[derive(Debug, Clone)] -pub enum Expression { +pub enum Expression { True, False, Integer(IntegerType), @@ -34,16 +45,16 @@ pub enum Expression { Set(super::structure::RSset), Element(super::translator::IdType), String(String), - Var(Variable), + Var(Variable), - Unary(Unary, Box), - Binary(Binary, Box, Box), + Unary(Unary, Box>), + Binary(Binary, Box>, Box>), } #[derive(Debug, Clone)] -pub enum Range { - IterateOverSet(Box), - IterateInRange(Box, Box), +pub enum Range { + IterateOverSet(Box>), + IterateInRange(Box>, Box>), } #[derive(Debug, Clone, Copy)] @@ -118,7 +129,56 @@ pub enum Binary { CommonSubStr, } +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +enum AssertionTypes { + Boolean, + Integer, + String, + Label, + Set, + Element, + System, + Context, + NoType, + RangeInteger, + RangeSet, + RangeNeighbours, + Node, + Edge, +} + +#[derive(Debug, Clone, Hash, PartialEq, Eq)] +pub enum AssertReturnValue { + Boolean(bool), + Integer(IntegerType), + String(String), + Label(super::structure::RSlabel), + Set(super::structure::RSset), + Element(super::translator::IdType), + Node(petgraph::graph::NodeIndex), + Edge(petgraph::graph::EdgeIndex), + Neighbours(petgraph::graph::NodeIndex), + System(super::structure::RSsystem), + Context(super::structure::RSprocess), +} + +impl AssertReturnValue { + pub fn assign_qualified(&mut self, q: Qualifier, val: AssertReturnValue) + -> Result<(), String> { + match (self, q, val) { + (Self::Label(l), + Qualifier::Restricted(q), + AssertReturnValue::Set(set)) => { + *q.referenced_mut(l) = set; + Ok(()) + }, + (s, q, val) => { + Err(format!("Cannot assign {val} to {s} with qualifier {q}")) + } + } + } +} @@ -390,9 +450,15 @@ impl Binary { (Self::Times, AssertionTypes::Set, AssertionTypes::Set) => { Ok(AssertionTypes::Set) }, - (Self::Exponential, AssertionTypes::Integer, AssertionTypes::Integer) | - (Self::Quotient, AssertionTypes::Integer, AssertionTypes::Integer) | - (Self::Reminder, AssertionTypes::Integer, AssertionTypes::Integer) => { + (Self::Exponential, + AssertionTypes::Integer, + AssertionTypes::Integer) | + (Self::Quotient, + AssertionTypes::Integer, + AssertionTypes::Integer) | + (Self::Reminder, + AssertionTypes::Integer, + AssertionTypes::Integer) => { Ok(AssertionTypes::Integer) }, (Self::Concat, AssertionTypes::String, AssertionTypes::String) => { @@ -405,7 +471,9 @@ impl Binary { (Self::Max, AssertionTypes::Integer, AssertionTypes::Integer) => { Ok(AssertionTypes::Integer) }, - (Self::CommonSubStr, AssertionTypes::String, AssertionTypes::String) => { + (Self::CommonSubStr, + AssertionTypes::String, + AssertionTypes::String) => { Ok(AssertionTypes::String) }, _ => { @@ -420,7 +488,7 @@ impl Binary { // ----------------------------------------------------------------------------- use std::collections::HashMap; -use std::fmt; +use std::fmt::{self, Display}; use petgraph::visit::EdgeRef; @@ -429,6 +497,11 @@ struct TypeContext { return_ty: Option } +struct Context { + data: HashMap, + special: HashMap, +} + impl TypeContext { fn new() -> Self { TypeContext { @@ -437,12 +510,32 @@ impl TypeContext { } } - fn assign( + fn return_type( &mut self, - v: &Variable, - q: Option<&Qualifier>, ty: AssertionTypes ) -> Result<(), String> { + if let Some(ty_return) = self.return_ty { + if ty_return == ty { + Ok(()) + } else { + Err(format!("Return statements don't agree: {ty_return} and \ + {ty} found.")) + } + } else { + self.return_ty = Some(ty); + Ok(()) + } + } +} + +impl TypeContext { + fn assign( + &mut self, + v: &Variable, + q: Option<&Qualifier>, + ty: AssertionTypes + ) -> Result<(), String> + where S: SpecialVariables { match (v, q) { (Variable::Id(v), None) => { self.data.insert(v.clone(), ty); @@ -471,68 +564,36 @@ impl TypeContext { } } }, - (Variable::Label, None) => { - if let AssertionTypes::Label = ty { + (Variable::Special(s), None) => { + if s.type_of() == ty { Ok(()) } else { - Err(format!("Variable label has type label but was \ - assigned a value of type {ty}.")) + Err(format!("Variable {s} has type {} but was \ + assigned a value of type {ty}.", s.type_of())) } - } - (Variable::Label, Some(q)) => { - match (q, ty) { - (Qualifier::Restricted(_), - AssertionTypes::Set) => { - Ok(()) - }, - (q, ty) => { - Err(format!("Variable label has type label, but \ - was assigned with qualifier {q} \ - value with type {ty}")) - } - } - } - (Variable::Edge, None) => { - if let AssertionTypes::Edge = ty { + }, + (Variable::Special(s), Some(q)) => { + if s.type_qualified(q)? == ty { Ok(()) } else { - Err(format!("Variable egde has type edge but was \ - assigned a value of type {ty}.")) + Err(format!("Variable {s} has type {} but was \ + assigned a value of type {ty} with qualifier \ + {q}.", s.type_of())) } } - (Variable::Edge, Some(q)) => { - Err(format!("Variable egde has type edge but was qualified \ - with qualifier {q}.")) - } } } - fn return_type( + fn assign_range( &mut self, + v: &Variable, ty: AssertionTypes - ) -> Result<(), String> { - if let Some(ty_return) = self.return_ty { - if ty_return == ty { - Ok(()) - } else { - Err(format!("Return statements don't agree: {ty_return} and \ - {ty} found.")) - } - } else { - self.return_ty = Some(ty); - Ok(()) - } - } - - fn assign_range( - &mut self, - v: &Variable, - ty: AssertionTypes - ) -> Result<(), String> { + ) -> Result<(), String> + where S: SpecialVariables { let v = match v { - Variable::Label | - Variable::Edge => return Err("Protected word label used in for \ - assignment.".into()), + Variable::Special(s) => + return Err(format!("Protected word {s} used in for \ + assignment.")), Variable::Id(v) => v }; match ty { @@ -554,16 +615,14 @@ impl TypeContext { } } - fn get( + fn get( &self, - v: &Variable, - ) -> Result { + v: &Variable, + ) -> Result + where S: SpecialVariables { match v { - Variable::Label => { - Ok(AssertionTypes::Label) - }, - Variable::Edge => { - Ok(AssertionTypes::Edge) + Variable::Special(s) => { + Ok(s.type_of()) }, Variable::Id(v) => { if let Some(ty) = self.data.get(v) { @@ -576,28 +635,22 @@ impl TypeContext { } } -struct Context { - data: HashMap, - label: super::structure::RSlabel, - edge: petgraph::graph::EdgeIndex, -} - -impl Context { - fn new( - label: &super::structure::RSlabel, - edge: &petgraph::graph::EdgeIndex, - ) -> Self { +impl Context { + fn new( + input: HashMap, + ) -> Self + where S: SpecialVariables { Self { data: HashMap::new(), - label: label.clone(), - edge: *edge } + special: S::new_context(input) } } - fn assign( + fn assign( &mut self, - v: &Variable, + v: &Variable, q: Option<&Qualifier>, val: AssertReturnValue, - ) -> Result<(), String> { + ) -> Result<(), String> + where S: SpecialVariables { match (v, q) { (Variable::Id(v), None) => { self.data.insert(v.clone(), val); @@ -627,94 +680,50 @@ impl Context { } } }, - (Variable::Edge, None) => { - if let AssertReturnValue::Edge(e) = val { - self.edge = e; - Ok(()) - } else { - Err(format!("Trying to assign {val} to variable edge.")) - } - } - (Variable::Edge, Some(q)) => { - Err(format!("No assignment on {q} for variable edge.")) - } - (Variable::Label, None) => { - if let AssertReturnValue::Label(l) = val { - self.label = l.clone(); - Ok(()) - } else { - Err(format!("Trying to assign {val} to variable label.")) - } - } - (Variable::Label, Some(q)) => { - match (q, val) { - (Qualifier::Restricted(q), AssertReturnValue::Set(set)) => { - *q.referenced_mut(&mut self.label) = set; - Ok(()) - }, - (q, newval) => { - Err(format!("Variable label could not be assigned with \ - qualifier {q} new value {newval}.")) + (Variable::Special(s), None) => { + if s.correct_type(&val) { + if let Some(s) = self.special.get_mut(s) { + *s = val; + } else { + self.special.insert(*s, val); } + Ok(()) + } else { + Err(format!("Trying to assign {val} to variable {s}.")) + } + }, + (Variable::Special(s), Some(q)) => { + if let Some(s) = self.special.get_mut(s) { + s.assign_qualified(*q, val) + } else { + Err(format!("Trying to assign {val} to variable {s} with \ + qualifier {q} but no value for {val} was found\ + .")) } } } } - fn get( + fn get( &self, - v: &Variable, - ) -> Result { + v: &Variable, + ) -> Result + where S: SpecialVariables { match v { Variable::Id(var) => { self.data.get(var) .cloned() .ok_or(format!("Variable {v} used, but no value assigned.")) }, - Variable::Label => { - Ok(AssertReturnValue::Label(self.label.clone())) - }, - Variable::Edge => { - Ok(AssertReturnValue::Edge(self.edge)) + Variable::Special(s) => { + self.special.get(s) + .cloned() + .ok_or(format!("Variable {v} used but no value assigned.")) }, } } } -#[derive(Copy, Clone, PartialEq, Eq)] -enum AssertionTypes { - Boolean, - Integer, - String, - Label, - Set, - Element, - System, - Context, - NoType, - RangeInteger, - RangeSet, - RangeNeighbours, - - Node, - Edge, -} - -#[derive(Debug, Clone, Hash, PartialEq, Eq)] -pub enum AssertReturnValue { - Boolean(bool), - Integer(IntegerType), - String(String), - Label(super::structure::RSlabel), - Set(super::structure::RSset), - Element(super::translator::IdType), - Node(petgraph::graph::NodeIndex), - Edge(petgraph::graph::EdgeIndex), - Neighbours(petgraph::graph::NodeIndex), - System(super::structure::RSsystem), - Context(super::structure::RSprocess), -} - impl AssertReturnValue { fn unary( self, @@ -878,10 +887,11 @@ impl AssertReturnValue { } } -fn typecheck( - tree: &Tree, +fn typecheck( + tree: &Tree, c: &mut TypeContext ) -> Result +where S: SpecialVariables { match tree { Tree::Concat(t1, t2) => { @@ -928,10 +938,11 @@ fn typecheck( } } -fn typecheck_expression( - exp: &Expression, +fn typecheck_expression( + exp: &Expression, c: &TypeContext -) -> Result { +) -> Result +where S: SpecialVariables { match exp { Expression::True | Expression::False => Ok(AssertionTypes::Boolean), @@ -956,10 +967,11 @@ fn typecheck_expression( } -fn typecheck_range( - range: &Range, +fn typecheck_range( + range: &Range, c: &mut TypeContext -) -> Result { +) -> Result +where S: SpecialVariables { match range { Range::IterateInRange(exp1, exp2) => { let type_exp1 = typecheck_expression(exp1, c)?; @@ -987,12 +999,13 @@ fn typecheck_range( } } -fn execute( - tree: &Tree, - c: &mut Context, +fn execute( + tree: &Tree, + c: &mut Context, translator: &mut super::translator::Translator, graph: &super::graph::RSgraph, -) -> Result, String> { +) -> Result, String> +where S: SpecialVariables { match tree { Tree::Concat(t1, t2) => { if let Some(val) = execute(t1, c, translator, graph)? { @@ -1040,12 +1053,13 @@ fn execute( type RangeIterator = std::vec::IntoIter; -fn range_into_iter( - range: &Range, - c: &mut Context, +fn range_into_iter( + range: &Range, + c: &mut Context, translator: &mut super::translator::Translator, graph: &super::graph::RSgraph, -) -> Result { +) -> Result +where S: SpecialVariables { match range { Range::IterateOverSet(exp) => { let val = execute_exp(exp, c, translator, graph)?; @@ -1083,12 +1097,13 @@ fn range_into_iter( } } -fn execute_exp( - exp: &Expression, - c: &Context, +fn execute_exp( + exp: &Expression, + c: &Context, translator: &mut super::translator::Translator, graph: &super::graph::RSgraph, -) -> Result { +) -> Result +where S: SpecialVariables { match exp { Expression::True => Ok(AssertReturnValue::Boolean(true)), Expression::False => Ok(AssertReturnValue::Boolean(false)), @@ -1111,7 +1126,90 @@ fn execute_exp( } } -impl RSassert { + + + + + +// ---------------------------------------------------------------------------- +// Specific Assert Implementation +// ---------------------------------------------------------------------------- + +#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)] +pub enum EdgeRelablerInput { + Label, + Edge, +} + +#[derive(Debug, Clone)] +pub enum EdgeRelablerInputValues { + Label(super::structure::RSlabel), + Edge(petgraph::graph::EdgeIndex), +} + +impl SpecialVariables for EdgeRelablerInput { + fn type_of(&self) -> AssertionTypes { + match self { + Self::Edge => AssertionTypes::Edge, + Self::Label => AssertionTypes::Label, + } + } + + fn type_qualified(&self, q: &Qualifier) -> Result { + match (self, q) { + (Self::Label, Qualifier::Label(_)) | + (Self::Label, Qualifier::Restricted(_)) => + Ok(AssertionTypes::Set), + (s, q) => + Err(format!("Wrong use of qualifier {q} on value {s}")) + } + } + + fn new_context(input: HashMap) + -> HashMap { + input.iter().map(|(key, value)| { + match value { + EdgeRelablerInputValues::Edge(e) => + (*key, AssertReturnValue::Edge(*e)), + EdgeRelablerInputValues::Label(l) => + (*key, AssertReturnValue::Label(l.clone())), + } + }).collect::>() + } + + fn correct_type(&self, other: &AssertReturnValue) -> bool { + match (self, other) { + (Self::Edge, AssertReturnValue::Edge(_)) | + (Self::Label, AssertReturnValue::Label(_)) => true, + (_, _) => false + } + } + + // fn correct_type_qualified(&self, q: &Qualifier, other: &AssertReturnValue) + // -> bool { + // match (self, q, other) { + // (Self::Label, Qualifier::Label(_), AssertReturnValue::Set(_)) | + // (Self::Label, Qualifier::Restricted(_), AssertReturnValue::Set(_)) + // => true, + // (_, _, _) => false + // } + // } +} + +impl Display for EdgeRelablerInput { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::Label => write!(f, "label"), + Self::Edge => write!(f, "edge"), + } + } +} + + + + + +impl RSassert { pub fn typecheck(&self) -> Result<(), String> { let mut context = TypeContext::new(); typecheck(&self.tree, &mut context)?; @@ -1143,7 +1241,14 @@ impl RSassert { translator: &mut super::translator::Translator, ) -> Result { let label = graph.edge_weight(*edge).unwrap(); - let mut context = Context::new(label, edge); + + let mut input_vals = HashMap::new(); + input_vals.insert(EdgeRelablerInput::Edge, + EdgeRelablerInputValues::Edge(*edge)); + input_vals.insert(EdgeRelablerInput::Label, + EdgeRelablerInputValues::Label(label.clone())); + + let mut context = Context::new(input_vals); if let Some(v) = execute(&self.tree, &mut context, translator, graph)? { Ok(v) } else { diff --git a/src/rsprocess/assert_fmt.rs b/src/rsprocess/assert_fmt.rs index fdcd952..06ec837 100644 --- a/src/rsprocess/assert_fmt.rs +++ b/src/rsprocess/assert_fmt.rs @@ -2,13 +2,13 @@ // Display Implementation for all types // ----------------------------------------------------------------------------- -impl fmt::Display for RSassert { +impl fmt::Display for RSassert where S: Display { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { write!(f, "label {{\n{}\n}}", self.tree) } } -impl fmt::Display for Tree { +impl fmt::Display for Tree where S: Display { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { Self::Concat(t1, t2) => {write!(f, "{t1};\n{t2}")}, @@ -29,17 +29,16 @@ impl fmt::Display for Tree { } } -impl fmt::Display for Variable { +impl fmt::Display for Variable where S: Display { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { - Self::Label => {write!(f, "label")}, - Self::Edge => {write!(f, "edge")}, + Self::Special(s) => {write!(f, "{s}")}, Self::Id(s) => {write!(f, "{s}")} } } } -impl fmt::Display for Expression { +impl fmt::Display for Expression where S: Display { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { Self::True => {write!(f, "True")}, @@ -74,7 +73,7 @@ impl fmt::Display for Expression { } } -impl fmt::Display for Range { +impl fmt::Display for Range where S: Display { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { Self::IterateOverSet(exp) => {write!(f, "{{{exp}}}")}, diff --git a/src/rsprocess/assert_tests.rs b/src/rsprocess/assert_tests.rs index 7426ad4..4a95e97 100644 --- a/src/rsprocess/assert_tests.rs +++ b/src/rsprocess/assert_tests.rs @@ -1322,7 +1322,9 @@ fn assert_tycheck_for_8() { Unary::Neighbours, Box::new(Expression::Unary( Unary::Source, - Box::new(Expression::Var(Variable::Edge)) + Box::new(Expression::Var( + Variable::Special(EdgeRelablerInput::Edge) + )) )) )) )), @@ -1402,7 +1404,9 @@ fn assert_tycheck_system() { Unary::System, Box::new(Expression::Unary( Unary::Target, - Box::new(Expression::Var(Variable::Edge)) + Box::new(Expression::Var( + Variable::Special(EdgeRelablerInput::Edge) + )) )) )) )) diff --git a/src/rsprocess/graph.rs b/src/rsprocess/graph.rs index 306836b..385fff8 100644 --- a/src/rsprocess/graph.rs +++ b/src/rsprocess/graph.rs @@ -128,7 +128,7 @@ where { fn map_edges( &self, - edge_map: &super::assert::RSassert, + edge_map: &super::structure::RSassert, translator: &mut super::translator::Translator ) -> Result, String>; } @@ -138,7 +138,7 @@ impl<'a> MapEdges<'a, RSsystem, RSlabel, Directed, u32> { fn map_edges( &self, - edge_map: &super::assert::RSassert, + edge_map: &super::structure::RSassert, translator: &mut super::translator::Translator )-> Result, String> { use petgraph::graph::EdgeIndex; diff --git a/src/rsprocess/presets.rs b/src/rsprocess/presets.rs index 7dd9feb..155f40e 100644 --- a/src/rsprocess/presets.rs +++ b/src/rsprocess/presets.rs @@ -89,7 +89,7 @@ pub enum Instruction { FastFrequency { experiment: String, so: SaveOptions }, Digraph { gso: Vec }, Bisimilarity { system_b: String, - edge_relabeler: Box, + edge_relabeler: Box, so: SaveOptions } } @@ -499,7 +499,7 @@ pub fn digraph(system: &mut EvaluatedSystem) -> Result<(), String> { /// Computes bisimularity of two provided systems pub fn bisimilar( system_a: &mut EvaluatedSystem, - edge_relabeler: &super::assert::RSassert, + edge_relabeler: &super::structure::RSassert, system_b: String ) -> Result { diff --git a/src/rsprocess/structure.rs b/src/rsprocess/structure.rs index e7914e3..e169586 100644 --- a/src/rsprocess/structure.rs +++ b/src/rsprocess/structure.rs @@ -619,7 +619,9 @@ impl Hash for RSlabel { // RSassert // ----------------------------------------------------------------------------- -pub use crate::rsprocess::assert::RSassert; +pub type RSassert = + crate::rsprocess::assert::RSassert< + crate::rsprocess::assert::EdgeRelablerInput>; pub mod assert { pub use crate::rsprocess::assert::*; @@ -636,6 +638,6 @@ pub enum RSBHML { False, Or(Vec), And(Vec), - Diamond(Box, Box), - Box(Box, Box), + // Diamond(Box, Box), + // Box(Box, Box), }