Grcov report - builder.rs

1

use merc_utilities::MercError;

2

3

use crate::RegFrm;

4

use crate::SortExpression;

5

use crate::StateFrm;

6

7

/// Applies the given function recursively to the state formula.

8

///

9

/// The substitution `function` takes a state formula and returns an optional new

10

/// formula. If it returns `Some(new_formula)`, the substitution is applied and

11

/// the new formula is returned. If it returns `None`, the substitution is not

12

/// applied and the function continues to traverse the formula tree.

13

12789

pub fn apply_statefrm<F>(formula: StateFrm, mut function: F) -> Result<StateFrm, MercError>

14

12789

where

15

12789

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

16

17

12789

    apply_statefrm_rec(formula, &mut function)

18

12789

19

20

/// Applies the given function recursively to the sort expression.

21

10

pub fn apply_sort_expression<E, F>(sort_expr: SortExpression, mut function: F) -> Result<SortExpression, E>

22

10

where

23

10

    F: FnMut(&SortExpression) -> Result<Option<SortExpression>, E>,

24

25

10

    apply_sort_expression_rec(sort_expr, &mut function)

26

10

27

28

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

29

///

30

/// # Details

31

///

32

/// The substitution function is a partial function, where `Some(formula)`

33

/// indicates that substitution should be applied.

34

pub fn apply_regular_formula<F>(formula: RegFrm, mut function: F) -> Result<RegFrm, MercError>

35

where

36

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

37

38

    apply_regular_formula_rec(formula, &mut function)

39

40

41

/// See [apply_regular_formula].

42

fn apply_regular_formula_rec<F>(formula: RegFrm, apply: &mut F) -> Result<RegFrm, MercError>

43

where

44

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

45

46

    if let Some(formula) = apply(&formula)? {

47

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

48

        return Ok(formula);

49

50

51

    match formula {

52

        RegFrm::Iteration(reg_frm) => {

53

            let new_reg_frm = apply_regular_formula_rec(*reg_frm, apply)?;

54

            Ok(RegFrm::Iteration(Box::new(new_reg_frm)))

55

56

        RegFrm::Plus(reg_frm) => {

57

            let new_reg_frm = apply_regular_formula_rec(*reg_frm, apply)?;

58

            Ok(RegFrm::Plus(Box::new(new_reg_frm)))

59

60

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

61

            let new_lhs = apply_regular_formula_rec(*lhs, apply)?;

62

            let new_rhs = apply_regular_formula_rec(*rhs, apply)?;

63

            Ok(RegFrm::Sequence {

64

                lhs: Box::new(new_lhs),

65

                rhs: Box::new(new_rhs),

66

})

67

68

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

69

            let new_lhs = apply_regular_formula_rec(*lhs, apply)?;

70

            let new_rhs = apply_regular_formula_rec(*rhs, apply)?;

71

            Ok(RegFrm::Choice {

72

                lhs: Box::new(new_lhs),

73

                rhs: Box::new(new_rhs),

74

})

75

76

        _ => Ok(formula),

77

78

79

80

/// See [`apply_statefrm`].

81

61803

fn apply_statefrm_rec<F>(formula: StateFrm, apply: &mut F) -> Result<StateFrm, MercError>

82

61803

where

83

61803

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

84

85

61803

    if let Some(formula) = apply(&formula)? {

86

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

87

8062

        return Ok(formula);

88

53741

89

90

53741

    match formula {

91

12331

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

92

12331

            let new_lhs = apply_statefrm_rec(*lhs, apply)?;

93

12331

            let new_rhs = apply_statefrm_rec(*rhs, apply)?;

94

12331

            Ok(StateFrm::Binary {

95

12331

op,

96

12331

                lhs: Box::new(new_lhs),

97

12331

                rhs: Box::new(new_rhs),

98

12331

})

99

100

        StateFrm::FixedPoint {

101

5000

            operator,

102

5000

            variable,

103

5000

            body,

104

        } => {

105

5000

            let new_body = apply_statefrm_rec(*body, apply)?;

106

5000

            Ok(StateFrm::FixedPoint {

107

5000

                operator,

108

5000

                variable,

109

5000

                body: Box::new(new_body),

110

5000

})

111

112

        StateFrm::Bound { bound, variables, body } => {

113

            let new_body = apply_statefrm_rec(*body, apply)?;

114

            Ok(StateFrm::Bound {

115

                bound,

116

                variables,

117

                body: Box::new(new_body),

118

})

119

120

        StateFrm::Modality {

121

19352

            operator,

122

19352

            formula,

123

19352

            expr,

124

        } => {

125

19352

            let expr = apply_statefrm_rec(*expr, apply)?;

126

19352

            Ok(StateFrm::Modality {

127

19352

                operator,

128

19352

                formula,

129

19352

                expr: Box::new(expr),

130

19352

})

131

132

        StateFrm::Quantifier {

133

            quantifier,

134

            variables,

135

            body,

136

        } => {

137

            let new_body = apply_statefrm_rec(*body, apply)?;

138

            Ok(StateFrm::Quantifier {

139

                quantifier,

140

                variables,

141

                body: Box::new(new_body),

142

})

143

144

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

145

            let new_expr = apply_statefrm_rec(*expr, apply)?;

146

            Ok(StateFrm::DataValExprRightMult(Box::new(new_expr), data_val))

147

148

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

149

            let new_expr = apply_statefrm_rec(*expr, apply)?;

150

            Ok(StateFrm::DataValExprLeftMult(data_val, Box::new(new_expr)))

151

152

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

153

            let new_expr = apply_statefrm_rec(*expr, apply)?;

154

            Ok(StateFrm::Unary {

155

op,

156

                expr: Box::new(new_expr),

157

})

158

159

        StateFrm::Id(_, _)

160

        | StateFrm::True

161

        | StateFrm::False

162

        | StateFrm::Delay(_)

163

        | StateFrm::Yaled(_)

164

17058

        | StateFrm::DataValExpr(_) => Ok(formula),

165

166

61803

167

168

/// See [`apply_sort_expression`].

169

14

fn apply_sort_expression_rec<E, F>(sort_expr: SortExpression, apply: &mut F) -> Result<SortExpression, E>

170

14

where

171

14

    F: FnMut(&SortExpression) -> Result<Option<SortExpression>, E>,

172

173

14

    if let Some(sort_expr) = apply(&sort_expr)? {

174

        // A substitution was made, return the new sort expression.

175

8

        return Ok(sort_expr);

176

6

177

178

6

    match sort_expr {

179

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

180

            let lhs = apply_sort_expression_rec(*lhs, apply)?;

181

            let rhs = apply_sort_expression_rec(*rhs, apply)?;

182

            Ok(SortExpression::Product {

183

                lhs: Box::new(lhs),

184

                rhs: Box::new(rhs),

185

})

186

187

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

188

            let domain = apply_sort_expression_rec(*domain, apply)?;

189

            let range = apply_sort_expression_rec(*range, apply)?;

190

            Ok(SortExpression::Function {

191

                domain: Box::new(domain),

192

                range: Box::new(range),

193

})

194

195

        SortExpression::Struct { mut inner } => {

196

            for decl in &mut inner {

197

                for (_, sort) in &mut decl.args {

198

                    *sort = apply_sort_expression_rec(sort.clone(), apply)?;

199

200

201

202

            Ok(SortExpression::Struct { inner })

203

204

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

205

            let inner = apply_sort_expression_rec(*sort_expression, apply)?;

206

            Ok(SortExpression::Complex(complex_sort, Box::new(inner)))

207

208

2

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

209

2

            let domain = domain

210

2

                .into_iter()

211

2

                .map(|sort| apply_sort_expression_rec(sort, apply))

212

2

                .collect::<Result<Vec<SortExpression>, _>>()?;

213

2

            let range = apply_sort_expression_rec(*range, apply)?;

214

2

            Ok(SortExpression::FlattenedFunction {

215

2

                domain,

216

2

                range: Box::new(range),

217

2

})

218

219

        SortExpression::Reference(_) | SortExpression::Simple(_) | SortExpression::Resolved(_, _) => {

220

            // Ignored

221

4

            Ok(sort_expr)

222

223

224

14

225

226

#[cfg(test)]

227

mod tests {

228

    use std::vec;

229

230

    use crate::StateFrm;

231

    use crate::UntypedStateFrmSpec;

232

233

    use super::apply_statefrm;

234

235

    #[test]

236

1

    fn test_visit_state_frm_variables() {

237

1

        let input = UntypedStateFrmSpec::parse("mu X. [a]X && mu X. X && Y").unwrap();

238

239

1

        let mut variables = vec![];

240

8

        apply_statefrm(input.formula, |frm| {

241

8

            if let StateFrm::Id(name, _) = frm {

242

3

                variables.push(name.clone());

243

5

244

245

8

            Ok(None)

246

8

})

247

1

        .unwrap();

248

249

1

        assert_eq!(variables, vec!["X", "X", "Y"]);

250

1

251