minitt/
pretty.rs

1use core::fmt::Write;
2use std::fmt::{Display, Error as FmtError, Formatter};
3
4use crate::ast::*;
5use crate::check::read_back::*;
6
7impl Display for Value {
8    fn fmt(&self, f: &mut Formatter) -> Result<(), FmtError> {
9        match self {
10            Value::Lambda(closure) => {
11                f.write_str("\u{03BB} ")?;
12                closure.fmt_with_type(f, None)
13            }
14            Value::Pair(first, second) => write!(f, "({}, {})", first, second),
15            Value::Unit => f.write_str("0"),
16            Value::One => f.write_str("1"),
17            Value::Pi(input, output) => {
18                f.write_str("\u{03A0}")?;
19                f.write_str(" ")?;
20                output.fmt_with_type(f, Some(&**input))
21            }
22            Value::Type(level) => write!(f, "Type{}", level),
23            Value::Sigma(first, second) => {
24                f.write_str("\u{03A3}")?;
25                f.write_str(" ")?;
26                second.fmt_with_type(f, Some(&**first))
27            }
28            Value::Constructor(name, arguments) => write!(f, "{} {}", name, arguments),
29            // Don't print context
30            Value::Split(branches) => {
31                f.write_str("split {")?;
32                fmt_branch(branches, f)?;
33                f.write_char('}')
34            }
35            // Don't print the context
36            Value::Sum(constructors) => {
37                f.write_str("Sum {")?;
38                fmt_branch(constructors, f)?;
39                f.write_char('}')
40            }
41            Value::Neutral(neutral) => write!(f, "[{}]", neutral),
42        }
43    }
44}
45
46impl Display for Expression {
47    fn fmt(&self, f: &mut Formatter) -> Result<(), FmtError> {
48        match self {
49            Expression::Var(name) => name.fmt(f),
50            Expression::First(pair) => write!(f, "({}.1)", pair),
51            Expression::Second(pair) => write!(f, "({}.2)", pair),
52            Expression::Application(function, argument) => write!(f, "({} {})", function, argument),
53            Expression::Lambda(pattern, parameter_type, body) => {
54                f.write_str("\u{03BB} ")?;
55                pattern.fmt(f)?;
56                if let Some(parameter_type) = parameter_type {
57                    f.write_str(": ")?;
58                    parameter_type.internal.fmt(f)?;
59                }
60                f.write_str(". ")?;
61                body.fmt(f)
62            }
63            Expression::Pair(first, second) => write!(f, "({}, {})", first, second),
64            Expression::Unit => f.write_str("0"),
65            Expression::One => f.write_str("1"),
66            Expression::Pi(input, output) => {
67                f.write_str("\u{03A0}")?;
68                write!(f, " {}. {}", input, output)
69            }
70            Expression::Type(level) => write!(f, "Type{}", level),
71            Expression::Sigma(first, second) => {
72                f.write_str("\u{03A3}")?;
73                write!(f, " {}. {}", first, second)
74            }
75            Expression::Constructor(name, arguments) => write!(f, "{} {}", name, arguments),
76            Expression::Split(clauses) => {
77                f.write_str("split {")?;
78                let mut started = false;
79                for (name, clause) in clauses.iter() {
80                    if started {
81                        f.write_str(" | ")?;
82                    } else {
83                        started = true;
84                    }
85                    name.fmt(f)?;
86                    f.write_char(' ')?;
87                    match &**clause {
88                        Expression::Lambda(pattern, _, body) => {
89                            pattern.fmt(f)?;
90                            f.write_str(" => ")?;
91                            body.fmt(f)
92                        }
93                        rest => rest.fmt(f),
94                    }?;
95                }
96                f.write_char('}')
97            }
98            // Don't print the context
99            Expression::Sum(constructors) => {
100                f.write_str("Sum")?;
101                f.write_str(" {")?;
102                fmt_branch(constructors, f)?;
103                f.write_char('}')
104            }
105            Expression::Declaration(declaration, rest) => writeln!(f, "{};\n{}", declaration, rest),
106            Expression::Constant(pattern, body, rest) => {
107                write!(f, "const {} = {};\n{}", pattern, body, rest)
108            }
109            Expression::Void => Ok(()),
110            Expression::Merge(lhs, rhs) => {
111                lhs.fmt(f)?;
112                f.write_str(" ++ ")?;
113                rhs.fmt(f)
114            }
115        }
116    }
117}
118
119impl<Expr: Display, Value: Clone + Display> Display for GenericCase<Expr, Value> {
120    fn fmt(&self, f: &mut Formatter) -> Result<(), FmtError> {
121        self.expression.fmt(f)
122    }
123}
124
125impl Display for Typed {
126    fn fmt(&self, f: &mut Formatter) -> Result<(), FmtError> {
127        write!(f, "{}: {}", self.pattern, self.expression)
128    }
129}
130
131fn fmt_branch<E: Display>(branch: &GenericBranch<E>, f: &mut Formatter) -> Result<(), FmtError> {
132    let mut started = false;
133    for (name, clause) in branch.iter() {
134        if started {
135            f.write_str(" | ")?;
136        } else {
137            started = true;
138        }
139        name.fmt(f)?;
140        f.write_char(' ')?;
141        clause.fmt(f)?;
142    }
143    Ok(())
144}
145
146impl Display for Pattern {
147    fn fmt(&self, f: &mut Formatter) -> Result<(), FmtError> {
148        match self {
149            Pattern::Pair(first, second) => write!(f, "({}, {})", first, second),
150            Pattern::Unit => f.write_char('_'),
151            Pattern::Var(name) => f.write_str(name.as_str()),
152        }
153    }
154}
155
156impl Display for Declaration {
157    fn fmt(&self, f: &mut Formatter) -> Result<(), FmtError> {
158        f.write_str(if self.is_recursive { "rec" } else { "let" })?;
159        f.write_char(' ')?;
160        self.pattern.fmt(f)?;
161        for typed in self.prefix_parameters.iter() {
162            write!(f, "({})", typed)?;
163        }
164        f.write_str(": ")?;
165        self.signature.fmt(f)?;
166        f.write_str(" = ")?;
167        self.body.fmt(f)
168    }
169}
170
171impl Display for Closure {
172    fn fmt(&self, f: &mut Formatter) -> Result<(), FmtError> {
173        match self {
174            // Don't print the scope
175            Closure::Abstraction(_, pt, _, _) => self.fmt_with_type(f, pt.as_ref().map(|t| &**t)),
176            e => e.fmt_with_type(f, None),
177        }
178    }
179}
180
181impl Closure {
182    /// Actual implementation of `fmt` for `Closure`
183    pub fn fmt_with_type(&self, f: &mut Formatter, t: Option<&Value>) -> Result<(), FmtError> {
184        match self {
185            Closure::Abstraction(pattern, _, body, _) => {
186                pattern.fmt(f)?;
187                if let Some(t) = t {
188                    f.write_str(": ")?;
189                    t.fmt(f)?;
190                }
191                f.write_str(". ")?;
192                body.fmt(f)
193            }
194            Closure::Value(value) => value.fmt(f),
195            Closure::Choice(rest, name) => write!(f, "{}. {}", name, rest),
196        }
197    }
198}
199
200impl<Value: Display + Clone> Display for GenericNeutral<Value> {
201    fn fmt(&self, f: &mut Formatter) -> Result<(), FmtError> {
202        match self {
203            GenericNeutral::Generated(index) => write!(f, "<{}>", index),
204            GenericNeutral::Application(function, argument) => {
205                write!(f, "({} {})", function, argument)
206            }
207            GenericNeutral::First(pair) => write!(f, "({}.1)", pair),
208            GenericNeutral::Second(pair) => write!(f, "({}.2)", pair),
209            GenericNeutral::Split(clauses, argument) => {
210                write!(f, "app {} {{", argument)?;
211                fmt_branch(clauses, f)?;
212                f.write_char('}')
213            }
214        }
215    }
216}
217
218impl Display for NormalExpression {
219    fn fmt(&self, f: &mut Formatter) -> Result<(), FmtError> {
220        use crate::check::read_back::NormalExpression as Expression;
221        match self {
222            Expression::Lambda(index, expression) => {
223                f.write_str("\u{03BB} <")?;
224                write!(f, "{}> {}", index, expression)
225            }
226            Expression::Pair(first, second) => write!(f, "({}, {})", first, second),
227            Expression::Unit => f.write_str("0"),
228            Expression::One => f.write_str("1"),
229            Expression::Pi(input, index, output) => {
230                f.write_str("\u{03A0}")?;
231                write!(f, " <{}> {}. {}", index, input, output)
232            }
233            Expression::Type(level) => write!(f, "Type{}", level),
234            Expression::Sigma(first, index, second) => {
235                f.write_str("\u{03A3}")?;
236                write!(f, " <{}> {}. {}", index, first, second)
237            }
238            Expression::Constructor(name, arguments) => write!(f, "{} {}", name, arguments),
239            Expression::Split(clauses) => {
240                f.write_str("split {")?;
241                fmt_branch(clauses, f)?;
242                f.write_char('}')
243            }
244            // Don't print the context
245            Expression::Sum(constructors) => {
246                f.write_str("Sum {")?;
247                fmt_branch(constructors, f)?;
248                f.write_char('}')
249            }
250            Expression::Neutral(neutral) => write!(f, "[{}]", neutral),
251        }
252    }
253}
254
255/// Actually it's for NeutralTelescope
256impl<Value: Clone + Display> Display for GenericTelescope<Value> {
257    fn fmt(&self, f: &mut Formatter) -> Result<(), FmtError> {
258        match self {
259            GenericTelescope::Nil => Ok(()),
260            GenericTelescope::UpDec(previous, declaration) => {
261                write!(f, "{};\n{}", declaration, previous)
262            }
263            GenericTelescope::UpVar(previous, pattern, value) => {
264                write!(f, "var {}: {};\n{}", pattern, value, previous)
265            }
266        }
267    }
268}
269
270#[cfg(test)]
271mod tests {
272    use crate::ast::Declaration;
273    use crate::ast::Expression;
274    use crate::ast::Pattern;
275
276    #[test]
277    fn simple_expr() {
278        let expr = Expression::Second(Box::new(Expression::Pair(
279            Box::new(Expression::One),
280            Box::new(Expression::Unit),
281        )));
282        println!("{}", expr);
283    }
284
285    #[test]
286    fn simple_decl() {
287        let var = "a".to_string();
288        let expr = Expression::Declaration(
289            Box::new(Declaration::simple(
290                Pattern::Unit,
291                vec![],
292                Expression::One,
293                Expression::Second(Box::new(Expression::Pair(
294                    Box::new(Expression::Unit),
295                    Box::new(Expression::Unit),
296                ))),
297            )),
298            Box::new(Expression::Declaration(
299                Box::new(Declaration::recursive(
300                    Pattern::Var(var.clone()),
301                    vec![],
302                    Expression::One,
303                    Expression::First(Box::new(Expression::Pair(
304                        Box::new(Expression::Unit),
305                        Box::new(Expression::Var(var)),
306                    ))),
307                )),
308                Box::new(Expression::Void),
309            )),
310        );
311        println!("{}", expr);
312    }
313}
minitt/pretty.rs

minitt/
pretty.rs
