use std::fmt;

use merc_aterm::Protected;

use merc_aterm::Term;

use merc_aterm::storage::ThreadTermPool;

use merc_data::DataExpression;

use merc_data::DataExpressionRef;

use crate::Rule;

use crate::matching::conditions::EMACondition;

use crate::matching::conditions::extend_conditions;

use crate::matching::nonlinear::EquivalenceClass;

use crate::matching::nonlinear::derive_equivalence_classes;

use crate::set_automaton::MatchAnnouncement;

use crate::set_automaton::SetAutomaton;

use super::DataPosition;

use super::DataPositionIndexed;

use super::DataSubstitutionBuilder;

use super::TermStack;

use super::create_var_map;

use super::data_substitute_with;

/// This is the announcement for Sabre, which stores additional information about the rewrite rules.

#[derive(Hash, Eq, PartialEq, Ord, PartialOrd, Debug)]

pub struct AnnouncementSabre {

    /// Positions in the pattern with the same variable, for non-linear patterns

    pub equivalence_classes: Vec<EquivalenceClass>,

    /// Conditions for applying the rule.

    pub conditions: Vec<EMACondition>,

    /// The right hand side stored such that it can be substituted easily.

    pub rhs_term_stack: TermStack,

    /// Whether the rewrite rule duplicates subterms, e.g. times(s(x), y) = plus(y, times(x, y))

    pub is_duplicating: bool,

}

impl AnnouncementSabre {

        // Compute the extra information for the InnermostRewriter.

        // Create a mapping of where the variables are and derive SemiCompressedTermTrees for the

        // rhs of the rewrite rule and for lhs and rhs of each condition.

        // Also see the documentation of SemiCompressedTermTree

}

/// A Configuration is part of the configuration stack/tree

/// It contains:

///     1. the index of a state of the set automaton

///     2. The subterm at the position of the configuration.

///     3. The difference of position compared to the parent configuration (None for the root).

///         Note that it stores a reference to a position. It references the position listed on

///         a transition of the set automaton.

#[derive(Debug)]

pub(crate) struct Configuration<'a> {

    pub state: usize,

    pub position: Option<&'a DataPosition>,

}

/// SideInfo stores additional information of a configuration. It stores an

/// index of the corresponding configuration on the configuration stack.

#[derive(Debug)]

pub(crate) struct SideInfo<'a> {

    pub corresponding_configuration: usize,

    pub info: SideInfoType<'a>,

}

/// A "side stack" is used besides the configuration stack to

/// remember a couple of things. There are 4 options.

///

/// 1. There is nothing on the side stack for this

///    configuration. This means we have never seen this

///    configuration before. It is a bud that needs to be

///    explored.

///

/// In the remaining three cases we have seen the

/// configuration before and have pruned back, either because

/// of applying a rewrite rule or just because our depth

/// first search has hit the bottom and needs to explore a

/// new branch.

///

/// 2. There is a side branch. That means we had a hyper

///    transition. The configuration has multiple children in

///    the overall tree. We have already explored some of these

///    child configurations and parked the remaining on the side

///    stack. We are going to explore the next child

///    configuration.

///

/// 3. There is a delayed rewrite rule. We had found a

///    matching rewrite rule the first time visiting this

///    configuration but did not want to apply it yet. At the

///    moment this is the case for "duplicating" rewrite rules

///    that copy some subterms. We first examine side branches

///    on the side stack, meaning that we have explored all

///    child configurations. Which, in turn, means that the

///    subterms of the term in the current configuration are in

///    normal form. Thus the duplicating rewrite rule only

///    duplicates terms that are in normal form.

///

/// 4. There is another type of delayed rewrite rule: one

///    that is non-linear or has a condition. We had found a

///    matching rewrite rule the first time visiting this

///    configuration but our strategy dictates that we only

///    perform the condition check and check on the equivalence

///    of positions when the subterms are in normal form. We

///    perform the checks and apply the rewrite rule if it

///    indeed matches.

pub(crate) enum SideInfoType<'a> {

    SideBranch(&'a [(DataPosition, usize)]),

    DelayedRewriteRule(&'a MatchAnnouncement, &'a AnnouncementSabre),

    EquivalenceAndConditionCheck(&'a MatchAnnouncement, &'a AnnouncementSabre),

}

/// A configuration stack. The first element is the root of the configuration tree.

#[derive(Debug)]

pub(crate) struct ConfigurationStack<'a, 'b> {

    pub stack: Vec<Configuration<'a>>,

    pub terms: Protected<Vec<DataExpressionRef<'static>>>,

    /// Separate stack with extra information on some configurations

    pub side_branch_stack: Vec<SideInfo<'a>>,

    /// Current node. Becomes None when the configuration tree is completed

    pub current_node: Option<usize>,

    /// Upon applying a rewrite rule we do not immediately update the subterm stored in every configuration on the stack.

    /// That would be very expensive. Instead we ensure that the subterm in the current_node is always up to date.

    /// oldest_reliable_subterm is an index to the highest configuration in the tree that is up to date.

    pub oldest_reliable_subterm: usize,

    /// A reusable substitution builder, borrowed from the caller so that a

    /// protected container is not registered on every rewrite call.

    pub substitution_builder: &'b mut DataSubstitutionBuilder,

}

impl<'a, 'b> ConfigurationStack<'a, 'b> {

    /// Initialise the stack with one Configuration containing 'term' and the initial state of the set automaton

    /// Obtain the first unexplored node of the stack, which is just the top of the stack.

    /// Returns the lowest configuration in the tree with SideInfo

    /// Grow a Configuration with index c. tr_slice contains the hypertransition to possibly multiple states

        // Pick the first transition to grow the stack

        // If there are more transitions store the remaining on the side stack

        // Create a new configuration and push it onto the stack

        // Push the term belonging to the leaf.

        // Safety: t is pushed into the container on the next line.

    /// When rewriting prune "prunes" the configuration stack to the place where the first symbol

    /// of the matching rewrite rule was observed (at index 'depth').

        // Reroll the configuration stack by truncating the Vec (which is a constant time operation)

        // Remove side info for the deleted configurations

        // Update the subterm stored at the prune point.

        // Note that the subterm stored earlier may not have been up to date. We replace it with a term that is up to date

        // Safety: subterm is stored in the container on the next line.

        };

    /// Removes side info for configurations beyond configuration index 'end'.

    /// If 'including' is true the side info for the configuration with index 'end' is also deleted.

        loop {

                None => {

                }

                }

            }

        }

    /// Roll back the configuration stack to level 'depth'.

    /// This function is used exclusively when a subtree has been explored and no matches have been found.

        // Updated subterms may have to be propagated up the configuration tree.

        // Only the subterm at 'depth' needs to be correct: everything below it is

        // truncated away immediately afterwards.

    /// When going back up the configuration tree the subterms stored in the configuration tree must be updated

    /// This function ensures that the Configuration at depth 'end' is made up to date.

        // Check if there is anything to do. Start updating from self.oldest_reliable_subterm

        // Safety: subterm is kept in write_terms throughout this function.

        // Go over the configurations one by one until we reach 'end'. The running

        // subterm is stored back into the container at every level rather than

        // held as an owned protected term.

            // If the position is not deepened nothing needs to be done, otherwise substitute on the position stored in the configuration.

                    );

                    // Safety: subterm is kept in write_terms throughout this function.

                }

            };

            // Safety: subterm is stored in the container on the next line.

        }

    /// Final term computed by integrating all subterms up to the root configuration

    /// Returns a SideInfoType object if there is side info for the configuration with index 'leaf_index'

        };

        } else {

        }

}

impl fmt::Display for ConfigurationStack<'_, '_> {

                "    Position: {}",

                }

            }

        }

}

impl fmt::Debug for SideInfoType<'_> {

                }

            }

            }

            }

        }

}