kontroli 0.4.0

Type checking for the lambda-Pi calculus modulo rewriting
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

//! Substitution and shifting for terms.

use super::sterm::{Comb, SComb, STerm};

impl<'s, 't> STerm<'s, 't> {
    pub fn apply_subst<S>(&mut self, subst: &S, k: usize) -> bool
    where
        S: Fn(usize, usize) -> STerm<'s, 't>,
    {
        match self {
            Self::Var(n) if *n >= k => *self = subst(*n, k),
            Self::LComb(c) => {
                let mut c = SComb::from(*c);
                let change = c.apply_subst(subst, k);
                *self = Self::SComb(c.into());
                return change;
            }
            Self::SComb(c) => match alloc::rc::Rc::get_mut(c) {
                Some(c) => return c.apply_subst(subst, k),
                None => {
                    let mut c2: SComb = (**c).clone();
                    if c2.apply_subst(subst, k) {
                        *c = c2.into();
                    } else {
                        return false;
                    }
                }
            },
            _ => return false,
        }
        true
    }

    pub fn subst(mut self, u: &Self) -> Self {
        self.apply_subst(&u.psubst_single(), 0);
        self
    }

    fn psubst_single<'a>(&'a self) -> impl Fn(usize, usize) -> STerm<'s, 't> + 'a {
        move |n: usize, k: usize| {
            if n == k {
                self.clone().shift(k)
            } else {
                Self::Var(n - 1)
            }
        }
    }

    pub fn shift(mut self, rhs: usize) -> Self {
        if rhs != 0 {
            self.shift_mut(rhs);
        }
        self
    }

    pub fn shift_mut(&mut self, rhs: usize) {
        self.apply_subst(&|n, _k| Self::Var(n + rhs), 0);
    }
}

impl<'s, 't> SComb<'s, 't> {
    pub fn apply_subst<S>(&mut self, subst: &S, k: usize) -> bool
    where
        S: Fn(usize, usize) -> STerm<'s, 't>,
    {
        let sub = |tm: &mut STerm<'s, 't>| tm.apply_subst(subst, k);
        let mut change;
        match self {
            Comb::Appl(f, args) => {
                change = sub(f);
                args.iter_mut().for_each(|x| change = sub(x) || change);
            }
            Comb::Abst(_, ty, f) => {
                change = f.apply_subst(subst, k + 1);
                ty.iter_mut().for_each(|x| change = sub(x) || change);
            }
            Comb::Prod(_, ty, f) => {
                change = sub(ty);
                change = f.apply_subst(subst, k + 1) || change;
            }
        }
        change
    }
}