Grcov report - visitor.rs

1

use std::ops::ControlFlow;

2

3

use merc_utilities::MercError;

4

5

use crate::ActFrm;

6

use crate::RegFrm;

7

use crate::SortExpression;

8

use crate::StateFrm;

9

10

/// Visits the state formula and calls the given function on each subformula.

11

///

12

/// The visitor function takes a state formula and returns a `ControlFlow`. If

13

/// it returns `ControlFlow::Break(value)`, the traversal is stopped and the

14

/// value is returned. If it returns `ControlFlow::Continue(())`, the traversal

15

/// continues.

16

4877

pub fn visit_statefrm<T, F>(formula: &StateFrm, mut visitor: F) -> Result<Option<T>, MercError>

17

4877

where

18

4877

    F: FnMut(&StateFrm) -> Result<ControlFlow<T>, MercError>,

19

20

4877

    visit_statefrm_rec(formula, &mut visitor)

21

4877

22

23

pub fn visit_sort_expr<T, F>(sort_expr: &SortExpression, mut visitor: F) -> Result<Option<T>, MercError>

24

where

25

    F: FnMut(&SortExpression) -> Result<ControlFlow<T>, MercError>,

26

27

    visit_sort_expr_rec(sort_expr, &mut visitor)

28

29

30

/// See [`visit_statefrm`].

31

47550

fn visit_statefrm_rec<T, F>(formula: &StateFrm, function: &mut F) -> Result<Option<T>, MercError>

32

47550

where

33

47550

    F: FnMut(&StateFrm) -> Result<ControlFlow<T>, MercError>,

34

35

47550

    if let ControlFlow::Break(result) = function(formula)? {

36

        // The visitor requested to break the traversal.

37

        return Ok(Some(result));

38

47550

39

40

47550

    match formula {

41

8132

        StateFrm::Binary { lhs, rhs, .. } => {

42

8132

            visit_statefrm_rec(lhs, function)?;

43

8132

            visit_statefrm_rec(rhs, function)?;

44

45

5592

        StateFrm::FixedPoint { body, .. } => {

46

5592

            visit_statefrm_rec(body, function)?;

47

48

        StateFrm::Bound { body, .. } => {

49

            visit_statefrm_rec(body, function)?;

50

51

20817

        StateFrm::Modality { expr, .. } => {

52

20817

            visit_statefrm_rec(expr, function)?;

53

54

        StateFrm::Quantifier { body, .. } => {

55

            visit_statefrm_rec(body, function)?;

56

57

        StateFrm::DataValExprRightMult(expr, _data_val) => {

58

            visit_statefrm_rec(expr, function)?;

59

60

        StateFrm::DataValExprLeftMult(_data_val, expr) => {

61

            visit_statefrm_rec(expr, function)?;

62

63

        StateFrm::Unary { expr, .. } => {

64

            visit_statefrm_rec(expr, function)?;

65

66

        StateFrm::Id(_, _)

67

        | StateFrm::True

68

        | StateFrm::False

69

        | StateFrm::Delay(_)

70

        | StateFrm::Yaled(_)

71

13009

        | StateFrm::DataValExpr(_) => {}

72

73

74

    // The visitor did not break the traversal.

75

47550

    Ok(None)

76

47550

77

78

fn visit_sort_expr_rec<T, F>(sort_expr: &SortExpression, function: &mut F) -> Result<Option<T>, MercError>

79

where

80

    F: FnMut(&SortExpression) -> Result<ControlFlow<T>, MercError>,

81

82

    if let ControlFlow::Break(result) = function(sort_expr)? {

83

        // The visitor requested to break the traversal.

84

        return Ok(Some(result));

85

86

87

    match sort_expr {

88

        SortExpression::Product { lhs, rhs } => {

89

            visit_sort_expr_rec(lhs, function)?;

90

            visit_sort_expr_rec(rhs, function)?;

91

92

        SortExpression::Function { domain, range } => {

93

            visit_sort_expr_rec(domain, function)?;

94

            visit_sort_expr_rec(range, function)?;

95

96

        SortExpression::Struct { inner } => {

97

            for constructors in inner {

98

                for (_name, sort) in &constructors.args {

99

                    visit_sort_expr_rec(sort, function)?;

100

101

102

103

        SortExpression::Complex(_complex_sort, sort_expression) => {

104

            visit_sort_expr_rec(sort_expression, function)?;

105

106

        SortExpression::Reference(_) | SortExpression::Simple(_) => {}

107

108

109

    // The visitor did not break the traversal.

110

    Ok(None)

111

112

113

/// Maps the given `function` recursively to the regular formula.

114

5201

pub fn visit_regular_formula<T, F>(formula: &RegFrm, mut function: F) -> Result<Option<T>, MercError>

115

5201

where

116

5201

    F: FnMut(&RegFrm) -> Result<ControlFlow<T>, MercError>,

117

118

5201

    visit_regular_formula_rec(formula, &mut function)

119

5201

120

121

/// See [visit_regular_formula].

122

7877

fn visit_regular_formula_rec<T, F>(formula: &RegFrm, visit: &mut F) -> Result<Option<T>, MercError>

123

7877

where

124

7877

    F: FnMut(&RegFrm) -> Result<ControlFlow<T>, MercError>,

125

126

7877

    if let ControlFlow::Break(result) = visit(formula)? {

127

        // A substitution was made, return the new formula.

128

        return Ok(Some(result));

129

7877

130

131

7877

    match formula {

132

2676

        RegFrm::Iteration(reg_frm) => {

133

2676

            visit_regular_formula_rec(reg_frm, visit)?;

134

135

        RegFrm::Plus(reg_frm) => {

136

            visit_regular_formula_rec(reg_frm, visit)?;

137

138

        RegFrm::Sequence { lhs, rhs } => {

139

            visit_regular_formula_rec(lhs, visit)?;

140

            visit_regular_formula_rec(rhs, visit)?;

141

142

        RegFrm::Choice { lhs, rhs } => {

143

            visit_regular_formula_rec(lhs, visit)?;

144

            visit_regular_formula_rec(rhs, visit)?;

145

146

5201

        _ => {}

147

148

149

7877

    Ok(None)

150

7877

151

152

/// Visitor for action formulas.

153

///

154

5201

pub fn visit_action_formula<T, F>(formula: &ActFrm, mut visitor: F) -> Result<Option<T>, MercError>

155

5201

where

156

5201

    F: FnMut(&ActFrm) -> Result<ControlFlow<T>, MercError>,

157

158

5201

    visit_action_formula_rec(formula, &mut visitor)

159

5201

160

161

5202

fn visit_action_formula_rec<T, F>(formula: &ActFrm, visitor: &mut F) -> Result<Option<T>, MercError>

162

5202

where

163

5202

    F: FnMut(&ActFrm) -> Result<ControlFlow<T>, MercError>,

164

165

5202

    if let ControlFlow::Break(result) = visitor(formula)? {

166

        // The visitor requested to break the traversal.

167

        return Ok(Some(result));

168

5202

169

170

5202

    match formula {

171

1

        ActFrm::Negation(act_frm) => {

172

1

            visit_action_formula_rec(act_frm, visitor)?;

173

174

        ActFrm::Quantifier {

175

            quantifier: _,

176

            variables: _,

177

            body,

178

        } => {

179

            visit_action_formula_rec(body, visitor)?;

180

181

        ActFrm::Binary { op: _, lhs, rhs } => {

182

            visit_action_formula_rec(lhs, visitor)?;

183

            visit_action_formula_rec(rhs, visitor)?;

184

185

5201

        ActFrm::True | ActFrm::False | ActFrm::MultAct(_) | ActFrm::DataExprVal(_) => {}

186

187

188

    // The visitor did not break the traversal.

189

5202

    Ok(None)

190

5202