use std::fmt;

use ahash::HashMap;

use ahash::HashMapExt;

use merc_aterm::ATermRef;

use merc_aterm::Markable;

use merc_aterm::Protected;

use merc_aterm::SymbolRef;

use merc_aterm::Term;

use merc_aterm::Transmutable;

use merc_aterm::storage::Marker;

use merc_data::DataApplication;

use merc_data::DataExpression;

use merc_data::DataExpressionRef;

use merc_data::DataFunctionSymbolRef;

use merc_data::DataVariable;

use merc_data::DataVariableRef;

use merc_data::is_data_machine_number;

use merc_data::is_data_variable;

use merc_utilities::debug_trace;

use crate::Rule;

use crate::utilities::InnermostStack;

use super::DataPosition;

use super::DataPositionIterator;

/// A stack used to represent a term with free variables that can be constructed

/// efficiently.

///

/// It stores as much as possible in the term pool. Due to variables it cannot

/// be fully compressed. For variables it stores the position in the lhs of a

/// rewrite rule where the concrete term can be found that will replace the

/// variable.

///

#[derive(Hash, Debug, PartialEq, Eq, PartialOrd, Ord)]

pub struct TermStack {

    /// The innermost rewrite stack for the right hand side and the positions that must be added to the stack.

    pub innermost_stack: Protected<Vec<Config<'static>>>,

    /// The variables of the left-hand side that must be placed at certain places in the stack.

    pub variables: Vec<(DataPosition, usize)>,

    /// The number of elements that must be reserved on the innermost stack.

    pub stack_size: usize,

}

#[derive(Hash, Eq, PartialEq, Ord, PartialOrd, Debug)]

pub enum Config<'a> {

    /// Rewrite the top of the stack and put result at the given index.

    Rewrite(usize),

    /// Constructs function symbol with given arity at the given index.

    Construct(DataFunctionSymbolRef<'a>, usize, usize),

    /// A concrete term to be placed at the current position in the stack.

    Term(DataExpressionRef<'a>, usize),

    /// Yields the given index as returned term.

    Return(),

}

impl Markable for Config<'_> {

        } else {

        }

        } else {

        }

}

impl Transmutable for Config<'static> {

    type Target<'a> = Config<'a>;

}

impl fmt::Display for Config<'_> {

            }

            }

        }

}

impl TermStack {

    /// Construct a new right-hand stack for a given equation/rewrite rule.

    /// Construct a term stack from a data expression where variables are taken from a specific position of the left hand side.

        // Compute the extra information for the InnermostRewriter.

        }

    // See [evaluate_with]

    /// Evaluate the rhs stack for the given term and returns the result.

            0,

        );

        loop {

                        // Take the last arity arguments.

                        } else {

                        };

                        // Add the term on the stack.

                    }

                    Config::Rewrite(_) => {

                    }

                    Config::Return() => {

                    }

                }

            } else {

            }

        }

            "Expect exactly one term on the result stack"

        );

    /// Used to check if a subterm is duplicated, for example "times(s(x), y) =

    /// plus(y, times(x,y))" is duplicating.

        // Check if there are duplicates.

}

impl Clone for TermStack {

        // TODO: It would make sense if Protected could implement Clone.

            }

        }

}

pub struct TermStackBuilder {

    stack: InnermostStack,

}

impl TermStackBuilder {

}

impl Default for TermStackBuilder {

}

/// Create a mapping of variables to their position in the given term

    }

#[cfg(test)]

mod tests {

    use super::*;

    use ahash::AHashSet;

    use merc_data::DataFunctionSymbol;

    use merc_utilities::test_logger;

    use crate::test_utility::create_rewrite_rule;

    use test_log::test;

    #[test]

    fn test_rhs_stack() {

        let rhs_stack = TermStack::new(&create_rewrite_rule("fact(s(N))", "times(s(N), fact(N))", &["N"]).unwrap());

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

        let t1 = DataFunctionSymbol::new("times");

        let t2 = DataFunctionSymbol::new("s");

        let t3 = DataFunctionSymbol::new("fact");

        let mut write = expected.write();

        write.push(Config::Construct(t1.copy(), 2, 0));

        write.push(Config::Construct(t2.copy(), 1, 1));

        write.push(Config::Construct(t3.copy(), 1, 2));

        drop(write);

        // Check if the resulting construction succeeded.

        assert_eq!(

            rhs_stack.innermost_stack, expected,

            "The resulting config stack is not as expected"

        );

        assert_eq!(rhs_stack.stack_size, 5, "The stack size does not match");

        // Test the evaluation

        let lhs = DataExpression::from_string("fact(s(a))").unwrap();

        let rhs = DataExpression::from_string("times(s(a), fact(a))").unwrap();

        assert_eq!(

            rhs_stack.evaluate(&lhs),

            rhs,

            "The rhs stack does not evaluate to the expected term"

        );

    }

    #[test]

    fn test_rhs_stack_variable() {

        let rhs = TermStack::new(&create_rewrite_rule("f(x)", "x", &["x"]).unwrap());

        // Check if the resulting construction succeeded.

        assert!(

            rhs.innermost_stack.read().is_empty(),

            "The resulting config stack is not as expected"

        );

        assert_eq!(rhs.stack_size, 1, "The stack size does not match");

    }

    #[test]

    fn test_evaluation() {

        test_logger();

        let rhs = DataExpression::from_string_untyped("f(f(a,a),x)", &AHashSet::from([String::from("x")])).unwrap();

        let lhs = DataExpression::from_string("g(b)").unwrap();

        // Make a variable map with only x@1.

        let mut map = HashMap::new();

        map.insert(DataVariable::new("x"), DataPosition::new(&[1]));

        let sctt = TermStack::from_term(&rhs.copy(), &map);

        let expected = DataExpression::from_string("f(f(a,a),b)").unwrap();

        assert_eq!(sctt.evaluate(&lhs), expected);

    }

    #[test]

    fn test_create_varmap() {

        let t = DataExpression::from_string_untyped("f(x,x)", &AHashSet::from([String::from("x")])).unwrap();

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

        let map = create_var_map(&t);

        assert!(map.contains_key(&x));

    }

    #[test]

    fn test_is_duplicating() {

        let rhs = DataExpression::from_string_untyped("f(x,x)", &AHashSet::from([String::from("x")])).unwrap();

        // Make a variable map with only x@1.

        let mut map = HashMap::new();

        map.insert(DataVariable::new("x"), DataPosition::new(&[1]));

        let sctt = TermStack::from_term(&rhs.copy(), &map);

        assert!(sctt.contains_duplicate_var_references(), "This sctt is duplicating");

    }

}