use super::{

    Atom, CnfClause, DeclarationPtr, Expression, Literal, Metadata, Moo, ReturnType, SymbolTable,

    SymbolTablePtr, Typeable,

    comprehension::Comprehension,

    declaration::DeclarationKind,

    pretty::{

        pretty_clauses, pretty_domain_letting_declaration, pretty_expressions_as_top_level,

        pretty_value_letting_declaration, pretty_variable_declaration,

    },

    serde::PtrAsInner,

};

use itertools::izip;

use serde::{Deserialize, Serialize};

use serde_with::serde_as;

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

use crate::{bug, into_matrix_expr};

use parking_lot::{RwLockReadGuard, RwLockWriteGuard};

use std::hash::Hash;

use std::{collections::VecDeque, fmt::Display};

/// A sub-model, representing a lexical scope in the model.

///

/// Each sub-model contains a symbol table representing its scope, as well as a expression tree.

///

/// The expression tree is formed of a root node of type [`Expression::Root`], which contains a

/// vector of top-level constraints.

#[serde_as]

#[derive(Clone, PartialEq, Eq, Debug, Hash, Serialize, Deserialize)]

pub struct SubModel {

    constraints: Moo<Expression>,

    #[serde_as(as = "PtrAsInner")]

    symbols: SymbolTablePtr,

    cnf_clauses: Vec<CnfClause>, // CNF clauses

}

impl SubModel {

    /// Creates a new [`Submodel`] with no parent scope.

    ///

    /// Top level models are represented as [`Model`](super::model): consider using

    /// [`Model::new`](super::Model::new) instead.

    #[doc(hidden)]

    /// Creates a new [`Submodel`] as a child scope of `parent`.

    ///

    /// `parent` should be the symbol table of the containing scope of this sub-model.

    /// The symbol table for this sub-model as a pointer.

    ///

    /// The caller should only mutate the returned symbol table if this method was called on a

    /// mutable model.

    /// The symbol table for this sub-model as a mutable pointer.

    ///

    /// The caller should only mutate the returned symbol table if this method was called on a

    /// mutable model.

    /// The symbol table for this sub-model as a reference.

    /// The symbol table for this sub-model as a mutable reference.

    /// The root node of this sub-model.

    ///

    /// The root node is an [`Expression::Root`] containing a vector of the top level constraints

    /// in this sub-model.

    /// The root node of this sub-model, as a mutable reference.

    ///

    /// The caller is responsible for ensuring that the root node remains an [`Expression::Root`].

    ///

    /// Replaces the root node with `new_root`, returning the old root node.

    ///

    /// # Panics

    ///

    /// - If `new_root` is not an [`Expression::Root`].

        };

        // INVARIANT: already checked that `new_root` is an [`Expression::Root`]

    /// The top-level constraints in this sub-model.

            bug!("The top level expression in a submodel should be Expr::Root");

        };

    /// The cnf clauses in this sub-model.

    /// The top-level constraints in this sub-model as a mutable vector.

            bug!("The top level expression in a submodel should be Expr::Root");

        };

    /// The cnf clauses in this sub-model as a mutable vector.

    /// Replaces the top-level constraints with `new_constraints`, returning the old ones.

    /// Replaces the cnf clauses with `new_clauses`, returning the old ones.

    /// Adds a top-level constraint.

    /// Adds a cnf clause.

    /// Adds top-level constraints.

    /// Adds cnf clauses.

    /// Adds a new symbol to the symbol table

    /// (Wrapper over `SymbolTable.insert`)

    /// Converts the constraints in this submodel to a single expression suitable for use inside

    /// another expression tree.

    ///

    /// * If this submodel has no constraints, true is returned.

    /// * If this submodel has a single constraint, that constraint is returned.

    /// * If this submodel has multiple constraints, they are returned as an `and` constraint.

        }

}

impl Typeable for SubModel {

}

impl Display for SubModel {

    #[allow(clippy::unwrap_used)] // [rustdocs]: should only fail iff the formatter fails

                DeclarationKind::Find(_) => {

                        "{}",

                }

                DeclarationKind::ValueLetting(_) => {

                        "{}",

                }

                DeclarationKind::DomainLetting(_) => {

                        "{}",

                }

                }

                }

                DeclarationKind::RecordField(_) => {

                    // Do not print a record field as it is an internal type

                    // TODO: is this correct?

                }

            }

        }

}

// Using manual implementations of Uniplate so that we can update the old Rc<RefCell<<>>> with the

// new value instead of creating a new one. This will keep the parent pointers in sync.

//

// I considered adding Rc RefCell shared-mutability to Uniplate, but I think this is unsound in

// generality: e.g. two pointers to the same object are in our tree, and both get modified in

// different ways.

//

// Shared mutability is probably fine here, as we only have one pointer to each symbol table

// reachable via Uniplate, the one in its Submodel. The SymbolTable implementation doesn't return

// or traverse through the parent pointers.

//

// -- nd60

impl Uniplate for SubModel {

        // Look inside constraint tree and symbol tables.

            };

                bug!("root expression not root");

            };

}

impl Biplate<Expression> for SubModel {

        // Return constraints tree and look inside symbol table.

            };

            };

                bug!("root expression not root");

            };

}

impl Biplate<SubModel> for SubModel {

        (

                };

        )

}

impl Biplate<Atom> for SubModel {

        // As atoms are only found in expressions, create a tree of atoms by

        //

        //  1. getting the expression tree

        //  2. Turning that into a list

        //  3. For each expression in the list, use Biplate<Atom> to turn it into an atom

        //

        //  Reconstruction works in reverse.

        // Let the atom tree be a Tree::Many where each element is the result of running Biplate<Atom>::biplate on an expression in the expression list.

            // 1. reconstruct expression_list from the atom tree

            };

                "the number of children should not change when using Biplate"

            );

            // 2. reconstruct expression_tree from expression_list

            // 3. reconstruct submodel from expression_tree

}

impl Biplate<Comprehension> for SubModel {

            };

                bug!("root expression not root");

            };

}