oxilean_kernel/expr/
expr_traits.rs

1//! # Expr - Trait Implementations
2//!
3//! This module contains trait implementations for `Expr`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use std::fmt;
12
13use super::functions::*;
14use super::types::{Expr, Literal};
15
16impl fmt::Display for Expr {
17    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
18        match self {
19            Expr::Sort(l) if l.is_zero() => write!(f, "Prop"),
20            Expr::Sort(l) => write!(f, "Type {}", l),
21            Expr::BVar(n) => write!(f, "#{}", n),
22            Expr::FVar(id) => write!(f, "fvar_{}", id.0),
23            Expr::Const(name, levels) if levels.is_empty() => write!(f, "{}", name),
24            Expr::Const(name, levels) => {
25                write!(f, "{}.{{", name)?;
26                for (i, l) in levels.iter().enumerate() {
27                    if i > 0 {
28                        write!(f, ", ")?;
29                    }
30                    write!(f, "{}", l)?;
31                }
32                write!(f, "}}")
33            }
34            Expr::App(fun, arg) => write!(f, "({} {})", fun, arg),
35            Expr::Lam(_, name, ty, body) => write!(f, "(λ {} : {}, {})", name, ty, body),
36            Expr::Pi(_, name, ty, body) => {
37                if !has_loose_bvar(body, 0) {
38                    write!(f, "({} → {})", ty, body)
39                } else {
40                    write!(f, "(Π {} : {}, {})", name, ty, body)
41                }
42            }
43            Expr::Let(name, ty, val, body) => {
44                write!(f, "(let {} : {} := {} in {})", name, ty, val, body)
45            }
46            Expr::Lit(Literal::Nat(n)) => write!(f, "{}", n),
47            Expr::Lit(Literal::Str(s)) => write!(f, "\"{}\"", s),
48            Expr::Proj(name, idx, e) => write!(f, "{}.{} {}", name, idx, e),
49        }
50    }
51}
oxilean_kernel/expr/expr_traits.rs

oxilean_kernel/expr/
expr_traits.rs
