Grcov report - substitution.rs

1

#![forbid(unsafe_code)]

2

3

use merc_aterm::ATerm;

4

use merc_aterm::ATermRef;

5

use merc_aterm::Protected;

6

use merc_aterm::Term;

7

use merc_aterm::storage::ThreadTermPool;

8

9

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

10

11

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

12

///

13

/// # Parameters

14

/// 't'             -   The original term

15

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

16

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

17

///                     given as a slice of position indexes

18

///

19

/// # Example

20

///

21

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

22

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

23

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

24

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

25

1

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

26

1

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

27

1

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

28

1

29

30

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

31

    builder: &mut SubstitutionBuilder,

32

    tp: &ThreadTermPool,

33

    t: &'b T,

34

    new_subterm: ATerm,

35

    p: &[usize],

36

) -> ATerm {

37

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

38

39

40

/// The recursive implementation for subsitute.

41

///

42

/// # Details

43

///

44

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

45

/// 'depth' = 0.

46

3

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

47

3

    tp: &ThreadTermPool,

48

3

    t: &'b T,

49

3

    new_subterm: ATerm,

50

3

    p: &[usize],

51

3

    args: &mut SubstitutionBuilder,

52

3

    depth: usize,

53

3

) -> ATerm {

54

3

    if p.len() == depth {

55

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

56

1

        new_subterm

57

    } else {

58

        // else recurse deeper into 't'

59

2

        let new_child_index = p[depth] - 1;

60

2

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

61

62

2

        let mut write_args = args.write();

63

2

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

64

2

            if index == new_child_index {

65

2

                let t = write_args.protect(&new_child);

66

2

                write_args.push(t);

67

2

            } else {

68

                let t = 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 super::*;

85

86

    use merc_aterm::storage::THREAD_TERM_POOL;

87

88

    use crate::utilities::ExplicitPosition;

89

    use crate::utilities::PositionIndexed;

90

91

    #[test]

92

1

    fn test_substitute() {

93

1

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

94

1

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

95

96

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

97

1

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

98

99

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

100

1

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

101

1

102