logicaffeine_kernel/dag/
pretty.rs

1//! A bounded, readable rendering of core expressions for diagnostics.
2
3use super::expr::{ExprId, Lit, Node};
4use super::level::{LevelId, LevelNode};
5use super::tc::Kernel;
6
7const BUDGET: usize = 400;
8
9pub fn show(k: &Kernel, e: ExprId) -> String {
10    let mut out = String::new();
11    let mut budget = BUDGET;
12    go(k, e, 0, &mut out, &mut budget, false);
13    out
14}
15
16pub fn show_level(k: &Kernel, l: LevelId) -> String {
17    match k.s.levels.node(l) {
18        LevelNode::Zero => "0".into(),
19        LevelNode::SProp => "SProp".into(),
20        LevelNode::Param(n) => k.s.names.display(n),
21        LevelNode::Succ(_) => {
22            let (mut base, mut n) = (l, 0);
23            while let LevelNode::Succ(a) = k.s.levels.node(base) {
24                base = a;
25                n += 1;
26            }
27            if base == LevelId::ZERO {
28                n.to_string()
29            } else {
30                format!("{}+{}", show_level(k, base), n)
31            }
32        }
33        LevelNode::Max(a, b) => format!("max ({}) ({})", show_level(k, a), show_level(k, b)),
34        LevelNode::IMax(a, b) => format!("imax ({}) ({})", show_level(k, a), show_level(k, b)),
35    }
36}
37
38fn go(k: &Kernel, e: ExprId, depth: u32, out: &mut String, budget: &mut usize, paren: bool) {
39    if *budget == 0 {
40        out.push('…');
41        return;
42    }
43    *budget -= 1;
44    let open = |out: &mut String| {
45        if paren {
46            out.push('(')
47        }
48    };
49    let close = |out: &mut String| {
50        if paren {
51            out.push(')')
52        }
53    };
54    match k.s.node(e) {
55        Node::BVar(i) => {
56            if i < depth {
57                out.push_str(&format!("x{}", depth - 1 - i));
58            } else {
59                out.push_str(&format!("#{i}"));
60            }
61        }
62        Node::FVar(i) => out.push_str(&format!("h{i}")),
63        Node::Sort(l) => {
64            if l == LevelId::ZERO {
65                out.push_str("Prop");
66            } else {
67                out.push_str(&format!("Sort ({})", show_level(k, l)));
68            }
69        }
70        Node::Const(n, _) => out.push_str(&k.s.names.display(n)),
71        Node::App(..) => {
72            open(out);
73            let (f, args) = k.s.app_args(e);
74            go(k, f, depth, out, budget, true);
75            for a in args {
76                out.push(' ');
77                go(k, a, depth, out, budget, true);
78            }
79            close(out);
80        }
81        Node::Lam(t, b) => {
82            open(out);
83            out.push_str(&format!("fun (x{depth} : "));
84            go(k, t, depth, out, budget, false);
85            out.push_str(") => ");
86            go(k, b, depth + 1, out, budget, false);
87            close(out);
88        }
89        Node::Pi(t, b) => {
90            open(out);
91            if k.s.loose_bvar_range(b) == 0 {
92                go(k, t, depth, out, budget, true);
93                out.push_str(" → ");
94            } else {
95                out.push_str(&format!("(x{depth} : "));
96                go(k, t, depth, out, budget, false);
97                out.push_str(") → ");
98            }
99            go(k, b, depth + 1, out, budget, false);
100            close(out);
101        }
102        Node::Let(t, v, b) => {
103            open(out);
104            out.push_str(&format!("let x{depth} : "));
105            go(k, t, depth, out, budget, false);
106            out.push_str(" := ");
107            go(k, v, depth, out, budget, false);
108            out.push_str("; ");
109            go(k, b, depth + 1, out, budget, false);
110            close(out);
111        }
112        Node::NatLit(n) => out.push_str(&k.s.nat(n).to_decimal()),
113        Node::StrLit(s) => out.push_str(&format!("{:?}", &*k.s.string(s))),
114        Node::Proj(_, i, x) => {
115            go(k, x, depth, out, budget, true);
116            out.push_str(&format!(".{}", i + 1));
117        }
118        Node::Lit(l) => out.push_str(&match k.s.lit_value(l) {
119            Lit::Int(i) => i.to_string(),
120            Lit::BigInt(b) => b.to_string(),
121            Lit::Float(bits) => format!("{:?}", f64::from_bits(*bits)),
122            Lit::Duration(d) => format!("{d}ns"),
123            Lit::Date(d) => format!("date({d})"),
124            Lit::Moment(m) => format!("moment({m})"),
125        }),
126        Node::Match(d, m, cs) => {
127            open(out);
128            out.push_str("match ");
129            go(k, d, depth, out, budget, true);
130            out.push_str(" return ");
131            go(k, m, depth, out, budget, true);
132            out.push_str(" with");
133            for c in k.s.seq_items(cs) {
134                out.push_str(" | ");
135                go(k, c, depth, out, budget, false);
136            }
137            out.push_str(" end");
138            close(out);
139        }
140        Node::Fix(b) => {
141            open(out);
142            out.push_str(&format!("fix x{depth} => "));
143            go(k, b, depth + 1, out, budget, false);
144            close(out);
145        }
146        Node::MutualFix(ds, i) => {
147            open(out);
148            let ds = k.s.seq_items(ds);
149            let n = ds.len() as u32;
150            out.push_str("fix");
151            for (j, b) in ds.iter().enumerate() {
152                out.push_str(&format!(
153                    " {}x{} => ",
154                    if j == 0 { "" } else { "with " },
155                    depth + j as u32
156                ));
157                go(k, *b, depth + n, out, budget, false);
158            }
159            out.push_str(&format!(" return x{}", depth + i));
160            close(out);
161        }
162        Node::Seq(..) | Node::Nil => out.push_str("⟨sequence⟩"),
163    }
164}
logicaffeine_kernel/dag/pretty.rs

logicaffeine_kernel/dag/
pretty.rs
