Grcov report - naive

1

#![forbid(unsafe_code)]

2

3

use log::info;

4

use merc_data::DataApplication;

5

use merc_data::DataExpression;

6

use merc_data::DataExpressionRef;

7

use merc_utilities::debug_trace;

8

9

use crate::AnnouncementInnermost;

10

use crate::MatchAnnouncement;

11

use crate::RewriteEngine;

12

use crate::RewriteSpecification;

13

use crate::RewritingStatistics;

14

use crate::set_automaton::SetAutomaton;

15

use crate::utilities::DataPositionIndexed;

16

17

/// Naive Adaptive Pattern Matching Automaton (APMA) rewrite engine

18

/// implementation for testing purposes.

19

pub struct NaiveRewriter {

20

    apma: SetAutomaton<AnnouncementInnermost>,

21

22

23

impl RewriteEngine for NaiveRewriter {

24

7

    fn rewrite(&mut self, t: &DataExpression) -> DataExpression {

25

7

        let mut stats = RewritingStatistics::default();

26

27

7

        let result = NaiveRewriter::rewrite_aux(&self.apma, t.copy(), &mut stats);

28

29

7

        info!(

30

            "{} rewrites, {} single steps and {} symbol comparisons",

31

            stats.recursions, stats.rewrite_steps, stats.symbol_comparisons

32

);

33

7

        result

34

7

35

36

37

impl NaiveRewriter {

38

5

    pub fn new(spec: &RewriteSpecification) -> NaiveRewriter {

39

5

        NaiveRewriter {

40

5

            apma: SetAutomaton::new(spec, AnnouncementInnermost::new, false),

41

5

42

5

43

44

    /// Function to rewrite a term 't'. The elements of the automaton 'states' and 'tp' are passed

45

    /// as separate parameters to satisfy the borrow checker.

46

3327

    fn rewrite_aux(

47

3327

        automaton: &SetAutomaton<AnnouncementInnermost>,

48

3327

        t: DataExpressionRef<'_>,

49

3327

        stats: &mut RewritingStatistics,

50

3327

    ) -> DataExpression {

51

3327

        let symbol = t.data_function_symbol();

52

53

        // Recursively call rewrite_aux on all the subterms.

54

3327

        let mut arguments = vec![];

55

3327

        for t in t.data_arguments() {

56

1970

            arguments.push(NaiveRewriter::rewrite_aux(automaton, t, stats));

57

1970

58

59

3327

        let nf: DataExpression = if arguments.is_empty() {

60

2240

            symbol.protect().into()

61

        } else {

62

1087

            DataApplication::with_args(&symbol, &arguments).into()

63

};

64

65

3327

        match NaiveRewriter::find_match(automaton, &nf, stats) {

66

1983

            None => nf,

67

1344

            Some((_announcement, ema)) => {

68

1344

                let result = ema.rhs_stack.evaluate(&nf);

69

1344

                debug_trace!("rewrote {} to {} using rule {}", nf, result, _announcement.rule);

70

1344

                NaiveRewriter::rewrite_aux(automaton, result.copy(), stats)

71

72

73

3327

74

75

    /// Use the APMA to find a match for the given term.

76

3327

    fn find_match<'a>(

77

3327

        automaton: &'a SetAutomaton<AnnouncementInnermost>,

78

3327

        t: &DataExpression,

79

3327

        stats: &mut RewritingStatistics,

80

3327

    ) -> Option<(&'a MatchAnnouncement, &'a AnnouncementInnermost)> {

81

        // Start at the initial state

82

3327

        let mut state_index = 0;

83

        loop {

84

4558

            let state = &automaton.states()[state_index];

85

86

            // Get the symbol at the position state.label

87

4558

            let u = t.get_data_position(state.label());

88

4558

            let symbol = u.data_function_symbol();

89

90

            // Get the transition for the label and check if there is a pattern match

91

4558

            if let Some(transition) = automaton.transitions().get(&(state_index, symbol.operation_id())) {

92

4557

                for (announcement, ema) in &transition.announcements {

93

1345

                    let mut conditions_hold = true;

94

95

                    // Check conditions if there are any

96

1345

                    if !ema.conditions.is_empty() {

97

3

                        conditions_hold = NaiveRewriter::check_conditions(automaton, &t.copy(), ema, stats);

98

1342

99

100

                    // Check equivalence of subterms for non-linear patterns

101

1345

                    'ec_check: for ec in &ema.equivalence_classes {

102

                        if ec.positions.len() > 1 {

103

                            let mut iter_pos = ec.positions.iter();

104

                            let first_pos = iter_pos.next().unwrap();

105

                            let first_term = t.get_data_position(first_pos);

106

107

                            for other_pos in iter_pos {

108

                                let other_term = t.get_data_position(other_pos);

109

                                if first_term != other_term {

110

                                    conditions_hold = false;

111

                                    break 'ec_check;

112

113

114

115

116

117

1345

                    if conditions_hold {

118

                        // We found a matching pattern

119

1344

                        return Some((announcement, ema));

120

1

121

122

123

                // If there is no pattern match we check if the transition has a destination state

124

3213

                if transition.destinations.is_empty() {

125

                    // If there is no destination state there is no pattern match

126

1982

                    return None;

127

1231

128

129

1231

                state_index = transition.destinations.first().unwrap().1;

130

            } else {

131

                // If there is no transition for the symbol, there is no match

132

1

                return None;

133

134

135

3327

136

137

    /// Given a term with head symbol 't_head' and subterms 't_subterms' and an EnhancedMatchAnnouncement,

138

    /// check if the conditions hold.

139

3

    fn check_conditions(

140

3

        automaton: &SetAutomaton<AnnouncementInnermost>,

141

3

        t: &DataExpressionRef<'_>,

142

3

        ema: &AnnouncementInnermost,

143

3

        stats: &mut RewritingStatistics,

144

3

    ) -> bool {

145

3

        for c in &ema.conditions {

146

3

            let rhs = c.lhs_term_stack.evaluate(t);

147

3

            let lhs = c.rhs_term_stack.evaluate(t);

148

149

3

            let rhs_normal = NaiveRewriter::rewrite_aux(automaton, rhs.copy(), stats);

150

3

            let lhs_normal = NaiveRewriter::rewrite_aux(automaton, lhs.copy(), stats);

151

152

3

            let holds = (lhs_normal == rhs_normal && c.equality) || (lhs_normal != rhs_normal && !c.equality);

153

3

            if !holds {

154

1

                return false;

155

2

156

157

158

2

        true

159

3

160