1 
//! Regression tests for the Sabre rewriter that exercise rules whose delayed
2 
//! equivalence/condition checks fail. A failing delayed check used to leave the
3 
//! configuration untouched, causing `SabreRewriter` to loop forever while
4 
//! `InnermostRewriter` returned immediately.
5 

            

        

            

                6
            

            

                
            

            

                
use ahash::AHashSet;

            

        

            

                7
            

            

                
            

            

                

            

        

            

                8
            

            

                
            

            

                
use merc_aterm::ATerm;

            

        

            

                9
            

            

                
            

            

                
use merc_data::DataExpression;

            

        

            

                10
            

            

                
            

            

                
use merc_data::to_untyped_data_expression;

            

        

            

                11
            

            

                
            

            

                
use merc_sabre::Condition;

            

        

            

                12
            

            

                
            

            

                
use merc_sabre::InnermostRewriter;

            

        

            

                13
            

            

                
            

            

                
use merc_sabre::RewriteEngine;

            

        

            

                14
            

            

                
            

            

                
use merc_sabre::RewriteSpecification;

            

        

            

                15
            

            

                
            

            

                
use merc_sabre::Rule;

            

        

            

                16
            

            

                
            

            

                
use merc_sabre::SabreRewriter;

            

        

            

                17
            

            

                
            

            

                
use merc_sabre::test_utility::create_rewrite_rule;

            

        

            

                18
            

            

                
            

            

                

            

        

            

                19
            

            

                
            

            

                
/// Parses `input` into an untyped data expression, treating `variables` as variables.

            

        

            

                20
            

            

                8
            

            

                
fn term(input: &str, variables: &[&str]) -> DataExpression {

            

        

            

                21
            

            

                8
            

            

                
    let vars: AHashSet<String> = variables.iter().map(|v| v.to_string()).collect();

            

        

            

                22
            

            

                8
            

            

                
    to_untyped_data_expression(ATerm::from_string(input).unwrap(), Some(&vars))

            

        

            

                23
            

            

                8
            

            

                
}

            

        

            

                24
            

            

                
            

            

                

            

        

            

                25
            

            

                
            

            

                
/// Asserts that both rewrite engines rewrite `input` to `expected`.

            

        

            

                26
            

            

                2
            

            

                
fn assert_both_engines(spec: &RewriteSpecification, input: &str, expected: &str) {

            

        

            

                27
            

            

                2
            

            

                
    let input = term(input, &[]);

            

        

            

                28
            

            

                2
            

            

                
    let expected = term(expected, &[]);

            

        

            

                29
            

            

                
            

            

                

            

        

            

                30
            

            

                2
            

            

                
    let mut inner = InnermostRewriter::new(spec);

            

        

            

                31
            

            

                2
            

            

                
    assert_eq!(inner.rewrite(&input), expected, "InnermostRewriter result mismatch");

            

        

            

                32
            

            

                
            

            

                

            

        

            

                33
            

            

                2
            

            

                
    let mut sabre = SabreRewriter::new(spec);

            

        

            

                34
            

            

                2
            

            

                
    assert_eq!(sabre.rewrite(&input), expected, "SabreRewriter result mismatch");

            

        

            

                35
            

            

                2
            

            

                
}

            

        

            

                36
            

            

                
            

            

                

            

        

            

                37
            

            

                
            

            

                
/// A non-linear rule `eq(x, x) -> t` whose equivalence-class check fails on

            

        

            

                38
            

            

                
            

            

                
/// `eq(a, b)`; the term is already in normal form.

            

        

            

                39
            

            

                
            

            

                
#[test]

            

        

            

                40
            

            

                1
            

            

                
fn test_failing_equivalence_check_terminates() {

            

        

            

                41
            

            

                1
            

            

                
    let spec = RewriteSpecification::new(vec![create_rewrite_rule("eq(x, x)", "t", &["x"]).unwrap()]);

            

        

            

                42
            

            

                
            

            

                

            

        

            

                43
            

            

                1
            

            

                
    assert_both_engines(&spec, "eq(a, b)", "eq(a, b)");

            

        

            

                44
            

            

                1
            

            

                
}

            

        

            

                45
            

            

                
            

            

                

            

        

            

                46
            

            

                
            

            

                
/// A conditional rule `f(x) -> t` (with condition `x == a`) whose condition

            

        

            

                47
            

            

                
            

            

                
/// check fails on `f(b)`; the term is already in normal form.

            

        

            

                48
            

            

                
            

            

                
#[test]

            

        

            

                49
            

            

                1
            

            

                
fn test_failing_condition_check_terminates() {

            

        

            

                50
            

            

                1
            

            

                
    let rule = Rule::with_condition(

            

        

            

                51
            

            

                1
            

            

                
        vec![Condition::new(term("x", &["x"]), term("a", &["x"]), true)],

            

        

            

                52
            

            

                1
            

            

                
        term("f(x)", &["x"]),

            

        

            

                53
            

            

                1
            

            

                
        term("t", &["x"]),

            

        

            

                54
            

            

                
            

            

                
    );

            

        

            

                55
            

            

                1
            

            

                
    let spec = RewriteSpecification::new(vec![rule]);

            

        

            

                56
            

            

                
            

            

                

            

        

            

                57
            

            

                1
            

            

                
    assert_both_engines(&spec, "f(b)", "f(b)");

            

        

            

                58
            

            

                1
            

            

                
}