oxilean_codegen/idris_backend/
idrisexpr_traits.rs

1//! # IdrisExpr - Trait Implementations
2//!
3//! This module contains trait implementations for `IdrisExpr`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Display`
8//!
9//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
10
11use super::types::IdrisExpr;
12use std::fmt;
13
14impl fmt::Display for IdrisExpr {
15    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
16        match self {
17            IdrisExpr::Lit(l) => write!(f, "{}", l),
18            IdrisExpr::Var(v) => write!(f, "{}", v),
19            IdrisExpr::Qualified(parts) => write!(f, "{}", parts.join(".")),
20            IdrisExpr::Refl => write!(f, "Refl"),
21            IdrisExpr::Hole(h) => write!(f, "?{}", h),
22            IdrisExpr::AnonHole => write!(f, "?_"),
23            IdrisExpr::App(func, arg) => {
24                write!(f, "{} {}", func.fmt_arg(), arg.fmt_arg())
25            }
26            IdrisExpr::Lam(params, body) => {
27                write!(f, "\\{} => {}", params.join(", "), body)
28            }
29            IdrisExpr::Let(name, val, body) => {
30                write!(f, "let {} = {} in {}", name, val, body)
31            }
32            IdrisExpr::IfThenElse(cond, t, e) => {
33                write!(f, "if {} then {} else {}", cond, t, e)
34            }
35            IdrisExpr::Tuple(exprs) => {
36                write!(f, "(")?;
37                for (i, e) in exprs.iter().enumerate() {
38                    if i > 0 {
39                        write!(f, ", ")?;
40                    }
41                    write!(f, "{}", e)?;
42                }
43                write!(f, ")")
44            }
45            IdrisExpr::ListLit(exprs) => {
46                write!(f, "[")?;
47                for (i, e) in exprs.iter().enumerate() {
48                    if i > 0 {
49                        write!(f, ", ")?;
50                    }
51                    write!(f, "{}", e)?;
52                }
53                write!(f, "]")
54            }
55            IdrisExpr::Annot(e, t) => write!(f, "({} : {})", e, t),
56            IdrisExpr::Idiom(e) => write!(f, "[| {} |]", e),
57            IdrisExpr::ProofTerm(e) => write!(f, "believe_me {}", e.fmt_arg()),
58            IdrisExpr::Neg(e) => write!(f, "-{}", e.fmt_arg()),
59            IdrisExpr::Infix(op, l, r) => {
60                write!(f, "{} {} {}", l.fmt_arg(), op, r.fmt_arg())
61            }
62            IdrisExpr::RecordUpdate(base, fields) => {
63                write!(f, "{{ {} with ", base)?;
64                for (i, (name, val)) in fields.iter().enumerate() {
65                    if i > 0 {
66                        write!(f, ", ")?;
67                    }
68                    write!(f, "{} = {}", name, val)?;
69                }
70                write!(f, " }}")
71            }
72            IdrisExpr::WithPattern(scrutinee, alts) => {
73                writeln!(f, "with ({})", scrutinee)?;
74                for (pat, body) in alts {
75                    writeln!(f, "  ... | {} = {}", pat, body)?;
76                }
77                Ok(())
78            }
79            IdrisExpr::CaseOf(scrutinee, alts) => {
80                writeln!(f, "case {} of", scrutinee)?;
81                for (pat, body) in alts {
82                    writeln!(f, "  {} => {}", pat, body)?;
83                }
84                Ok(())
85            }
86            IdrisExpr::Do(stmts) => {
87                writeln!(f, "do")?;
88                for s in stmts {
89                    writeln!(f, "  {}", s)?;
90                }
91                Ok(())
92            }
93        }
94    }
95}
oxilean_codegen/idris_backend/idrisexpr_traits.rs

oxilean_codegen/idris_backend/
idrisexpr_traits.rs
