kontroli/kernel/
subst.rs

1//! Substitution and shifting for terms.
2
3use super::sterm::{Comb, SComb, STerm};
4
5impl<'s, 't> STerm<'s, 't> {
6    pub fn apply_subst<S>(&mut self, subst: &S, k: usize) -> bool
7    where
8        S: Fn(usize, usize) -> STerm<'s, 't>,
9    {
10        match self {
11            Self::Var(n) if *n >= k => *self = subst(*n, k),
12            Self::LComb(c) => {
13                let mut c = SComb::from(*c);
14                let change = c.apply_subst(subst, k);
15                *self = Self::SComb(c.into());
16                return change;
17            }
18            Self::SComb(c) => match alloc::rc::Rc::get_mut(c) {
19                Some(c) => return c.apply_subst(subst, k),
20                None => {
21                    let mut c2: SComb = (**c).clone();
22                    if c2.apply_subst(subst, k) {
23                        *c = c2.into();
24                    } else {
25                        return false;
26                    }
27                }
28            },
29            _ => return false,
30        }
31        true
32    }
33
34    pub fn subst(mut self, u: &Self) -> Self {
35        self.apply_subst(&u.psubst_single(), 0);
36        self
37    }
38
39    fn psubst_single<'a>(&'a self) -> impl Fn(usize, usize) -> STerm<'s, 't> + 'a {
40        move |n: usize, k: usize| {
41            if n == k {
42                self.clone().shift(k)
43            } else {
44                Self::Var(n - 1)
45            }
46        }
47    }
48
49    pub fn shift(mut self, rhs: usize) -> Self {
50        if rhs != 0 {
51            self.shift_mut(rhs);
52        }
53        self
54    }
55
56    pub fn shift_mut(&mut self, rhs: usize) {
57        self.apply_subst(&|n, _k| Self::Var(n + rhs), 0);
58    }
59}
60
61impl<'s, 't> SComb<'s, 't> {
62    pub fn apply_subst<S>(&mut self, subst: &S, k: usize) -> bool
63    where
64        S: Fn(usize, usize) -> STerm<'s, 't>,
65    {
66        let sub = |tm: &mut STerm<'s, 't>| tm.apply_subst(subst, k);
67        let mut change;
68        match self {
69            Comb::Appl(f, args) => {
70                change = sub(f);
71                args.iter_mut().for_each(|x| change = sub(x) || change);
72            }
73            Comb::Abst(_, ty, f) => {
74                change = f.apply_subst(subst, k + 1);
75                ty.iter_mut().for_each(|x| change = sub(x) || change);
76            }
77            Comb::Prod(_, ty, f) => {
78                change = sub(ty);
79                change = f.apply_subst(subst, k + 1) || change;
80            }
81        }
82        change
83    }
84}
kontroli/kernel/subst.rs

kontroli/kernel/
subst.rs
