use std::cell::UnsafeCell;

use std::fmt;

use std::sync::Arc;

use std::sync::LazyLock;

use std::sync::Mutex;

use std::sync::atomic::AtomicUsize;

use std::time::Instant;

use log::debug;

use rustc_hash::FxHashSet;

use merc_io::LargeFormatter;

use merc_sharedmutex::GlobalBfSharedMutex;

use merc_sharedmutex::RecursiveLockReadGuard;

use merc_unsafety::ProtectionSet;

use merc_unsafety::StablePointer;

use merc_utilities::debug_trace;

use crate::ATermIndex;

use crate::ATermRef;

use crate::Markable;

use crate::Symb;

use crate::Symbol;

use crate::SymbolIndex;

use crate::SymbolRef;

use crate::Term;

use crate::storage::ATermStorage;

use crate::storage::SharedTerm;

use crate::storage::SymbolPool;

/// This is the global set of protection sets that are managed by the [crate::storage::ThreadTermPool].

pub static GLOBAL_TERM_POOL: LazyLock<GlobalBfSharedMutex<GlobalTermPool>> =

/// Enables aggressive garbage collection, which is used for testing.

pub(crate) const AGGRESSIVE_GC: bool = false;

/// A type alias for the global term pool guard

pub(crate) type GlobalTermPoolGuard<'a> = RecursiveLockReadGuard<'a, GlobalTermPool>;

/// A type alias for deletion hooks

type DeletionHook = Box<dyn Fn(&ATermIndex) + Sync + Send>;

/// The single global (singleton) term pool, accessed via [GLOBAL_TERM_POOL].

pub struct GlobalTermPool {

    /// Unique table of all terms with stable pointers for references

    terms: ATermStorage,

    /// The symbol pool for managing function symbols.

    symbol_pool: SymbolPool,

    /// The thread-specific protection sets.

    thread_pools: ThreadPoolList,

    /// A separate protection set for sendable terms, see [crate::ATermSend].

    send_term_protection_sets: Vec<Option<Arc<Mutex<ProtectionSet<ATermIndex>>>>>,

    // Data structures used for garbage collection

    /// Used to avoid reallocations for the markings of all terms - uses pointers as keys

    marked_terms: FxHashSet<ATermIndex>,

    /// Used to avoid reallocations for the markings of all symbols

    marked_symbols: FxHashSet<SymbolIndex>,

    /// A stack used to mark terms recursively.

    stack: Vec<ATermIndex>,

    /// Deletion hooks called whenever a term with the given head symbol is deleted.

    deletion_hooks: Vec<(Symbol, DeletionHook)>,

    /// Indicates whether automatic garbage collection is enabled.

    garbage_collection: bool,

    /// Default terms

    int_symbol: SymbolRef<'static>,

    empty_list_symbol: SymbolRef<'static>,

    list_symbol: SymbolRef<'static>,

}

impl GlobalTermPool {

        // Insert the default symbols, mirrors the symbols defined in mCRL2.

    /// Returns the number of terms in the pool.

    /// Returns whether the term pool is empty.

    /// Creates a term storing a single integer value.

    /// Create a term from a head symbol and an iterator over its arguments

    /// Create a function symbol

    {

    /// Registers a new thread term pool.

    ///

    /// # Safety

    ///

    /// Note that the returned `Arc<UnsafeCell<...>>` is not Send or Sync, so it

    /// *must* be protected through other means.

    #[allow(clippy::arc_with_non_send_sync)]

    /// Deregisters a thread pool.

    /// Triggers garbage collection if necessary and returns an updated counter for the thread local pool.

    /// Returns a counter for the unique numeric suffix of the given prefix.

    /// Removes the registration of a prefix from the symbol pool.

    /// Register a deletion hook that is called whenever a term is deleted with the given symbol.

    {

    /// Enables or disables automatic garbage collection.

    /// Collects garbage terms.

        // Mark the default symbols

        // Loop through all protection sets and mark the terms.

            // SAFETY: We have exclusive access to the global term pool, so no other thread can modify the protection sets.

            }

        }

            }

        }

        // Delete all terms that are not marked

                // Call the deletion hooks for the term

                }

        // We ensure that every removed symbol is not used anymore.

            "Garbage collection: marking took {}ms, collection took {}ms, {} terms and {} symbols removed",

        );

        // Print information from the protection sets.

            // SAFETY: We have exclusive access to the global term pool, so no other thread can modify the protection sets.

        }

        // Clear marking data structures

    /// Returns the metrics of the term pool, can be formatted and written to output.

    /// Marks the given term as being reachable.

    ///

    /// # Safety

    ///

    /// Should only be called during garbage collection.

        // Ensure that the global term pool is locked for writing.

    /// Returns integer function symbol.

    /// Returns integer function symbol.

    /// Returns integer function symbol.

}

pub struct TermPoolMetrics<'a>(&'a GlobalTermPool);

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

            "There are {} terms, and {} symbols",

        )

}

/// A newtype wrapping the per-thread protection-set list stored inside

/// [`GlobalTermPool`].

///

/// # Safety

///

/// Note that [`UnsafeCell`] is not [`Sync`], but we explicitly only use this in

/// `&mut self` contexts, so we can safely implement `Sync` for this wrapper.

struct ThreadPoolList(Vec<Option<Arc<UnsafeCell<SharedTermProtection>>>>);

// SAFETY: See the safety documentation on `ThreadPoolList`.

unsafe impl Sync for ThreadPoolList {}

unsafe impl Send for ThreadPoolList {}

impl std::ops::Deref for ThreadPoolList {

    type Target = Vec<Option<Arc<UnsafeCell<SharedTermProtection>>>>;

}

impl std::ops::DerefMut for ThreadPoolList {

}

/// A struct that contains the protection sets for a thread, as well as the

/// index of the thread pool in the global term pool.

pub struct SharedTermProtection {

    /// Protection set for terms

    pub term_protection_set: ProtectionSet<ATermIndex>,

    /// Protection set to prevent garbage collection of symbols

    pub symbol_protection_set: ProtectionSet<SymbolIndex>,

    /// Protection set for containers

    pub container_protection_set: ProtectionSet<Arc<dyn Markable + Sync + Send>>,

    /// Index in global pool's thread pools list

    pub index: usize,

}

impl SharedTermProtection {

    /// Returns the metrics of the term pool, can be formatted and written to output.

}

/// A struct that can be used to print the performance of the protection sets.

pub struct ProtectionMetrics<'a>(&'a SharedTermProtection);

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

            "Protection set {} has {} roots, max {} and {} insertions",

            self.0.index,

            "Containers: {} roots, max {} and {} insertions",

            "Symbols: {} roots, max {} and {} insertions",

        )

}

/// Helper struct to pass private data required to mark term recursively.

pub struct Marker<'a> {

    marked_terms: &'a mut FxHashSet<ATermIndex>,

    marked_symbols: &'a mut FxHashSet<SymbolIndex>,

    stack: &'a mut Vec<ATermIndex>,

}

impl Marker<'_> {

    // Marks the given term as being reachable.

                // Each term should be marked.

                // Mark the function symbol.

                // For some terms, such as ATermInt, we must ONLY consider the valid arguments (indicated by the arity)

                    // Skip if unnecessary, otherwise mark before pushing to stack since it can be shared.

                }

            }

    /// Marks the given symbol as being reachable.

}

#[cfg(test)]

mod tests {

    use std::collections::HashMap;

    use merc_utilities::random_test;

    use crate::ATerm;

    use crate::Symbol;

    use crate::Term;

    use crate::random_term;

    #[test]

    #[cfg_attr(miri, ignore)]

            }

    #[test]

    #[should_panic]

        // Currently we check on access

}