Refactoring but this time modular
This commit is contained in:
@ -4,29 +4,40 @@
|
|||||||
type IntegerType = i64;
|
type IntegerType = i64;
|
||||||
|
|
||||||
#[derive(Debug, Clone)]
|
#[derive(Debug, Clone)]
|
||||||
pub struct RSassert {
|
pub struct RSassert<S> {
|
||||||
pub tree: Tree
|
pub tree: Tree<S>
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Debug, Clone)]
|
#[derive(Debug, Clone)]
|
||||||
pub enum Tree {
|
pub enum Tree<S> {
|
||||||
Concat(Box<Tree>, Box<Tree>),
|
Concat(Box<Tree<S>>, Box<Tree<S>>),
|
||||||
If(Box<Expression>, Box<Tree>),
|
If(Box<Expression<S>>, Box<Tree<S>>),
|
||||||
IfElse(Box<Expression>, Box<Tree>, Box<Tree>),
|
IfElse(Box<Expression<S>>, Box<Tree<S>>, Box<Tree<S>>),
|
||||||
Assignment(Variable, Option<Qualifier>, Box<Expression>),
|
Assignment(Variable<S>, Option<Qualifier>, Box<Expression<S>>),
|
||||||
Return(Box<Expression>),
|
Return(Box<Expression<S>>),
|
||||||
For(Variable, Range, Box<Tree>),
|
For(Variable<S>, Range<S>, Box<Tree<S>>),
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
|
||||||
pub enum Variable {
|
pub enum Variable<S> {
|
||||||
Id(String),
|
Id(String),
|
||||||
Label, // special label that is the input of the function
|
Special(S)
|
||||||
Edge, // special edge that is the input of the function
|
}
|
||||||
|
|
||||||
|
trait SpecialVariables<G>: Display + std::fmt::Debug + Sized + Eq + Copy
|
||||||
|
+ std::hash::Hash
|
||||||
|
{
|
||||||
|
fn type_of(&self) -> AssertionTypes;
|
||||||
|
fn type_qualified(&self, q: &Qualifier) -> Result<AssertionTypes, String>;
|
||||||
|
fn new_context(input: HashMap<Self, G>)
|
||||||
|
-> HashMap<Self, AssertReturnValue>;
|
||||||
|
fn correct_type(&self, other: &AssertReturnValue) -> bool;
|
||||||
|
// fn correct_type_qualified(&self, q: &Qualifier, other: &AssertReturnValue)
|
||||||
|
// -> bool;
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Debug, Clone)]
|
#[derive(Debug, Clone)]
|
||||||
pub enum Expression {
|
pub enum Expression<S> {
|
||||||
True,
|
True,
|
||||||
False,
|
False,
|
||||||
Integer(IntegerType),
|
Integer(IntegerType),
|
||||||
@ -34,16 +45,16 @@ pub enum Expression {
|
|||||||
Set(super::structure::RSset),
|
Set(super::structure::RSset),
|
||||||
Element(super::translator::IdType),
|
Element(super::translator::IdType),
|
||||||
String(String),
|
String(String),
|
||||||
Var(Variable),
|
Var(Variable<S>),
|
||||||
|
|
||||||
Unary(Unary, Box<Expression>),
|
Unary(Unary, Box<Expression<S>>),
|
||||||
Binary(Binary, Box<Expression>, Box<Expression>),
|
Binary(Binary, Box<Expression<S>>, Box<Expression<S>>),
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Debug, Clone)]
|
#[derive(Debug, Clone)]
|
||||||
pub enum Range {
|
pub enum Range<S> {
|
||||||
IterateOverSet(Box<Expression>),
|
IterateOverSet(Box<Expression<S>>),
|
||||||
IterateInRange(Box<Expression>, Box<Expression>),
|
IterateInRange(Box<Expression<S>>, Box<Expression<S>>),
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive(Debug, Clone, Copy)]
|
#[derive(Debug, Clone, Copy)]
|
||||||
@ -118,7 +129,56 @@ pub enum Binary {
|
|||||||
CommonSubStr,
|
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) => {
|
(Self::Times, AssertionTypes::Set, AssertionTypes::Set) => {
|
||||||
Ok(AssertionTypes::Set)
|
Ok(AssertionTypes::Set)
|
||||||
},
|
},
|
||||||
(Self::Exponential, AssertionTypes::Integer, AssertionTypes::Integer) |
|
(Self::Exponential,
|
||||||
(Self::Quotient, AssertionTypes::Integer, AssertionTypes::Integer) |
|
AssertionTypes::Integer,
|
||||||
(Self::Reminder, AssertionTypes::Integer, AssertionTypes::Integer) => {
|
AssertionTypes::Integer) |
|
||||||
|
(Self::Quotient,
|
||||||
|
AssertionTypes::Integer,
|
||||||
|
AssertionTypes::Integer) |
|
||||||
|
(Self::Reminder,
|
||||||
|
AssertionTypes::Integer,
|
||||||
|
AssertionTypes::Integer) => {
|
||||||
Ok(AssertionTypes::Integer)
|
Ok(AssertionTypes::Integer)
|
||||||
},
|
},
|
||||||
(Self::Concat, AssertionTypes::String, AssertionTypes::String) => {
|
(Self::Concat, AssertionTypes::String, AssertionTypes::String) => {
|
||||||
@ -405,7 +471,9 @@ impl Binary {
|
|||||||
(Self::Max, AssertionTypes::Integer, AssertionTypes::Integer) => {
|
(Self::Max, AssertionTypes::Integer, AssertionTypes::Integer) => {
|
||||||
Ok(AssertionTypes::Integer)
|
Ok(AssertionTypes::Integer)
|
||||||
},
|
},
|
||||||
(Self::CommonSubStr, AssertionTypes::String, AssertionTypes::String) => {
|
(Self::CommonSubStr,
|
||||||
|
AssertionTypes::String,
|
||||||
|
AssertionTypes::String) => {
|
||||||
Ok(AssertionTypes::String)
|
Ok(AssertionTypes::String)
|
||||||
},
|
},
|
||||||
_ => {
|
_ => {
|
||||||
@ -420,7 +488,7 @@ impl Binary {
|
|||||||
|
|
||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
use std::collections::HashMap;
|
use std::collections::HashMap;
|
||||||
use std::fmt;
|
use std::fmt::{self, Display};
|
||||||
|
|
||||||
use petgraph::visit::EdgeRef;
|
use petgraph::visit::EdgeRef;
|
||||||
|
|
||||||
@ -429,6 +497,11 @@ struct TypeContext {
|
|||||||
return_ty: Option<AssertionTypes>
|
return_ty: Option<AssertionTypes>
|
||||||
}
|
}
|
||||||
|
|
||||||
|
struct Context<S> {
|
||||||
|
data: HashMap<String, AssertReturnValue>,
|
||||||
|
special: HashMap<S, AssertReturnValue>,
|
||||||
|
}
|
||||||
|
|
||||||
impl TypeContext {
|
impl TypeContext {
|
||||||
fn new() -> Self {
|
fn new() -> Self {
|
||||||
TypeContext {
|
TypeContext {
|
||||||
@ -437,12 +510,32 @@ impl TypeContext {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn assign(
|
fn return_type(
|
||||||
&mut self,
|
&mut self,
|
||||||
v: &Variable,
|
|
||||||
q: Option<&Qualifier>,
|
|
||||||
ty: AssertionTypes
|
ty: AssertionTypes
|
||||||
) -> Result<(), String> {
|
) -> 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<S, G>(
|
||||||
|
&mut self,
|
||||||
|
v: &Variable<S>,
|
||||||
|
q: Option<&Qualifier>,
|
||||||
|
ty: AssertionTypes
|
||||||
|
) -> Result<(), String>
|
||||||
|
where S: SpecialVariables<G> {
|
||||||
match (v, q) {
|
match (v, q) {
|
||||||
(Variable::Id(v), None) => {
|
(Variable::Id(v), None) => {
|
||||||
self.data.insert(v.clone(), ty);
|
self.data.insert(v.clone(), ty);
|
||||||
@ -471,68 +564,36 @@ impl TypeContext {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
(Variable::Label, None) => {
|
(Variable::Special(s), None) => {
|
||||||
if let AssertionTypes::Label = ty {
|
if s.type_of() == ty {
|
||||||
Ok(())
|
Ok(())
|
||||||
} else {
|
} else {
|
||||||
Err(format!("Variable label has type label but was \
|
Err(format!("Variable {s} has type {} but was \
|
||||||
assigned a value of type {ty}."))
|
assigned a value of type {ty}.", s.type_of()))
|
||||||
}
|
}
|
||||||
}
|
|
||||||
(Variable::Label, Some(q)) => {
|
|
||||||
match (q, ty) {
|
|
||||||
(Qualifier::Restricted(_),
|
|
||||||
AssertionTypes::Set) => {
|
|
||||||
Ok(())
|
|
||||||
},
|
},
|
||||||
(q, ty) => {
|
(Variable::Special(s), Some(q)) => {
|
||||||
Err(format!("Variable label has type label, but \
|
if s.type_qualified(q)? == ty {
|
||||||
was assigned with qualifier {q} \
|
|
||||||
value with type {ty}"))
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
(Variable::Edge, None) => {
|
|
||||||
if let AssertionTypes::Edge = ty {
|
|
||||||
Ok(())
|
Ok(())
|
||||||
} else {
|
} else {
|
||||||
Err(format!("Variable egde has type edge but was \
|
Err(format!("Variable {s} has type {} but was \
|
||||||
assigned a value of type {ty}."))
|
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<S, G>(
|
||||||
&mut self,
|
&mut self,
|
||||||
|
v: &Variable<S>,
|
||||||
ty: AssertionTypes
|
ty: AssertionTypes
|
||||||
) -> Result<(), String> {
|
) -> Result<(), String>
|
||||||
if let Some(ty_return) = self.return_ty {
|
where S: SpecialVariables<G> {
|
||||||
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> {
|
|
||||||
let v = match v {
|
let v = match v {
|
||||||
Variable::Label |
|
Variable::Special(s) =>
|
||||||
Variable::Edge => return Err("Protected word label used in for \
|
return Err(format!("Protected word {s} used in for \
|
||||||
assignment.".into()),
|
assignment.")),
|
||||||
Variable::Id(v) => v
|
Variable::Id(v) => v
|
||||||
};
|
};
|
||||||
match ty {
|
match ty {
|
||||||
@ -554,16 +615,14 @@ impl TypeContext {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn get(
|
fn get<S, G>(
|
||||||
&self,
|
&self,
|
||||||
v: &Variable,
|
v: &Variable<S>,
|
||||||
) -> Result<AssertionTypes, String> {
|
) -> Result<AssertionTypes, String>
|
||||||
|
where S: SpecialVariables<G> {
|
||||||
match v {
|
match v {
|
||||||
Variable::Label => {
|
Variable::Special(s) => {
|
||||||
Ok(AssertionTypes::Label)
|
Ok(s.type_of())
|
||||||
},
|
|
||||||
Variable::Edge => {
|
|
||||||
Ok(AssertionTypes::Edge)
|
|
||||||
},
|
},
|
||||||
Variable::Id(v) => {
|
Variable::Id(v) => {
|
||||||
if let Some(ty) = self.data.get(v) {
|
if let Some(ty) = self.data.get(v) {
|
||||||
@ -576,28 +635,22 @@ impl TypeContext {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
struct Context {
|
impl<S> Context<S> {
|
||||||
data: HashMap<String, AssertReturnValue>,
|
fn new<G>(
|
||||||
label: super::structure::RSlabel,
|
input: HashMap<S, G>,
|
||||||
edge: petgraph::graph::EdgeIndex,
|
) -> Self
|
||||||
}
|
where S: SpecialVariables<G> {
|
||||||
|
|
||||||
impl Context {
|
|
||||||
fn new(
|
|
||||||
label: &super::structure::RSlabel,
|
|
||||||
edge: &petgraph::graph::EdgeIndex,
|
|
||||||
) -> Self {
|
|
||||||
Self { data: HashMap::new(),
|
Self { data: HashMap::new(),
|
||||||
label: label.clone(),
|
special: S::new_context(input) }
|
||||||
edge: *edge }
|
|
||||||
}
|
}
|
||||||
|
|
||||||
fn assign(
|
fn assign<G>(
|
||||||
&mut self,
|
&mut self,
|
||||||
v: &Variable,
|
v: &Variable<S>,
|
||||||
q: Option<&Qualifier>,
|
q: Option<&Qualifier>,
|
||||||
val: AssertReturnValue,
|
val: AssertReturnValue,
|
||||||
) -> Result<(), String> {
|
) -> Result<(), String>
|
||||||
|
where S: SpecialVariables<G> {
|
||||||
match (v, q) {
|
match (v, q) {
|
||||||
(Variable::Id(v), None) => {
|
(Variable::Id(v), None) => {
|
||||||
self.data.insert(v.clone(), val);
|
self.data.insert(v.clone(), val);
|
||||||
@ -627,94 +680,50 @@ impl Context {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
},
|
},
|
||||||
(Variable::Edge, None) => {
|
(Variable::Special(s), None) => {
|
||||||
if let AssertReturnValue::Edge(e) = val {
|
if s.correct_type(&val) {
|
||||||
self.edge = e;
|
if let Some(s) = self.special.get_mut(s) {
|
||||||
|
*s = val;
|
||||||
|
} else {
|
||||||
|
self.special.insert(*s, val);
|
||||||
|
}
|
||||||
Ok(())
|
Ok(())
|
||||||
} else {
|
} else {
|
||||||
Err(format!("Trying to assign {val} to variable edge."))
|
Err(format!("Trying to assign {val} to variable {s}."))
|
||||||
}
|
}
|
||||||
}
|
|
||||||
(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) => {
|
(Variable::Special(s), Some(q)) => {
|
||||||
Err(format!("Variable label could not be assigned with \
|
if let Some(s) = self.special.get_mut(s) {
|
||||||
qualifier {q} new value {newval}."))
|
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<G>(
|
||||||
&self,
|
&self,
|
||||||
v: &Variable,
|
v: &Variable<S>,
|
||||||
) -> Result<AssertReturnValue, String> {
|
) -> Result<AssertReturnValue, String>
|
||||||
|
where S: SpecialVariables<G> {
|
||||||
match v {
|
match v {
|
||||||
Variable::Id(var) => {
|
Variable::Id(var) => {
|
||||||
self.data.get(var)
|
self.data.get(var)
|
||||||
.cloned()
|
.cloned()
|
||||||
.ok_or(format!("Variable {v} used, but no value assigned."))
|
.ok_or(format!("Variable {v} used, but no value assigned."))
|
||||||
},
|
},
|
||||||
Variable::Label => {
|
Variable::Special(s) => {
|
||||||
Ok(AssertReturnValue::Label(self.label.clone()))
|
self.special.get(s)
|
||||||
},
|
.cloned()
|
||||||
Variable::Edge => {
|
.ok_or(format!("Variable {v} used but no value assigned."))
|
||||||
Ok(AssertReturnValue::Edge(self.edge))
|
|
||||||
},
|
},
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
#[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 {
|
impl AssertReturnValue {
|
||||||
fn unary(
|
fn unary(
|
||||||
self,
|
self,
|
||||||
@ -878,10 +887,11 @@ impl AssertReturnValue {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn typecheck(
|
fn typecheck<S, G>(
|
||||||
tree: &Tree,
|
tree: &Tree<S>,
|
||||||
c: &mut TypeContext
|
c: &mut TypeContext
|
||||||
) -> Result<AssertionTypes, String>
|
) -> Result<AssertionTypes, String>
|
||||||
|
where S: SpecialVariables<G>
|
||||||
{
|
{
|
||||||
match tree {
|
match tree {
|
||||||
Tree::Concat(t1, t2) => {
|
Tree::Concat(t1, t2) => {
|
||||||
@ -928,10 +938,11 @@ fn typecheck(
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn typecheck_expression(
|
fn typecheck_expression<S, G>(
|
||||||
exp: &Expression,
|
exp: &Expression<S>,
|
||||||
c: &TypeContext
|
c: &TypeContext
|
||||||
) -> Result<AssertionTypes, String> {
|
) -> Result<AssertionTypes, String>
|
||||||
|
where S: SpecialVariables<G> {
|
||||||
match exp {
|
match exp {
|
||||||
Expression::True |
|
Expression::True |
|
||||||
Expression::False => Ok(AssertionTypes::Boolean),
|
Expression::False => Ok(AssertionTypes::Boolean),
|
||||||
@ -956,10 +967,11 @@ fn typecheck_expression(
|
|||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
fn typecheck_range(
|
fn typecheck_range<S, G>(
|
||||||
range: &Range,
|
range: &Range<S>,
|
||||||
c: &mut TypeContext
|
c: &mut TypeContext
|
||||||
) -> Result<AssertionTypes, String> {
|
) -> Result<AssertionTypes, String>
|
||||||
|
where S: SpecialVariables<G> {
|
||||||
match range {
|
match range {
|
||||||
Range::IterateInRange(exp1, exp2) => {
|
Range::IterateInRange(exp1, exp2) => {
|
||||||
let type_exp1 = typecheck_expression(exp1, c)?;
|
let type_exp1 = typecheck_expression(exp1, c)?;
|
||||||
@ -987,12 +999,13 @@ fn typecheck_range(
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn execute(
|
fn execute<S, G>(
|
||||||
tree: &Tree,
|
tree: &Tree<S>,
|
||||||
c: &mut Context,
|
c: &mut Context<S>,
|
||||||
translator: &mut super::translator::Translator,
|
translator: &mut super::translator::Translator,
|
||||||
graph: &super::graph::RSgraph,
|
graph: &super::graph::RSgraph,
|
||||||
) -> Result<Option<AssertReturnValue>, String> {
|
) -> Result<Option<AssertReturnValue>, String>
|
||||||
|
where S: SpecialVariables<G> {
|
||||||
match tree {
|
match tree {
|
||||||
Tree::Concat(t1, t2) => {
|
Tree::Concat(t1, t2) => {
|
||||||
if let Some(val) = execute(t1, c, translator, graph)? {
|
if let Some(val) = execute(t1, c, translator, graph)? {
|
||||||
@ -1040,12 +1053,13 @@ fn execute(
|
|||||||
|
|
||||||
type RangeIterator = std::vec::IntoIter<AssertReturnValue>;
|
type RangeIterator = std::vec::IntoIter<AssertReturnValue>;
|
||||||
|
|
||||||
fn range_into_iter(
|
fn range_into_iter<S, G>(
|
||||||
range: &Range,
|
range: &Range<S>,
|
||||||
c: &mut Context,
|
c: &mut Context<S>,
|
||||||
translator: &mut super::translator::Translator,
|
translator: &mut super::translator::Translator,
|
||||||
graph: &super::graph::RSgraph,
|
graph: &super::graph::RSgraph,
|
||||||
) -> Result<RangeIterator, String> {
|
) -> Result<RangeIterator, String>
|
||||||
|
where S: SpecialVariables<G> {
|
||||||
match range {
|
match range {
|
||||||
Range::IterateOverSet(exp) => {
|
Range::IterateOverSet(exp) => {
|
||||||
let val = execute_exp(exp, c, translator, graph)?;
|
let val = execute_exp(exp, c, translator, graph)?;
|
||||||
@ -1083,12 +1097,13 @@ fn range_into_iter(
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn execute_exp(
|
fn execute_exp<S, G>(
|
||||||
exp: &Expression,
|
exp: &Expression<S>,
|
||||||
c: &Context,
|
c: &Context<S>,
|
||||||
translator: &mut super::translator::Translator,
|
translator: &mut super::translator::Translator,
|
||||||
graph: &super::graph::RSgraph,
|
graph: &super::graph::RSgraph,
|
||||||
) -> Result<AssertReturnValue, String> {
|
) -> Result<AssertReturnValue, String>
|
||||||
|
where S: SpecialVariables<G> {
|
||||||
match exp {
|
match exp {
|
||||||
Expression::True => Ok(AssertReturnValue::Boolean(true)),
|
Expression::True => Ok(AssertReturnValue::Boolean(true)),
|
||||||
Expression::False => Ok(AssertReturnValue::Boolean(false)),
|
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<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
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// 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<EdgeRelablerInput> {
|
||||||
pub fn typecheck(&self) -> Result<(), String> {
|
pub fn typecheck(&self) -> Result<(), String> {
|
||||||
let mut context = TypeContext::new();
|
let mut context = TypeContext::new();
|
||||||
typecheck(&self.tree, &mut context)?;
|
typecheck(&self.tree, &mut context)?;
|
||||||
@ -1143,7 +1241,14 @@ impl RSassert {
|
|||||||
translator: &mut super::translator::Translator,
|
translator: &mut super::translator::Translator,
|
||||||
) -> Result<AssertReturnValue, String> {
|
) -> Result<AssertReturnValue, String> {
|
||||||
let label = graph.edge_weight(*edge).unwrap();
|
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)? {
|
if let Some(v) = execute(&self.tree, &mut context, translator, graph)? {
|
||||||
Ok(v)
|
Ok(v)
|
||||||
} else {
|
} else {
|
||||||
|
|||||||
@ -2,13 +2,13 @@
|
|||||||
// Display Implementation for all types
|
// Display Implementation for all types
|
||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
|
|
||||||
impl fmt::Display for RSassert {
|
impl<S> fmt::Display for RSassert<S> where S: Display {
|
||||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
write!(f, "label {{\n{}\n}}", self.tree)
|
write!(f, "label {{\n{}\n}}", self.tree)
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl fmt::Display for Tree {
|
impl<S> fmt::Display for Tree<S> where S: Display {
|
||||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
match self {
|
match self {
|
||||||
Self::Concat(t1, t2) => {write!(f, "{t1};\n{t2}")},
|
Self::Concat(t1, t2) => {write!(f, "{t1};\n{t2}")},
|
||||||
@ -29,17 +29,16 @@ impl fmt::Display for Tree {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl fmt::Display for Variable {
|
impl<S> fmt::Display for Variable<S> where S: Display {
|
||||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
match self {
|
match self {
|
||||||
Self::Label => {write!(f, "label")},
|
Self::Special(s) => {write!(f, "{s}")},
|
||||||
Self::Edge => {write!(f, "edge")},
|
|
||||||
Self::Id(s) => {write!(f, "{s}")}
|
Self::Id(s) => {write!(f, "{s}")}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl fmt::Display for Expression {
|
impl<S> fmt::Display for Expression<S> where S: Display {
|
||||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
match self {
|
match self {
|
||||||
Self::True => {write!(f, "True")},
|
Self::True => {write!(f, "True")},
|
||||||
@ -74,7 +73,7 @@ impl fmt::Display for Expression {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl fmt::Display for Range {
|
impl<S> fmt::Display for Range<S> where S: Display {
|
||||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||||
match self {
|
match self {
|
||||||
Self::IterateOverSet(exp) => {write!(f, "{{{exp}}}")},
|
Self::IterateOverSet(exp) => {write!(f, "{{{exp}}}")},
|
||||||
|
|||||||
@ -1322,7 +1322,9 @@ fn assert_tycheck_for_8() {
|
|||||||
Unary::Neighbours,
|
Unary::Neighbours,
|
||||||
Box::new(Expression::Unary(
|
Box::new(Expression::Unary(
|
||||||
Unary::Source,
|
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,
|
Unary::System,
|
||||||
Box::new(Expression::Unary(
|
Box::new(Expression::Unary(
|
||||||
Unary::Target,
|
Unary::Target,
|
||||||
Box::new(Expression::Var(Variable::Edge))
|
Box::new(Expression::Var(
|
||||||
|
Variable::Special(EdgeRelablerInput::Edge)
|
||||||
|
))
|
||||||
))
|
))
|
||||||
))
|
))
|
||||||
))
|
))
|
||||||
|
|||||||
@ -128,7 +128,7 @@ where
|
|||||||
{
|
{
|
||||||
fn map_edges(
|
fn map_edges(
|
||||||
&self,
|
&self,
|
||||||
edge_map: &super::assert::RSassert,
|
edge_map: &super::structure::RSassert,
|
||||||
translator: &mut super::translator::Translator
|
translator: &mut super::translator::Translator
|
||||||
) -> Result<Graph<RSsystem, super::assert::AssertReturnValue, Ty, Ix>, String>;
|
) -> Result<Graph<RSsystem, super::assert::AssertReturnValue, Ty, Ix>, String>;
|
||||||
}
|
}
|
||||||
@ -138,7 +138,7 @@ impl<'a> MapEdges<'a, RSsystem, RSlabel, Directed, u32>
|
|||||||
{
|
{
|
||||||
fn map_edges(
|
fn map_edges(
|
||||||
&self,
|
&self,
|
||||||
edge_map: &super::assert::RSassert,
|
edge_map: &super::structure::RSassert,
|
||||||
translator: &mut super::translator::Translator
|
translator: &mut super::translator::Translator
|
||||||
)-> Result<Graph<RSsystem, super::assert::AssertReturnValue, Directed, u32>, String> {
|
)-> Result<Graph<RSsystem, super::assert::AssertReturnValue, Directed, u32>, String> {
|
||||||
use petgraph::graph::EdgeIndex;
|
use petgraph::graph::EdgeIndex;
|
||||||
|
|||||||
@ -89,7 +89,7 @@ pub enum Instruction {
|
|||||||
FastFrequency { experiment: String, so: SaveOptions },
|
FastFrequency { experiment: String, so: SaveOptions },
|
||||||
Digraph { gso: Vec<GraphSaveOptions> },
|
Digraph { gso: Vec<GraphSaveOptions> },
|
||||||
Bisimilarity { system_b: String,
|
Bisimilarity { system_b: String,
|
||||||
edge_relabeler: Box<super::assert::RSassert>,
|
edge_relabeler: Box<super::structure::RSassert>,
|
||||||
so: SaveOptions }
|
so: SaveOptions }
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -499,7 +499,7 @@ pub fn digraph(system: &mut EvaluatedSystem) -> Result<(), String> {
|
|||||||
/// Computes bisimularity of two provided systems
|
/// Computes bisimularity of two provided systems
|
||||||
pub fn bisimilar(
|
pub fn bisimilar(
|
||||||
system_a: &mut EvaluatedSystem,
|
system_a: &mut EvaluatedSystem,
|
||||||
edge_relabeler: &super::assert::RSassert,
|
edge_relabeler: &super::structure::RSassert,
|
||||||
system_b: String
|
system_b: String
|
||||||
) -> Result<String, String>
|
) -> Result<String, String>
|
||||||
{
|
{
|
||||||
|
|||||||
@ -619,7 +619,9 @@ impl Hash for RSlabel {
|
|||||||
// RSassert
|
// RSassert
|
||||||
// -----------------------------------------------------------------------------
|
// -----------------------------------------------------------------------------
|
||||||
|
|
||||||
pub use crate::rsprocess::assert::RSassert;
|
pub type RSassert =
|
||||||
|
crate::rsprocess::assert::RSassert<
|
||||||
|
crate::rsprocess::assert::EdgeRelablerInput>;
|
||||||
|
|
||||||
pub mod assert {
|
pub mod assert {
|
||||||
pub use crate::rsprocess::assert::*;
|
pub use crate::rsprocess::assert::*;
|
||||||
@ -636,6 +638,6 @@ pub enum RSBHML {
|
|||||||
False,
|
False,
|
||||||
Or(Vec<RSBHML>),
|
Or(Vec<RSBHML>),
|
||||||
And(Vec<RSBHML>),
|
And(Vec<RSBHML>),
|
||||||
Diamond(Box<RSassert>, Box<RSBHML>),
|
// Diamond(Box<RSassert>, Box<RSBHML>),
|
||||||
Box(Box<RSassert>, Box<RSBHML>),
|
// Box(Box<RSassert>, Box<RSBHML>),
|
||||||
}
|
}
|
||||||
|
|||||||
Reference in New Issue
Block a user