Grcov report - substitution.rs

1

use merc_aterm::ATerm;

2

use merc_aterm::ATermRef;

3

use merc_aterm::Protected;

4

use merc_aterm::Term;

5

use merc_aterm::storage::ThreadTermPool;

6

7

pub type SubstitutionBuilder = Protected<Vec<ATermRef<'static>>>;

8

9

/// Creates a new term where a subterm is replaced with another term.

10

///

11

/// # Parameters

12

/// 't'             -   The original term

13

/// 'new_subterm'   -   The subterm that will be injected

14

/// 'p'             -   The place in 't' on which 'new_subterm' will be placed,

15

///                     given as a slice of position indexes

16

///

17

/// # Example

18

///

19

/// The term is constructed bottom up. As an example take the term s(s(a)).

20

/// Lets say we want to replace the a with the term 0. Then we traverse the term

21

/// until we have arrived at a and replace it with 0. We then construct s(0)

22

/// and then construct s(s(0)).

23

1

pub fn substitute<'a, 'b, T: Term<'a, 'b>>(tp: &ThreadTermPool, t: &'b T, new_subterm: ATerm, p: &[usize]) -> ATerm {

24

1

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

25

1

    substitute_rec(tp, t, new_subterm, p, &mut args, 0)

26

1

27

28

pub fn substitute_with<'a, 'b, T: Term<'a, 'b>>(

29

    builder: &mut SubstitutionBuilder,

30

    tp: &ThreadTermPool,

31

    t: &'b T,

32

    new_subterm: ATerm,

33

    p: &[usize],

34

) -> ATerm {

35

    substitute_rec(tp, t, new_subterm, p, builder, 0)

36

37

38

/// The recursive implementation for substitute.

39

///

40

/// # Details

41

///

42

/// The `depth` keeps track of the depth in 't'. Function should be called with

43

/// 'depth' = 0.

44

3

fn substitute_rec<'a, 'b, T: Term<'a, 'b>>(

45

3

    tp: &ThreadTermPool,

46

3

    t: &'b T,

47

3

    new_subterm: ATerm,

48

3

    p: &[usize],

49

3

    args: &mut SubstitutionBuilder,

50

3

    depth: usize,

51

3

) -> ATerm {

52

3

    if p.len() == depth {

53

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

54

1

        new_subterm

55

    } else {

56

        // else recurse deeper into 't'

57

2

        let new_child_index = p[depth] - 1;

58

2

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

59

60

2

        let mut write_args = args.write();

61

2

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

62

2

            if index == new_child_index {

63

2

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

64

2

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

65

2

                write_args.push(t);

66

2

            } else {

67

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

68

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

69

                write_args.push(t);

70

71

72

73

2

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

74

2

        drop(write_args);

75

76

        // Clear the args buffer for reuse.

77

2

        args.write().clear();

78

2

        result.protect()

79

80

3

81

82

#[cfg(test)]

83

mod tests {

84

    use merc_aterm::ATerm;

85

    use merc_aterm::Term;

86

    use merc_aterm::storage::THREAD_TERM_POOL;

87

88

    use crate::utilities::ExplicitPosition;

89

    use crate::utilities::PositionIndexed;

90

91

    use super::substitute;

92

93

    #[test]

94

1

    fn test_substitute() {

95

1

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

96

1

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

97

98

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

99

1

        let result = THREAD_TERM_POOL.with(|tp| substitute(tp, &t, t0.clone(), &[1, 1]));

100

101

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

102

1

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

103

1

104