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

396

    fn new() -> Self {

49

396

        Self {

50

396

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

51

396

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

52

396

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

53

396

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

54

396

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

55

396

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

56

396

57

396

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

58

396

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

59

396

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

60

396

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

61

396

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

62

396

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

63

396

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

64

396

65

396

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

66

396

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

67

396

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

68

396

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

69

396

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

70

396

71

396

            data_appl: Vec::new(),

72

396

73

396

74

75

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

76

    /// Note that this check is relatively expensive.

77

609654111

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

78

609654111

        self.is_data_variable(term)

79

608546407

            || self.is_data_function_symbol(term)

80

539742252

            || self.is_data_machine_number(term)

81

539741652

            || self.is_data_binder(term)

82

539741652

            || self.is_data_where_clause(term)

83

539741652

            || self.is_data_application(term)

84

609654111

85

86

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

87

611382294

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

88

611382294

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

89

611382294

90

91

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

92

946978114

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

93

946978114

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

94

540289983

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

95

946978114

96

97

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

98

539817183

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

99

539817183

        is_int_term(term)

100

539817183

101

102

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

103

539741652

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

104

539741652

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

105

539741652

106

107

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

108

539741652

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

109

539741652

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

110

539741652

111

112

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

113

854288827

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

114

854288827

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

115

854288827

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

116

854288827

117

118

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

119

888573808

    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

888575269

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

122

1461

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

123

1461

124

1461

            self.data_appl.push(symbol);

125

1461

126

127

888573808

        &self.data_appl[arity]

128

888573808

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

1728183

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

155

1728183

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

156

1728183

157

158

/// See [DataSymbols::is_data_expression].

159

609654111

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

160

609654111

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

161

609654111

162

163

/// See [DataSymbols::is_data_function_symbol].

164

338431707

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

165

338431707

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

166

338431707

167

168

/// See [DataSymbols::is_data_machine_number].

169

74931

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

170

74931

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

171

74931

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

314547175

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

185

314547175

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

186

314547175