oxilean-parse 0.1.2

OxiLean parser - Concrete syntax to abstract syntax
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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115

//! # SurfaceExpr - Trait Implementations
//!
//! This module contains trait implementations for `SurfaceExpr`.
//!
//! ## Implemented Traits
//!
//! - `Display`
//!
//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)

use super::types::SurfaceExpr;
use std::fmt;

impl fmt::Display for SurfaceExpr {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            SurfaceExpr::Sort(sk) => write!(f, "{}", sk),
            SurfaceExpr::Var(name) => write!(f, "{}", name),
            SurfaceExpr::App(fun, arg) => write!(f, "({} {})", fun.value, arg.value),
            SurfaceExpr::Lam(_, body) => write!(f, "(fun ... => {})", body.value),
            SurfaceExpr::Pi(_, body) => write!(f, "(forall ..., {})", body.value),
            SurfaceExpr::Let(name, _, val, body) => {
                write!(f, "(let {} := {} in {})", name, val.value, body.value)
            }
            SurfaceExpr::Lit(lit) => write!(f, "{}", lit),
            SurfaceExpr::Ann(expr, ty) => write!(f, "({} : {})", expr.value, ty.value),
            SurfaceExpr::Hole => write!(f, "_"),
            SurfaceExpr::Proj(expr, field) => write!(f, "{}.{}", expr.value, field),
            SurfaceExpr::If(cond, then_e, else_e) => {
                write!(
                    f,
                    "(if {} then {} else {})",
                    cond.value, then_e.value, else_e.value
                )
            }
            SurfaceExpr::Match(scrut, _arms) => {
                write!(f, "(match {} with ...)", scrut.value)
            }
            SurfaceExpr::Do(_) => write!(f, "(do ...)"),
            SurfaceExpr::Have(name, ty, _, _) => {
                write!(f, "(have {} : {} ...)", name, ty.value)
            }
            SurfaceExpr::Suffices(name, ty, _) => {
                write!(f, "(suffices {} : {} ...)", name, ty.value)
            }
            SurfaceExpr::Show(ty, _) => write!(f, "(show {} ...)", ty.value),
            SurfaceExpr::NamedArg(fun, name, val) => {
                write!(f, "({} ({} := {}))", fun.value, name, val.value)
            }
            SurfaceExpr::AnonymousCtor(fields) => {
                write!(f, "<")?;
                for (i, field) in fields.iter().enumerate() {
                    if i > 0 {
                        write!(f, ", ")?;
                    }
                    write!(f, "{}", field.value)?;
                }
                write!(f, ">")
            }
            SurfaceExpr::ListLit(elems) => {
                write!(f, "[")?;
                for (i, elem) in elems.iter().enumerate() {
                    if i > 0 {
                        write!(f, ", ")?;
                    }
                    write!(f, "{}", elem.value)?;
                }
                write!(f, "]")
            }
            SurfaceExpr::Tuple(elems) => {
                write!(f, "(")?;
                for (i, elem) in elems.iter().enumerate() {
                    if i > 0 {
                        write!(f, ", ")?;
                    }
                    write!(f, "{}", elem.value)?;
                }
                write!(f, ")")
            }
            SurfaceExpr::Return(expr) => write!(f, "(return {})", expr.value),
            SurfaceExpr::StringInterp(_parts) => write!(f, "s!\"...\""),
            SurfaceExpr::Range(lo, hi) => {
                if let Some(lo) = lo {
                    write!(f, "{}", lo.value)?;
                }
                write!(f, "..")?;
                if let Some(hi) = hi {
                    write!(f, "{}", hi.value)?;
                }
                Ok(())
            }
            SurfaceExpr::ByTactic(tactics) => {
                write!(f, "(by")?;
                for (i, t) in tactics.iter().enumerate() {
                    if i > 0 {
                        write!(f, ";")?;
                    }
                    write!(f, " {}", t.value)?;
                }
                write!(f, ")")
            }
            SurfaceExpr::Calc(steps) => {
                write!(f, "(calc")?;
                for step in steps {
                    write!(
                        f,
                        " {} {} {} := ...",
                        step.lhs.value, step.rel, step.rhs.value
                    )?;
                }
                write!(f, ")")
            }
        }
    }
}