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

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

use voile_util::tags::{Plicit, VarRec};
use Plicit::{Ex as Explicit, Im as Implicit};

use crate::syntax::{
    common::ConHead,
    core::{Bind, Closure, Elim, Term, TermInfo, Val, ValData},
};

impl Display for Elim {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        match self {
            Elim::App(app) => app.fmt(f),
            Elim::Proj(field) => write!(f, ".{}", field),
        }
    }
}

impl Display for Term {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        match self {
            Term::Whnf(v) => v.fmt(f),
            Term::Redex(_, ident, args) => pretty_application(f, &ident.text, args),
        }
    }
}

impl Display for Val {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        use Val::*;
        match self {
            Meta(mi, a) => {
                f.write_str("?")?;
                pretty_application(f, mi, a)
            }
            Var(fun, a) => pretty_application(f, fun, a),
            Type(l) => write!(f, "set{}", l),
            Pi(Bind { licit, ty, .. }, clos) => match licit {
                Explicit => write!(f, "({} -> {})", ty, clos),
                Implicit => write!(f, "({{{}}} -> {})", ty, clos),
            },
            Cons(name, a) => pretty_application(f, name, a),
            Data(info) => info.fmt(f),
            Axiom(i) => write!(f, "<{}>", i),
            Id(ty, a, b) => write!(f, "({} =[{}] {})", a, ty, b),
            Refl => f.write_str("refl"),
        }
    }
}

impl Display for ValData {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        f.write_str(match self.kind {
            VarRec::Variant => "data",
            VarRec::Record => "codata",
        })?;
        pretty_application(f, &self.def, &self.args)
    }
}

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

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

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

fn pretty_application(
    f: &mut Formatter,
    fun: &impl Display,
    a: &[impl Display],
) -> Result<(), Error> {
    if a.is_empty() {
        fun.fmt(f)
    } else {
        write!(f, "({}", fun)?;
        for x in a {
            write!(f, " {}", x)?;
        }
        f.write_str(")")
    }
}