1 
use std::fmt;
2 

            

        

            

                3
            

            

                
            

            

                
#[derive(Debug)]

            

        

            

                4
            

            

                
            

            

                
pub struct Mcrl2Specification {

            

        

            

                5
            

            

                
            

            

                
    pub map: Vec<IdsDecl>,

            

        

            

                6
            

            

                
            

            

                
}

            

        

            

                7
            

            

                
            

            

                

            

        

            

                8
            

            

                
            

            

                
#[derive(Debug)]

            

        

            

                9
            

            

                
            

            

                
pub struct IdsDecl {

            

        

            

                10
            

            

                
            

            

                
    pub identifiers: Vec<String>,

            

        

            

                11
            

            

                
            

            

                
    pub sort: SortExpression,

            

        

            

                12
            

            

                
            

            

                
    pub span: Span,

            

        

            

                13
            

            

                
            

            

                
}

            

        

            

                14
            

            

                
            

            

                

            

        

            

                15
            

            

                
            

            

                
#[derive(Debug)]

            

        

            

                16
            

            

                
            

            

                
pub enum SortExpression {

            

        

            

                17
            

            

                
            

            

                
    Product {

            

        

            

                18
            

            

                
            

            

                
        lhs: Box<SortExpression>,

            

        

            

                19
            

            

                
            

            

                
        rhs: Box<SortExpression>,

            

        

            

                20
            

            

                
            

            

                
    },

            

        

            

                21
            

            

                
            

            

                
    Function {

            

        

            

                22
            

            

                
            

            

                
        domain: Box<SortExpression>,

            

        

            

                23
            

            

                
            

            

                
        range: Box<SortExpression>,

            

        

            

                24
            

            

                
            

            

                
    },

            

        

            

                25
            

            

                
            

            

                
    Reference(String),

            

        

            

                26
            

            

                
            

            

                
    Simple(Sort),

            

        

            

                27
            

            

                
            

            

                
    Complex(ComplexSort, Box<SortExpression>),

            

        

            

                28
            

            

                
            

            

                
}

            

        

            

                29
            

            

                
            

            

                

            

        

            

                30
            

            

                
            

            

                
#[derive(Debug)]

            

        

            

                31
            

            

                
            

            

                
pub enum Sort {

            

        

            

                32
            

            

                
            

            

                
    Bool,

            

        

            

                33
            

            

                
            

            

                
    Pos,

            

        

            

                34
            

            

                
            

            

                
    Int,

            

        

            

                35
            

            

                
            

            

                
    Nat,

            

        

            

                36
            

            

                
            

            

                
    Real,

            

        

            

                37
            

            

                
            

            

                
}

            

        

            

                38
            

            

                
            

            

                

            

        

            

                39
            

            

                
            

            

                
#[derive(Debug)]

            

        

            

                40
            

            

                
            

            

                
pub enum ComplexSort {

            

        

            

                41
            

            

                
            

            

                
    List,

            

        

            

                42
            

            

                
            

            

                
    Set,

            

        

            

                43
            

            

                
            

            

                
    FSet,

            

        

            

                44
            

            

                
            

            

                
    FBag,

            

        

            

                45
            

            

                
            

            

                
}

            

        

            

                46
            

            

                
            

            

                

            

        

            

                47
            

            

                
            

            

                
pub struct Span {

            

        

            

                48
            

            

                
            

            

                
    start: usize,

            

        

            

                49
            

            

                
            

            

                
    end: usize,

            

        

            

                50
            

            

                
            

            

                
}

            

        

            

                51
            

            

                
            

            

                

            

        

            

                52
            

            

                
            

            

                
impl From<pest::Span<'_>> for Span {

            

        

            

                53
            

            

                
            

            

                
    fn from(span: pest::Span) -> Self {

            

        

            

                54
            

            

                
            

            

                
        Span {

            

        

            

                55
            

            

                
            

            

                
            start: span.start(),

            

        

            

                56
            

            

                
            

            

                
            end: span.end(),

            

        

            

                57
            

            

                
            

            

                
        }

            

        

            

                58
            

            

                
            

            

                
    }

            

        

            

                59
            

            

                
            

            

                
}

            

        

            

                60
            

            

                
            

            

                

            

        

            

                61
            

            

                
            

            

                
pub fn print_location(input: &str, span: &Span) {

            

        

            

                62
            

            

                
            

            

                
    input.lines().enumerate().fold(span.start, |current, (number, line)| {

            

        

            

                63
            

            

                
            

            

                
        if current < line.len() {

            

        

            

                64
            

            

                
            

            

                
            println!("ln {number}, col {}", span.start - current);

            

        

            

                65
            

            

                
            

            

                
        }

            

        

            

                66
            

            

                
            

            

                

            

        

            

                67
            

            

                
            

            

                
        current - line.len()

            

        

            

                68
            

            

                
            

            

                
    });

            

        

            

                69
            

            

                
            

            

                
}

            

        

            

                70
            

            

                
            

            

                

            

        

            

                71
            

            

                
            

            

                
impl fmt::Debug for Span {

            

        

            

                72
            

            

                
            

            

                
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

            

        

            

                73
            

            

                
            

            

                
        write!(f, "{}..{}", self.start, self.end)

            

        

            

                74
            

            

                
            

            

                
    }

            

        

            

                75
            

            

                
            

            

                
}

            

        

            

                76
            

            

                
            

            

                

            

        

            

                77
            

            

                
            

            

                
impl fmt::Display for Sort {

            

        

            

                78
            

            

                
            

            

                
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

            

        

            

                79
            

            

                
            

            

                
        write!(f, "{:?}", self)

            

        

            

                80
            

            

                
            

            

                
    }

            

        

            

                81
            

            

                
            

            

                
}

            

        

            

                82
            

            

                
            

            

                

            

        

            

                83
            

            

                
            

            

                
impl fmt::Display for ComplexSort {

            

        

            

                84
            

            

                
            

            

                
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

            

        

            

                85
            

            

                
            

            

                
        write!(f, "{:?}", self)

            

        

            

                86
            

            

                
            

            

                
    }

            

        

            

                87
            

            

                
            

            

                
}

            

        

            

                88
            

            

                
            

            

                

            

        

            

                89
            

            

                
            

            

                
impl fmt::Display for Mcrl2Specification {

            

        

            

                90
            

            

                1
            

            

                
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

            

        

            

                91
            

            

                1
            

            

                
        for decl in &self.map {

            

        

            

                92
            

            

                
            

            

                
            writeln!(f, "{}", decl)?;

            

        

            

                93
            

            

                
            

            

                
        }

            

        

            

                94
            

            

                1
            

            

                
        Ok(())

            

        

            

                95
            

            

                1
            

            

                
    }

            

        

            

                96
            

            

                
            

            

                
}

            

        

            

                97
            

            

                
            

            

                

            

        

            

                98
            

            

                
            

            

                
impl fmt::Display for IdsDecl {

            

        

            

                99
            

            

                
            

            

                
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

            

        

            

                100
            

            

                
            

            

                
        write!(f, "{} : {}", self.identifiers.join(", "), self.sort)

            

        

            

                101
            

            

                
            

            

                
    }

            

        

            

                102
            

            

                
            

            

                
}

            

        

            

                103
            

            

                
            

            

                

            

        

            

                104
            

            

                
            

            

                
impl fmt::Display for SortExpression {

            

        

            

                105
            

            

                
            

            

                
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

            

        

            

                106
            

            

                
            

            

                
        match self {

            

        

            

                107
            

            

                
            

            

                
            SortExpression::Product { lhs, rhs } => write!(f, "({} # {})", lhs, rhs),

            

        

            

                108
            

            

                
            

            

                
            SortExpression::Function { domain, range } => write!(f, "({} -> {})", domain, range),

            

        

            

                109
            

            

                
            

            

                
            SortExpression::Reference(ident) => write!(f, "\"{}\"", ident),

            

        

            

                110
            

            

                
            

            

                
            SortExpression::Simple(sort) => write!(f, "{}", sort),

            

        

            

                111
            

            

                
            

            

                
            SortExpression::Complex(complex, inner) => write!(f, "{}({})", complex, inner),

            

        

            

                112
            

            

                
            

            

                
        }

            

        

            

                113
            

            

                
            

            

                
    }

            

        

            

                114
            

            

                
            

            

                
}