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::Write;

use crate::lang::display::PrecedenceLevel::*;
use crate::lang::{PartialExpr, TcEnv};
use crate::lang::UnionIndex;

#[derive(Ord, PartialOrd, Eq, PartialEq, Copy, Clone, Default)]
enum PrecedenceLevel {
    #[default]
    Let,
    Construct,
    FnType,
    Destruct,
    Base,
}

impl PartialExpr {
    fn precendence_level(&self) -> PrecedenceLevel {
        match self {
            PartialExpr::Type => Base,
            PartialExpr::Let(_, _) => Let,
            PartialExpr::DeBruijnIndex(_) => Base,
            PartialExpr::FnType(_, _) => FnType,
            PartialExpr::FnConstruct(_, _) => Construct,
            PartialExpr::FnDestruct(_, _) => Destruct,
            PartialExpr::Free => Base,
            PartialExpr::Shift(_, _) => unreachable!(),
        }
    }
}

impl TcEnv {
    fn display(
        &self,
        i: UnionIndex,
        w: &mut impl Write,
        max_precedence: PrecedenceLevel,
    ) -> std::fmt::Result {
        let e = self.values[i.0];

        if e.precendence_level() < max_precedence {
            write!(w, "(")?;
        }

        match e {
            PartialExpr::Type => write!(w, "Type")?,
            PartialExpr::Let(v, b) => {
                write!(w, "let ")?;
                self.display(v, w, Construct)?;
                writeln!(w, ";")?;
                self.display(b, w, Let)?;
            }
            PartialExpr::DeBruijnIndex(i) => write!(w, "#{i}")?,
            PartialExpr::FnType(a, b) => {
                self.display(a, w, Destruct)?;
                write!(w, " -> ")?;
                self.display(b, w, FnType)?;
            }
            PartialExpr::FnConstruct(a, b) => {
                self.display(a, w, FnType)?;
                write!(w, " => ")?;
                self.display(b, w, Construct)?;
            }
            PartialExpr::FnDestruct(a, b) => {
                self.display(a, w, Destruct)?;
                write!(w, " ")?;
                self.display(b, w, Base)?;
            }
            PartialExpr::Free => write!(w, "{{{}}}", i.0)?,
            PartialExpr::Shift(..) => unreachable!(),
        }

        if e.precendence_level() < max_precedence {
            write!(w, ")")?;
        }

        Ok(())
    }

    pub fn index_to_string(&self, i: UnionIndex) -> String {
        let mut s = String::new();
        self.display(i, &mut s, PrecedenceLevel::default())
            .expect("Writing to String shouldn't fail");
        s
    }

    pub fn index_to_sm_string(&mut self, i: UnionIndex) -> String {
        let i = self.simplify(i);
        self.index_to_string(i)
    }

    pub fn index_to_br_string(&mut self, i: UnionIndex) -> String {
        let i = self.beta_reduce(i);
        self.index_to_string(i)
    }
}