Grcov report - data_expression.rs

1

use std::fmt;

2

use std::ops::Deref;

3

4

use ahash::AHashSet;

5

use delegate::delegate;

6

7

use merc_aterm::ATerm;

8

use merc_aterm::ATermArgs;

9

use merc_aterm::ATermIndex;

10

use merc_aterm::ATermRef;

11

use merc_aterm::ATermString;

12

use merc_aterm::Markable;

13

use merc_aterm::Symb;

14

use merc_aterm::SymbolRef;

15

use merc_aterm::Term;

16

use merc_aterm::TermBuilder;

17

use merc_aterm::TermIterator;

18

use merc_aterm::Transmutable;

19

use merc_aterm::Yield;

20

use merc_aterm::storage::Marker;

21

use merc_aterm::storage::THREAD_TERM_POOL;

22

use merc_macros::merc_derive_terms;

23

use merc_macros::merc_ignore;

24

use merc_macros::merc_term;

25

26

use crate::DATA_SYMBOLS;

27

use crate::SortExpression;

28

use crate::SortExpressionRef;

29

use crate::is_data_application;

30

use crate::is_data_expression;

31

use crate::is_data_function_symbol;

32

use crate::is_data_machine_number;

33

use crate::is_data_variable;

34

35

// This module is only used internally to run the proc macro.

36

#[merc_derive_terms]

37

mod inner {

38

39

    use std::iter;

40

41

    use merc_aterm::ATermStringRef;

42

    use merc_utilities::MercError;

43

44

    use super::*;

45

46

    /// A data expression is an [merc_aterm::ATerm] with additional structure.

47

///

48

    /// # Details

49

///

50

    /// A data expression can be any of:

51

    ///     - a variable

52

    ///     - a function symbol, i.e. f without arguments.

53

    ///     - a term applied to a number of arguments, i.e., t_0(t1, ..., tn).

54

    ///     - an abstraction lambda x: Sort . e, or forall and exists.

55

    ///     - machine number, a value [0, ..., 2^64-1].

56

///

57

    /// Not supported:

58

    ///     - a where clause "e where [x := f, ...]"

59

    ///     - set enumeration

60

    ///     - bag enumeration

61

///

62

    #[merc_term(is_data_expression)]

63

    pub struct DataExpression {

64

        term: ATerm,

65

66

67

    impl DataExpression {

68

        /// Returns the head symbol a data expression

69

        ///     - function symbol                  f -> f

70

        ///     - application       f(t_0, ..., t_n) -> f

71

161109434

        pub fn data_function_symbol(&self) -> DataFunctionSymbolRef<'_> {

72

161109434

            if is_data_application(&self.term) {

73

132275417

                self.term.arg(0).into()

74

28834017

            } else if is_data_function_symbol(&self.term) {

75

28834017

                self.term.copy().into()

76

            } else {

77

                // This can only happen if the term is an incorrect data expression.

78

                panic!("data_function_symbol not implemented for {self}");

79

80

161109434

81

82

        /// Returns the arguments of a data expression

83

        ///     - function symbol                  f -> []

84

        ///     - application       f(t_0, ..., t_n) -> [t_0, ..., t_n]

85

        #[merc_ignore]

86

607369

        pub fn data_arguments(&self) -> impl ExactSizeIterator<Item = DataExpressionRef<'_>> + use<'_> {

87

607369

            let mut result = self.term.arguments();

88

607369

            if is_data_application(&self.term) {

89

527937

                result.next();

90

527937

            } else if is_data_function_symbol(&self.term) || is_data_variable(&self.term) {

91

79432

                result.next();

92

79432

                result.next();

93

79432

            } else {

94

                // This can only happen if the term is an incorrect data expression.

95

                panic!("data_arguments not implemented for {self}");

96

97

98

635397

            result.map(|t| t.into())

99

607369

100

101

        /// Creates a closed [DataExpression] from a string, i.e., has no free variables.

102

        #[merc_ignore]

103

81

        pub fn from_string(text: &str) -> Result<DataExpression, MercError> {

104

81

            Ok(to_untyped_data_expression(ATerm::from_string(text)?, None))

105

81

106

107

        /// Creates a [DataExpression] from a string with free untyped variables indicated by the set of names.

108

        #[merc_ignore]

109

24

        pub fn from_string_untyped(text: &str, variables: &AHashSet<String>) -> Result<DataExpression, MercError> {

110

24

            Ok(to_untyped_data_expression(ATerm::from_string(text)?, Some(variables)))

111

24

112

113

        /// Returns the ith argument of a data application.

114

        #[merc_ignore]

115

2

        pub fn data_arg(&self, index: usize) -> DataExpressionRef<'_> {

116

2

            debug_assert!(is_data_application(self), "Term {self:?} is not a data application");

117

2

            debug_assert!(

118

2

                index + 1 < self.get_head_symbol().arity(),

119

                "data_arg({index}) is not defined for term {self:?}"

120

);

121

122

2

            self.term.arg(index + 1).into()

123

2

124

125

        /// Returns the arguments of a data expression

126

        ///     - function symbol                  f -> []

127

        ///     - application       f(t_0, ..., t_n) -> [t_0, ..., t_n]

128

        pub fn data_sort(&self) -> SortExpression {

129

            if is_data_function_symbol(&self.term) {

130

                DataFunctionSymbolRef::from(self.term.copy()).sort().protect()

131

            } else if is_data_variable(&self.term) {

132

                DataVariableRef::from(self.term.copy()).sort().protect()

133

            } else {

134

                panic!("data_sort not implemented for {self}");

135

136

137

138

139

    impl fmt::Display for DataExpression {

140

1

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

141

1

            if is_data_function_symbol(&self.term) {

142

1

                write!(f, "{}", DataFunctionSymbolRef::from(self.term.copy()))

143

            } else if is_data_application(&self.term) {

144

                write!(f, "{}", DataApplicationRef::from(self.term.copy()))

145

            } else if is_data_variable(&self.term) {

146

                write!(f, "{}", DataVariableRef::from(self.term.copy()))

147

            } else if is_data_machine_number(&self.term) {

148

                write!(f, "{}", MachineNumberRef::from(self.term.copy()))

149

            } else {

150

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

151

152

1

153

154

155

    #[merc_term(is_data_function_symbol)]

156

    pub struct DataFunctionSymbol {

157

        term: ATerm,

158

159

160

    impl DataFunctionSymbol {

161

        #[merc_ignore]

162

66659

        pub fn new(name: impl Into<String> + AsRef<str>) -> DataFunctionSymbol {

163

66659

            DATA_SYMBOLS.with_borrow(|ds| DataFunctionSymbol {

164

66659

                term: ATerm::with_args(

165

66659

                    ds.data_function_symbol.deref(),

166

66659

&[

167

66659

                        Into::<ATerm>::into(ATermString::new(name)),

168

66659

                        SortExpression::unknown_sort().into(),

169

66659

],

170

66659

171

66659

                .protect(),

172

66659

})

173

66659

174

175

        /// Returns the name of the function symbol

176

5

        pub fn name(&self) -> ATermStringRef<'_> {

177

5

            ATermStringRef::from(self.term.arg(0))

178

5

179

180

        /// Returns the sort of the function symbol.

181

        pub fn sort(&self) -> SortExpressionRef<'_> {

182

            self.term.arg(1).into()

183

184

185

        /// Returns the internal operation id (a unique number) for the data::function_symbol.

186

102007592

        pub fn operation_id(&self) -> usize {

187

102007592

            self.term.index()

188

102007592

189

190

191

    impl fmt::Display for DataFunctionSymbol {

192

3

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

193

3

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

194

3

195

196

197

    #[merc_term(is_data_variable)]

198

    pub struct DataVariable {

199

        term: ATerm,

200

201

202

    impl DataVariable {

203

        /// Create a new untyped variable with the given name.

204

        #[merc_ignore]

205

17656

        pub fn new(name: impl Into<ATermString>) -> DataVariable {

206

17656

            DATA_SYMBOLS.with_borrow(|ds| {

207

                // TODO: Storing terms temporarily is not optimal.

208

17656

                let t = name.into();

209

17656

                let args: &[ATerm] = &[t.into(), SortExpression::unknown_sort().into()];

210

211

17656

                DataVariable {

212

17656

                    term: ATerm::with_args(ds.data_variable.deref(), args).protect(),

213

17656

214

17656

})

215

17656

216

217

        /// Create a variable with the given sort and name.

218

        pub fn with_sort(name: impl Into<ATermString>, sort: SortExpressionRef<'_>) -> DataVariable {

219

            DATA_SYMBOLS.with_borrow(|ds| {

220

                // TODO: Storing terms temporarily is not optimal.

221

                let t = name.into();

222

                let args: &[ATermRef<'_>] = &[t.copy().into(), sort.into()];

223

224

                DataVariable {

225

                    term: ATerm::with_args(ds.data_variable.deref(), args).protect(),

226

227

})

228

229

230

        /// Returns the name of the variable.

231

2552

        pub fn name(&self) -> &str {

232

            // We only change the lifetime, but that is fine since it is derived from the current term.

233

2552

            self.term.arg(0).get_head_symbol().name()

234

2552

235

236

        /// Returns the sort of the variable.

237

        pub fn sort(&self) -> SortExpressionRef<'_> {

238

            self.term.arg(1).into()

239

240

241

242

    impl fmt::Display for DataVariable {

243

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

244

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

245

246

247

248

    #[merc_term(is_data_application)]

249

    pub struct DataApplication {

250

        term: ATerm,

251

252

253

    impl DataApplication {

254

        /// Create a new data application with the given head and arguments.

255

        #[merc_ignore]

256

1090

        pub fn with_args<'a, 'b>(head: &'b impl Term<'a, 'b>, arguments: &'b [impl Term<'a, 'b>]) -> DataApplication {

257

1090

            DATA_SYMBOLS.with_borrow_mut(|ds| {

258

1090

                let symbol = ds.get_data_application_symbol(arguments.len() + 1).copy();

259

260

1973

                let args = iter::once(head.copy()).chain(arguments.iter().map(|t| t.copy()));

261

1090

                let term = ATerm::with_iter(&symbol, args);

262

263

1090

                DataApplication { term }

264

1090

})

265

1090

266

267

        /// Create a new data application with the given head and arguments.

268

///

269

        /// arity must be equal to the number of arguments + 1.

270

        #[merc_ignore]

271

4324541

        pub fn with_iter<'a, 'b, 'c, 'd, T, I>(

272

4324541

            head: &'b impl Term<'a, 'b>,

273

4324541

            arity: usize,

274

4324541

            arguments: I,

275

4324541

        ) -> DataApplication

276

4324541

        where

277

4324541

            I: Iterator<Item = T>,

278

4324541

            T: Term<'c, 'd>,

279

280

4324541

            DATA_SYMBOLS.with_borrow_mut(|ds| {

281

4324541

                let symbol = ds.get_data_application_symbol(arity + 1).copy();

282

283

4324541

                let term = ATerm::with_iter_head(&symbol, head, arguments);

284

285

4324541

                DataApplication { term }

286

4324541

})

287

4324541

288

289

        /// Returns the head symbol a data application

290

1

        pub fn data_function_symbol(&self) -> DataFunctionSymbolRef<'_> {

291

1

            self.term.arg(0).into()

292

1

293

294

        /// Returns the arguments of a data application

295

2

        pub fn data_arguments(&self) -> ATermArgs<'_> {

296

2

            let mut result = self.term.arguments();

297

2

            result.next();

298

2

            result

299

2

300

301

        /// Returns the ith argument of a data application.

302

        pub fn data_arg(&self, index: usize) -> DataExpressionRef<'_> {

303

            debug_assert!(

304

                index + 1 < self.get_head_symbol().arity(),

305

                "data_arg({index}) is not defined for term {self:?}"

306

);

307

308

            self.term.arg(index + 1).into()

309

310

311

        /// Returns the sort of a data application.

312

        pub fn sort(&self) -> SortExpressionRef<'_> {

313

            // We only change the lifetime, but that is fine since it is derived from the current term.

314

            SortExpressionRef::from(self.term.arg(0))

315

316

317

318

    impl fmt::Display for DataApplication {

319

1

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

320

1

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

321

322

1

            let mut first = true;

323

1

            for arg in self.data_arguments() {

324

1

                if !first {

325

                    write!(f, ", ")?;

326

                } else {

327

1

                    write!(f, "(")?;

328

329

330

1

                write!(f, "{}", DataExpressionRef::from(arg.copy()))?;

331

1

                first = false;

332

333

334

1

            if !first {

335

1

                write!(f, ")")?;

336

337

338

1

            Ok(())

339

1

340

341

342

    #[merc_term(is_data_machine_number)]

343

    struct MachineNumber {

344

        pub term: ATerm,

345

346

347

    impl MachineNumber {

348

        /// Obtain the underlying value of a machine number.

349

        pub fn value(&self) -> u64 {

350

            self.term

351

                .copy()

352

                .annotation()

353

                .expect("MachineNumber must have an integer annotation") as u64

354

355

356

357

    impl fmt::Display for MachineNumber {

358

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

359

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

360

361

362

363

    /// Conversions to `DataExpression`

364

    #[merc_ignore]

365

    impl From<DataFunctionSymbol> for DataExpression {

366

7606536

        fn from(value: DataFunctionSymbol) -> Self {

367

7606536

            value.term.into()

368

7606536

369

370

371

    #[merc_ignore]

372

    impl From<DataApplication> for DataExpression {

373

34234449

        fn from(value: DataApplication) -> Self {

374

34234449

            value.term.into()

375

34234449

376

377

378

    #[merc_ignore]

379

    impl From<DataVariable> for DataExpression {

380

2400

        fn from(value: DataVariable) -> Self {

381

2400

            value.term.into()

382

2400

383

384

385

    #[merc_ignore]

386

    impl From<DataExpression> for DataFunctionSymbol {

387

20000

        fn from(value: DataExpression) -> Self {

388

20000

            value.term.into()

389

20000

390

391

392

    #[merc_ignore]

393

    impl From<DataExpression> for DataVariable {

394

230768

        fn from(value: DataExpression) -> Self {

395

230768

            value.term.into()

396

230768

397

398

399

    #[merc_ignore]

400

    impl<'a> From<DataExpressionRef<'a>> for DataVariableRef<'a> {

401

287440

        fn from(value: DataExpressionRef<'a>) -> Self {

402

287440

            value.term.into()

403

287440

404

405

406

407

pub use inner::*;

408

409

impl<'a> DataExpressionRef<'a> {

410

20140264

    pub fn data_arguments(&self) -> impl ExactSizeIterator<Item = DataExpressionRef<'a>> + use<'a> {

411

20140264

        let mut result = self.term.arguments();

412

20140264

        if is_data_application(&self.term) {

413

15488040

            result.next();

414

15488040

        } else if is_data_function_symbol(&self.term) || is_data_variable(&self.term) {

415

4652224

            result.next();

416

4652224

            result.next();

417

4652224

        } else {

418

            // This can only happen if the term is not a data expression.

419

            panic!("data_arguments not implemented for {self}");

420

421

422

20140264

        result.map(|t| t.into())

423

20140264

424

425

    /// Returns the ith argument of a data application.

426

130956697

    pub fn data_arg(&self, index: usize) -> DataExpressionRef<'a> {

427

130956697

        debug_assert!(is_data_application(self), "Term {self:?} is not a data application");

428

130956697

        debug_assert!(

429

130956697

            index + 1 < self.get_head_symbol().arity(),

430

            "data_arg({index}) is not defined for term {self:?}"

431

);

432

433

130956697

        self.term.arg(index + 1).into()

434

130956697

435

436

437

/// Converts an [ATerm] to an untyped data expression.

438

15289

pub fn to_untyped_data_expression(t: ATerm, variables: Option<&AHashSet<String>>) -> DataExpression {

439

15289

    let mut builder = TermBuilder::<ATerm, ATerm>::new();

440

15289

    THREAD_TERM_POOL.with_borrow(|tp| {

441

15289

        builder

442

15289

            .evaluate(

443

15289

tp,

444

15289

t,

445

81853

                |_tp, args, t| {

446

81853

                    if variables.is_some_and(|v| v.contains(t.get_head_symbol().name())) {

447

                        // Convert a constant variable, for example 'x', into an untyped variable.

448

15224

                        Ok(Yield::Term(DataVariable::new(t.get_head_symbol().name()).into()))

449

66629

                    } else if t.get_head_symbol().arity() == 0 {

450

20307

                        Ok(Yield::Term(DataFunctionSymbol::new(t.get_head_symbol().name()).into()))

451

                    } else {

452

                        // This is a function symbol applied to a number of arguments

453

46322

                        let head = DataFunctionSymbol::new(t.get_head_symbol().name());

454

455

66564

                        for arg in t.arguments() {

456

66564

                            args.push(arg.protect());

457

66564

458

459

46322

                        Ok(Yield::Construct(head.into()))

460

461

81853

},

462

46322

                |_tp, input, args| {

463

46322

                    let arity = args.clone().count();

464

46322

                    Ok(DataApplication::with_iter(&input, arity, args).into())

465

46322

},

466

467

15289

            .unwrap()

468

15289

            .into()

469

15289

})

470

15289

471

472

#[cfg(test)]

473

mod tests {

474

    use super::*;

475

476

    use merc_aterm::ATerm;

477

478

    #[test]

479

1

    fn test_print() {

480

1

        let _ = merc_utilities::test_logger();

481

482

1

        let a = DataFunctionSymbol::new("a");

483

1

        assert_eq!("a", format!("{}", a));

484

485

        // Check printing of data applications.

486

1

        let f = DataFunctionSymbol::new("f");

487

1

        let appl = DataApplication::with_args(&f, &[a]);

488

1

        assert_eq!("f(a)", format!("{}", appl));

489

1

490

491

    #[test]

492

1

    fn test_recognizers() {

493

1

        let a = DataFunctionSymbol::new("a");

494

1

        let f = DataFunctionSymbol::new("f");

495

1

        let appl = DataApplication::with_args(&f, &[a]);

496

497

1

        let term: ATerm = appl.into();

498

1

        assert!(is_data_application(&term));

499

1

500

501

    #[test]

502

1

    fn test_data_arguments() {

503

1

        let a = DataFunctionSymbol::new("a");

504

1

        let f = DataFunctionSymbol::new("f");

505

1

        let appl = DataApplication::with_args(&f, &[a]);

506

507

1

        assert_eq!(appl.data_arguments().count(), 1);

508

509

1

        let data_expr: DataExpression = appl.clone().into();

510

511

1

        assert_eq!(data_expr.data_arguments().count(), 1);

512

1

513

514

    #[test]

515

1

    fn test_to_data_expression() {

516

1

        let expression = DataExpression::from_string("s(s(a, b), c)").unwrap();

517

518

1

        assert_eq!(expression.data_arg(0).data_function_symbol().name(), "s");

519

1

        assert_eq!(expression.data_arg(0).data_arg(0).data_function_symbol().name(), "a");

520

1

521