merc_syntax 1.0.0

#![allow(clippy::result_large_err)]

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::ActionRenameDecl;
use crate::Assignment;
use crate::BagElement;
use crate::Comm;
use crate::ComplexSort;
use crate::ConstructorDecl;
use crate::DataExpr;
use crate::DataExprUnaryOp;
use crate::DataExprUpdate;
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::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::UntypedProcessSpecification;
use crate::UntypedStateFrmSpec;
use crate::VarDecl;
use crate::parse_actfrm;
use crate::parse_dataexpr;
use crate::parse_pbesexpr;
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())
    }

    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)] => {
                Ok(identifiers.iter().map(|name| ActDecl { identifier: name.clone(), args: Vec::new(), span: span.into() }).collect())
            },
            [IdList(identifiers), SortProduct(args)] => {
                Ok(identifiers.iter().map(|name| ActDecl { identifier: name.clone(), args: args.clone(), span: span.into() }).collect())
            },
        )
    }

    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<VarDecl>> {
        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.push(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();
            [Id(identifier), SortExpr(expr)] => {
                Ok(vec![SortDecl { identifier, expr: Some(expr), span: span.into() }])
            },
            [IdList(ids)] => {
                Ok(ids.iter().map(|identifier| SortDecl { identifier: identifier.clone(), expr: None, span: span.into() }).collect())
            },
            [IdsDecl(decl)] => {
                Ok(decl.iter().map(|element| SortDecl { identifier: element.identifier.clone(), expr: Some(element.sort.clone()), span: span.into() }).collect())
            }
        )
    }

    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<VarDecl>> {
        match_nodes!(input.into_children();
            [VarsDeclList(variables)] => {
                Ok(variables)
            },
        )
    }

    pub(crate) fn StateFrmForall(input: ParseNode) -> ParseResult<Vec<VarDecl>> {
        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<VarDecl>> {
        match_nodes!(input.into_children();
            [VarsDeclList(variables)] => {
                Ok(variables)
            },
        )
    }

    pub(crate) fn ActFrmForall(input: ParseNode) -> ParseResult<Vec<VarDecl>> {
        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();
            [Id(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<VarDecl>> {
        match_nodes!(vars.into_children();
            [VarsDeclList(ids)..] => {
                Ok(ids.flatten().collect())
            },
        )
    }

    pub(crate) fn VarsDeclList(vars: ParseNode) -> ParseResult<Vec<VarDecl>> {
        match_nodes!(vars.into_children();
            [VarsDecl(decl)..] => {
                Ok(decl.flatten().collect())
            },
        )
    }

    fn VarsDecl(decl: ParseNode) -> ParseResult<Vec<VarDecl>> {
        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(VarDecl { identifier: id, sort: sort.clone(), span: 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 IdList(identifiers: ParseNode) -> ParseResult<Vec<String>> {
        match_nodes!(identifiers.into_children();
            [Id(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();
            [Id(name)] => {
                Ok(ConstructorDecl { name, args: Vec::new(), projection: None })
            },
            [Id(name), Id(projection)] => {
                Ok(ConstructorDecl { name, args: Vec::new(), projection: Some(projection)  })
            },
            [Id(name), ProjDeclList(args)] => {
                Ok(ConstructorDecl { name, args, projection: None })
            },
            [Id(name), ProjDeclList(args), Id(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<VarDecl> {
        let span = decl.as_span();
        match_nodes!(decl.into_children();
            [Id(identifier), SortExpr(sort)] => {
                Ok(VarDecl { identifier, sort, span: span.into() })
            },
        )
    }

    pub(crate) fn DataExprLambda(input: ParseNode) -> ParseResult<Vec<VarDecl>> {
        match_nodes!(input.into_children();
            [VarsDeclList(vars)] => {
                Ok(vars)
            },
        )
    }

    pub(crate) fn DataExprForall(input: ParseNode) -> ParseResult<Vec<VarDecl>> {
        match_nodes!(input.into_children();
            [VarsDeclList(vars)] => {
                Ok(vars)
            },
        )
    }

    pub(crate) fn DataExprExists(input: ParseNode) -> ParseResult<Vec<VarDecl>> {
        match_nodes!(input.into_children();
            [VarsDeclList(vars)] => {
                Ok(vars)
            },
        )
    }

    pub(crate) fn ActFrm(input: ParseNode) -> ParseResult<ActFrm> {
        parse_actfrm(input.children().as_pairs().clone())
    }

    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())
            },
        )
    }

    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(())
    }

    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<Comm> {
        match_nodes!(action.into_children();
            [Id(id), MultActId(multiact), Id(to)] => {
                let mut actions = vec![id];
                actions.extend(multiact.actions);

                Ok(Comm {
                    from: MultiActionLabel { actions },
                    to
                })
            },
        )
    }

    fn CommExprList(actions: ParseNode) -> ParseResult<Vec<Comm>> {
        match_nodes!(actions.into_children();
            [CommExpr(action), CommExpr(actions)..] => {
                Ok(iter::once(action).chain(actions).collect())
            },
        )
    }

    fn CommExprSet(actions: ParseNode) -> ParseResult<Vec<Comm>> {
        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<VarDecl>> {
        match_nodes!(input.into_children();
            [VarsDeclList(variables)] => {
                Ok(variables)
            },
        )
    }

    pub(crate) fn ProcExprDist(input: ParseNode) -> ParseResult<(Vec<VarDecl>, 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<VarDecl>> {
        match_nodes!(input.into_children();
            [VarsDeclList(vars)] => {
                Ok(vars)
            },
        )
    }

    pub(crate) fn PbesExprExists(input: ParseNode) -> ParseResult<Vec<VarDecl>> {
        match_nodes!(input.into_children();
            [VarsDeclList(vars)] => {
                Ok(vars)
            },
        )
    }

    fn IdsDecl(decl: ParseNode) -> ParseResult<Vec<IdDecl>> {
        let span = decl.as_span();
        match_nodes!(decl.into_children();
            [IdList(identifiers), SortExpr(sort)] => {
                let id_decls = identifiers.into_iter().map(|identifier| {
                    IdDecl { identifier, sort: sort.clone(), span: span.into() }
                }).collect();

                Ok(id_decls)
            },
        )
    }

    fn EqnSpec(spec: ParseNode) -> ParseResult<Vec<EqnSpec>> {
        let mut ids = Vec::new();

        match_nodes!(spec.into_children();
            [VarSpec(variables), EqnDecl(decls)..] => {
                ids.push(EqnSpec { variables, equations: decls.collect() });
            },
            [EqnDecl(decls)..] => {
                ids.push(EqnSpec { variables: Vec::new(), equations: decls.collect() });
            },
        );

        Ok(ids)
    }

    fn EqnDecl(decl: ParseNode) -> ParseResult<EqnDecl> {
        let span = decl.as_span();
        match_nodes!(decl.into_children();
            [DataExpr(condition), DataExpr(lhs), DataExpr(rhs)] => {
                Ok(EqnDecl { condition: Some(condition), lhs, rhs, span: span.into() })
            },
            [DataExpr(lhs), DataExpr(rhs)] => {
                Ok(EqnDecl { condition: None, lhs, rhs, span: span.into() })
            },
        )
    }

    fn StateFrm(input: ParseNode) -> ParseResult<StateFrm> {
        parse_statefrm(input.children().as_pairs().clone())
    }

    fn RegFrm(input: ParseNode) -> ParseResult<RegFrm> {
        parse_regfrm(input.children().as_pairs().clone())
    }

    fn StateVarDecl(input: ParseNode) -> ParseResult<StateVarDecl> {
        let span = input.as_span();
        match_nodes!(input.into_children();
            [Id(identifier), StateVarAssignmentList(arguments)] => {
                Ok(StateVarDecl {
                    identifier,
                    arguments,
                    span: span.into(),
                })
            },
            [Id(identifier)] => {
                Ok(StateVarDecl {
                    identifier,
                    arguments: Vec::new(),
                    span: span.into(),
                })
            }
        )
    }

    fn StateVarAssignmentList(input: ParseNode) -> ParseResult<Vec<StateVarAssignment>> {
        match_nodes!(input.into_children();
            [StateVarAssignment(assignments)..] => {
                Ok(assignments.collect())
            }
        )
    }

    fn StateVarAssignment(input: ParseNode) -> ParseResult<StateVarAssignment> {
        match_nodes!(input.into_children();
            [Id(identifier), SortExpr(sort), DataExpr(expr)] => {
                Ok(StateVarAssignment {
                    identifier,
                    sort,
                    expr,
                })
            }
        )
    }

    fn ActionRenameRuleSpec(spec: ParseNode) -> ParseResult<ActionRenameDecl> {
        unimplemented!();
    }

    fn FormSpec(input: ParseNode) -> ParseResult<StateFrm> {
        match_nodes!(input.into_children();
            [StateFrm(formula)] => {
                Ok(formula)
            },
        )
    }

    pub(crate) fn StateFrmSup(input: ParseNode) -> ParseResult<Vec<VarDecl>> {
        match_nodes!(input.into_children();
            [VarsDeclList(variables)] => {
                Ok(variables)
            },
        )
    }

    pub(crate) fn StateFrmInf(input: ParseNode) -> ParseResult<Vec<VarDecl>> {
        match_nodes!(input.into_children();
            [VarsDeclList(variables)] => {
                Ok(variables)
            },
        )
    }

    pub(crate) fn StateFrmSum(input: ParseNode) -> ParseResult<Vec<VarDecl>> {
        match_nodes!(input.into_children();
            [VarsDeclList(variables)] => {
                Ok(variables)
            },
        )
    }

    fn EOI(_input: ParseNode) -> ParseResult<()> {
        Ok(())
    }
}