use conjure_cp::{

    ast::Metadata,

    ast::{

        AbstractLiteral, Atom, DeclarationPtr, Expression as Expr, Literal, Moo, Name, SymbolTable,

        categories::Category,

    },

};

use tracing::{instrument, trace};

/// True iff `expr` is an `Atom`.

/// True iff `expr` is an `Atom` or `Not(Atom)`.

    }

/// True if `expr` is flat; i.e. it only contains atoms.

    }

/// Returns the arity of a tuple constant expression, if this expression is one.

        }

/// Returns record field names of a record constant expression, if this expression is one.

        }

    }

/// True if the entire AST is constants.

            _ => {

            }

        }

    }

/// Converts a vector of expressions to a vector of atoms.

///

/// # Returns

///

/// `Some(Vec<Atom>)` if the vectors direct children expressions are all atomic, otherwise `None`.

#[allow(dead_code)]

    }

/// Creates a new auxiliary variable using the given expression.

///

/// # Returns

///

/// * `None` if `Expr` is a `Atom`, or `Expr` does not have a domain (for example, if it is a `Bubble`).

///

/// * `Some(ToAuxVarOutput)` if successful, containing:

///

///     + A new symbol table, modified to include the auxiliary variable.

///     + A new top level expression, containing the declaration of the auxiliary variable.

///     + A reference to the auxiliary variable to replace the existing expression with.

///

    // No need to put an atom in an aux_var

    // Anything that should be bubbled, bubble

    // Do not put abstract literals containing expressions into aux vars.

    //

    // e.g. for `[1,2,3,f/2,e][e]`, the lhs should not be put in an aux var.

    //

    // instead, we should flatten the elements inside this abstract literal, or wait for it to be

    // turned into an atom, or an abstract literal containing only literals - e.g. through an index

    // or slice operation.

    //

                why = "expression is an abstract literal",

                "to_aux_var() failed"

            );

    // Only flatten an expression if it contains decision variables or decision variables with some

    // constants.

    //

    // i.e. dont flatten things containing givens, quantified variables, just constants, etc.

    {

                why = "expression has sub-expressions that are not in the decision category",

                "to_aux_var() failed"

            );

    // FIXME: why does removing this make tests fail!

    //

    // do not put matrix[e] in auxvar

    //

    // eventually this will rewrite into an indomain constraint, or a single variable.

    //

    // To understand why deferring this until a lower level constraint is chosen is good, consider

    // the comprehension:

    //

    // and([m[i] = i + 1  | i: int(1..5)])

    //

    // Here, if we rewrite inside the comprehension, we will end up making the auxvar

    // __0  = m[i].

    //

    // When we expand the matrix, this will expand to:

    //

    // __0 = m[1]

    // __1 = m[2]

    // __2 = m[3]

    // __3 = m[4]

    // __4 = m[5]

    //

    //

    // These all rewrite to variable references (e.g. m[1] ~> m#matrix_to_atom_1), so these auxvars

    // are redundant. However, we don't know this before expanding, as they are just m[i].

    //

    // In the future, we can do this more fine-grained using categories (e.g. only flatten matrices

    // indexed by expressions with the decision variable category) : however, doing this for

    // all matrix indexing is fine, as they can be rewritten into a lower-level expression, then

    // flattened.

    };

/// Output data of `to_aux_var`.

    symbols: SymbolTable,

    _unconstructable: (),

}

impl ToAuxVarOutput {

    /// Returns the new auxiliary variable as an `Atom`.

    /// Returns the new auxiliary variable as an `Expression`.

    ///

    /// This expression will have default `Metadata`.

    /// Returns the top level `Expression` to add to the model.

    /// Returns the new `SymbolTable`, modified to contain this auxiliary variable in the symbol table.

}