Grcov report - data

1

use std::cell::RefCell;

2

use std::mem::ManuallyDrop;

3

4

use merc_aterm::Symb;

5

use merc_aterm::Symbol;

6

use merc_aterm::SymbolRef;

7

use merc_aterm::Term;

8

use merc_aterm::is_int_term;

9

10

thread_local! {

11

    /// Thread local storage that stores various default terms representing data symbols.

12

    pub static DATA_SYMBOLS: RefCell<DataSymbols> = RefCell::new(DataSymbols::new());

13

14

15

/// Defines default symbols and terms for data elements.

16

///

17

/// These mirror the mCRL2 definitions since that is convenient for loading the mCRL2 binary formats.

18

pub struct DataSymbols {

19

    // Sorts

20

    pub basic_sort_symbol: ManuallyDrop<Symbol>,

21

    pub function_sort_symbol: ManuallyDrop<Symbol>,

22

    pub container_sort_symbol: ManuallyDrop<Symbol>,

23

    pub structured_sort_symbol: ManuallyDrop<Symbol>,

24

    pub untyped_sort_symbol: ManuallyDrop<Symbol>,

25

    pub untyped_possible_sorts_symbol: ManuallyDrop<Symbol>,

26

27

    // Data expressions that are abstractions

28

    pub data_binder_symbol: ManuallyDrop<Symbol>,

29

    pub data_lambda_symbol: ManuallyDrop<Symbol>,

30

    pub data_exists_symbol: ManuallyDrop<Symbol>,

31

    pub data_forall_symbol: ManuallyDrop<Symbol>,

32

    pub data_set_comprehension_symbol: ManuallyDrop<Symbol>,

33

    pub data_bag_comprehension_symbol: ManuallyDrop<Symbol>,

34

    pub data_untyped_set_bag_comprehension_symbol: ManuallyDrop<Symbol>,

35

36

    // Data expressions

37

    pub data_function_symbol: ManuallyDrop<Symbol>,

38

    pub data_function_symbol_no_index: ManuallyDrop<Symbol>,

39

    pub data_variable: ManuallyDrop<Symbol>,

40

    pub data_where_clause: ManuallyDrop<Symbol>,

41

    pub data_untyped_identifier_clause: ManuallyDrop<Symbol>,

42

43

    /// The data application symbol for a given arity.

44

    data_appl: Vec<Symbol>,

45

46

47

impl DataSymbols {

48

704

    fn new() -> Self {

49

704

        Self {

50

704

            basic_sort_symbol: ManuallyDrop::new(Symbol::new("SortId", 1)),

51

704

            function_sort_symbol: ManuallyDrop::new(Symbol::new("SortArrow", 2)),

52

704

            container_sort_symbol: ManuallyDrop::new(Symbol::new("SortCons", 2)),

53

704

            structured_sort_symbol: ManuallyDrop::new(Symbol::new("SortStruct", 1)),

54

704

            untyped_sort_symbol: ManuallyDrop::new(Symbol::new("UntypedSortUnknown", 0)),

55

704

            untyped_possible_sorts_symbol: ManuallyDrop::new(Symbol::new("UntypedSortsPossible", 1)),

56

704

57

704

            data_binder_symbol: ManuallyDrop::new(Symbol::new("Binder", 3)),

58

704

            data_lambda_symbol: ManuallyDrop::new(Symbol::new("Lambda", 0)),

59

704

            data_exists_symbol: ManuallyDrop::new(Symbol::new("Exists", 0)),

60

704

            data_forall_symbol: ManuallyDrop::new(Symbol::new("Forall", 0)),

61

704

            data_set_comprehension_symbol: ManuallyDrop::new(Symbol::new("SetComp", 0)),

62

704

            data_bag_comprehension_symbol: ManuallyDrop::new(Symbol::new("BagComp", 0)),

63

704

            data_untyped_set_bag_comprehension_symbol: ManuallyDrop::new(Symbol::new("UntypedSetBagComp", 0)),

64

704

65

704

            data_function_symbol: ManuallyDrop::new(Symbol::new("OpId", 2)),

66

704

            data_function_symbol_no_index: ManuallyDrop::new(Symbol::new("OpIdNoIndex", 2)),

67

704

            data_variable: ManuallyDrop::new(Symbol::new("DataVarId", 2)),

68

704

            data_where_clause: ManuallyDrop::new(Symbol::new("Where", 2)),

69

704

            data_untyped_identifier_clause: ManuallyDrop::new(Symbol::new("UntypedIdentifier", 1)),

70

704

71

704

            data_appl: Vec::new(),

72

704

73

704

74

75

    /// Returns true iff the given term is any of the possible data expressions.

76

    /// Note that this check is relatively expensive.

77

1066897237

    pub fn is_data_expression<'a, 'b, T: Term<'a, 'b>>(&mut self, term: &'b T) -> bool {

78

1066897237

        self.is_data_variable(term)

79

1064957691

            || self.is_data_function_symbol(term)

80

944549358

            || self.is_data_machine_number(term)

81

944548308

            || self.is_data_binder(term)

82

944548308

            || self.is_data_where_clause(term)

83

944548308

            || self.is_data_application(term)

84

1066897237

85

86

    /// Returns true iff the given term is a data variable.

87

1072974850

    pub fn is_data_variable<'a, 'b, T: Term<'a, 'b>>(&self, term: &'b T) -> bool {

88

1072974850

        term.get_head_symbol() == **self.data_variable

89

1072974850

90

91

    /// Returns true iff the given term is a data function symbol.

92

1657202116

    pub fn is_data_function_symbol<'a, 'b, T: Term<'a, 'b>>(&self, term: &'b T) -> bool {

93

1657202116

        term.get_head_symbol() == **self.data_function_symbol

94

945503765

            || term.get_head_symbol() == **self.data_function_symbol_no_index

95

1657202116

96

97

    /// Returns true iff the given term is a data machine number.

98

944625189

    pub fn is_data_machine_number<'a, 'b, T: Term<'a, 'b>>(&self, term: &'b T) -> bool {

99

944625189

        is_int_term(term)

100

944625189

101

102

    /// Returns true iff the given term is a data where clause.

103

944548308

    pub fn is_data_where_clause<'a, 'b, T: Term<'a, 'b>>(&self, term: &'b T) -> bool {

104

944548308

        term.get_head_symbol() == **self.data_where_clause

105

944548308

106

107

    /// Returns true iff the given term is a data abstraction (binder).

108

944548308

    pub fn is_data_binder<'a, 'b, T: Term<'a, 'b>>(&self, term: &'b T) -> bool {

109

944548308

        term.get_head_symbol() == **self.data_binder_symbol

110

944548308

111

112

    /// Returns true iff the given term is a data application.

113

1495005859

    pub fn is_data_application<'a, 'b, T: Term<'a, 'b>>(&mut self, term: &'b T) -> bool {

114

1495005859

        let arity = term.get_head_symbol().arity();

115

1495005859

        term.get_head_symbol() == *self.get_data_application_symbol(arity)

116

1495005859

117

118

    /// Returns the data application symbol for the given arity, creating it if necessary.

119

1555004572

    pub fn get_data_application_symbol(&mut self, arity: usize) -> &SymbolRef<'_> {

120

        // It can be that data_applications are created without create_data_application in the mcrl2 ffi.

121

1555007203

        while self.data_appl.len() <= arity {

122

2631

            let symbol = Symbol::new("DataAppl", self.data_appl.len());

123

2631

124

2631

            self.data_appl.push(symbol);

125

2631

126

127

1555004572

        &self.data_appl[arity]

128

1555004572

129

130

    /// Returns true iff the given term is a sort expression.

131

    pub fn is_sort_expression<'a, 'b, T: Term<'a, 'b>>(&self, term: &'b T) -> bool {

132

        self.is_basic_sort(term)

133

134

135

    /// Returns true iff the given term is a basic sort.

136

    pub fn is_basic_sort<'a, 'b, T: Term<'a, 'b>>(&self, term: &'b T) -> bool {

137

        term.get_head_symbol() == **self.basic_sort_symbol

138

139

140

141

// Helper functions to access the DATA_SYMBOLS thread local storage.

142

143

/// See [DataSymbols::is_sort_expression].

144

pub fn is_sort_expression<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

145

    DATA_SYMBOLS.with_borrow(|ds| ds.is_sort_expression(term))

146

147

148

/// See [DataSymbols::is_basic_sort].

149

pub fn is_basic_sort<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

150

    DATA_SYMBOLS.with_borrow(|ds| ds.is_basic_sort(term))

151

152

153

/// See [DataSymbols::is_data_variable].

154

6077613

pub fn is_data_variable<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

155

6077613

    DATA_SYMBOLS.with_borrow(|ds| ds.is_data_variable(term))

156

6077613

157

158

/// See [DataSymbols::is_data_expression].

159

1066897237

pub fn is_data_expression<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

160

1066897237

    DATA_SYMBOLS.with_borrow_mut(|ds| ds.is_data_expression(term))

161

1066897237

162

163

/// See [DataSymbols::is_data_function_symbol].

164

592244425

pub fn is_data_function_symbol<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

165

592244425

    DATA_SYMBOLS.with_borrow(|ds| ds.is_data_function_symbol(term))

166

592244425

167

168

/// See [DataSymbols::is_data_machine_number].

169

75831

pub fn is_data_machine_number<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

170

75831

    DATA_SYMBOLS.with_borrow(|ds| ds.is_data_machine_number(term))

171

75831

172

173

/// See [DataSymbols::is_data_where_clause].

174

pub fn is_data_where_clause<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

175

    DATA_SYMBOLS.with_borrow(|ds| ds.is_data_where_clause(term))

176

177

178

/// See [DataSymbols::is_data_binder].

179

pub fn is_data_binder<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

180

    DATA_SYMBOLS.with_borrow(|ds| ds.is_data_binder(term))

181

182

183

/// See [DataSymbols::is_data_application].

184

550457551

pub fn is_data_application<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {

185

550457551

    DATA_SYMBOLS.with_borrow_mut(|ds| ds.is_data_application(term))

186

550457551