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

            if is_data_application(&self.term) {

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

            } else if is_data_function_symbol(&self.term) {

                self.term.copy().into()

        }

        pub fn data_arguments(&self) -> impl ExactSizeIterator<Item = DataExpressionRef<'_>> + use<'_> {

            let skip = data_argument_skip_count(&self.term)

                .unwrap_or_else(|| panic!("data_arguments is not defined for binders and where clauses: {self}"));

            self.term.arguments().skip(skip).map(|t| t.into())

        }

        pub fn from_string(text: &str) -> Result<DataExpression, MercError> {

            Ok(to_untyped_data_expression(ATerm::from_string(text)?, None))

        }

        pub fn from_string_untyped(text: &str, variables: &AHashSet<String>) -> Result<DataExpression, MercError> {

            Ok(to_untyped_data_expression(ATerm::from_string(text)?, Some(variables)))

        }

        pub fn data_arg(&self, index: usize) -> DataExpressionRef<'_> {

            debug_assert!(is_data_application(self), "Term {self:?} is not a data application");

            debug_assert!(

                index + 1 < self.get_head_symbol().arity(),

            self.term.arg(index + 1).into()

        }

        pub fn data_sort(&self) -> SortExpression {

            if is_data_function_symbol(&self.term) {

            } else if is_data_variable(&self.term) {

                DataVariableRef::from(self.term.copy()).sort().protect()

        }

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

            if is_data_function_symbol(&self.term) {

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

            } else if is_data_application(&self.term) {

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

            } else if is_data_variable(&self.term) {

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

            } else if is_data_machine_number(&self.term) {

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

        }

        pub fn new<N>(name: N) -> DataFunctionSymbol

        where

            N: Into<ATermString> + AsRef<str>,

            DATA_SYMBOLS.with_borrow(|ds| DataFunctionSymbol {

                term: ATerm::with_args(

                    ds.data_function_symbol.deref(),

                    &[Into::<ATerm>::into(name.into()), SortExpression::unknown_sort().into()],

                )

                .protect(),

            })

        }

        pub fn name(&self) -> ATermStringRef<'_> {

            ATermStringRef::from(self.term.arg(0))

        }

        pub fn operation_id(&self) -> usize {

            self.term.index()

        }

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

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

        }

        pub fn new<N: Into<ATermString>>(name: N) -> DataVariable {

            DATA_SYMBOLS.with_borrow(|ds| {

                let t = name.into();

                let args: &[ATerm] = &[t.into(), SortExpression::unknown_sort().into()];

                DataVariable {

                    term: ATerm::with_args(ds.data_variable.deref(), args).protect(),

                }

            })

        }

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

            self.term.arg(0).get_head_symbol().name()

        }

        pub fn sort(&self) -> SortExpressionRef<'_> {

            self.term.arg(1).into()

        }

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

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

        }

        pub fn with_args<'a, 'b, H: Term<'a, 'b>, T: Term<'a, 'b>>(head: &'b H, arguments: &'b [T]) -> DataApplication {

            DATA_SYMBOLS.with_borrow_mut(|ds| {

                let symbol = ds.get_data_application_symbol(arguments.len() + 1).copy();

                let args = iter::once(head.copy()).chain(arguments.iter().map(|t| t.copy()));

                let term = ATerm::with_iter(&symbol, args);

                DataApplication { term }

            })

        }

        pub fn with_iter<'a, 'b, 'c, 'd, T, H, I>(head: &'b H, arity: usize, arguments: I) -> DataApplication

        where

            I: Iterator<Item = T>,

            T: Term<'c, 'd>,

            H: Term<'a, 'b>,

            DATA_SYMBOLS.with_borrow_mut(|ds| {

                let symbol = ds.get_data_application_symbol(arity + 1).copy();

                let term = ATerm::with_iter_head(&symbol, head, arguments);

                DataApplication { term }

            })

        }

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

            self.term.arg(0).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, "(")?;

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

                first = false;

            if !first {

                write!(f, ")")?;

            Ok(())

        }

        pub(crate) fn value(&self) -> u64 {

            Into::<ATermIntRef<'_>>::into(self.term.copy()).value() as u64

        }

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

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

        }

        fn from(value: DataFunctionSymbol) -> Self {

            value.term.into()

        }

        fn from(value: DataApplication) -> Self {

            value.term.into()

        }

        fn from(value: DataVariable) -> Self {

            value.term.into()

        }

        fn from(value: DataExpression) -> Self {

            value.term.into()

        }

        fn from(value: DataExpression) -> Self {

            value.term.into()

        }

        fn from(value: DataExpressionRef<'a>) -> Self {

            value.term.into()

        }

fn data_argument_skip_count<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> Option<usize> {

    if is_data_application(term) {

        Some(1)

    } else if is_data_function_symbol(term) || is_data_variable(term) {

        Some(2)

    } else if is_data_machine_number(term) {

        Some(0)

}

    pub fn data_arguments(&self) -> impl ExactSizeIterator<Item = DataExpressionRef<'a>> + use<'a> {

        let skip = data_argument_skip_count(&self.term)

            .unwrap_or_else(|| panic!("data_arguments is not defined for binders and where clauses: {self}"));

        self.term.arguments().skip(skip).map(|t| t.into())

    }

    pub fn data_arg(&self, index: usize) -> DataExpressionRef<'a> {

        debug_assert!(is_data_application(self), "Term {self:?} is not a data application");

        debug_assert!(

            index + 1 < self.get_head_symbol().arity(),

        self.term.arg(index + 1).into()

    }

pub fn to_untyped_data_expression(t: ATerm, variables: Option<&AHashSet<String>>) -> DataExpression {

    let mut builder = TermBuilder::<ATerm, ATerm>::new();

    THREAD_TERM_POOL.with(|tp| {

        builder

            .evaluate(

                tp,

                t,

                |_tp, args, t| {

                    let name = t.get_head_symbol().name();

                    if t.get_head_symbol().arity() == 0 {

                        if variables.is_some_and(|v| v.contains(name)) {

                            Ok(Yield::Term(DataVariable::new(name).into()))

                            Ok(Yield::Term(DataFunctionSymbol::new(name).into()))

                        let head = DataFunctionSymbol::new(name);

                        for arg in t.arguments() {

                            args.push(arg.protect());

                        }

                        Ok(Yield::Construct(head.into()))

                },

                |_tp, input, args| {

                    let args: Vec<ATerm> = args.cloned().collect();

                    Ok(DataApplication::with_args(&input, &args).into())

                },

            .unwrap()

            .into()

    })

}

    fn test_print() {

        merc_utilities::test_logger();

        let a = DataFunctionSymbol::new("a");

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

        let f = DataFunctionSymbol::new("f");

        let appl = DataApplication::with_args(&f, &[a]);

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

    }

    fn test_recognizers() {

        let a = DataFunctionSymbol::new("a");

        let f = DataFunctionSymbol::new("f");

        let appl = DataApplication::with_args(&f, &[a]);

        let term: ATerm = appl.into();

        assert!(is_data_application(&term));

    }

    fn test_data_arguments() {

        let a = DataFunctionSymbol::new("a");

        let f = DataFunctionSymbol::new("f");

        let appl = DataApplication::with_args(&f, &[a]);

        assert_eq!(appl.data_arguments().count(), 1);

        let data_expr: DataExpression = appl.clone().into();

        assert_eq!(data_expr.data_arguments().count(), 1);

    }

    fn test_to_data_expression() {

        let expression = DataExpression::from_string("s(s(a, b), c)").unwrap();

        assert_eq!(expression.data_arg(0).data_function_symbol().name(), "s");

        assert_eq!(expression.data_arg(0).data_arg(0).data_function_symbol().name(), "a");

    }

    fn test_machine_number() {

        let term: ATerm = ATermInt::new(42).into();

        assert!(is_data_machine_number(&term));

        let expr: DataExpression = term.into();

        assert_eq!(format!("{expr}"), "42");

        assert_eq!(expr.data_arguments().count(), 0);

    }

    fn test_variable_sort() {

        let var = DataVariable::new("x");

        assert_eq!(var.name(), "x");

        let expr: DataExpression = var.into();

        assert!(is_data_variable(&expr));

        assert_eq!(expr.data_sort().name(), "@no_value@");

        assert_eq!(expr.data_arguments().count(), 0);

    }

    fn test_from_string_untyped_variable() {

        let vars = AHashSet::from_iter(["x".to_string()]);

        let expr = DataExpression::from_string_untyped("f(x, a)", &vars).unwrap();

        assert!(is_data_variable(&expr.data_arg(0)));

        assert_eq!(expr.data_arg(1).data_function_symbol().name(), "a");

    }

    fn test_from_string_untyped_applied_identifier_keeps_args() {

        let vars = AHashSet::from_iter(["x".to_string()]);

        let expr = DataExpression::from_string_untyped("x(a)", &vars).unwrap();

        assert!(is_data_application(&expr));

        assert_eq!(expr.data_function_symbol().name(), "x");

        assert_eq!(expr.data_arguments().count(), 1);

    }