oxilean_parse/ast_impl/
surfaceexpr_traits.rs

1//! # SurfaceExpr - Trait Implementations
2//!
3//! This module contains trait implementations for `SurfaceExpr`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use super::types::SurfaceExpr;
12use std::fmt;
13
14impl fmt::Display for SurfaceExpr {
15    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
16        match self {
17            SurfaceExpr::Sort(sk) => write!(f, "{}", sk),
18            SurfaceExpr::Var(name) => write!(f, "{}", name),
19            SurfaceExpr::App(fun, arg) => write!(f, "({} {})", fun.value, arg.value),
20            SurfaceExpr::Lam(_, body) => write!(f, "(fun ... => {})", body.value),
21            SurfaceExpr::Pi(_, body) => write!(f, "(forall ..., {})", body.value),
22            SurfaceExpr::Let(name, _, val, body) => {
23                write!(f, "(let {} := {} in {})", name, val.value, body.value)
24            }
25            SurfaceExpr::Lit(lit) => write!(f, "{}", lit),
26            SurfaceExpr::Ann(expr, ty) => write!(f, "({} : {})", expr.value, ty.value),
27            SurfaceExpr::Hole => write!(f, "_"),
28            SurfaceExpr::Proj(expr, field) => write!(f, "{}.{}", expr.value, field),
29            SurfaceExpr::If(cond, then_e, else_e) => {
30                write!(
31                    f,
32                    "(if {} then {} else {})",
33                    cond.value, then_e.value, else_e.value
34                )
35            }
36            SurfaceExpr::Match(scrut, _arms) => {
37                write!(f, "(match {} with ...)", scrut.value)
38            }
39            SurfaceExpr::Do(_) => write!(f, "(do ...)"),
40            SurfaceExpr::Have(name, ty, _, _) => {
41                write!(f, "(have {} : {} ...)", name, ty.value)
42            }
43            SurfaceExpr::Suffices(name, ty, _) => {
44                write!(f, "(suffices {} : {} ...)", name, ty.value)
45            }
46            SurfaceExpr::Show(ty, _) => write!(f, "(show {} ...)", ty.value),
47            SurfaceExpr::NamedArg(fun, name, val) => {
48                write!(f, "({} ({} := {}))", fun.value, name, val.value)
49            }
50            SurfaceExpr::AnonymousCtor(fields) => {
51                write!(f, "<")?;
52                for (i, field) in fields.iter().enumerate() {
53                    if i > 0 {
54                        write!(f, ", ")?;
55                    }
56                    write!(f, "{}", field.value)?;
57                }
58                write!(f, ">")
59            }
60            SurfaceExpr::ListLit(elems) => {
61                write!(f, "[")?;
62                for (i, elem) in elems.iter().enumerate() {
63                    if i > 0 {
64                        write!(f, ", ")?;
65                    }
66                    write!(f, "{}", elem.value)?;
67                }
68                write!(f, "]")
69            }
70            SurfaceExpr::Tuple(elems) => {
71                write!(f, "(")?;
72                for (i, elem) in elems.iter().enumerate() {
73                    if i > 0 {
74                        write!(f, ", ")?;
75                    }
76                    write!(f, "{}", elem.value)?;
77                }
78                write!(f, ")")
79            }
80            SurfaceExpr::Return(expr) => write!(f, "(return {})", expr.value),
81            SurfaceExpr::StringInterp(_parts) => write!(f, "s!\"...\""),
82            SurfaceExpr::Range(lo, hi) => {
83                if let Some(lo) = lo {
84                    write!(f, "{}", lo.value)?;
85                }
86                write!(f, "..")?;
87                if let Some(hi) = hi {
88                    write!(f, "{}", hi.value)?;
89                }
90                Ok(())
91            }
92            SurfaceExpr::ByTactic(tactics) => {
93                write!(f, "(by")?;
94                for (i, t) in tactics.iter().enumerate() {
95                    if i > 0 {
96                        write!(f, ";")?;
97                    }
98                    write!(f, " {}", t.value)?;
99                }
100                write!(f, ")")
101            }
102            SurfaceExpr::Calc(steps) => {
103                write!(f, "(calc")?;
104                for step in steps {
105                    write!(
106                        f,
107                        " {} {} {} := ...",
108                        step.lhs.value, step.rel, step.rhs.value
109                    )?;
110                }
111                write!(f, ")")
112            }
113        }
114    }
115}
oxilean_parse/ast_impl/surfaceexpr_traits.rs

oxilean_parse/ast_impl/
surfaceexpr_traits.rs
