Grcov report - concat.rs

1

// rules for concatenations of subsetEq with intersect and union

2

// analogous rules for subset, supset and supsetEq are not needed because these are converted to subsetEq first.

3

use conjure_cp::ast::Metadata;

4

use conjure_cp::ast::{Expression as Expr, Moo, ReturnType, SymbolTable, Typeable};

5

use conjure_cp::matrix_expr;

6

use conjure_cp::rule_engine::Reduction;

7

use conjure_cp::rule_engine::{

8

    ApplicationError::RuleNotApplicable, ApplicationResult, register_rule,

9

};

10

11

// A subsetEq (B intersect C) -> A subsetEq B /\ A subsetEq C

12

#[register_rule(("Base", 8700))]

13

fn subseteq_intersect(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

14

    match expr {

15

        Expr::SubsetEq(_, a, rhs) if matches!(a.as_ref().return_type(), ReturnType::Set(_)) => {

16

            match rhs.as_ref() {

17

                Expr::Intersect(_, b, c)

18

                    if matches!(b.as_ref().return_type(), ReturnType::Set(_))

19

                        && matches!(c.as_ref().return_type(), ReturnType::Set(_)) =>

20

21

                    let expr1 = Expr::SubsetEq(Metadata::new(), a.clone(), b.clone());

22

                    let expr2 = Expr::SubsetEq(Metadata::new(), a.clone(), c.clone());

23

                    Ok(Reduction::pure(Expr::And(

24

                        Metadata::new(),

25

                        Moo::new(matrix_expr![expr1, expr2]),

26

)))

27

28

                _ => Err(RuleNotApplicable),

29

30

31

        _ => Err(RuleNotApplicable),

32

33

34

35

// (A union B) subsetEq C -> A subsetEq C /\ B subsetEq C

36

#[register_rule(("Base", 8700))]

37

fn union_subseteq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

38

    match expr {

39

        Expr::SubsetEq(_, lhs, c) if matches!(c.as_ref().return_type(), ReturnType::Set(_)) => {

40

            match lhs.as_ref() {

41

                Expr::Union(_, a, b)

42

                    if matches!(a.as_ref().return_type(), ReturnType::Set(_))

43

                        && matches!(b.as_ref().return_type(), ReturnType::Set(_)) =>

44

45

                    let expr1 = Expr::SubsetEq(Metadata::new(), a.clone(), b.clone());

46

                    let expr2 = Expr::SubsetEq(Metadata::new(), a.clone(), c.clone());

47

                    Ok(Reduction::pure(Expr::And(

48

                        Metadata::new(),

49

                        Moo::new(matrix_expr![expr1, expr2]),

50

)))

51

52

                _ => Err(RuleNotApplicable),

53

54

55

        _ => Err(RuleNotApplicable),

56

57