1 
use merc_aterm::ATerm;
2 
use merc_aterm::Symbol;
3 
use merc_data::DataApplication;
4 
use merc_data::DataExpression;
5 
use merc_syntax::DataExpr;
6 
use merc_syntax::EqnDecl;
7 
use merc_syntax::UntypedDataSpecification;
8 
use merc_utilities::MercError;
9 

            

        

            

                10
            

            

                
            

            

                
use crate::Condition;

            

        

            

                11
            

            

                
            

            

                
use crate::RewriteSpecification;

            

        

            

                12
            

            

                
            

            

                
use crate::Rule;

            

        

            

                13
            

            

                
            

            

                

            

        

            

                14
            

            

                
            

            

                
/// Converts an `DataSpecification` to a `RewriteSpecification` by converting each equation declaration to a rewrite rule.

            

        

            

                15
            

            

                
            

            

                
pub fn to_rewrite_spec(spec: &UntypedDataSpecification) -> Result<RewriteSpecification, MercError> {

            

        

            

                16
            

            

                
            

            

                
    let mut rewrite_rules = Vec::new();

            

        

            

                17
            

            

                
            

            

                

            

        

            

                18
            

            

                
            

            

                
    let true_term = DataApplication::with_args(&ATerm::constant(&Symbol::new("true", 0)), &[] as &[ATerm]).into();

            

        

            

                19
            

            

                
            

            

                

            

        

            

                20
            

            

                
            

            

                
    for eqn_spec in &spec.equation_declarations {

            

        

            

                21
            

            

                
            

            

                
        for equation in &eqn_spec.equations {

            

        

            

                22
            

            

                
            

            

                
            rewrite_rules.push(to_rewrite_rule(equation, &true_term));

            

        

            

                23
            

            

                
            

            

                
        }

            

        

            

                24
            

            

                
            

            

                
    }

            

        

            

                25
            

            

                
            

            

                

            

        

            

                26
            

            

                
            

            

                
    Ok(RewriteSpecification::new(rewrite_rules))

            

        

            

                27
            

            

                
            

            

                
}

            

        

            

                28
            

            

                
            

            

                

            

        

            

                29
            

            

                
            

            

                
/// Convert a `crate::DataExpr` to a term representation.

            

        

            

                30
            

            

                
            

            

                
pub fn data_expr_to_term(_expr: &DataExpr) -> DataExpression {

            

        

            

                31
            

            

                
            

            

                
    unimplemented!("Conversion of data expressions to terms is not yet implemented");

            

        

            

                32
            

            

                
            

            

                
}

            

        

            

                33
            

            

                
            

            

                

            

        

            

                34
            

            

                
            

            

                
/// Convert an `EqnDecl` to a rewrite rule in the `Rule` form.

            

        

            

                35
            

            

                
            

            

                
fn to_rewrite_rule(equation: &EqnDecl, true_term: &DataExpression) -> Rule {

            

        

            

                36
            

            

                
            

            

                
    // Convert the left-hand side and right-hand side terms

            

        

            

                37
            

            

                
            

            

                
    let lhs = data_expr_to_term(&equation.lhs);

            

        

            

                38
            

            

                
            

            

                
    let rhs = data_expr_to_term(&equation.rhs);

            

        

            

                39
            

            

                
            

            

                

            

        

            

                40
            

            

                
            

            

                
    if let Some(condition) = &equation.condition {

            

        

            

                41
            

            

                
            

            

                
        let condition = Condition::new(data_expr_to_term(condition), true_term.clone(), true);

            

        

            

                42
            

            

                
            

            

                

            

        

            

                43
            

            

                
            

            

                
        Rule::with_condition(vec![condition], lhs, rhs)

            

        

            

                44
            

            

                
            

            

                
    } else {

            

        

            

                45
            

            

                
            

            

                
        Rule::new(lhs, rhs)

            

        

            

                46
            

            

                
            

            

                
    }

            

        

            

                47
            

            

                
            

            

                
}