Grcov report - innermost

1

use std::fmt;

2

3

use merc_aterm::Protected;

4

use merc_aterm::ProtectedWriteGuard;

5

use merc_data::DataExpressionRef;

6

use merc_data::DataFunctionSymbolRef;

7

use merc_utilities::debug_trace;

8

9

// Only used in debug_trace!

10

#[allow(unused_imports)]

11

use itertools::Itertools;

12

13

use crate::utilities::DataPositionIndexed;

14

15

use super::Config;

16

use super::TermStack;

17

18

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

19

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

20

/// side.

21

#[derive(Default)]

22

pub struct InnermostStack {

23

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

24

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

25

26

27

impl InnermostStack {

28

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

29

7818593

    pub fn integrate(

30

7818593

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

31

7818593

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

32

7818593

        rhs_stack: &TermStack,

33

7818593

        term: &DataExpressionRef<'_>,

34

7818593

        result_index: usize,

35

7818593

) {

36

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

37

7818593

        let top_of_stack = write_terms.len();

38

7818593

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

39

14165657

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

40

14165657

            write_terms.push(None);

41

14165657

42

43

7818593

        let mut first = true;

44

8948947

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

45

8948947

            match config {

46

8948947

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

47

8948947

                    if first {

48

7331573

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

49

7331573

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

50

7331576

                    } else {

51

1617374

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

52

1617374

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

53

1617374

54

55

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

56

                    // Safety: term is pushed into the container on the next line.

57

                    let term = unsafe { write_configs.protect(term) };

58

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

59

60

                Config::Rewrite(_) => {

61

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

62

63

                Config::Return() => {

64

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

65

66

67

8948947

            first = false;

68

69

7818593

        debug_trace!(

70

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

71

            rhs_stack.stack_size,

72

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

73

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

74

}),

75

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

76

);

77

78

7818593

        debug_assert!(

79

7818593

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

80

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

81

);

82

7818593

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

83

487020

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

84

487020

            // The right hand side is only a variable

85

487020

            // Safety: term is stored in the container on the next line.

86

487020

            write_terms[result_index] =

87

487020

                Some(unsafe { write_terms.protect(&term.get_data_position(&rhs_stack.variables[0].0)) }.into());

88

487020

        } else {

89

12548283

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

90

12548283

                // Add the positions to the stack.

91

12548283

                // Safety: term is stored in the container on the same line.

92

12548283

                write_terms[top_of_stack + index - 1] =

93

12548283

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

94

12548283

95

96

7818593

97

98

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

99

15683458

    pub fn add_result(

100

15683458

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

101

15683458

        symbol: DataFunctionSymbolRef<'_>,

102

15683458

        arity: usize,

103

15683458

        index: usize,

104

15683458

) {

105

        // Safety: symbol is pushed into the container on the next line.

106

15683458

        let symbol = unsafe { write_configs.protect(&symbol) };

107

15683458

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

108

15683458

109

110

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

111

6734511

    pub fn add_rewrite(

112

6734511

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

113

6734511

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

114

6734511

        term: DataExpressionRef<'_>,

115

6734511

        index: usize,

116

6734511

) {

117

        // Safety: term is pushed into the container two lines below.

118

6734511

        let term = unsafe { write_terms.protect(&term) };

119

6734511

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

120

6734511

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

121

6734511

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