Grcov report - data.rs

1

#[cxx::bridge(namespace = "mcrl2::data")]

2

#[allow(clippy::missing_safety_doc)]

3

pub mod ffi {

4

5

    unsafe extern "C++" {

6

        include!("mcrl2-sys/cpp/data/data.h");

7

8

        type data_specification;

9

10

        #[namespace = "mcrl2::data::detail"]

11

        type RewriterJitty;

12

13

        #[namespace = "mcrl2::data::detail"]

14

        type RewriterCompilingJitty;

15

16

        #[namespace = "atermpp"]

17

        type aterm = crate::atermpp::ffi::aterm;

18

19

        #[namespace = "atermpp::detail"]

20

        type _aterm = crate::atermpp::ffi::_aterm;

21

22

        /// Parses the given text into a data specification.

23

        fn parse_data_specification(text: &str) -> Result<UniquePtr<data_specification>>;

24

25

        /// Parses the given text and typechecks it using the given data specification

26

        fn parse_data_expression(text: &str, data_spec: &data_specification) -> Result<UniquePtr<aterm>>;

27

28

        /// Parses the given text v: Sort as a variable and typechecks it using the given data specification

29

        fn parse_variable(text: &str, data_spec: &data_specification) -> Result<UniquePtr<aterm>>;

30

31

        /// Returns the data equations for the given specification.

32

168

        fn get_data_specification_equations(data_spec: &data_specification) -> UniquePtr<CxxVector<aterm>>;

33

34

        /// Returns the data constructors for the given sort.

35

        unsafe fn get_data_specification_constructors(

36

            data_spec: &data_specification,

37

            sort: *const _aterm,

38

        ) -> UniquePtr<CxxVector<aterm>>;

39

40

        /// Creates an instance of the jitty rewriter.

41

8

        fn create_jitty_rewriter(data_spec: &data_specification) -> UniquePtr<RewriterJitty>;

42

43

        /// Creates an instance of the compiling jitty rewriter.

44

        fn create_jitty_compiling_rewriter(data_spec: &data_specification) -> UniquePtr<RewriterCompilingJitty>;

45

46

        /// Rewrites the given term to normal form.

47

8

        unsafe fn rewrite(rewriter: Pin<&mut RewriterJitty>, term: *const _aterm) -> UniquePtr<aterm>;

48

49

        /// Clone the data specification

50

160

        fn data_specification_clone(data_spec: &data_specification) -> UniquePtr<data_specification>;

51

52

        /// Obtain the index assigned internally to every data function symbol.

53

243485840

        unsafe fn get_data_function_symbol_index(term: *const _aterm) -> usize;

54

55

        /// Create the data::true term

56

62064

        fn true_term() -> UniquePtr<aterm>;

57

58

        /// Create the data::false term

59

        fn false_term() -> UniquePtr<aterm>;

60

61

        // For data::variable

62

641643184

        unsafe fn is_data_variable(term: *const _aterm) -> bool;

63

64

        /// Creates an unsorted data variable, must be within in a critical section.

65

15352

        fn create_data_variable(name: String) -> *const _aterm;

66

67

        /// Creates an sorted data variable, must be within in a critical section.

68

        unsafe fn create_sorted_data_variable(name: String, sort: *const _aterm) -> *const _aterm;

69

70

        // For data::function_symbol

71

7079936064

        unsafe fn is_data_function_symbol(term: *const _aterm) -> bool;

72

73

        /// Creates an unprotected data function symbol, must be within in a critical section.

74

162288

        fn create_data_function_symbol(name: String) -> *const _aterm;

75

76

        // For data::sort_expression

77

        unsafe fn is_data_sort_expression(term: *const _aterm) -> bool;

78

        unsafe fn is_data_basic_sort(term: *const _aterm) -> bool;

79

        unsafe fn is_data_function_sort(term: *const _aterm) -> bool;

80

81

        // For data::data_expression

82

4123576

        unsafe fn is_data_where_clause(term: *const _aterm) -> bool;

83

4126376

        unsafe fn is_data_abstraction(term: *const _aterm) -> bool;

84

3768304

        unsafe fn is_data_untyped_identifier(term: *const _aterm) -> bool;

85

513727888

        unsafe fn is_data_machine_number(term: *const _aterm) -> bool;

86

87