use std::borrow::Borrow;

use std::cmp::Ordering;

use std::collections::VecDeque;

use std::fmt;

use std::hash::Hash;

use std::hash::Hasher;

use std::marker::PhantomData;

use std::ops::Deref;

use mcrl2_sys::atermpp::ffi;

use mcrl2_sys::cxx::UniquePtr;

use utilities::PhantomUnsend;

use crate::aterm::SymbolRef;

use crate::aterm::THREAD_TERM_POOL;

use super::global_aterm_pool::GLOBAL_TERM_POOL;

/// This represents a lifetime bound reference to an existing ATerm that is

/// protected somewhere statically.

///

/// Can be 'static if the term is protected in a container or ATerm. That means

/// we either return &'a ATermRef<'static> or with a concrete lifetime

/// ATermRef<'a>. However, this means that the functions for ATermRef cannot use

/// the associated lifetime for the results parameters, as that would allow us

/// to acquire the 'static lifetime. This occasionally gives rise to issues

/// where we look at the argument of a term and want to return it's name, but

/// this is not allowed since the temporary returned by the argument is dropped.

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

pub struct ATermRef<'a> {

    term: *const ffi::_aterm,

    marker: PhantomData<&'a ()>,

}

/// These are safe because terms are never modified. Garbage collection is

/// always performed with exclusive access and uses relaxed atomics to perform

/// some interior mutability.

unsafe impl Send for ATermRef<'_> {}

unsafe impl Sync for ATermRef<'_> {}

impl Default for ATermRef<'_> {

}

impl<'a> ATermRef<'a> {

    /// Protects the reference on the thread local protection pool.

        } else {

        }

    /// Protects the reference on the global protection pool.

        } else {

        }

    /// This allows us to extend our borrowed lifetime from 'a to 'b based on

    /// existing parent term which has lifetime 'b.

    ///

    /// The main usecase is to establish transitive lifetimes. For example given

    /// a term t from which we borrow `u = t.arg(0)` then we cannot have

    /// u.arg(0) live as long as t since the intermediate temporary u is

    /// dropped. However, since we know that u.arg(0) is a subterm of `t` we can

    /// upgrade its lifetime to the lifetime of `t` using this function.

    ///

    /// # Safety

    ///

    /// This function might only be used if witness is a parent term of the

    /// current term.

        );

    /// A private unchecked version of [`ATermRef::upgrade`] to use in iterators.

    /// Obtains the underlying pointer

}

impl<'a> ATermRef<'a> {

}

impl ATermRef<'_> {

    /// Returns the indexed argument of the term

            self

        );

        unsafe {

    /// Returns the list of arguments as a collection

    /// Makes a copy of the term with the same lifetime as itself.

    /// Returns whether the term is the default term (not initialised)

    /// Returns true iff this is an aterm_list

    /// Returns true iff this is the empty aterm_list

    /// Returns true iff this is a aterm_int

    /// Returns the head function symbol of the term.

    /// Returns an iterator over all arguments of the term that runs in pre order traversal of the term trees.

    /// Panics if the term is default

        );

}

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

}

impl fmt::Debug for ATermRef<'_> {

        } else {

            unsafe {

            }

        }

}

/// The protected version of [ATermRef], mostly derived from it.

#[derive(Default)]

pub struct ATerm {

    pub(crate) term: ATermRef<'static>,

    pub(crate) root: usize,

    // ATerm is not Send because it uses thread-local state for its protection

    // mechanism.

    _marker: PhantomUnsend,

}

impl ATerm {

    /// Obtains the underlying pointer

    ///

    /// # Safety

    /// Should not be modified in any way.

    /// Creates a new term from the given reference and protection set root

    /// entry.

}

impl Drop for ATerm {

}

impl Clone for ATerm {

}

impl Deref for ATerm {

    type Target = ATermRef<'static>;

}

impl<'a> Borrow<ATermRef<'a>> for ATerm {

}

impl fmt::Display for ATerm {

}

impl fmt::Debug for ATerm {

}

impl Hash for ATerm {

}

impl PartialEq for ATerm {

}

impl PartialOrd for ATerm {

}

impl Ord for ATerm {

}

impl Eq for ATerm {}

// Some convenient conversions.

impl From<UniquePtr<ffi::aterm>> for ATerm {

}

impl From<&ffi::aterm> for ATerm {

}

/// The same as [ATerm] but protected on the global protection set. This allows

/// the term to be Send and Sync among threads.

#[derive(Default)]

pub struct ATermGlobal {

    pub(crate) term: ATermRef<'static>,

    pub(crate) root: usize,

}

impl Drop for ATermGlobal {

}

impl Clone for ATermGlobal {

}

impl Deref for ATermGlobal {

    type Target = ATermRef<'static>;

}

impl Hash for ATermGlobal {

}

impl PartialEq for ATermGlobal {

}

impl PartialOrd for ATermGlobal {

}

impl Ord for ATermGlobal {

}

impl Eq for ATermGlobal {}

impl fmt::Display for ATermGlobal {

}

impl fmt::Debug for ATermGlobal {

}

impl From<ATerm> for ATermGlobal {

}

pub struct ATermList<T> {

    term: ATerm,

    _marker: PhantomData<T>,

}

impl<T: From<ATerm>> ATermList<T> {

    /// Obtain the head, i.e. the first element, of the list.

}

impl<T> ATermList<T> {

    /// Returns true iff the list is empty.

    /// Obtain the tail, i.e. the remainder, of the list.

    /// Returns an iterator over all elements in the list.

}

impl<T> Clone for ATermList<T> {

}

impl<T> From<ATermList<T>> for ATerm {

}

impl<T: From<ATerm>> Iterator for ATermListIter<T> {

    type Item = T;

        } else {

        }

}

impl<T> From<ATerm> for ATermList<T> {

}

impl<'a, T> From<ATermRef<'a>> for ATermList<T> {

}

impl<T: From<ATerm>> IntoIterator for ATermList<T> {

    type IntoIter = ATermListIter<T>;

    type Item = T;

}

impl<T: From<ATerm>> IntoIterator for &ATermList<T> {

    type IntoIter = ATermListIter<T>;

    type Item = T;

}

/// An iterator over the arguments of a term.

#[derive(Default)]

pub struct ATermArgs<'a> {

    term: ATermRef<'a>,

    arity: usize,

    index: usize,

}

impl<'a> ATermArgs<'a> {

}

impl<'a> Iterator for ATermArgs<'a> {

    type Item = ATermRef<'a>;

        } else {

        }

}

impl DoubleEndedIterator for ATermArgs<'_> {

        } else {

        }

}

impl ExactSizeIterator for ATermArgs<'_> {

}

pub struct ATermListIter<T> {

    current: ATermList<T>,

}

/// An iterator over all subterms of the given [ATerm] in preorder traversal, i.e.,

/// for f(g(a), b) we visit f(g(a), b), g(a), a, b.

pub struct TermIterator<'a> {

    queue: VecDeque<ATermRef<'a>>,

}

impl TermIterator<'_> {

}

impl<'a> Iterator for TermIterator<'a> {

    type Item = ATermRef<'a>;

                // Put subterms in the queue

                }

            }

        }

}

#[cfg(test)]

mod tests {

    use std::sync::Mutex;

    use std::thread;

    use test_log::test;

    use crate::aterm::random_term;

    use crate::aterm::TermPool;

    use rand::rngs::StdRng;

    use rand::Rng;

    use rand::SeedableRng;

    use super::*;

    /// Make sure that the term has the same number of arguments as its arity.

            )

        }

    fn test_term_iterator() {

        let mut tp = TermPool::new();

        let t = tp.from_string("f(g(a),b)").unwrap();

        let mut result = t.iter();

        assert_eq!(result.next().unwrap(), tp.from_string("f(g(a),b)").unwrap().copy());

        assert_eq!(result.next().unwrap(), tp.from_string("g(a)").unwrap().copy());

        assert_eq!(result.next().unwrap(), tp.from_string("a").unwrap().copy());

        assert_eq!(result.next().unwrap(), tp.from_string("b").unwrap().copy());

    }

    fn test_aterm_list() {

        let mut tp = TermPool::new();

        let list: ATermList<ATerm> = tp.from_string("[f,g,h,i]").unwrap().into();

        assert!(!list.is_empty());

        // Convert into normal vector.

        let values: Vec<ATerm> = list.iter().collect();

        assert_eq!(values[0], tp.from_string("f").unwrap());

        assert_eq!(values[1], tp.from_string("g").unwrap());

        assert_eq!(values[2], tp.from_string("h").unwrap());

        assert_eq!(values[3], tp.from_string("i").unwrap());

    }

    fn test_global_aterm_pool_parallel() {

        let seed: u64 = rand::rng().random();

        println!("seed: {}", seed);

        let terms: Mutex<Vec<ATermGlobal>> = Mutex::new(vec![]);

        for term in &*terms.lock().unwrap() {

            verify_term(&term);

        }

    }

}