dyadic_rationals/
traits.rs

1use crate::context::{Set, Ctx};
2
3pub trait Specializable<T, V> {
4    fn specialize(&mut self, id: &T, val: V)
5    where
6        Self: Sized;
7
8    fn free_vars(&self) -> Set<&T>;
9
10    fn is_closed(&self) -> bool where T: Ord {
11        self.free_vars().is_empty()
12    }
13
14    fn specialize_all(&mut self, ctx: Ctx<T, V>)
15    where
16        T: Ord + Clone,
17        V: Clone,
18        Self: Sized {
19        for (id, val) in ctx.iter() {
20            self.specialize(id, val.clone());
21        }
22    }
23}
24
25/// A term that can be normalized
26pub trait Normalizable {
27    fn normalize(&mut self);
28
29    /// Check if it is in normal form by syntactic equality
30    fn is_normal(&self) -> bool where Self: Clone + Eq {
31        let mut clone = self.clone();
32        clone.normalize();
33        self == &clone
34    }
35
36    /// Equality modulo normalization
37    fn eqn(&self, other: &Self) -> bool where Self: Eq + Clone {
38        let mut self_clone = self.clone();
39        let mut other_clone = other.clone();
40        self_clone.normalize();
41        other_clone.normalize();
42        self_clone == other_clone
43    }
44}
45
46// Match two expressions, like `assert_eqn!(a, b)` modulo beta-equivalence
47#[cfg(test)]
48#[macro_export]
49macro_rules! assert_eqn {
50    ($left:expr, $right:expr) => ({
51        if !Normalizable::eqn(&$left, &$right) {
52            let mut l = $left.clone();
53            let mut r = $right.clone();
54            l.normalize();
55            r.normalize();
56            panic!(
57                "Assertion failed: `assert_eqn!({}, {})`\n  left (pre): `{}`,\n  right (pre): `{}`,\n  left (post): `{}`,\n  right (post): `{}`",
58                stringify!($left), stringify!($right), $left, $right, l, r,
59            );
60        }
61    });
62}
dyadic_rationals/traits.rs

dyadic_rationals/
traits.rs
