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.

        // SAFETY: the default symbols are marked on every collection (see `collect_garbage`),

        // so these indices stay valid for the lifetime of the pool.

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

    /// Returns whether the term pool is empty.

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

    ///

    /// Crate-private: the returned pointer is unprotected, so the caller must protect it

    /// (or hand it to a [crate::Return]) before the read guard it was created under drops.

        // SAFETY: `int_symbol` is one of the default symbols, which are marked on every

        // collection, so the index stays valid for the pool's lifetime.

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

    ///

    /// Crate-private: the returned pointer is unprotected, see [Self::create_int].

    /// Create a function symbol

    ///

    /// Crate-private: `protect` receives an unprotected index, see [Self::create_int].

    {

    /// 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.

    ///

    /// The `send_term_protection_sets` slot is deliberately left in place: a

    /// still-live ATermSend created on this thread may outlive it and

    /// must keep being marked.

    /// 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.

    ///

    /// The hook runs in the middle of garbage collection, when the dying term's arguments may

    /// already have been deallocated by an earlier pass over a different arity table. Hooks must

    /// therefore not dereference the term's arguments; they may only use the term's address and

    /// its head symbol. For the same reason a hook must not create terms or otherwise re-enter the

    /// pool mutably (e.g. trigger another collection): the sweep holds `&mut self` throughout.

    {

    /// Enables or disables automatic garbage collection.

    /// Collects garbage terms.

        // Mark the default symbols

        // SAFETY: mark-set entries only live for the duration of this collection pass

        // (the sets are drained by the sweep below), and a marked symbol is by

        // definition retained by the sweep.

        // 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.

            }

            // Marking a `Protected` container goes through `GcMutex::lock`, which takes a

            // `read_recursive` on the same lock we already hold for writing here.

        }

            }

        }

        // Reclaim send-term protection sets whose owning thread has exited and that hold no

        // outstanding ATermSend.

        }

        // Delete all terms that are not marked.

        // SAFETY: Marking visited every root in every protection set while holding the exclusive

        // lock, so unmarked terms have no live references that could be dereferenced afterwards.

        unsafe {

                    // Call the deletion hooks for the term

                        // `term` is still resident in `self.terms` during the

                        // retain predicate, so its pointee is valid to read

                        // (covered by the enclosing `unsafe` block).

                    }

        }

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

        // SAFETY: Unmarked symbols are not referenced by any marked term or protection set root.

        unsafe {

        }

            "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.

        // SAFETY: all copies below go into the mark sets and the work stack, which are

        // drained before the collection pass ends, and a marked term or symbol is by

        // definition retained by the sweep; `term` itself is alive for the borrow.

        unsafe {

                    // 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.

        // SAFETY: see `mark`; the entry is dropped when the sweep finishes and a marked

        // symbol is retained by it.

}

#[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

}