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

2069

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

17

2069

where

18

2069

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

19

20

2069

    visit_statefrm_rec(formula, &mut visitor)

21

2069

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

35816

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

32

35816

where

33

35816

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

34

35

35816

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

36

        // The visitor requested to break the traversal.

37

        return Ok(Some(result));

38

35816

39

40

35816

    match formula {

41

5848

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

42

5848

            visit_statefrm_rec(lhs, function)?;

43

5848

            visit_statefrm_rec(rhs, function)?;

44

45

4190

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

46

4190

            visit_statefrm_rec(body, function)?;

47

48

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

49

            visit_statefrm_rec(body, function)?;

50

51

17861

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

52

17861

            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

7917

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

72

73

74

    // The visitor did not break the traversal.

75

35816

    Ok(None)

76

35816

77

78

79

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

80

where

81

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

82

83

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

84

        // The visitor requested to break the traversal.

85

        return Ok(Some(result));

86

87

88

    match sort_expr {

89

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

90

            visit_sort_expr_rec(lhs, function)?;

91

            visit_sort_expr_rec(rhs, function)?;

92

93

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

94

            visit_sort_expr_rec(domain, function)?;

95

            visit_sort_expr_rec(range, function)?;

96

97

        SortExpression::Struct { inner } => {

98

            for constructors in inner {

99

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

100

                    visit_sort_expr_rec(sort, function)?;

101

102

103

104

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

105

            visit_sort_expr_rec(sort_expression, function)?;

106

107

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

108

109

110

    // The visitor did not break the traversal.

111

    Ok(None)

112

113

114

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

115

4462

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

116

4462

where

117

4462

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

118

119

4462

    visit_regular_formula_rec(formula, &mut function)

120

4462

121

122

/// See [visit_regular_formula].

123

6486

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

124

6486

where

125

6486

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

126

127

6486

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

128

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

129

        return Ok(Some(result));

130

6486

131

132

6486

    match formula {

133

2024

        RegFrm::Iteration(reg_frm) => {

134

2024

            visit_regular_formula_rec(reg_frm, visit)?;

135

136

        RegFrm::Plus(reg_frm) => {

137

            visit_regular_formula_rec(reg_frm, visit)?;

138

139

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

140

            visit_regular_formula_rec(lhs, visit)?;

141

            visit_regular_formula_rec(rhs, visit)?;

142

143

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

144

            visit_regular_formula_rec(lhs, visit)?;

145

            visit_regular_formula_rec(rhs, visit)?;

146

147

4462

        _ => {}

148

149

150

6486

    Ok(None)

151

6486

152

153

/// Visitor for action formulas.

154

///

155

4462

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

156

4462

where

157

4462

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

158

159

4462

    visit_action_formula_rec(formula, &mut visitor)

160

4462

161

162

4462

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

163

4462

where

164

4462

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

165

166

4462

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

167

        // The visitor requested to break the traversal.

168

        return Ok(Some(result));

169

4462

170

171

4462

    match formula {

172

        ActFrm::Negation(act_frm) => {

173

            visit_action_formula_rec(act_frm, visitor)?;

174

175

        ActFrm::Quantifier {

176

            quantifier: _,

177

            variables: _,

178

            body,

179

        } => {

180

            visit_action_formula_rec(body, visitor)?;

181

182

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

183

            visit_action_formula_rec(lhs, visitor)?;

184

            visit_action_formula_rec(rhs, visitor)?;

185

186

4462

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

187

188

189

    // The visitor did not break the traversal.

190

4462

    Ok(None)

191

4462