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, RecordEntry, Reference,

    ReturnType, Typeable,

};

use parking_lot::{

    MappedRwLockReadGuard, MappedRwLockWriteGuard, RwLock, RwLockReadGuard, RwLockWriteGuard,

};

use serde::{Deserialize, Serialize};

use serde_with::serde_as;

use std::any::TypeId;

use std::collections::VecDeque;

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

use std::mem;

use std::sync::Arc;

use std::sync::atomic::{AtomicU32, 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) };

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

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

}

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

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

        });

    /// 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 record field declaration.

    ///

    /// # Examples

    ///

    /// ```

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

    ///

    /// // create declaration for field A in `find rec: record {A: int(0..1), B: int(0..2)}`

    ///

    /// let field = RecordEntry {

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

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

    /// };

    ///

    /// let declaration = DeclarationPtr::new_record_field(field);

    /// ```

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

    /*        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)])))

    ///

    /// ```

            }

        }

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

            } else {

            }

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

            } else {

            }

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

            } else {

            }

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

            } else {

            }

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

            {

            } else {

            }

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

            {

            } else {

            }

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

            } else {

            }

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

            } else {

            }

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

            } else {

            }

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

            } else {

            }

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

}

impl CategoryOf for DeclarationPtr {

        }

}

impl HasId for DeclarationPtr {

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

}

impl DefaultWithId for DeclarationPtr {

}

impl Typeable for DeclarationPtr {

        }

}

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 {

        (

        )

}

            (

            )

        }

            (

            )

        }

            (

            )

        }

            (

            )

        }

            (

            )

        }

            (

            )

        }

            {

                (

                )

            } else {

                (

                )

            };

            (

                    };

            )

        }

            (

            )

        }

    }

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),

    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),

    /// A named field inside a record type.

    /// e.g. A, B in record{A: int(0..1), B: int(0..2)}

    RecordField(DomainPtr),

}

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

}