11using namespace std::literals;
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;
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();
37std::string_view external(
const Def* def) {
38 if (def->is_external())
return "extern "sv;
48 Inline(
const Def* def,
int dump_gid)
50 , dump_gid_(dump_gid) {}
51 Inline(
const Def* def)
52 : Inline(def, def->world().flags().dump_gid) {}
54 const Def* operator->()
const {
return def_; }
55 const Def* operator*()
const {
return def_; }
56 explicit operator bool()
const {
57 if (def_->dep_const())
return true;
59 if (
auto mut = def_->isa_mut()) {
60 if (isa_decl(mut))
return false;
64 if (
auto app = def_->isa<App>()) {
65 if (app->type()->isa<Pi>())
return true;
66 if (app->type()->isa<
Type>())
return true;
67 if (app->callee()->isa<
Axiom>())
return app->callee_type()->num_doms() <= 1;
78 friend std::ostream&
operator<<(std::ostream&, Inline);
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)
87#define CODE(l, p, r) p,
92static constexpr std::array<MyPrec, 2> my_prec(MyPrec p) {
94#define CODE(l, p, r) \
95 case MyPrec::p: return {MyPrec::l, MyPrec::r};
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;
112template<
bool L>
struct LRPrec {
113 LRPrec(
const Def* l,
const Def* r)
121 friend std::ostream&
operator<<(std::ostream& os,
const LRPrec& p) {
123 if (Inline(p.l) && my_prec(my_prec(p.r))[0] > my_prec(p.r))
return print(os,
"({})", p.l);
124 return print(os,
"{}", p.l);
126 if (Inline(p.r) && my_prec(p.l) > my_prec(my_prec(p.l))[1])
return print(os,
"({})", p.r);
127 return print(os,
"{}", p.r);
132using LPrec = LRPrec<true>;
133using RPrec = LRPrec<false>;
135std::ostream&
operator<<(std::ostream& os, Inline u) {
136 if (
u.dump_gid_ == 2 || (
u.dump_gid_ == 1 && !
u->isa<
Var>() &&
u->num_ops() != 0))
print(os,
"/*{}*/",
u->gid());
137 if (
auto mut =
u->isa_mut(); mut && !mut->is_set())
return os <<
"unset";
139 bool ascii =
u->world().flags().ascii;
140 auto arw = ascii ?
"->" :
"→";
141 auto al = ascii ?
"<<" :
"«";
142 auto ar = ascii ?
">>" :
"»";
143 auto pl = ascii ?
"(<" :
"‹";
144 auto pr = ascii ?
">)" :
"›";
146 if (
auto type =
u->isa<
Type>()) {
147 if (
auto level =
Lit::isa(type->level()); level && !ascii) {
148 if (level == 0)
return print(os,
"★");
149 if (level == 1)
return print(os,
"□");
151 return print(os,
"(Type {})", type->level());
152 }
else if (
u->isa<Nat>()) {
153 return print(os,
"Nat");
154 }
else if (
u->isa<Idx>()) {
155 return print(os,
"Idx");
156 }
else if (
auto ext =
u->isa<Ext>()) {
157 auto x = ext->isa<
Bot>() ? (ascii ?
".bot" :
"⊥") : (ascii ?
".top" :
"⊤");
158 if (ext->type()->isa<Nat>())
return print(os,
"{}:{}", x, ext->type());
159 return print(os,
"{}:({})", x, ext->type());
160 }
else if (
auto top =
u->isa<
Top>()) {
161 return print(os,
"{}:({})", ascii ?
".top" :
"⊤",
top->type());
162 }
else if (
auto axiom =
u->isa<
Axiom>()) {
163 const auto name = axiom->sym();
164 return print(os,
"{}{}", name[0] ==
'%' ?
"" :
"%", name);
165 }
else if (
auto lit =
u->isa<Lit>()) {
166 if (
lit->type()->isa<Nat>()) {
167 switch (
lit->get()) {
169 case 0x0'0000'0100_n:
return os <<
"i8";
170 case 0x0'0001'0000_n:
return os <<
"i16";
171 case 0x1'0000'0000_n:
return os <<
"i32";
173 default:
return print(os,
"{}",
lit->get());
179 case 0x0'0000'0002_n:
return os << (
lit->get<
bool>() ?
"tt" :
"ff");
180 case 0x0'0000'0100_n:
return os <<
lit->get() <<
"I8";
181 case 0x0'0001'0000_n:
return os <<
lit->get() <<
"I16";
182 case 0x1'0000'0000_n:
return os <<
lit->get() <<
"I32";
183 case 0_n:
return os <<
lit->get() <<
"I64";
186 std::vector<uint8_t> digits;
187 for (
auto z = *s; z; z /= 10) digits.emplace_back(z % 10);
191 for (
auto d : digits | std::ranges::views::reverse)
194 for (
auto d : digits | std::ranges::views::reverse)
195 os << uint8_t(0xE2) << uint8_t(0x82) << (uint8_t(0x80 + d));
203 if (
lit->type()->isa<App>())
return print(os,
"{}:({})",
lit->get(),
lit->type());
204 return print(os,
"{}:{}",
lit->get(),
lit->type());
205 }
else if (
auto ex =
u->isa<Extract>()) {
206 if (ex->tuple()->isa<
Var>() && ex->index()->isa<Lit>())
return print(os,
"{}", ex->unique_name());
207 return print(os,
"{}#{}", ex->tuple(), ex->index());
208 }
else if (
auto var =
u->isa<
Var>()) {
209 return print(os,
"{}", var->unique_name());
210 }
else if (
auto pi =
u->isa<Pi>()) {
213 if (
auto mut = pi->isa_mut<Pi>(); mut && mut->var())
214 return print(os,
"Π {}: {} {} {}", mut->var(), pi->dom(), arw, pi->codom());
215 return print(os,
"Π {} {} {}", pi->dom(), arw, pi->codom());
216 }
else if (
auto lam =
u->isa<Lam>()) {
217 return print(os,
"{}, {}", lam->filter(), lam->body());
218 }
else if (
auto app =
u->isa<App>()) {
223 case 0x0'0000'0002_n:
return os <<
"Bool";
224 case 0x0'0000'0100_n:
return os <<
"I8";
225 case 0x0'0001'0000_n:
return os <<
"I16";
226 case 0x1'0000'0000_n:
return os <<
"I32";
227 case 0_n:
return os <<
"I64";
233 return print(os,
"{} {}", LPrec(app->callee(), app), RPrec(app, app->arg()));
234 }
else if (
auto sigma =
u->isa<Sigma>()) {
235 if (
auto mut = sigma->isa_mut<Sigma>(); mut && mut->var()) {
237 return print(os,
"[{, }]", Elem(sigma->ops(), [&](
auto op) {
238 if (auto v = mut->var(i++))
239 print(os,
"{}: {}", v, op);
244 return print(os,
"[{, }]", sigma->ops());
245 }
else if (
auto tuple =
u->isa<Tuple>()) {
246 print(os,
"({, })", tuple->ops());
247 return tuple->type()->isa_mut() ?
print(os,
":{}", tuple->type()) : os;
248 }
else if (
auto arr =
u->isa<Arr>()) {
249 if (
auto mut = arr->isa_mut<Arr>(); mut && mut->var())
250 return print(os,
"{}{}: {}; {}{}", al, mut->var(), mut->shape(), mut->body(), ar);
251 return print(os,
"{}{}; {}{}", al, arr->shape(), arr->body(), ar);
252 }
else if (
auto pack =
u->isa<Pack>()) {
253 if (
auto mut = pack->isa_mut<Pack>(); mut && mut->var())
254 return print(os,
"{}{}: {}; {}{}", pl, mut->var(), mut->shape(), mut->body(), pr);
255 return print(os,
"{}{}; {}{}", pl, pack->shape(), pack->body(), pr);
256 }
else if (
auto proxy =
u->isa<
Proxy>()) {
257 return print(os,
".proxy#{}#{} {, }", proxy->pass(), proxy->tag(), proxy->ops());
258 }
else if (
auto bound =
u->isa<Bound>()) {
259 auto op = bound->isa<
Join>() ?
"∪" :
"∩";
260 if (
auto mut =
u->isa_mut())
print(os,
"{}{}: {}", op, mut->unique_name(), mut->type());
261 return print(os,
"{}({, })", op, bound->ops());
265 if (
u->flags() == 0)
return print(os,
"(.{} {, })",
u->node_name(),
u->ops());
266 return print(os,
"(.{}#{} {, })",
u->node_name(),
u->flags(),
u->ops());
279 Dumper(std::ostream& os,
const DepTree* dep =
nullptr)
285 void dump_let(
const Def*);
286 void dump_ptrn(
const Def*,
const Def*);
287 void recurse(
const DepNode*);
288 void recurse(
const Def*,
bool first =
false);
293 unique_queue<MutSet> muts;
297void Dumper::dump(Def* mut) {
298 if (
auto lam = mut->isa<Lam>()) {
303 auto mut_prefix = [&](
const Def* def) {
304 if (def->isa<Sigma>())
return "Sigma";
305 if (def->isa<Arr>())
return ".Arr";
306 if (def->isa<Pack>())
return ".pack";
307 if (def->isa<Pi>())
return ".Pi";
311 auto mut_op0 = [&](
const Def* def) -> std::ostream& {
312 if (
auto sig = def->isa<Sigma>())
return print(os,
", {}", sig->num_ops());
313 if (
auto arr = def->isa<Arr>())
return print(os,
", {}", arr->shape());
314 if (
auto pack = def->isa<Pack>())
return print(os,
", {}", pack->shape());
315 if (
auto pi = def->isa<Pi>())
return print(os,
", {}", pi->dom());
319 if (!mut->is_set()) {
320 tab.
print(os,
"{}: {} = {{ <unset> }};",
id(mut), mut->type());
324 tab.
print(os,
"{} {}{}: {}", mut_prefix(mut), external(mut),
id(mut), mut->type());
327 if (
auto e = mut->num_vars(); e != 1) {
328 print(os,
"{, }", Elem(mut->vars(), [&](
auto def) {
330 os << def->unique_name();
335 print(os,
", @{}", mut->var()->unique_name());
340 if (dep) recurse(dep->
mut2node(mut));
342 tab.
print(os,
"{, }\n", mut->ops());
344 tab.
print(os,
"}};\n");
347void Dumper::dump(Lam* lam) {
349 auto ptrn = [&](
auto&) { dump_ptrn(lam->var(), lam->type()->dom()); };
351 if (Lam::isa_cn(lam))
352 tab.
println(os,
"con {}{} {}@({}) = {{", external(lam),
id(lam), ptrn, lam->filter());
354 tab.
println(os,
"lam {}{} {}: {} = {{", external(lam),
id(lam), ptrn, lam->type()->codom());
358 if (dep) recurse(dep->
mut2node(lam));
359 recurse(lam->filter());
360 recurse(lam->body(),
true);
361 if (lam->body()->isa_mut())
362 tab.
print(os,
"{}\n", lam->body());
364 tab.
print(os,
"{}\n", Inline(lam->body()));
366 tab.
print(os,
" <unset>\n");
369 tab.
print(os,
"}};\n");
372void Dumper::dump_let(
const Def* def) {
373 tab.
print(os,
"let {}: {} = {};\n", def->unique_name(), def->type(), Inline(def, 0));
376void Dumper::dump_ptrn(
const Def* def,
const Def* type) {
380 auto projs = def->tprojs();
381 if (projs.size() == 1 || std::ranges::all_of(projs, [](
auto def) { return !def; })) {
382 print(os,
"{}: {}", def->unique_name(), type);
385 print(os,
"{}::[{, }]", def->unique_name(),
386 Elem(projs, [&](
auto proj) { dump_ptrn(proj, type->proj(i++)); }));
391void Dumper::recurse(
const DepNode* node) {
392 for (
auto child : node->children())
393 if (
auto mut = isa_decl(child->mut())) dump(mut);
396void Dumper::recurse(
const Def* def,
bool first ) {
397 if (
auto mut = isa_decl(def)) {
398 if (!dep) muts.push(mut);
402 if (!defs.emplace(def).second)
return;
404 for (
auto op : def->partial_ops()) {
409 if (!first && !Inline(def)) dump_let(def);
423 if (def ==
nullptr)
return os <<
"<nullptr>";
426 return os << Inline(def);
428 return os << id(def);
433 auto dumper = Dumper(os);
436 os <<
this << std::endl;
437 }
else if (
auto mut = isa_decl(
this)) {
438 dumper.muts.push(mut);
440 dumper.recurse(
this);
441 dumper.tab.print(os,
"{}\n", Inline(
this));
445 for (; !dumper.muts.empty() && max > 0; --max) dumper.dump(dumper.muts.pop());
450void Def::dump()
const { std::cout <<
this << std::endl; }
451void Def::dump(
int max)
const { stream(std::cout, max) << std::endl; }
454 auto ofs = std::ofstream(file);
459 auto file = id(
this) +
".mim"s;
460 write(max, file.c_str());
469 auto old_gid = curr_gid();
471 if (flags().dump_recursive) {
472 auto dumper = Dumper(os);
473 for (
const auto& [_, mut] : externals()) dumper.muts.push(mut);
474 while (!dumper.muts.empty()) dumper.dump(dumper.muts.pop());
477 auto dumper = Dumper(os, &dep);
479 for (
auto [_, name] : driver().imports())
480 print(os,
".{} {};\n", driver().is_loaded(name) ?
"mim/plugin" :
"import", name);
481 dumper.recurse(dep.root());
484 assertf(old_gid == curr_gid(),
"new nodes created during dump. old_gid: {}; curr_gid: {}", old_gid, curr_gid());
494 auto ofs = std::ofstream(file);
499 auto file = name().str() +
".mim"s;
void write(int max) const
std::ostream & stream(std::ostream &, int max) const
const DepNode * mut2node(Def *mut) const
static Ref size(Ref def)
Checks if def is a Idx s and returns s or nullptr otherwise.
static std::optional< T > isa(Ref def)
static const Pi * isa_cn(Ref d)
Is this a continuation - i.e. is the Pi::codom mim::Bottom?
Helper class to retrieve Infer::arg if present.
std::ostream & println(std::ostream &os, const char *s, Args &&... args)
Same as Tab::print but appends a std::endl to os.
std::ostream & print(std::ostream &os, const char *s, Args &&... args)
void dump()
Dump to std::cout.
void write()
Same above but file name defaults to World::name.
void debug_dump()
Dump in Debug build if World::log::level is Log::Level::Debug.
Ref op(trait o, Ref type)
std::ostream & print(std::ostream &os, const char *s)
Base case.
GIDSet< const Def * > DefSet
std::ostream & operator<<(std::ostream &, const CFNode *)
#define assertf(condition,...)
Use to World::freeze and automatically unfreeze at the end of scope.