pub fn integrate(

        write_configs: &mut Protector<Vec<Config>>,

        write_terms: &mut Protector<Vec<DataExpressionRef<'static>>>,

        rhs_stack: &RHSStack,

        term: &DataExpression,

        result_index: usize,

    ) {

        // TODO: This ignores the first element of the stack, but that is kind of difficult to deal with.

        let top_of_stack = write_terms.len();

        write_terms.reserve(rhs_stack.stack_size - 1); // We already reserved space for the result.

        for _ in 0..rhs_stack.stack_size - 1 {

            write_terms.push(Default::default());

        }

        let mut first = true;

        for config in rhs_stack.innermost_stack.read().iter() {

            match config {

                Config::Construct(symbol, arity, offset) => {

                    if first {

                        // The first result must be placed on the original result index.

                        InnermostStack::add_result(write_configs, symbol.copy(), *arity, result_index);

                    } else {

                        // Otherwise, we put it on the end of the stack.

                        InnermostStack::add_result(write_configs, symbol.copy(), *arity, top_of_stack + offset - 1);

                    }

            first = false;

        trace!(

        debug_assert!(

            rhs_stack.stack_size != 1 || rhs_stack.variables.len() <= 1,

        if rhs_stack.stack_size == 1 && rhs_stack.variables.len() == 1 {

            // This is a special case where we place the result on the correct position immediately.

            // The right hand side is only a variable

            let t: ATermRef<'_> = write_terms.protect(&term.get_position(&rhs_stack.variables[0].0));

            write_terms[result_index] = t.into();

        } else {

            for (position, index) in &rhs_stack.variables {

                // Add the positions to the stack.

                let t = write_terms.protect(&term.get_position(position));

                write_terms[top_of_stack + index - 1] = t.into();

            }

    }

    pub fn add_result(

        write_configs: &mut Protector<Vec<Config>>,

        symbol: DataFunctionSymbolRef<'_>,

        arity: usize,

        index: usize,

    ) {

        let symbol = write_configs.protect(&symbol.into());

        write_configs.push(Config::Construct(symbol.into(), arity, index));

    }

    pub fn add_rewrite(

        write_configs: &mut Protector<Vec<Config>>,

        write_terms: &mut Protector<Vec<DataExpressionRef<'static>>>,

        term: DataExpressionRef<'_>,

        index: usize,

    ) {

        let term = write_terms.protect(&term);

        write_configs.push(Config::Rewrite(index));

        write_terms.push(term.into());

    }

    fn contains_term(&self, term: &ATermRef<'_>) -> bool {

        if let Config::Construct(t, _, _) = self {

            term == &<DataFunctionSymbolRef as Into<ATermRef>>::into(t.copy())

            false

    }

    pub fn new(rule: &Rule) -> RHSStack {

        let var_map = create_var_map(&rule.lhs.clone().into());

        // Compute the extra information for the InnermostRewriter.

        let mut innermost_stack: Protected<Vec<Config>> = Protected::new(vec![]);

        let mut variables = vec![];

        let mut stack_size = 0;

        for (term, position) in PositionIterator::new(rule.rhs.copy().into()) {

            if let Some(index) = position.indices.last() {

                if *index == 1 {

                    continue; // Skip the function symbol.

                }

            }

            if is_data_variable(&term) {

                variables.push((

                    var_map

                        .get(&term.protect())

                        .expect("All variables in the right hand side must occur in the left hand side")

                        .clone(),

                    stack_size,

                ));

                stack_size += 1;

            } else if is_data_machine_number(&term) {

                // Skip SortId(@NoValue) and OpId

            } else if is_data_expression(&term) {

                let t: DataExpressionRef = term.into();

                let arity = t.data_arguments().len();

                let mut write = innermost_stack.write();

                let symbol = write.protect(&t.data_function_symbol().into());

                write.push(Config::Construct(symbol.into(), arity, stack_size));

                stack_size += 1;

            } else {

                // Skip intermediate terms such as UntypeSortUnknown.

            }

        RHSStack {

            innermost_stack,

            stack_size,

            variables,

        }

    }

    pub fn evaluate(&self, tp: &mut TermPool, term: &DataExpression) -> DataExpression {

        let mut stack = InnermostStack::default();

        stack.terms.write().push(DataExpressionRef::default());

        InnermostStack::integrate(&mut stack.configs.write(), &mut stack.terms.write(), self, term, 0);

            trace!("{}", stack);

            let mut write_configs = stack.configs.write();

            if let Some(config) = write_configs.pop() {

                match config {

                    Config::Construct(symbol, arity, index) => {

                        // Take the last arity arguments.

                        let mut write_terms = stack.terms.write();

                        let length = write_terms.len();

                        let arguments = &write_terms[length - arity..];

                        let term: DataExpression = if arguments.is_empty() {

                            DataApplication::new(tp, &symbol.copy(), arguments).into()

                        write_terms.drain(length - arity..);

                        let t = write_terms.protect(&term);

                        write_terms[index] = t.into();

                break;

            }

        }

        debug_assert!(

            stack.terms.read().len() == 1,

        let mut write_terms = stack.terms.write();

        write_terms

            .pop()

            .expect("The result should be the last element on the stack")

            .protect()

    }

    #[test]

    #[test]