ocas-rewrite 0.13.1

Pattern matching, rewriting and rule-based simplification for oCAS
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131

//! Rule-based simplification for oCAS.
//!
//! The [`simplify`] function applies a list of rewrite rules to an atom tree in
//! a bottom-up traversal, repeatedly, until no rule fires or a limit is
//! reached. It composes with the [`Transformer`](crate::transformer) and
//! [`Rule`] machinery.

use ocas_atom::{Atom, AtomArena};

use crate::rules::Rule;
use crate::transformer::transform;

/// Simplify an atom using the supplied rewrite rules.
///
/// Rules are applied bottom-up and repeatedly until a fixpoint is reached or
/// `iter_limit` iterations have been performed. For the default rule set, a
/// small limit (e.g., 20) is usually sufficient.
///
/// # Example
///
/// ```
/// use ocas_atom::AtomArena;
/// use ocas_core::arena::Arena;
/// use ocas_rewrite::rules::{default_rules, Rule};
/// use ocas_rewrite::simplify::simplify;
///
/// let arena = Arena::new();
/// let ctx = AtomArena::new(&arena);
/// let rules = default_rules(&ctx, &VecAlloc);
///
/// let x = ctx.var("x");
/// let expr = ctx.mul(&[x, ctx.num(0)]);
/// let result = simplify(&ctx, expr, &rules, 10);
///
/// assert_eq!(result.to_string(), "0");
/// # struct VecAlloc;
/// # impl<'a> ocas_rewrite::pattern::PatternAlloc<'a> for VecAlloc {
/// #     fn alloc_slice(&self, _: &[ocas_rewrite::pattern::Pattern<'a>]) -> &'a [ocas_rewrite::pattern::Pattern<'a>] { unreachable!() }
/// # }
/// ```
pub fn simplify<'a>(
    ctx: &'a AtomArena<'a>,
    atom: Atom<'a>,
    rules: &[Rule<'a>],
    iter_limit: usize,
) -> Atom<'a> {
    let mut current = transform(ctx, atom, |a| apply_rules(ctx, a, rules));
    for _ in 1..iter_limit {
        let next = transform(ctx, current, |a| apply_rules(ctx, a, rules));
        if next == current {
            return next;
        }
        current = next;
    }
    current
}

fn apply_rules<'a>(ctx: &'a AtomArena<'a>, atom: Atom<'a>, rules: &[Rule<'a>]) -> Option<Atom<'a>> {
    for rule in rules {
        if let Some(replacement) = rule.apply(ctx, atom) {
            return Some(replacement);
        }
    }
    None
}

#[cfg(test)]
mod tests {
    use super::*;
    use ocas_atom::AtomArena;
    use ocas_core::arena::Arena;

    use crate::pattern::PatternAlloc;
    use crate::rules::default_rules;

    struct VecAlloc;

    impl<'a> PatternAlloc<'a> for VecAlloc {
        fn alloc_slice(
            &self,
            _items: &[crate::pattern::Pattern<'a>],
        ) -> &'a [crate::pattern::Pattern<'a>] {
            unreachable!()
        }
    }

    #[test]
    fn simplify_mul_zero() {
        let arena = Arena::new();
        let ctx = AtomArena::new(&arena);
        let rules = default_rules(&ctx, &VecAlloc);
        let x = ctx.var("x");
        let expr = ctx.mul(&[x, ctx.num(0)]);
        let result = simplify(&ctx, expr, &rules, 10);
        assert_eq!(result.to_string(), "0");
    }

    #[test]
    fn simplify_add_same() {
        let arena = Arena::new();
        let ctx = AtomArena::new(&arena);
        let rules = default_rules(&ctx, &VecAlloc);
        let x = ctx.var("x");
        let expr = ctx.add(&[x, x]);
        let result = simplify(&ctx, expr, &rules, 10);
        assert_eq!(result.to_string(), "2*x");
    }

    #[test]
    fn simplify_nested() {
        let arena = Arena::new();
        let ctx = AtomArena::new(&arena);
        let rules = default_rules(&ctx, &VecAlloc);
        let x = ctx.var("x");
        let inner = ctx.mul(&[x, ctx.num(0)]);
        let expr = ctx.add(&[inner, x]);
        let result = simplify(&ctx, expr, &rules, 10);
        assert_eq!(result.to_string(), "x");
    }

    #[test]
    fn simplify_pow_zero() {
        let arena = Arena::new();
        let ctx = AtomArena::new(&arena);
        let rules = default_rules(&ctx, &VecAlloc);
        let x = ctx.var("x");
        let expr = ctx.pow(x, ctx.num(0));
        let result = simplify(&ctx, expr, &rules, 10);
        assert_eq!(result.to_string(), "1");
    }
}