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

use core::fmt::{self, Display};

/// Combinator term.
#[derive(Clone, Debug, Eq, PartialEq)]
pub enum Comb<Id, Tm> {
    /// Application
    Appl(Tm, alloc::vec::Vec<Tm>),
    /// Product
    Prod(Id, Tm, Tm),
    /// Abstraction
    Abst(Id, Option<Tm>, Tm),
}

impl<Id, Tm> Comb<Id, Tm> {
    /// Return true if the term
    /// (or the application of some terms to it, if `no_args` is false)
    /// is *surely* in weak-head normal form.
    ///
    /// In cases where it is not clear by looking at the term
    /// whether it is in WHNF (for example, for applications),
    /// this function plays it safe and returns false.
    pub fn is_whnf(&self, no_args: impl FnOnce() -> bool) -> bool {
        match self {
            Comb::Appl(..) => false,
            Comb::Prod(..) => true,
            Comb::Abst(..) => no_args(),
        }
    }
}

/// This is usually used to convert LComb to SComb.
impl<'c, Id, Tm, Tm2: From<&'c Tm>> From<&'c Comb<Id, Tm>> for Comb<&'c Id, Tm2> {
    fn from(comb: &'c Comb<Id, Tm>) -> Self {
        match comb {
            Comb::Appl(tm, args) => Self::Appl(Tm2::from(tm), args.iter().map(Tm2::from).collect()),
            Comb::Prod(id, ty, tm) => Self::Prod(id, Tm2::from(ty), Tm2::from(tm)),
            Comb::Abst(id, ty, tm) => Self::Abst(id, ty.as_ref().map(Tm2::from), Tm2::from(tm)),
        }
    }
}

/// This is usually used to convert SComb to LComb.
impl<'s, 'c, Id: Clone, Tm, Tm2: TryFrom<&'c Tm>> TryFrom<&'c Comb<&'s Id, Tm>> for Comb<Id, Tm2> {
    type Error = Tm2::Error;
    fn try_from(comb: &'c Comb<&'s Id, Tm>) -> Result<Self, Self::Error> {
        match comb {
            Comb::Appl(head, args) => Ok(Self::Appl(
                Tm2::try_from(head)?,
                args.iter().map(Tm2::try_from).collect::<Result<_, _>>()?,
            )),
            Comb::Prod(id, ty, tm) => Ok(Self::Prod(
                (*id).clone(),
                Tm2::try_from(ty)?,
                Tm2::try_from(tm)?,
            )),
            Comb::Abst(id, ty, tm) => Ok(Self::Abst(
                (*id).clone(),
                ty.as_ref().map(Tm2::try_from).transpose()?,
                Tm2::try_from(tm)?,
            )),
        }
    }
}

impl<V: Display, Tm: Display> Display for Comb<V, Tm> {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        match self {
            Self::Appl(head, tail) => crate::app::format(head, tail, f),
            Self::Prod(id, ty, tm) => write!(f, "(Π {} : {}. {})", id, ty, tm),
            Self::Abst(id, None, tm) => write!(f, "(λ {}. {})", id, tm),
            Self::Abst(id, Some(ty), tm) => write!(f, "(λ {} : {}. {})", id, ty, tm),
        }
    }
}