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::PresExpr;

26

use crate::PresExprBinaryOp;

27

use crate::ProcExprBinaryOp;

28

use crate::ProcessExpr;

29

use crate::Quantifier;

30

use crate::RegFrm;

31

use crate::Rule;

32

use crate::Sort;

33

use crate::StateFrm;

34

use crate::StateFrmOp;

35

use crate::StateFrmUnaryOp;

36

use crate::syntax_tree::SortExpression;

37

38

2208

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

39

    // Precedence is defined lowest to highest

40

2208

    PrattParser::new()

41

        // Sort operators

42

2208

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

43

2208

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

44

2208

});

45

46

#[allow(clippy::result_large_err)]

47

155076

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

48

155076

    match primary.as_rule() {

49

115752

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

50

6174

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

51

52

6426

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

53

1104

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

54

3864

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

55

10584

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

56

618

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

57

58

3528

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

59

1620

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

60

408

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

61

342

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

62

270

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

63

64

        Rule::SortExprParens => {

65

            // Handle parentheses by recursively parsing the inner expression

66

258

            let inner = primary

67

258

                .into_inner()

68

258

                .next()

69

258

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

70

258

            parse_sortexpr(inner.into_inner())

71

72

73

4128

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

74

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

75

76

155076

77

78

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

79

#[allow(clippy::result_large_err)]

80

96858

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

81

96858

    SORT_PRATT_PARSER

82

148224

        .map_primary(|primary| parse_sortexpr_primary(primary))

83

96858

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

84

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

85

21564

                domain: Box::new(lhs?),

86

21564

                range: Box::new(rhs?),

87

}),

88

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

89

29802

                lhs: Box::new(lhs?),

90

29802

                rhs: Box::new(rhs?),

91

}),

92

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

93

51366

})

94

96858

        .parse(pairs)

95

96858

96

97

2280

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

98

    // Precedence is defined lowest to highest

99

2280

    PrattParser::new()

100

2280

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

101

2280

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

102

2280

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

103

2280

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

104

2280

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

105

2280

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

106

2280

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

107

2280

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

108

2280

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

109

2280

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

110

2280

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

111

2280

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

112

2280

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

113

2280

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

114

2280

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

115

2280

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

116

2280

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

117

2280

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

118

2280

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

119

2280

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

120

2280

            | Op::prefix(Rule::DataExprMinus)

121

2280

            | Op::prefix(Rule::DataExprNegation)

122

2280

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

123

2280

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

124

2280

});

125

126

#[allow(clippy::result_large_err)]

127

824118

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

128

824118

    DATAEXPR_PRATT_PARSER

129

890934

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

130

3810

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

131

4098

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

132

3414

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

133

1248

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

134

498

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

135

2850

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

136

276

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

137

66

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

138

2088

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

139

35784

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

140

823542

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

141

142

            Rule::DataExprBrackets => {

143

                // Handle parentheses by recursively parsing the inner expression

144

13260

                let inner = primary

145

13260

                    .into_inner()

146

13260

                    .next()

147

13260

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

148

13260

                parse_dataexpr(inner.into_inner())

149

150

151

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

152

890934

})

153

824118

        .map_infix(|lhs, op, rhs| {

154

66816

            let op = match op.as_rule() {

155

9270

                Rule::DataExprConj => DataExprBinaryOp::Conj,

156

2910

                Rule::DataExprDisj => DataExprBinaryOp::Disj,

157

12630

                Rule::DataExprEq => DataExprBinaryOp::Equal,

158

3552

                Rule::DataExprNeq => DataExprBinaryOp::NotEqual,

159

2658

                Rule::DataExprLess => DataExprBinaryOp::LessThan,

160

2796

                Rule::DataExprLeq => DataExprBinaryOp::LessEqual,

161

1476

                Rule::DataExprGreater => DataExprBinaryOp::GreaterThan,

162

954

                Rule::DataExprGeq => DataExprBinaryOp::GreaterEqual,

163

2934

                Rule::DataExprIn => DataExprBinaryOp::In,

164

4878

                Rule::DataExprCons => DataExprBinaryOp::Cons,

165

84

                Rule::DataExprSnoc => DataExprBinaryOp::Snoc,

166

282

                Rule::DataExprConcat => DataExprBinaryOp::Concat,

167

9126

                Rule::DataExprAdd => DataExprBinaryOp::Add,

168

4128

                Rule::DataExprSubtract => DataExprBinaryOp::Subtract,

169

504

                Rule::DataExprDiv => DataExprBinaryOp::Div,

170

126

                Rule::DataExprIntDiv => DataExprBinaryOp::IntDiv,

171

570

                Rule::DataExprMod => DataExprBinaryOp::Mod,

172

1890

                Rule::DataExprMult => DataExprBinaryOp::Multiply,

173

5682

                Rule::DataExprAt => DataExprBinaryOp::At,

174

366

                Rule::DataExprImpl => DataExprBinaryOp::Implies,

175

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

176

};

177

178

            Ok(DataExpr::Binary {

179

66816

op,

180

66816

                lhs: Box::new(lhs?),

181

66816

                rhs: Box::new(rhs?),

182

})

183

66816

})

184

824118

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

185

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

186

1716

                expr: Box::new(expr?),

187

1716

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

188

}),

189

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

190

241962

                function: Box::new(expr?),

191

241962

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

192

}),

193

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

194

144

                expr: Box::new(expr?),

195

144

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

196

}),

197

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

198

243822

})

199

824118

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

200

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

201

162

                op: Quantifier::Forall,

202

162

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

203

162

                body: Box::new(expr?),

204

}),

205

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

206

228

                op: Quantifier::Exists,

207

228

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

208

228

                body: Box::new(expr?),

209

}),

210

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

211

174

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

212

174

                body: Box::new(expr?),

213

}),

214

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

215

2682

                op: DataExprUnaryOp::Negation,

216

2682

                expr: Box::new(expr?),

217

}),

218

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

219

354

                op: DataExprUnaryOp::Minus,

220

354

                expr: Box::new(expr?),

221

}),

222

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

223

408

                op: DataExprUnaryOp::Size,

224

408

                expr: Box::new(expr?),

225

}),

226

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

227

4008

})

228

824118

        .parse(pairs)

229

824118

230

231

1014

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

232

    // Precedence is defined lowest to highest

233

1014

    PrattParser::new()

234

1014

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

235

1014

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

236

1014

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

237

1014

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

238

1014

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

239

1014

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

240

1014

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

241

1014

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

242

1014

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

243

1014

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

244

1014

});

245

246

#[allow(clippy::result_large_err)]

247

19872

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

248

19872

    PROCEXPR_PRATT_PARSER

249

47826

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

250

3510

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

251

552

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

252

36

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

253

42

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

254

594

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

255

276

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

256

54

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

257

606

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

258

            Rule::Action => {

259

33708

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

260

261

33708

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

262

263

            Rule::ProcExprBrackets => {

264

                // Handle parentheses by recursively parsing the inner expression

265

8448

                let inner = primary

266

8448

                    .into_inner()

267

8448

                    .next()

268

8448

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

269

8448

                parse_process_expr(inner.into_inner())

270

271

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

272

47826

})

273

27954

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

274

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

275

6252

                op: ProcExprBinaryOp::Choice,

276

6252

                lhs: Box::new(lhs?),

277

6252

                rhs: Box::new(rhs?),

278

}),

279

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

280

3222

                op: ProcExprBinaryOp::Parallel,

281

3222

                lhs: Box::new(lhs?),

282

3222

                rhs: Box::new(rhs?),

283

}),

284

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

285

                op: ProcExprBinaryOp::LeftMerge,

286

                lhs: Box::new(lhs?),

287

                rhs: Box::new(rhs?),

288

}),

289

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

290

16038

                op: ProcExprBinaryOp::Sequence,

291

16038

                lhs: Box::new(lhs?),

292

16038

                rhs: Box::new(rhs?),

293

}),

294

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

295

2442

                op: ProcExprBinaryOp::CommMerge,

296

2442

                lhs: Box::new(lhs?),

297

2442

                rhs: Box::new(rhs?),

298

}),

299

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

300

27954

})

301

19872

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

302

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

303

5688

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

304

5688

                operand: Box::new(expr?),

305

}),

306

            Rule::ProcExprDist => {

307

156

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

308

309

                Ok(ProcessExpr::Dist {

310

156

                    variables,

311

156

                    expr: data_expr,

312

156

                    operand: Box::new(expr?),

313

})

314

315

            Rule::ProcExprIf => {

316

5646

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

317

318

                Ok(ProcessExpr::Condition {

319

5646

                    condition,

320

5646

                    then: Box::new(expr?),

321

5646

                    else_: None,

322

})

323

324

            Rule::ProcExprIfThen => {

325

3402

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

326

327

                Ok(ProcessExpr::Condition {

328

3402

                    condition,

329

3402

                    then: Box::new(then),

330

3402

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

331

})

332

333

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

334

14892

})

335

19872

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

336

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

337

84

                expr: Box::new(expr?),

338

84

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

339

}),

340

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

341

84

})

342

19872

        .parse(pairs)

343

19872

344

345

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

346

901

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

347

    // Precedence is defined lowest to highest

348

901

    PrattParser::new()

349

901

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

350

901

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

351

901

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

352

901

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

353

901

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

354

901

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

355

901

});

356

357

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

358

#[allow(clippy::result_large_err)]

359

5929

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

360

5929

    ACTFRM_PRATT_PARSER

361

6691

        .map_primary(|primary| {

362

6691

            match primary.as_rule() {

363

738

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

364

6

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

365

5101

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

366

126

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

367

                Rule::ActFrmBrackets => {

368

                    // Handle parentheses by recursively parsing the inner expression

369

720

                    let inner = primary

370

720

                        .into_inner()

371

720

                        .next()

372

720

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

373

720

                    parse_actfrm(inner.into_inner())

374

375

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

376

377

6691

})

378

5929

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

379

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

380

780

                quantifier: Quantifier::Exists,

381

780

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

382

780

                body: Box::new(expr?),

383

}),

384

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

385

24

                quantifier: Quantifier::Forall,

386

24

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

387

24

                body: Box::new(expr?),

388

}),

389

930

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

390

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

391

1734

})

392

5929

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

393

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

394

450

                op: ActFrmBinaryOp::Union,

395

450

                lhs: Box::new(lhs?),

396

450

                rhs: Box::new(rhs?),

397

}),

398

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

399

300

                op: ActFrmBinaryOp::Intersect,

400

300

                lhs: Box::new(lhs?),

401

300

                rhs: Box::new(rhs?),

402

}),

403

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

404

12

                op: ActFrmBinaryOp::Implies,

405

12

                lhs: Box::new(lhs?),

406

12

                rhs: Box::new(rhs?),

407

}),

408

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

409

762

})

410

5929

        .parse(pairs)

411

5929

412

413

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

414

901

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

415

    // Precedence is defined lowest to highest

416

901

    PrattParser::new()

417

901

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

418

901

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

419

901

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

420

901

});

421

422

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

423

#[allow(clippy::result_large_err)]

424

4537

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

425

4537

    REGFRM_PRATT_PARSER

426

5221

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

427

5209

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

428

            Rule::RegFrmBackets => {

429

                // Handle parentheses by recursively parsing the inner expression

430

12

                let inner = primary

431

12

                    .into_inner()

432

12

                    .next()

433

12

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

434

12

                parse_regfrm(inner.into_inner())

435

436

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

437

5221

})

438

4537

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

439

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

440

30

                lhs: Box::new(lhs?),

441

30

                rhs: Box::new(rhs?),

442

}),

443

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

444

654

                lhs: Box::new(lhs?),

445

654

                rhs: Box::new(rhs?),

446

}),

447

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

448

684

})

449

4537

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

450

804

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

451

6

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

452

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

453

810

})

454

4537

        .parse(pairs)

455

4537

456

457

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

458

901

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

459

    // Precedence is defined lowest to highest

460

901

    PrattParser::new()

461

901

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

462

901

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

463

901

            | Op::prefix(Rule::StateFrmExists)

464

901

            | Op::prefix(Rule::StateFrmInf)

465

901

            | Op::prefix(Rule::StateFrmSup)

466

901

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

467

901

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

468

901

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

469

901

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

470

901

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

471

901

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

472

901

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

473

901

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

474

901

});

475

476

#[allow(clippy::result_large_err)]

477

6667

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

478

6667

    STATEFRM_PRATT_PARSER

479

12957

        .map_primary(|primary| {

480

12957

            match primary.as_rule() {

481

6387

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

482

588

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

483

216

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

484

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

485

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

486

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

487

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

488

                Rule::StateFrmBrackets => {

489

                    // Handle parentheses by recursively parsing the inner expression

490

5766

                    let inner = primary

491

5766

                        .into_inner()

492

5766

                        .next()

493

5766

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

494

5766

                    parse_statefrm(inner.into_inner())

495

496

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

497

498

12957

})

499

7449

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

500

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

501

12

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

502

12

                Box::new(expr?),

503

)),

504

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

505

1740

                operator: ModalityOperator::Diamond,

506

1740

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

507

1740

                expr: Box::new(expr?),

508

}),

509

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

510

2785

                operator: ModalityOperator::Box,

511

2785

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

512

2785

                expr: Box::new(expr?),

513

}),

514

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

515

546

                quantifier: Quantifier::Exists,

516

546

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

517

546

                body: Box::new(expr?),

518

}),

519

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

520

1044

                quantifier: Quantifier::Forall,

521

1044

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

522

1044

                body: Box::new(expr?),

523

}),

524

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

525

554

                operator: FixedPointOperator::Least,

526

554

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

527

554

                body: Box::new(expr?),

528

}),

529

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

530

672

                operator: FixedPointOperator::Greatest,

531

672

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

532

672

                body: Box::new(expr?),

533

}),

534

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

535

90

                op: StateFrmUnaryOp::Negation,

536

90

                expr: Box::new(expr?),

537

}),

538

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

539

                bound: Bound::Sup,

540

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

541

                body: Box::new(expr?),

542

}),

543

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

544

                bound: Bound::Sup,

545

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

546

                body: Box::new(expr?),

547

}),

548

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

549

6

                bound: Bound::Sup,

550

6

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

551

6

                body: Box::new(expr?),

552

}),

553

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

554

7449

})

555

6668

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

556

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

557

6

                op: StateFrmOp::Addition,

558

6

                lhs: Box::new(lhs?),

559

6

                rhs: Box::new(rhs?),

560

}),

561

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

562

1542

                op: StateFrmOp::Implies,

563

1542

                lhs: Box::new(lhs?),

564

1542

                rhs: Box::new(rhs?),

565

}),

566

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

567

1170

                op: StateFrmOp::Disjunction,

568

1170

                lhs: Box::new(lhs?),

569

1170

                rhs: Box::new(rhs?),

570

}),

571

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

572

3572

                op: StateFrmOp::Conjunction,

573

3572

                lhs: Box::new(lhs?),

574

3572

                rhs: Box::new(rhs?),

575

}),

576

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

577

6290

})

578

6667

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

579

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

580

                Box::new(expr?),

581

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

582

)),

583

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

584

})

585

6667

        .parse(pairs)

586

6667

587

588

18

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

589

    // Precedence is defined lowest to highest

590

18

    PrattParser::new()

591

18

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

592

18

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

593

18

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

594

18

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

595

18

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

596

18

});

597

598

#[allow(clippy::result_large_err)]

599

30

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

600

30

    PBESEXPR_PRATT_PARSER

601

42

        .map_primary(|primary| {

602

42

            match primary.as_rule() {

603

12

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

604

                Rule::PbesExprParens => {

605

                    // Handle parentheses by recursively parsing the inner expression

606

                    let inner = primary

607

                        .into_inner()

608

                        .next()

609

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

610

                    parse_pbesexpr(inner.into_inner())

611

612

6

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

613

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

614

24

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

615

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

616

617

42

})

618

30

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

619

6

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

620

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

621

6

})

622

30

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

623

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

624

12

                op: PbesExprBinaryOp::Conjunction,

625

12

                lhs: Box::new(lhs?),

626

12

                rhs: Box::new(rhs?),

627

}),

628

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

629

                op: PbesExprBinaryOp::Disjunction,

630

                lhs: Box::new(lhs?),

631

                rhs: Box::new(rhs?),

632

}),

633

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

634

                op: PbesExprBinaryOp::Implies,

635

                lhs: Box::new(lhs?),

636

                rhs: Box::new(rhs?),

637

}),

638

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

639

12

})

640

30

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

641

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

642

                quantifier: Quantifier::Exists,

643

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

644

                body: Box::new(expr?),

645

}),

646

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

647

                quantifier: Quantifier::Forall,

648

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

649

                body: Box::new(expr?),

650

}),

651

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

652

})

653

30

        .parse(pairs)

654

30

655

656

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

657

    // Precedence is defined lowest to highest

658

    PrattParser::new()

659

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

660

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

661

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

662

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

663

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

664

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

665

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

666

});

667

668

#[allow(clippy::result_large_err)]

669

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

670

    PRESEXPR_PRATT_PARSER

671

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

672

            Rule::PresExprParens => {

673

                // Handle parentheses by recursively parsing the inner expression

674

                let inner = primary

675

                    .into_inner()

676

                    .next()

677

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

678

                parse_presexpr(inner.into_inner())

679

680

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

681

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

682

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

683

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

684

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

685

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

686

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

687

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

688

})

689

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

690

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

691

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

692

                op: Bound::Inf,

693

                expr: Box::new(expr?),

694

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

695

}),

696

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

697

                op: Bound::Sup,

698

                expr: Box::new(expr?),

699

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

700

}),

701

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

702

                op: Bound::Sum,

703

                expr: Box::new(expr?),

704

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

705

}),

706

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

707

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

708

                expr: Box::new(expr?),

709

}),

710

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

711

})

712

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

713

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

714

                op: PresExprBinaryOp::Implies,

715

                lhs: Box::new(lhs?),

716

                rhs: Box::new(rhs?),

717

}),

718

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

719

                op: PresExprBinaryOp::Disjunction,

720

                lhs: Box::new(lhs?),

721

                rhs: Box::new(rhs?),

722

}),

723

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

724

                op: PresExprBinaryOp::Conjunction,

725

                lhs: Box::new(lhs?),

726

                rhs: Box::new(rhs?),

727

}),

728

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

729

                op: PresExprBinaryOp::Add,

730

                lhs: Box::new(lhs?),

731

                rhs: Box::new(rhs?),

732

}),

733

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

734

})

735

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

736

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

737

                expr: Box::new(expr?),

738

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

739

}),

740

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

741

})

742

        .parse(pairs)

743