use std::fmt;

use std::ops::Deref;

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

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

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

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

use crate::set_automaton::MatchAnnouncement;

use crate::set_automaton::SetAutomaton;

use crate::utilities::ExplicitPosition;

use crate::Rule;

use mcrl2::aterm::Protected;

use mcrl2::aterm::TermPool;

use mcrl2::data::DataExpression;

use mcrl2::data::DataExpressionRef;

use super::create_var_map;

use super::substitute_with;

use super::PositionIndexed;

use super::SemiCompressedTermTree;

use super::SubstitutionBuilder;

/// 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>,

    /// Right hand side is stored in the term pool as much as possible with a SemiCompressedTermTree

    pub semi_compressed_rhs: SemiCompressedTermTree,

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

    pub is_duplicating: bool,

}

impl AnnouncementSabre {

}

/// 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 ExplicitPosition>,

}

/// 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.

#[derive(Debug)]

pub(crate) enum SideInfoType<'a> {

    SideBranch(&'a [(ExplicitPosition, 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> {

    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,

    pub substitution_builder: SubstitutionBuilder,

}

impl<'a> ConfigurationStack<'a> {

    /// 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

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

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

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

    /// 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.

    /// 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.

    /// If store_intermediate is true, all configurations below 'end' are also up to date.

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

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

                }

            };

        }

    /// 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<'_> {

                }

            }

        }

}

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

                }

            }

            }

            }

        }

}