use std::{

    cell::RefCell,

    collections::{BTreeSet, HashMap, VecDeque},

    sync::{Arc, Mutex},

};

use conjure_cp::{

    ast::{

        Atom, DeclarationPtr, Expression, Metadata, Model, Moo, Name, Reference, ReturnType,

        SymbolTable, Typeable as _,

        ac_operators::ACOperatorKind,

        comprehension::{Comprehension, ComprehensionQualifier},

        serde::HasId as _,

    },

    bug_assert,

    rule_engine::resolve_rule_sets,

    settings::{SolverFamily, current_rewriter},

    solver::{Solver, SolverError, adaptors::Minion},

};

use tracing::debug;

use uniplate::{Biplate, zipper::Zipper};

use super::via_solver_common::{

    detach_symbols, instantiate_return_expressions_from_values, retain_quantified_solution_values,

    rewrite_model_with_configured_rewriter, simplify_expression, split_symbolic_guards,

    temporarily_materialise_quantified_vars_as_finds, with_temporary_model,

};

/// Expands the comprehension using Minion, returning the resulting expressions.

///

/// This method is only suitable for comprehensions inside an AC operator. The AC operator that

/// contains this comprehension should be passed into the `ac_operator` argument.

///

/// This method performs additional pruning of "uninteresting" values, only possible when the

/// comprehension is inside an AC operator.

    // Guards over non-quantified decision variables belong to the outer model, not the generator

    // submodel; hold them back and re-apply them per element with this operator's skip semantics.

    // Add the return-expression constraint only when it can restrict at least one quantified

    // variable. If dummy replacement removes every quantified dependency, the constraint cannot

    // prune the generator assignments and ordinary guard-only solver expansion is cheaper.

    // REWRITE GENERATOR MODEL AND PASS TO MINION

    // ==========================================

    // REWRITE RETURN EXPRESSION

    // =========================

    // Keep return expressions unreduced until quantified assignments are substituted.

    // Rewriting before substitution can introduce index auxiliaries that remain symbolic and may

    // produce unsupported Minion shapes after expansion.

    let return_expression_model =

    let values = {

        // Minion expects quantified variables in the temporary generator model as find

        // declarations. Keep this conversion scoped to solver-backed expansion.

        let _temp_finds =

        // Rewrite with quantified vars materialised as finds so Minion flattening can

        // introduce auxiliaries for constraints involving quantified variables.

        let solver_model =

            Err(e) => {

                // Callers fall back to native expansion, so this is a routine outcome rather

                // than a problem; the model is large, so keep it out of the default log.

                debug!(why=%e,model=%generator_model,"Loading generator model failed, failing solver-backed AC comprehension expansion rule");

            }

        };

        // SOLVE FOR THE QUANTIFIED VARIABLES, AND SUBSTITUTE INTO THE RETURN EXPRESSION

        // ============================================================================

        tracing::debug!(model=%generator_model,comprehension=%comprehension,"Minion solving comprehnesion (ac mode)");

            // Only keep quantified assignments; discard solver auxiliaries/locals.

    };

/// Build the detached AC generator model and add its derived return constraint when useful.

        // A nested comprehension may have generator domains depending on variables this model is

        // still solving for. It is expanded later, once those variables have concrete bindings.

    let constraint = {

    };

/// True iff `expr` contains a comprehension.

///

/// Comprehensions are leaves of the traversal, so this finds nested ones without descending into

/// their own scopes.

/// Eliminate all references to non-quantified variables by introducing dummy variables, then

/// derive the constraint that discards AC-identity return values.

///

/// Dummy variables must be the same type as the AC operators identity value.

///

/// To reduce the number of dummy variables, we turn the largest expression containing only

/// non-quantified variables and of the correct type into a dummy variable.

///

/// If there is no such expression, (e.g. and[(a<i) | i: int(1..10)]) , we use the smallest

/// expression of the correct type that contains a non-quantified variable. This ensures that

/// we lose as few references to quantified variables as possible.

    // for sum/product we want to put integer expressions into dummy variables,

    // for and/or we want to put boolean expressions into dummy variables.

    'outer: loop {

        let (non_quantified_vars, quantified_references) =

        // an expression or its descendants needs to be turned into a dummy variable if it

        // contains non-quantified variables.

        // does this expression contain quantified variables?

        // can this expression be turned into a dummy variable?

        // The expression and its descendants don't need a dummy variables, so we don't

        // need to descend into its children.

            // go to next node or quit

                    // visited all nodes

                };

            }

        // The expression contains non-quantified variables:

        // does this expression have any children that can be turned into dummy variables?

            // eligible if it can be turned into a dummy variable, and turning it into a

            // dummy variable removes a non-quantified variable from the model.

        // This expression has no child that can be turned into a dummy variable, but can

        // be a dummy variable => turn it into a dummy variable and continue.

            // introduce dummy var and continue

            // go to next node

                    // visited all nodes

                };

            }

        }

        // This expression has no child that can be turned into a dummy variable, and

        // cannot be a dummy variable => backtrack upwards to find a parent that can be a

        // dummy variable, and make it a dummy variable.

            // TODO: remove this case, make has_eligible_child check better?

            // go upwards until we find something that can be a dummy variable, make it

            // a dummy variable, then continue.

                    // TODO: this expression we are rewritng might already contain

                    // dummy vars - we might need a pass to get rid of the unused

                    // ones!

                    //

                    // introduce dummy var and continue

                    // go to next node

                            // visited all nodes

                        };

                    }

            }

        }

        // If the expression contains quantified variables as well as non-quantified

        // variables, try to retain the quantified variables by finding a child that can be

        // made a dummy variable which has only non-quantified variables.

        }

        // This expression contains no quantified variables, so no point trying to turn a

        // child into a dummy variable.

            // introduce dummy var and continue

            // go to next node

                    // visited all nodes

                };

            }

        } else {

        }

    }

    // double check that the above transformation didn't miss any stray non-quantified vars

    bug_assert!(

        "generator model should only contain references to variables in its symbol table."

    );

/// Replaces references to declarations outside `symtab` with local dummy declarations.

///

/// This preserves locality by construction for temporary generator models passed to Minion.

/// All rewrites then operate purely on local references and cannot reintroduce parent-scope vars.

        {

            }

        }

        };

        // Already local to this temporary generator model.

        } else {

            let new_dummy = {

                });

            };

        };

/// Returns the non-quantified and quantified references inside the expression.

///

/// Membership is tested against the comprehension's original quantified names. In particular,

/// dummy declarations introduced while localising outer references are local to the temporary

/// model but remain non-quantified for pruning analysis.

#[inline]

    let (non_quantified_vars, quantified_vars): (VecDeque<Name>, VecDeque<Name>) =

/// Returns `true` if `expr` can be turned into a dummy variable.

#[inline]

    // do not put root expression in a dummy variable or things go wrong.

    // is the expression the same type as the dummy variable?

/// Returns `true` if `expr` or its descendants contains non-quantified variables.

#[inline]