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

//! Terms for the lambda-Pi calculus.

use crate::{Comb, Pattern, Symbol};
use alloc::{boxed::Box, string::String};
use core::fmt::{self, Display};

/// De Bruijn variable.
pub type DeBruijn = usize;

/// Long term for the lambda-Pi calculus.
#[derive(Clone, Debug, Eq, PartialEq)]
pub enum LTerm<'s> {
    Type,
    Const(Symbol<'s>),
    Var(DeBruijn),
    Comb(Box<LComb<'s>>),
}

pub type LComb<'s> = Comb<String, LTerm<'s>>;

impl<'s> TryFrom<Pattern<Symbol<'s>>> for LTerm<'s> {
    type Error = ();

    fn try_from(p: Pattern<Symbol<'s>>) -> Result<Self, Self::Error> {
        use Pattern::*;
        match p {
            Symb(s, args) => {
                let args: Result<_, _> = args.into_iter().map(Self::try_from).collect();
                Ok(LTerm::Comb(Box::new(Comb::Appl(LTerm::Const(s), args?))))
            }
            MVar(v) => Ok(LTerm::Var(v)),
            Joker => Err(()),
        }
    }
}

impl<'s> Display for LTerm<'s> {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        match self {
            Self::Type => write!(f, "Type"),
            Self::Var(v) => write!(f, "β{}", v),
            Self::Const(c) => c.fmt(f),
            Self::Comb(c) => c.fmt(f),
        }
    }
}