merc_syntax/
precedence.rs

1use std::sync::LazyLock;
2
3use pest::iterators::Pair;
4use pest::iterators::Pairs;
5use pest::pratt_parser::Assoc;
6use pest::pratt_parser::Assoc::Left;
7use pest::pratt_parser::Assoc::Right;
8use pest::pratt_parser::Op;
9use pest::pratt_parser::PrattParser;
10
11use merc_pest_consume::Node;
12
13use crate::ActFrm;
14use crate::ActFrmBinaryOp;
15use crate::Bound;
16use crate::DataExpr;
17use crate::DataExprBinaryOp;
18use crate::DataExprUnaryOp;
19use crate::FixedPointOperator;
20use crate::Mcrl2Parser;
21use crate::ModalityOperator;
22use crate::ParseResult;
23use crate::PbesExpr;
24use crate::PbesExprBinaryOp;
25use crate::PresExpr;
26use crate::PresExprBinaryOp;
27use crate::ProcExprBinaryOp;
28use crate::ProcessExpr;
29use crate::Quantifier;
30use crate::RegFrm;
31use crate::Rule;
32use crate::Sort;
33use crate::StateFrm;
34use crate::StateFrmOp;
35use crate::StateFrmUnaryOp;
36use crate::syntax_tree::SortExpression;
37
38pub static SORT_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {
39    // Precedence is defined lowest to highest
40    PrattParser::new()
41        // Sort operators
42        .op(Op::infix(Rule::SortExprFunction, Left)) // $right 0
43        .op(Op::infix(Rule::SortExprProduct, Right)) // $left 1
44});
45
46#[allow(clippy::result_large_err)]
47pub fn parse_sortexpr_primary(primary: Pair<'_, Rule>) -> ParseResult<SortExpression> {
48    match primary.as_rule() {
49        Rule::IdAt => Ok(SortExpression::Reference(Mcrl2Parser::IdAt(Node::new(primary))?)),
50        Rule::SortExpr => Mcrl2Parser::SortExpr(Node::new(primary)),
51
52        Rule::SortExprBool => Ok(SortExpression::Simple(Sort::Bool)),
53        Rule::SortExprInt => Ok(SortExpression::Simple(Sort::Int)),
54        Rule::SortExprPos => Ok(SortExpression::Simple(Sort::Pos)),
55        Rule::SortExprNat => Ok(SortExpression::Simple(Sort::Nat)),
56        Rule::SortExprReal => Ok(SortExpression::Simple(Sort::Real)),
57
58        Rule::SortExprList => Mcrl2Parser::SortExprList(Node::new(primary)),
59        Rule::SortExprSet => Mcrl2Parser::SortExprSet(Node::new(primary)),
60        Rule::SortExprBag => Mcrl2Parser::SortExprBag(Node::new(primary)),
61        Rule::SortExprFSet => Mcrl2Parser::SortExprFSet(Node::new(primary)),
62        Rule::SortExprFBag => Mcrl2Parser::SortExprFBag(Node::new(primary)),
63
64        Rule::SortExprParens => {
65            // Handle parentheses by recursively parsing the inner expression
66            let inner = primary
67                .into_inner()
68                .next()
69                .expect("Expected inner expression in brackets");
70            parse_sortexpr(inner.into_inner())
71        }
72
73        Rule::SortExprStruct => Mcrl2Parser::SortExprStruct(Node::new(primary)),
74        _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),
75    }
76}
77
78/// Parses a sequence of `Rule` pairs into a `SortExpression` using a Pratt parser for operator precedence.
79#[allow(clippy::result_large_err)]
80pub fn parse_sortexpr(pairs: Pairs<Rule>) -> ParseResult<SortExpression> {
81    SORT_PRATT_PARSER
82        .map_primary(|primary| parse_sortexpr_primary(primary))
83        .map_infix(|lhs, op, rhs| match op.as_rule() {
84            Rule::SortExprFunction => Ok(SortExpression::Function {
85                domain: Box::new(lhs?),
86                range: Box::new(rhs?),
87            }),
88            Rule::SortExprProduct => Ok(SortExpression::Product {
89                lhs: Box::new(lhs?),
90                rhs: Box::new(rhs?),
91            }),
92            _ => unimplemented!("Unexpected binary operator: {:?}", op.as_rule()),
93        })
94        .parse(pairs)
95}
96
97pub static DATAEXPR_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {
98    // Precedence is defined lowest to highest
99    PrattParser::new()
100        .op(Op::postfix(Rule::DataExprWhr)) // $left 0
101        .op(Op::prefix(Rule::DataExprForall) | Op::prefix(Rule::DataExprExists) | Op::prefix(Rule::DataExprLambda)) // $right 1
102        .op(Op::infix(Rule::DataExprImpl, Assoc::Right)) // $right 2
103        .op(Op::infix(Rule::DataExprDisj, Assoc::Right)) // $right 3
104        .op(Op::infix(Rule::DataExprConj, Assoc::Right)) // $right 4
105        .op(Op::infix(Rule::DataExprEq, Assoc::Left) | Op::infix(Rule::DataExprNeq, Assoc::Left)) // $left 5
106        .op(Op::infix(Rule::DataExprLess, Assoc::Left)
107            | Op::infix(Rule::DataExprLeq, Assoc::Left)
108            | Op::infix(Rule::DataExprGeq, Assoc::Left)
109            | Op::infix(Rule::DataExprGreater, Assoc::Left)
110            | Op::infix(Rule::DataExprIn, Assoc::Left)) // $left 6
111        .op(Op::infix(Rule::DataExprCons, Assoc::Right)) // $right 7
112        .op(Op::infix(Rule::DataExprSnoc, Assoc::Left)) // $left 8
113        .op(Op::infix(Rule::DataExprConcat, Assoc::Left)) // $left 9
114        .op(Op::infix(Rule::DataExprAdd, Assoc::Left) | Op::infix(Rule::DataExprSubtract, Assoc::Left)) // $left 10
115        .op(Op::infix(Rule::DataExprDiv, Assoc::Left)
116            | Op::infix(Rule::DataExprIntDiv, Assoc::Left)
117            | Op::infix(Rule::DataExprMod, Assoc::Left)) // $left 11
118        .op(Op::infix(Rule::DataExprMult, Assoc::Left)
119            | Op::infix(Rule::DataExprAt, Assoc::Left) // $left 12
120            | Op::prefix(Rule::DataExprMinus)
121            | Op::prefix(Rule::DataExprNegation)
122            | Op::prefix(Rule::DataExprSize)) // $right 12
123        .op(Op::postfix(Rule::DataExprUpdate) | Op::postfix(Rule::DataExprApplication)) // ) // $left 13
124});
125
126#[allow(clippy::result_large_err)]
127pub fn parse_dataexpr(pairs: Pairs<Rule>) -> ParseResult<DataExpr> {
128    DATAEXPR_PRATT_PARSER
129        .map_primary(|primary| match primary.as_rule() {
130            Rule::DataExprTrue => Ok(DataExpr::Bool(true)),
131            Rule::DataExprFalse => Ok(DataExpr::Bool(false)),
132            Rule::DataExprEmptyList => Ok(DataExpr::EmptyList),
133            Rule::DataExprEmptySet => Ok(DataExpr::EmptySet),
134            Rule::DataExprEmptyBag => Ok(DataExpr::EmptyBag),
135            Rule::DataExprListEnum => Mcrl2Parser::DataExprListEnum(Node::new(primary)),
136            Rule::DataExprBagEnum => Mcrl2Parser::DataExprBagEnum(Node::new(primary)),
137            Rule::DataExprSetBagComp => Mcrl2Parser::DataExprSetBagComp(Node::new(primary)),
138            Rule::DataExprSetEnum => Mcrl2Parser::DataExprSetEnum(Node::new(primary)),
139            Rule::Number => Mcrl2Parser::Number(Node::new(primary)),
140            Rule::IdAt => Ok(DataExpr::Id(Mcrl2Parser::IdAt(Node::new(primary))?)),
141
142            Rule::DataExprBrackets => {
143                // Handle parentheses by recursively parsing the inner expression
144                let inner = primary
145                    .into_inner()
146                    .next()
147                    .expect("Expected inner expression in brackets");
148                parse_dataexpr(inner.into_inner())
149            }
150
151            _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),
152        })
153        .map_infix(|lhs, op, rhs| {
154            let op = match op.as_rule() {
155                Rule::DataExprConj => DataExprBinaryOp::Conj,
156                Rule::DataExprDisj => DataExprBinaryOp::Disj,
157                Rule::DataExprEq => DataExprBinaryOp::Equal,
158                Rule::DataExprNeq => DataExprBinaryOp::NotEqual,
159                Rule::DataExprLess => DataExprBinaryOp::LessThan,
160                Rule::DataExprLeq => DataExprBinaryOp::LessEqual,
161                Rule::DataExprGreater => DataExprBinaryOp::GreaterThan,
162                Rule::DataExprGeq => DataExprBinaryOp::GreaterEqual,
163                Rule::DataExprIn => DataExprBinaryOp::In,
164                Rule::DataExprCons => DataExprBinaryOp::Cons,
165                Rule::DataExprSnoc => DataExprBinaryOp::Snoc,
166                Rule::DataExprConcat => DataExprBinaryOp::Concat,
167                Rule::DataExprAdd => DataExprBinaryOp::Add,
168                Rule::DataExprSubtract => DataExprBinaryOp::Subtract,
169                Rule::DataExprDiv => DataExprBinaryOp::Div,
170                Rule::DataExprIntDiv => DataExprBinaryOp::IntDiv,
171                Rule::DataExprMod => DataExprBinaryOp::Mod,
172                Rule::DataExprMult => DataExprBinaryOp::Multiply,
173                Rule::DataExprAt => DataExprBinaryOp::At,
174                Rule::DataExprImpl => DataExprBinaryOp::Implies,
175                _ => unimplemented!("Unexpected binary operator rule: {:?}", op.as_rule()),
176            };
177
178            Ok(DataExpr::Binary {
179                op,
180                lhs: Box::new(lhs?),
181                rhs: Box::new(rhs?),
182            })
183        })
184        .map_postfix(|expr, postfix| match postfix.as_rule() {
185            Rule::DataExprUpdate => Ok(DataExpr::FunctionUpdate {
186                expr: Box::new(expr?),
187                update: Box::new(Mcrl2Parser::DataExprUpdate(Node::new(postfix))?),
188            }),
189            Rule::DataExprApplication => Ok(DataExpr::Application {
190                function: Box::new(expr?),
191                arguments: Mcrl2Parser::DataExprApplication(Node::new(postfix))?,
192            }),
193            Rule::DataExprWhr => Ok(DataExpr::Whr {
194                expr: Box::new(expr?),
195                assignments: Mcrl2Parser::DataExprWhr(Node::new(postfix))?,
196            }),
197            _ => unimplemented!("Unexpected postfix operator: {:?}", postfix.as_rule()),
198        })
199        .map_prefix(|prefix, expr| match prefix.as_rule() {
200            Rule::DataExprForall => Ok(DataExpr::Quantifier {
201                op: Quantifier::Forall,
202                variables: Mcrl2Parser::DataExprForall(Node::new(prefix))?,
203                body: Box::new(expr?),
204            }),
205            Rule::DataExprExists => Ok(DataExpr::Quantifier {
206                op: Quantifier::Exists,
207                variables: Mcrl2Parser::DataExprExists(Node::new(prefix))?,
208                body: Box::new(expr?),
209            }),
210            Rule::DataExprLambda => Ok(DataExpr::Lambda {
211                variables: Mcrl2Parser::DataExprLambda(Node::new(prefix))?,
212                body: Box::new(expr?),
213            }),
214            Rule::DataExprNegation => Ok(DataExpr::Unary {
215                op: DataExprUnaryOp::Negation,
216                expr: Box::new(expr?),
217            }),
218            Rule::DataExprMinus => Ok(DataExpr::Unary {
219                op: DataExprUnaryOp::Minus,
220                expr: Box::new(expr?),
221            }),
222            Rule::DataExprSize => Ok(DataExpr::Unary {
223                op: DataExprUnaryOp::Size,
224                expr: Box::new(expr?),
225            }),
226            _ => unimplemented!("Unexpected prefix operator: {:?}", prefix.as_rule()),
227        })
228        .parse(pairs)
229}
230
231pub static PROCEXPR_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {
232    // Precedence is defined lowest to highest
233    PrattParser::new()
234        .op(Op::infix(Rule::ProcExprChoice, Assoc::Left)) // $left 1
235        .op(Op::prefix(Rule::ProcExprSum) | Op::prefix(Rule::ProcExprDist)) // $right 2
236        .op(Op::infix(Rule::ProcExprParallel, Assoc::Right)) // $right 3
237        .op(Op::infix(Rule::ProcExprLeftMerge, Assoc::Right)) // $right 4
238        .op(Op::prefix(Rule::ProcExprIf)) // $right 5
239        .op(Op::prefix(Rule::ProcExprIfThen)) // $right 5
240        .op(Op::infix(Rule::ProcExprUntil, Assoc::Left)) // $left 6
241        .op(Op::infix(Rule::ProcExprSeq, Assoc::Right)) // $right 7
242        .op(Op::postfix(Rule::ProcExprAt)) // $left 8
243        .op(Op::infix(Rule::ProcExprSync, Assoc::Left)) // $left 9
244});
245
246#[allow(clippy::result_large_err)]
247pub fn parse_process_expr(pairs: Pairs<Rule>) -> ParseResult<ProcessExpr> {
248    PROCEXPR_PRATT_PARSER
249        .map_primary(|primary| match primary.as_rule() {
250            Rule::ProcExprId => Ok(Mcrl2Parser::ProcExprId(Node::new(primary))?),
251            Rule::ProcExprDelta => Ok(ProcessExpr::Delta),
252            Rule::ProcExprTau => Ok(ProcessExpr::Tau),
253            Rule::ProcExprBlock => Ok(Mcrl2Parser::ProcExprBlock(Node::new(primary))?),
254            Rule::ProcExprAllow => Ok(Mcrl2Parser::ProcExprAllow(Node::new(primary))?),
255            Rule::ProcExprHide => Ok(Mcrl2Parser::ProcExprHide(Node::new(primary))?),
256            Rule::ProcExprRename => Ok(Mcrl2Parser::ProcExprRename(Node::new(primary))?),
257            Rule::ProcExprComm => Ok(Mcrl2Parser::ProcExprComm(Node::new(primary))?),
258            Rule::Action => {
259                let action = Mcrl2Parser::Action(Node::new(primary))?;
260
261                Ok(ProcessExpr::Action(action.id, action.args))
262            }
263            Rule::ProcExprBrackets => {
264                // Handle parentheses by recursively parsing the inner expression
265                let inner = primary
266                    .into_inner()
267                    .next()
268                    .expect("Expected inner expression in brackets");
269                parse_process_expr(inner.into_inner())
270            }
271            _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),
272        })
273        .map_infix(|lhs, op, rhs| match op.as_rule() {
274            Rule::ProcExprChoice => Ok(ProcessExpr::Binary {
275                op: ProcExprBinaryOp::Choice,
276                lhs: Box::new(lhs?),
277                rhs: Box::new(rhs?),
278            }),
279            Rule::ProcExprParallel => Ok(ProcessExpr::Binary {
280                op: ProcExprBinaryOp::Parallel,
281                lhs: Box::new(lhs?),
282                rhs: Box::new(rhs?),
283            }),
284            Rule::ProcExprLeftMerge => Ok(ProcessExpr::Binary {
285                op: ProcExprBinaryOp::LeftMerge,
286                lhs: Box::new(lhs?),
287                rhs: Box::new(rhs?),
288            }),
289            Rule::ProcExprSeq => Ok(ProcessExpr::Binary {
290                op: ProcExprBinaryOp::Sequence,
291                lhs: Box::new(lhs?),
292                rhs: Box::new(rhs?),
293            }),
294            Rule::ProcExprSync => Ok(ProcessExpr::Binary {
295                op: ProcExprBinaryOp::CommMerge,
296                lhs: Box::new(lhs?),
297                rhs: Box::new(rhs?),
298            }),
299            _ => unimplemented!("Unexpected rule: {:?}", op.as_rule()),
300        })
301        .map_prefix(|prefix, expr| match prefix.as_rule() {
302            Rule::ProcExprSum => Ok(ProcessExpr::Sum {
303                variables: Mcrl2Parser::ProcExprSum(Node::new(prefix))?,
304                operand: Box::new(expr?),
305            }),
306            Rule::ProcExprDist => {
307                let (variables, data_expr) = Mcrl2Parser::ProcExprDist(Node::new(prefix))?;
308
309                Ok(ProcessExpr::Dist {
310                    variables,
311                    expr: data_expr,
312                    operand: Box::new(expr?),
313                })
314            }
315            Rule::ProcExprIf => {
316                let condition = Mcrl2Parser::ProcExprIf(Node::new(prefix))?;
317
318                Ok(ProcessExpr::Condition {
319                    condition,
320                    then: Box::new(expr?),
321                    else_: None,
322                })
323            }
324            Rule::ProcExprIfThen => {
325                let (condition, then) = Mcrl2Parser::ProcExprIfThen(Node::new(prefix))?;
326
327                Ok(ProcessExpr::Condition {
328                    condition,
329                    then: Box::new(then),
330                    else_: Some(Box::new(expr?)),
331                })
332            }
333            _ => unimplemented!("Unexpected rule: {:?}", prefix.as_rule()),
334        })
335        .map_postfix(|expr, postfix| match postfix.as_rule() {
336            Rule::ProcExprAt => Ok(ProcessExpr::At {
337                expr: Box::new(expr?),
338                operand: Mcrl2Parser::ProcExprAt(Node::new(postfix))?,
339            }),
340            _ => unimplemented!("Unexpected postfix rule: {:?}", postfix.as_rule()),
341        })
342        .parse(pairs)
343}
344
345/// Defines the operator precedence for action formulas using a Pratt parser.
346pub static ACTFRM_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {
347    // Precedence is defined lowest to highest
348    PrattParser::new()
349        .op(Op::prefix(Rule::ActFrmExists) | Op::prefix(Rule::ActFrmForall)) // $right  0
350        .op(Op::infix(Rule::ActFrmImplies, Assoc::Right)) //  $right 2
351        .op(Op::infix(Rule::ActFrmUnion, Assoc::Right)) // $right 3
352        .op(Op::infix(Rule::ActFrmIntersect, Assoc::Right)) // $right 4
353        .op(Op::postfix(Rule::ActFrmAt)) //  $left 5
354        .op(Op::prefix(Rule::ActFrmNegation)) // $right 6
355});
356
357/// Parses a sequence of `Rule` pairs into an `ActFrm` using a Pratt parser defined in [ACTFRM_PRATT_PARSER] for operator precedence.
358#[allow(clippy::result_large_err)]
359pub fn parse_actfrm(pairs: Pairs<Rule>) -> ParseResult<ActFrm> {
360    ACTFRM_PRATT_PARSER
361        .map_primary(|primary| {
362            match primary.as_rule() {
363                Rule::ActFrmTrue => Ok(ActFrm::True),
364                Rule::ActFrmFalse => Ok(ActFrm::False),
365                Rule::MultAct => Ok(ActFrm::MultAct(Mcrl2Parser::MultAct(Node::new(primary))?)),
366                Rule::DataValExpr => Ok(ActFrm::DataExprVal(Mcrl2Parser::DataValExpr(Node::new(primary))?)),
367                Rule::ActFrmBrackets => {
368                    // Handle parentheses by recursively parsing the inner expression
369                    let inner = primary
370                        .into_inner()
371                        .next()
372                        .expect("Expected inner expression in brackets");
373                    parse_actfrm(inner.into_inner())
374                }
375                _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),
376            }
377        })
378        .map_prefix(|prefix, expr| match prefix.as_rule() {
379            Rule::ActFrmExists => Ok(ActFrm::Quantifier {
380                quantifier: Quantifier::Exists,
381                variables: Mcrl2Parser::ActFrmExists(Node::new(prefix))?,
382                body: Box::new(expr?),
383            }),
384            Rule::ActFrmForall => Ok(ActFrm::Quantifier {
385                quantifier: Quantifier::Forall,
386                variables: Mcrl2Parser::ActFrmForall(Node::new(prefix))?,
387                body: Box::new(expr?),
388            }),
389            Rule::ActFrmNegation => Ok(ActFrm::Negation(Box::new(expr?))),
390            _ => unimplemented!("Unexpected prefix operator: {:?}", prefix.as_rule()),
391        })
392        .map_infix(|lhs, op, rhs| match op.as_rule() {
393            Rule::ActFrmUnion => Ok(ActFrm::Binary {
394                op: ActFrmBinaryOp::Union,
395                lhs: Box::new(lhs?),
396                rhs: Box::new(rhs?),
397            }),
398            Rule::ActFrmIntersect => Ok(ActFrm::Binary {
399                op: ActFrmBinaryOp::Intersect,
400                lhs: Box::new(lhs?),
401                rhs: Box::new(rhs?),
402            }),
403            Rule::ActFrmImplies => Ok(ActFrm::Binary {
404                op: ActFrmBinaryOp::Implies,
405                lhs: Box::new(lhs?),
406                rhs: Box::new(rhs?),
407            }),
408            _ => unimplemented!("Unexpected binary operator: {:?}", op.as_rule()),
409        })
410        .parse(pairs)
411}
412
413/// Defines the operator precedence for regular expressions using a Pratt parser.
414pub static REGFRM_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {
415    // Precedence is defined lowest to highest
416    PrattParser::new()
417        .op(Op::infix(Rule::RegFrmAlternative, Assoc::Left)) // $left 1
418        .op(Op::infix(Rule::RegFrmComposition, Assoc::Right)) // $right 2
419        .op(Op::postfix(Rule::RegFrmIteration) | Op::postfix(Rule::RegFrmPlus)) // $left 3
420});
421
422/// Parses a sequence of `Rule` pairs into an [RegFrm] using a Pratt parser defined in [REGFRM_PRATT_PARSER] for operator precedence.
423#[allow(clippy::result_large_err)]
424pub fn parse_regfrm(pairs: Pairs<Rule>) -> ParseResult<RegFrm> {
425    REGFRM_PRATT_PARSER
426        .map_primary(|primary| match primary.as_rule() {
427            Rule::ActFrm => Ok(RegFrm::Action(Mcrl2Parser::ActFrm(Node::new(primary))?)),
428            Rule::RegFrmBackets => {
429                // Handle parentheses by recursively parsing the inner expression
430                let inner = primary
431                    .into_inner()
432                    .next()
433                    .expect("Expected inner expression in brackets");
434                parse_regfrm(inner.into_inner())
435            }
436            _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),
437        })
438        .map_infix(|lhs, op, rhs| match op.as_rule() {
439            Rule::RegFrmAlternative => Ok(RegFrm::Choice {
440                lhs: Box::new(lhs?),
441                rhs: Box::new(rhs?),
442            }),
443            Rule::RegFrmComposition => Ok(RegFrm::Sequence {
444                lhs: Box::new(lhs?),
445                rhs: Box::new(rhs?),
446            }),
447            _ => unimplemented!("Unexpected binary operator: {:?}", op.as_rule()),
448        })
449        .map_postfix(|expr, postfix| match postfix.as_rule() {
450            Rule::RegFrmIteration => Ok(RegFrm::Iteration(Box::new(expr?))),
451            Rule::RegFrmPlus => Ok(RegFrm::Plus(Box::new(expr?))),
452            _ => unimplemented!("Unexpected rule: {:?}", postfix.as_rule()),
453        })
454        .parse(pairs)
455}
456
457/// Defines the operator precedence for state formulas using a Pratt parser.
458static STATEFRM_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {
459    // Precedence is defined lowest to highest
460    PrattParser::new()
461        .op(Op::prefix(Rule::StateFrmMu) | Op::prefix(Rule::StateFrmNu)) // $right 1
462        .op(Op::prefix(Rule::StateFrmForall)
463            | Op::prefix(Rule::StateFrmExists)
464            | Op::prefix(Rule::StateFrmInf)
465            | Op::prefix(Rule::StateFrmSup)
466            | Op::prefix(Rule::StateFrmSum)) // $right 2
467        .op(Op::infix(Rule::StateFrmAddition, Assoc::Left)) // $left 3
468        .op(Op::infix(Rule::StateFrmImplication, Assoc::Right)) // $right 4
469        .op(Op::infix(Rule::StateFrmDisjunction, Assoc::Right)) // $right 5
470        .op(Op::infix(Rule::StateFrmConjunction, Assoc::Right)) // $right 6
471        .op(Op::prefix(Rule::StateFrmLeftConstantMultiply) | Op::postfix(Rule::StateFrmRightConstantMultiply)) // $right 7
472        .op(Op::prefix(Rule::StateFrmBox) | Op::prefix(Rule::StateFrmDiamond)) // $right 8
473        .op(Op::prefix(Rule::StateFrmNegation) | Op::prefix(Rule::StateFrmUnaryMinus)) // $right 9
474});
475
476#[allow(clippy::result_large_err)]
477pub fn parse_statefrm(pairs: Pairs<Rule>) -> ParseResult<StateFrm> {
478    STATEFRM_PRATT_PARSER
479        .map_primary(|primary| {
480            match primary.as_rule() {
481                Rule::StateFrmId => Mcrl2Parser::StateFrmId(Node::new(primary)),
482                Rule::StateFrmTrue => Ok(StateFrm::True),
483                Rule::StateFrmFalse => Ok(StateFrm::False),
484                Rule::StateFrmDelay => Mcrl2Parser::StateFrmDelay(Node::new(primary)),
485                Rule::StateFrmYaled => Mcrl2Parser::StateFrmYaled(Node::new(primary)),
486                Rule::StateFrmNegation => Mcrl2Parser::StateFrmNegation(Node::new(primary)),
487                Rule::StateFrmDataValExpr => Ok(StateFrm::DataValExpr(Mcrl2Parser::DataValExpr(Node::new(primary))?)),
488                Rule::StateFrmBrackets => {
489                    // Handle parentheses by recursively parsing the inner expression
490                    let inner = primary
491                        .into_inner()
492                        .next()
493                        .expect("Expected inner expression in brackets");
494                    parse_statefrm(inner.into_inner())
495                }
496                _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),
497            }
498        })
499        .map_prefix(|prefix, expr| match prefix.as_rule() {
500            Rule::StateFrmLeftConstantMultiply => Ok(StateFrm::DataValExprLeftMult(
501                Mcrl2Parser::StateFrmLeftConstantMultiply(Node::new(prefix))?,
502                Box::new(expr?),
503            )),
504            Rule::StateFrmDiamond => Ok(StateFrm::Modality {
505                operator: ModalityOperator::Diamond,
506                formula: Mcrl2Parser::StateFrmDiamond(Node::new(prefix))?,
507                expr: Box::new(expr?),
508            }),
509            Rule::StateFrmBox => Ok(StateFrm::Modality {
510                operator: ModalityOperator::Box,
511                formula: Mcrl2Parser::StateFrmBox(Node::new(prefix))?,
512                expr: Box::new(expr?),
513            }),
514            Rule::StateFrmExists => Ok(StateFrm::Quantifier {
515                quantifier: Quantifier::Exists,
516                variables: Mcrl2Parser::StateFrmExists(Node::new(prefix))?,
517                body: Box::new(expr?),
518            }),
519            Rule::StateFrmForall => Ok(StateFrm::Quantifier {
520                quantifier: Quantifier::Forall,
521                variables: Mcrl2Parser::StateFrmForall(Node::new(prefix))?,
522                body: Box::new(expr?),
523            }),
524            Rule::StateFrmMu => Ok(StateFrm::FixedPoint {
525                operator: FixedPointOperator::Least,
526                variable: Mcrl2Parser::StateFrmMu(Node::new(prefix))?,
527                body: Box::new(expr?),
528            }),
529            Rule::StateFrmNu => Ok(StateFrm::FixedPoint {
530                operator: FixedPointOperator::Greatest,
531                variable: Mcrl2Parser::StateFrmNu(Node::new(prefix))?,
532                body: Box::new(expr?),
533            }),
534            Rule::StateFrmNegation => Ok(StateFrm::Unary {
535                op: StateFrmUnaryOp::Negation,
536                expr: Box::new(expr?),
537            }),
538            Rule::StateFrmSup => Ok(StateFrm::Bound {
539                bound: Bound::Sup,
540                variables: Mcrl2Parser::StateFrmSup(Node::new(prefix))?,
541                body: Box::new(expr?),
542            }),
543            Rule::StateFrmSum => Ok(StateFrm::Bound {
544                bound: Bound::Sup,
545                variables: Mcrl2Parser::StateFrmSum(Node::new(prefix))?,
546                body: Box::new(expr?),
547            }),
548            Rule::StateFrmInf => Ok(StateFrm::Bound {
549                bound: Bound::Sup,
550                variables: Mcrl2Parser::StateFrmInf(Node::new(prefix))?,
551                body: Box::new(expr?),
552            }),
553            _ => unimplemented!("Unexpected prefix operator: {:?}", prefix.as_rule()),
554        })
555        .map_infix(|lhs, op, rhs| match op.as_rule() {
556            Rule::StateFrmAddition => Ok(StateFrm::Binary {
557                op: StateFrmOp::Addition,
558                lhs: Box::new(lhs?),
559                rhs: Box::new(rhs?),
560            }),
561            Rule::StateFrmImplication => Ok(StateFrm::Binary {
562                op: StateFrmOp::Implies,
563                lhs: Box::new(lhs?),
564                rhs: Box::new(rhs?),
565            }),
566            Rule::StateFrmDisjunction => Ok(StateFrm::Binary {
567                op: StateFrmOp::Disjunction,
568                lhs: Box::new(lhs?),
569                rhs: Box::new(rhs?),
570            }),
571            Rule::StateFrmConjunction => Ok(StateFrm::Binary {
572                op: StateFrmOp::Conjunction,
573                lhs: Box::new(lhs?),
574                rhs: Box::new(rhs?),
575            }),
576            _ => unimplemented!("Unexpected binary operator: {:?}", op.as_rule()),
577        })
578        .map_postfix(|expr, postfix| match postfix.as_rule() {
579            Rule::StateFrmRightConstantMultiply => Ok(StateFrm::DataValExprRightMult(
580                Box::new(expr?),
581                Mcrl2Parser::StateFrmRightConstantMultiply(Node::new(postfix))?,
582            )),
583            _ => unimplemented!("Unexpected binary operator: {:?}", postfix.as_rule()),
584        })
585        .parse(pairs)
586}
587
588static PBESEXPR_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {
589    // Precedence is defined lowest to highest
590    PrattParser::new()
591        .op(Op::prefix(Rule::PbesExprForall) | Op::prefix(Rule::PbesExprExists)) // $right 0
592        .op(Op::infix(Rule::PbesExprImplies, Assoc::Right)) // $right 2
593        .op(Op::infix(Rule::PbesExprDisj, Assoc::Right)) // $right 3
594        .op(Op::infix(Rule::PbesExprConj, Assoc::Right)) // $right 4
595        .op(Op::prefix(Rule::PbesExprNegation)) // $right 5
596});
597
598#[allow(clippy::result_large_err)]
599pub fn parse_pbesexpr(pairs: Pairs<Rule>) -> ParseResult<PbesExpr> {
600    PBESEXPR_PRATT_PARSER
601        .map_primary(|primary| {
602            match primary.as_rule() {
603                Rule::DataValExpr => Ok(PbesExpr::DataValExpr(Mcrl2Parser::DataValExpr(Node::new(primary))?)),
604                Rule::PbesExprParens => {
605                    // Handle parentheses by recursively parsing the inner expression
606                    let inner = primary
607                        .into_inner()
608                        .next()
609                        .expect("Expected inner expression in brackets");
610                    parse_pbesexpr(inner.into_inner())
611                }
612                Rule::PbesExprTrue => Ok(PbesExpr::True),
613                Rule::PbesExprFalse => Ok(PbesExpr::False),
614                Rule::PropVarInst => Ok(PbesExpr::PropVarInst(Mcrl2Parser::PropVarInst(Node::new(primary))?)),
615                _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),
616            }
617        })
618        .map_prefix(|op, expr| match op.as_rule() {
619            Rule::PbesExprNegation => Ok(PbesExpr::Negation(Box::new(expr?))),
620            _ => unimplemented!("Unexpected prefix operator: {:?}", op.as_rule()),
621        })
622        .map_infix(|lhs, op, rhs| match op.as_rule() {
623            Rule::PbesExprConj => Ok(PbesExpr::Binary {
624                op: PbesExprBinaryOp::Conjunction,
625                lhs: Box::new(lhs?),
626                rhs: Box::new(rhs?),
627            }),
628            Rule::PbesExprDisj => Ok(PbesExpr::Binary {
629                op: PbesExprBinaryOp::Disjunction,
630                lhs: Box::new(lhs?),
631                rhs: Box::new(rhs?),
632            }),
633            Rule::PbesExprImplies => Ok(PbesExpr::Binary {
634                op: PbesExprBinaryOp::Implies,
635                lhs: Box::new(lhs?),
636                rhs: Box::new(rhs?),
637            }),
638            _ => unimplemented!("Unexpected binary operator: {:?}", op.as_rule()),
639        })
640        .map_postfix(|expr, postfix| match postfix.as_rule() {
641            Rule::PbesExprExists => Ok(PbesExpr::Quantifier {
642                quantifier: Quantifier::Exists,
643                variables: Mcrl2Parser::PbesExprExists(Node::new(postfix))?,
644                body: Box::new(expr?),
645            }),
646            Rule::PbesExprForall => Ok(PbesExpr::Quantifier {
647                quantifier: Quantifier::Forall,
648                variables: Mcrl2Parser::PbesExprForall(Node::new(postfix))?,
649                body: Box::new(expr?),
650            }),
651            _ => unimplemented!("Unexpected postfix operator: {:?}", postfix.as_rule()),
652        })
653        .parse(pairs)
654}
655
656static PRESEXPR_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {
657    // Precedence is defined lowest to highest
658    PrattParser::new()
659        .op(Op::prefix(Rule::PresExprInf) | Op::prefix(Rule::PresExprSup) | Op::prefix(Rule::PresExprSum)) // $right 0
660        .op(Op::infix(Rule::PresExprAdd, Assoc::Right)) // $right 2
661        .op(Op::infix(Rule::PbesExprImplies, Assoc::Right)) // $right 3
662        .op(Op::infix(Rule::PbesExprDisj, Assoc::Right)) // $right 4
663        .op(Op::infix(Rule::PbesExprConj, Assoc::Right)) // $right 5
664        .op(Op::prefix(Rule::PresExprLeftConstantMultiply) | Op::postfix(Rule::PresExprRightConstMultiply)) // $right 6
665        .op(Op::prefix(Rule::PbesExprNegation)) // $right 7
666});
667
668#[allow(clippy::result_large_err)]
669pub fn parse_presexpr(pairs: Pairs<Rule>) -> ParseResult<PresExpr> {
670    PRESEXPR_PRATT_PARSER
671        .map_primary(|primary| match primary.as_rule() {
672            Rule::PresExprParens => {
673                // Handle parentheses by recursively parsing the inner expression
674                let inner = primary
675                    .into_inner()
676                    .next()
677                    .expect("Expected inner expression in brackets");
678                parse_presexpr(inner.into_inner())
679            }
680            Rule::PbesExprTrue => Ok(PresExpr::True),
681            Rule::PbesExprFalse => Ok(PresExpr::False),
682            Rule::PropVarInst => Ok(PresExpr::PropVarInst(Mcrl2Parser::PropVarInst(Node::new(primary))?)),
683            Rule::PresExprEqinf => Ok(Mcrl2Parser::PresExprEqinf(Node::new(primary))?),
684            Rule::PresExprEqninf => Ok(Mcrl2Parser::PresExprEqninf(Node::new(primary))?),
685            Rule::PresExprCondsm => Ok(Mcrl2Parser::PresExprCondsm(Node::new(primary))?),
686            Rule::PresExprCondeq => Ok(Mcrl2Parser::PresExprCondeq(Node::new(primary))?),
687            _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),
688        })
689        .map_prefix(|op, expr| match op.as_rule() {
690            Rule::PbesExprNegation => Ok(PresExpr::Negation(Box::new(expr?))),
691            Rule::PresExprInf => Ok(PresExpr::Bound {
692                op: Bound::Inf,
693                expr: Box::new(expr?),
694                variables: Mcrl2Parser::PresExprInf(Node::new(op))?,
695            }),
696            Rule::PresExprSup => Ok(PresExpr::Bound {
697                op: Bound::Sup,
698                expr: Box::new(expr?),
699                variables: Mcrl2Parser::PresExprSup(Node::new(op))?,
700            }),
701            Rule::PresExprSum => Ok(PresExpr::Bound {
702                op: Bound::Sum,
703                expr: Box::new(expr?),
704                variables: Mcrl2Parser::PresExprSum(Node::new(op))?,
705            }),
706            Rule::PresExprLeftConstantMultiply => Ok(PresExpr::LeftConstantMultiply {
707                constant: Mcrl2Parser::PresExprLeftConstantMultiply(Node::new(op))?,
708                expr: Box::new(expr?),
709            }),
710            _ => unimplemented!("Unexpected prefix operator: {:?}", op.as_rule()),
711        })
712        .map_infix(|lhs, op, rhs| match op.as_rule() {
713            Rule::PbesExprImplies => Ok(PresExpr::Binary {
714                op: PresExprBinaryOp::Implies,
715                lhs: Box::new(lhs?),
716                rhs: Box::new(rhs?),
717            }),
718            Rule::PbesExprDisj => Ok(PresExpr::Binary {
719                op: PresExprBinaryOp::Disjunction,
720                lhs: Box::new(lhs?),
721                rhs: Box::new(rhs?),
722            }),
723            Rule::PbesExprConj => Ok(PresExpr::Binary {
724                op: PresExprBinaryOp::Conjunction,
725                lhs: Box::new(lhs?),
726                rhs: Box::new(rhs?),
727            }),
728            Rule::PresExprAdd => Ok(PresExpr::Binary {
729                op: PresExprBinaryOp::Add,
730                lhs: Box::new(lhs?),
731                rhs: Box::new(rhs?),
732            }),
733            _ => unimplemented!("Unexpected binary operator: {:?}", op.as_rule()),
734        })
735        .map_postfix(|expr, postfix| match postfix.as_rule() {
736            Rule::PresExprRightConstMultiply => Ok(PresExpr::RightConstantMultiply {
737                expr: Box::new(expr?),
738                constant: Mcrl2Parser::PresExprRightConstMultiply(Node::new(postfix))?,
739            }),
740            _ => unimplemented!("Unexpected postfix operator: {:?}", postfix.as_rule()),
741        })
742        .parse(pairs)
743}
merc_syntax/precedence.rs

merc_syntax/
precedence.rs
