merc_syntax/
parse.rs

1use pest::Parser;
2use pest_derive::Parser;
3
4use merc_pest_consume::Error;
5use merc_utilities::MercError;
6
7use crate::CommExpr;
8use crate::DataExpr;
9use crate::DataExprBinaryOp;
10use crate::MultiAction;
11use crate::MultiActionLabel;
12use crate::ParseNode;
13use crate::StateFrmOp;
14use crate::UntypedActionRenameSpec;
15use crate::UntypedDataSpecification;
16use crate::UntypedPbes;
17use crate::UntypedPres;
18use crate::UntypedProcessSpecification;
19use crate::UntypedStateFrmSpec;
20
21#[derive(Parser)]
22#[grammar = "mcrl2_grammar.pest"]
23pub struct Mcrl2Parser;
24
25/// Parses the given mCRL2 specification into an AST.
26impl UntypedProcessSpecification {
27    pub fn parse(spec: &str) -> Result<UntypedProcessSpecification, MercError> {
28        let mut result = Mcrl2Parser::parse(Rule::MCRL2Spec, spec).map_err(extend_parser_error)?;
29        let root = result.next().expect("Could not parse mCRL2 specification");
30
31        Ok(Mcrl2Parser::MCRL2Spec(ParseNode::new(root))?)
32    }
33}
34
35/// Parses the given mCRL2 specification into an AST.
36impl UntypedDataSpecification {
37    pub fn parse(spec: &str) -> Result<UntypedDataSpecification, MercError> {
38        let mut result = Mcrl2Parser::parse(Rule::DataSpec, spec).map_err(extend_parser_error)?;
39        let root = result.next().expect("Could not parse mCRL2 data specification");
40
41        Ok(Mcrl2Parser::DataSpec(ParseNode::new(root))?)
42    }
43}
44
45impl DataExpr {
46    pub fn parse(spec: &str) -> Result<DataExpr, MercError> {
47        let mut result = Mcrl2Parser::parse(Rule::DataExpr, spec).map_err(extend_parser_error)?;
48        let root = result.next().expect("Could not parse mCRL2 data expression");
49
50        Ok(Mcrl2Parser::DataExpr(ParseNode::new(root))?)
51    }
52}
53
54impl MultiAction {
55    pub fn parse(spec: &str) -> Result<MultiAction, MercError> {
56        let mut result = Mcrl2Parser::parse(Rule::MultAct, spec).map_err(extend_parser_error)?;
57        let root = result.next().expect("Could not parse mCRL2 multi-action");
58
59        Ok(Mcrl2Parser::MultAct(ParseNode::new(root))?)
60    }
61}
62
63impl UntypedStateFrmSpec {
64    pub fn parse(spec: &str) -> Result<UntypedStateFrmSpec, MercError> {
65        let mut result = Mcrl2Parser::parse(Rule::StateFrmSpec, spec).map_err(extend_parser_error)?;
66        let root = result
67            .next()
68            .expect("Could not parse mCRL2 state formula specification");
69
70        Ok(Mcrl2Parser::StateFrmSpec(ParseNode::new(root))?)
71    }
72}
73
74impl UntypedActionRenameSpec {
75    pub fn parse(spec: &str) -> Result<UntypedActionRenameSpec, MercError> {
76        let mut result = Mcrl2Parser::parse(Rule::ActionRenameSpec, spec).map_err(extend_parser_error)?;
77        let root = result
78            .next()
79            .expect("Could not parse mCRL2 action rename specification");
80
81        Ok(Mcrl2Parser::ActionRenameSpec(ParseNode::new(root))?)
82    }
83}
84
85impl UntypedPbes {
86    pub fn parse(spec: &str) -> Result<UntypedPbes, MercError> {
87        let mut result = Mcrl2Parser::parse(Rule::PbesSpec, spec).map_err(extend_parser_error)?;
88        let root = result
89            .next()
90            .expect("Could not parse parameterised boolean equation system");
91
92        Ok(Mcrl2Parser::PbesSpec(ParseNode::new(root))?)
93    }
94}
95
96impl UntypedPres {
97    pub fn parse(spec: &str) -> Result<UntypedPres, MercError> {
98        let mut result = Mcrl2Parser::parse(Rule::PresSpec, spec).map_err(extend_parser_error)?;
99        let root = result
100            .next()
101            .expect("Could not parse parameterised real equation system");
102
103        Ok(Mcrl2Parser::PresSpec(ParseNode::new(root))?)
104    }
105}
106
107/// Parses a list of communication expressions from the given input string.
108pub fn parse_comm_expr_set(input: &str) -> Result<Vec<CommExpr>, MercError> {
109    let mut result = Mcrl2Parser::parse(Rule::CommExprSet, input).map_err(extend_parser_error)?;
110    let root = result.next().expect("Could not parse communication expression set");
111
112    Ok(Mcrl2Parser::CommExprSet(ParseNode::new(root))?)
113}
114
115/// Parses a list of action names from the given input string, for example those used in the hide operator.
116pub fn parse_action_names(input: &str) -> Result<Vec<String>, MercError> {
117    let mut result = Mcrl2Parser::parse(Rule::ActIdSet, input).map_err(extend_parser_error)?;
118    let root = result.next().expect("Could not parse action name list");
119
120    Ok(Mcrl2Parser::ActIdSet(ParseNode::new(root))?)
121}
122
123/// Parses the action names for the allow operator from the given input string.
124pub fn parse_allow_action_names(input: &str) -> Result<Vec<MultiActionLabel>, MercError> {
125    let mut result = Mcrl2Parser::parse(Rule::MultActIdSet, input).map_err(extend_parser_error)?;
126    let root = result.next().expect("Could not parse allow set name list");
127
128    Ok(Mcrl2Parser::MultActIdSet(ParseNode::new(root))?)
129}
130
131fn extend_parser_error(error: Error<Rule>) -> Error<Rule> {
132    error.renamed_rules(|rule| match rule {
133        Rule::DataExprWhr => "DataExpr whr AssignmentList end".to_string(),
134        Rule::DataExprUpdate => "DataExpr[(DataExpr -> DataExpr)*]".to_string(),
135        Rule::DataExprApplication => "DataExpr(DataExpr*)".to_string(),
136
137        // DataExpr Binary Operators
138        Rule::DataExprConj => format!("{}", DataExprBinaryOp::Conj),
139        Rule::DataExprDisj => format!("{}", DataExprBinaryOp::Disj),
140        Rule::DataExprImpl => format!("{}", DataExprBinaryOp::Implies),
141        Rule::DataExprEq => format!("{}", DataExprBinaryOp::Equal),
142        Rule::DataExprNeq => format!("{}", DataExprBinaryOp::NotEqual),
143        Rule::DataExprLess => format!("{}", DataExprBinaryOp::LessThan),
144        Rule::DataExprLeq => format!("{}", DataExprBinaryOp::LessEqual),
145        Rule::DataExprGreater => format!("{}", DataExprBinaryOp::GreaterThan),
146        Rule::DataExprGeq => format!("{}", DataExprBinaryOp::GreaterEqual),
147        Rule::DataExprIn => format!("{}", DataExprBinaryOp::In),
148        Rule::DataExprDiv => format!("{}", DataExprBinaryOp::Div),
149        Rule::DataExprIntDiv => format!("{}", DataExprBinaryOp::IntDiv),
150        Rule::DataExprMod => format!("{}", DataExprBinaryOp::Mod),
151        Rule::DataExprMult => format!("{}", DataExprBinaryOp::Multiply),
152        Rule::DataExprAdd => format!("{}", DataExprBinaryOp::Add),
153        Rule::DataExprSubtract => format!("{}", DataExprBinaryOp::Subtract),
154        Rule::DataExprAt => format!("{}", DataExprBinaryOp::At),
155        Rule::DataExprCons => format!("{}", DataExprBinaryOp::Cons),
156        Rule::DataExprSnoc => format!("{}", DataExprBinaryOp::Snoc),
157        Rule::DataExprConcat => format!("{}", DataExprBinaryOp::Concat),
158
159        // Regular Formulas
160        Rule::RegFrmAlternative => "RegFrm + RegFrm".to_string(),
161        Rule::RegFrmComposition => "RegFrm . RegFrm".to_string(),
162        Rule::RegFrmIteration => "RegFrm*".to_string(),
163        Rule::RegFrmPlus => "RegFrm+".to_string(),
164
165        // State formulas
166        Rule::StateFrmAddition => format!("{}", StateFrmOp::Addition),
167        Rule::StateFrmLeftConstantMultiply => "Number * StateFrm".to_string(),
168        Rule::StateFrmImplication => format!("{}", StateFrmOp::Implies),
169        Rule::StateFrmDisjunction => format!("{}", StateFrmOp::Disjunction),
170        Rule::StateFrmConjunction => format!("{}", StateFrmOp::Conjunction),
171        Rule::StateFrmRightConstantMultiply => "StateFrm * Number".to_string(),
172        _ => format!("{rule:?}"),
173    })
174}
merc_syntax/parse.rs

merc_syntax/
parse.rs
