Grcov report - innermost

1

#![forbid(unsafe_code)]

2

3

use std::fmt;

4

5

use merc_aterm::Protected;

6

use merc_aterm::ProtectedWriteGuard;

7

use merc_data::DataExpressionRef;

8

use merc_data::DataFunctionSymbolRef;

9

use merc_utilities::debug_trace;

10

11

// Only used in debug_trace!

12

#[allow(unused_imports)]

13

use itertools::Itertools;

14

15

use crate::utilities::DataPositionIndexed;

16

17

use super::Config;

18

use super::TermStack;

19

20

/// This stack is used to avoid recursion and also to keep track of terms in

21

/// normal forms by explicitly representing the rewrites of a right hand

22

/// side.

23

#[derive(Default)]

24

pub struct InnermostStack {

25

    pub configs: Protected<Vec<Config<'static>>>,

26

    pub terms: Protected<Vec<Option<DataExpressionRef<'static>>>>,

27

28

29

impl InnermostStack {

30

    /// Updates the InnermostStack to integrate the rhs_stack instructions.

31

2606692

    pub fn integrate(

32

2606692

        write_configs: &mut ProtectedWriteGuard<Vec<Config<'static>>>,

33

2606692

        write_terms: &mut ProtectedWriteGuard<Vec<Option<DataExpressionRef<'static>>>>,

34

2606692

        rhs_stack: &TermStack,

35

2606692

        term: &DataExpressionRef<'_>,

36

2606692

        result_index: usize,

37

2606692

) {

38

        // TODO: This ignores the first element of the stack, but that is kind of difficult to deal with.

39

2606692

        let top_of_stack = write_terms.len();

40

2606692

        write_terms.reserve(rhs_stack.stack_size - 1); // We already reserved space for the result.

41

4721893

        for _ in 0..rhs_stack.stack_size - 1 {

42

4721893

            write_terms.push(None);

43

4721893

44

45

2606692

        let mut first = true;

46

2983018

        for config in rhs_stack.innermost_stack.read().iter() {

47

2983018

            match config {

48

2983018

                Config::Construct(symbol, arity, offset) => {

49

2983018

                    if first {

50

2443890

                        // The first result must be placed on the original result index.

51

2443890

                        InnermostStack::add_result(write_configs, symbol.copy(), *arity, result_index);

52

2443893

                    } else {

53

539128

                        // Otherwise, we put it on the end of the stack.

54

539128

                        InnermostStack::add_result(write_configs, symbol.copy(), *arity, top_of_stack + offset - 1);

55

539128

56

57

                Config::Term(term, index) => {

58

                    let term = write_configs.protect(term);

59

                    write_configs.push(Config::Term(term.into(), *index));

60

61

                Config::Rewrite(_) => {

62

                    unreachable!("This case should not happen");

63

64

                Config::Return() => {

65

                    unreachable!("This case should not happen");

66

67

68

2983018

            first = false;

69

70

2606692

        debug_trace!(

71

            "\t applied stack size: {}, substitution: {{{}}}, stack: [{}]",

72

            rhs_stack.stack_size,

73

            rhs_stack.variables.iter().format_with(", ", |element, f| {

74

                f(&format_args!("{} -> {}", element.0, element.1))

75

}),

76

            rhs_stack.innermost_stack.read().iter().format("\n")

77

);

78

79

2606692

        debug_assert!(

80

2606692

            rhs_stack.stack_size != 1 || rhs_stack.variables.len() <= 1,

81

            "There can only be a single variable in the right hand side"

82

);

83

2606692

        if rhs_stack.stack_size == 1 && rhs_stack.variables.len() == 1 {

84

162802

            // This is a special case where we place the result on the correct position immediately.

85

162802

            // The right hand side is only a variable

86

162802

            write_terms[result_index] = Some(

87

162802

                write_terms

88

162802

                    .protect(&term.get_data_position(&rhs_stack.variables[0].0))

89

162802

                    .into(),

90

162802

);

91

162802

        } else {

92

4182765

            for (position, index) in &rhs_stack.variables {

93

4182765

                // Add the positions to the stack.

94

4182765

                write_terms[top_of_stack + index - 1] =

95

4182765

                    Some(write_terms.protect(&term.get_data_position(position)).into());

96

4182765

97

98

2606692

99

100

    /// Indicate that the given symbol with arity can be constructed at the given index.

101

5226796

    pub fn add_result(

102

5226796

        write_configs: &mut ProtectedWriteGuard<Vec<Config<'static>>>,

103

5226796

        symbol: DataFunctionSymbolRef<'_>,

104

5226796

        arity: usize,

105

5226796

        index: usize,

106

5226796

) {

107

5226796

        let symbol = write_configs.protect(&symbol);

108

5226796

        write_configs.push(Config::Construct(symbol.into(), arity, index));

109

5226796

110

111

    /// Indicate that the term must be rewritten and its result must be placed at the given index.

112

2243778

    pub fn add_rewrite(

113

2243778

        write_configs: &mut ProtectedWriteGuard<Vec<Config<'static>>>,

114

2243778

        write_terms: &mut ProtectedWriteGuard<Vec<Option<DataExpressionRef<'static>>>>,

115

2243778

        term: DataExpressionRef<'_>,

116

2243778

        index: usize,

117

2243778

) {

118

2243778

        let term = write_terms.protect(&term);

119

2243778

        write_configs.push(Config::Rewrite(index));

120

2243778

        write_terms.push(Some(term.into()));

121

2243778

122

123

124

impl fmt::Display for InnermostStack {

125

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

126

        writeln!(f, "Terms: [")?;

127

        for (i, entry) in self.terms.read().iter().enumerate() {

128

            match entry {

129

                Some(term) => writeln!(f, "{i}\t{term}")?,

130

                None => writeln!(f, "{i}\tNone")?,

131

132

133

        writeln!(f, "]")?;

134

135

        writeln!(f, "Configs: [")?;

136

        for config in self.configs.read().iter() {

137

            writeln!(f, "\t{config}")?;

138

139

        write!(f, "]")

140

141