pub mod serde;

use std::any::TypeId;

// allow use of Declaration in this file, and nowhere else

use std::cell::{Cell, Ref, RefCell, RefMut};

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

use std::rc::Rc;

use ::serde::{Deserialize, Serialize};

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

use super::name::Name;

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

use super::{

    DecisionVariable, DomainPtr, Expression, GroundDomain, Moo, RecordEntry, ReturnType, Typeable,

};

use crate::ast::domains::HasDomain;

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

thread_local! {

    // make each thread have its own id counter.

    static DECLARATION_PTR_ID_COUNTER: Cell<u32> = const { Cell::new(0) };

    // We run integration tests in parallel threads - making this thread local ensures that

    // declarations in a test always have the same id, instead of the ids depending on how many

    // threads are running, how they are scheduled, etc.

}

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

    // the shared bits of the pointer

    inner: Rc<DeclarationPtrInner>,

}

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

#[derive(Clone, 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: RefCell<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 decision variable declaration with the decision category.

    ///

    /// # Examples

    ///

    /// ```

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

    ///

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

    /// let declaration = DeclarationPtr::new_var(

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

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

    ///

    /// ```

    /// Creates a new decision variable with the quantified category.

    ///

    /// This is useful to represent a quantified / induction variable in a comprehension.

    /// 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 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 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 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_var(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_var(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));

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

    /// ```

    /// 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_var(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 {

            }

    /// 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_var(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()));

    /// ```

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

    /*        Pointer utility methods        */

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

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

    // convenience.

    /// Immutably borrows the declaration.

        // unlike refcell.borrow(), this never panics

    /// Mutably borrows the declaration.

        // unlike refcell.borrow_mut(), this never panics

    /// 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_var(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 {

}

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

            (

            )

        }

}

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

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 {

    DecisionVariable(DecisionVariable),

    ValueLetting(Expression),

    DomainLetting(DomainPtr),

    Given(DomainPtr),

    /// A named field inside a record type.

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

    RecordField(DomainPtr),

}