use crate::ast::serde::{AsId, HasId};

use crate::representation::types::ReprGetOrInitResult;

use crate::representation::{

    ReferenceReprError, ReprError, ReprRule, ReprRulePtr, ReprSelectError, ReprStateStored,

};

use crate::{ast::DeclarationPtr, bug};

use derivative::Derivative;

use parking_lot::{MappedRwLockReadGuard, RwLockReadGuard};

use serde::{Deserialize, Serialize};

use serde_with::serde_as;

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

use uniplate::Uniplate;

use super::{

    Atom, DeclarationKind, DomainPtr, Expression, GroundDomain, Literal, Metadata, Moo, Name,

    ReturnType,

    categories::{Category, CategoryOf},

    domains::HasDomain,

};

/// A reference to a declaration (variable, parameter, etc.)

///

/// This is a thin wrapper around [`DeclarationPtr`] with two main purposes:

/// 1. Encapsulate the serde pragmas (e.g., serializing as IDs rather than full objects)

/// 2. Enable type-directed traversals of references via uniplate

#[serde_as]

#[derive(

    Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize, Uniplate, Derivative,

)]

#[derivative(Hash)]

#[uniplate()]

#[biplate(to=DeclarationPtr)]

#[biplate(to=Name)]

pub struct Reference {

    #[serde_as(as = "AsId")]

    pub ptr: DeclarationPtr,

    pub repr: Option<ReprRulePtr>,

}

impl Reference {

    /// Select the given representation for this reference, if it is currently unrepresented

    /// and the representation exists for the underlying variable.

    ///

    /// # Errors

    /// - [ReprSelectError::AlreadySelected] if a different representation is already selected for this reference

    /// - [ReprSelectError::DoesNotExist] if the representation does not exist for this variable

    ///

    /// # Returns

    /// State of the initialised representation

    /// Same as [Reference::select_repr], but type-erased

        {

    /// Same as [Reference::select_or_init_repr], but type-erased

        {

    /// Select the given representation for this reference, initialising it if necessary.

    /// Will fail if a different representation is already selected.

    ///

    /// # Errors

    /// - [ReprSelectError] if a different representation is already selected for this reference

    /// - [ReprInitError] | [ReprInstantiateError] if the representation could not be initialised

    ///

    /// # Returns

    ///

    /// `(state, symbols, constraints)`

    /// where:

    /// - `state` is an instance of the given representation

    /// - `symbols` are new variables created by the representation

    /// - `constraints` are new top-level constraints created by the representation

    /// Select the given representation for this reference, initialising it if necessary.

    /// Will overwrite the existing selection.

    ///

    /// # Errors

    /// - [ReprInitError] | [ReprInstantiateError] if the representation could not be initialised

    ///

    /// # Returns

    ///

    /// `(state, symbols, constraints)`

    /// where:

    /// - `state` is an instance of the given representation

    /// - `symbols` are new variables created by the representation

    /// - `constraints` are new top-level constraints created by the representation

    /// Same as [Reference::update_or_init_repr], but type-erased

    /// If this reference has a representation selected, return `(rule, state)`

    /// where

    /// - `rule` is a pointer to the representation rule

    /// - `state` is an instance of that representation

    /// If this reference has this specific representation selected, get its state as a concrete type

        {

    /// If this reference has a representation selected, return its state, otherwise crash

            .unwrap_or_else(|| bug!("`{}` had no representation", self.name()));

                bug!(

                    "Representation '{}' was selected for '{}' but its state was not stored!",

                )

            })

    /// If this reference has this specific representation selected, return its state

    /// as a concrete type, otherwise crash

            bug!(

                "`{}` did not have the expected representation `{}`",

            )

        })

    /// Returns the expression behind a value-letting reference, if this is one.

    ///

    /// Prefer [`Reference::with_resolved_expression`] when the expression only needs to be

    /// inspected. Returning an owned value here necessarily clones collection-bearing

    /// expressions such as matrix literals.

        let generator = {

            } else {

            }

        };

        {

    /// The formula named by this boolean value letting, when that formula is not an atom.

    ///

    /// Constants and aliases of decision variables return [`None`]: those names already stand for

    /// a value. An alias of another value letting returns that reference, so the caller can follow

    /// the chain. Unit `or`/`and` removal rewrites a singleton connective down to the remaining

    /// name, and that name is still a connective.

    /// Calls `inspect` with the expression behind a value-letting reference.

    ///

    /// The declaration is kept read-locked for the duration of `inspect`, allowing callers to ask

    /// questions about large value lettings without cloning them. Quantified declarations may

    /// delegate their value to an expression generator; those are handled here as well.

        let generator = {

            } else {

            }

    /// Evaluates this reference to a literal if it resolves to a constant.

    /// Resolves this reference to an atomic expression, if possible.

        .flatten()

}

/// True when a value-letting body should be read as a boolean formula rather than as an atom.

        other => {

                    Expression::Not(_, _)

                        | Expression::Or(_, _)

                        | Expression::And(_, _)

                        | Expression::Imply(_, _, _)

                        | Expression::Iff(_, _, _)

                        | Expression::Eq(_, _, _)

                        | Expression::Neq(_, _, _)

                        | Expression::Geq(_, _, _)

                        | Expression::Leq(_, _, _)

                        | Expression::Gt(_, _, _)

                        | Expression::Lt(_, _, _)

                        | Expression::FlatIneq(_, _, _, _)

                        | Expression::MinionReify(_, _, _)

                        | Expression::MinionReifyImply(_, _, _)

                )

        }

    }

impl From<Reference> for Expression {

}

impl From<Reference> for Moo<Expression> {

}

impl From<DeclarationPtr> for Reference {

}

impl CategoryOf for Reference {

}

impl HasDomain for Reference {

                bug!(

                    "reference ({name}) should have a domain",

                )

            })

}

impl Display for Reference {

}