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

use std::fmt::{Display, Error, Formatter};

use crate::syntax::common::DtKind::*;

use super::{Axiom, Closure, Neutral, Val, ValInfo};

impl Display for Neutral {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        use Neutral::*;
        match self {
            Var(dbi) => write!(f, "[{:?}]", dbi),
            // This might be conflict with other syntax.
            Ref(dbi) => write!(f, "[|{:?}|]", dbi),
            Axi(a) => a.fmt(f),
            App(fun, a) => write!(f, "({} {})", fun, a),
            Fst(p) => write!(f, "({}.1)", p),
            Snd(p) => write!(f, "({}.2)", p),
            Lift(levels, p) => write!(f, "(^[{:?}] {})", levels, p),
        }
    }
}

impl Display for Axiom {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        use Axiom::*;
        match self {
            Postulated(uid) => write!(f, "<{:?}>", uid),
            Generated(uid, dbi) => write!(f, "<{:?} {:?}>", uid, dbi),
            Unimplemented(uid, dbi) => write!(f, "[|{:?} {:?}|]", uid, dbi),
        }
    }
}

impl Display for Closure {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        self.body.fmt(f)
    }
}

impl Display for ValInfo {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        write!(f, "{} at {}", self.ast, self.info)
    }
}

impl Display for Val {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        match self {
            Val::Type(l) => write!(f, "set{}", l),
            Val::Lam(clos) => write!(f, "(\\ {})", clos),
            Val::Sum(variants) => {
                let mut started = false;
                for (name, param) in variants {
                    if started {
                        f.write_str(" + ")?;
                    } else {
                        started = true;
                    }
                    write!(f, "'{} {}", name, param)?;
                }
                if !started {
                    f.write_str("!")?;
                }
                Ok(())
            }
            Val::Dt(Pi, param_ty, clos) => write!(f, "({} -> {})", param_ty, clos),
            Val::Dt(Sigma, param_ty, clos) => write!(f, "({} * {})", param_ty, clos),
            Val::Pair(fst, snd) => write!(f, "({}, {})", fst, snd),
            Val::Neut(neut) => neut.fmt(f),
            Val::Cons(name, a) => write!(f, "(@{} {})", name, a),
        }
    }
}