use std::collections::HashSet;

use std::fmt;

use std::ops::ControlFlow;

use log::debug;

use merc_syntax::FixedPointOperator;

use merc_syntax::StateFrm;

use merc_syntax::StateVarDecl;

use merc_syntax::apply_statefrm;

use merc_syntax::visit_statefrm;

/// A fixpoint equation system representing a ranked set of fixpoint equations.

///

/// Each equation is of the shape `{mu, nu} X(args...) = rhs`. Where rhs

/// contains no further fixpoint equations.

pub struct ModalEquationSystem {

    equations: Vec<Equation>,

}

/// A single fixpoint equation of the shape `{mu, nu} X(args...) = rhs`.

#[derive(Clone)]

pub struct Equation {

    operator: FixedPointOperator,

    variable: StateVarDecl,

    rhs: StateFrm,

}

impl Equation {

    /// Returns the operator of the equation.

    /// Returns the variable declaration of the equation.

    /// Returns the body of the equation.

}

impl From<Equation> for StateFrm {

}

impl ModalEquationSystem {

    /// Converts a plain state formula into a fixpoint equation system.

        // Ensure that the formula has an outermost fixpoint operator.

        // Apply E to extract all equations from the formula

        // Check that there are no duplicate variable names

            "Duplicate variable names found in fixpoint equation system"

        );

            "At least one fixpoint equation expected in the equation system"

        );

    /// Returns the ith equation in the system.

    /// Returns the number of equations in the system.

    /// Returns true if the system contains no equations.

    /// The alternation depth is a complexity measure of the given formula.

    ///

    /// # Details

    ///

    /// The alternation depth of mu X . psi is defined as the maximum chain X <= X_1 <= ... <= X_n,

    /// where X <= Y iff X appears freely in the corresponding equation sigma Y . phi. And furthermore,

    /// X_0, X_2, ... are bound by mu and X_1, X_3, ... are bound by nu. Similarly, for nu X . psi. Note

    /// that the alternation depth of a formula with a rhs is always 1, since the chain cannot be extended.

    /// Finds an equation by its variable identifier.

    ///

    /// # Details

    ///

    /// This is a linear scan over the equations, and is also called from within

    /// [`Self::alternation_depth`]'s recursion. Equation systems correspond to a

    /// single (modal) formula and are therefore small, so an index map is not

    /// worth its maintenance cost; revisit if very large formulas become common.

    /// Recursive helper function to compute the alternation depth of equation `i`.

                } else {

                            } else {

                            })

                    } else {

                        // Only consider nested equations

                    }

                }

            }

            _ => {

            }

        }

}

/// If the given formula has no outermost fixpoint operator, adds a placeholder

/// fixpoint operator around it.

        // The outer operator is already a fixpoint

    } else {

        // Introduce a placeholder.

    }

/// Applies `E` to the given formula, adding equations to the given vector.

///

/// E(nu X. f) = (nu X = RHS(f)) + E(f)

/// E(mu X. f) = (mu X = RHS(f)) + E(f)

/// E(g) = ... (traverse all the subformulas of g and apply E to them)

        StateFrm::FixedPoint {

        } => {

            // Add the equation with the renamed variable (the span is the same as the original variable).

        }

/// Applies `RHS` to the given formula.

///

/// RHS(true) = true

/// RHS(false) = false

/// RHS(<a>f) = <a>RHS(f)

/// RHS([a]f) = [a]RHS(f)

/// RHS(f1 && f2) = RHS(f1) && RHS(f2)

/// RHS(f1 || f2) = RHS(f1) || RHS(f2)

/// RHS(X) = X

/// RHS(mu X. f) = X(args)

/// RHS(nu X. f) = X(args)

        // RHS(mu X. phi) = X(args)

        ))),

/// A generator for fresh state variable names.

pub struct FreshStateVarGenerator {

    used: HashSet<String>,

}

impl FreshStateVarGenerator {

    /// Creates a new fresh state variable generator.

    ///

    /// # Details

    ///

    /// Traverses the given formula to collect all used variable names.

    /// Generates a fresh state variable name based on the given base.

        loop {

        }

}

impl fmt::Display for ModalEquationSystem {

        }

}

#[cfg(test)]

mod tests {

    use merc_macros::merc_test;

    use merc_syntax::UntypedStateFrmSpec;

    use super::ModalEquationSystem;

    #[merc_test]

    fn test_fixpoint_equation_system_construction() {

        let formula = UntypedStateFrmSpec::parse("mu X. [a]X && nu Y. <b>true")

            .unwrap()

            .formula;

        let fes = ModalEquationSystem::new(&formula);

        println!("{}", fes);

        assert_eq!(fes.equations.len(), 2);

        assert_eq!(fes.alternation_depth(0), 1);

        assert_eq!(fes.alternation_depth(1), 0);

    }

    #[merc_test]

    fn test_fixpoint_equation_system_example() {

        let formula = UntypedStateFrmSpec::parse(include_str!("../../../examples/vpg/running_example.mcf"))

            .unwrap()

            .formula;

        let fes = ModalEquationSystem::new(&formula);

        println!("{}", fes);

        assert_eq!(fes.equations.len(), 2);

        assert_eq!(fes.alternation_depth(0), 2);

        assert_eq!(fes.alternation_depth(1), 1);

    }

    #[merc_test]

    #[should_panic(expected = "Duplicate variable names found in fixpoint equation system")]

    fn test_fixpoint_equation_system_duplicates() {

        let formula = UntypedStateFrmSpec::parse("mu X. [a]X && (nu Y. <b>true) && (nu Y . <c>X)")

            .unwrap()

            .formula;

        let fes = ModalEquationSystem::new(&formula);

        println!("{}", fes);

        assert_eq!(fes.equations.len(), 3);

    }

}