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 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>(tp: &ThreadTermPool, t: &'b impl Term<'a, 'b>, 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>(

31

    builder: &mut SubstitutionBuilder,

32

    tp: &ThreadTermPool,

33

    t: &'b impl Term<'a, 'b>,

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

/// 'depth'         -   Used to keep track of the depth in 't'. Function should be called with

43

///                     'depth' = 0.

44

3

fn substitute_rec<'a, 'b>(

45

3

    tp: &ThreadTermPool,

46

3

    t: &'b impl Term<'a, 'b>,

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

                let t = write_args.protect(&new_child);

64

2

                write_args.push(t);

65

2

            } else {

66

                let t = write_args.protect(&arg);

67

                write_args.push(t);

68

69

70

71

2

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

72

2

        drop(write_args);

73

74

        // TODO: When write is dropped we check whether all terms where inserted, but this clear violates that assumption.

75

2

        args.write().clear();

76

2

        result.protect()

77

78

3

79

80

#[cfg(test)]

81

mod tests {

82

    use super::*;

83

84

    use merc_aterm::storage::THREAD_TERM_POOL;

85

86

    use crate::utilities::ExplicitPosition;

87

    use crate::utilities::PositionIndexed;

88

89

    #[test]

90

1

    fn test_substitute() {

91

1

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

92

1

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

93

94

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

95

1

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

96

97

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

98

1

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

99

1

100