Grcov report - parse

1

use std::error::Error;

2

use std::fs;

3

use std::path::PathBuf;

4

use std::str::FromStr;

5

6

use mcrl2::aterm::ATerm;

7

use mcrl2::aterm::Symbol;

8

use mcrl2::aterm::TermBuilder;

9

use mcrl2::aterm::TermPool;

10

use mcrl2::aterm::Yield;

11

use pest::iterators::Pair;

12

use pest::Parser;

13

use pest_derive::Parser;

14

15

use crate::syntax::ConditionSyntax;

16

use crate::syntax::RewriteRuleSyntax;

17

use crate::syntax::RewriteSpecificationSyntax;

18

19

558845

#[derive(Parser)]

20

#[grammar = "rec_grammar.pest"]

21

pub struct RecParser;

22

23

/// Parses a REC specification. REC files can import other REC files.

24

/// Returns a RewriteSpec containing all the rewrite rules and a list of terms that need to be rewritten.

25

///

26

/// Arguments

27

/// `contents` - A REC specification as string

28

/// `path` - An optional path to a folder in which other importable REC files can be found.

29

#[allow(non_snake_case)]

30

97

fn parse_REC(

31

97

    tp: &mut TermPool,

32

97

    contents: &str,

33

97

    path: Option<PathBuf>,

34

97

) -> Result<(RewriteSpecificationSyntax, Vec<ATerm>), Box<dyn Error>> {

35

97

    // Initialise return result

36

97

    let mut rewrite_spec = RewriteSpecificationSyntax::default();

37

97

    let mut terms = vec![];

38

39

    // Use Pest parser (generated automatically from the grammar.pest file)

40

97

    let mut pairs = RecParser::parse(Rule::rec_spec, contents)?;

41

42

    // Get relevant sections from the REC file

43

97

    let pair = pairs.next().unwrap();

44

97

    let mut inner = pair.into_inner();

45

97

    let header = inner.next().unwrap();

46

97

    let _sorts = inner.next().unwrap();

47

97

    let cons = inner.next().unwrap();

48

97

    let _opns = inner.next().unwrap();

49

97

    let vars = inner.next().unwrap();

50

97

    let rules = inner.next().unwrap();

51

97

    let eval = inner.next().unwrap();

52

97

    let (_name, include_files) = parse_header(header);

53

97

54

97

    rewrite_spec.rewrite_rules = parse_rewrite_rules(tp, rules);

55

97

    rewrite_spec.constructors = parse_constructors(cons);

56

97

    if eval.as_rule() == Rule::eval {

57

91

        terms.extend_from_slice(&parse_eval(tp, eval));

58

91

59

60

97

    rewrite_spec.variables = parse_vars(vars);

61

62

    // REC files can import other REC files. Import all referenced by the header.

63

133

    for file in include_files {

64

36

        if let Some(p) = &path {

65

            let include_path = p.parent().unwrap();

66

            let file_name = PathBuf::from_str(&(file.to_lowercase() + ".rec")).unwrap();

67

            let load_file = include_path.join(file_name);

68

            let contents = fs::read_to_string(load_file).unwrap();

69

            let (include_spec, include_terms) = parse_REC(tp, &contents, path.clone())?;

70

71

            // Add rewrite rules and terms to the result.

72

            terms.extend_from_slice(&include_terms);

73

            rewrite_spec

74

                .rewrite_rules

75

                .extend_from_slice(&include_spec.rewrite_rules);

76

            rewrite_spec.constructors.extend_from_slice(&include_spec.constructors);

77

            for s in include_spec.variables {

78

                if !rewrite_spec.variables.contains(&s) {

79

                    rewrite_spec.variables.push(s);

80

81

82

36

83

84

85

97

    Ok((rewrite_spec, terms))

86

97

87

88

/// Load a REC specification from a specified file.

89

#[allow(non_snake_case)]

90

pub fn load_REC_from_file(

91

    tp: &mut TermPool,

92

    file: PathBuf,

93

) -> Result<(RewriteSpecificationSyntax, Vec<ATerm>), Box<dyn Error>> {

94

    let contents = fs::read_to_string(file.clone()).unwrap();

95

    parse_REC(tp, &contents, Some(file))

96

97

98

/// Load and join multiple REC specifications

99

#[allow(non_snake_case)]

100

60

pub fn load_REC_from_strings(

101

60

    tp: &mut TermPool,

102

60

    specs: &[&str],

103

60

) -> Result<(RewriteSpecificationSyntax, Vec<ATerm>), Box<dyn Error>> {

104

60

    let mut rewrite_spec = RewriteSpecificationSyntax::default();

105

60

    let mut terms = vec![];

106

107

156

    for spec in specs {

108

96

        let (include_spec, include_terms) = parse_REC(tp, spec, None)?;

109

96

        rewrite_spec.merge(&include_spec);

110

96

        terms.extend_from_slice(&include_terms);

111

112

113

60

    Ok((rewrite_spec, terms))

114

60

115

116

/// Extracts data from parsed header of REC spec. Returns name and include files.

117

97

fn parse_header(pair: Pair<Rule>) -> (String, Vec<String>) {

118

97

    debug_assert_eq!(pair.as_rule(), Rule::header);

119

120

97

    let mut inner = pair.into_inner();

121

97

    let name = inner.next().unwrap().as_str().to_string();

122

97

    let mut include_files = vec![];

123

124

133

    for f in inner {

125

36

        include_files.push(f.as_str().to_string());

126

36

127

128

97

    (name, include_files)

129

97

130

131

/// Extracts data from parsed constructor section, derives the arity of symbols. Types are ignored.

132

97

fn parse_constructors(pair: Pair<Rule>) -> Vec<(String, usize)> {

133

97

    debug_assert_eq!(pair.as_rule(), Rule::cons);

134

135

97

    let mut constructors = Vec::new();

136

542

    for decl in pair.into_inner() {

137

542

        debug_assert_eq!(decl.as_rule(), Rule::cons_decl);

138

542

        let mut inner = decl.into_inner();

139

542

        let symbol = inner.next().unwrap().as_str().to_string();

140

542

        let arity = inner.count() - 1;

141

542

        constructors.push((symbol, arity));

142

143

97

    constructors

144

97

145

146

/// Extracts data from parsed rewrite rules. Returns list of rewrite rules

147

97

fn parse_rewrite_rules(tp: &mut TermPool, pair: Pair<Rule>) -> Vec<RewriteRuleSyntax> {

148

97

    debug_assert_eq!(pair.as_rule(), Rule::rules);

149

97

    let mut rules = vec![];

150

97

    let inner = pair.into_inner();

151

1763

    for p in inner {

152

1666

        let rule = parse_rewrite_rule(tp, p);

153

1666

        rules.push(rule);

154

1666

155

97

    rules

156

97

157

158

// Extracts data from the variable VARS block. Types are ignored.

159

97

fn parse_vars(pair: Pair<Rule>) -> Vec<String> {

160

97

    debug_assert_eq!(pair.as_rule(), Rule::vars);

161

162

97

    let mut variables = vec![];

163

97

    let inner = pair.into_inner();

164

246

    for v in inner {

165

149

        debug_assert_eq!(v.as_rule(), Rule::var_decl);

166

167

149

        variables.extend(parse_var_decl(v));

168

169

170

97

    variables

171

97

172

173

150

fn parse_var_decl(pair: Pair<Rule>) -> Vec<String> {

174

150

    debug_assert_eq!(pair.as_rule(), Rule::var_decl);

175

176

150

    let mut variables = vec![];

177

150

    let inner = pair.into_inner();

178

657

    for v in inner {

179

507

        debug_assert_eq!(v.as_rule(), Rule::identifier);

180

181

507

        variables.push(String::from(v.as_str()));

182

183

184

    // There might be a better way, but the last identifier is the type.

185

150

    variables.pop();

186

150

187

150

    variables

188

150

189

190

/// Extracts data from parsed EVAL section, returns a list of terms that need to be rewritten.

191

91

fn parse_eval(tp: &mut TermPool, pair: Pair<Rule>) -> Vec<ATerm> {

192

91

    assert_eq!(pair.as_rule(), Rule::eval);

193

91

    let mut terms = vec![];

194

91

    let inner = pair.into_inner();

195

183

    for p in inner {

196

92

        let term = parse_term(tp, p).unwrap();

197

92

        terms.push(term);

198

92

199

200

91

    terms

201

91

202

203

/// Constructs a ATerm from a string.

204

6

pub fn from_string(tp: &mut TermPool, str: &str) -> Result<ATerm, Box<dyn Error>> {

205

6

    let mut pairs = RecParser::parse(Rule::term, str)?;

206

6

    parse_term(tp, pairs.next().unwrap())

207

6

208

209

/// Extracts data from parsed term.

210

3794

fn parse_term(tp: &mut TermPool, pair: Pair<Rule>) -> Result<ATerm, Box<dyn Error>> {

211

3794

    debug_assert_eq!(pair.as_rule(), Rule::term);

212

213

3794

    let mut builder = TermBuilder::<Pair<'_, Rule>, Symbol>::new();

214

3794

215

3794

    Ok(builder

216

3794

        .evaluate(

217

3794

tp,

218

3794

            pair,

219

14929

            |tp, stack, pair| {

220

14929

                match pair.as_rule() {

221

                    Rule::term => {

222

14929

                        let mut inner = pair.into_inner();

223

14929

                        let head_symbol = inner.next().unwrap().as_str();

224

14929

225

14929

                        // Queue applications for all the arguments.

226

14929

                        let mut arity = 0;

227

14929

                        if let Some(args) = inner.next() {

228

11135

                            for arg in args.into_inner() {

229

11135

                                stack.push(arg);

230

11135

                                arity += 1;

231

11135

232

7817

233

234

14929

                        Ok(Yield::Construct(tp.create_symbol(head_symbol, arity)))

235

236

                    _ => {

237

                        panic!("Should be unreachable!")

238

239

240

14929

},

241

14929

            |tp, symbol, args| Ok(tp.create(&symbol, args)),

242

3794

243

3794

        .unwrap())

244

3794

245

246

// /Extracts data from parsed rewrite rule

247

1667

fn parse_rewrite_rule(tp: &mut TermPool, pair: Pair<Rule>) -> RewriteRuleSyntax {

248

1667

    debug_assert!(pair.as_rule() == Rule::single_rewrite_rule || pair.as_rule() == Rule::rewrite_rule);

249

250

1667

    let mut inner = match pair.as_rule() {

251

1

        Rule::single_rewrite_rule => pair.into_inner().next().unwrap().into_inner(),

252

1666

        Rule::rewrite_rule => pair.into_inner(),

253

        _ => {

254

            panic!("Unreachable");

255

256

};

257

1667

    let lhs = parse_term(tp, inner.next().unwrap()).unwrap();

258

1667

    let rhs = parse_term(tp, inner.next().unwrap()).unwrap();

259

1667

260

1667

    // Extract conditions

261

1667

    let mut conditions = vec![];

262

1848

    for c in inner {

263

181

        assert_eq!(c.as_rule(), Rule::condition);

264

181

        let mut c_inner = c.into_inner();

265

181

        let lhs_cond = parse_term(tp, c_inner.next().unwrap()).unwrap();

266

181

        let equality = match c_inner.next().unwrap().as_str() {

267

181

            "=" => true,

268

72

            "<>" => false,

269

            _ => {

270

                panic!("Unknown comparison operator");

271

272

};

273

181

        let rhs_cond = parse_term(tp, c_inner.next().unwrap()).unwrap();

274

181

275

181

        let condition = ConditionSyntax {

276

181

            lhs: lhs_cond,

277

181

            rhs: rhs_cond,

278

181

            equality,

279

181

};

280

181

        conditions.push(condition);

281

282

283

1667

    RewriteRuleSyntax { lhs, rhs, conditions }

284

1667

285

286

#[cfg(test)]

287

mod tests {

288

    use super::*;

289

290

    #[test]

291

1

    fn test_raw_parsing() {

292

1

        assert!(RecParser::parse(Rule::single_term, "f(a").is_err());

293

1

        assert!(RecParser::parse(Rule::single_term, "f()").is_err());

294

1

        assert!(RecParser::parse(Rule::single_term, "f(a,)").is_err());

295

1

        assert!(RecParser::parse(Rule::single_term, "f").is_ok());

296

1

        assert!(RecParser::parse(Rule::single_term, "f(a)").is_ok());

297

1

        assert!(RecParser::parse(Rule::single_term, "f(a,b)").is_ok());

298

1

        assert!(RecParser::parse(Rule::single_rewrite_rule, "f(a,b) = g(x)").is_ok());

299

1

        assert!(RecParser::parse(Rule::single_rewrite_rule, "f(a,b) = g(x) if x = a").is_ok());

300

1

        assert!(RecParser::parse(Rule::single_rewrite_rule, "f(a,b) = g(x) if x<> a").is_ok());

301

1

        assert!(RecParser::parse(Rule::single_rewrite_rule, "f(a,b) = g(x) if x <= a").is_err());

302

1

        assert!(RecParser::parse(Rule::single_rewrite_rule, "f(a,b) = ").is_err());

303

1

304

305

    #[test]

306

1

    fn test_parsing_rewrite_rule() {

307

1

        let mut tp = TermPool::new();

308

1

309

1

        let expected = RewriteRuleSyntax {

310

1

            lhs: from_string(&mut tp, "f(x,b)").unwrap(),

311

1

            rhs: from_string(&mut tp, "g(x)").unwrap(),

312

1

            conditions: vec![

313

1

                ConditionSyntax {

314

1

                    lhs: from_string(&mut tp, "x").unwrap(),

315

1

                    rhs: from_string(&mut tp, "a").unwrap(),

316

1

                    equality: true,

317

1

},

318

1

                ConditionSyntax {

319

1

                    lhs: from_string(&mut tp, "b").unwrap(),

320

1

                    rhs: from_string(&mut tp, "b").unwrap(),

321

1

                    equality: true,

322

1

},

323

1

],

324

1

};

325

1

326

1

        let actual = parse_rewrite_rule(

327

1

            &mut tp,

328

1

            RecParser::parse(Rule::single_rewrite_rule, "f(x,b) = g(x) if x = a and-if b = b")

329

1

                .unwrap()

330

1

                .next()

331

1

                .unwrap(),

332

1

);

333

1

        assert_eq!(actual, expected);

334

1

335

336

    #[test]

337

1

    fn test_variable_parsing() {

338

1

        let mut pairs = RecParser::parse(Rule::var_decl, "X Y Val Max : Nat").unwrap();

339

1

        assert_eq!(parse_var_decl(pairs.next().unwrap()), vec!["X", "Y", "Val", "Max"]);

340

1

341

342

    #[test]

343

1

    fn test_parsing_rec() {

344

1

        assert!(RecParser::parse(

345

1

            Rule::rec_spec,

346

1

            include_str!("../../../examples/REC/rec/missionaries.rec")

347

1

348

1

        .is_ok());

349

1

350

351

    #[test]

352

1

    fn loading_rec() {

353

1

        let mut tp = TermPool::new();

354

1

        let _ = parse_REC(

355

1

            &mut tp,

356

1

            include_str!("../../../examples/REC/rec/missionaries.rec"),

357

1

            None,

358

1

);

359

1

360