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::Assoc::Left;

7

use pest::pratt_parser::Assoc::Right;

8

use pest::pratt_parser::Op;

9

use pest::pratt_parser::PrattParser;

10

11

use merc_pest_consume::Node;

12

13

use crate::ActFrm;

14

use crate::ActFrmBinaryOp;

15

use crate::Bound;

16

use crate::DataExpr;

17

use crate::DataExprBinaryOp;

18

use crate::DataExprUnaryOp;

19

use crate::FixedPointOperator;

20

use crate::Mcrl2Parser;

21

use crate::ModalityOperator;

22

use crate::ParseResult;

23

use crate::PbesExpr;

24

use crate::PbesExprBinaryOp;

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

1432

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

37

    // Precedence is defined lowest to highest

38

1432

    PrattParser::new()

39

        // Sort operators

40

1432

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

41

1432

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

42

1432

});

43

44

#[allow(clippy::result_large_err)]

45

99692

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

46

99692

    match primary.as_rule() {

47

76240

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

48

3524

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

49

50

4076

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

51

500

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

52

2240

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

53

6556

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

54

224

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

55

56

2276

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

57

992

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

58

188

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

59

64

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

60

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

61

62

        Rule::SortExprParens => {

63

            // Handle parentheses by recursively parsing the inner expression

64

60

            let inner = primary

65

60

                .into_inner()

66

60

                .next()

67

60

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

68

60

            parse_sortexpr(inner.into_inner())

69

70

71

2752

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

72

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

73

74

99692

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

62276

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

79

62276

    SORT_PRATT_PARSER

80

95124

        .map_primary(|primary| parse_sortexpr_primary(primary))

81

62276

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

82

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

83

13520

                domain: Box::new(lhs?),

84

13520

                range: Box::new(rhs?),

85

}),

86

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

87

19328

                lhs: Box::new(lhs?),

88

19328

                rhs: Box::new(rhs?),

89

}),

90

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

91

32848

})

92

62276

        .parse(pairs)

93

62276

94

95

1480

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

96

    // Precedence is defined lowest to highest

97

1480

    PrattParser::new()

98

1480

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

99

1480

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

100

1480

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

101

1480

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

102

1480

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

103

1480

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

104

1480

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

105

1480

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

106

1480

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

107

1480

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

108

1480

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

109

1480

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

110

1480

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

111

1480

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

112

1480

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

113

1480

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

114

1480

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

115

1480

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

116

1480

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

117

1480

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

118

1480

            | Op::prefix(Rule::DataExprMinus)

119

1480

            | Op::prefix(Rule::DataExprNegation)

120

1480

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

121

1480

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

122

1480

});

123

124

#[allow(clippy::result_large_err)]

125

535144

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

126

535144

    DATAEXPR_PRATT_PARSER

127

577496

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

128

2312

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

129

2316

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

130

2216

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

131

680

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

132

140

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

133

1900

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

134

184

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

135

44

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

136

1392

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

137

23856

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

138

534148

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

139

140

            Rule::DataExprBrackets => {

141

                // Handle parentheses by recursively parsing the inner expression

142

8308

                let inner = primary

143

8308

                    .into_inner()

144

8308

                    .next()

145

8308

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

146

8308

                parse_dataexpr(inner.into_inner())

147

148

149

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

150

577496

})

151

535144

        .map_infix(|lhs, op, rhs| {

152

42352

            let op = match op.as_rule() {

153

6104

                Rule::DataExprConj => DataExprBinaryOp::Conj,

154

1888

                Rule::DataExprDisj => DataExprBinaryOp::Disj,

155

8108

                Rule::DataExprEq => DataExprBinaryOp::Equal,

156

2332

                Rule::DataExprNeq => DataExprBinaryOp::NotEqual,

157

1424

                Rule::DataExprLess => DataExprBinaryOp::LessThan,

158

1608

                Rule::DataExprLeq => DataExprBinaryOp::LessEqual,

159

960

                Rule::DataExprGreater => DataExprBinaryOp::GreaterThan,

160

636

                Rule::DataExprGeq => DataExprBinaryOp::GreaterEqual,

161

1956

                Rule::DataExprIn => DataExprBinaryOp::In,

162

3124

                Rule::DataExprCons => DataExprBinaryOp::Cons,

163

44

                Rule::DataExprSnoc => DataExprBinaryOp::Snoc,

164

172

                Rule::DataExprConcat => DataExprBinaryOp::Concat,

165

5836

                Rule::DataExprAdd => DataExprBinaryOp::Add,

166

2600

                Rule::DataExprSubtract => DataExprBinaryOp::Subtract,

167

320

                Rule::DataExprDiv => DataExprBinaryOp::Div,

168

52

                Rule::DataExprIntDiv => DataExprBinaryOp::IntDiv,

169

352

                Rule::DataExprMod => DataExprBinaryOp::Mod,

170

840

                Rule::DataExprMult => DataExprBinaryOp::Multiply,

171

3776

                Rule::DataExprAt => DataExprBinaryOp::At,

172

220

                Rule::DataExprImpl => DataExprBinaryOp::Implies,

173

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

174

};

175

176

            Ok(DataExpr::Binary {

177

42352

op,

178

42352

                lhs: Box::new(lhs?),

179

42352

                rhs: Box::new(rhs?),

180

})

181

42352

})

182

535144

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

183

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

184

1144

                expr: Box::new(expr?),

185

1144

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

186

}),

187

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

188

156232

                function: Box::new(expr?),

189

156232

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

190

}),

191

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

192

96

                expr: Box::new(expr?),

193

96

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

194

}),

195

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

196

157472

})

197

535144

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

198

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

199

100

                op: Quantifier::Forall,

200

100

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

201

100

                body: Box::new(expr?),

202

}),

203

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

204

152

                op: Quantifier::Exists,

205

152

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

206

152

                body: Box::new(expr?),

207

}),

208

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

209

116

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

210

116

                body: Box::new(expr?),

211

}),

212

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

213

1692

                op: DataExprUnaryOp::Negation,

214

1692

                expr: Box::new(expr?),

215

}),

216

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

217

164

                op: DataExprUnaryOp::Minus,

218

164

                expr: Box::new(expr?),

219

}),

220

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

221

232

                op: DataExprUnaryOp::Size,

222

232

                expr: Box::new(expr?),

223

}),

224

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

225

2456

})

226

535144

        .parse(pairs)

227

535144

228

229

676

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

230

    // Precedence is defined lowest to highest

231

676

    PrattParser::new()

232

676

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

233

676

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

234

676

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

235

676

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

236

676

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

237

676

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

238

676

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

239

676

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

240

676

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

241

676

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

242

676

});

243

244

#[allow(clippy::result_large_err)]

245

13248

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

246

13248

    PROCEXPR_PRATT_PARSER

247

31884

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

248

2340

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

249

368

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

250

24

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

251

28

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

252

396

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

253

184

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

254

36

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

255

404

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

256

            Rule::Action => {

257

22472

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

258

259

22472

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

260

261

            Rule::ProcExprBrackets => {

262

                // Handle parentheses by recursively parsing the inner expression

263

5632

                let inner = primary

264

5632

                    .into_inner()

265

5632

                    .next()

266

5632

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

267

5632

                parse_process_expr(inner.into_inner())

268

269

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

270

31884

})

271

18636

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

272

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

273

4168

                op: ProcExprBinaryOp::Choice,

274

4168

                lhs: Box::new(lhs?),

275

4168

                rhs: Box::new(rhs?),

276

}),

277

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

278

2148

                op: ProcExprBinaryOp::Parallel,

279

2148

                lhs: Box::new(lhs?),

280

2148

                rhs: Box::new(rhs?),

281

}),

282

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

283

                op: ProcExprBinaryOp::LeftMerge,

284

                lhs: Box::new(lhs?),

285

                rhs: Box::new(rhs?),

286

}),

287

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

288

10692

                op: ProcExprBinaryOp::Sequence,

289

10692

                lhs: Box::new(lhs?),

290

10692

                rhs: Box::new(rhs?),

291

}),

292

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

293

1628

                op: ProcExprBinaryOp::CommMerge,

294

1628

                lhs: Box::new(lhs?),

295

1628

                rhs: Box::new(rhs?),

296

}),

297

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

298

18636

})

299

13248

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

300

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

301

3792

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

302

3792

                operand: Box::new(expr?),

303

}),

304

            Rule::ProcExprDist => {

305

104

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

306

307

                Ok(ProcessExpr::Dist {

308

104

                    variables,

309

104

                    expr: data_expr,

310

104

                    operand: Box::new(expr?),

311

})

312

313

            Rule::ProcExprIf => {

314

3764

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

315

316

                Ok(ProcessExpr::Condition {

317

3764

                    condition,

318

3764

                    then: Box::new(expr?),

319

3764

                    else_: None,

320

})

321

322

            Rule::ProcExprIfThen => {

323

2268

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

324

325

                Ok(ProcessExpr::Condition {

326

2268

                    condition,

327

2268

                    then: Box::new(then),

328

2268

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

329

})

330

331

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

332

9928

})

333

13248

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

334

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

335

56

                expr: Box::new(expr?),

336

56

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

337

}),

338

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

339

56

})

340

13248

        .parse(pairs)

341

13248

342

343

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

344

601

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

345

    // Precedence is defined lowest to highest

346

601

    PrattParser::new()

347

601

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

348

601

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

349

601

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

350

601

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

351

601

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

352

601

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

353

601

});

354

355

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

356

#[allow(clippy::result_large_err)]

357

3953

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

358

3953

    ACTFRM_PRATT_PARSER

359

4461

        .map_primary(|primary| {

360

4461

            match primary.as_rule() {

361

492

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

362

4

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

363

3401

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

364

84

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

365

                Rule::ActFrmBrackets => {

366

                    // Handle parentheses by recursively parsing the inner expression

367

480

                    let inner = primary

368

480

                        .into_inner()

369

480

                        .next()

370

480

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

371

480

                    parse_actfrm(inner.into_inner())

372

373

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

374

375

4461

})

376

3953

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

377

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

378

520

                quantifier: Quantifier::Exists,

379

520

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

380

520

                body: Box::new(expr?),

381

}),

382

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

383

16

                quantifier: Quantifier::Forall,

384

16

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

385

16

                body: Box::new(expr?),

386

}),

387

620

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

388

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

389

1156

})

390

3953

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

391

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

392

300

                op: ActFrmBinaryOp::Union,

393

300

                lhs: Box::new(lhs?),

394

300

                rhs: Box::new(rhs?),

395

}),

396

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

397

200

                op: ActFrmBinaryOp::Intersect,

398

200

                lhs: Box::new(lhs?),

399

200

                rhs: Box::new(rhs?),

400

}),

401

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

402

8

                op: ActFrmBinaryOp::Implies,

403

8

                lhs: Box::new(lhs?),

404

8

                rhs: Box::new(rhs?),

405

}),

406

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

407

508

})

408

3953

        .parse(pairs)

409

3953

410

411

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

412

601

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

413

    // Precedence is defined lowest to highest

414

601

    PrattParser::new()

415

601

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

416

601

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

417

601

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

418

601

});

419

420

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

421

#[allow(clippy::result_large_err)]

422

3025

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

423

3025

    REGFRM_PRATT_PARSER

424

3481

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

425

3473

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

426

            Rule::RegFrmBackets => {

427

                // Handle parentheses by recursively parsing the inner expression

428

8

                let inner = primary

429

8

                    .into_inner()

430

8

                    .next()

431

8

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

432

8

                parse_regfrm(inner.into_inner())

433

434

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

435

3481

})

436

3025

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

437

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

438

20

                lhs: Box::new(lhs?),

439

20

                rhs: Box::new(rhs?),

440

}),

441

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

442

436

                lhs: Box::new(lhs?),

443

436

                rhs: Box::new(rhs?),

444

}),

445

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

446

456

})

447

3025

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

448

536

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

449

4

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

450

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

451

540

})

452

3025

        .parse(pairs)

453

3025

454

455

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

456

601

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

457

    // Precedence is defined lowest to highest

458

601

    PrattParser::new()

459

601

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

460

601

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

461

601

            | Op::prefix(Rule::StateFrmExists)

462

601

            | Op::prefix(Rule::StateFrmInf)

463

601

            | Op::prefix(Rule::StateFrmSup)

464

601

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

465

601

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

466

601

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

467

601

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

468

601

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

469

601

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

470

601

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

471

601

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

472

601

});

473

474

#[allow(clippy::result_large_err)]

475

4445

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

476

4445

    STATEFRM_PRATT_PARSER

477

8639

        .map_primary(|primary| {

478

8639

            match primary.as_rule() {

479

4259

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

480

392

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

481

144

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

482

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

483

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

484

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

485

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

486

                Rule::StateFrmBrackets => {

487

                    // Handle parentheses by recursively parsing the inner expression

488

3844

                    let inner = primary

489

3844

                        .into_inner()

490

3844

                        .next()

491

3844

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

492

3844

                    parse_statefrm(inner.into_inner())

493

494

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

495

496

8639

})

497

4967

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

498

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

499

8

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

500

8

                Box::new(expr?),

501

)),

502

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

503

1160

                operator: ModalityOperator::Diamond,

504

1160

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

505

1160

                expr: Box::new(expr?),

506

}),

507

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

508

1857

                operator: ModalityOperator::Box,

509

1857

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

510

1857

                expr: Box::new(expr?),

511

}),

512

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

513

364

                quantifier: Quantifier::Exists,

514

364

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

515

364

                body: Box::new(expr?),

516

}),

517

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

518

696

                quantifier: Quantifier::Forall,

519

696

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

520

696

                body: Box::new(expr?),

521

}),

522

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

523

370

                operator: FixedPointOperator::Least,

524

370

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

525

370

                body: Box::new(expr?),

526

}),

527

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

528

448

                operator: FixedPointOperator::Greatest,

529

448

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

530

448

                body: Box::new(expr?),

531

}),

532

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

533

60

                op: StateFrmUnaryOp::Negation,

534

60

                expr: Box::new(expr?),

535

}),

536

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

537

                bound: Bound::Sup,

538

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

539

                body: Box::new(expr?),

540

}),

541

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

542

                bound: Bound::Sup,

543

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

544

                body: Box::new(expr?),

545

}),

546

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

547

4

                bound: Bound::Sup,

548

4

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

549

4

                body: Box::new(expr?),

550

}),

551

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

552

4967

})

553

4446

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

554

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

555

4

                op: StateFrmOp::Addition,

556

4

                lhs: Box::new(lhs?),

557

4

                rhs: Box::new(rhs?),

558

}),

559

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

560

1028

                op: StateFrmOp::Implies,

561

1028

                lhs: Box::new(lhs?),

562

1028

                rhs: Box::new(rhs?),

563

}),

564

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

565

780

                op: StateFrmOp::Disjunction,

566

780

                lhs: Box::new(lhs?),

567

780

                rhs: Box::new(rhs?),

568

}),

569

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

570

2382

                op: StateFrmOp::Conjunction,

571

2382

                lhs: Box::new(lhs?),

572

2382

                rhs: Box::new(rhs?),

573

}),

574

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

575

4194

})

576

4445

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

577

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

578

                Box::new(expr?),

579

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

580

)),

581

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

582

})

583

4445

        .parse(pairs)

584

4445

585

586

12

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

587

    // Precedence is defined lowest to highest

588

12

    PrattParser::new()

589

12

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

590

12

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

591

12

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

592

12

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

593

12

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

594

12

});

595

596

#[allow(clippy::result_large_err)]

597

20

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

598

20

    PBESEXPR_PRATT_PARSER

599

28

        .map_primary(|primary| {

600

28

            match primary.as_rule() {

601

8

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

602

                Rule::PbesExprParens => {

603

                    // Handle parentheses by recursively parsing the inner expression

604

                    let inner = primary

605

                        .into_inner()

606

                        .next()

607

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

608

                    parse_pbesexpr(inner.into_inner())

609

610

4

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

611

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

612

16

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

613

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

614

615

28

})

616

20

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

617

4

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

618

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

619

4

})

620

20

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

621

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

622

8

                op: PbesExprBinaryOp::Conjunction,

623

8

                lhs: Box::new(lhs?),

624

8

                rhs: Box::new(rhs?),

625

}),

626

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

627

                op: PbesExprBinaryOp::Disjunction,

628

                lhs: Box::new(lhs?),

629

                rhs: Box::new(rhs?),

630

}),

631

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

632

                op: PbesExprBinaryOp::Implies,

633

                lhs: Box::new(lhs?),

634

                rhs: Box::new(rhs?),

635

}),

636

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

637

8

})

638

20

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

639

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

640

                quantifier: Quantifier::Exists,

641

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

642

                body: Box::new(expr?),

643

}),

644

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

645

                quantifier: Quantifier::Forall,

646

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

647

                body: Box::new(expr?),

648

}),

649

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

650

})

651

20

        .parse(pairs)

652

20

653

654

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

655

    // Precedence is defined lowest to highest

656

    PrattParser::new()

657

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

658

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

659

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

660

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

661

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

662

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

663

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

664

});