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

1074

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

37

    // Precedence is defined lowest to highest

38

1074

    PrattParser::new()

39

        // Sort operators

40

1074

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

41

1074

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

42

1074

});

43

44

#[allow(clippy::result_large_err)]

45

74769

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

46

74769

    match primary.as_rule() {

47

57180

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

48

2643

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

49

50

3057

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

51

375

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

52

1680

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

53

4917

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

54

168

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

55

56

1707

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

57

744

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

58

141

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

59

48

        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

45

            let inner = primary

65

45

                .into_inner()

66

45

                .next()

67

45

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

68

45

            parse_sortexpr(inner.into_inner())

69

70

71

2064

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

72

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

73

74

74769

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

46707

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

79

46707

    SORT_PRATT_PARSER

80

71343

        .map_primary(|primary| parse_sortexpr_primary(primary))

81

46707

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

82

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

83

10140

                domain: Box::new(lhs?),

84

10140

                range: Box::new(rhs?),

85

}),

86

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

87

14496

                lhs: Box::new(lhs?),

88

14496

                rhs: Box::new(rhs?),

89

}),

90

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

91

24636

})

92

46707

        .parse(pairs)

93

46707

94

95

1107

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

96

    // Precedence is defined lowest to highest

97

1107

    PrattParser::new()

98

1107

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

99

1107

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

100

1107

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

101

1107

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

102

1107

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

103

1107

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

104

1107

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

105

1107

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

106

1107

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

107

1107

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

108

1107

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

109

1107

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

110

1107

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

111

1107

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

112

1107

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

113

1107

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

114

1107

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

115

1107

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

116

1107

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

117

1107

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

118

1107

            | Op::prefix(Rule::DataExprMinus)

119

1107

            | Op::prefix(Rule::DataExprNegation)

120

1107

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

121

1107

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

122

1107

});

123

124

#[allow(clippy::result_large_err)]

125

401280

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

126

401280

    DATAEXPR_PRATT_PARSER

127

433044

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

128

1716

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

129

1719

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

130

1662

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

131

510

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

132

105

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

133

1425

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

134

138

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

135

33

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

136

1044

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

137

17892

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

138

400569

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

139

140

            Rule::DataExprBrackets => {

141

                // Handle parentheses by recursively parsing the inner expression

142

6231

                let inner = primary

143

6231

                    .into_inner()

144

6231

                    .next()

145

6231

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

146

6231

                parse_dataexpr(inner.into_inner())

147

148

149

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

150

433044

})

151

401280

        .map_infix(|lhs, op, rhs| {

152

31764

            let op = match op.as_rule() {

153

4578

                Rule::DataExprConj => DataExprBinaryOp::Conj,

154

1416

                Rule::DataExprDisj => DataExprBinaryOp::Disj,

155

6081

                Rule::DataExprEq => DataExprBinaryOp::Equal,

156

1749

                Rule::DataExprNeq => DataExprBinaryOp::NotEqual,

157

1068

                Rule::DataExprLess => DataExprBinaryOp::LessThan,

158

1206

                Rule::DataExprLeq => DataExprBinaryOp::LessEqual,

159

720

                Rule::DataExprGreater => DataExprBinaryOp::GreaterThan,

160

477

                Rule::DataExprGeq => DataExprBinaryOp::GreaterEqual,

161

1467

                Rule::DataExprIn => DataExprBinaryOp::In,

162

2343

                Rule::DataExprCons => DataExprBinaryOp::Cons,

163

33

                Rule::DataExprSnoc => DataExprBinaryOp::Snoc,

164

129

                Rule::DataExprConcat => DataExprBinaryOp::Concat,

165

4377

                Rule::DataExprAdd => DataExprBinaryOp::Add,

166

1950

                Rule::DataExprSubtract => DataExprBinaryOp::Subtract,

167

240

                Rule::DataExprDiv => DataExprBinaryOp::Div,

168

39

                Rule::DataExprIntDiv => DataExprBinaryOp::IntDiv,

169

264

                Rule::DataExprMod => DataExprBinaryOp::Mod,

170

630

                Rule::DataExprMult => DataExprBinaryOp::Multiply,

171

2832

                Rule::DataExprAt => DataExprBinaryOp::At,

172

165

                Rule::DataExprImpl => DataExprBinaryOp::Implies,

173

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

174

};

175

176

            Ok(DataExpr::Binary {

177

31764

op,

178

31764

                lhs: Box::new(lhs?),

179

31764

                rhs: Box::new(rhs?),

180

})

181

31764

})

182

401280

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

183

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

184

858

                expr: Box::new(expr?),

185

858

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

186

}),

187

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

188

117174

                function: Box::new(expr?),

189

117174

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

190

}),

191

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

192

72

                expr: Box::new(expr?),

193

72

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

194

}),

195

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

196

118104

})

197

401280

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

198

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

199

75

                op: Quantifier::Forall,

200

75

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

201

75

                body: Box::new(expr?),

202

}),

203

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

204

114

                op: Quantifier::Exists,

205

114

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

206

114

                body: Box::new(expr?),

207

}),

208

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

209

87

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

210

87

                body: Box::new(expr?),

211

}),

212

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

213

1269

                op: DataExprUnaryOp::Negation,

214

1269

                expr: Box::new(expr?),

215

}),

216

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

217

123

                op: DataExprUnaryOp::Minus,

218

123

                expr: Box::new(expr?),

219

}),

220

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

221

174

                op: DataExprUnaryOp::Size,

222

174

                expr: Box::new(expr?),

223

}),

224

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

225

1842

})

226

401280

        .parse(pairs)

227

401280

228

229

507

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

230

    // Precedence is defined lowest to highest

231

507

    PrattParser::new()

232

507

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

233

507

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

234

507

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

235

507

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

236

507

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

237

507

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

238

507

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

239

507

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

240

507

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

241

507

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

242

507

});

243

244

#[allow(clippy::result_large_err)]

245

9936

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

246

9936

    PROCEXPR_PRATT_PARSER

247

23913

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

248

1755

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

249

276

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

250

18

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

251

21

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

252

297

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

253

138

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

254

27

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

255

303

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

256

            Rule::Action => {

257

16854

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

258

259

16854

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

260

261

            Rule::ProcExprBrackets => {

262

                // Handle parentheses by recursively parsing the inner expression

263

4224

                let inner = primary

264

4224

                    .into_inner()

265

4224

                    .next()

266

4224

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

267

4224

                parse_process_expr(inner.into_inner())

268

269

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

270

23913

})

271

13977

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

272

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

273

3126

                op: ProcExprBinaryOp::Choice,

274

3126

                lhs: Box::new(lhs?),

275

3126

                rhs: Box::new(rhs?),

276

}),

277

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

278

1611

                op: ProcExprBinaryOp::Parallel,

279

1611

                lhs: Box::new(lhs?),

280

1611

                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

8019

                op: ProcExprBinaryOp::Sequence,

289

8019

                lhs: Box::new(lhs?),

290

8019

                rhs: Box::new(rhs?),

291

}),

292

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

293

1221

                op: ProcExprBinaryOp::CommMerge,

294

1221

                lhs: Box::new(lhs?),

295

1221

                rhs: Box::new(rhs?),

296

}),

297

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

298

13977

})

299

9936

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

300

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

301

2844

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

302

2844

                operand: Box::new(expr?),

303

}),

304

            Rule::ProcExprDist => {

305

78

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

306

307

                Ok(ProcessExpr::Dist {

308

78

                    variables,

309

78

                    expr: data_expr,

310

78

                    operand: Box::new(expr?),

311

})

312

313

            Rule::ProcExprIf => {

314

2823

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

315

316

                Ok(ProcessExpr::Condition {

317

2823

                    condition,

318

2823

                    then: Box::new(expr?),

319

2823

                    else_: None,

320

})

321

322

            Rule::ProcExprIfThen => {

323

1701

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

324

325

                Ok(ProcessExpr::Condition {

326

1701

                    condition,

327

1701

                    then: Box::new(then),

328

1701

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

329

})

330

331

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

332

7446

})

333

9936

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

334

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

335

42

                expr: Box::new(expr?),

336

42

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

337

}),

338

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

339

42

})

340

9936

        .parse(pairs)

341

9936

342

343

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

344

448

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

345

    // Precedence is defined lowest to highest

346

448

    PrattParser::new()

347

448

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

348

448

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

349

448

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

350

448

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

351

448

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

352

448

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

353

448

});

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

2956

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

358

2956

    ACTFRM_PRATT_PARSER

359

3337

        .map_primary(|primary| {

360

3337

            match primary.as_rule() {

361

369

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

362

3

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

363

2542

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

364

63

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

365

                Rule::ActFrmBrackets => {

366

                    // Handle parentheses by recursively parsing the inner expression

367

360

                    let inner = primary

368

360

                        .into_inner()

369

360

                        .next()

370

360

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

371

360

                    parse_actfrm(inner.into_inner())

372

373

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

374

375

3337

})

376

2956

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

377

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

378

390

                quantifier: Quantifier::Exists,

379

390

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

380

390

                body: Box::new(expr?),

381

}),

382

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

383

12

                quantifier: Quantifier::Forall,

384

12

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

385

12

                body: Box::new(expr?),

386

}),

387

465

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

388

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

389

867

})

390

2956

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

391

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

392

225

                op: ActFrmBinaryOp::Union,

393

225

                lhs: Box::new(lhs?),

394

225

                rhs: Box::new(rhs?),

395

}),

396

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

397

150

                op: ActFrmBinaryOp::Intersect,

398

150

                lhs: Box::new(lhs?),

399

150

                rhs: Box::new(rhs?),

400

}),

401

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

402

6

                op: ActFrmBinaryOp::Implies,

403

6

                lhs: Box::new(lhs?),

404

6

                rhs: Box::new(rhs?),

405

}),

406

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

407

381

})

408

2956

        .parse(pairs)

409

2956

410

411

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

412

448

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

413

    // Precedence is defined lowest to highest

414

448

    PrattParser::new()

415

448

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

416

448

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

417

448

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

418

448

});

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

2260

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

423

2260

    REGFRM_PRATT_PARSER

424

2602

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

425

2596

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

426

            Rule::RegFrmBackets => {

427

                // Handle parentheses by recursively parsing the inner expression

428

6

                let inner = primary

429

6

                    .into_inner()

430

6

                    .next()

431

6

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

432

6

                parse_regfrm(inner.into_inner())

433

434

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

435

2602

})

436

2260

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

437

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

438

15

                lhs: Box::new(lhs?),

439

15

                rhs: Box::new(rhs?),

440

}),

441

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

442

327

                lhs: Box::new(lhs?),

443

327

                rhs: Box::new(rhs?),

444

}),

445

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

446

342

})

447

2260

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

448

402

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

449

3

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

450

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

451

405

})

452

2260

        .parse(pairs)

453

2260

454

455

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

456

448

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

457

    // Precedence is defined lowest to highest

458

448

    PrattParser::new()

459

448

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

460

448

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

461

448

            | Op::prefix(Rule::StateFrmExists)

462

448

            | Op::prefix(Rule::StateFrmInf)

463

448

            | Op::prefix(Rule::StateFrmSup)

464

448

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

465

448

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

466

448

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

467

448

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

468

448

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

469

448

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

470

448

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

471

448

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

472

448

});

473

474

#[allow(clippy::result_large_err)]

475

3328

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

476

3328

    STATEFRM_PRATT_PARSER

477

6468

        .map_primary(|primary| {

478

6468

            match primary.as_rule() {

479

3186

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

480

294

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

481

108

                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

2880

                    let inner = primary

489

2880

                        .into_inner()

490

2880

                        .next()

491

2880

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

492

2880

                    parse_statefrm(inner.into_inner())

493

494

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

495

496

6468

})

497

3711

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

498

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

499

6

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

500

6

                Box::new(expr?),

501

)),

502

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

503

870

                operator: ModalityOperator::Diamond,

504

870

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

505

870

                expr: Box::new(expr?),

506

}),

507

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

508

1384

                operator: ModalityOperator::Box,

509

1384

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

510

1384

                expr: Box::new(expr?),

511

}),

512

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

513

273

                quantifier: Quantifier::Exists,

514

273

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

515

273

                body: Box::new(expr?),

516

}),

517

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

518

522

                quantifier: Quantifier::Forall,

519

522

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

520

522

                body: Box::new(expr?),

521

}),

522

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

523

275

                operator: FixedPointOperator::Least,

524

275

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

525

275

                body: Box::new(expr?),

526

}),

527

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

528

333

                operator: FixedPointOperator::Greatest,

529

333

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

530

333

                body: Box::new(expr?),

531

}),

532

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

533

45

                op: StateFrmUnaryOp::Negation,

534

45

                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

3

                bound: Bound::Sup,

548

3

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

549

3

                body: Box::new(expr?),

550

}),

551

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

552

3711

})

553

3329

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

554

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

555

3

                op: StateFrmOp::Addition,

556

3

                lhs: Box::new(lhs?),

557

3

                rhs: Box::new(rhs?),

558

}),

559

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

560

771

                op: StateFrmOp::Implies,

561

771

                lhs: Box::new(lhs?),

562

771

                rhs: Box::new(rhs?),

563

}),

564

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

565

585

                op: StateFrmOp::Disjunction,

566

585

                lhs: Box::new(lhs?),

567

585

                rhs: Box::new(rhs?),

568

}),

569

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

570

1781

                op: StateFrmOp::Conjunction,

571

1781

                lhs: Box::new(lhs?),

572

1781

                rhs: Box::new(rhs?),

573

}),

574

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

575

3140

})

576

3328

        .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

3328

        .parse(pairs)

584

3328

585

586

9

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

587

    // Precedence is defined lowest to highest

588

9

    PrattParser::new()

589

9

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

590

9

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

591

9

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

592

9

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

593

9

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

594

9

});

595

596

#[allow(clippy::result_large_err)]

597

15

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

598

15

    PBESEXPR_PRATT_PARSER

599

21

        .map_primary(|primary| {

600

21

            match primary.as_rule() {

601

6

                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

3

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

611

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

612

12

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

613

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

614

615

21

})

616

15

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

617

3

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

618

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

619

3

})

620

15

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

621

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

622

6

                op: PbesExprBinaryOp::Conjunction,

623

6

                lhs: Box::new(lhs?),

624

6

                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

6

})

638

15

        .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

15

        .parse(pairs)

652

15

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

});