use std::collections::HashSet;

use std::fs;

use std::path::Path;

use std::path::PathBuf;

use pest::Parser;

use pest_derive::Parser;

use merc_aterm::ATerm;

use merc_aterm::storage::THREAD_TERM_POOL;

use merc_pest_consume::Error;

use merc_pest_consume::Node;

use merc_pest_consume::match_nodes;

use merc_utilities::MercError;

use crate::syntax::ConditionSyntax;

use crate::syntax::RewriteRuleSyntax;

use crate::syntax::RewriteSpecificationSyntax;

#[derive(Parser)]

#[grammar = "rec_grammar.pest"]

pub(crate) struct RecParser;

type ParseResult<T> = Result<T, Error<Rule>>;

type ParseNode<'i> = Node<'i, Rule, ()>;

/// Result of parsing a REC specification containing all extracted components

#[derive(Debug)]

struct RecSpecResult {

    /// Name of the specification

    _name: String,

    /// List of included files

    include_files: Vec<String>,

    /// Constructor symbols with their arities

    constructors: Vec<(String, usize)>,

    /// Variable declarations

    variables: Vec<String>,

    /// Rewrite rules

    rewrite_rules: Vec<RewriteRuleSyntax>,

    /// Terms to evaluate

    eval_terms: Vec<ATerm>,

}

/// Load a REC specification from a specified file.

///

/// Files referenced by the header (`REC-SPEC name : include ...`) are resolved

/// relative to the including file's directory and loaded recursively.

/// Load and join multiple REC specifications.

///

/// Header include directives are *not* resolved here: there is no base

/// directory to resolve them against, so every required specification must be

/// passed explicitly in `specs`.

    }

/// Parses a REC specification. REC files can import other REC files.

/// Returns a RewriteSpec containing all the rewrite rules and a list of terms that need to be rewritten.

/// Recursive worker for [parse_rec]. `visited` records the canonical paths of

/// the files already loaded so that cyclic or diamond includes are not loaded

/// twice (and cannot recurse forever).

    // Initialize return result

    // Use Pest parser (generated automatically from the grammar.pest file)

    // Parse using the consumed-based implementation

    // REC files can import other REC files. Import all referenced by the header.

            // Skip files we have already loaded to break include cycles and

            // avoid duplicating rules on diamond-shaped include graphs.

            // Resolve nested includes relative to the included file itself.

            // Add rewrite rules and terms to the result.

    }

#[merc_pest_consume::parser]

impl RecParser {

    /// Parse a REC specification, returns structured result with all components

    fn rec_spec(spec: ParseNode) -> ParseResult<RecSpecResult> {

        // Extract all sections of the REC file

        match_nodes!(spec.into_children();

            [header((name, include_files)), _sorts, cons(constructors), _opns, vars(variables), rules(rewrite_rules), eval(eval_terms), EOI(_)] => {

                Ok(RecSpecResult {

                    _name: name,

                    include_files,

                    constructors,

                    variables,

                    rewrite_rules,

                    eval_terms,

                })

            },

            [header((name, include_files)), _sorts, cons(constructors), _opns, vars(variables), rules(rewrite_rules), EOI(_)] => {

                Ok(RecSpecResult {

                    _name: name,

                    include_files,

                    constructors,

                    variables,

                    rewrite_rules,

                    eval_terms: Vec::new(),

                })

            }

        )

    }

    /// Extracts data from parsed header of REC spec. Returns name and include files.

    fn header(header: ParseNode) -> ParseResult<(String, Vec<String>)> {

        match_nodes!(header.into_children();

            [identifier(name), identifier(include_files)..] => {

                Ok((name, include_files.collect()))

            }

        )

    }

    /// Extracts data from parsed constructor section, derives the arity of symbols. Types are ignored.

    fn cons(cons: ParseNode) -> ParseResult<Vec<(String, usize)>> {

        let mut constructors = Vec::new();

        match_nodes!(cons.into_children();

            [cons_decl(decls)..] => {

                constructors.extend(decls);

                Ok(constructors)

            }

        )

    }

    /// Parse a constructor declaration

    fn cons_decl(decl: ParseNode) -> ParseResult<(String, usize)> {

        match_nodes!(decl.into_children();

            [identifier(symbol), identifier(params).., identifier(_)] => {

                Ok((symbol, params.len()))

            }

        )

    }

    /// Extracts data from parsed rewrite rules. Returns list of rewrite rules

    fn rules(rules: ParseNode) -> ParseResult<Vec<RewriteRuleSyntax>> {

        match_nodes!(rules.into_children();

            [rewrite_rule(rule_nodes)..] => {

                Ok(rule_nodes.collect())

            }

        )

    }

    /// Parse a rewrite rule

    fn rewrite_rule(rule: ParseNode) -> ParseResult<RewriteRuleSyntax> {

        match_nodes!(rule.into_children();

            [term(lhs), term(rhs), condition(conditions)..] => {

                Ok(RewriteRuleSyntax {

                    lhs,

                    rhs,

                    conditions: conditions.collect(),

                })

            },

            [term(lhs), term(rhs)] => {

                Ok(RewriteRuleSyntax {

                    lhs,

                    rhs,

                    conditions: vec![],

                })

            }

        )

    }

    /// Parse a single rewrite rule

    fn single_rewrite_rule(rule: ParseNode) -> ParseResult<RewriteRuleSyntax> {

        match_nodes!(rule.into_children();

            [rewrite_rule(rule), EOI(_)] => {

                Ok(rule)

            },

        )

    }

    /// Parse a condition in a rewrite rule

    fn condition(condition: ParseNode) -> ParseResult<ConditionSyntax> {

        match_nodes!(condition.into_children();

            [term(lhs), comparison(equality), term(rhs)] => {

                Ok(ConditionSyntax {

                    lhs,

                    rhs,

                    equality,

                })

            }

        )

    }

    /// Parse a comparison operator

    fn comparison(comparison: ParseNode) -> ParseResult<bool> {

        match comparison.as_str() {

            "=" => Ok(true),

            "<>" => Ok(false),

            // The `comparison` grammar rule only matches "=" or "<>".

            other => unreachable!("unexpected comparison operator {other:?}"),

        }

    }

    /// Extracts data from the variable VARS block. Types are ignored.

    fn vars(vars: ParseNode) -> ParseResult<Vec<String>> {

        let mut variables = vec![];

        match_nodes!(vars.into_children();

            [var_decl(var_lists)..] => {

                for var_list in var_lists {

                    variables.extend(var_list);

                }

                Ok(variables)

            }

        )

    }

    /// Parse a variable declaration

    fn var_decl(var_decl: ParseNode) -> ParseResult<Vec<String>> {

        match_nodes!(var_decl.into_children();

            [identifier(vars).., identifier(_type)] => {

                // The last identifier is the type, so we exclude it

                Ok(vars.collect())

            }

        )

    }

    /// Extracts data from parsed EVAL section, returns a list of terms that need to be rewritten.

    fn eval(eval: ParseNode) -> ParseResult<Vec<ATerm>> {

        match_nodes!(eval.into_children();

            [term(terms)..] => {

                Ok(terms.collect())

            }

        )

    }

    /// Parse a term

    fn term(term: ParseNode) -> ParseResult<ATerm> {

        match_nodes!(term.into_children();

            [identifier(head_symbol), args(arguments)] => {

            },

            [identifier(head_symbol)] => {

            }

        )

    }

    /// Parse arguments of a term

    fn args(args: ParseNode) -> ParseResult<Vec<ATerm>> {

        match_nodes!(args.into_children();

            [term(term_args)..] => {

                Ok(term_args.collect())

            }

        )

    }

    /// Parse an identifier

    fn identifier(id: ParseNode) -> ParseResult<String> {

        Ok(id.as_str().to_string())

    }

    /// Ignored rules

    fn EOI(_eof: ParseNode) -> ParseResult<()> {

        Ok(())

    }

    fn sorts(_sorts: ParseNode) -> ParseResult<()> {

        Ok(())

    }

    fn opns(_opns: ParseNode) -> ParseResult<()> {

        Ok(())

    }

}

#[cfg(test)]

mod tests {

    use super::*;

    #[test]

    #[test]

    #[test]

    #[test]

        );

    #[test]

}