Grcov report - data_substitution.rs

1

use merc_aterm::Protected;

2

use merc_aterm::Term;

3

use merc_aterm::storage::ThreadTermPool;

4

use merc_data::DataExpression;

5

use merc_data::DataExpressionRef;

6

use merc_data::is_data_application;

7

8

use super::DataPosition;

9

10

pub type DataSubstitutionBuilder = Protected<Vec<DataExpressionRef<'static>>>;

11

12

/// This function substitutes the term 't' at the position 'p' with 'new_subterm', see [super::substitute].

13

1

pub fn data_substitute(

14

1

    tp: &ThreadTermPool,

15

1

    t: &DataExpressionRef<'_>,

16

1

    new_subterm: DataExpression,

17

1

    position: &DataPosition,

18

1

) -> DataExpression {

19

1

    let mut args = Protected::new(vec![]);

20

1

    substitute_rec(tp, t, new_subterm, position.indices(), &mut args, 0)

21

1

22

23

/// This is the same as [data_substitute], but it uses a [DataSubstitutionBuilder] to store the arguments temporarily.

24

3876234

pub fn data_substitute_with(

25

3876234

    builder: &mut DataSubstitutionBuilder,

26

3876234

    tp: &ThreadTermPool,

27

3876234

    t: &DataExpressionRef<'_>,

28

3876234

    new_subterm: DataExpression,

29

3876234

    position: &DataPosition,

30

3876234

) -> DataExpression {

31

3876234

    substitute_rec(tp, t, new_subterm, position.indices(), builder, 0)

32

3876234

33

34

/// The recursive implementation for [data_substitute]

35

///

36

/// Uses `depth` to keep track of the depth in 't', initially 0.

37

4402980

fn substitute_rec(

38

4402980

    tp: &ThreadTermPool,

39

4402980

    t: &DataExpressionRef<'_>,

40

4402980

    new_subterm: DataExpression,

41

4402980

    p: &[usize],

42

4402980

    args: &mut DataSubstitutionBuilder,

43

4402980

    depth: usize,

44

4402980

) -> DataExpression {

45

4402980

    if p.len() == depth {

46

        // in this case we have arrived at the place where 'new_subterm' needs to be injected

47

3876235

        new_subterm

48

    } else {

49

        // else recurse deeper into 't', do not subtract 1 from the index, since we are using DataPosition

50

526745

        let new_child_index = p[depth];

51

526745

        let new_child = substitute_rec(tp, &t.arg(new_child_index).into(), new_subterm, p, args, depth + 1);

52

53

526745

        debug_assert!(

54

526745

            is_data_application(t),

55

            "Can only perform data substitution on DataApplications"

56

);

57

58

526745

        let mut write_args = args.write();

59

1869133

        for (index, arg) in t.arguments().enumerate() {

60

1869133

            if index == new_child_index {

61

526745

                // Safety: t is pushed into the container on the next line.

62

526745

                let t = unsafe { write_args.protect(&new_child) };

63

526745

                write_args.push(t.into());

64

1342388

            } else {

65

1342388

                // Safety: t is pushed into the container on the next line.

66

1342388

                let t = unsafe { write_args.protect(&arg) };

67

1342388

                write_args.push(t.into());

68

1342388

69

70

71

        // Avoid the (more expensive) DataApplication constructor by simply having the data_function_symbol in args.

72

526745

        let result = tp.create_term(&t.get_head_symbol(), &write_args);

73

526745

        drop(write_args);

74

75

        // Clear the args buffer for reuse.

76

526745

        args.write().clear();

77

526745

        result.protect().into()

78

79

4402980

80

81

#[cfg(test)]

82

mod tests {

83

    use merc_aterm::storage::THREAD_TERM_POOL;

84

    use merc_data::DataExpression;

85

86

    use crate::utilities::DataPosition;

87

    use crate::utilities::DataPositionIndexed;

88

89

    use super::data_substitute;

90

91

    #[test]

92

1

    fn test_data_substitute() {

93

1

        let t = DataExpression::from_string("s(s(a))").unwrap();

94

1

        let t0 = DataExpression::from_string("0").unwrap();

95

96

        // substitute the a for 0 in the term s(s(a))

97

1

        let result =

98

1

            THREAD_TERM_POOL.with(|tp| data_substitute(tp, &t.copy(), t0.clone(), &DataPosition::new(&[1, 1])));

99

100

        // Check that indeed the new term as a 0 at position 1.1.

101

1

        assert_eq!(t0, result.get_data_position(&DataPosition::new(&[1, 1])).protect());

102

1

103