Grcov report - precedence.rs

1

use std::sync::LazyLock;

2

3

use pest::iterators::Pair;

4

use pest::iterators::Pairs;

5

use pest::pratt_parser::Assoc;

6

use pest::pratt_parser::Op;

7

use pest::pratt_parser::PrattParser;

8

9

use merc_pest_consume::Node;

10

11

use crate::ActFrm;

12

use crate::ActFrmBinaryOp;

13

use crate::Bound;

14

use crate::DataExpr;

15

use crate::DataExprBinaryOp;

16

use crate::DataExprUnaryOp;

17

use crate::FixedPointOperator;

18

use crate::Mcrl2Parser;

19

use crate::ModalityOperator;

20

use crate::ParseResult;

21

use crate::PbesExpr;

22

use crate::PbesExprBinaryOp;

23

use crate::PresExpr;

24

use crate::PresExprBinaryOp;

25

use crate::ProcExprBinaryOp;

26

use crate::ProcessExpr;

27

use crate::Quantifier;

28

use crate::RegFrm;

29

use crate::Rule;

30

use crate::Sort;

31

use crate::StateFrm;

32

use crate::StateFrmOp;

33

use crate::StateFrmUnaryOp;

34

use crate::syntax_tree::SortExpression;

35

36

3800

pub static SORT_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {

37

    // Precedence is defined lowest to highest

38

3800

    PrattParser::new()

39

        // Sort operators

40

3800

        .op(Op::infix(Rule::SortExprFunction, Assoc::Left)) // $right 0

41

3800

        .op(Op::infix(Rule::SortExprProduct, Assoc::Right)) // $left 1

42

3800

});

43

44

#[allow(clippy::result_large_err)]

45

645970

pub fn parse_sortexpr_primary(primary: Pair<'_, Rule>) -> ParseResult<SortExpression> {

46

645970

    match primary.as_rule() {

47

411390

        Rule::IdAt => Ok(SortExpression::Reference(Mcrl2Parser::IdAt(Node::new(primary))?)),

48

21000

        Rule::SortExpr => Mcrl2Parser::SortExpr(Node::new(primary)),

49

50

28230

        Rule::SortExprBool => Ok(SortExpression::Simple(Sort::Bool)),

51

3410

        Rule::SortExprInt => Ok(SortExpression::Simple(Sort::Int)),

52

14620

        Rule::SortExprPos => Ok(SortExpression::Simple(Sort::Pos)),

53

47060

        Rule::SortExprNat => Ok(SortExpression::Simple(Sort::Nat)),

54

1640

        Rule::SortExprReal => Ok(SortExpression::Simple(Sort::Real)),

55

56

12990

        Rule::SortExprList => Mcrl2Parser::SortExprList(Node::new(primary)),

57

5670

        Rule::SortExprSet => Mcrl2Parser::SortExprSet(Node::new(primary)),

58

1150

        Rule::SortExprBag => Mcrl2Parser::SortExprBag(Node::new(primary)),

59

730

        Rule::SortExprFSet => Mcrl2Parser::SortExprFSet(Node::new(primary)),

60

450

        Rule::SortExprFBag => Mcrl2Parser::SortExprFBag(Node::new(primary)),

61

62

        Rule::SortExprParens => {

63

            // Handle parentheses by recursively parsing the inner expression

64

83870

            let inner = primary

65

83870

                .into_inner()

66

83870

                .next()

67

83870

                .expect("Expected inner expression in brackets");

68

83870

            parse_sortexpr(inner.into_inner())

69

70

71

13760

        Rule::SortExprStruct => Mcrl2Parser::SortExprStruct(Node::new(primary)),

72

        _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),

73

74

645970

75

76

/// Parses a sequence of `Rule` pairs into a `SortExpression` using a Pratt parser for operator precedence.

77

#[allow(clippy::result_large_err)]

78

434050

pub fn parse_sortexpr(pairs: Pairs<Rule>) -> ParseResult<SortExpression> {

79

434050

    SORT_PRATT_PARSER

80

603220

        .map_primary(|primary| parse_sortexpr_primary(primary))

81

434050

        .map_infix(|lhs, op, rhs| match op.as_rule() {

82

            Rule::SortExprFunction => Ok(SortExpression::Function {

83

70780

                domain: Box::new(lhs?),

84

70780

                range: Box::new(rhs?),

85

}),

86

            Rule::SortExprProduct => Ok(SortExpression::Product {

87

98390

                lhs: Box::new(lhs?),

88

98390

                rhs: Box::new(rhs?),

89

}),

90

            _ => unimplemented!("Unexpected binary operator: {:?}", op.as_rule()),

91

169170

})

92

434050

        .parse(pairs)

93

434050

94

95

3900

pub static DATAEXPR_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {

96

    // Precedence is defined lowest to highest

97

3900

    PrattParser::new()

98

3900

        .op(Op::postfix(Rule::DataExprWhr)) // $left 0

99

3900

        .op(Op::prefix(Rule::DataExprForall) | Op::prefix(Rule::DataExprExists) | Op::prefix(Rule::DataExprLambda)) // $right 1

100

3900

        .op(Op::infix(Rule::DataExprImpl, Assoc::Right)) // $right 2

101

3900

        .op(Op::infix(Rule::DataExprDisj, Assoc::Right)) // $right 3

102

3900

        .op(Op::infix(Rule::DataExprConj, Assoc::Right)) // $right 4

103

3900

        .op(Op::infix(Rule::DataExprEq, Assoc::Left) | Op::infix(Rule::DataExprNeq, Assoc::Left)) // $left 5

104

3900

        .op(Op::infix(Rule::DataExprLess, Assoc::Left)

105

3900

            | Op::infix(Rule::DataExprLeq, Assoc::Left)

106

3900

            | Op::infix(Rule::DataExprGeq, Assoc::Left)

107

3900

            | Op::infix(Rule::DataExprGreater, Assoc::Left)

108

3900

            | Op::infix(Rule::DataExprIn, Assoc::Left)) // $left 6

109

3900

        .op(Op::infix(Rule::DataExprCons, Assoc::Right)) // $right 7

110

3900

        .op(Op::infix(Rule::DataExprSnoc, Assoc::Left)) // $left 8

111

3900

        .op(Op::infix(Rule::DataExprConcat, Assoc::Left)) // $left 9

112

3900

        .op(Op::infix(Rule::DataExprAdd, Assoc::Left) | Op::infix(Rule::DataExprSubtract, Assoc::Left)) // $left 10

113

3900

        .op(Op::infix(Rule::DataExprDiv, Assoc::Left)

114

3900

            | Op::infix(Rule::DataExprIntDiv, Assoc::Left)

115

3900

            | Op::infix(Rule::DataExprMod, Assoc::Left)) // $left 11

116

3900

        .op(Op::infix(Rule::DataExprMult, Assoc::Left)

117

3900

            | Op::infix(Rule::DataExprAt, Assoc::Left) // $left 12

118

3900

            | Op::prefix(Rule::DataExprMinus)

119

3900

            | Op::prefix(Rule::DataExprNegation)

120

3900

            | Op::prefix(Rule::DataExprSize)) // $right 12

121

3900

        .op(Op::postfix(Rule::DataExprUpdate) | Op::postfix(Rule::DataExprApplication)) // ) // $left 13

122

3900

});

123

124

#[allow(clippy::result_large_err)]

125

2892760

pub fn parse_dataexpr(pairs: Pairs<Rule>) -> ParseResult<DataExpr> {

126

2892760

    DATAEXPR_PRATT_PARSER

127

3127530

        .map_primary(|primary| match primary.as_rule() {

128

21050

            Rule::DataExprTrue => Ok(DataExpr::Bool(true)),

129

20860

            Rule::DataExprFalse => Ok(DataExpr::Bool(false)),

130

11230

            Rule::DataExprEmptyList => Ok(DataExpr::EmptyList),

131

3780

            Rule::DataExprEmptySet => Ok(DataExpr::EmptySet),

132

1180

            Rule::DataExprEmptyBag => Ok(DataExpr::EmptyBag),

133

9500

            Rule::DataExprListEnum => Mcrl2Parser::DataExprListEnum(Node::new(primary)),

134

920

            Rule::DataExprBagEnum => Mcrl2Parser::DataExprBagEnum(Node::new(primary)),

135

220

            Rule::DataExprSetBagComp => Mcrl2Parser::DataExprSetBagComp(Node::new(primary)),

136

6960

            Rule::DataExprSetEnum => Mcrl2Parser::DataExprSetEnum(Node::new(primary)),

137

144560

            Rule::Number => Mcrl2Parser::Number(Node::new(primary)),

138

2731210

            Rule::IdAt => Ok(DataExpr::Id(Mcrl2Parser::IdAt(Node::new(primary))?)),

139

140

            Rule::DataExprBrackets => {

141

                // Handle parentheses by recursively parsing the inner expression

142

176060

                let inner = primary

143

176060

                    .into_inner()

144

176060

                    .next()

145

176060

                    .expect("Expected inner expression in brackets");

146

176060

                parse_dataexpr(inner.into_inner())

147

148

149

            _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),

150

3127530

})

151

2892760

        .map_infix(|lhs, op, rhs| {

152

234770

            let op = match op.as_rule() {

153

30740

                Rule::DataExprConj => DataExprBinaryOp::Conj,

154

9590

                Rule::DataExprDisj => DataExprBinaryOp::Disj,

155

49960

                Rule::DataExprEq => DataExprBinaryOp::Equal,

156

11750

                Rule::DataExprNeq => DataExprBinaryOp::NotEqual,

157

12940

                Rule::DataExprLess => DataExprBinaryOp::LessThan,

158

8880

                Rule::DataExprLeq => DataExprBinaryOp::LessEqual,

159

6890

                Rule::DataExprGreater => DataExprBinaryOp::GreaterThan,

160

3180

                Rule::DataExprGeq => DataExprBinaryOp::GreaterEqual,

161

9780

                Rule::DataExprIn => DataExprBinaryOp::In,

162

15940

                Rule::DataExprCons => DataExprBinaryOp::Cons,

163

250

                Rule::DataExprSnoc => DataExprBinaryOp::Snoc,

164

900

                Rule::DataExprConcat => DataExprBinaryOp::Concat,

165

30570

                Rule::DataExprAdd => DataExprBinaryOp::Add,

166

14270

                Rule::DataExprSubtract => DataExprBinaryOp::Subtract,

167

1640

                Rule::DataExprDiv => DataExprBinaryOp::Div,

168

340

                Rule::DataExprIntDiv => DataExprBinaryOp::IntDiv,

169

1830

                Rule::DataExprMod => DataExprBinaryOp::Mod,

170

5250

                Rule::DataExprMult => DataExprBinaryOp::Multiply,

171

18910

                Rule::DataExprAt => DataExprBinaryOp::At,

172

1160

                Rule::DataExprImpl => DataExprBinaryOp::Implies,

173

                _ => unimplemented!("Unexpected binary operator rule: {:?}", op.as_rule()),

174

};

175

176

            Ok(DataExpr::Binary {

177

234770

op,

178

234770

                lhs: Box::new(lhs?),

179

234770

                rhs: Box::new(rhs?),

180

})

181

234770

})

182

2892760

        .map_postfix(|expr, postfix| match postfix.as_rule() {

183

            Rule::DataExprUpdate => Ok(DataExpr::FunctionUpdate {

184

5720

                expr: Box::new(expr?),

185

5720

                update: Box::new(Mcrl2Parser::DataExprUpdate(Node::new(postfix))?),

186

}),

187

            Rule::DataExprApplication => Ok(DataExpr::Application {

188

793640

                function: Box::new(expr?),

189

793640

                arguments: Mcrl2Parser::DataExprApplication(Node::new(postfix))?,

190

}),

191

            Rule::DataExprWhr => Ok(DataExpr::Whr {

192

480

                expr: Box::new(expr?),

193

480

                assignments: Mcrl2Parser::DataExprWhr(Node::new(postfix))?,

194

}),

195

            _ => unimplemented!("Unexpected postfix operator: {:?}", postfix.as_rule()),

196

799840

})

197

2892760

        .map_prefix(|prefix, expr| match prefix.as_rule() {

198

            Rule::DataExprForall => Ok(DataExpr::Quantifier {

199

520

                op: Quantifier::Forall,

200

520

                variables: Mcrl2Parser::DataExprForall(Node::new(prefix))?,

201

520

                body: Box::new(expr?),

202

}),

203

            Rule::DataExprExists => Ok(DataExpr::Quantifier {

204

760

                op: Quantifier::Exists,

205

760

                variables: Mcrl2Parser::DataExprExists(Node::new(prefix))?,

206

760

                body: Box::new(expr?),

207

}),

208

            Rule::DataExprLambda => Ok(DataExpr::Lambda {

209

580

                variables: Mcrl2Parser::DataExprLambda(Node::new(prefix))?,

210

580

                body: Box::new(expr?),

211

}),

212

            Rule::DataExprNegation => Ok(DataExpr::Unary {

213

8700

                op: DataExprUnaryOp::Negation,

214

8700

                expr: Box::new(expr?),

215

}),

216

            Rule::DataExprMinus => Ok(DataExpr::Unary {

217

1000

                op: DataExprUnaryOp::Minus,

218

1000

                expr: Box::new(expr?),

219

}),

220

            Rule::DataExprSize => Ok(DataExpr::Unary {

221

1260

                op: DataExprUnaryOp::Size,

222

1260

                expr: Box::new(expr?),

223

}),

224

            _ => unimplemented!("Unexpected prefix operator: {:?}", prefix.as_rule()),

225

12820

})

226

2892760

        .parse(pairs)

227

2892760

228

229

1730

pub static PROCEXPR_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {

230

    // Precedence is defined lowest to highest

231

1730

    PrattParser::new()

232

1730

        .op(Op::infix(Rule::ProcExprChoice, Assoc::Left)) // $left 1

233

1730

        .op(Op::prefix(Rule::ProcExprSum) | Op::prefix(Rule::ProcExprDist)) // $right 2

234

1730

        .op(Op::infix(Rule::ProcExprParallel, Assoc::Right)) // $right 3

235

1730

        .op(Op::infix(Rule::ProcExprLeftMerge, Assoc::Right)) // $right 4

236

1730

        .op(Op::prefix(Rule::ProcExprIf)) // $right 5

237

1730

        .op(Op::prefix(Rule::ProcExprIfThen)) // $right 5

238

1730

        .op(Op::infix(Rule::ProcExprUntil, Assoc::Left)) // $left 6

239

1730

        .op(Op::infix(Rule::ProcExprSeq, Assoc::Right)) // $right 7

240

1730

        .op(Op::postfix(Rule::ProcExprAt)) // $left 8

241

1730

        .op(Op::infix(Rule::ProcExprSync, Assoc::Left)) // $left 9

242

1730

});

243

244

#[allow(clippy::result_large_err)]

245

199070

pub fn parse_process_expr(pairs: Pairs<Rule>) -> ParseResult<ProcessExpr> {

246

199070

    PROCEXPR_PRATT_PARSER

247

314140

        .map_primary(|primary| match primary.as_rule() {

248

20400

            Rule::ProcExprId => Ok(Mcrl2Parser::ProcExprId(Node::new(primary))?),

249

2560

            Rule::ProcExprDelta => Ok(ProcessExpr::Delta),

250

870

            Rule::ProcExprTau => Ok(ProcessExpr::Tau),

251

650

            Rule::ProcExprBlock => Ok(Mcrl2Parser::ProcExprBlock(Node::new(primary))?),

252

2420

            Rule::ProcExprAllow => Ok(Mcrl2Parser::ProcExprAllow(Node::new(primary))?),

253

1500

            Rule::ProcExprHide => Ok(Mcrl2Parser::ProcExprHide(Node::new(primary))?),

254

680

            Rule::ProcExprRename => Ok(Mcrl2Parser::ProcExprRename(Node::new(primary))?),

255

2650

            Rule::ProcExprComm => Ok(Mcrl2Parser::ProcExprComm(Node::new(primary))?),

256

            Rule::Action => {

257

131530

                let action = Mcrl2Parser::Action(Node::new(primary))?;

258

259

131530

                Ok(ProcessExpr::Action(action.id, action.args))

260

261

            Rule::ProcExprBrackets => {

262

                // Handle parentheses by recursively parsing the inner expression

263

150880

                let inner = primary

264

150880

                    .into_inner()

265

150880

                    .next()

266

150880

                    .expect("Expected inner expression in brackets");

267

150880

                parse_process_expr(inner.into_inner())

268

269

            _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),

270

314140

})

271

199070

        .map_infix(|lhs, op, rhs| match op.as_rule() {

272

            Rule::ProcExprChoice => Ok(ProcessExpr::Binary {

273

29810

                op: ProcExprBinaryOp::Choice,

274

29810

                lhs: Box::new(lhs?),

275

29810

                rhs: Box::new(rhs?),

276

}),

277

            Rule::ProcExprParallel => Ok(ProcessExpr::Binary {

278

12740

                op: ProcExprBinaryOp::Parallel,

279

12740

                lhs: Box::new(lhs?),

280

12740

                rhs: Box::new(rhs?),

281

}),

282

            Rule::ProcExprLeftMerge => Ok(ProcessExpr::Binary {

283

20

                op: ProcExprBinaryOp::LeftMerge,

284

20

                lhs: Box::new(lhs?),

285

20

                rhs: Box::new(rhs?),

286

}),

287

            Rule::ProcExprSeq => Ok(ProcessExpr::Binary {

288

64350

                op: ProcExprBinaryOp::Sequence,

289

64350

                lhs: Box::new(lhs?),

290

64350

                rhs: Box::new(rhs?),

291

}),

292

            Rule::ProcExprSync => Ok(ProcessExpr::Binary {

293

8140

                op: ProcExprBinaryOp::CommMerge,

294

8140

                lhs: Box::new(lhs?),

295

8140

                rhs: Box::new(rhs?),

296

}),

297

            Rule::ProcExprUntil => Ok(ProcessExpr::Binary {

298

10

                op: ProcExprBinaryOp::Until,

299

10

                lhs: Box::new(lhs?),

300

10

                rhs: Box::new(rhs?),

301

}),

302

            _ => unimplemented!("Unexpected rule: {:?}", op.as_rule()),

303

115070

})

304

199070

        .map_prefix(|prefix, expr| match prefix.as_rule() {

305

            Rule::ProcExprSum => Ok(ProcessExpr::Sum {

306

20350

                variables: Mcrl2Parser::ProcExprSum(Node::new(prefix))?,

307

20350

                operand: Box::new(expr?),

308

}),

309

            Rule::ProcExprDist => {

310

520

                let (variables, data_expr) = Mcrl2Parser::ProcExprDist(Node::new(prefix))?;

311

312

                Ok(ProcessExpr::Dist {

313

520

                    variables,

314

520

                    expr: data_expr,

315

520

                    operand: Box::new(expr?),

316

})

317

318

            Rule::ProcExprIf => {

319

27280

                let condition = Mcrl2Parser::ProcExprIf(Node::new(prefix))?;

320

321

                Ok(ProcessExpr::Condition {

322

27280

                    condition,

323

27280

                    then: Box::new(expr?),

324

27280

                    else_: None,

325

})

326

327

            Rule::ProcExprIfThen => {

328

12780

                let (condition, then) = Mcrl2Parser::ProcExprIfThen(Node::new(prefix))?;

329

330

                Ok(ProcessExpr::Condition {

331

12780

                    condition,

332

12780

                    then: Box::new(then),

333

12780

                    else_: Some(Box::new(expr?)),

334

})

335

336

            _ => unimplemented!("Unexpected rule: {:?}", prefix.as_rule()),

337

60930

})

338

199070

        .map_postfix(|expr, postfix| match postfix.as_rule() {

339

            Rule::ProcExprAt => Ok(ProcessExpr::At {

340

280

                expr: Box::new(expr?),

341

280

                operand: Mcrl2Parser::ProcExprAt(Node::new(postfix))?,

342

}),

343

            _ => unimplemented!("Unexpected postfix rule: {:?}", postfix.as_rule()),

344

280

})

345

199070

        .parse(pairs)

346

199070

347

348

/// Defines the operator precedence for action formulas using a Pratt parser.

349

1501

pub static ACTFRM_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {

350

    // Precedence is defined lowest to highest

351

1501

    PrattParser::new()

352

1501

        .op(Op::prefix(Rule::ActFrmExists) | Op::prefix(Rule::ActFrmForall)) // $right  0

353

1501

        .op(Op::infix(Rule::ActFrmImplies, Assoc::Right)) //  $right 2

354

1501

        .op(Op::infix(Rule::ActFrmUnion, Assoc::Right)) // $right 3

355

1501

        .op(Op::infix(Rule::ActFrmIntersect, Assoc::Right)) // $right 4

356

1501

        .op(Op::postfix(Rule::ActFrmAt)) //  $left 5

357

1501

        .op(Op::prefix(Rule::ActFrmNegation)) // $right 6

358

1501

});

359

360

/// Parses a sequence of `Rule` pairs into an `ActFrm` using a Pratt parser defined in [ACTFRM_PRATT_PARSER] for operator precedence.

361

#[allow(clippy::result_large_err)]

362

23871

pub fn parse_actfrm(pairs: Pairs<Rule>) -> ParseResult<ActFrm> {

363

23871

    ACTFRM_PRATT_PARSER

364

26411

        .map_primary(|primary| {

365

26411

            match primary.as_rule() {

366

2450

                Rule::ActFrmTrue => Ok(ActFrm::True),

367

10

                Rule::ActFrmFalse => Ok(ActFrm::False),

368

16831

                Rule::MultAct => Ok(ActFrm::MultAct(Mcrl2Parser::MultAct(Node::new(primary))?)),

369

420

                Rule::DataValExpr => Ok(ActFrm::DataExprVal(Mcrl2Parser::DataValExpr(Node::new(primary))?)),

370

                Rule::ActFrmBrackets => {

371

                    // Handle parentheses by recursively parsing the inner expression

372

6700

                    let inner = primary

373

6700

                        .into_inner()

374

6700

                        .next()

375

6700

                        .expect("Expected inner expression in brackets");

376

6700

                    parse_actfrm(inner.into_inner())

377

378

                _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),

379

380

26411

})

381

23871

        .map_prefix(|prefix, expr| match prefix.as_rule() {

382

            Rule::ActFrmExists => Ok(ActFrm::Quantifier {

383

2600

                quantifier: Quantifier::Exists,

384

2600

                variables: Mcrl2Parser::ActFrmExists(Node::new(prefix))?,

385

2600

                body: Box::new(expr?),

386

}),

387

            Rule::ActFrmForall => Ok(ActFrm::Quantifier {

388

80

                quantifier: Quantifier::Forall,

389

80

                variables: Mcrl2Parser::ActFrmForall(Node::new(prefix))?,

390

80

                body: Box::new(expr?),

391

}),

392

3110

            Rule::ActFrmNegation => Ok(ActFrm::Negation(Box::new(expr?))),

393

            _ => unimplemented!("Unexpected prefix operator: {:?}", prefix.as_rule()),

394

5790

})

395

23871

        .map_infix(|lhs, op, rhs| match op.as_rule() {

396

            Rule::ActFrmUnion => Ok(ActFrm::Binary {

397

1500

                op: ActFrmBinaryOp::Union,

398

1500

                lhs: Box::new(lhs?),

399

1500

                rhs: Box::new(rhs?),

400

}),

401

            Rule::ActFrmIntersect => Ok(ActFrm::Binary {

402

1000

                op: ActFrmBinaryOp::Intersect,

403

1000

                lhs: Box::new(lhs?),

404

1000

                rhs: Box::new(rhs?),

405

}),

406

            Rule::ActFrmImplies => Ok(ActFrm::Binary {

407

40

                op: ActFrmBinaryOp::Implies,

408

40

                lhs: Box::new(lhs?),

409

40

                rhs: Box::new(rhs?),

410

}),

411

            _ => unimplemented!("Unexpected binary operator: {:?}", op.as_rule()),

412

2540

})

413

23871

        .parse(pairs)

414

23871

415

416

/// Defines the operator precedence for regular expressions using a Pratt parser.

417

1501

pub static REGFRM_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {

418

    // Precedence is defined lowest to highest

419

1501

    PrattParser::new()

420

1501

        .op(Op::infix(Rule::RegFrmAlternative, Assoc::Left)) // $left 1

421

1501

        .op(Op::infix(Rule::RegFrmComposition, Assoc::Right)) // $right 2

422

1501

        .op(Op::postfix(Rule::RegFrmIteration) | Op::postfix(Rule::RegFrmPlus)) // $left 3

423

1501

});

424

425

/// Parses a sequence of `Rule` pairs into an [RegFrm] using a Pratt parser defined in [REGFRM_PRATT_PARSER] for operator precedence.

426

#[allow(clippy::result_large_err)]

427

16051

pub fn parse_regfrm(pairs: Pairs<Rule>) -> ParseResult<RegFrm> {

428

16051

    REGFRM_PRATT_PARSER

429

18321

        .map_primary(|primary| match primary.as_rule() {

430

17171

            Rule::ActFrm => Ok(RegFrm::Action(Mcrl2Parser::ActFrm(Node::new(primary))?)),

431

            Rule::RegFrmBackets => {

432

                // Handle parentheses by recursively parsing the inner expression

433

1150

                let inner = primary

434

1150

                    .into_inner()

435

1150

                    .next()

436

1150

                    .expect("Expected inner expression in brackets");

437

1150

                parse_regfrm(inner.into_inner())

438

439

            _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),

440

18321

})

441

16051

        .map_infix(|lhs, op, rhs| match op.as_rule() {

442

            Rule::RegFrmAlternative => Ok(RegFrm::Choice {

443

90

                lhs: Box::new(lhs?),

444

90

                rhs: Box::new(rhs?),

445

}),

446

            Rule::RegFrmComposition => Ok(RegFrm::Sequence {

447

2180

                lhs: Box::new(lhs?),

448

2180

                rhs: Box::new(rhs?),

449

}),

450

            _ => unimplemented!("Unexpected binary operator: {:?}", op.as_rule()),

451

2270

})

452

16051

        .map_postfix(|expr, postfix| match postfix.as_rule() {

453

2680

            Rule::RegFrmIteration => Ok(RegFrm::Iteration(Box::new(expr?))),

454

10

            Rule::RegFrmPlus => Ok(RegFrm::Plus(Box::new(expr?))),

455

            _ => unimplemented!("Unexpected rule: {:?}", postfix.as_rule()),

456

2690

})

457

16051

        .parse(pairs)

458

16051

459

460

/// Defines the operator precedence for state formulas using a Pratt parser.

461

1531

static STATEFRM_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {

462

    // Precedence is defined lowest to highest

463

1531

    PrattParser::new()

464

1531

        .op(Op::prefix(Rule::StateFrmMu) | Op::prefix(Rule::StateFrmNu)) // $right 1

465

1531

        .op(Op::prefix(Rule::StateFrmForall)

466

1531

            | Op::prefix(Rule::StateFrmExists)

467

1531

            | Op::prefix(Rule::StateFrmInf)

468

1531

            | Op::prefix(Rule::StateFrmSup)

469

1531

            | Op::prefix(Rule::StateFrmSum)) // $right 2

470

1531

        .op(Op::infix(Rule::StateFrmAddition, Assoc::Left)) // $left 3

471

1531

        .op(Op::infix(Rule::StateFrmImplication, Assoc::Right)) // $right 4

472

1531

        .op(Op::infix(Rule::StateFrmDisjunction, Assoc::Right)) // $right 5

473

1531

        .op(Op::infix(Rule::StateFrmConjunction, Assoc::Right)) // $right 6

474

1531

        .op(Op::prefix(Rule::StateFrmLeftConstantMultiply) | Op::postfix(Rule::StateFrmRightConstantMultiply)) // $right 7

475

1531

        .op(Op::prefix(Rule::StateFrmBox) | Op::prefix(Rule::StateFrmDiamond)) // $right 8

476

1531

        .op(Op::prefix(Rule::StateFrmNegation) | Op::prefix(Rule::StateFrmUnaryMinus)) // $right 9

477

1531

});

478

479

#[allow(clippy::result_large_err)]

480

27751

pub fn parse_statefrm(pairs: Pairs<Rule>) -> ParseResult<StateFrm> {

481

27751

    STATEFRM_PRATT_PARSER

482

48623

        .map_primary(|primary| {

483

48623

            match primary.as_rule() {

484

21183

                Rule::StateFrmId => Mcrl2Parser::StateFrmId(Node::new(primary)),

485

1940

                Rule::StateFrmTrue => Ok(StateFrm::True),

486

720

                Rule::StateFrmFalse => Ok(StateFrm::False),

487

20

                Rule::StateFrmDelay => Mcrl2Parser::StateFrmDelay(Node::new(primary)),

488

10

                Rule::StateFrmYaled => Mcrl2Parser::StateFrmYaled(Node::new(primary)),

489

                Rule::StateFrmNegation => Mcrl2Parser::StateFrmNegation(Node::new(primary)),

490

                Rule::StateFrmDataValExpr => Ok(StateFrm::DataValExpr(Mcrl2Parser::DataValExpr(Node::new(primary))?)),

491

                Rule::StateFrmBrackets => {

492

                    // Handle parentheses by recursively parsing the inner expression

493

24750

                    let inner = primary

494

24750

                        .into_inner()

495

24750

                        .next()

496

24750

                        .expect("Expected inner expression in brackets");

497

24750

                    parse_statefrm(inner.into_inner())

498

499

                _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),

500

501

48623

})

502

27753

        .map_prefix(|prefix, expr| match prefix.as_rule() {

503

            Rule::StateFrmLeftConstantMultiply => Ok(StateFrm::DataValExprLeftMult(

504

40

                Mcrl2Parser::StateFrmLeftConstantMultiply(Node::new(prefix))?,

505

40

                Box::new(expr?),

506

)),

507

            Rule::StateFrmDiamond => Ok(StateFrm::Modality {

508

5770

                operator: ModalityOperator::Diamond,

509

5770

                formula: Mcrl2Parser::StateFrmDiamond(Node::new(prefix))?,

510

5770

                expr: Box::new(expr?),

511

}),

512

            Rule::StateFrmBox => Ok(StateFrm::Modality {

513

9131

                operator: ModalityOperator::Box,

514

9131

                formula: Mcrl2Parser::StateFrmBox(Node::new(prefix))?,

515

9131

                expr: Box::new(expr?),

516

}),

517

            Rule::StateFrmExists => Ok(StateFrm::Quantifier {

518

1810

                quantifier: Quantifier::Exists,

519

1810

                variables: Mcrl2Parser::StateFrmExists(Node::new(prefix))?,

520

1810

                body: Box::new(expr?),

521

}),

522

            Rule::StateFrmForall => Ok(StateFrm::Quantifier {

523

3480

                quantifier: Quantifier::Forall,

524

3480

                variables: Mcrl2Parser::StateFrmForall(Node::new(prefix))?,

525

3480

                body: Box::new(expr?),

526

}),

527

            Rule::StateFrmMu => Ok(StateFrm::FixedPoint {

528

1802

                operator: FixedPointOperator::Least,

529

1802

                variable: Mcrl2Parser::StateFrmMu(Node::new(prefix))?,

530

1802

                body: Box::new(expr?),

531

}),

532

            Rule::StateFrmNu => Ok(StateFrm::FixedPoint {

533

2180

                operator: FixedPointOperator::Greatest,

534

2180

                variable: Mcrl2Parser::StateFrmNu(Node::new(prefix))?,

535

2180

                body: Box::new(expr?),

536

}),

537

            Rule::StateFrmNegation => Ok(StateFrm::Unary {

538

290

                op: StateFrmUnaryOp::Negation,

539

290

                expr: Box::new(expr?),

540

}),

541

            Rule::StateFrmSup => Ok(StateFrm::Bound {

542

10

                bound: Bound::Sup,

543

10

                variables: Mcrl2Parser::StateFrmSup(Node::new(prefix))?,

544

10

                body: Box::new(expr?),

545

}),

546

            Rule::StateFrmSum => Ok(StateFrm::Bound {

547

10

                bound: Bound::Sum,

548

10

                variables: Mcrl2Parser::StateFrmSum(Node::new(prefix))?,

549

10

                body: Box::new(expr?),

550

}),

551

            Rule::StateFrmInf => Ok(StateFrm::Bound {

552

30

                bound: Bound::Inf,

553

30

                variables: Mcrl2Parser::StateFrmInf(Node::new(prefix))?,

554

30

                body: Box::new(expr?),

555

}),

556

            _ => unimplemented!("Unexpected prefix operator: {:?}", prefix.as_rule()),

557

24553

})

558

27752

        .map_infix(|lhs, op, rhs| match op.as_rule() {

559

            Rule::StateFrmAddition => Ok(StateFrm::Binary {

560

20

                op: StateFrmOp::Addition,

561

20

                lhs: Box::new(lhs?),

562

20

                rhs: Box::new(rhs?),

563

}),

564

            Rule::StateFrmImplication => Ok(StateFrm::Binary {

565

5140

                op: StateFrmOp::Implies,

566

5140

                lhs: Box::new(lhs?),

567

5140

                rhs: Box::new(rhs?),

568

}),

569

            Rule::StateFrmDisjunction => Ok(StateFrm::Binary {

570

3910

                op: StateFrmOp::Disjunction,

571

3910

                lhs: Box::new(lhs?),

572

3910

                rhs: Box::new(rhs?),

573

}),

574

            Rule::StateFrmConjunction => Ok(StateFrm::Binary {

575

11802

                op: StateFrmOp::Conjunction,

576

11802

                lhs: Box::new(lhs?),

577

11802

                rhs: Box::new(rhs?),

578

}),

579

            _ => unimplemented!("Unexpected binary operator: {:?}", op.as_rule()),

580

20872

})

581

27751

        .map_postfix(|expr, postfix| match postfix.as_rule() {

582

            Rule::StateFrmRightConstantMultiply => Ok(StateFrm::DataValExprRightMult(

583

                Box::new(expr?),

584

                Mcrl2Parser::StateFrmRightConstantMultiply(Node::new(postfix))?,

585

)),

586

            _ => unimplemented!("Unexpected binary operator: {:?}", postfix.as_rule()),

587

})

588

27751

        .parse(pairs)

589

27751

590

591

50

static PBESEXPR_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {

592

    // Precedence is defined lowest to highest

593

50

    PrattParser::new()

594

50

        .op(Op::prefix(Rule::PbesExprForall) | Op::prefix(Rule::PbesExprExists)) // $right 0

595

50

        .op(Op::infix(Rule::PbesExprImplies, Assoc::Right)) // $right 2

596

50

        .op(Op::infix(Rule::PbesExprDisj, Assoc::Right)) // $right 3

597

50

        .op(Op::infix(Rule::PbesExprConj, Assoc::Right)) // $right 4

598

50

        .op(Op::prefix(Rule::PbesExprNegation)) // $right 5

599

50

});

600

601

#[allow(clippy::result_large_err)]

602

43400

pub fn parse_pbesexpr(pairs: Pairs<Rule>) -> ParseResult<PbesExpr> {

603

43400

    PBESEXPR_PRATT_PARSER

604

67570

        .map_primary(|primary| {

605

67570

            match primary.as_rule() {

606

14840

                Rule::DataValExpr => Ok(PbesExpr::DataValExpr(Mcrl2Parser::DataValExpr(Node::new(primary))?)),

607

                Rule::PbesExprParens => {

608

                    // Handle parentheses by recursively parsing the inner expression

609

40290

                    let inner = primary

610

40290

                        .into_inner()

611

40290

                        .next()

612

40290

                        .expect("Expected inner expression in brackets");

613

40290

                    parse_pbesexpr(inner.into_inner())

614

615

20

                Rule::PbesExprTrue => Ok(PbesExpr::True),

616

                Rule::PbesExprFalse => Ok(PbesExpr::False),

617

12420

                Rule::PropVarInst => Ok(PbesExpr::PropVarInst(Mcrl2Parser::PropVarInst(Node::new(primary))?)),

618

                _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),

619

620

67570

})

621

43400

        .map_prefix(|op, expr| match op.as_rule() {

622

13320

            Rule::PbesExprNegation => Ok(PbesExpr::Negation(Box::new(expr?))),

623

            Rule::PbesExprExists => Ok(PbesExpr::Quantifier {

624

1570

                quantifier: Quantifier::Exists,

625

1570

                variables: Mcrl2Parser::PbesExprExists(Node::new(op))?,

626

1570

                body: Box::new(expr?),

627

}),

628

            Rule::PbesExprForall => Ok(PbesExpr::Quantifier {

629

1290

                quantifier: Quantifier::Forall,

630

1290

                variables: Mcrl2Parser::PbesExprForall(Node::new(op))?,

631

1290

                body: Box::new(expr?),

632

}),

633

            _ => unimplemented!("Unexpected prefix operator: {:?}", op.as_rule()),

634

16180

})

635

43400

        .map_infix(|lhs, op, rhs| match op.as_rule() {

636

            Rule::PbesExprConj => Ok(PbesExpr::Binary {

637

8510

                op: PbesExprBinaryOp::Conjunction,

638

8510

                lhs: Box::new(lhs?),

639

8510

                rhs: Box::new(rhs?),

640

}),

641

            Rule::PbesExprDisj => Ok(PbesExpr::Binary {

642

6840

                op: PbesExprBinaryOp::Disjunction,

643

6840

                lhs: Box::new(lhs?),

644

6840

                rhs: Box::new(rhs?),

645

}),

646

            Rule::PbesExprImplies => Ok(PbesExpr::Binary {

647

8820

                op: PbesExprBinaryOp::Implies,

648

8820

                lhs: Box::new(lhs?),

649

8820

                rhs: Box::new(rhs?),

650

}),

651

            _ => unimplemented!("Unexpected binary operator: {:?}", op.as_rule()),

652

24170

})

653

43400

        .parse(pairs)

654

43400

655

656

10

static PRESEXPR_PRATT_PARSER: LazyLock<PrattParser<Rule>> = LazyLock::new(|| {

657

    // Precedence is defined lowest to highest

658

10

    PrattParser::new()

659

10

        .op(Op::prefix(Rule::PresExprInf) | Op::prefix(Rule::PresExprSup) | Op::prefix(Rule::PresExprSum)) // $right 0

660

10

        .op(Op::infix(Rule::PresExprAdd, Assoc::Right)) // $right 2

661

10

        .op(Op::infix(Rule::PbesExprImplies, Assoc::Right)) // $right 3

662

10

        .op(Op::infix(Rule::PbesExprDisj, Assoc::Right)) // $right 4

663

10

        .op(Op::infix(Rule::PbesExprConj, Assoc::Right)) // $right 5

664

10

        .op(Op::prefix(Rule::PresExprLeftConstantMultiply) | Op::postfix(Rule::PresExprRightConstMultiply)) // $right 6

665

10

        .op(Op::prefix(Rule::PbesExprNegation)) // $right 7

666

10

});

667

668

#[allow(clippy::result_large_err)]

669

40

pub fn parse_presexpr(pairs: Pairs<Rule>) -> ParseResult<PresExpr> {

670

40

    PRESEXPR_PRATT_PARSER

671

80

        .map_primary(|primary| match primary.as_rule() {

672

10

            Rule::DataValExpr => Ok(PresExpr::DataValExpr(Mcrl2Parser::DataValExpr(Node::new(primary))?)),

673

            Rule::PresExprParens => {

674

                // Handle parentheses by recursively parsing the inner expression

675

20

                let inner = primary

676

20

                    .into_inner()

677

20

                    .next()

678

20

                    .expect("Expected inner expression in brackets");

679

20

                parse_presexpr(inner.into_inner())

680

681

            Rule::PbesExprTrue => Ok(PresExpr::True),

682

            Rule::PbesExprFalse => Ok(PresExpr::False),

683

50

            Rule::PropVarInst => Ok(PresExpr::PropVarInst(Mcrl2Parser::PropVarInst(Node::new(primary))?)),

684

            Rule::PresExprEqinf => Ok(Mcrl2Parser::PresExprEqinf(Node::new(primary))?),

685

            Rule::PresExprEqninf => Ok(Mcrl2Parser::PresExprEqninf(Node::new(primary))?),

686

            Rule::PresExprCondsm => Ok(Mcrl2Parser::PresExprCondsm(Node::new(primary))?),

687

            Rule::PresExprCondeq => Ok(Mcrl2Parser::PresExprCondeq(Node::new(primary))?),

688

            _ => unimplemented!("Unexpected rule: {:?}", primary.as_rule()),

689

80

})

690

40

        .map_prefix(|op, expr| match op.as_rule() {

691

            Rule::PbesExprNegation => Ok(PresExpr::Negation(Box::new(expr?))),

692

            Rule::PresExprInf => Ok(PresExpr::Bound {

693

                op: Bound::Inf,

694

                expr: Box::new(expr?),

695

                variables: Mcrl2Parser::PresExprInf(Node::new(op))?,

696

}),

697

            Rule::PresExprSup => Ok(PresExpr::Bound {

698

10

                op: Bound::Sup,

699

10

                expr: Box::new(expr?),

700

10

                variables: Mcrl2Parser::PresExprSup(Node::new(op))?,

701

}),

702

            Rule::PresExprSum => Ok(PresExpr::Bound {

703

                op: Bound::Sum,

704

                expr: Box::new(expr?),

705

                variables: Mcrl2Parser::PresExprSum(Node::new(op))?,

706

}),

707

            Rule::PresExprLeftConstantMultiply => Ok(PresExpr::LeftConstantMultiply {

708

10

                constant: Mcrl2Parser::PresExprLeftConstantMultiply(Node::new(op))?,

709

10

                expr: Box::new(expr?),

710

}),

711

            _ => unimplemented!("Unexpected prefix operator: {:?}", op.as_rule()),

712

20

})

713

40

        .map_infix(|lhs, op, rhs| match op.as_rule() {

714

            Rule::PbesExprImplies => Ok(PresExpr::Binary {

715

10

                op: PresExprBinaryOp::Implies,

716

10

                lhs: Box::new(lhs?),

717

10

                rhs: Box::new(rhs?),

718

}),

719

            Rule::PbesExprDisj => Ok(PresExpr::Binary {

720

                op: PresExprBinaryOp::Disjunction,

721

                lhs: Box::new(lhs?),

722

                rhs: Box::new(rhs?),

723

}),

724

            Rule::PbesExprConj => Ok(PresExpr::Binary {

725

10

                op: PresExprBinaryOp::Conjunction,

726

10

                lhs: Box::new(lhs?),

727

10

                rhs: Box::new(rhs?),

728

}),

729

            Rule::PresExprAdd => Ok(PresExpr::Binary {

730

20

                op: PresExprBinaryOp::Add,

731

20

                lhs: Box::new(lhs?),

732

20

                rhs: Box::new(rhs?),

733

}),

734

            _ => unimplemented!("Unexpected binary operator: {:?}", op.as_rule()),

735

40

})

736

40

        .map_postfix(|expr, postfix| match postfix.as_rule() {

737

            Rule::PresExprRightConstMultiply => Ok(PresExpr::RightConstantMultiply {

738

                expr: Box::new(expr?),

739

                constant: Mcrl2Parser::PresExprRightConstMultiply(Node::new(postfix))?,

740

}),

741

            _ => unimplemented!("Unexpected postfix operator: {:?}", postfix.as_rule()),

742

})

743

40

        .parse(pairs)

744

40