pub fn substitute(tp: &mut TermPool, t: &ATermRef<'_>, new_subterm: ATerm, p: &[usize]) -> ATerm {

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

    substitute_rec(tp, t, new_subterm, p, &mut args, 0)

}

pub fn substitute_with(

    builder: &mut SubstitutionBuilder,

    tp: &mut TermPool,

    t: &ATermRef<'_>,

    new_subterm: ATerm,

    p: &[usize],

) -> ATerm {

    substitute_rec(tp, t, new_subterm, p, builder, 0)

}

fn substitute_rec(

    tp: &mut TermPool,

    t: &ATermRef<'_>,

    new_subterm: ATerm,

    p: &[usize],

    args: &mut Protected<Vec<ATermRef<'static>>>,

    depth: usize,

) -> ATerm {

    if p.len() == depth {

        new_subterm

        let new_child_index = p[depth] - 1;

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

        let mut write_args = args.write();

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

            if index == new_child_index {

                let t = write_args.protect(&new_child);

                write_args.push(t);

            } else {

                let t = write_args.protect(&arg);

                write_args.push(t);

            }

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

        drop(write_args);

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

        args.write().clear();

        result

}

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

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

    builder

        .evaluate(

            tp,

            t.clone(),

            |tp, args, t| {

                debug_assert!(!t.is_int(), "Term cannot be an aterm_int, although not sure why");

                if variables.contains(t.get_head_symbol().name()) {

                    Ok(Yield::Term(DataVariable::new(tp, t.get_head_symbol().name()).into()))

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

                    Ok(Yield::Term(

                        DataFunctionSymbol::new(tp, t.get_head_symbol().name()).into(),

                    ))

                    let head = DataFunctionSymbol::new(tp, t.get_head_symbol().name());

                    for arg in t.arguments() {

                        args.push(arg.protect());

                    }

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

            },

            |tp, input, args| Ok(tp.create_data_application(&input, args)),

        )

        .unwrap()

        .into()

}

    fn test_substitute() {

        let mut term_pool = TermPool::new();

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

        let t0 = term_pool.from_string("0").unwrap();

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

        let result = substitute(&mut term_pool, &t, t0.clone(), &vec![1, 1]);

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

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

    }

    fn test_to_data_expression() {

        let mut term_pool = TermPool::new();

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

        let _expression = to_untyped_data_expression(&mut term_pool, &t, &AHashSet::from_iter(["a".to_string()]));

    }