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

use alloc::vec::Vec;
use core::fmt::{self, Display};

/// Application of a list of arguments to a symbol.
#[derive(Clone)]
pub struct App<S, A> {
    pub symbol: S,
    pub args: Vec<A>,
}

impl<S, A> From<S> for App<S, A> {
    fn from(symbol: S) -> Self {
        let args = Vec::new();
        Self { symbol, args }
    }
}

impl<S: Display, A: Display> Display for App<S, A> {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        format(&self.symbol, &self.args, f)
    }
}

pub fn format<H: Display, T: Display>(head: &H, tail: &[T], f: &mut fmt::Formatter) -> fmt::Result {
    let parens = !tail.is_empty();
    if parens {
        write!(f, "(")?;
    };
    write!(f, "{}", head)?;
    for t in tail {
        write!(f, " {}", t)?;
    }
    if parens {
        write!(f, ")")?;
    };
    Ok(())
}