pub fn is_data_variable(term: &ATermRef<'_>) -> bool {

    term.require_valid();

    unsafe { ffi::is_data_variable(term.get()) }

}

pub fn is_data_expression(term: &ATermRef<'_>) -> bool {

    term.require_valid();

    is_data_variable(term)

        || is_data_function_symbol(term)

        || is_data_machine_number(term)

        || is_data_application(term)

        || is_data_abstraction(term)

        || is_data_where_clause(term)

}

pub fn is_data_function_symbol(term: &ATermRef<'_>) -> bool {

    term.require_valid();

    unsafe { ffi::is_data_function_symbol(term.get()) }

}

pub fn is_data_machine_number(term: &ATermRef<'_>) -> bool {

    term.require_valid();

    unsafe { ffi::is_data_machine_number(term.get()) }

}

pub fn is_data_where_clause(term: &ATermRef<'_>) -> bool {

    term.require_valid();

    unsafe { ffi::is_data_where_clause(term.get()) }

}

pub fn is_data_abstraction(term: &ATermRef<'_>) -> bool {

    term.require_valid();

    unsafe { ffi::is_data_abstraction(term.get()) }

}

pub fn is_data_untyped_identifier(term: &ATermRef<'_>) -> bool {

    term.require_valid();

    unsafe { ffi::is_data_untyped_identifier(term.get()) }

}

pub fn is_data_application(term: &ATermRef<'_>) -> bool {

    term.require_valid();

    THREAD_TERM_POOL.with_borrow_mut(|tp| tp.is_data_application(term))

}

#[mcrl2_derive_terms]

        pub fn data_function_symbol(&self) -> DataFunctionSymbolRef<'_> {

            if is_data_application(&self.term) {

                self.term.arg(0).upgrade(&self.term).into()

            } else if is_data_function_symbol(&self.term) {

                self.term.copy().into()

        }

        pub fn data_arguments(&self) -> ATermArgs<'_> {

            if is_data_application(&self.term) {

                let mut result = self.term.arguments();

                result.next();

                result

            } else if is_data_function_symbol(&self.term) {

                Default::default()

        }

        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

            if is_data_function_symbol(&self.term) {

                write!(f, "{}", DataFunctionSymbolRef::from(self.term.copy()))

        }

        pub fn new(tp: &mut TermPool, name: &str) -> DataFunctionSymbol {

            DataFunctionSymbol {

                term: tp.create_with(|| mcrl2_sys::data::ffi::create_data_function_symbol(name.to_string())),

            }

        }

        pub fn name(&self) -> &str {

            // We only change the lifetime, but that is fine since it is derived from the current term.

            unsafe { std::mem::transmute(self.term.arg(0).get_head_symbol().name()) }

        }

        pub fn operation_id(&self) -> usize {

            debug_assert!(

                is_data_function_symbol(&self.term),

            unsafe { ffi::get_data_function_symbol_index(self.term.get()) }

        }

        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

            if !self.is_default() {

                write!(f, "{}", self.name())

        }

        pub fn new(tp: &mut TermPool, name: &str) -> DataVariable {

            DataVariable {

                term: tp.create_with(|| mcrl2_sys::data::ffi::create_data_variable(name.to_string())),

            }

        }

        pub fn name(&self) -> &str {

            // We only change the lifetime, but that is fine since it is derived from the current term.

            unsafe { std::mem::transmute(self.term.arg(0).get_head_symbol().name()) }

        }

        pub fn new<'a, 'b>(

            tp: &mut TermPool,

            head: &impl Borrow<ATermRef<'a>>,

            arguments: &[impl Borrow<ATermRef<'b>>],

        ) -> DataApplication {

            DataApplication {

                term: tp.create_data_application(head, arguments),

            }

        }

        pub fn data_function_symbol(&self) -> DataFunctionSymbolRef<'_> {

            self.term.arg(0).upgrade(&self.term).into()

        }

        pub fn data_arguments(&self) -> ATermArgs<'_> {

            let mut result = self.term.arguments();

            result.next();

            result

        }

        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {

            write!(f, "{}", self.data_function_symbol())?;

            let mut first = true;

            for arg in self.data_arguments() {

                if !first {

                    write!(f, "(")?;

                write!(f, "{}", DataExpressionRef::from(arg.copy()))?;

                first = false;

            if !first {

                write!(f, ")")?;

            Ok(())

        }

        fn from(value: DataFunctionSymbol) -> Self {

            value.term.into()

        }

        fn from(value: DataApplication) -> Self {

            value.term.into()

        }

    fn test_print() {

        let mut tp = TermPool::new();

        let a = DataFunctionSymbol::new(&mut tp, "a");

        assert_eq!("a", format!("{}", a));

        let f = DataFunctionSymbol::new(&mut tp, "f");

        let a_term: ATerm = a.clone().into();

        let appl = DataApplication::new(&mut tp, &f, &[a_term]);

        assert_eq!("f(a)", format!("{}", appl));

    }

    fn test_recognizers() {

        let mut tp = TermPool::new();

        let a = DataFunctionSymbol::new(&mut tp, "a");

        let f = DataFunctionSymbol::new(&mut tp, "f");

        let a_term: ATerm = a.clone().into();

        let appl = DataApplication::new(&mut tp, &f, &[a_term]);

        let term: ATerm = appl.into();

        assert!(is_data_application(&term));

    }