use std::collections::HashMap;

use rsprocess::set::BasicSet;
use rsprocess::{element, graph, label, process, set, system, translator};
use serde::{Deserialize, Serialize};

/// If changing IntegerType in assert.rs, also change from Num to another
/// similar parser with different return type in grammar.lalrpop in
/// AssertExpression
type IntegerType = i64;

#[derive(Clone, Serialize, Deserialize, Hash)]
pub struct PositiveAssert<S> {
    pub tree: PositiveTree<S>,
}

#[derive(Clone, Serialize, Deserialize, Hash)]
pub enum PositiveTree<S> {
    Concat(Box<PositiveTree<S>>, Box<PositiveTree<S>>),
    If(Box<PositiveExpression<S>>, Box<PositiveTree<S>>),
    IfElse(
        Box<PositiveExpression<S>>,
        Box<PositiveTree<S>>,
        Box<PositiveTree<S>>,
    ),
    Assignment(
        PositiveVariable<S>,
        Option<PositiveQualifier>,
        Box<PositiveExpression<S>>,
    ),
    Return(Box<PositiveExpression<S>>),
    For(PositiveVariable<S>, PositiveRange<S>, Box<PositiveTree<S>>),
}

#[derive(Clone, PartialEq, Eq, Hash, Serialize, Deserialize)]
pub enum PositiveVariable<S> {
    Id(String),
    Special(S),
}

/// Trait needed for special variables.
pub(super) trait SpecialVariables<G>:
    translator::PrintableWithTranslator
    + std::fmt::Debug
    + Sized
    + Eq
    + Copy
    + std::hash::Hash
{
    /// Returns the type of the specific special variable.
    fn type_of(&self) -> PositiveAssertionTypes;

    /// Returns the type of the qualified special variable.
    fn type_qualified(
        &self,
        q: &PositiveQualifier,
    ) -> Result<PositiveAssertionTypes, String>;

    /// Creates a new context.
    fn new_context(
        input: HashMap<Self, G>,
    ) -> HashMap<Self, PositiveAssertReturnValue>;

    /// Returns true if
    fn correct_type(&self, other: &PositiveAssertReturnValue) -> bool;
}

#[derive(Clone, Serialize, Deserialize, Hash)]
pub enum PositiveExpression<S> {
    True,
    False,
    Integer(IntegerType),
    Label(Box<label::PositiveLabel>),
    Set(set::PositiveSet),
    PositiveElement(element::PositiveType),
    String(String),
    Var(PositiveVariable<S>),

    Unary(PositiveUnary, Box<PositiveExpression<S>>),
    Binary(
        PositiveBinary,
        Box<PositiveExpression<S>>,
        Box<PositiveExpression<S>>,
    ),
}

#[derive(Clone, Serialize, Deserialize, Hash)]
pub enum PositiveRange<S> {
    IterateOverSet(Box<PositiveExpression<S>>),
    IterateInRange(Box<PositiveExpression<S>>, Box<PositiveExpression<S>>),
}

#[derive(Clone, Copy, Serialize, Deserialize, Hash)]
pub enum PositiveUnary {
    Not,
    Rand,

    Empty,
    Length,
    ToStr,
    ToEl,
    Qualifier(PositiveQualifier),
}

#[derive(Clone, Copy, Serialize, Deserialize, Hash)]
pub enum QualifierRestricted {
    Entities,
    Context,
    Reactants,
    ReactantsAbsent,
    Inhibitors,
    InhibitorsPresent,
    Products,
}

#[derive(Clone, Copy, Serialize, Deserialize, Hash)]
pub enum QualifierLabel {
    AvailableEntities,
    AllReactants,
    AllInhibitors,
}

#[derive(Clone, Copy, Serialize, Deserialize, Hash)]
pub enum QualifierSystem {
    Entities,
    Context,
}

#[derive(Clone, Copy, Serialize, Deserialize, Hash)]
pub enum QualifierEdge {
    Source,
    Target,
    Label,
}

#[derive(Clone, Copy, Serialize, Deserialize, Hash)]
pub enum QualifierNode {
    Neighbours,
    System,
}

#[derive(Clone, Copy, Serialize, Deserialize, Hash)]
pub enum PositiveQualifier {
    System(QualifierSystem),
    Label(QualifierLabel),
    Restricted(QualifierRestricted),
    Edge(QualifierEdge),
    Node(QualifierNode),
}

#[derive(Clone, Copy, Serialize, Deserialize, Hash)]
pub enum PositiveBinary {
    And,
    Or,
    Xor,
    Less,
    LessEq,
    More,
    MoreEq,
    Eq,
    NotEq,
    Plus,
    Minus,
    Times,
    Exponential,
    Quotient,
    Reminder,
    Concat,

    SubStr,
    Min,
    Max,
    CommonSubStr,
}

#[derive(Copy, Clone, PartialEq, Eq, Serialize, Deserialize, Hash)]
pub(super) enum PositiveAssertionTypes {
    Boolean,
    Integer,
    String,
    Label,
    Set,
    PositiveElement,
    System,
    Context,
    NoType,
    RangeInteger,
    RangeSet,
    RangeNeighbours,

    Node,
    Edge,
}

#[derive(Clone, Hash, PartialEq, Eq, Serialize, Deserialize)]
pub enum PositiveAssertReturnValue {
    Boolean(bool),
    Integer(IntegerType),
    String(String),
    Label(label::PositiveLabel),
    Set(set::PositiveSet),
    PositiveElement(element::PositiveType),
    Node(petgraph::graph::NodeIndex),
    Edge(petgraph::graph::EdgeIndex),
    Neighbours(petgraph::graph::NodeIndex),
    System(system::PositiveSystem),
    Context(process::PositiveProcess),
}

// -----------------------------------------------------------------------------
//                         Implementations for types
// -----------------------------------------------------------------------------

impl<S> Default for PositiveAssert<S> {
    fn default() -> Self {
        Self {
            tree: PositiveTree::Return(Box::new(PositiveExpression::True)),
        }
    }
}

impl QualifierRestricted {
    pub(super) fn referenced_mut<'a>(
        &self,
        label: &'a mut label::PositiveLabel,
    ) -> &'a mut set::PositiveSet {
        match self {
            | Self::Entities => &mut label.available_entities,
            | Self::Context => &mut label.context,
            | Self::Reactants => &mut label.reactants,
            | Self::ReactantsAbsent => &mut label.reactants_absent,
            | Self::Inhibitors => &mut label.inhibitors,
            | Self::InhibitorsPresent => &mut label.inhibitors_present,
            | Self::Products => &mut label.products,
        }
    }

    pub(super) fn referenced<'a>(
        &self,
        label: &'a label::PositiveLabel,
    ) -> &'a set::PositiveSet {
        match self {
            | Self::Entities => &label.available_entities,
            | Self::Context => &label.context,
            | Self::Reactants => &label.reactants,
            | Self::ReactantsAbsent => &label.reactants_absent,
            | Self::Inhibitors => &label.inhibitors,
            | Self::InhibitorsPresent => &label.inhibitors_present,
            | Self::Products => &label.products,
        }
    }

    pub(super) fn get(
        &self,
        label: &label::PositiveLabel,
    ) -> PositiveAssertReturnValue {
        PositiveAssertReturnValue::Set(self.referenced(label).clone())
    }
}

impl QualifierLabel {
    pub(super) fn get(
        &self,
        l: &label::PositiveLabel,
    ) -> PositiveAssertReturnValue {
        match self {
            | QualifierLabel::AvailableEntities =>
                PositiveAssertReturnValue::Set(l.t.clone()),
            | QualifierLabel::AllReactants => PositiveAssertReturnValue::Set(
                l.reactants.union(&l.reactants_absent),
            ),
            | QualifierLabel::AllInhibitors => PositiveAssertReturnValue::Set(
                l.inhibitors.union(&l.inhibitors_present),
            ),
        }
    }
}

impl QualifierSystem {
    pub(super) fn get(
        &self,
        l: &system::PositiveSystem,
    ) -> PositiveAssertReturnValue {
        match self {
            | Self::Context =>
                PositiveAssertReturnValue::Context(l.context_process.clone()),
            | Self::Entities =>
                PositiveAssertReturnValue::Set(l.available_entities.clone()),
        }
    }
}

impl PositiveUnary {
    pub(super) fn is_prefix(&self) -> bool {
        match self {
            | Self::Not | Self::Rand => true,
            | Self::Empty
            | Self::Length
            | Self::ToStr
            | Self::Qualifier(_)
            | Self::ToEl => false,
        }
    }

    pub(super) fn is_suffix(&self) -> bool {
        !self.is_prefix()
    }

    pub(super) fn associate(
        &self,
        type_exp: &PositiveAssertionTypes,
    ) -> Result<PositiveAssertionTypes, String> {
        match (self, type_exp) {
            | (Self::Not, PositiveAssertionTypes::Boolean) =>
                Ok(PositiveAssertionTypes::Boolean),
            | (Self::Rand, PositiveAssertionTypes::Integer) =>
                Ok(PositiveAssertionTypes::Integer),
            | (Self::Empty, PositiveAssertionTypes::Set) =>
                Ok(PositiveAssertionTypes::Boolean),
            | (Self::Length, PositiveAssertionTypes::Set)
            | (Self::Length, PositiveAssertionTypes::String) =>
                Ok(PositiveAssertionTypes::Integer),
            | (Self::ToStr, PositiveAssertionTypes::Boolean)
            | (Self::ToStr, PositiveAssertionTypes::PositiveElement)
            | (Self::ToStr, PositiveAssertionTypes::Integer) =>
                Ok(PositiveAssertionTypes::String),
            | (
                Self::Qualifier(PositiveQualifier::Label(_)),
                PositiveAssertionTypes::Label,
            ) => Ok(PositiveAssertionTypes::Set),
            | (
                Self::Qualifier(PositiveQualifier::Restricted(_)),
                PositiveAssertionTypes::Label,
            ) => Ok(PositiveAssertionTypes::Set),
            | (Self::ToEl, PositiveAssertionTypes::String) =>
                Ok(PositiveAssertionTypes::PositiveElement),
            | (
                Self::Qualifier(PositiveQualifier::Edge(QualifierEdge::Source)),
                PositiveAssertionTypes::Edge,
            ) => Ok(PositiveAssertionTypes::Node),
            | (
                Self::Qualifier(PositiveQualifier::Edge(QualifierEdge::Target)),
                PositiveAssertionTypes::Edge,
            ) => Ok(PositiveAssertionTypes::Node),
            | (
                Self::Qualifier(PositiveQualifier::Edge(QualifierEdge::Label)),
                PositiveAssertionTypes::Edge,
            ) => Ok(PositiveAssertionTypes::Label),
            | (
                Self::Qualifier(PositiveQualifier::Node(
                    QualifierNode::Neighbours,
                )),
                PositiveAssertionTypes::Node,
            ) => Ok(PositiveAssertionTypes::RangeNeighbours),
            | (
                Self::Qualifier(PositiveQualifier::System(
                    QualifierSystem::Entities,
                )),
                PositiveAssertionTypes::System,
            ) => Ok(PositiveAssertionTypes::Set),
            | (
                Self::Qualifier(PositiveQualifier::Restricted(
                    QualifierRestricted::Entities,
                )),
                PositiveAssertionTypes::System,
            )
            | (
                Self::Qualifier(PositiveQualifier::Restricted(
                    QualifierRestricted::Context,
                )),
                PositiveAssertionTypes::System,
            ) => Err(format!(
                "Expression has incompatible type with operation: type \
                     system with operation \"{self:?}\" (be sure to use \
                     \".SystemEntities\" and \".SystemContext\" to refer to \
                     the system fields)."
            )),
            | (
                Self::Qualifier(PositiveQualifier::System(
                    QualifierSystem::Context,
                )),
                PositiveAssertionTypes::System,
            ) => Ok(PositiveAssertionTypes::Context),
            | (
                Self::Qualifier(PositiveQualifier::Node(QualifierNode::System)),
                PositiveAssertionTypes::Node,
            ) => Ok(PositiveAssertionTypes::System),
            | (op, type_exp) => Err(format!(
                "Expression has incompatible type with operation: type \
                     {type_exp:?} with operation \"{op:?}\"."
            )),
        }
    }
}

impl PositiveBinary {
    pub(super) fn is_prefix(&self) -> bool {
        match self {
            | Self::And
            | Self::Or
            | Self::Xor
            | Self::Less
            | Self::LessEq
            | Self::More
            | Self::MoreEq
            | Self::Eq
            | Self::NotEq
            | Self::Plus
            | Self::Minus
            | Self::Times
            | Self::Exponential
            | Self::Quotient
            | Self::Reminder
            | Self::Concat => false,
            | Self::SubStr | Self::Min | Self::Max | Self::CommonSubStr => true,
        }
    }

    pub(super) fn is_suffix(&self) -> bool {
        false
    }

    pub(super) fn is_infix(&self) -> bool {
        match self {
            | Self::And
            | Self::Or
            | Self::Xor
            | Self::Less
            | Self::LessEq
            | Self::More
            | Self::MoreEq
            | Self::Eq
            | Self::NotEq
            | Self::Plus
            | Self::Minus
            | Self::Times
            | Self::Exponential
            | Self::Quotient
            | Self::Reminder
            | Self::Concat => true,
            | Self::SubStr | Self::Min | Self::Max | Self::CommonSubStr =>
                false,
        }
    }

    pub(super) fn associate(
        &self,
        t1: &PositiveAssertionTypes,
        t2: &PositiveAssertionTypes,
    ) -> Result<PositiveAssertionTypes, String> {
        match (self, t1, t2) {
            | (
                Self::And,
                PositiveAssertionTypes::Boolean,
                PositiveAssertionTypes::Boolean,
            )
            | (
                Self::Or,
                PositiveAssertionTypes::Boolean,
                PositiveAssertionTypes::Boolean,
            ) => Ok(PositiveAssertionTypes::Boolean),
            | (
                Self::Xor,
                PositiveAssertionTypes::Boolean,
                PositiveAssertionTypes::Boolean,
            ) => Ok(PositiveAssertionTypes::Boolean),
            | (
                Self::Xor,
                PositiveAssertionTypes::Set,
                PositiveAssertionTypes::Set,
            ) => Ok(PositiveAssertionTypes::Set),
            | (
                Self::Less,
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            )
            | (
                Self::Less,
                PositiveAssertionTypes::Set,
                PositiveAssertionTypes::Set,
            )
            | (
                Self::LessEq,
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            )
            | (
                Self::LessEq,
                PositiveAssertionTypes::Set,
                PositiveAssertionTypes::Set,
            )
            | (
                Self::More,
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            )
            | (
                Self::More,
                PositiveAssertionTypes::Set,
                PositiveAssertionTypes::Set,
            )
            | (
                Self::MoreEq,
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            )
            | (
                Self::MoreEq,
                PositiveAssertionTypes::Set,
                PositiveAssertionTypes::Set,
            ) => Ok(PositiveAssertionTypes::Boolean),
            | (
                Self::Eq,
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            )
            | (
                Self::Eq,
                PositiveAssertionTypes::Boolean,
                PositiveAssertionTypes::Boolean,
            )
            | (
                Self::Eq,
                PositiveAssertionTypes::PositiveElement,
                PositiveAssertionTypes::PositiveElement,
            )
            | (
                Self::Eq,
                PositiveAssertionTypes::Label,
                PositiveAssertionTypes::Label,
            )
            | (
                Self::Eq,
                PositiveAssertionTypes::String,
                PositiveAssertionTypes::String,
            )
            | (
                Self::Eq,
                PositiveAssertionTypes::Set,
                PositiveAssertionTypes::Set,
            )
            | (
                Self::NotEq,
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            )
            | (
                Self::NotEq,
                PositiveAssertionTypes::Boolean,
                PositiveAssertionTypes::Boolean,
            )
            | (
                Self::NotEq,
                PositiveAssertionTypes::PositiveElement,
                PositiveAssertionTypes::PositiveElement,
            )
            | (
                Self::NotEq,
                PositiveAssertionTypes::Label,
                PositiveAssertionTypes::Label,
            )
            | (
                Self::NotEq,
                PositiveAssertionTypes::String,
                PositiveAssertionTypes::String,
            )
            | (
                Self::NotEq,
                PositiveAssertionTypes::Set,
                PositiveAssertionTypes::Set,
            ) => Ok(PositiveAssertionTypes::Boolean),
            | (
                Self::Plus,
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            )
            | (
                Self::Minus,
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            )
            | (
                Self::Times,
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            ) => Ok(PositiveAssertionTypes::Integer),
            | (
                Self::Plus,
                PositiveAssertionTypes::Set,
                PositiveAssertionTypes::Set,
            )
            | (
                Self::Minus,
                PositiveAssertionTypes::Set,
                PositiveAssertionTypes::Set,
            )
            | (
                Self::Times,
                PositiveAssertionTypes::Set,
                PositiveAssertionTypes::Set,
            ) => Ok(PositiveAssertionTypes::Set),
            | (
                Self::Exponential,
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            )
            | (
                Self::Quotient,
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            )
            | (
                Self::Reminder,
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            ) => Ok(PositiveAssertionTypes::Integer),
            | (
                Self::Concat,
                PositiveAssertionTypes::String,
                PositiveAssertionTypes::String,
            ) => Ok(PositiveAssertionTypes::String),
            | (
                Self::Concat,
                PositiveAssertionTypes::Set,
                PositiveAssertionTypes::PositiveElement,
            ) => Ok(PositiveAssertionTypes::Set),
            | (
                Self::SubStr,
                PositiveAssertionTypes::String,
                PositiveAssertionTypes::String,
            ) => Ok(PositiveAssertionTypes::Integer),
            | (
                Self::Min,
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            )
            | (
                Self::Max,
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            ) => Ok(PositiveAssertionTypes::Integer),
            | (
                Self::CommonSubStr,
                PositiveAssertionTypes::String,
                PositiveAssertionTypes::String,
            ) => Ok(PositiveAssertionTypes::String),
            | _ => Err(format!(
                "Expressions have incompatible types: {t1:?} and \
                             {t2:?} with operation {self:?}."
            )),
        }
    }
}

impl PositiveAssertReturnValue {
    pub(super) fn assign_qualified(
        &mut self,
        q: PositiveQualifier,
        val: PositiveAssertReturnValue,
    ) -> Result<(), String> {
        match (self, q, val) {
            | (
                Self::Label(l),
                PositiveQualifier::Restricted(q),
                PositiveAssertReturnValue::Set(set),
            ) => {
                *q.referenced_mut(l) = set;
                Ok(())
            },
            | (s, q, val) => Err(format!(
                "Cannot assign {val:?} to {s:?} with qualifier \
                             {q:?}"
            )),
        }
    }
}

// -----------------------------------------------------------------------------
//                        Typechecking and Evaluation
// -----------------------------------------------------------------------------

pub(super) struct TypeContext {
    data:      HashMap<String, PositiveAssertionTypes>,
    return_ty: Option<PositiveAssertionTypes>,
}

pub(super) struct Context<S> {
    data:    HashMap<String, PositiveAssertReturnValue>,
    special: HashMap<S, PositiveAssertReturnValue>,
}

impl TypeContext {
    pub(super) fn new() -> Self {
        TypeContext {
            data:      HashMap::new(),
            return_ty: None,
        }
    }

    fn return_type(
        &mut self,
        ty: PositiveAssertionTypes,
    ) -> 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: &PositiveVariable<S>,
        q: Option<&PositiveQualifier>,
        ty: PositiveAssertionTypes,
    ) -> Result<(), String>
    where
        S: SpecialVariables<G>,
    {
        match (v, q) {
            | (PositiveVariable::Id(v), None) => {
                self.data.insert(v.clone(), ty);
                Ok(())
            },
            | (PositiveVariable::Id(v), Some(q)) =>
                match self.data.entry(v.clone()) {
                    | std::collections::hash_map::Entry::Vacant(_ve) =>
                        Err(format!(
                            "Variable {v:?} as no assignment while \
                                     trying to assign to qualification {q:?}, \
                                     assign first a value."
                        )),
                    | std::collections::hash_map::Entry::Occupied(oe) =>
                        match (oe.get(), q, ty) {
                            | (
                                PositiveAssertionTypes::Label,
                                PositiveQualifier::Restricted(_),
                                PositiveAssertionTypes::Set,
                            ) => Ok(()),
                            | (t, q, ty) => Err(format!(
                                "Variable {v:?} has type {t:?}, \
                                             but was assigned with qualifier \
                                             {q:?} value with type {ty:?}."
                            )),
                        },
                },
            | (PositiveVariable::Special(s), None) =>
                if s.type_of() == ty {
                    Ok(())
                } else {
                    Err(format!(
                        "Variable {s:?} has type {:?} but was \
                                 assigned a value of type {ty:?}.",
                        s.type_of()
                    ))
                },
            | (PositiveVariable::Special(s), Some(q)) =>
                if s.type_qualified(q)? == ty {
                    Ok(())
                } else {
                    Err(format!(
                        "Variable {s:?} has type {:?} but was \
                                 assigned a value of type {ty:?} with \
                                 qualifier {q:?}.",
                        s.type_of()
                    ))
                },
        }
    }

    fn assign_range<S, G>(
        &mut self,
        v: &PositiveVariable<S>,
        ty: PositiveAssertionTypes,
    ) -> Result<(), String>
    where
        S: SpecialVariables<G>,
    {
        let v = match v {
            | PositiveVariable::Special(s) => {
                return Err(format!(
                    "Protected word {s:?} used in for \
                                    assignment."
                ));
            },
            | PositiveVariable::Id(v) => v,
        };
        match ty {
            | PositiveAssertionTypes::RangeSet => {
                self.data
                    .insert(v.clone(), PositiveAssertionTypes::PositiveElement);
                Ok(())
            },
            | PositiveAssertionTypes::RangeInteger => {
                self.data.insert(v.clone(), PositiveAssertionTypes::Integer);
                Ok(())
            },
            | PositiveAssertionTypes::RangeNeighbours => {
                self.data.insert(v.clone(), PositiveAssertionTypes::Edge);
                Ok(())
            },
            | _ => Err(format!("Range has incorrect type {ty:?}.")),
        }
    }

    fn get<S, G>(
        &self,
        v: &PositiveVariable<S>,
    ) -> Result<PositiveAssertionTypes, String>
    where
        S: SpecialVariables<G>,
    {
        match v {
            | PositiveVariable::Special(s) => Ok(s.type_of()),
            | PositiveVariable::Id(v) =>
                if let Some(ty) = self.data.get(v) {
                    Ok(*ty)
                } else {
                    Err(format!("Could not find variable {v:?}."))
                },
        }
    }
}

impl<S> Context<S> {
    pub(super) fn new<G>(input: HashMap<S, G>) -> Self
    where
        S: SpecialVariables<G>,
    {
        Self {
            data:    HashMap::new(),
            special: S::new_context(input),
        }
    }

    fn assign<G>(
        &mut self,
        v: &PositiveVariable<S>,
        q: Option<&PositiveQualifier>,
        val: PositiveAssertReturnValue,
    ) -> Result<(), String>
    where
        S: SpecialVariables<G>,
    {
        match (v, q) {
            | (PositiveVariable::Id(v), None) => {
                self.data.insert(v.clone(), val);
                Ok(())
            },
            | (PositiveVariable::Id(v), Some(q)) => match self
                .data
                .entry(v.clone())
            {
                | std::collections::hash_map::Entry::Vacant(_ve) =>
                    Err(format!(
                        "Variable {v:?} as no assignment while \
                                     trying to assign to qualification {q:?}, \
                                     assign first a value."
                    )),
                | std::collections::hash_map::Entry::Occupied(mut oe) =>
                    match (oe.get_mut(), q, val) {
                        | (
                            &mut PositiveAssertReturnValue::Label(ref mut l),
                            PositiveQualifier::Restricted(q),
                            PositiveAssertReturnValue::Set(set),
                        ) => {
                            *q.referenced_mut(l) = set;
                            Ok(())
                        },
                        | (val, q, newval) => Err(format!(
                            "Variable {v:?} has value {val:?}, \
                                             but was assigned with qualifier \
                                             {q:?} new value {newval:?}."
                        )),
                    },
            },
            | (PositiveVariable::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:?}."))
                },
            | (PositiveVariable::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<G>(
        &self,
        v: &PositiveVariable<S>,
    ) -> Result<PositiveAssertReturnValue, String>
    where
        S: SpecialVariables<G>,
    {
        match v {
            | PositiveVariable::Id(var) =>
                self.data.get(var).cloned().ok_or(format!(
                    "Variable {v:?} used, but no value \
                                    assigned."
                )),
            | PositiveVariable::Special(s) =>
                self.special.get(s).cloned().ok_or(format!(
                    "Variable {v:?} used but no value \
                                    assigned."
                )),
        }
    }
}

impl PositiveAssertReturnValue {
    fn unary(
        self,
        u: &PositiveUnary,
        translator: &mut translator::Translator,
        graph: &graph::PositiveSystemGraph,
    ) -> Result<PositiveAssertReturnValue, String> {
        match (self, u) {
            | (PositiveAssertReturnValue::Boolean(b), PositiveUnary::Not) =>
                Ok(PositiveAssertReturnValue::Boolean(!b)),
            | (PositiveAssertReturnValue::Integer(i), PositiveUnary::Rand) =>
                Ok(PositiveAssertReturnValue::Integer(rand::random_range(0..i))),
            | (PositiveAssertReturnValue::Set(set), PositiveUnary::Empty) =>
                Ok(PositiveAssertReturnValue::Boolean(set.is_empty())),
            | (PositiveAssertReturnValue::String(s), PositiveUnary::Empty) =>
                Ok(PositiveAssertReturnValue::Boolean(s.is_empty())),
            | (PositiveAssertReturnValue::Set(set), PositiveUnary::Length) =>
                Ok(PositiveAssertReturnValue::Integer(set.len() as i64)),
            | (PositiveAssertReturnValue::String(s), PositiveUnary::Length) =>
                Ok(PositiveAssertReturnValue::Integer(s.len() as i64)),
            | (PositiveAssertReturnValue::Boolean(b), PositiveUnary::ToStr) =>
                Ok(PositiveAssertReturnValue::String(format!("{b}"))),
            | (PositiveAssertReturnValue::Integer(i), PositiveUnary::ToStr) =>
                Ok(PositiveAssertReturnValue::String(format!("{i}"))),
            | (
                PositiveAssertReturnValue::PositiveElement(el),
                PositiveUnary::ToStr,
            ) => Ok(PositiveAssertReturnValue::String(format!(
                "{}",
                translator::Formatter::from(translator, &el)
            ))),
            | (
                PositiveAssertReturnValue::Label(l),
                PositiveUnary::Qualifier(PositiveQualifier::Label(q)),
            ) => Ok(q.get(&l)),
            | (
                PositiveAssertReturnValue::Label(l),
                PositiveUnary::Qualifier(PositiveQualifier::Restricted(q)),
            ) => Ok(q.get(&l)),
            | (PositiveAssertReturnValue::String(s), PositiveUnary::ToEl) =>
                Ok(PositiveAssertReturnValue::PositiveElement(
                    match s.chars().nth(0) {
                        | Some('+') => (
                            translator
                                .encode(s.chars().skip(1).collect::<String>()),
                            element::IdState::Positive,
                        )
                            .into(),
                        | Some('-') => (
                            translator
                                .encode(s.chars().skip(1).collect::<String>()),
                            element::IdState::Negative,
                        )
                            .into(),
                        | _ => {
                            return Err(format!(
                                "Could not decode symbol from string {s}"
                            ));
                        },
                    },
                )),
            | (
                PositiveAssertReturnValue::Edge(edge),
                PositiveUnary::Qualifier(PositiveQualifier::Edge(
                    QualifierEdge::Source,
                )),
            ) => Ok(PositiveAssertReturnValue::Node(
                graph.edge_endpoints(edge).unwrap().0,
            )),
            | (
                PositiveAssertReturnValue::Edge(edge),
                PositiveUnary::Qualifier(PositiveQualifier::Edge(
                    QualifierEdge::Target,
                )),
            ) => Ok(PositiveAssertReturnValue::Node(
                graph.edge_endpoints(edge).unwrap().1,
            )),
            | (
                PositiveAssertReturnValue::Edge(edge),
                PositiveUnary::Qualifier(PositiveQualifier::Edge(
                    QualifierEdge::Label,
                )),
            ) => Ok(PositiveAssertReturnValue::Label(
                graph[edge].clone(),
            )),
            | (
                PositiveAssertReturnValue::Node(node),
                PositiveUnary::Qualifier(PositiveQualifier::Node(
                    QualifierNode::Neighbours,
                )),
            ) => Ok(PositiveAssertReturnValue::Neighbours(node)),
            | (
                PositiveAssertReturnValue::Node(node),
                PositiveUnary::Qualifier(PositiveQualifier::Node(
                    QualifierNode::System,
                )),
            ) => Ok(PositiveAssertReturnValue::System(
                graph.node_weight(node).unwrap().clone(),
            )),
            | (
                PositiveAssertReturnValue::System(sys),
                PositiveUnary::Qualifier(PositiveQualifier::System(q)),
            ) => Ok(q.get(&sys)),
            | (val, u) => Err(format!(
                "Incompatible unary operation {u:?} on value \
                             {val:?}."
            )),
        }
    }

    fn binary(
        self,
        b: &PositiveBinary,
        other: PositiveAssertReturnValue,
        _translator: &mut translator::Translator,
    ) -> Result<PositiveAssertReturnValue, String> {
        use PositiveAssertReturnValue::*;
        Ok(match (b, self, other) {
            | (PositiveBinary::And, Boolean(b1), Boolean(b2)) =>
                Boolean(b1 && b2),
            | (PositiveBinary::Or, Boolean(b1), Boolean(b2)) =>
                Boolean(b1 || b2),
            | (PositiveBinary::Xor, Boolean(b1), Boolean(b2)) =>
                Boolean(b1 ^ b2),
            | (PositiveBinary::Xor, Set(s1), Set(s2)) =>
                Set(s1.union(&s2).subtraction(&s1.intersection(&s2))),
            | (PositiveBinary::Less, Integer(i1), Integer(i2)) =>
                Boolean(i1 < i2),
            | (PositiveBinary::Less, Set(s1), Set(s2)) =>
                Boolean(s1.is_subset(&s2) && !s2.is_subset(&s1)),
            | (PositiveBinary::LessEq, Integer(i1), Integer(i2)) =>
                Boolean(i1 <= i2),
            | (PositiveBinary::LessEq, Set(s1), Set(s2)) =>
                Boolean(s1.is_subset(&s2)),
            | (PositiveBinary::More, Integer(i1), Integer(i2)) =>
                Boolean(i1 > i2),
            | (PositiveBinary::More, Set(s1), Set(s2)) =>
                Boolean(s2.is_subset(&s1) && !s1.is_subset(&s2)),
            | (PositiveBinary::MoreEq, Integer(i1), Integer(i2)) =>
                Boolean(i1 >= i2),
            | (PositiveBinary::MoreEq, Set(s1), Set(s2)) =>
                Boolean(s2.is_subset(&s1)),
            | (PositiveBinary::Eq, Integer(i1), Integer(i2)) =>
                Boolean(i1 == i2),
            | (PositiveBinary::Eq, Boolean(b1), Boolean(b2)) =>
                Boolean(b1 == b2),
            | (
                PositiveBinary::Eq,
                PositiveElement(el1),
                PositiveElement(el2),
            ) => Boolean(el1 == el2),
            | (PositiveBinary::Eq, Label(l1), Label(l2)) => Boolean(l1 == l2),
            | (PositiveBinary::Eq, String(s1), String(s2)) => Boolean(s1 == s2),
            | (PositiveBinary::Eq, Set(set1), Set(set2)) =>
                Boolean(set1 == set2),
            | (PositiveBinary::NotEq, Integer(i1), Integer(i2)) =>
                Boolean(i1 != i2),
            | (PositiveBinary::NotEq, Boolean(b1), Boolean(b2)) =>
                Boolean(b1 != b2),
            | (
                PositiveBinary::NotEq,
                PositiveElement(el1),
                PositiveElement(el2),
            ) => Boolean(el1 != el2),
            | (PositiveBinary::NotEq, Label(l1), Label(l2)) =>
                Boolean(l1 != l2),
            | (PositiveBinary::NotEq, String(s1), String(s2)) =>
                Boolean(s1 != s2),
            | (PositiveBinary::NotEq, Set(set1), Set(set2)) =>
                Boolean(set1 != set2),
            | (PositiveBinary::Plus, Integer(i1), Integer(i2)) =>
                Integer(i1 + i2),
            | (PositiveBinary::Plus, Set(set1), Set(set2)) =>
                Set(set1.union(&set2)),
            | (PositiveBinary::Minus, Integer(i1), Integer(i2)) =>
                Integer(i1 - i2),
            | (PositiveBinary::Minus, Set(set1), Set(set2)) =>
                Set(set1.subtraction(&set2)),
            | (PositiveBinary::Times, Integer(i1), Integer(i2)) =>
                Integer(i1 * i2),
            | (PositiveBinary::Times, Set(set1), Set(set2)) =>
                Set(set1.intersection(&set2)),
            | (PositiveBinary::Exponential, Integer(i1), Integer(i2)) =>
                if i2 < 0 {
                    Integer(0)
                } else {
                    Integer(i1.pow(i2 as u32))
                },
            | (PositiveBinary::Quotient, Integer(i1), Integer(i2)) =>
                Integer(i1.div_euclid(i2)),
            | (PositiveBinary::Reminder, Integer(i1), Integer(i2)) =>
                Integer(i1.rem_euclid(i2)),
            | (PositiveBinary::Concat, String(s1), String(s2)) =>
                String(s1 + &s2),
            | (PositiveBinary::Concat, Set(s), PositiveElement(e)) =>
                Set(s.union(&set::PositiveSet::from([e]))),
            | (PositiveBinary::SubStr, String(s1), String(s2)) => {
                let mut len = s1.len() as i64;
                for (p, c) in s1.chars().enumerate() {
                    if s2.chars().nth(p) != Some(c) {
                        len = p as i64;
                        break;
                    }
                }
                Integer(len)
            },
            | (PositiveBinary::Min, Integer(i1), Integer(i2)) =>
                Integer(i1.min(i2)),
            | (PositiveBinary::Max, Integer(i1), Integer(i2)) =>
                Integer(i1.max(i2)),
            | (PositiveBinary::CommonSubStr, String(s1), String(s2)) => {
                let mut s = std::string::String::new();
                for (p, c) in s1.chars().enumerate() {
                    if s2.chars().nth(p) != Some(c) {
                        break;
                    }
                    s.push(c);
                }
                String(s)
            },
            | (b, val1, val2) => {
                return Err(format!(
                    "Operation {b:?} on values {val1:?} and \
                                    {val2:?} could not be executed."
                ));
            },
        })
    }
}

fn typecheck_helper<S, G>(
    tree: &PositiveTree<S>,
    c: &mut TypeContext,
) -> Result<PositiveAssertionTypes, String>
where
    S: SpecialVariables<G>,
{
    match tree {
        | PositiveTree::Concat(t1, t2) => {
            typecheck_helper(t1, c)?;
            typecheck_helper(t2, c)
        },
        | PositiveTree::If(exp, t) => {
            match typecheck_expression(exp, c)? {
                | PositiveAssertionTypes::Boolean => {},
                | _ => {
                    return Err("Expression in if statement doesn't return a \
                                  boolean."
                        .to_string());
                },
            };
            typecheck_helper(t, c)
        },
        | PositiveTree::IfElse(exp, t1, t2) => {
            match typecheck_expression(exp, c)? {
                | PositiveAssertionTypes::Boolean => {},
                | _ => {
                    return Err("Expression in if statement doesn't return a \
                                  boolean."
                        .into());
                },
            };
            let type_t1 = typecheck_helper(t1, c)?;
            let type_t2 = typecheck_helper(t2, c)?;
            if type_t1 == type_t2 {
                Ok(type_t1)
            } else {
                Err("Branches of if statement do not match.".into())
            }
        },
        | PositiveTree::Assignment(assignvar, q, exp) => {
            let type_exp = typecheck_expression(exp, c)?;
            c.assign(assignvar, q.into(), type_exp)?;
            Ok(PositiveAssertionTypes::NoType)
        },
        | PositiveTree::Return(exp) => {
            let type_exp = typecheck_expression(exp, c)?;
            c.return_type(type_exp)?;
            Ok(PositiveAssertionTypes::NoType)
        },
        | PositiveTree::For(var, range, t) => {
            let type_range = typecheck_range(range, c)?;
            c.assign_range(var, type_range)?;
            typecheck_helper(t, c)
        },
    }
}

pub(super) fn typecheck<S, G>(
    tree: &PositiveTree<S>,
    c: &mut TypeContext,
) -> Result<PositiveAssertionTypes, String>
where
    S: SpecialVariables<G>,
{
    typecheck_helper(tree, c)?;
    Ok(c.return_ty.unwrap_or(PositiveAssertionTypes::NoType))
}

fn typecheck_expression<S, G>(
    exp: &PositiveExpression<S>,
    c: &TypeContext,
) -> Result<PositiveAssertionTypes, String>
where
    S: SpecialVariables<G>,
{
    match exp {
        | PositiveExpression::True | PositiveExpression::False =>
            Ok(PositiveAssertionTypes::Boolean),
        | PositiveExpression::Integer(_) => Ok(PositiveAssertionTypes::Integer),
        | PositiveExpression::Label(_) => Ok(PositiveAssertionTypes::Label),
        | PositiveExpression::Set(_) => Ok(PositiveAssertionTypes::Set),
        | PositiveExpression::PositiveElement(_) =>
            Ok(PositiveAssertionTypes::PositiveElement),
        | PositiveExpression::String(_) => Ok(PositiveAssertionTypes::String),
        | PositiveExpression::Var(v) => c.get(v),

        | PositiveExpression::Unary(u, exp) => {
            let type_exp = typecheck_expression(exp, c)?;
            u.associate(&type_exp)
        },

        | PositiveExpression::Binary(b, exp1, exp2) => {
            let type_exp1 = typecheck_expression(exp1, c)?;
            let type_exp2 = typecheck_expression(exp2, c)?;
            b.associate(&type_exp1, &type_exp2)
        },
    }
}

fn typecheck_range<S, G>(
    range: &PositiveRange<S>,
    c: &mut TypeContext,
) -> Result<PositiveAssertionTypes, String>
where
    S: SpecialVariables<G>,
{
    match range {
        | PositiveRange::IterateInRange(exp1, exp2) => {
            let type_exp1 = typecheck_expression(exp1, c)?;
            let type_exp2 = typecheck_expression(exp2, c)?;
            if let (
                PositiveAssertionTypes::Integer,
                PositiveAssertionTypes::Integer,
            ) = (type_exp1, type_exp2)
            {
                Ok(PositiveAssertionTypes::RangeInteger)
            } else {
                Err(format!(
                    "Expressions in range are not integers, but are: \
                             {type_exp1:?} and {type_exp2:?}."
                ))
            }
        },
        | PositiveRange::IterateOverSet(exp) => {
            let type_exp = typecheck_expression(exp, c)?;
            match type_exp {
                | PositiveAssertionTypes::Set =>
                    Ok(PositiveAssertionTypes::RangeSet),
                | PositiveAssertionTypes::RangeNeighbours =>
                    Ok(PositiveAssertionTypes::RangeNeighbours),
                | _ => Err(format!(
                    "Expressions in range is not a set or \
                                  neighbours of a node, but is: {type_exp:?}."
                )),
            }
        },
    }
}

pub(super) fn execute<S, G>(
    tree: &PositiveTree<S>,
    c: &mut Context<S>,
    translator: &mut translator::Translator,
    graph: &graph::PositiveSystemGraph,
) -> Result<Option<PositiveAssertReturnValue>, String>
where
    S: SpecialVariables<G>,
{
    match tree {
        | PositiveTree::Concat(t1, t2) => {
            if let Some(val) = execute(t1, c, translator, graph)? {
                Ok(Some(val))
            } else {
                execute(t2, c, translator, graph)
            }
        },
        | PositiveTree::If(exp, t) => {
            let guard = execute_exp(exp, c, translator, graph)?;
            if let PositiveAssertReturnValue::Boolean(true) = guard {
                execute(t, c, translator, graph)
            } else {
                Ok(None)
            }
        },
        | PositiveTree::IfElse(exp, t1, t2) => {
            let guard = execute_exp(exp, c, translator, graph)?;
            if let PositiveAssertReturnValue::Boolean(true) = guard {
                execute(t1, c, translator, graph)
            } else {
                execute(t2, c, translator, graph)
            }
        },
        | PositiveTree::Assignment(v, q, exp) => {
            let val = execute_exp(exp, c, translator, graph)?;
            c.assign(v, q.into(), val)?;
            Ok(None)
        },
        | PositiveTree::Return(exp) =>
            Ok(Some(execute_exp(exp, c, translator, graph)?)),
        | PositiveTree::For(v, r, t) => {
            let range = range_into_iter(r, c, translator, graph)?;
            for val in range {
                c.assign(v, None, val)?;
                if let Some(v) = execute(t, c, translator, graph)? {
                    return Ok(Some(v));
                }
            }
            Ok(None)
        },
    }
}

type RangeIterator = std::vec::IntoIter<PositiveAssertReturnValue>;

fn range_into_iter<S, G>(
    range: &PositiveRange<S>,
    c: &mut Context<S>,
    translator: &mut translator::Translator,
    graph: &graph::PositiveSystemGraph,
) -> Result<RangeIterator, String>
where
    S: SpecialVariables<G>,
{
    use petgraph::visit::EdgeRef;

    match range {
        | PositiveRange::IterateOverSet(exp) => {
            let val = execute_exp(exp, c, translator, graph)?;
            match val {
                | PositiveAssertReturnValue::Set(set) => Ok(set
                    .into_iter()
                    .map(|el| {
                        PositiveAssertReturnValue::PositiveElement(el.into())
                    })
                    .collect::<Vec<_>>()
                    .into_iter()),
                | PositiveAssertReturnValue::Neighbours(node) => Ok(graph
                    .edges(node)
                    .map(|x| PositiveAssertReturnValue::Edge(x.id()))
                    .collect::<Vec<_>>()
                    .into_iter()),
                | _ => Err(format!("{val:?} is not a set in for cycle.")),
            }
        },
        | PositiveRange::IterateInRange(exp1, exp2) => {
            let val1 = execute_exp(exp1, c, translator, graph)?;
            let val2 = execute_exp(exp2, c, translator, graph)?;
            match (val1, val2) {
                | (
                    PositiveAssertReturnValue::Integer(i1),
                    PositiveAssertReturnValue::Integer(i2),
                ) => Ok((i1..i2)
                    .map(PositiveAssertReturnValue::Integer)
                    .collect::<Vec<_>>()
                    .into_iter()),
                | (val1, val2) => Err(format!(
                    "{val1:?}..{val2:?} is not a valid integer \
                                 range in for cycle."
                )),
            }
        },
    }
}

fn execute_exp<S, G>(
    exp: &PositiveExpression<S>,
    c: &Context<S>,
    translator: &mut translator::Translator,
    graph: &graph::PositiveSystemGraph,
) -> Result<PositiveAssertReturnValue, String>
where
    S: SpecialVariables<G>,
{
    match exp {
        | PositiveExpression::True =>
            Ok(PositiveAssertReturnValue::Boolean(true)),
        | PositiveExpression::False =>
            Ok(PositiveAssertReturnValue::Boolean(false)),
        | PositiveExpression::Integer(i) =>
            Ok(PositiveAssertReturnValue::Integer(*i)),
        | PositiveExpression::Label(l) =>
            Ok(PositiveAssertReturnValue::Label(*l.clone())),
        | PositiveExpression::Set(set) =>
            Ok(PositiveAssertReturnValue::Set(set.clone())),
        | PositiveExpression::PositiveElement(el) =>
            Ok(PositiveAssertReturnValue::PositiveElement(*el)),
        | PositiveExpression::String(s) =>
            Ok(PositiveAssertReturnValue::String(s.clone())),
        | PositiveExpression::Var(var) => c.get(var),
        | PositiveExpression::Unary(u, exp) => {
            let val = execute_exp(exp, c, translator, graph)?;
            val.unary(u, translator, graph)
        },
        | PositiveExpression::Binary(b, exp1, exp2) => {
            let val1 = execute_exp(exp1, c, translator, graph)?;
            let val2 = execute_exp(exp2, c, translator, graph)?;
            val1.binary(b, val2, translator)
        },
    }
}