Grcov report - syntax_tree

1

use std::fmt;

2

3

use itertools::Itertools;

4

5

use crate::ActDecl;

6

use crate::ActFrm;

7

use crate::ActFrmBinaryOp;

8

use crate::Action;

9

use crate::Assignment;

10

use crate::Bound;

11

use crate::CommExpr;

12

use crate::ComplexSort;

13

use crate::ConstructorDecl;

14

use crate::DataExpr;

15

use crate::DataExprBinaryOp;

16

use crate::DataExprUnaryOp;

17

use crate::DataExprUpdate;

18

use crate::EqnDecl;

19

use crate::EqnSpec;

20

use crate::FixedPointOperator;

21

use crate::IdDecl;

22

use crate::ModalityOperator;

23

use crate::MultiAction;

24

use crate::MultiActionLabel;

25

use crate::PbesEquation;

26

use crate::PbesExpr;

27

use crate::PbesExprBinaryOp;

28

use crate::ProcDecl;

29

use crate::ProcExprBinaryOp;

30

use crate::ProcessExpr;

31

use crate::PropVarDecl;

32

use crate::PropVarInst;

33

use crate::Quantifier;

34

use crate::RegFrm;

35

use crate::Rename;

36

use crate::Sort;

37

use crate::SortDecl;

38

use crate::SortExpression;

39

use crate::Span;

40

use crate::StateFrm;

41

use crate::StateFrmOp;

42

use crate::StateFrmUnaryOp;

43

use crate::StateVarAssignment;

44

use crate::StateVarDecl;

45

use crate::UntypedDataSpecification;

46

use crate::UntypedPbes;

47

use crate::UntypedProcessSpecification;

48

use crate::UntypedStateFrmSpec;

49

50

/// Returns the 1-based `(line, column)` of the byte offset `span.start` within `input`.

51

///

52

/// Counts the bytes consumed by each preceding line (including its newline) until

53

/// the offset falls inside the current line. Offsets past the end of the input

54

/// resolve to the position just after the last character.

55

50

pub fn line_column(input: &str, span: &Span) -> (usize, usize) {

56

50

    let mut consumed = 0;

57

70

    for (number, line) in input.lines().enumerate() {

58

        // `+ 1` accounts for the newline that `lines()` strips.

59

70

        let line_bytes = line.len() + 1;

60

70

        if span.start < consumed + line_bytes {

61

40

            return (number + 1, span.start - consumed + 1);

62

30

63

30

        consumed += line_bytes;

64

65

66

    // The offset is at (or past) the end of the input.

67

10

    let last_line = input.lines().count().max(1);

68

10

    (last_line, span.start.saturating_sub(consumed) + 1)

69

50

70

71

// Display implementations

72

impl fmt::Display for Sort {

73

163550

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

74

163550

        write!(f, "{self:?}")

75

163550

76

77

78

impl fmt::Display for ComplexSort {

79

33610

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

80

33610

        write!(f, "{self:?}")

81

33610

82

83

84

impl fmt::Display for Assignment {

85

41370

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

86

41370

        write!(f, "{} = {}", self.identifier, self.expr)

87

41370

88

89

90

impl fmt::Display for UntypedProcessSpecification {

91

9070

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

92

9070

        writeln!(f, "{}", self.data_specification)?;

93

94

9070

        if !self.action_declarations.is_empty() {

95

8720

            writeln!(f, "act")?;

96

73800

            for act_decl in &self.action_declarations {

97

73800

                writeln!(f, "   {act_decl};")?;

98

99

100

8720

            writeln!(f)?;

101

350

102

103

9070

        if !self.process_declarations.is_empty() {

104

8710

            writeln!(f, "proc")?;

105

35180

            for proc_decl in &self.process_declarations {

106

35180

                writeln!(f, "   {proc_decl};")?;

107

108

109

8710

            writeln!(f)?;

110

360

111

112

9070

        if !self.global_variables.is_empty() {

113

30

            writeln!(f, "glob")?;

114

30

            for var_decl in &self.global_variables {

115

30

                writeln!(f, "   {var_decl};")?;

116

117

118

30

            writeln!(f)?;

119

9040

120

121

9070

        if let Some(init) = &self.init {

122

9040

            writeln!(f, "init {init};")?;

123

30

124

9070

        Ok(())

125

9070

126

127

128

impl fmt::Display for UntypedDataSpecification {

129

18130

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

130

18130

        if !self.sort_declarations.is_empty() {

131

5790

            writeln!(f, "sort")?;

132

25590

            for decl in &self.sort_declarations {

133

25590

                writeln!(f, "   {decl};")?;

134

135

136

5790

            writeln!(f)?;

137

12340

138

139

18130

        if !self.constructor_declarations.is_empty() {

140

90

            writeln!(f, "cons")?;

141

170

            for decl in &self.constructor_declarations {

142

170

                writeln!(f, "   {decl};")?;

143

144

145

90

            writeln!(f)?;

146

18040

147

148

18130

        if !self.map_declarations.is_empty() {

149

6470

            writeln!(f, "map")?;

150

207950

            for decl in &self.map_declarations {

151

207950

                writeln!(f, "   {decl};")?;

152

153

154

6470

            writeln!(f)?;

155

11660

156

157

18770

        for decl in &self.equation_declarations {

158

18770

            writeln!(f, "{decl}")?;

159

160

18130

        Ok(())

161

18130

162

163

164

impl fmt::Display for UntypedPbes {

165

2090

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

166

2090

        writeln!(f, "{}", self.data_specification)?;

167

2090

        writeln!(f)?;

168

2090

        if !self.global_variables.is_empty() {

169

            writeln!(f, "glob")?;

170

            for var_decl in &self.global_variables {

171

                writeln!(f, "   {var_decl};")?;

172

173

174

            writeln!(f)?;

175

2090

176

2090

        writeln!(f)?;

177

178

2090

        if !self.equations.is_empty() {

179

2090

            writeln!(f, "pbes")?;

180

6150

            for equation in &self.equations {

181

6150

                writeln!(f, "   {equation};")?;

182

183

184

185

2090

        writeln!(f, "init {};", self.init)

186

2090

187

188

189

impl fmt::Display for PropVarInst {

190

26890

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

191

26890

        if self.arguments.is_empty() {

192

10200

            write!(f, "{}", self.identifier)

193

        } else {

194

16690

            write!(f, "{}({})", self.identifier, self.arguments.iter().format(", "))

195

196

26890

197

198

199

impl fmt::Display for PbesEquation {

200

6150

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

201

6150

        write!(f, "{} {} = {}", self.operator, self.variable, self.formula)

202

6150

203

204

205

impl fmt::Display for PropVarDecl {

206

6150

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

207

6150

        if self.parameters.is_empty() {

208

2290

            write!(f, "{}", self.identifier)

209

        } else {

210

3860

            write!(f, "{}({})", self.identifier, self.parameters.iter().format(", "))

211

212

6150

213

214

215

impl fmt::Display for PbesExpr {

216

135060

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

217

135060

        match self {

218

30

            PbesExpr::True => write!(f, "true"),

219

            PbesExpr::False => write!(f, "false"),

220

24800

            PbesExpr::PropVarInst(instance) => write!(f, "{instance}"),

221

26630

            PbesExpr::Negation(expr) => write!(f, "(! {expr})"),

222

48300

            PbesExpr::Binary { op, lhs, rhs } => write!(f, "({lhs} {op} {rhs})"),

223

            PbesExpr::Quantifier {

224

5680

                quantifier,

225

5680

                variables,

226

5680

                body,

227

5680

            } => write!(f, "({} {} . {})", quantifier, variables.iter().format(", "), body),

228

29620

            PbesExpr::DataValExpr(data_expr) => write!(f, "val({data_expr})"),

229

230

135060

231

232

233

impl fmt::Display for PbesExprBinaryOp {

234

48300

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

235

48300

        match self {

236

17000

            PbesExprBinaryOp::Conjunction => write!(f, "&&"),

237

13680

            PbesExprBinaryOp::Disjunction => write!(f, "||"),

238

17620

            PbesExprBinaryOp::Implies => write!(f, "=>"),

239

240

48300

241

242

243

impl fmt::Display for EqnSpec {

244

18770

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

245

        // The grammar requires at least one declaration after `var`, so only

246

        // emit the section when there are variables to declare.

247

18770

        if !self.variables.is_empty() {

248

14830

            writeln!(f, "var")?;

249

91370

            for decl in &self.variables {

250

91370

                writeln!(f, "   {decl};")?;

251

252

3940

253

254

18770

        writeln!(f, "eqn")?;

255

334050

        for decl in &self.equations {

256

334050

            writeln!(f, "   {decl};")?;

257

258

18770

        Ok(())

259

18770

260

261

262

impl fmt::Display for SortDecl {

263

25590

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

264

25590

        write!(f, "{}", self.identifier)?;

265

266

25590

        if let Some(expr) = &self.expr {

267

25440

            write!(f, " = {expr}")?;

268

150

269

270

25590

        Ok(())

271

25590

272

273

274

impl fmt::Display for ActDecl {

275

73800

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

276

        // An action declaration is `id: sort # sort # ...`, matching the

277

        // `IdList ~ ":" ~ SortProduct` grammar rule.

278

73800

        if self.args.is_empty() {

279

21590

            write!(f, "{}", self.identifier)

280

        } else {

281

52210

            write!(f, "{}: {}", self.identifier, self.args.iter().format(" # "))

282

283

73800

284

285

286

impl fmt::Display for EqnDecl {

287

334050

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

288

334050

        match &self.condition {

289

22540

            Some(condition) => write!(f, "{} -> {} = {}", condition, self.lhs, self.rhs),

290

311510

            None => write!(f, "{} = {}", self.lhs, self.rhs),

291

292

334050

293

294

295

impl fmt::Display for DataExprUnaryOp {

296

16180

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

297

16180

        match self {

298

12930

            DataExprUnaryOp::Negation => write!(f, "!"),

299

1410

            DataExprUnaryOp::Minus => write!(f, "-"),

300

1840

            DataExprUnaryOp::Size => write!(f, "#"),

301

302

16180

303

304

305

impl fmt::Display for DataExpr {

306

5999260

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

307

5999260

        match self {

308

16770

            DataExpr::EmptyList => write!(f, "[]"),

309

1530

            DataExpr::EmptyBag => write!(f, "{{:}}"),

310

5480

            DataExpr::EmptySet => write!(f, "{{}}"),

311

14250

            DataExpr::List(expressions) => write!(f, "[{}]", expressions.iter().format(", ")),

312

1380

            DataExpr::Bag(expressions) => write!(

313

1380

f,

314

                "{{ {} }}",

315

1380

                expressions

316

1380

                    .iter()

317

1500

                    .format_with(", ", |e, f| f(&format_args!("{}: {}", e.expr, e.multiplicity)))

318

),

319

10440

            DataExpr::Set(expressions) => write!(f, "{{ {} }}", expressions.iter().format(", ")),

320

4083190

            DataExpr::Id(identifier) => write!(f, "{identifier}"),

321

356660

            DataExpr::Binary { op, lhs, rhs } => write!(f, "({lhs} {op} {rhs})"),

322

16180

            DataExpr::Unary { op, expr } => write!(f, "({op} {expr})"),

323

69380

            DataExpr::Bool(value) => write!(f, "{value}"),

324

1910

            DataExpr::Quantifier { op, variables, body } => {

325

1910

                write!(f, "({} {} . {})", op, variables.iter().format(", "), body)

326

327

870

            DataExpr::Lambda { variables, body } => write!(f, "(lambda {} . {})", variables.iter().format(", "), body),

328

1182270

            DataExpr::Application { function, arguments } => {

329

1182270

                if arguments.is_empty() {

330

                    write!(f, "{function}")

331

                } else {

332

1182270

                    write!(f, "{}({})", function, arguments.iter().format(", "))

333

334

335

229320

            DataExpr::Number(value) => write!(f, "{value}"),

336

8580

            DataExpr::FunctionUpdate { expr, update } => write!(f, "{expr}[{update}]"),

337

330

            DataExpr::SetBagComp { variable, predicate } => write!(f, "{{ {variable} | {predicate} }}"),

338

720

            DataExpr::Whr { expr, assignments } => write!(f, "{} whr {} end", expr, assignments.iter().format(", ")),

339

340

5999260

341

342

343

impl fmt::Display for IdDecl {

344

428370

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

345

428370

        write!(f, "{}: {}", self.identifier, self.sort)

346

428370

347

348

349

impl fmt::Display for DataExprUpdate {

350

8580

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

351

8580

        write!(f, "{} -> {}", self.expr, self.update)

352

8580

353

354

355

impl fmt::Display for SortExpression {

356

1128920

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

357

1128920

        match self {

358

147500

            SortExpression::Product { lhs, rhs } => write!(f, "({lhs} # {rhs})"),

359

106380

            SortExpression::Function { domain, range } => write!(f, "({domain} -> {range})"),

360

657280

            SortExpression::Reference(name) => write!(f, "{name}"),

361

163550

            SortExpression::Simple(sort) => write!(f, "{sort}"),

362

33610

            SortExpression::Complex(complex, inner) => write!(f, "{complex}({inner})"),

363

20600

            SortExpression::Struct { inner } => {

364

20600

                write!(f, "struct ")?;

365

20600

                write!(f, "{}", inner.iter().format(" | "))

366

367

            SortExpression::Resolved(name, _id) => write!(f, "{name}"),

368

            SortExpression::FlattenedFunction { domain, range } => {

369

                let domain = domain.iter().format(" # ");

370

                write!(f, "({domain} -> {range})")

371

372

373

1128920

374

375

376

impl fmt::Display for UntypedStateFrmSpec {

377

4310

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

378

4310

        writeln!(f, "{}", self.data_specification)?;

379

380

        // Wrap the formula in a `form ...;` section: the bare-formula grammar

381

        // alternative is only valid when no specification elements precede it.

382

4310

        writeln!(f, "form {};", self.formula)

383

4310

384

385

386

impl fmt::Display for StateFrmUnaryOp {

387

430

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

388

430

        match self {

389

            StateFrmUnaryOp::Minus => write!(f, "-"),

390

430

            StateFrmUnaryOp::Negation => write!(f, "!"),

391

392

430

393

394

395

impl fmt::Display for FixedPointOperator {

396

11990

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

397

11990

        match self {

398

6080

            FixedPointOperator::Greatest => write!(f, "nu"),

399

5910

            FixedPointOperator::Least => write!(f, "mu"),

400

401

11990

402

403

404

impl fmt::Display for StateFrm {

405

139060

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

406

        match self {

407

7570

            StateFrm::True => write!(f, "true"),

408

5190

            StateFrm::False => write!(f, "false"),

409

            StateFrm::DataValExpr(expr) => write!(f, "val({expr})"),

410

31590

            StateFrm::Id(identifier, args) => {

411

31590

                if args.is_empty() {

412

2820

                    write!(f, "{identifier}")

413

                } else {

414

28770

                    write!(f, "{}({})", identifier, args.iter().format(", "))

415

416

417

430

            StateFrm::Unary { op, expr } => write!(f, "({op} {expr})"),

418

            StateFrm::Modality {

419

46360

                operator,

420

46360

                formula,

421

46360

                expr,

422

46360

            } => match operator {

423

21000

                ModalityOperator::Box => write!(f, "[{formula}]{expr}"),

424

25360

                ModalityOperator::Diamond => write!(f, "<{formula}>{expr}"),

425

},

426

            StateFrm::Quantifier {

427

7930

                quantifier,

428

7930

                variables,

429

7930

                body,

430

            } => {

431

7930

                write!(f, "({} {} . {})", quantifier, variables.iter().format(", "), body)

432

433

            StateFrm::Bound {

434

30

                bound: quantifier,

435

30

                variables,

436

30

                body,

437

            } => {

438

30

                write!(f, "({} {} . {})", quantifier, variables.iter().format(", "), body)

439

440

34100

            StateFrm::Binary { op, lhs, rhs } => {

441

34100

                write!(f, "({lhs} {op} {rhs})")

442

443

            StateFrm::FixedPoint {

444

5800

                operator,

445

5800

                variable,

446

5800

                body,

447

            } => {

448

5800

                write!(f, "({operator} {variable} . {body})")

449

450

            StateFrm::Delay(Some(expr)) => write!(f, "delay@({expr})"),

451

            StateFrm::Delay(None) => write!(f, "delay"),

452

            StateFrm::Yaled(Some(expr)) => write!(f, "yaled@({expr})"),

453

            StateFrm::Yaled(None) => write!(f, "yaled"),

454

60

            StateFrm::DataValExprLeftMult(value, expr) => write!(f, "(val({value}) * {expr})"),

455

            StateFrm::DataValExprRightMult(expr, value) => write!(f, "({expr} * val({value}))"),

456

457

139060

458

459

460

impl fmt::Display for StateVarDecl {

461

5840

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

462

5840

        if self.arguments.is_empty() {

463

2900

            write!(f, "{}", self.identifier)

464

        } else {

465

2940

            write!(f, "{}({})", self.identifier, self.arguments.iter().format(","))

466

467

5840

468

469

470

impl fmt::Display for StateVarAssignment {

471

4020

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

472

4020

        write!(f, "{} : {} = {}", self.identifier, self.sort, self.expr)

473

4020

474

475

476

impl fmt::Display for StateFrmOp {

477

34100

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

478

34100

        match self {

479

7710

            StateFrmOp::Implies => write!(f, "=>"),

480

20510

            StateFrmOp::Conjunction => write!(f, "&&"),

481

5850

            StateFrmOp::Disjunction => write!(f, "||"),

482

30

            StateFrmOp::Addition => write!(f, "+"),

483

484

34100

485

486

487

impl fmt::Display for RegFrm {

488

69670

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

489

69670

        match self {

490

49760

            RegFrm::Action(action) => write!(f, "{action}"),

491

16500

            RegFrm::Iteration(body) => write!(f, "({body})*"),

492

10

            RegFrm::Plus(body) => write!(f, "({body})+"),

493

130

            RegFrm::Choice { lhs, rhs } => write!(f, "({lhs} + {rhs})"),

494

3270

            RegFrm::Sequence { lhs, rhs } => write!(f, "({lhs} . {rhs})"),

495

496

69670

497

498

499

impl fmt::Display for DataExprBinaryOp {

500

356660

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

501

356660

        match self {

502

28350

            DataExprBinaryOp::At => write!(f, "."),

503

1330

            DataExprBinaryOp::Concat => write!(f, "++"),

504

23750

            DataExprBinaryOp::Cons => write!(f, "|>"),

505

78410

            DataExprBinaryOp::Equal => write!(f, "=="),

506

17580

            DataExprBinaryOp::NotEqual => write!(f, "!="),

507

20890

            DataExprBinaryOp::LessThan => write!(f, "<"),

508

12700

            DataExprBinaryOp::LessEqual => write!(f, "<="),

509

11320

            DataExprBinaryOp::GreaterThan => write!(f, ">"),

510

4770

            DataExprBinaryOp::GreaterEqual => write!(f, ">="),

511

45970

            DataExprBinaryOp::Conj => write!(f, "&&"),

512

14290

            DataExprBinaryOp::Disj => write!(f, "||"),

513

45930

            DataExprBinaryOp::Add => write!(f, "+"),

514

21660

            DataExprBinaryOp::Subtract => write!(f, "-"),

515

2440

            DataExprBinaryOp::Div => write!(f, "/"),

516

1710

            DataExprBinaryOp::Implies => write!(f, "=>"),

517

14670

            DataExprBinaryOp::In => write!(f, "in"),

518

470

            DataExprBinaryOp::IntDiv => write!(f, "div"),

519

2710

            DataExprBinaryOp::Mod => write!(f, "mod"),

520

7350

            DataExprBinaryOp::Multiply => write!(f, "*"),

521

360

            DataExprBinaryOp::Snoc => write!(f, "<|"),

522

523

356660

524

525

526

impl fmt::Display for ActFrm {

527

66050

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

528

66050

        match self {

529

10

            ActFrm::False => write!(f, "false"),

530

3670

            ActFrm::True => write!(f, "true"),

531

49260

            ActFrm::MultAct(action) => write!(f, "{action}"),

532

3810

            ActFrm::Binary { op, lhs, rhs } => {

533

                // Wrap the whole expression (not just the operands) so that a

534

                // surrounding tighter operator such as `!` cannot re-associate.

535

3810

                write!(f, "({lhs} {op} {rhs})")

536

537

630

            ActFrm::DataExprVal(expr) => write!(f, "val({expr})"),

538

            ActFrm::Quantifier {

539

4020

                quantifier,

540

4020

                variables,

541

4020

                body,

542

4020

            } => write!(f, "({} {} . {})", quantifier, variables.iter().format(", "), body),

543

4650

            ActFrm::Negation(expr) => write!(f, "(!{expr})"),

544

545

66050

546

547

548

impl fmt::Display for ActFrmBinaryOp {

549

3810

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

550

3810

        match self {

551

60

            ActFrmBinaryOp::Implies => write!(f, "=>"),

552

1500

            ActFrmBinaryOp::Intersect => write!(f, "&&"),

553

2250

            ActFrmBinaryOp::Union => write!(f, "||"),

554

555

3810

556

557

558

impl fmt::Display for Bound {

559

30

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

560

30

        match self {

561

30

            Bound::Inf => write!(f, "inf"),

562

            Bound::Sum => write!(f, "sum"),

563

            Bound::Sup => write!(f, "sup"),

564

565

30

566

567

568

impl fmt::Display for MultiAction {

569

49260

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

570

49260

        if self.actions.is_empty() {

571

14330

            write!(f, "tau")

572

        } else {

573

34930

            write!(f, "{}", self.actions.iter().format("|"))

574

575

49260

576

577

578

impl fmt::Display for Action {

579

35710

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

580

35710

        if self.args.is_empty() {

581

19300

            write!(f, "{}", self.id)

582

        } else {

583

16410

            write!(f, "{}({})", self.id, self.args.iter().format(", "))

584

585

35710

586

587

588

impl fmt::Display for Quantifier {

589

19540

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

590

19540

        match self {

591

10870

            Quantifier::Exists => write!(f, "exists"),

592

8670

            Quantifier::Forall => write!(f, "forall"),

593

594

19540

595

596

597

impl fmt::Display for ConstructorDecl {

598

57540

    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {

599

57540

        if self.args.is_empty() {

600

40920

            write!(f, "{}", self.name)

601

        } else {

602

16620

            write!(f, "{}(", self.name)?;

603

35730

            for (i, (name, sort)) in self.args.iter().enumerate() {

604

35730

                if i > 0 {

605

19110

                    write!(f, ", ")?;

606

16620

607

35730

                match name {

608

13740

                    Some(name) => write!(f, "{name} : {sort}")?,

609

21990

                    None => write!(f, "{sort}")?,

610

611

612

16620

            write!(f, ")")?;

613

614

16620

            if let Some(projection) = &self.projection {

615

1500

                write!(f, "?{projection}")?;

616

15120

617

618

16620

            Ok(())

619

620

57540

621

622

623

impl fmt::Display for ProcDecl {

624

35180

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

625

35180

        if self.params.is_empty() {

626

6000

            write!(f, "{} = {}", self.identifier, self.body)

627

        } else {

628

29180

            write!(

629

29180

f,

630

                "{}({}) = {}",

631

                self.identifier,

632

29180

                self.params.iter().format(", "),

633

                self.body

634

635

636

35180

637

638

639

impl fmt::Display for ProcExprBinaryOp {

640

183500

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

641

183500

        match self {

642

101970

            ProcExprBinaryOp::Sequence => write!(f, "."),

643

49200

            ProcExprBinaryOp::Choice => write!(f, "+"),

644

20110

            ProcExprBinaryOp::Parallel => write!(f, "||"),

645

10

            ProcExprBinaryOp::LeftMerge => write!(f, "||_"),

646

12210

            ProcExprBinaryOp::CommMerge => write!(f, "|"),

647

            ProcExprBinaryOp::Until => write!(f, "<<"),

648

649

183500

650

651

652

impl fmt::Display for ProcessExpr {

653

541750

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

654

541750

        match self {

655

37950

            ProcessExpr::Id(identifier, assignments) => {

656

37950

                if assignments.is_empty() {

657

4850

                    write!(f, "{identifier}")

658

                } else {

659

33100

                    write!(f, "{}({})", identifier, assignments.iter().format(", "))

660

661

662

203780

            ProcessExpr::Action(identifier, data_exprs) => {

663

203780

                if data_exprs.is_empty() {

664

53720

                    write!(f, "{identifier}")

665

                } else {

666

150060

                    write!(f, "{}({})", identifier, data_exprs.iter().format(", "))

667

668

669

4200

            ProcessExpr::Delta => write!(f, "delta"),

670

1680

            ProcessExpr::Tau => write!(f, "tau"),

671

31220

            ProcessExpr::Sum { variables, operand } => {

672

31220

                write!(f, "(sum {} . {})", variables.iter().format(", "), operand)

673

674

            ProcessExpr::Dist {

675

780

                variables,

676

780

                expr,

677

780

                operand,

678

780

            } => write!(f, "(dist {} [{}] . {})", variables.iter().format(", "), expr, operand),

679

183500

            ProcessExpr::Binary { op, lhs, rhs } => write!(f, "({lhs} {op} {rhs})"),

680

2540

            ProcessExpr::Hide { actions, operand } => {

681

2540

                if !actions.is_empty() {

682

2540

                    write!(f, "hide({{{}}}, {})", actions.iter().format(", "), operand)

683

                } else {

684

                    Ok(())

685

686

687

1270

            ProcessExpr::Rename { renames, operand } => {

688

1270

                if !renames.is_empty() {

689

1270

                    write!(f, "rename({{{}}}, {})", renames.iter().format(", "), operand)

690

                } else {

691

                    Ok(())

692

693

694

3850

            ProcessExpr::Allow { actions, operand } => {

695

3850

                if !actions.is_empty() {

696

3850

                    write!(f, "allow({{{}}}, {})", actions.iter().format(", "), operand)

697

                } else {

698

                    Ok(())

699

700

701

1230

            ProcessExpr::Block { actions, operand } => {

702

1230

                if !actions.is_empty() {

703

1230

                    write!(f, "block({{{}}}, {})", actions.iter().format(", "), operand)

704

                } else {

705

                    Ok(())

706

707

708

4290

            ProcessExpr::Comm { comm, operand } => {

709

4290

                if !comm.is_empty() {

710

4290

                    write!(f, "comm({{{}}}, {})", comm.iter().format(", "), operand)

711

                } else {

712

                    Ok(())

713

714

715

65040

            ProcessExpr::Condition { condition, then, else_ } => {

716

                // Wrap the whole conditional so it stays a single unit when it is

717

                // an operand of a higher-precedence operator such as sequence.

718

65040

                if let Some(else_) = else_ {

719

19890

                    write!(f, "(({condition}) -> ({then}) <> ({else_}))")

720

                } else {

721

45150

                    write!(f, "(({condition}) -> ({then}))")

722

723

724

420

            ProcessExpr::At { expr, operand } => write!(f, "({expr})@({operand})"),

725

726

541750

727

728

729

impl fmt::Display for CommExpr {

730

15090

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

731

15090

        write!(f, "{} -> {}", self.from, self.to)

732

15090

733

734

735

impl fmt::Display for Rename {

736

1840

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

737

1840

        write!(f, "{} -> {}", self.from, self.to)

738

1840

739

740

741

impl fmt::Display for MultiActionLabel {

742

46800

    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

743

46800

        if self.actions.is_empty() {

744

            write!(f, "tau")

745

        } else {

746

46800

            write!(f, "{}", self.actions.iter().format("|"))

747

748

46800

749