use std::iter;

use itertools::Itertools;

use pest::error::ErrorVariant;

use merc_pest_consume::Error;

use merc_pest_consume::match_nodes;

use crate::ActDecl;

use crate::ActFrm;

use crate::Action;

use crate::ActionRHS;

use crate::ActionRenameDecl;

use crate::ActionRenameRule;

use crate::Assignment;

use crate::BagElement;

use crate::CommExpr;

use crate::ComplexSort;

use crate::Condition;

use crate::ConstructorDecl;

use crate::DataExpr;

use crate::DataExprUnaryOp;

use crate::DataExprUpdate;

use crate::Eq;

use crate::EqnDecl;

use crate::EqnSpec;

use crate::FixedPointOperator;

use crate::IdDecl;

use crate::Mcrl2Parser;

use crate::MultiAction;

use crate::MultiActionLabel;

use crate::PbesEquation;

use crate::PbesExpr;

use crate::PresEquation;

use crate::PresExpr;

use crate::ProcDecl;

use crate::ProcessExpr;

use crate::PropVarDecl;

use crate::PropVarInst;

use crate::RegFrm;

use crate::Rename;

use crate::Rule;

use crate::SortDecl;

use crate::SortExpression;

use crate::StateFrm;

use crate::StateVarAssignment;

use crate::StateVarDecl;

use crate::UntypedActionRenameSpec;

use crate::UntypedDataSpecification;

use crate::UntypedPbes;

use crate::UntypedPres;

use crate::UntypedProcessSpecification;

use crate::UntypedStateFrmSpec;

use crate::parse_actfrm;

use crate::parse_dataexpr;

use crate::parse_pbesexpr;

use crate::parse_presexpr;

use crate::parse_process_expr;

use crate::parse_regfrm;

use crate::parse_sortexpr;

use crate::parse_sortexpr_primary;

use crate::parse_statefrm;

/// Type alias for Errors resulting parsing.

pub(crate) type ParseResult<T> = std::result::Result<T, Error<Rule>>;

pub(crate) type ParseNode<'i> = merc_pest_consume::Node<'i, Rule, ()>;

/// These functions are used to consume the parse tree generated by the `pest` parser into a syntax tree.

///

/// Functions that are private are only used by other functions within the module, especially within the `matches_nodes!` macro.

/// See `pest_consume` documentation for more details on how to use this macro. The main idea is to apply the consume functions to the children of a parse node whenver they matce the arm.

///

/// Functions that are `pub(crate)` are used by the pratt parser to consume the parse tree and build the syntax tree with priorities

/// and associativity. They are defined in `precedence.rs`.

#[merc_pest_consume::parser]

impl Mcrl2Parser {

    // Although these are not public, they are the main entry points for consuming the parse tree.

    pub(crate) fn MCRL2Spec(spec: ParseNode) -> ParseResult<UntypedProcessSpecification> {

        let mut action_declarations = Vec::new();

        let mut map_declarations = Vec::new();

        let mut constructor_declarations = Vec::new();

        let mut equation_declarations = Vec::new();

        let mut global_variables = Vec::new();

        let mut process_declarations = Vec::new();

        let mut sort_declarations = Vec::new();

        let mut init = None;

        for child in spec.into_children() {

            match child.as_rule() {

                Rule::ActSpec => {

                    action_declarations.extend(Mcrl2Parser::ActSpec(child)?);

                }

                Rule::ConsSpec => {

                    constructor_declarations.append(&mut Mcrl2Parser::ConsSpec(child)?);

                }

                Rule::MapSpec => {

                    map_declarations.append(&mut Mcrl2Parser::MapSpec(child)?);

                }

                Rule::GlobVarSpec => {

                    global_variables.append(&mut Mcrl2Parser::GlobVarSpec(child)?);

                }

                Rule::EqnSpec => {

                    equation_declarations.append(&mut Mcrl2Parser::EqnSpec(child)?);

                }

                Rule::ProcSpec => {

                    process_declarations.append(&mut Mcrl2Parser::ProcSpec(child)?);

                }

                Rule::SortSpec => {

                    sort_declarations.append(&mut Mcrl2Parser::SortSpec(child)?);

                }

                Rule::Init => {

                    if init.is_some() {

                        return Err(Error::new_from_span(

                            ErrorVariant::CustomError {

                                message: "Multiple init expressions are not allowed".to_string(),

                            },

                            child.as_span(),

                        ));

                    }

                    init = Some(Mcrl2Parser::Init(child)?);

                }

                Rule::EOI => {

                    // End of input

                    break;

                }

                _ => {

                    unimplemented!("Unexpected rule: {:?}", child.as_rule());

                }

            }

        }

        let data_specification = UntypedDataSpecification {

            map_declarations,

            constructor_declarations,

            equation_declarations,

            sort_declarations,

        };

        Ok(UntypedProcessSpecification {

            data_specification,

            global_variables,

            action_declarations,

            process_declarations,

            init,

        })

    }

    pub fn PbesSpec(spec: ParseNode) -> ParseResult<UntypedPbes> {

        let mut data_specification = None;

        let mut global_variables = None;

        let mut equations = None;

        let mut init = None;

        for child in spec.into_children() {

            match child.as_rule() {

                Rule::DataSpec => {

                    data_specification = Some(Mcrl2Parser::DataSpec(child)?);

                }

                Rule::GlobVarSpec => {

                    global_variables = Some(Mcrl2Parser::GlobVarSpec(child)?);

                }

                Rule::PbesEqnSpec => {

                    equations = Some(Mcrl2Parser::PbesEqnSpec(child)?);

                }

                Rule::PbesInit => {

                    init = Some(Mcrl2Parser::PbesInit(child)?);

                }

                Rule::EOI => {

                    // End of input

                    break;

                }

                _ => {

                    unimplemented!("Unexpected rule: {:?}", child.as_rule());

                }

            }

        }

        Ok(UntypedPbes {

            data_specification: data_specification.unwrap_or_default(),

            global_variables: global_variables.unwrap_or_default(),

            equations: equations.unwrap(),

            init: init.unwrap(),

        })

    }

    fn PbesInit(init: ParseNode) -> ParseResult<PropVarInst> {

        match_nodes!(init.into_children();

            [PropVarInst(inst)] => {

                Ok(inst)

            }

        )

    }

    fn PbesEqnSpec(spec: ParseNode) -> ParseResult<Vec<PbesEquation>> {

        match_nodes!(spec.into_children();

            [PbesEqnDecl(equations)..] => {

                Ok(equations.collect())

            },

        )

    }

    fn PbesEqnDecl(decl: ParseNode) -> ParseResult<PbesEquation> {

        let span = decl.as_span();

        match_nodes!(decl.into_children();

            [FixedPointOperator(operator), PropVarDecl(variable), PbesExpr(formula)] => {

                Ok(PbesEquation {

                    operator,

                    variable,

                    formula,

                    span: span.into(),

                })

            },

        )

    }

    fn FixedPointOperator(op: ParseNode) -> ParseResult<FixedPointOperator> {

        match op.into_children().next().unwrap().as_rule() {

            Rule::FixedPointMu => Ok(FixedPointOperator::Least),

            Rule::FixedPointNu => Ok(FixedPointOperator::Greatest),

            x => unimplemented!("This is not a fixed point operator: {:?}", x),

        }

    }

    fn PropVarDecl(decl: ParseNode) -> ParseResult<PropVarDecl> {

        let span = decl.as_span();

        match_nodes!(decl.into_children();

            [Id(identifier), VarsDeclList(params)] => {

                Ok(PropVarDecl {

                    identifier,

                    parameters: params,

                    span: span.into(),

                })

            },

            [Id(identifier)] => {

                Ok(PropVarDecl {

                    identifier,

                    parameters: Vec::new(),

                    span: span.into(),

                })

            }

        )

    }

    pub(crate) fn PropVarInst(inst: ParseNode) -> ParseResult<PropVarInst> {

        match_nodes!(inst.into_children();

            [Id(identifier)] => {

                Ok(PropVarInst {

                    identifier,

                    arguments: Vec::new(),

                })

            },

            [Id(identifier), DataExprList(arguments)] => {

                Ok(PropVarInst {

                    identifier,

                    arguments,

                })

            }

        )

    }

    fn PbesExpr(expr: ParseNode) -> ParseResult<PbesExpr> {

        parse_pbesexpr(expr.children().as_pairs().clone())

    }

    pub fn PresSpec(spec: ParseNode) -> ParseResult<UntypedPres> {

        let mut data_specification = None;

        let mut global_variables = None;

        let mut equations = None;

        let mut init = None;

        for child in spec.into_children() {

            match child.as_rule() {

                Rule::DataSpec => {

                    data_specification = Some(Mcrl2Parser::DataSpec(child)?);

                }

                Rule::GlobVarSpec => {

                    global_variables = Some(Mcrl2Parser::GlobVarSpec(child)?);

                }

                Rule::PresEqnSpec => {

                    equations = Some(Mcrl2Parser::PresEqnSpec(child)?);

                }

                Rule::PbesInit => {

                    init = Some(Mcrl2Parser::PbesInit(child)?);

                }

                Rule::EOI => {

                    // End of input

                    break;

                }

                _ => {

                    unimplemented!("Unexpected rule: {:?}", child.as_rule());

                }

            }

        }

        Ok(UntypedPres {

            data_specification: data_specification.unwrap_or_default(),

            global_variables: global_variables.unwrap_or_default(),

            equations: equations.unwrap(),

            init: init.unwrap(),

        })

    }

    fn PresEqnSpec(spec: ParseNode) -> ParseResult<Vec<PresEquation>> {

        match_nodes!(spec.into_children();

            [PresEqnDecl(equations)..] => {

                Ok(equations.collect())

            },

        )

    }

    fn PresEqnDecl(decl: ParseNode) -> ParseResult<PresEquation> {

        let span = decl.as_span();

        match_nodes!(decl.into_children();

            [FixedPointOperator(operator), PropVarDecl(variable), PresExpr(formula)] => {

                Ok(PresEquation {

                    operator,

                    variable,

                    formula,

                    span: span.into(),

                })

            },

        )

    }

    fn PresExpr(expr: ParseNode) -> ParseResult<PresExpr> {

        parse_presexpr(expr.children().as_pairs().clone())

    }

    fn ActSpec(spec: ParseNode) -> ParseResult<Vec<ActDecl>> {

        match_nodes!(spec.into_children();

            [ActDecl(decls)..] => {

                Ok(decls.flatten().collect())

            },

        )

    }

    fn ActDecl(decl: ParseNode) -> ParseResult<Vec<ActDecl>> {

        let span = decl.as_span();

        match_nodes!(decl.into_children();

            [IdList(identifiers)] => {

            },

            [IdList(identifiers), SortProduct(args)] => {

            },

        )

    }

    fn SortProduct(sort: ParseNode) -> ParseResult<Vec<SortExpression>> {

        let mut iter = sort.into_children();

        // An expression of the shape SortExprPrimary ~ (SortExprProduct ~ SortExprPrimary)*

        let mut result = vec![parse_sortexpr_primary(iter.next().unwrap().as_pair().clone())?];

        for mut chunk in &iter.chunks(2) {

            if chunk.next().unwrap().as_rule() == Rule::SortExprProduct {

                let sort = parse_sortexpr_primary(chunk.next().unwrap().as_pair().clone())?;

                result.push(sort);

            }

        }

        Ok(result)

    }

    fn GlobVarSpec(spec: ParseNode) -> ParseResult<Vec<IdDecl>> {

        match_nodes!(spec.into_children();

            [VarsDeclList(vars)] => {

                Ok(vars)

            }

        )

    }

    fn SortExprPrimary(sort: ParseNode) -> ParseResult<SortExpression> {

        parse_sortexpr(sort.children().as_pairs().clone())

    }

    pub(crate) fn DataSpec(spec: ParseNode) -> ParseResult<UntypedDataSpecification> {

        let mut map_declarations = Vec::new();

        let mut equation_declarations = Vec::new();

        let mut constructor_declarations = Vec::new();

        let mut sort_declarations = Vec::new();

        for child in spec.into_children() {

            match child.as_rule() {

                Rule::ConsSpec => {

                    constructor_declarations.append(&mut Mcrl2Parser::ConsSpec(child)?);

                }

                Rule::MapSpec => {

                    map_declarations.append(&mut Mcrl2Parser::MapSpec(child)?);

                }

                Rule::EqnSpec => {

                    equation_declarations.append(&mut Mcrl2Parser::EqnSpec(child)?);

                }

                Rule::SortSpec => {

                    sort_declarations.append(&mut Mcrl2Parser::SortSpec(child)?);

                }

                Rule::EOI => {

                    // End of input

                    break;

                }

                _ => {

                    unimplemented!("Unexpected rule: {:?}", child.as_rule());

                }

            }

        }

        Ok(UntypedDataSpecification {

            map_declarations,

            equation_declarations,

            constructor_declarations,

            sort_declarations,

        })

    }

    pub fn ActionRenameSpec(spec: ParseNode) -> ParseResult<UntypedActionRenameSpec> {

        let mut map_declarations = Vec::new();

        let mut equation_declarations = Vec::new();

        let mut constructor_declarations = Vec::new();

        let mut sort_declarations = Vec::new();

        let mut action_declarations = Vec::new();

        let mut rename_declarations = Vec::new();

        for child in spec.into_children() {

            match child.as_rule() {

                Rule::ConsSpec => {

                    constructor_declarations.append(&mut Mcrl2Parser::ConsSpec(child)?);

                }

                Rule::MapSpec => {

                    map_declarations.append(&mut Mcrl2Parser::MapSpec(child)?);

                }

                Rule::EqnSpec => {

                    equation_declarations.append(&mut Mcrl2Parser::EqnSpec(child)?);

                }

                Rule::SortSpec => {

                    sort_declarations.append(&mut Mcrl2Parser::SortSpec(child)?);

                }

                Rule::ActSpec => {

                    action_declarations.append(&mut Mcrl2Parser::ActSpec(child)?);

                }

                Rule::ActionRenameRuleSpec => {

                    rename_declarations.append(&mut Mcrl2Parser::ActionRenameRuleSpec(child)?)

                }

                Rule::EOI => {

                    // End of input

                    break;

                }

                _ => {

                    unimplemented!("Unexpected rule: {:?}", child.as_rule());

                }

            }

        }

        let data_specification = UntypedDataSpecification {

            map_declarations,

            equation_declarations,

            constructor_declarations,

            sort_declarations,

        };

        Ok(UntypedActionRenameSpec {

            data_specification,

            action_declarations,

            rename_declarations,

        })

    }

    pub(crate) fn StateFrmId(id: ParseNode) -> ParseResult<StateFrm> {

        match_nodes!(id.into_children();

            [Id(identifier)] => {

                Ok(StateFrm::Id(identifier, Vec::new()))

            },

            [Id(identifier), DataExprList(expressions)] => {

                Ok(StateFrm::Id(identifier, expressions))

            },

        )

    }

    fn MapSpec(spec: ParseNode) -> ParseResult<Vec<IdDecl>> {

        match_nodes!(spec.into_children();

            [IdsDecl(decls)..] => {

                Ok(decls.flatten().collect())

            }

        )

    }

    fn SortSpec(spec: ParseNode) -> ParseResult<Vec<SortDecl>> {

        match_nodes!(spec.into_children();

            [SortDecl(decls)..] => {

                Ok(decls.flatten().collect())

            }

        )

    }

    fn SortDecl(decl: ParseNode) -> ParseResult<Vec<SortDecl>> {

        let span = decl.as_span();

        match_nodes!(decl.into_children();

            [IdAt(identifier), SortExpr(expr)] => {

                Ok(vec![SortDecl::new(identifier, Some(expr), span.into())])

            },

            [IdList(ids)] => {

            },

            [IdsDecl(decl)] => {

            }

        )

    }

    fn ConsSpec(spec: ParseNode) -> ParseResult<Vec<IdDecl>> {

        match_nodes!(spec.into_children();

            [IdsDecl(decls)..] => {

                Ok(decls.flatten().collect())

            }

        )

    }

    fn Init(init: ParseNode) -> ParseResult<ProcessExpr> {

        match_nodes!(init.into_children();

            [ProcExpr(expr)] => {

                Ok(expr)

            }

        )

    }

    fn ProcSpec(spec: ParseNode) -> ParseResult<Vec<ProcDecl>> {

        match_nodes!(spec.into_children();

            [ProcDecl(decls)..] => {

                Ok(decls.collect())

            },

        )

    }

    fn ProcDecl(decl: ParseNode) -> ParseResult<ProcDecl> {

        let span = decl.as_span();

        match_nodes!(decl.into_children();

            [Id(identifier), VarsDeclList(params), ProcExpr(body)] => {

                Ok(ProcDecl {

                    identifier,

                    params,

                    body,

                    span: span.into(),

                })

            },

            [Id(identifier), ProcExpr(body)] => {

                Ok(ProcDecl {

                    identifier,

                    params: Vec::new(),

                    body,

                    span: span.into(),

                })

            }

        )

    }

    pub(crate) fn ProcExprAt(input: ParseNode) -> ParseResult<DataExpr> {

        match_nodes!(input.into_children();

            [DataExprUnit(expr)] => {

                Ok(expr)

            },

        )

    }

    pub(crate) fn StateFrmExists(input: ParseNode) -> ParseResult<Vec<IdDecl>> {

        match_nodes!(input.into_children();

            [VarsDeclList(variables)] => {

                Ok(variables)

            },

        )

    }

    pub(crate) fn StateFrmForall(input: ParseNode) -> ParseResult<Vec<IdDecl>> {

        match_nodes!(input.into_children();

            [VarsDeclList(variables)] => {

                Ok(variables)

            },

        )

    }

    pub(crate) fn StateFrmMu(input: ParseNode) -> ParseResult<StateVarDecl> {

        match_nodes!(input.into_children();

            [StateVarDecl(variable)] => {

                Ok(variable)

            },

        )

    }

    pub(crate) fn StateFrmNu(input: ParseNode) -> ParseResult<StateVarDecl> {

        match_nodes!(input.into_children();

            [StateVarDecl(variable)] => {

                Ok(variable)

            },

        )

    }

    pub(crate) fn ActFrmExists(input: ParseNode) -> ParseResult<Vec<IdDecl>> {

        match_nodes!(input.into_children();

            [VarsDeclList(variables)] => {

                Ok(variables)

            },

        )

    }

    pub(crate) fn ActFrmForall(input: ParseNode) -> ParseResult<Vec<IdDecl>> {

        match_nodes!(input.into_children();

            [VarsDeclList(variables)] => {

                Ok(variables)

            },

        )

    }

    pub(crate) fn DataExpr(expr: ParseNode) -> ParseResult<DataExpr> {

        parse_dataexpr(expr.children().as_pairs().clone())

    }

    pub(crate) fn DataExprUnit(expr: ParseNode) -> ParseResult<DataExpr> {

        parse_dataexpr(expr.children().as_pairs().clone())

    }

    pub(crate) fn DataValExpr(expr: ParseNode) -> ParseResult<DataExpr> {

        match_nodes!(expr.into_children();

            [DataExpr(expr)] => {

                Ok(expr)

            },

        )

    }

    pub(crate) fn DataExprUpdate(expr: ParseNode) -> ParseResult<DataExprUpdate> {

        match_nodes!(expr.into_children();

            [DataExpr(expr), DataExpr(update)] => {

                Ok(DataExprUpdate { expr, update })

            },

        )

    }

    pub(crate) fn DataExprApplication(expr: ParseNode) -> ParseResult<Vec<DataExpr>> {

        match_nodes!(expr.into_children();

            [DataExprList(expressions)] => {

                Ok(expressions)

            },

        )

    }

    pub(crate) fn DataExprWhr(expr: ParseNode) -> ParseResult<Vec<Assignment>> {

        match_nodes!(expr.into_children();

            [AssignmentList(assignments)] => {

                Ok(assignments)

            },

        )

    }

    pub(crate) fn AssignmentList(assignments: ParseNode) -> ParseResult<Vec<Assignment>> {

        match_nodes!(assignments.into_children();

            [Assignment(assignment)] => {

                Ok(vec![assignment])

            },

            [Assignment(assignment)..] => {

                Ok(assignment.collect())

            },

        )

    }

    pub(crate) fn Assignment(assignment: ParseNode) -> ParseResult<Assignment> {

        match_nodes!(assignment.into_children();

            [IdAt(identifier), DataExpr(expr)] => {

                Ok(Assignment { identifier, expr })

            },

        )

    }

    pub(crate) fn DataExprSize(expr: ParseNode) -> ParseResult<DataExpr> {

        match_nodes!(expr.into_children();

            [DataExpr(expr)] => {

                Ok(DataExpr::Unary { op: DataExprUnaryOp::Size, expr: Box::new(expr) })

            },

        )

    }

    fn DataExprList(expr: ParseNode) -> ParseResult<Vec<DataExpr>> {

        match_nodes!(expr.into_children();

            [DataExpr(expr)] => {

                Ok(vec![expr])

            },

            [DataExpr(expr)..] => {

                Ok(expr.collect())

            },

        )

    }

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

        match_nodes!(vars.into_children();

            [VarsDeclList(ids)..] => {

                Ok(ids.flatten().collect())

            },

        )

    }

    pub(crate) fn VarsDeclList(vars: ParseNode) -> ParseResult<Vec<IdDecl>> {

        match_nodes!(vars.into_children();

            [VarsDecl(decl)..] => {

                Ok(decl.flatten().collect())

            },

        )

    }

    fn VarsDecl(decl: ParseNode) -> ParseResult<Vec<IdDecl>> {

        let mut vars = Vec::new();

        let span = decl.as_span();

        match_nodes!(decl.into_children();

            [IdList(identifier), SortExpr(sort)] => {

                for id in identifier {

                    vars.push(IdDecl::new(id, sort.clone(), span.into()));

                }

            },

        );

        Ok(vars)

    }

    pub(crate) fn SortExpr(expr: ParseNode) -> ParseResult<SortExpression> {

        parse_sortexpr(expr.children().as_pairs().clone())

    }

    pub(crate) fn Id(identifier: ParseNode) -> ParseResult<String> {

        Ok(identifier.as_str().to_string())

    }

    pub(crate) fn IdAt(identifier: ParseNode) -> ParseResult<String> {

        Ok(identifier.as_str().to_string())

    }

    pub(crate) fn IdList(identifiers: ParseNode) -> ParseResult<Vec<String>> {

        match_nodes!(identifiers.into_children();

            [IdAt(ids)..] => {

                Ok(ids.collect())

            },

        )

    }

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

        Ok(identifier.as_str().to_string())

    }

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

        match_nodes!(identifiers.into_children();

            [IdInfix(ids)..] => {

                Ok(ids.collect())

            },

        )

    }

    // Complex sorts

    pub(crate) fn SortExprList(inner: ParseNode) -> ParseResult<SortExpression> {

        Ok(SortExpression::Complex(

            ComplexSort::List,

            Box::new(parse_sortexpr(inner.children().as_pairs().clone())?),

        ))

    }

    pub(crate) fn SortExprSet(inner: ParseNode) -> ParseResult<SortExpression> {

        Ok(SortExpression::Complex(

            ComplexSort::Set,

            Box::new(parse_sortexpr(inner.children().as_pairs().clone())?),

        ))

    }

    pub(crate) fn SortExprBag(inner: ParseNode) -> ParseResult<SortExpression> {

        Ok(SortExpression::Complex(

            ComplexSort::Bag,

            Box::new(parse_sortexpr(inner.children().as_pairs().clone())?),

        ))

    }

    pub(crate) fn SortExprFSet(inner: ParseNode) -> ParseResult<SortExpression> {

        Ok(SortExpression::Complex(

            ComplexSort::FSet,

            Box::new(parse_sortexpr(inner.children().as_pairs().clone())?),

        ))

    }

    pub(crate) fn SortExprFBag(inner: ParseNode) -> ParseResult<SortExpression> {

        Ok(SortExpression::Complex(

            ComplexSort::FBag,

            Box::new(parse_sortexpr(inner.children().as_pairs().clone())?),

        ))

    }

    pub(crate) fn SortExprStruct(inner: ParseNode) -> ParseResult<SortExpression> {

        match_nodes!(inner.into_children();

            [ConstrDeclList(inner)] => {

                Ok(SortExpression::Struct { inner })

            },

        )

    }

    pub(crate) fn ConstrDeclList(input: ParseNode) -> ParseResult<Vec<ConstructorDecl>> {

        match_nodes!(input.into_children();

            [ConstrDecl(decl)..] => {

                Ok(decl.collect())

            },

        )

    }

    pub(crate) fn ProjDeclList(input: ParseNode) -> ParseResult<Vec<(Option<String>, SortExpression)>> {

        match_nodes!(input.into_children();

            [ProjDecl(decl)..] => {

                Ok(decl.collect())

            },

        )

    }

    pub(crate) fn ConstrDecl(input: ParseNode) -> ParseResult<ConstructorDecl> {

        match_nodes!(input.into_children();

            [IdAt(name)] => {

                Ok(ConstructorDecl { name, args: Vec::new(), projection: None })

            },

            [IdAt(name), IdAt(projection)] => {

                Ok(ConstructorDecl { name, args: Vec::new(), projection: Some(projection)  })

            },

            [IdAt(name), ProjDeclList(args)] => {

                Ok(ConstructorDecl { name, args, projection: None })

            },

            [IdAt(name), ProjDeclList(args), IdAt(projection)] => {

                Ok(ConstructorDecl { name, args, projection: Some(projection) })

            },

        )

    }

    pub(crate) fn ProjDecl(input: ParseNode) -> ParseResult<(Option<String>, SortExpression)> {

        match_nodes!(input.into_children();

            [SortExpr(sort)] => {

                Ok((None, sort))

            },

            [Id(name), SortExpr(sort)] => {

                Ok((Some(name), sort))

            },

        )

    }

    pub(crate) fn DataExprListEnum(input: ParseNode) -> ParseResult<DataExpr> {

        match_nodes!(input.into_children();

            [DataExprList(expressions)] => {

                Ok(DataExpr::List(expressions))

            },

        )

    }

    pub(crate) fn DataExprBagEnum(input: ParseNode) -> ParseResult<DataExpr> {

        match_nodes!(input.into_children();

            [BagEnumEltList(elements)] => {

                Ok(DataExpr::Bag(elements))

            },

        )

    }

    fn BagEnumEltList(input: ParseNode) -> ParseResult<Vec<BagElement>> {

        match_nodes!(input.into_children();

            [BagEnumElt(elements)..] => {

                Ok(elements.collect())

            },

        )

    }

    fn BagEnumElt(input: ParseNode) -> ParseResult<BagElement> {

        match_nodes!(input.into_children();

            [DataExpr(expr), DataExpr(multiplicity)] => {

                Ok(BagElement { expr, multiplicity })

            },

        )

    }

    pub(crate) fn DataExprSetEnum(input: ParseNode) -> ParseResult<DataExpr> {

        match_nodes!(input.into_children();

            [DataExprList(expressions)] => {

                Ok(DataExpr::Set(expressions))

            },

        )

    }

    pub(crate) fn DataExprSetBagComp(input: ParseNode) -> ParseResult<DataExpr> {

        match_nodes!(input.into_children();

            [VarDecl(variable), DataExpr(predicate)] => {

                Ok(DataExpr::SetBagComp { variable, predicate: Box::new(predicate) })

            },

        )

    }

    pub(crate) fn Number(input: ParseNode) -> ParseResult<DataExpr> {

        Ok(DataExpr::Number(input.as_str().into()))

    }

    fn VarDecl(decl: ParseNode) -> ParseResult<IdDecl> {

        let span = decl.as_span();

        match_nodes!(decl.into_children();

            [IdAt(identifier), SortExpr(sort)] => {

                Ok(IdDecl::new(identifier, sort, span.into()))

            },

        )

    }

    pub(crate) fn DataExprLambda(input: ParseNode) -> ParseResult<Vec<IdDecl>> {

        match_nodes!(input.into_children();

            [VarsDeclList(vars)] => {

                Ok(vars)

            },

        )

    }

    pub(crate) fn DataExprForall(input: ParseNode) -> ParseResult<Vec<IdDecl>> {

        match_nodes!(input.into_children();

            [VarsDeclList(vars)] => {

                Ok(vars)

            },

        )

    }

    pub(crate) fn DataExprExists(input: ParseNode) -> ParseResult<Vec<IdDecl>> {

        match_nodes!(input.into_children();

            [VarsDeclList(vars)] => {

                Ok(vars)

            },

        )

    }

    pub(crate) fn ActFrm(input: ParseNode) -> ParseResult<ActFrm> {

        parse_actfrm(input.children().as_pairs().clone())

    }

    pub(crate) fn ActIdSet(actions: ParseNode) -> ParseResult<Vec<String>> {

        match_nodes!(actions.into_children();

            [IdList(list)] => {

                Ok(list)

            },

        )

    }

    fn MultActId(actions: ParseNode) -> ParseResult<MultiActionLabel> {

        match_nodes!(actions.into_children();

            [Id(action), Id(actions)..] => {

                Ok(MultiActionLabel { actions: iter::once(action).chain(actions).collect() })

            },

        )

    }

    fn MultActIdList(actions: ParseNode) -> ParseResult<Vec<MultiActionLabel>> {

        match_nodes!(actions.into_children();

            [MultActId(action), MultActId(actions)..] => {

                Ok(iter::once(action).chain(actions).collect())

            },

        )

    }

    pub(crate) fn MultActIdSet(actions: ParseNode) -> ParseResult<Vec<MultiActionLabel>> {

        match_nodes!(actions.into_children();

            [MultActIdList(list)] => {

                Ok(list)

            },

        )

    }

    fn ProcExpr(input: ParseNode) -> ParseResult<ProcessExpr> {

        parse_process_expr(input.children().as_pairs().clone())

    }

    fn ProcExprNoIf(input: ParseNode) -> ParseResult<ProcessExpr> {

        parse_process_expr(input.children().as_pairs().clone())

    }

    pub(crate) fn ProcExprId(input: ParseNode) -> ParseResult<ProcessExpr> {

        match_nodes!(input.into_children();

            [Id(identifier)] => {

                Ok(ProcessExpr::Id(identifier, Vec::new()))

            },

            [Id(identifier), AssignmentList(assignments)] => {

                Ok(ProcessExpr::Id(identifier, assignments))

            },

        )

    }

    pub(crate) fn ProcExprBlock(input: ParseNode) -> ParseResult<ProcessExpr> {

        match_nodes!(input.into_children();

            [ActIdSet(actions), ProcExpr(expr)] => {

                Ok(ProcessExpr::Block {

                    actions,

                    operand: Box::new(expr),

                })

            },

        )

    }

    pub(crate) fn ProcExprIf(input: ParseNode) -> ParseResult<DataExpr> {

        match_nodes!(input.into_children();

            [DataExpr(condition)] => {

                Ok(condition)

            },

        )

    }

    pub(crate) fn ProcExprIfThen(input: ParseNode) -> ParseResult<(DataExpr, ProcessExpr)> {

        match_nodes!(input.into_children();

            [DataExpr(condition), ProcExprNoIf(expr)] => {

                Ok((condition, expr))

            },

        )

    }

    pub(crate) fn ProcExprAllow(input: ParseNode) -> ParseResult<ProcessExpr> {

        match_nodes!(input.into_children();

            [MultActIdSet(actions), ProcExpr(expr)] => {

                Ok(ProcessExpr::Allow {

                    actions,

                    operand: Box::new(expr),

                })

            },

        )

    }

    pub(crate) fn ProcExprHide(input: ParseNode) -> ParseResult<ProcessExpr> {

        match_nodes!(input.into_children();

            [ActIdSet(actions), ProcExpr(expr)] => {

                Ok(ProcessExpr::Hide {

                    actions,

                    operand: Box::new(expr),

                })

            },

        )

    }

    fn ActionList(actions: ParseNode) -> ParseResult<Vec<Action>> {

        match_nodes!(actions.into_children();

            [Action(action), Action(actions)..] => {

                Ok(iter::once(action).chain(actions).collect())

            },

        )

    }

    fn MultiActTau(_input: ParseNode) -> ParseResult<()> {

        Ok(())

    }

    fn ProcExprDelta(_input: ParseNode) -> ParseResult<()> {

        Ok(())

    }

    pub(crate) fn MultAct(input: ParseNode) -> ParseResult<MultiAction> {

        match_nodes!(input.into_children();

            [MultiActTau(_)] => {

                Ok(MultiAction { actions: Vec::new() })

            },

            [ActionList(actions)] => {

                Ok(MultiAction { actions })

            },

        )

    }

    fn CommExpr(action: ParseNode) -> ParseResult<CommExpr> {

        match_nodes!(action.into_children();

            [Id(id), MultActId(multiact), Id(to)] => {

                let mut actions = vec![id];

                actions.extend(multiact.actions);

                Ok(CommExpr {

                    from: MultiActionLabel { actions },

                    to

                })

            },

        )

    }

    fn CommExprList(actions: ParseNode) -> ParseResult<Vec<CommExpr>> {

        match_nodes!(actions.into_children();

            [CommExpr(action), CommExpr(actions)..] => {

                Ok(iter::once(action).chain(actions).collect())

            },

        )

    }

    pub(crate) fn CommExprSet(actions: ParseNode) -> ParseResult<Vec<CommExpr>> {

        match_nodes!(actions.into_children();

            [CommExprList(list)] => {

                Ok(list)

            },

        )

    }

    pub(crate) fn ProcExprRename(input: ParseNode) -> ParseResult<ProcessExpr> {

        match_nodes!(input.into_children();

            [RenExprSet(renames), ProcExpr(expr)] => {

                Ok(ProcessExpr::Rename {

                    renames,

                    operand: Box::new(expr),

                })

            },

        )

    }

    pub(crate) fn ProcExprComm(input: ParseNode) -> ParseResult<ProcessExpr> {

        match_nodes!(input.into_children();

            [CommExprSet(comm), ProcExpr(expr)] => {

                Ok(ProcessExpr::Comm {

                    comm,

                    operand: Box::new(expr),

                })

            },

        )

    }

    pub(crate) fn Action(input: ParseNode) -> ParseResult<Action> {

        match_nodes!(input.into_children();

            [Id(id), DataExprList(args)] => {

                Ok(Action { id, args })

            },

            [Id(id)] => {

                Ok(Action { id, args: Vec::new() })

            },

        )

    }

    fn RenExprSet(renames: ParseNode) -> ParseResult<Vec<Rename>> {

        match_nodes!(renames.into_children();

            [RenExprList(renames)] => {

                Ok(renames)

            },

        )

    }

    fn RenExprList(renames: ParseNode) -> ParseResult<Vec<Rename>> {

        match_nodes!(renames.into_children();

            [RenExpr(renames)..] => {

                Ok(renames.collect())

            },

        )

    }

    fn RenExpr(renames: ParseNode) -> ParseResult<Rename> {

        match_nodes!(renames.into_children();

            [Id(from), Id(to)] => {

                Ok(Rename { from, to })

            },

        )

    }

    pub(crate) fn ProcExprSum(input: ParseNode) -> ParseResult<Vec<IdDecl>> {

        match_nodes!(input.into_children();

            [VarsDeclList(variables)] => {

                Ok(variables)

            },

        )

    }

    pub(crate) fn ProcExprDist(input: ParseNode) -> ParseResult<(Vec<IdDecl>, DataExpr)> {

        match_nodes!(input.into_children();

            [VarsDeclList(variables), DataExpr(expr)] => {

                Ok((variables, expr))

            },

        )

    }

    pub(crate) fn StateFrmDelay(input: ParseNode) -> ParseResult<StateFrm> {

        match_nodes!(input.into_children();

            [DataExpr(delay)] => {

                Ok(StateFrm::Delay(delay))

            },

        )

    }

    pub(crate) fn StateFrmYaled(input: ParseNode) -> ParseResult<StateFrm> {

        match_nodes!(input.into_children();

            [DataExpr(delay)] => {

                Ok(StateFrm::Yaled(delay))

            },

        )

    }

    pub(crate) fn StateFrmNegation(input: ParseNode) -> ParseResult<StateFrm> {

        match_nodes!(input.into_children();

            [StateFrm(state)] => {

                Ok(StateFrm::Unary { op: crate::StateFrmUnaryOp::Negation, expr: Box::new(state) })

            },

        )

    }

    pub(crate) fn StateFrmLeftConstantMultiply(input: ParseNode) -> ParseResult<DataExpr> {

        match_nodes!(input.into_children();

            [DataValExpr(expr)] => {

                Ok(expr)

            },

        )

    }

    pub(crate) fn StateFrmRightConstantMultiply(input: ParseNode) -> ParseResult<DataExpr> {

        match_nodes!(input.into_children();

            [DataValExpr(expr)] => {

                Ok(expr)

            },

        )

    }

    pub(crate) fn StateFrmDiamond(input: ParseNode) -> ParseResult<RegFrm> {

        match_nodes!(input.into_children();

            [RegFrm(formula)] => {

                Ok(formula)

            },

        )

    }

    pub(crate) fn StateFrmBox(input: ParseNode) -> ParseResult<RegFrm> {

        match_nodes!(input.into_children();

            [RegFrm(formula)] => {

                Ok(formula)

            },

        )

    }

    pub(crate) fn StateFrmSpec(spec: ParseNode) -> ParseResult<UntypedStateFrmSpec> {

        let mut map_declarations = Vec::new();

        let mut equation_declarations = Vec::new();

        let mut constructor_declarations = Vec::new();

        let mut sort_declarations = Vec::new();

        let mut action_declarations = Vec::new();

        let mut form_spec = None;

        let span = spec.as_span();

        for child in spec.into_children() {

            match child.as_rule() {

                Rule::StateFrmSpecElt => {

                    let element = child

                        .into_children()

                        .next()

                        .expect("StateFrmSpecElt has exactly one child");

                    match element.as_rule() {

                        Rule::ConsSpec => {

                            constructor_declarations.append(&mut Mcrl2Parser::ConsSpec(element)?);

                        }

                        Rule::MapSpec => {

                            map_declarations.append(&mut Mcrl2Parser::MapSpec(element)?);

                        }

                        Rule::EqnSpec => {

                            equation_declarations.append(&mut Mcrl2Parser::EqnSpec(element)?);

                        }

                        Rule::SortSpec => {

                            sort_declarations.append(&mut Mcrl2Parser::SortSpec(element)?);

                        }

                        Rule::ActSpec => {

                            action_declarations.append(&mut Mcrl2Parser::ActSpec(element)?);

                        }

                        _ => {

                            unimplemented!("Unexpected rule in StateFrmSpecElt: {:?}", element.as_rule());

                        }

                    }

                }

                Rule::StateFrm => {

                    if form_spec.is_some() {

                        return Err(Error::new_from_span(

                            ErrorVariant::CustomError {

                                message: "Multiple state formula specifications are not allowed".to_string(),

                            },

                            child.as_span(),

                        ));

                    }

                    form_spec = Some(Mcrl2Parser::StateFrm(child)?);

                }

                Rule::FormSpec => {

                    if form_spec.is_some() {

                        return Err(Error::new_from_span(

                            ErrorVariant::CustomError {

                                message: "Multiple state formula specifications are not allowed".to_string(),

                            },

                            child.as_span(),

                        ));

                    }

                    form_spec = Some(Mcrl2Parser::FormSpec(child)?);

                }

                Rule::EOI => {

                    // End of input

                    break;

                }

                _ => {

                    unimplemented!("Unexpected rule: {:?}", child.as_rule());

                }

            }

        }

        let data_specification = UntypedDataSpecification {

            map_declarations,

            equation_declarations,

            constructor_declarations,

            sort_declarations,

        };

        Ok(UntypedStateFrmSpec {

            data_specification,

            action_declarations,

            formula: form_spec.ok_or(Error::new_from_span(

                ErrorVariant::CustomError {

                    message: "No state formula found in the state formula specification".to_string(),

                },

                span,

            ))?,

        })

    }

    pub(crate) fn PbesExprForall(input: ParseNode) -> ParseResult<Vec<IdDecl>> {

        match_nodes!(input.into_children();

            [VarsDeclList(vars)] => {

                Ok(vars)

            },

        )

    }

    pub(crate) fn PbesExprExists(input: ParseNode) -> ParseResult<Vec<IdDecl>> {

        match_nodes!(input.into_children();

            [VarsDeclList(vars)] => {

                Ok(vars)

            },

        )

    }

    pub(crate) fn PresExprEqinf(input: ParseNode) -> ParseResult<PresExpr> {

        match_nodes!(input.into_children();

            [PresExpr(body)] => {

                Ok(PresExpr::Equal {

                    eq: Eq::EqInf,

                    body: Box::new(body),

                })

            },

        )

    }