oxilean_codegen/lean4_backend/
lean4expr_traits.rs

1//! # Lean4Expr - Trait Implementations
2//!
3//! This module contains trait implementations for `Lean4Expr`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use super::functions::*;
12use super::types::Lean4Expr;
13use std::fmt;
14
15impl fmt::Display for Lean4Expr {
16    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
17        match self {
18            Lean4Expr::Var(name) => write!(f, "{}", name),
19            Lean4Expr::NatLit(n) => write!(f, "{}", n),
20            Lean4Expr::IntLit(n) => write!(f, "{}", n),
21            Lean4Expr::BoolLit(b) => write!(f, "{}", b),
22            Lean4Expr::StrLit(s) => {
23                write!(f, "\"{}\"", s.replace('\\', "\\\\").replace('"', "\\\""))
24            }
25            Lean4Expr::FloatLit(v) => write!(f, "{}", v),
26            Lean4Expr::Hole => write!(f, "_"),
27            Lean4Expr::Sorry => write!(f, "sorry"),
28            Lean4Expr::Panic(msg) => write!(f, "panic! \"{}\"", msg),
29            Lean4Expr::App(func, arg) => write!(f, "{} {}", func, paren_expr(arg)),
30            Lean4Expr::Lambda(param, ty, body) => {
31                if let Some(t) = ty {
32                    write!(f, "fun ({} : {}) => {}", param, t, body)
33                } else {
34                    write!(f, "fun {} => {}", param, body)
35                }
36            }
37            Lean4Expr::Pi(param, ty, body) => {
38                write!(f, "({} : {}) → {}", param, ty, body)
39            }
40            Lean4Expr::Let(name, ty, val, body) => {
41                if let Some(t) = ty {
42                    write!(f, "let {} : {} := {}\n{}", name, t, val, body)
43                } else {
44                    write!(f, "let {} := {}\n{}", name, val, body)
45                }
46            }
47            Lean4Expr::LetRec(name, val, body) => {
48                write!(f, "let rec {} := {}\n{}", name, val, body)
49            }
50            Lean4Expr::Match(scrutinee, arms) => {
51                writeln!(f, "match {} with", scrutinee)?;
52                for (pat, body) in arms {
53                    writeln!(f, "  | {} => {}", pat, body)?;
54                }
55                Ok(())
56            }
57            Lean4Expr::If(cond, then_e, else_e) => {
58                write!(f, "if {} then {} else {}", cond, then_e, else_e)
59            }
60            Lean4Expr::Do(stmts) => {
61                writeln!(f, "do")?;
62                for stmt in stmts {
63                    writeln!(f, "  {}", stmt)?;
64                }
65                Ok(())
66            }
67            Lean4Expr::Have(name, ty, proof, rest) => {
68                write!(f, "have {} : {} := {}\n{}", name, ty, proof, rest)
69            }
70            Lean4Expr::Show(ty, expr) => write!(f, "show {} from {}", ty, expr),
71            Lean4Expr::Calc(steps) => {
72                writeln!(f, "calc")?;
73                for step in steps {
74                    writeln!(f, "  {}", step)?;
75                }
76                Ok(())
77            }
78            Lean4Expr::ByTactic(tactics) => write!(f, "by {}", tactics.join("; ")),
79            Lean4Expr::Ascription(expr, ty) => write!(f, "({} : {})", expr, ty),
80            Lean4Expr::Tuple(elems) => {
81                write!(f, "(")?;
82                for (i, e) in elems.iter().enumerate() {
83                    if i > 0 {
84                        write!(f, ", ")?;
85                    }
86                    write!(f, "{}", e)?;
87                }
88                write!(f, ")")
89            }
90            Lean4Expr::AnonymousCtor(elems) => {
91                write!(f, "⟨")?;
92                for (i, e) in elems.iter().enumerate() {
93                    if i > 0 {
94                        write!(f, ", ")?;
95                    }
96                    write!(f, "{}", e)?;
97                }
98                write!(f, "⟩")
99            }
100            Lean4Expr::Proj(expr, field) => write!(f, "{}.{}", paren_expr(expr), field),
101            Lean4Expr::StructLit(name, fields) => {
102                write!(f, "{{ ")?;
103                if !name.is_empty() {
104                    write!(f, "{} . ", name)?;
105                }
106                for (i, (k, v)) in fields.iter().enumerate() {
107                    if i > 0 {
108                        write!(f, ", ")?;
109                    }
110                    write!(f, "{} := {}", k, v)?;
111                }
112                write!(f, " }}")
113            }
114        }
115    }
116}
oxilean_codegen/lean4_backend/lean4expr_traits.rs

oxilean_codegen/lean4_backend/
lean4expr_traits.rs
