Grcov report - data_substitution.rs

1

#![forbid(unsafe_code)]

2

3

use merc_aterm::Protected;

4

use merc_aterm::Term;

5

use merc_aterm::storage::ThreadTermPool;

6

use merc_data::DataExpression;

7

use merc_data::DataExpressionRef;

8

use merc_data::is_data_application;

9

10

use super::DataPosition;

11

12

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

13

14

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

15

1

pub fn data_substitute(

16

1

    tp: &ThreadTermPool,

17

1

    t: &DataExpressionRef<'_>,

18

1

    new_subterm: DataExpression,

19

1

    position: &DataPosition,

20

1

) -> DataExpression {

21

1

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

22

1

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

23

1

24

25

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

26

1292241

pub fn data_substitute_with(

27

1292241

    builder: &mut DataSubstitutionBuilder,

28

1292241

    tp: &ThreadTermPool,

29

1292241

    t: &DataExpressionRef<'_>,

30

1292241

    new_subterm: DataExpression,

31

1292241

    position: &DataPosition,

32

1292241

) -> DataExpression {

33

1292241

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

34

1292241

35

36

/// The recursive implementation for [data_substitute]

37

///

38

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

39

///                     'depth' = 0.

40

1467825

fn substitute_rec(

41

1467825

    tp: &ThreadTermPool,

42

1467825

    t: &DataExpressionRef<'_>,

43

1467825

    new_subterm: DataExpression,

44

1467825

    p: &[usize],

45

1467825

    args: &mut DataSubstitutionBuilder,

46

1467825

    depth: usize,

47

1467825

) -> DataExpression {

48

1467825

    if p.len() == depth {

49

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

50

1292242

        new_subterm

51

    } else {

52

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

53

175583

        let new_child_index = p[depth];

54

175583

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

55

56

175583

        debug_assert!(

57

175583

            is_data_application(t),

58

            "Can only perform data substitution on DataApplications"

59

);

60

61

175583

        let mut write_args = args.write();

62

623047

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

63

623047

            if index == new_child_index {

64

175583

                let t = write_args.protect(&new_child);

65

175583

                write_args.push(t.into());

66

447464

            } else {

67

447464

                let t = write_args.protect(&arg);

68

447464

                write_args.push(t.into());

69

447464

70

71

72

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

73

175583

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

74

175583

        drop(write_args);

75

76

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

77

175583

        args.write().clear();

78

175583

        result.protect().into()

79

80

1467825

81

82

#[cfg(test)]

83

mod tests {

84

    use super::*;

85

86

    use merc_aterm::storage::THREAD_TERM_POOL;

87

88

    use crate::utilities::DataPosition;

89

    use crate::utilities::DataPositionIndexed;

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_borrow(|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(&vec![1, 1])).protect());

102

1

103