Refactoring and adding node grouping functionality
This commit is contained in:
@ -29,8 +29,8 @@ pub enum Variable<S> {
|
|||||||
}
|
}
|
||||||
|
|
||||||
/// Trait needed for special variables.
|
/// Trait needed for special variables.
|
||||||
trait SpecialVariables<G>: std::fmt::Display + std::fmt::Debug + Sized + Eq
|
pub(super) trait SpecialVariables<G>: std::fmt::Display + std::fmt::Debug
|
||||||
+ Copy + std::hash::Hash
|
+ Sized + Eq + Copy + std::hash::Hash
|
||||||
{
|
{
|
||||||
/// Returns the type of the specific special variable.
|
/// Returns the type of the specific special variable.
|
||||||
fn type_of(&self) -> AssertionTypes;
|
fn type_of(&self) -> AssertionTypes;
|
||||||
@ -504,18 +504,18 @@ impl AssertReturnValue {
|
|||||||
// Typechecking and Evaluation
|
// Typechecking and Evaluation
|
||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
|
|
||||||
struct TypeContext {
|
pub(super) struct TypeContext {
|
||||||
data: HashMap<String, AssertionTypes>,
|
data: HashMap<String, AssertionTypes>,
|
||||||
return_ty: Option<AssertionTypes>
|
return_ty: Option<AssertionTypes>
|
||||||
}
|
}
|
||||||
|
|
||||||
struct Context<S> {
|
pub(super) struct Context<S> {
|
||||||
data: HashMap<String, AssertReturnValue>,
|
data: HashMap<String, AssertReturnValue>,
|
||||||
special: HashMap<S, AssertReturnValue>,
|
special: HashMap<S, AssertReturnValue>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl TypeContext {
|
impl TypeContext {
|
||||||
fn new() -> Self {
|
pub(super) fn new() -> Self {
|
||||||
TypeContext {
|
TypeContext {
|
||||||
data: HashMap::new(),
|
data: HashMap::new(),
|
||||||
return_ty: None
|
return_ty: None
|
||||||
@ -648,7 +648,7 @@ impl TypeContext {
|
|||||||
}
|
}
|
||||||
|
|
||||||
impl<S> Context<S> {
|
impl<S> Context<S> {
|
||||||
fn new<G>(
|
pub(super) fn new<G>(
|
||||||
input: HashMap<S, G>,
|
input: HashMap<S, G>,
|
||||||
) -> Self
|
) -> Self
|
||||||
where S: SpecialVariables<G> {
|
where S: SpecialVariables<G> {
|
||||||
@ -903,7 +903,7 @@ impl AssertReturnValue {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn typecheck<S, G>(
|
fn typecheck_helper<S, G>(
|
||||||
tree: &Tree<S>,
|
tree: &Tree<S>,
|
||||||
c: &mut TypeContext
|
c: &mut TypeContext
|
||||||
) -> Result<AssertionTypes, String>
|
) -> Result<AssertionTypes, String>
|
||||||
@ -911,8 +911,8 @@ where S: SpecialVariables<G>
|
|||||||
{
|
{
|
||||||
match tree {
|
match tree {
|
||||||
Tree::Concat(t1, t2) => {
|
Tree::Concat(t1, t2) => {
|
||||||
typecheck(t1, c)?;
|
typecheck_helper(t1, c)?;
|
||||||
typecheck(t2, c)
|
typecheck_helper(t2, c)
|
||||||
},
|
},
|
||||||
Tree::If(exp, t) => {
|
Tree::If(exp, t) => {
|
||||||
match typecheck_expression(exp, c)? {
|
match typecheck_expression(exp, c)? {
|
||||||
@ -920,7 +920,7 @@ where S: SpecialVariables<G>
|
|||||||
_ => {return Err("Expression in if statement doesn't return a \
|
_ => {return Err("Expression in if statement doesn't return a \
|
||||||
boolean.".to_string())}
|
boolean.".to_string())}
|
||||||
};
|
};
|
||||||
typecheck(t, c)
|
typecheck_helper(t, c)
|
||||||
},
|
},
|
||||||
Tree::IfElse(exp, t1, t2) => {
|
Tree::IfElse(exp, t1, t2) => {
|
||||||
match typecheck_expression(exp, c)? {
|
match typecheck_expression(exp, c)? {
|
||||||
@ -928,8 +928,8 @@ where S: SpecialVariables<G>
|
|||||||
_ => {return Err("Expression in if statement doesn't return a \
|
_ => {return Err("Expression in if statement doesn't return a \
|
||||||
boolean.".into())}
|
boolean.".into())}
|
||||||
};
|
};
|
||||||
let type_t1 = typecheck(t1, c)?;
|
let type_t1 = typecheck_helper(t1, c)?;
|
||||||
let type_t2 = typecheck(t2, c)?;
|
let type_t2 = typecheck_helper(t2, c)?;
|
||||||
if type_t1 == type_t2 {
|
if type_t1 == type_t2 {
|
||||||
Ok(type_t1)
|
Ok(type_t1)
|
||||||
} else {
|
} else {
|
||||||
@ -949,11 +949,21 @@ where S: SpecialVariables<G>
|
|||||||
Tree::For(var, range, t) => {
|
Tree::For(var, range, t) => {
|
||||||
let type_range = typecheck_range(range, c)?;
|
let type_range = typecheck_range(range, c)?;
|
||||||
c.assign_range(var, type_range)?;
|
c.assign_range(var, type_range)?;
|
||||||
typecheck(t, c)
|
typecheck_helper(t, c)
|
||||||
},
|
},
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub(super) fn typecheck<S, G>(
|
||||||
|
tree: &Tree<S>,
|
||||||
|
c: &mut TypeContext
|
||||||
|
) -> Result<AssertionTypes, String>
|
||||||
|
where S: SpecialVariables<G>
|
||||||
|
{
|
||||||
|
typecheck_helper(tree, c)?;
|
||||||
|
Ok(c.return_ty.unwrap_or(AssertionTypes::NoType))
|
||||||
|
}
|
||||||
|
|
||||||
fn typecheck_expression<S, G>(
|
fn typecheck_expression<S, G>(
|
||||||
exp: &Expression<S>,
|
exp: &Expression<S>,
|
||||||
c: &TypeContext
|
c: &TypeContext
|
||||||
@ -1015,7 +1025,7 @@ where S: SpecialVariables<G> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn execute<S, G>(
|
pub(super) fn execute<S, G>(
|
||||||
tree: &Tree<S>,
|
tree: &Tree<S>,
|
||||||
c: &mut Context<S>,
|
c: &mut Context<S>,
|
||||||
translator: &mut translator::Translator,
|
translator: &mut translator::Translator,
|
||||||
@ -1143,121 +1153,3 @@ where S: SpecialVariables<G> {
|
|||||||
},
|
},
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
// ----------------------------------------------------------------------------
|
|
||||||
// Specific Assert Implementation
|
|
||||||
// ----------------------------------------------------------------------------
|
|
||||||
|
|
||||||
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
|
|
||||||
pub enum EdgeRelablerInput {
|
|
||||||
Label,
|
|
||||||
Edge,
|
|
||||||
}
|
|
||||||
|
|
||||||
#[derive(Debug, Clone)]
|
|
||||||
pub enum EdgeRelablerInputValues {
|
|
||||||
Label(structure::RSlabel),
|
|
||||||
Edge(petgraph::graph::EdgeIndex),
|
|
||||||
}
|
|
||||||
|
|
||||||
impl SpecialVariables<EdgeRelablerInputValues> for EdgeRelablerInput {
|
|
||||||
fn type_of(&self) -> AssertionTypes {
|
|
||||||
match self {
|
|
||||||
Self::Edge => AssertionTypes::Edge,
|
|
||||||
Self::Label => AssertionTypes::Label,
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
fn type_qualified(&self, q: &Qualifier) -> Result<AssertionTypes, String> {
|
|
||||||
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<Self, EdgeRelablerInputValues>)
|
|
||||||
-> HashMap<Self, AssertReturnValue> {
|
|
||||||
input.iter().map(|(key, value)| {
|
|
||||||
match value {
|
|
||||||
EdgeRelablerInputValues::Edge(e) =>
|
|
||||||
(*key, AssertReturnValue::Edge(*e)),
|
|
||||||
EdgeRelablerInputValues::Label(l) =>
|
|
||||||
(*key, AssertReturnValue::Label(l.clone())),
|
|
||||||
}
|
|
||||||
}).collect::<HashMap<Self, AssertReturnValue>>()
|
|
||||||
}
|
|
||||||
|
|
||||||
fn correct_type(&self, other: &AssertReturnValue) -> bool {
|
|
||||||
match (self, other) {
|
|
||||||
(Self::Edge, AssertReturnValue::Edge(_)) |
|
|
||||||
(Self::Label, AssertReturnValue::Label(_)) => true,
|
|
||||||
(_, _) => false
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl std::fmt::Display for EdgeRelablerInput {
|
|
||||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
|
||||||
match self {
|
|
||||||
Self::Label => write!(f, "label"),
|
|
||||||
Self::Edge => write!(f, "edge"),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
impl RSassert<EdgeRelablerInput> {
|
|
||||||
pub fn typecheck(&self) -> Result<(), String> {
|
|
||||||
let mut context = TypeContext::new();
|
|
||||||
typecheck(&self.tree, &mut context)?;
|
|
||||||
let ty = context.return_ty.unwrap_or(AssertionTypes::NoType);
|
|
||||||
match ty {
|
|
||||||
AssertionTypes::Boolean |
|
|
||||||
AssertionTypes::Integer |
|
|
||||||
AssertionTypes::String |
|
|
||||||
AssertionTypes::Label |
|
|
||||||
AssertionTypes::Set |
|
|
||||||
AssertionTypes::Element |
|
|
||||||
AssertionTypes::Edge |
|
|
||||||
AssertionTypes::Node |
|
|
||||||
AssertionTypes::System |
|
|
||||||
AssertionTypes::Context =>
|
|
||||||
Ok(()),
|
|
||||||
AssertionTypes::NoType |
|
|
||||||
AssertionTypes::RangeInteger |
|
|
||||||
AssertionTypes::RangeSet |
|
|
||||||
AssertionTypes::RangeNeighbours =>
|
|
||||||
Err(format!("Returned type {ty} is not a valid return type.")),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub fn execute(
|
|
||||||
&self,
|
|
||||||
graph: &graph::RSgraph,
|
|
||||||
edge: &<graph::RSgraph as petgraph::visit::GraphBase>::EdgeId,
|
|
||||||
translator: &mut translator::Translator,
|
|
||||||
) -> Result<AssertReturnValue, String> {
|
|
||||||
let label = graph.edge_weight(*edge).unwrap();
|
|
||||||
|
|
||||||
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 {
|
|
||||||
Err("No value returned.".into())
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|||||||
@ -1,4 +1,5 @@
|
|||||||
pub mod dsl;
|
pub mod dsl;
|
||||||
|
pub mod rsassert;
|
||||||
|
|
||||||
mod fmt;
|
mod fmt;
|
||||||
|
|
||||||
|
|||||||
230
src/rsprocess/assert/rsassert.rs
Normal file
230
src/rsprocess/assert/rsassert.rs
Normal file
@ -0,0 +1,230 @@
|
|||||||
|
use super::dsl::*;
|
||||||
|
use super::super::{structure, translator, graph};
|
||||||
|
use std::collections::HashMap;
|
||||||
|
|
||||||
|
// ----------------------------------------------------------------------------
|
||||||
|
// Specific Assert Implementation
|
||||||
|
// ----------------------------------------------------------------------------
|
||||||
|
|
||||||
|
// Implementation for graph labeling in bisimulation.
|
||||||
|
|
||||||
|
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
|
||||||
|
pub enum EdgeRelablerInput {
|
||||||
|
Label,
|
||||||
|
Edge,
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone)]
|
||||||
|
pub enum EdgeRelablerInputValues {
|
||||||
|
Label(structure::RSlabel),
|
||||||
|
Edge(petgraph::graph::EdgeIndex),
|
||||||
|
}
|
||||||
|
|
||||||
|
impl SpecialVariables<EdgeRelablerInputValues> for EdgeRelablerInput {
|
||||||
|
fn type_of(&self) -> AssertionTypes {
|
||||||
|
match self {
|
||||||
|
Self::Edge => AssertionTypes::Edge,
|
||||||
|
Self::Label => AssertionTypes::Label,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn type_qualified(&self, q: &Qualifier) -> Result<AssertionTypes, String> {
|
||||||
|
match (self, q) {
|
||||||
|
(Self::Label, Qualifier::Label(_)) |
|
||||||
|
(Self::Label, Qualifier::Restricted(_)) =>
|
||||||
|
Ok(AssertionTypes::Set),
|
||||||
|
(s, q) =>
|
||||||
|
Err(format!("Wrong use of qualifier {q} on variable {s}."))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn new_context(input: HashMap<Self, EdgeRelablerInputValues>)
|
||||||
|
-> HashMap<Self, AssertReturnValue> {
|
||||||
|
input.iter().map(|(key, value)| {
|
||||||
|
match value {
|
||||||
|
EdgeRelablerInputValues::Edge(e) =>
|
||||||
|
(*key, AssertReturnValue::Edge(*e)),
|
||||||
|
EdgeRelablerInputValues::Label(l) =>
|
||||||
|
(*key, AssertReturnValue::Label(l.clone())),
|
||||||
|
}
|
||||||
|
}).collect::<HashMap<Self, AssertReturnValue>>()
|
||||||
|
}
|
||||||
|
|
||||||
|
fn correct_type(&self, other: &AssertReturnValue) -> bool {
|
||||||
|
match (self, other) {
|
||||||
|
(Self::Edge, AssertReturnValue::Edge(_)) |
|
||||||
|
(Self::Label, AssertReturnValue::Label(_)) => true,
|
||||||
|
(_, _) => false
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl std::fmt::Display for EdgeRelablerInput {
|
||||||
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
|
match self {
|
||||||
|
Self::Label => write!(f, "label"),
|
||||||
|
Self::Edge => write!(f, "edge"),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
impl RSassert<EdgeRelablerInput> {
|
||||||
|
pub fn typecheck(&self) -> Result<(), String> {
|
||||||
|
let mut context = TypeContext::new();
|
||||||
|
let ty = typecheck(&self.tree, &mut context)?;
|
||||||
|
match ty {
|
||||||
|
AssertionTypes::Boolean |
|
||||||
|
AssertionTypes::Integer |
|
||||||
|
AssertionTypes::String |
|
||||||
|
AssertionTypes::Label |
|
||||||
|
AssertionTypes::Set |
|
||||||
|
AssertionTypes::Element |
|
||||||
|
AssertionTypes::Edge |
|
||||||
|
AssertionTypes::Node |
|
||||||
|
AssertionTypes::System |
|
||||||
|
AssertionTypes::Context =>
|
||||||
|
Ok(()),
|
||||||
|
AssertionTypes::NoType |
|
||||||
|
AssertionTypes::RangeInteger |
|
||||||
|
AssertionTypes::RangeSet |
|
||||||
|
AssertionTypes::RangeNeighbours =>
|
||||||
|
Err(format!("Returned type {ty} is not a valid return type.")),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn execute(
|
||||||
|
&self,
|
||||||
|
graph: &graph::RSgraph,
|
||||||
|
edge: &<graph::RSgraph as petgraph::visit::GraphBase>::EdgeId,
|
||||||
|
translator: &mut translator::Translator,
|
||||||
|
) -> Result<AssertReturnValue, String> {
|
||||||
|
let label = graph.edge_weight(*edge)
|
||||||
|
.ok_or("Missing edge {{debug: {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 {
|
||||||
|
Err("No value returned.".into())
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// Implementation for node grouping.
|
||||||
|
|
||||||
|
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
|
||||||
|
pub enum NodeRelablerInput {
|
||||||
|
Entities,
|
||||||
|
Node,
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Debug, Clone)]
|
||||||
|
pub enum NodeRelablerInputValues {
|
||||||
|
Entities(structure::RSset),
|
||||||
|
Node(petgraph::graph::NodeIndex),
|
||||||
|
}
|
||||||
|
|
||||||
|
impl SpecialVariables<NodeRelablerInputValues> for NodeRelablerInput {
|
||||||
|
fn type_of(&self) -> AssertionTypes {
|
||||||
|
match self {
|
||||||
|
Self::Entities => AssertionTypes::Set,
|
||||||
|
Self::Node => AssertionTypes::Node,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn type_qualified(&self, q: &Qualifier) -> Result<AssertionTypes, String> {
|
||||||
|
match (self, q) {
|
||||||
|
(Self::Node, Qualifier::Node(QualifierNode::System)) =>
|
||||||
|
Ok(AssertionTypes::System),
|
||||||
|
(Self::Node, Qualifier::Node(QualifierNode::Neighbours)) =>
|
||||||
|
Ok(AssertionTypes::RangeNeighbours),
|
||||||
|
(s, q) =>
|
||||||
|
Err(format!("Wrong use of qualifier {q} on variable {s}."))
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fn new_context(input: HashMap<Self, NodeRelablerInputValues>)
|
||||||
|
-> HashMap<Self, AssertReturnValue> {
|
||||||
|
input.iter().map(|(key, value)| {
|
||||||
|
match value {
|
||||||
|
NodeRelablerInputValues::Entities(e) =>
|
||||||
|
(*key, AssertReturnValue::Set(e.clone())),
|
||||||
|
NodeRelablerInputValues::Node(n) =>
|
||||||
|
(*key, AssertReturnValue::Node(*n)),
|
||||||
|
}
|
||||||
|
}).collect::<HashMap<Self, AssertReturnValue>>()
|
||||||
|
}
|
||||||
|
|
||||||
|
fn correct_type(&self, other: &AssertReturnValue) -> bool {
|
||||||
|
match (self, other) {
|
||||||
|
(Self::Entities, AssertReturnValue::Set(_)) |
|
||||||
|
(Self::Node, AssertReturnValue::Node(_)) => true,
|
||||||
|
(_, _) => false
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
impl std::fmt::Display for NodeRelablerInput {
|
||||||
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
|
match self {
|
||||||
|
Self::Entities => write!(f, "entities"),
|
||||||
|
Self::Node => write!(f, "node"),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
impl RSassert<NodeRelablerInput> {
|
||||||
|
pub fn typecheck(&self) -> Result<(), String> {
|
||||||
|
let mut context = TypeContext::new();
|
||||||
|
let ty = typecheck(&self.tree, &mut context)?;
|
||||||
|
match ty {
|
||||||
|
AssertionTypes::Boolean |
|
||||||
|
AssertionTypes::Integer |
|
||||||
|
AssertionTypes::String |
|
||||||
|
AssertionTypes::Label |
|
||||||
|
AssertionTypes::Set |
|
||||||
|
AssertionTypes::Element |
|
||||||
|
AssertionTypes::Edge |
|
||||||
|
AssertionTypes::Node |
|
||||||
|
AssertionTypes::System |
|
||||||
|
AssertionTypes::Context =>
|
||||||
|
Ok(()),
|
||||||
|
AssertionTypes::NoType |
|
||||||
|
AssertionTypes::RangeInteger |
|
||||||
|
AssertionTypes::RangeSet |
|
||||||
|
AssertionTypes::RangeNeighbours =>
|
||||||
|
Err(format!("Returned type {ty} is not a valid return type.")),
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn execute(
|
||||||
|
&self,
|
||||||
|
graph: &graph::RSgraph,
|
||||||
|
node: &<graph::RSgraph as petgraph::visit::GraphBase>::NodeId,
|
||||||
|
translator: &mut translator::Translator,
|
||||||
|
) -> Result<AssertReturnValue, String> {
|
||||||
|
let structure::RSsystem {available_entities: entities, ..} =
|
||||||
|
graph.node_weight(*node).ok_or("Missing node {{debug: {node:?}}}")?;
|
||||||
|
|
||||||
|
let mut input_vals = HashMap::new();
|
||||||
|
input_vals.insert(NodeRelablerInput::Entities,
|
||||||
|
NodeRelablerInputValues::Entities(entities.clone()));
|
||||||
|
input_vals.insert(NodeRelablerInput::Node,
|
||||||
|
NodeRelablerInputValues::Node(*node));
|
||||||
|
|
||||||
|
let mut context = Context::new(input_vals);
|
||||||
|
if let Some(v) = execute(&self.tree, &mut context, translator, graph)? {
|
||||||
|
Ok(v)
|
||||||
|
} else {
|
||||||
|
Err("No value returned.".into())
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
@ -4,13 +4,16 @@
|
|||||||
|
|
||||||
use super::dsl::*;
|
use super::dsl::*;
|
||||||
use super::super::{translator, structure};
|
use super::super::{translator, structure};
|
||||||
|
use super::rsassert::*;
|
||||||
|
|
||||||
|
type LocalAssert = RSassert<EdgeRelablerInput>;
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn assert_tycheck_true() {
|
fn assert_tycheck_true() {
|
||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {tree: Tree::Return(Box::new(Expression::True))};
|
let tree = LocalAssert {tree: Tree::Return(Box::new(Expression::True))};
|
||||||
assert!(tree.typecheck().is_ok());
|
assert!(tree.typecheck().is_ok());
|
||||||
|
|
||||||
|
|
||||||
@ -30,7 +33,7 @@ fn assert_tycheck_concat_1() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
Variable::Id("a".into()),
|
Variable::Id("a".into()),
|
||||||
@ -58,7 +61,7 @@ fn assert_tycheck_concat_2() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Return(Box::new(Expression::True))),
|
Box::new(Tree::Return(Box::new(Expression::True))),
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
@ -86,7 +89,7 @@ fn assert_tycheck_return_1() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Return(Box::new(Expression::True))),
|
Box::new(Tree::Return(Box::new(Expression::True))),
|
||||||
Box::new(Tree::Return(Box::new(Expression::False))),
|
Box::new(Tree::Return(Box::new(Expression::False))),
|
||||||
@ -108,7 +111,7 @@ fn assert_tycheck_return_1() {
|
|||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn assert_tycheck_return_incompatible_1() {
|
fn assert_tycheck_return_incompatible_1() {
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Return(Box::new(Expression::True))),
|
Box::new(Tree::Return(Box::new(Expression::True))),
|
||||||
Box::new(Tree::Return(Box::new(Expression::Integer(10)))),
|
Box::new(Tree::Return(Box::new(Expression::Integer(10)))),
|
||||||
@ -119,7 +122,7 @@ fn assert_tycheck_return_incompatible_1() {
|
|||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn assert_tycheck_return_incompatible_2() {
|
fn assert_tycheck_return_incompatible_2() {
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Return(Box::new(Expression::True))),
|
Box::new(Tree::Return(Box::new(Expression::True))),
|
||||||
Box::new(
|
Box::new(
|
||||||
@ -142,7 +145,7 @@ fn assert_tycheck_return_2() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Return(Box::new(Expression::True))),
|
Box::new(Tree::Return(Box::new(Expression::True))),
|
||||||
Box::new(
|
Box::new(
|
||||||
@ -177,7 +180,7 @@ fn assert_tycheck_return_3() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(
|
Box::new(
|
||||||
Tree::Concat(
|
Tree::Concat(
|
||||||
@ -211,7 +214,7 @@ fn assert_tycheck_if_1() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Return(Box::new(Expression::True))),
|
Box::new(Tree::Return(Box::new(Expression::True))),
|
||||||
Box::new(
|
Box::new(
|
||||||
@ -247,7 +250,7 @@ fn assert_tycheck_if_2() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(
|
Box::new(
|
||||||
Tree::If(
|
Tree::If(
|
||||||
@ -282,7 +285,7 @@ fn assert_tycheck_if_3() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(
|
Box::new(
|
||||||
Tree::If(
|
Tree::If(
|
||||||
@ -315,7 +318,7 @@ fn assert_tycheck_if_3() {
|
|||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn assert_tycheck_if_4() {
|
fn assert_tycheck_if_4() {
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(
|
Box::new(
|
||||||
Tree::If(
|
Tree::If(
|
||||||
@ -340,7 +343,7 @@ fn assert_tycheck_if_else_1() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Return(Box::new(Expression::True))),
|
Box::new(Tree::Return(Box::new(Expression::True))),
|
||||||
Box::new(
|
Box::new(
|
||||||
@ -379,7 +382,7 @@ fn assert_tycheck_if_else_2() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(
|
Box::new(
|
||||||
Tree::IfElse(
|
Tree::IfElse(
|
||||||
@ -415,7 +418,7 @@ fn assert_tycheck_if_else_2() {
|
|||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn assert_tycheck_if_else_3() {
|
fn assert_tycheck_if_else_3() {
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(
|
Box::new(
|
||||||
Tree::IfElse(
|
Tree::IfElse(
|
||||||
@ -440,7 +443,7 @@ fn assert_tycheck_if_else_3() {
|
|||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn assert_tycheck_if_else_4() {
|
fn assert_tycheck_if_else_4() {
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(
|
Box::new(
|
||||||
Tree::IfElse(
|
Tree::IfElse(
|
||||||
@ -465,7 +468,7 @@ fn assert_tycheck_if_else_4() {
|
|||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn assert_tycheck_assignment_1() {
|
fn assert_tycheck_assignment_1() {
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Assignment(
|
tree: Tree::Assignment(
|
||||||
Variable::Id("a".into()),
|
Variable::Id("a".into()),
|
||||||
None,
|
None,
|
||||||
@ -480,7 +483,7 @@ fn assert_tycheck_assignment_2() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(
|
Box::new(
|
||||||
Tree::Assignment(
|
Tree::Assignment(
|
||||||
@ -517,7 +520,7 @@ fn assert_tycheck_assignment_3() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(
|
Box::new(
|
||||||
Tree::Assignment(
|
Tree::Assignment(
|
||||||
@ -553,7 +556,7 @@ fn assert_tycheck_assignment_3() {
|
|||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn assert_tycheck_assignment_4() {
|
fn assert_tycheck_assignment_4() {
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(
|
Box::new(
|
||||||
Tree::Assignment(
|
Tree::Assignment(
|
||||||
@ -581,7 +584,7 @@ fn assert_tycheck_assignment_5() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
Variable::Id("a".into()),
|
Variable::Id("a".into()),
|
||||||
@ -621,7 +624,7 @@ fn assert_tycheck_assignment_6() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Concat(
|
Box::new(Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
@ -668,7 +671,7 @@ fn assert_tycheck_assignment_7() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Concat(
|
Box::new(Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
@ -713,7 +716,7 @@ fn assert_tycheck_assignment_8() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Concat(
|
Box::new(Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
@ -762,7 +765,7 @@ fn assert_tycheck_assignment_9() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Concat(
|
Box::new(Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
@ -809,7 +812,7 @@ fn assert_tycheck_assignment_10() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Concat(
|
Box::new(Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
@ -859,7 +862,7 @@ fn assert_tycheck_for_1() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel, RSset};
|
use structure::{RSsystem, RSlabel, RSset};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Concat(
|
Box::new(Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
@ -907,7 +910,7 @@ fn assert_tycheck_for_2() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel, RSset};
|
use structure::{RSsystem, RSlabel, RSset};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Concat(
|
Box::new(Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
@ -959,7 +962,7 @@ fn assert_tycheck_for_3() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel, RSset};
|
use structure::{RSsystem, RSlabel, RSset};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Concat(
|
Box::new(Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
@ -1025,7 +1028,7 @@ fn assert_tycheck_for_4() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel, RSset};
|
use structure::{RSsystem, RSlabel, RSset};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Concat(
|
Box::new(Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
@ -1092,7 +1095,7 @@ fn assert_tycheck_for_5() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel, RSset};
|
use structure::{RSsystem, RSlabel, RSset};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Concat(
|
Box::new(Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
@ -1172,7 +1175,7 @@ fn assert_tycheck_for_6() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel, RSset};
|
use structure::{RSsystem, RSlabel, RSset};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Concat(
|
Box::new(Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
@ -1263,7 +1266,7 @@ fn assert_tycheck_for_7() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Concat(
|
Box::new(Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
@ -1315,7 +1318,7 @@ fn assert_tycheck_for_8() {
|
|||||||
use translator::Translator;
|
use translator::Translator;
|
||||||
use structure::{RSsystem, RSlabel};
|
use structure::{RSsystem, RSlabel};
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Concat(
|
Box::new(Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
@ -1396,7 +1399,7 @@ fn assert_tycheck_system() {
|
|||||||
use structure::{RSsystem, RSlabel, RSset, RSenvironment, RSprocess};
|
use structure::{RSsystem, RSlabel, RSset, RSenvironment, RSprocess};
|
||||||
use std::rc::Rc;
|
use std::rc::Rc;
|
||||||
|
|
||||||
let tree = RSassert {
|
let tree = LocalAssert {
|
||||||
tree: Tree::Concat(
|
tree: Tree::Concat(
|
||||||
Box::new(Tree::Assignment(
|
Box::new(Tree::Assignment(
|
||||||
Variable::Id("a".into()),
|
Variable::Id("a".into()),
|
||||||
|
|||||||
@ -621,13 +621,12 @@ impl Hash for RSlabel {
|
|||||||
|
|
||||||
pub type RSassert =
|
pub type RSassert =
|
||||||
crate::rsprocess::assert::dsl::RSassert<
|
crate::rsprocess::assert::dsl::RSassert<
|
||||||
crate::rsprocess::assert::dsl::EdgeRelablerInput>;
|
crate::rsprocess::assert::rsassert::EdgeRelablerInput>;
|
||||||
|
|
||||||
pub mod assert {
|
pub mod assert {
|
||||||
pub use crate::rsprocess::assert::dsl::*;
|
pub use crate::rsprocess::assert::dsl::*;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
// RSBHML
|
// RSBHML
|
||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
|
|||||||
Reference in New Issue
Block a user