merc_sabre 1.0.0

Implements a term rewrite engine based on a set automaton based rewriter.
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

use crate::Rule;
use crate::utilities::TermStack;
use crate::utilities::create_var_map;

/// This is a [Rule] condition stored as semi compressed trees such that they can be
/// subsituted efficiently.
#[derive(Hash, Clone, Eq, PartialEq, Ord, PartialOrd, Debug)]
pub struct EMACondition {
    /// Conditions lhs and rhs are stored in the term pool as much as possible with a SemiCompressedTermTree
    pub lhs_term_stack: TermStack,
    pub rhs_term_stack: TermStack,

    /// whether the lhs and rhs should be equal or different
    pub equality: bool,
}

/// Computes the extended condition from a given rewrite rule.
pub fn extend_conditions(rule: &Rule) -> Vec<EMACondition> {
    let var_map = create_var_map(&rule.lhs);
    let mut conditions = vec![];

    for c in &rule.conditions {
        let ema_condition = EMACondition {
            lhs_term_stack: TermStack::from_term(&c.lhs.copy(), &var_map),
            rhs_term_stack: TermStack::from_term(&c.rhs.copy(), &var_map),
            equality: c.equality,
        };
        conditions.push(ema_condition);
    }

    conditions
}