MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
dump.cpp
Go to the documentation of this file.
1#include <fstream>
2
3#include <fe/assert.h>
4
5#include "mim/driver.h"
6#include "mim/nest.h"
7
8#include "mim/ast/tok.h"
9#include "mim/util/util.h"
10
11using namespace std::literals;
12
13// During dumping, we classify Defs according to the following logic:
14// * Inline: These Defs are *always* displayed with all of its operands "inline".
15// E.g.: (1, 2, 3).
16// * All other Defs are referenced by its name/unique_name (see id) when they appear as an operand.
17// * Mutables are either classifed as "decl" (see isa_decl).
18// In this case, recursing through the Defs' operands stops and this particular Decl is dumped as its own thing.
19// * Or - if they are not a "decl" - they are basicallally handled like immutables.
20
21namespace mim {
22
23namespace {
24
25Def* isa_decl(const Def* def) {
26 if (auto mut = def->isa_mut()) {
27 if (mut->is_external() || mut->isa<Lam>() || (mut->sym() && mut->sym() != '_')) return mut;
28 }
29 return nullptr;
30}
31
32std::string id(const Def* def) {
33 if (def->is_external() || (!def->is_set() && def->isa<Lam>())) return def->sym().str();
34 return def->unique_name();
35}
36
37std::string_view external(const Def* def) {
38 if (def->is_external()) return "extern "sv;
39 return ""sv;
40}
41
42/*
43 * Inline + LRPrec
44 */
45
46/// This is a wrapper to dump a Def "inline" and print it with all of its operands.
47struct Inline {
48 Inline(const Def* def, int dump_gid)
49 : def_(def)
50 , dump_gid_(dump_gid) {}
51 Inline(const Def* def)
52 : Inline(def, def->world().flags().dump_gid) {}
53
54 const Def* operator->() const { return def_; }
55 const Def* operator*() const { return def_; }
56 explicit operator bool() const {
57 if (auto mut = def_->isa_mut()) {
58 if (isa_decl(mut)) return false;
59 return true;
60 }
61
62 if (def_->is_closed()) return true;
63
64 if (auto app = def_->isa<App>()) {
65 if (app->type()->isa<Pi>()) return true; // curried apps are printed inline
66 if (app->type()->isa<Type>()) return true;
67 if (app->callee()->isa<Axm>()) return app->callee_type()->num_doms() <= 1;
68 return false;
69 }
70
71 return true;
72 }
73
74private:
75 const Def* def_;
76 const int dump_gid_;
77
78 friend std::ostream& operator<<(std::ostream&, Inline);
79};
80
81#define MY_PREC(m) \
82 /* left prec, right */ \
83 m(Nil, Bot, Nil) m(Nil, Nil, Nil) m(Lam, Arrow, Arrow) m(Nil, Lam, Pi) m(Nil, Pi, App) m(App, App, Extract) \
84 m(Extract, Extract, Lit) m(Nil, Lit, Lit)
85
86enum class MyPrec {
87#define CODE(l, p, r) p,
89#undef CODE
90};
91
92static constexpr std::array<MyPrec, 2> my_prec(MyPrec p) {
93 switch (p) {
94#define CODE(l, p, r) \
95 case MyPrec::p: return {MyPrec::l, MyPrec::r};
96 default: fe::unreachable(); MY_PREC(CODE)
97#undef CODE
98 }
99}
100
101// clang-format off
102MyPrec my_prec(const Def* def) {
103 if (def->isa<Pi >()) return MyPrec::Arrow;
104 if (def->isa<App >()) return MyPrec::App;
105 if (def->isa<Extract>()) return MyPrec::Extract;
106 if (def->isa<Lit >()) return MyPrec::Lit;
107 return MyPrec::Bot;
108}
109// clang-format on
110
111// TODO prec is currently broken
112template<bool L>
113struct LRPrec {
114 LRPrec(const Def* l, const Def* r)
115 : l(l)
116 , r(r) {}
117
118private:
119 const Def* l;
120 const Def* r;
121
122 friend std::ostream& operator<<(std::ostream& os, const LRPrec& p) {
123 if constexpr (L) {
124 if (Inline(p.l) && my_prec(my_prec(p.r))[0] > my_prec(p.r)) return print(os, "({})", p.l);
125 return print(os, "{}", p.l);
126 } else {
127 if (Inline(p.r) && my_prec(p.l) > my_prec(my_prec(p.l))[1]) return print(os, "({})", p.r);
128 return print(os, "{}", p.r);
129 }
130 }
131};
132
133using LPrec = LRPrec<true>;
134using RPrec = LRPrec<false>;
135
136std::ostream& operator<<(std::ostream& os, Inline u) {
137 if (u.dump_gid_ == 2 || (u.dump_gid_ == 1 && !u->isa<Var>() && u->num_ops() != 0)) print(os, "/*{}*/", u->gid());
138 if (auto mut = u->isa_mut(); mut && !mut->is_set()) return os << "unset";
139
140 bool ascii = u->world().flags().ascii;
141 auto arw = ascii ? "->" : "→";
142 auto al = ascii ? "<<" : "«";
143 auto ar = ascii ? ">>" : "»";
144 auto pl = ascii ? "(<" : "‹";
145 auto pr = ascii ? ">)" : "›";
146
147 if (auto type = u->isa<Type>()) {
148 if (auto level = Lit::isa(type->level()); level && !ascii) {
149 if (level == 0) return print(os, "★");
150 if (level == 1) return print(os, "□");
151 }
152 return print(os, "(Type {})", type->level());
153 } else if (u->isa<Nat>()) {
154 return print(os, "Nat");
155 } else if (u->isa<Idx>()) {
156 return print(os, "Idx");
157 } else if (auto ext = u->isa<Ext>()) {
158 auto x = ext->isa<Bot>() ? (ascii ? ".bot" : "⊥") : (ascii ? ".top" : "⊤");
159 if (ext->type()->isa<Nat>()) return print(os, "{}:{}", x, ext->type());
160 return print(os, "{}:({})", x, ext->type());
161 } else if (auto top = u->isa<Top>()) {
162 return print(os, "{}:({})", ascii ? ".top" : "⊤", top->type());
163 } else if (auto axm = u->isa<Axm>()) {
164 const auto name = axm->sym();
165 return print(os, "{}{}", name[0] == '%' ? "" : "%", name);
166 } else if (auto lit = u->isa<Lit>()) {
167 if (lit->type()->isa<Nat>()) {
168 switch (lit->get()) {
169 // clang-format off
170 case 0x0'0000'0100_n: return os << "i8";
171 case 0x0'0001'0000_n: return os << "i16";
172 case 0x1'0000'0000_n: return os << "i32";
173 // clang-format on
174 default: return print(os, "{}", lit->get());
175 }
176 } else if (auto size = Idx::isa(lit->type())) {
177 if (auto s = Lit::isa(size)) {
178 switch (*s) {
179 // clang-format off
180 case 0x0'0000'0002_n: return os << (lit->get<bool>() ? "tt" : "ff");
181 case 0x0'0000'0100_n: return os << lit->get() << "I8";
182 case 0x0'0001'0000_n: return os << lit->get() << "I16";
183 case 0x1'0000'0000_n: return os << lit->get() << "I32";
184 case 0_n: return os << lit->get() << "I64";
185 default: {
186 os << lit->get();
187 std::vector<uint8_t> digits;
188 for (auto z = *s; z; z /= 10) digits.emplace_back(z % 10);
189
190 if (ascii) {
191 os << '_';
192 for (auto d : digits | std::ranges::views::reverse)
193 os << char('0' + d);
194 } else {
195 for (auto d : digits | std::ranges::views::reverse)
196 os << uint8_t(0xE2) << uint8_t(0x82) << (uint8_t(0x80 + d));
197 }
198 return os;
199 }
200 // clang-format on
201 }
202 }
203 }
204 if (lit->type()->isa<App>()) return print(os, "{}:({})", lit->get(), lit->type()); // HACK prec magic is broken
205 return print(os, "{}:{}", lit->get(), lit->type());
206 } else if (auto ex = u->isa<Extract>()) {
207 if (ex->tuple()->isa<Var>() && ex->index()->isa<Lit>()) return print(os, "{}", ex->unique_name());
208 return print(os, "{}#{}", ex->tuple(), ex->index());
209 } else if (auto var = u->isa<Var>()) {
210 return print(os, "{}", var->unique_name());
211 } else if (auto pi = u->isa<Pi>()) {
212 /*return os << "TODO";*/
213 if (Pi::isa_cn(pi)) return print(os, "Cn {}", pi->dom());
214 if (auto mut = pi->isa_mut<Pi>(); mut && mut->var())
215 return print(os, "Π {}: {} {} {}", mut->var(), pi->dom(), arw, pi->codom());
216 return print(os, "Π {} {} {}", pi->dom(), arw, pi->codom());
217 } else if (auto lam = u->isa<Lam>()) {
218 return print(os, "{}, {}", lam->filter(), lam->body());
219 } else if (auto app = u->isa<App>()) {
220 if (auto size = Idx::isa(app)) {
221 if (auto l = Lit::isa(size)) {
222 // clang-format off
223 switch (*l) {
224 case 0x0'0000'0002_n: return os << "Bool";
225 case 0x0'0000'0100_n: return os << "I8";
226 case 0x0'0001'0000_n: return os << "I16";
227 case 0x1'0000'0000_n: return os << "I32";
228 case 0_n: return os << "I64";
229 default: break;
230 }
231 // clang-format on
232 }
233 }
234 return print(os, "{} {}", LPrec(app->callee(), app), RPrec(app, app->arg()));
235 } else if (auto sigma = u->isa<Sigma>()) {
236 if (auto mut = sigma->isa_mut<Sigma>(); mut && mut->var()) {
237 size_t i = 0;
238 return print(os, "[{, }]", Elem(sigma->ops(), [&](auto op) {
239 if (auto v = mut->var(i++))
240 print(os, "{}: {}", v, op);
241 else
242 os << op;
243 }));
244 }
245 return print(os, "[{, }]", sigma->ops());
246 } else if (auto tuple = u->isa<Tuple>()) {
247 print(os, "({, })", tuple->ops());
248 return tuple->type()->isa_mut() ? print(os, ":{}", tuple->type()) : os;
249 } else if (auto arr = u->isa<Arr>()) {
250 if (auto mut = arr->isa_mut<Arr>(); mut && mut->var())
251 return print(os, "{}{}: {}; {}{}", al, mut->var(), mut->arity(), mut->body(), ar);
252 return print(os, "{}{}; {}{}", al, arr->arity(), arr->body(), ar);
253 } else if (auto pack = u->isa<Pack>()) {
254 if (auto mut = pack->isa_mut<Pack>(); mut && mut->var())
255 return print(os, "{}{}: {}; {}{}", pl, mut->var(), mut->arity(), mut->body(), pr);
256 return print(os, "{}{}; {}{}", pl, pack->arity(), pack->body(), pr);
257 } else if (auto proxy = u->isa<Proxy>()) {
258 return print(os, ".proxy#{}#{} {, }", proxy->pass(), proxy->tag(), proxy->ops());
259 } else if (auto bound = u->isa<Bound>()) {
260 auto op = bound->isa<Join>() ? "∪" : "∩"; // TODO ascii
261 if (auto mut = u->isa_mut()) print(os, "{}{}: {}", op, mut->unique_name(), mut->type());
262 return print(os, "{}({, })", op, bound->ops());
263 }
264
265 // other
266 if (u->flags() == 0) return print(os, "(.{} {, })", u->node_name(), u->ops());
267 return print(os, "(.{}#{} {, })", u->node_name(), u->flags(), u->ops());
268}
269
270/*
271 * Dumper
272 */
273
274/// This thing operates in two modes:
275/// 1. The output of decls is driven by the Nest.
276/// 2. Alternatively, decls are output as soon as they appear somewhere during recurse%ing.
277/// Then, they are pushed to Dumper::muts.
278class Dumper {
279public:
280 Dumper(std::ostream& os, const Nest* nest = nullptr)
281 : os(os)
282 , nest(nest) {}
283
284 void dump(Def*);
285 void dump(Lam*);
286 void dump_let(const Def*);
287 void dump_ptrn(const Def*, const Def*);
288 void recurse(const Nest::Node*);
289 void recurse(const Def*, bool first = false);
290
291 std::ostream& os;
292 const Nest* nest;
293 Tab tab;
294 unique_queue<MutSet> muts;
295 DefSet defs;
296};
297
298void Dumper::dump(Def* mut) {
299 if (auto lam = mut->isa<Lam>()) {
300 dump(lam);
301 return;
302 }
303
304 auto mut_prefix = [&](const Def* def) {
305 if (def->isa<Sigma>()) return "Sigma";
306 if (def->isa<Arr>()) return "Arr";
307 if (def->isa<Pack>()) return "pack";
308 if (def->isa<Pi>()) return "Pi";
309 if (def->isa<Hole>()) return "Hole";
310 if (def->isa<Rule>()) return "Rule";
311 fe::unreachable();
312 };
313
314 auto mut_op0 = [&](const Def* def) -> std::ostream& {
315 if (auto sig = def->isa<Sigma>()) return print(os, ", {}", sig->num_ops());
316 if (auto arr = def->isa<Arr>()) return print(os, ", {}", arr->arity());
317 if (auto pack = def->isa<Pack>()) return print(os, ", {}", pack->arity());
318 if (auto pi = def->isa<Pi>()) return print(os, ", {}", pi->dom());
319 if (auto hole = def->isa_mut<Hole>()) return hole->is_set() ? print(os, ", {}", hole->op()) : print(os, ", ??");
320 if (auto rule = def->isa<Rule>()) return print(os, "{} => {}", rule->lhs(), rule->rhs());
321 fe::unreachable();
322 };
323
324 if (!mut->is_set()) {
325 tab.print(os, "{}: {} = {{ <unset> }};", id(mut), mut->type());
326 return;
327 }
328
329 tab.print(os, "{} {}{}: {}", mut_prefix(mut), external(mut), id(mut), mut->type());
330 mut_op0(mut);
331 if (mut->var()) { // TODO rewrite with dedicated methods
332 if (auto e = mut->num_vars(); e != 1) {
333 print(os, "{, }", Elem(mut->vars(), [&](auto def) {
334 if (def)
335 os << def->unique_name();
336 else
337 os << "<TODO>";
338 }));
339 } else {
340 print(os, ", @{}", mut->var()->unique_name());
341 }
342 }
343 tab.println(os, " = {{");
344 ++tab;
345 if (nest) recurse(nest->mut2node(mut));
346 recurse(mut);
347 tab.print(os, "{, }\n", mut->ops());
348 --tab;
349 tab.print(os, "}};\n");
350}
351
352void Dumper::dump(Lam* lam) {
353 // TODO filter
354 auto ptrn = [&](auto&) { dump_ptrn(lam->var(), lam->type()->dom()); };
355
356 if (Lam::isa_cn(lam))
357 tab.println(os, "con {}{} {}@({}) = {{", external(lam), id(lam), ptrn, lam->filter());
358 else
359 tab.println(os, "lam {}{} {}: {} = {{", external(lam), id(lam), ptrn, lam->type()->codom());
360
361 ++tab;
362 if (lam->is_set()) {
363 if (nest) recurse(nest->mut2node(lam));
364 recurse(lam->filter());
365 recurse(lam->body(), true);
366 if (lam->body()->isa_mut())
367 tab.print(os, "{}\n", lam->body());
368 else
369 tab.print(os, "{}\n", Inline(lam->body()));
370 } else {
371 tab.print(os, " <unset>\n");
372 }
373 --tab;
374 tab.print(os, "}};\n");
375}
376
377void Dumper::dump_let(const Def* def) {
378 tab.print(os, "let {}: {} = {};\n", def->unique_name(), def->type(), Inline(def, 0));
379}
380
381void Dumper::dump_ptrn(const Def* def, const Def* type) {
382 if (!def) {
383 os << type;
384 } else {
385 auto projs = def->tprojs();
386 if (projs.size() == 1 || std::ranges::all_of(projs, [](auto def) { return !def; })) {
387 print(os, "{}: {}", def->unique_name(), type);
388 } else {
389 size_t i = 0;
390 print(os, "{}::[{, }]", def->unique_name(),
391 Elem(projs, [&](auto proj) { dump_ptrn(proj, type->proj(i++)); }));
392 }
393 }
394}
395
396void Dumper::recurse(const Nest::Node* node) {
397 for (auto child : node->child_muts())
398 if (auto mut = isa_decl(child)) dump(mut);
399}
400
401void Dumper::recurse(const Def* def, bool first /*= false*/) {
402 if (auto mut = isa_decl(def)) {
403 if (!nest) muts.push(mut);
404 return;
405 }
406
407 if (!defs.emplace(def).second) return;
408
409 for (auto op : def->deps())
410 recurse(op);
411
412 if (!first && !Inline(def)) dump_let(def);
413}
414
415} // namespace
416
417/*
418 * Def
419 */
420
421/// This will stream @p def as an operand.
422/// This is usually `id(def)` unless it can be displayed Inline.
423std::ostream& operator<<(std::ostream& os, const Def* def) {
424 if (def == nullptr) return os << "<nullptr>";
425 if (Inline(def)) {
426 auto freezer = World::Freezer(def->world());
427 return os << Inline(def);
428 }
429 return os << id(def);
430}
431
432std::ostream& Def::stream(std::ostream& os, int max) const {
433 auto freezer = World::Freezer(world());
434 auto dumper = Dumper(os);
435
436 if (max == 0) {
437 os << this << std::endl;
438 } else if (auto mut = isa_decl(this)) {
439 dumper.muts.push(mut);
440 } else {
441 dumper.recurse(this);
442 dumper.tab.print(os, "{}\n", Inline(this));
443 --max;
444 }
445
446 for (; !dumper.muts.empty() && max > 0; --max)
447 dumper.dump(dumper.muts.pop());
448
449 return os;
450}
451
452void Def::dump() const { std::cout << this << std::endl; }
453void Def::dump(int max) const { stream(std::cout, max) << std::endl; }
454
455void Def::write(int max, const char* file) const {
456 auto ofs = std::ofstream(file);
457 stream(ofs, max);
458}
459
460void Def::write(int max) const {
461 auto file = id(this) + ".mim"s;
462 write(max, file.c_str());
463}
464
465/*
466 * World
467 */
468
469void World::dump(std::ostream& os) {
470 auto freezer = World::Freezer(*this);
471 auto old_gid = curr_gid();
472
473 if (flags().dump_recursive) {
474 auto dumper = Dumper(os);
475 for (auto mut : externals())
476 dumper.muts.push(mut);
477 while (!dumper.muts.empty())
478 dumper.dump(dumper.muts.pop());
479 } else {
480 auto nest = Nest(*this);
481 auto dumper = Dumper(os, &nest);
482
483 for (auto name : driver().import_syms())
484 print(os, ".{} {};\n", driver().is_loaded(name) ? "mim/plugin" : "import", name);
485 dumper.recurse(nest.root());
486 }
487
488 assertf(old_gid == curr_gid(), "new nodes created during dump. old_gid: {}; curr_gid: {}", old_gid, curr_gid());
489}
490
491void World::dump() { dump(std::cout); }
492
494 if (log().level() == Log::Level::Debug) dump(log().ostream());
495}
496
497void World::write(const char* file) {
498 auto ofs = std::ofstream(file);
499 dump(ofs);
500}
501
503 auto file = name().str() + ".mim"s;
504 write(file.c_str());
505}
506
507} // namespace mim
A (possibly paramterized) Array.
Definition tuple.h:117
Definition axm.h:9
Common base for TBound.
Definition lattice.h:13
Base class for all Defs.
Definition def.h:251
void dump() const
Definition dump.cpp:452
World & world() const noexcept
Definition def.cpp:436
const Def * var(nat_t a, nat_t i) noexcept
Definition def.h:429
void write(int max) const
Definition dump.cpp:460
std::ostream & stream(std::ostream &, int max) const
Definition dump.cpp:432
Common base for TExtremum.
Definition lattice.h:144
Extracts from a Sigma or Array-typed Extract::tuple the element at position Extract::index.
Definition tuple.h:206
A built-in constant of type Nat -> *.
Definition def.h:845
static const Def * isa(const Def *def)
Checks if def is a Idx s and returns s or nullptr otherwise.
Definition def.cpp:605
A function.
Definition lam.h:111
static std::optional< T > isa(const Def *def)
Definition def.h:810
Builds a nesting tree of all immutables‍/binders.
Definition nest.h:11
const auto & mut2node() const
Definition nest.h:141
A (possibly paramterized) Tuple.
Definition tuple.h:166
A dependent function type.
Definition lam.h:15
static const Pi * isa_cn(const Def *d)
Is this a continuation - i.e. is the Pi::codom mim::Bottom?
Definition lam.h:48
A dependent tuple type.
Definition tuple.h:20
std::ostream & println(std::ostream &os, const char *s, Args &&... args)
Same as Tab::print but appends a std::endl to os.
Definition print.h:235
std::ostream & print(std::ostream &os, const char *s, Args &&... args)
Definition print.h:223
Data constructor for a Sigma.
Definition tuple.h:68
const Driver & driver() const
Definition world.h:91
u32 curr_gid() const
Manage global identifier - a unique number for each Def.
Definition world.h:99
Sym name() const
Definition world.h:94
void dump()
Dump to std::cout.
Definition dump.cpp:491
void write()
Same above but file name defaults to World::name.
Definition dump.cpp:502
Flags & flags()
Retrieve compile Flags.
Definition world.cpp:72
void debug_dump()
Dump in Debug build if World::log::level is Log::Level::Debug.
Definition dump.cpp:493
auto externals() const
Definition world.h:209
void write(const char *file)
Write to a file named file.
Definition dump.cpp:497
void dump(std::ostream &os)
Dump to os.
Definition dump.cpp:469
Log & log() const
Definition world.cpp:71
#define MY_PREC(m)
Definition dump.cpp:81
const Def * op(trait o, const Def *type)
Definition core.h:33
Definition ast.h:14
std::ostream & print(std::ostream &os, const char *s)
Base case.
Definition print.cpp:5
TBound< true > Join
AKA union.
Definition lattice.h:174
TExt< true > Top
Definition lattice.h:172
GIDSet< const Def * > DefSet
Definition def.h:74
std::ostream & operator<<(std::ostream &os, const Def *def)
This will stream def as an operand.
Definition dump.cpp:423
TExt< false > Bot
Definition lattice.h:171
@ Pi
Definition def.h:114
CODE(node, _)
Definition def.h:113
@ Lam
Definition def.h:114
@ Axm
Definition def.h:114
@ Type
Definition def.h:114
@ App
Definition def.h:114
#define assertf(condition,...)
Definition print.h:183
Use with print to output complicated std::ranges::ranges.
Definition print.h:85
Use to World::freeze and automatically unfreeze at the end of scope.
Definition world.h:151
#define CODE(t, str)
Definition tok.h:60