Grcov report - syntax.rs

1

use core::fmt;

2

3

use ahash::AHashSet;

4

use mcrl2::aterm::ATerm;

5

use mcrl2::aterm::TermPool;

6

use sabre::rewrite_specification::Condition;

7

use sabre::rewrite_specification::RewriteSpecification;

8

use sabre::rewrite_specification::Rule;

9

use sabre::utilities::to_untyped_data_expression;

10

11

/// A rewrite specification contains all the bare info we need for rewriting (in particular no type information) as a syntax tree.

12

/// Parsing a REC file results in a RewriteSpecificationSyntax.

13

#[derive(Clone, Default, Debug)]

14

pub struct RewriteSpecificationSyntax {

15

    pub rewrite_rules: Vec<RewriteRuleSyntax>,

16

    pub constructors: Vec<(String, usize)>,

17

    pub variables: Vec<String>,

18

19

20

impl RewriteSpecificationSyntax {

21

60

    pub fn to_rewrite_spec(&self, tp: &mut TermPool) -> RewriteSpecification {

22

60

        // The names for all variables

23

60

        let variables = AHashSet::from_iter(self.variables.clone());

24

60

25

60

        // Store the rewrite rules in the maximally shared term storage

26

60

        let mut rewrite_rules = Vec::new();

27

1678

        for rule in &self.rewrite_rules {

28

            // Convert the conditions.

29

1618

            let mut conditions = vec![];

30

1780

            for c in &rule.conditions {

31

162

                let condition = Condition {

32

162

                    lhs: to_untyped_data_expression(tp, &c.lhs, &variables),

33

162

                    rhs: to_untyped_data_expression(tp, &c.rhs, &variables),

34

162

                    equality: c.equality,

35

162

};

36

162

                conditions.push(condition);

37

162

38

39

1618

            rewrite_rules.push(Rule {

40

1618

                lhs: to_untyped_data_expression(tp, &rule.lhs, &variables),

41

1618

                rhs: to_untyped_data_expression(tp, &rule.rhs, &variables),

42

1618

                conditions,

43

1618

});

44

45

46

60

        RewriteSpecification { rewrite_rules }

47

60

48

49

96

    pub fn merge(&mut self, include_spec: &RewriteSpecificationSyntax) {

50

96

        self.rewrite_rules.extend_from_slice(&include_spec.rewrite_rules);

51

96

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

52

53

426

        for s in &include_spec.variables {

54

330

            if !self.variables.contains(s) {

55

330

                self.variables.push(s.clone());

56

330

57

58

96

59

60

61

impl fmt::Display for RewriteSpecificationSyntax {

62

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

63

        writeln!(f, "Variables: ")?;

64

        for variable in &self.variables {

65

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

66

67

        writeln!(f, "Rewrite rules: ")?;

68

        for rule in &self.rewrite_rules {

69

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

70

71

        writeln!(f)

72

73

74

75

/// Syntax tree for rewrite rules

76

#[derive(Debug, Clone, Eq, PartialEq)]

77

pub struct RewriteRuleSyntax {

78

    pub lhs: ATerm,

79

    pub rhs: ATerm,

80

    pub conditions: Vec<ConditionSyntax>,

81

82

83

impl fmt::Display for RewriteRuleSyntax {

84

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

85

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

86

87

88

89

/// Syntax tree for conditional part of a rewrite rule

90

#[derive(Debug, Clone, Eq, PartialEq, Ord, PartialOrd)]

91

pub struct ConditionSyntax {

92

    pub lhs: ATerm,

93

    pub rhs: ATerm,

94

    pub equality: bool, // The condition either specifies that lhs and rhs are equal or different

95