use std::cell::RefCell;

use std::collections::BTreeSet;

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

use std::hash::Hash;

use std::rc::Rc;

use thiserror::Error;

use crate::Model;

use crate::ast::{CnfClause, DeclarationPtr, Expression, Name, SymbolTable};

use crate::rule_engine::RuleData;

use crate::rule_engine::rewriter_common::{RuleResult, log_rule_application};

use tree_morph::prelude::Commands;

use tree_morph::prelude::Rule as MorphRule;

#[derive(Clone, Debug, Default)]

pub(crate) struct MorphState {

    pub symbols: SymbolTable,

    pub clauses: Vec<CnfClause>,

}

#[derive(Debug, Error)]

pub enum ApplicationError {

    #[error("Rule is not applicable")]

    RuleNotApplicable,

    #[error("Could not calculate the expression domain")]

    DomainError,

}

/// Represents the result of applying a rule to an expression within a model.

///

/// A `Reduction` encapsulates the changes made to a model during a rule application.

/// It includes a new expression to replace the original one, an optional top-level constraint

/// to be added to the model, and any updates to the model's symbol table.

///

/// This struct allows for representing side-effects of rule applications, ensuring that

/// all modifications, including symbol table expansions and additional constraints, are

/// accounted for and can be applied to the model consistently.

///

/// # Fields

/// - `new_expression`: The updated [`Expression`] that replaces the original one after applying the rule.

/// - `new_top`: An additional top-level [`Vec<Expression>`] constraint that should be added to the model. If no top-level

///   constraint is needed, this field can be set to an empty vector [`Vec::new()`].

/// - `symbols`: A [`SymbolTable`] containing any new symbol definitions or modifications to be added to the model's

///   symbol table. If no symbols are modified, this field can be set to an empty symbol table.

///

/// # Usage

/// A `Reduction` can be created using one of the provided constructors:

/// - [`Reduction::new`]: Creates a reduction with a new expression, top-level constraint, and symbol modifications.

/// - [`Reduction::pure`]: Creates a reduction with only a new expression and no side-effects on the symbol table or constraints.

/// - [`Reduction::with_symbols`]: Creates a reduction with a new expression and symbol table modifications, but no top-level constraint.

/// - [`Reduction::with_top`]: Creates a reduction with a new expression and a top-level constraint, but no symbol table modifications.

/// - [`Reduction::cnf`]: Creates a reduction with a new expression, cnf clauses and symbol modifications, but no no top-level constraints.

///

/// The `apply` method allows for applying the changes represented by the `Reduction` to a [`Model`].

///

/// # Example

/// ```

/// // Need to add an example

/// ```

///

/// # See Also

/// - [`ApplicationResult`]: Represents the result of applying a rule, which may either be a `Reduction` or an `ApplicationError`.

/// - [`Model`]: The structure to which the `Reduction` changes are applied.

#[non_exhaustive]

#[derive(Clone, Debug)]

pub struct Reduction {

    pub new_expression: Expression,

    pub new_top: Vec<Expression>,

    pub symbols: SymbolTable,

    pub new_clauses: Vec<CnfClause>,

}

/// The result of applying a rule to an expression.

/// Contains either a set of reduction instructions or an error.

pub type ApplicationResult = Result<Reduction, ApplicationError>;

impl Reduction {

    /// Represents a reduction with no side effects on the model.

    /// Represents a reduction that also modifies the symbol table.

    /// Represents a reduction that also adds a top-level constraint to the model.

    /// Represents a reduction that also adds clauses to the model.

    /// Applies side-effects (e.g. symbol table updates)

    /// Gets symbols added by this reduction

    /// Gets symbols changed by this reduction

    ///

    /// Returns a list of tuples of (name, domain before reduction, domain after reduction)

            };

        }

}

/// The function type used in a [`Rule`].

pub type RuleFn = fn(&Expression, &SymbolTable) -> ApplicationResult;

/**

 * A rule with a name, application function, and rule sets.

 *

 * # Fields

 * - `name` The name of the rule.

 * - `application` The function to apply the rule.

 * - `rule_sets` A list of rule set names and priorities that this rule is a part of. This is used to populate rulesets at runtime.

 */

#[derive(Clone, Debug)]

pub struct Rule<'a> {

    pub name: &'a str,

    pub application: RuleFn,

    pub rule_sets: &'a [(&'a str, u16)], // (name, priority). At runtime, we add the rule to rulesets

    /// Discriminant ids of Expression variants this rule applies to, or None for universal rules.

    pub applicable_to: Option<&'static [usize]>,

}

impl<'a> Rule<'a> {

}

impl Display for Rule<'_> {

}

impl PartialEq for Rule<'_> {

}

impl Eq for Rule<'_> {}

impl Hash for Rule<'_> {

}

impl MorphRule<Expression, MorphState> for Rule<'_> {

}

impl MorphRule<Expression, MorphState> for &Rule<'_> {

}

impl MorphRule<Expression, Rc<RefCell<MorphState>>> for Rule<'_> {

}

impl MorphRule<Expression, MorphState> for RuleData<'_> {

}