use crate::ast::enumerated::EnumeratedType;

use super::categories::{Category, CategoryOf};

use super::name::Name;

use super::serde::{DefaultWithId, HasId, IdPtr, ObjId, PtrAsInner};

use super::{

    DecisionVariable, DomainPtr, Expression, GroundDomain, HasDomain, Moo, Reference, ReturnType,

    Typeable,

};

use crate::representation::{ReprRule, ReprStore};

use parking_lot::{

    MappedRwLockReadGuard, MappedRwLockWriteGuard, RwLock, RwLockReadGuard, RwLockWriteGuard,

};

use serde::{Deserialize, Serialize};

use serde_with::serde_as;

use std::any::TypeId;

use std::collections::BTreeSet;

use std::collections::VecDeque;

use std::fmt::{Debug, Display};

use std::hash::{DefaultHasher, Hash, Hasher};

use std::mem;

use std::ops::{Deref, DerefMut};

use std::sync::Arc;

use std::sync::atomic::{AtomicU32, AtomicU64, Ordering};

use uniplate::{Biplate, Tree, Uniplate};

/// Global counter of declarations.

/// Note that the counter is shared between all threads

/// Thus, when running multiple models in parallel, IDs may

/// be different with every run depending on scheduling order

static DECLARATION_PTR_ID_COUNTER: AtomicU32 = const { AtomicU32::new(0) };

/// Global generation of declaration contents.

///

/// Declaration pointers are shared across symbol tables, so an in-place update cannot cheaply

/// notify every table that contains the pointer. Symbol-table content caches compare against this

/// generation instead.

static DECLARATION_CONTENT_GENERATION: AtomicU64 = const { AtomicU64::new(1) };

/// Returns the generation shared by all mutable declaration contents.

/// Records that a declaration's contents may have changed.

/// Mutable access to part of a declaration that records a semantic change when released.

pub struct DeclarationMutGuard<'a, T: ?Sized> {

    inner: Option<MappedRwLockWriteGuard<'a, T>>,

}

impl<'a, T: ?Sized> DeclarationMutGuard<'a, T> {

    /// Wraps a mapped write guard so dropping it records a content change.

}

impl<T: ?Sized> Deref for DeclarationMutGuard<'_, T> {

    type Target = T;

}

impl<T: ?Sized> DerefMut for DeclarationMutGuard<'_, T> {

}

impl<T: ?Sized> Drop for DeclarationMutGuard<'_, T> {

}

#[doc(hidden)]

/// Resets the id counter of `DeclarationPtr` to 0.

///

/// This is probably always a bad idea.

/// A shared pointer to a [`Declaration`].

///

/// Two declaration pointers are equal if they point to the same underlying declaration.

///

/// # Id

///

///  The id of `DeclarationPtr` obeys the following invariants:

///

/// 1. Declaration pointers have the same id if they point to the same

///    underlying declaration.

///

/// 2. The id is immutable.

///

/// 3. Changing the declaration pointed to by the declaration pointer does not change the id. This

///    allows declarations to be updated by replacing them with a newer version of themselves.

///

/// `Ord`, `Hash`, and `Eq` use id for comparisons.

/// # Serde

///

/// Declaration pointers can be serialised using the following serializers:

///

/// + [`DeclarationPtrFull`](serde::DeclarationPtrFull)

/// + [`DeclarationPtrAsId`](serde::DeclarationPtrAsId)

///

/// See their documentation for more information.

#[derive(Clone, Debug)]

pub struct DeclarationPtr

where

    Self: Send + Sync,

{

    // the shared bits of the pointer

    inner: Arc<DeclarationPtrInner>,

}

// The bits of a declaration that are shared between all pointers.

#[derive(Debug)]

struct DeclarationPtrInner {

    // Identity hash/order key. Declaration content is mutable and is hashed separately by

    // `DeclarationPtr::content_hash`.

    // We don't want this to be mutable, as `HashMap` and `BTreeMap` rely on the hash or order of

    // keys to be unchanging.

    //

    // See:  https://rust-lang.github.io/rust-clippy/master/index.html#mutable_key_type

    id: ObjId,

    // The contents of the declaration itself should be mutable.

    value: RwLock<Declaration>,

    /// Representations initialised for this declaration.

    representations: RwLock<ReprStore>,

    /// The declaration from which this auxiliary declaration was created.

    source: RwLock<Option<DeclarationPtr>>,

}

impl DeclarationPtrInner {

    // SAFETY: only use if you are really really sure you arn't going to break the id invariants of

    // DeclarationPtr and HasId!

}

#[allow(dead_code)]

impl DeclarationPtr {

    /******************************/

    /*        Constructors        */

    /******************************/

    /// Creates a `DeclarationPtr` for the given `Declaration`.

    /// Gets the declaration from which this auxiliary declaration was created.

    /// Mutates the declaration from which this auxiliary declaration was created.

    /// Gets the representations initialised for this declaration.

    /// Mutates the representations initialised for this declaration.

    /// Gets a particular representation state, if it has been initialised.

    /// Creates a new declaration.

    ///

    /// # Examples

    ///

    /// ```

    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};

    ///

    /// // letting MyDomain be int(1..5)

    /// let declaration = DeclarationPtr::new(

    ///     Name::User("MyDomain".into()),

    ///     DeclarationKind::DomainLetting(Domain::int(vec![

    ///         Range::Bounded(1,5)])));

    /// ```

    /// Creates a new find declaration.

    ///

    /// # Examples

    ///

    /// ```

    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};

    ///

    /// // find x: int(1..5)

    /// let declaration = DeclarationPtr::new_find(

    ///     Name::User("x".into()),

    ///     Domain::int(vec![Range::Bounded(1,5)]));

    ///

    /// ```

    /// Creates a new auxiliary find declaration.

    ///

    /// Auxiliary finds are introduced by rewriting (for example, turning a top-level `exists`

    /// into constraints), and can also be written in Essence as `findAux`.

    /// They are decision variables for solvers, but must not be branched on during search:

    /// different assignments to them must not produce distinct user-facing solutions.

    /// Creates a new given declaration.

    ///

    /// # Examples

    ///

    /// ```

    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};

    ///

    /// // given n: int(1..5)

    /// let declaration = DeclarationPtr::new_given(

    ///     Name::User("n".into()),

    ///     Domain::int(vec![Range::Bounded(1,5)]));

    ///

    /// ```

    /// Creates a new quantified declaration for local comprehension scopes.

    ///

    /// Used when creating the quantified variable in a generator.

    /// Creates a quantified declaration backed by a generator declaration.

    ///

    /// This is used in comprehensions to refer to a quantified variable that is already defined using a generator.

        let kind = DeclarationKind::Quantified(Quantified {

        });

    /// Creates a new value letting declaration.

    ///

    /// # Examples

    ///

    /// ```

    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range, Expression,

    /// Literal,Atom,Moo};

    /// use conjure_cp_core::{matrix_expr,ast::Metadata};

    ///

    /// // letting n be 10 + 10

    /// let ten = Expression::Atomic(Metadata::new(),Atom::Literal(Literal::Int(10)));

    /// let expression = Expression::Sum(Metadata::new(),Moo::new(matrix_expr![ten.clone(),ten]));

    /// let declaration = DeclarationPtr::new_value_letting(

    ///     Name::User("n".into()),

    ///     expression);

    ///

    /// ```

    /// Creates a new value letting declaration with domain.

    ///

    /// # Examples

    ///

    /// ```

    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range, Expression,

    /// Literal,Atom,Moo,DomainPtr,Metadata};

    /// use conjure_cp_core::{matrix_expr};

    ///

    /// // letting n be 10 + 10

    /// let ten = Expression::Atomic(Metadata::new(),Atom::Literal(Literal::Int(10)));

    /// let expression = Expression::Sum(Metadata::new(),Moo::new(matrix_expr![ten.clone(),ten]));

    /// let domain = Domain::bool();

    /// let declaration = DeclarationPtr::new_value_letting_with_domain(

    ///     Name::User("n".into()),

    ///     expression,

    ///     domain,

    /// );

    /// ```

    /// Creates a new domain letting declaration.

    ///

    /// # Examples

    ///

    /// ```

    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};

    ///

    /// // letting MyDomain be int(1..5)

    /// let declaration = DeclarationPtr::new_domain_letting(

    ///     Name::User("MyDomain".into()),

    ///     Domain::int(vec![Range::Bounded(1,5)]));

    ///

    /// ```

    /// Creates a new enumerated type declaration

    /// TODO: Example

    /// Creates a new unnamed type declaration

    /// TODO: Example

    /**********************************************/

    /*        Declaration accessor methods        */

    /**********************************************/

    /// Gets the domain of the declaration, if it has one.

    ///

    /// # Examples

    ///

    /// ```

    /// use conjure_cp_core::ast::{DeclarationPtr, Name, Domain, Range, GroundDomain};

    ///

    /// // find a: int(1..5)

    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));

    ///

    /// assert!(declaration.domain().is_some_and(|x| x.as_ground().unwrap() == &GroundDomain::Int(vec![Range::Bounded(1,5)], None)))

    ///

    /// ```

        // Expressions stored inside a declaration (as opposed to the constraint tree the rewrite

        // engine walks) can be mutated in place by substitution utilities that never touch

        // the constraint-tree metadata cache, so `domain_of`'s cache would go stale silently for

        // them. Use the uncached path here.

            DeclarationKind::Find(var) | DeclarationKind::FindAuxiliary(var) => {

            }

            DeclarationKind::ValueLetting(e, domain) => {

            }

        }

    /// Returns true if this declaration is an auxiliary find.

    ///

    /// Auxiliary finds are solver variables that must not be included in the search/branching

    /// order (see [`DeclarationKind::FindAuxiliary`]).

            DeclarationKind::FindAuxiliary(_)

        )

    /// Gets the domain of the declaration and fully resolve it

    /// Gets the kind of the declaration.

    ///

    /// # Examples

    ///

    /// ```

    /// use conjure_cp_core::ast::{DeclarationPtr,DeclarationKind,Name,Domain,Range};

    ///

    /// // find a: int(1..5)

    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));

    /// assert!(matches!(&declaration.kind() as &DeclarationKind, DeclarationKind::Find(_)))

    /// ```

    /// Gets the name of the declaration.

    ///

    /// # Examples

    ///

    /// ```

    /// use conjure_cp_core::ast::{DeclarationPtr,Name,Domain,Range};

    ///

    /// // find a: int(1..5)

    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));

    ///

    /// assert_eq!(&declaration.name() as &Name, &Name::User("a".into()))

    /// ```

    /// This declaration as a decision variable, if it is one.

    ///

    /// Both user [`DeclarationKind::Find`] and rewriter-introduced

    /// [`DeclarationKind::FindAuxiliary`] declarations are treated as decision variables.

        .ok()

    /// This declaration as a mutable decision variable, if it is one.

    ///

    /// Both user [`DeclarationKind::Find`] and rewriter-introduced

    /// [`DeclarationKind::FindAuxiliary`] declarations are treated as decision variables.

        .ok()

    /// This declaration as a domain letting, if it is one.

            } else {

            }

        .ok()

    /// This declaration as a mutable domain letting, if it is one.

            } else {

            }

        .ok()

    /// This declaration as a value letting, if it is one.

            {

            } else {

            }

        .ok()

    /// This declaration as a mutable value letting, if it is one.

            {

            } else {

            }

        .ok()

    /// This declaration as a given statement, if it is one.

            } else {

            }

        .ok()

    /// This declaration as a mutable given statement, if it is one.

            } else {

            }

        .ok()

    /// This declaration as a quantified expression, if it is one.

            } else {

            }

        .ok()

    /// This declaration as a mutable quantified expression, if it is one.

            } else {

            }

        .ok()

    /// This declaration as an enumerated type, if it is one.

            } else {

            }

        .ok()

    /// This declaration as a mutable enumerated type, if it is one.

            } else {

            }

        .ok()

    /// This declaration as an unnamed type, if it is one.

            } else {

            }

        .ok()

    /// This declaration as a mutable unnamed type, if it is one.

            } else {

            }

        .ok()

    /// Changes the name in this declaration, returning the old one.

    ///

    /// # Examples

    ///

    /// ```

    /// use conjure_cp_core::ast::{DeclarationPtr, Domain, Range, Name};

    ///

    /// // find a: int(1..5)

    /// let mut declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));

    ///

    /// let old_name = declaration.replace_name(Name::User("b".into()));

    /// assert_eq!(old_name,Name::User("a".into()));

    /// assert_eq!(&declaration.name() as &Name,&Name::User("b".into()));

    /// ```

    /// Replaces the underlying declaration kind and returns the previous kind.

    /// Note: this affects all cloned `DeclarationPtr`s pointing to the same declaration.

    /*****************************************/

    /*        Pointer utility methods        */

    /*****************************************/

    // These are mostly wrappers over RefCell, Ref, and RefMut methods, re-exported here for

    // convenience.

    /// Read the underlying [Declaration].

    ///

    /// Will block the current thread until no other thread has a write lock.

    /// Attempting to get a read lock if the current thread already has one

    /// **will** cause it to deadlock.

    /// The lock is released when the returned guard goes out of scope.

    /// Write the underlying [Declaration].

    ///

    /// Will block the current thread until no other thread has a read or write lock.

    /// The lock is released when the returned guard goes out of scope.

    /// Creates a new declaration pointer with the same contents as `self` that is not shared with

    /// anyone else.

    ///

    /// As the resulting pointer is unshared, it will have a new id.

    ///

    /// # Examples

    ///

    /// ```

    /// use conjure_cp_core::ast::{DeclarationPtr,Name,Domain,Range};

    ///

    /// // find a: int(1..5)

    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));

    ///

    /// let mut declaration2 = declaration.clone();

    ///

    /// declaration2.replace_name(Name::User("b".into()));

    ///

    /// assert_eq!(&declaration.name() as &Name, &Name::User("b".into()));

    /// assert_eq!(&declaration2.name() as &Name, &Name::User("b".into()));

    ///

    /// declaration2 = declaration2.detach();

    ///

    /// assert_eq!(&declaration2.name() as &Name, &Name::User("b".into()));

    ///

    /// declaration2.replace_name(Name::User("c".into()));

    ///

    /// assert_eq!(&declaration.name() as &Name, &Name::User("b".into()));

    /// assert_eq!(&declaration2.name() as &Name, &Name::User("c".into()));

    /// ```

        // despite having the same contents, the new declaration pointer is unshared, so it should

        // get a new id.

    /// Applies `f` to the declaration, returning the result as a reference.

    /// Applies mutable function `f` to the declaration, returning the result as a mutable reference.

    /// Replaces the declaration with a new one, returning the old value, without deinitialising

    /// either one.

    /// Hashes the declaration contents rather than the stable declaration pointer id.

    ///

    /// Pointer hashing intentionally remains id-based for map/set invariants. This helper is for

    /// rewrite caches that need to be invalidated when the declaration value behind a reference

    /// changes.

    /// Compares current declaration contents without considering pointer identity.

    /// Hashes this declaration's value into `state`, guarding against declaration-reference cycles.

}

impl CategoryOf for DeclarationPtr {

            DeclarationKind::Find(decision_variable)

            DeclarationKind::ValueLetting(expression, _)

            DeclarationKind::EnumeratedType(_) | DeclarationKind::UnnamedType(_) => {

            }

        }

}

impl HasId for DeclarationPtr {

    const TYPE_NAME: &'static str = "DeclarationPtrInner";

}

impl DefaultWithId for DeclarationPtr {

}

impl Typeable for DeclarationPtr {

            DeclarationKind::ValueLetting(expression, _)

            DeclarationKind::UnnamedType(size) => {

            }

        }

}

impl Uniplate for DeclarationPtr {

        (

        )

}

impl<To> Biplate<To> for DeclarationPtr

where

    Declaration: Biplate<To>,

    To: Uniplate,

{

            unsafe {

                (

                )

            }

        } else {

            // call biplate on the enclosed declaration

            (

            )

        }

}

type ReferenceTree = Tree<Reference>;

type ReferenceReconstructor<T> = Box<dyn Fn(ReferenceTree) -> T>;

impl Biplate<Reference> for DeclarationPtr {

        (

        )

}

        DeclarationKind::Find(var) => {

            (

            )

        }

        DeclarationKind::FindAuxiliary(var) => {

            (

            )

        }

        DeclarationKind::Given(domain) => {

            (

            )

        }

        DeclarationKind::DomainLetting(domain) => {

            (

            )

        }

        DeclarationKind::ValueLetting(expression, domain) => {

            (

            )

        }

        DeclarationKind::TemporaryValueLetting(expression) => {

            (

            )

        }

        DeclarationKind::Quantified(quantified) => {

            let (domain_tree, recons_domain) =

            {

                (

                        as ReferenceReconstructor<Option<DeclarationPtr>>,

                )

            } else {

                (

                )

            };

            (

                    };

            )

        }

        DeclarationKind::QuantifiedExpr(expr) => {

            (

            )

        }

        kind @ (DeclarationKind::EnumeratedType(_) | DeclarationKind::UnnamedType(_)) => {

        }

    }

impl IdPtr for DeclarationPtr {

    type Data = Declaration;

}

impl Ord for DeclarationPtr {

}

impl PartialOrd for DeclarationPtr {

}

impl PartialEq for DeclarationPtr {

}

impl Eq for DeclarationPtr {}

impl std::hash::Hash for DeclarationPtr {

        // invariant: x == y -> hash(x) == hash(y)

}

impl Display for DeclarationPtr {

}

#[derive(Clone, PartialEq, Debug, Serialize, Deserialize, Eq, Uniplate)]

#[biplate(to=Expression)]

#[biplate(to=DeclarationPtr)]

#[biplate(to=Name)]

/// The contents of a declaration

pub struct Declaration {

    /// The name of the declared symbol.

    name: Name,

    /// The kind of the declaration.

    kind: DeclarationKind,

}

impl Declaration {

    /// Creates a new declaration.

}

/// A specific kind of declaration.

#[non_exhaustive]

#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Uniplate)]

#[biplate(to=Expression)]

#[biplate(to=DeclarationPtr)]

#[biplate(to=Declaration)]

pub enum DeclarationKind {

    Find(DecisionVariable),

    /// A rewriter-introduced or `findAux`-declared decision variable that must not be branched on

    /// during search.

    ///

    /// Used for auxiliaries such as those created when rewriting `exists` into constraints.

    FindAuxiliary(DecisionVariable),

    Given(DomainPtr),

    Quantified(Quantified),

    QuantifiedExpr(Expression),

    /// Carries an optional domain so instantiated `given`s can retain their declared domain.

    ValueLetting(Expression, Option<DomainPtr>),

    DomainLetting(DomainPtr),

    /// A short-lived value binding used internally during rewrites (e.g. comprehension unrolling).

    ///

    /// Unlike `ValueLetting`, this is not intended to represent a user-visible top-level `letting`.

    TemporaryValueLetting(Expression),

    /// An enumerated type.

    EnumeratedType(Moo<EnumeratedType>),

    /// An unnamed type.

    UnnamedType(u32),

}

impl DeclarationKind {

    /// Hashes declaration-kind contents without using declaration pointer identity.

            DeclarationKind::Find(var) | DeclarationKind::FindAuxiliary(var) => {

                            }

                        } else {

                        }

                    }

                }

            }

            DeclarationKind::Given(domain) | DeclarationKind::DomainLetting(domain) => {

            }

            DeclarationKind::Quantified(quantified) => {

            }

            DeclarationKind::QuantifiedExpr(expr)

            | DeclarationKind::TemporaryValueLetting(expr) => {

            }

            DeclarationKind::ValueLetting(expr, domain) => {

            }

        }

}

#[serde_as]

#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Uniplate)]

pub struct Quantified {

    domain: DomainPtr,

    #[serde_as(as = "Option<PtrAsInner>")]

    generator: Option<DeclarationPtr>,

}

impl Quantified {

}