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 (
auto mut = def_->isa_mut()) {
58 if (isa_decl(mut))
return false;
62 if (def_->is_closed())
return true;
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<
Axm>())
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;
114 LRPrec(
const Def* l,
const Def* r)
122 friend std::ostream&
operator<<(std::ostream& os,
const LRPrec& p) {
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);
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);
133using LPrec = LRPrec<true>;
134using RPrec = LRPrec<false>;
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";
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 ?
">)" :
"›";
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,
"□");
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()) {
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";
174 default:
return print(os,
"{}",
lit->get());
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";
187 std::vector<uint8_t> digits;
188 for (
auto z = *s; z; z /= 10) digits.emplace_back(z % 10);
192 for (
auto d : digits | std::ranges::views::reverse)
195 for (
auto d : digits | std::ranges::views::reverse)
196 os << uint8_t(0xE2) << uint8_t(0x82) << (uint8_t(0x80 + d));
204 if (
lit->type()->isa<
App>())
return print(os,
"{}:({})",
lit->get(),
lit->type());
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>()) {
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>()) {
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";
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()) {
238 return print(os,
"[{, }]",
Elem(sigma->ops(), [&](
auto op) {
239 if (auto v = mut->var(i++))
240 print(os,
"{}: {}", v, op);
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>() ?
"∪" :
"∩";
261 if (
auto mut =
u->isa_mut())
print(os,
"{}{}: {}", op, mut->unique_name(), mut->type());
262 return print(os,
"{}({, })", op, bound->ops());
266 if (
u->flags() == 0)
return print(os,
"(.{} {, })",
u->node_name(),
u->ops());
267 return print(os,
"(.{}#{} {, })",
u->node_name(),
u->flags(),
u->ops());
280 Dumper(std::ostream& os,
const Nest* nest =
nullptr)
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);
294 unique_queue<MutSet> muts;
298void Dumper::dump(
Def* mut) {
299 if (
auto lam = mut->isa<Lam>()) {
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";
313 auto mut_op0 = [&](
const Def* def) -> std::ostream& {
314 if (
auto sig = def->isa<Sigma>())
return print(os,
", {}", sig->num_ops());
315 if (
auto arr = def->isa<Arr>())
return print(os,
", {}", arr->arity());
316 if (
auto pack = def->isa<Pack>())
return print(os,
", {}", pack->arity());
317 if (
auto pi = def->isa<Pi>())
return print(os,
", {}", pi->dom());
318 if (
auto hole = def->isa_mut<Hole>())
return hole->is_set() ?
print(os,
", {}", hole->op()) :
print(os,
", ??");
322 if (!mut->is_set()) {
323 tab.
print(os,
"{}: {} = {{ <unset> }};",
id(mut), mut->type());
327 tab.
print(os,
"{} {}{}: {}", mut_prefix(mut), external(mut),
id(mut), mut->type());
330 if (
auto e = mut->num_vars(); e != 1) {
331 print(os,
"{, }", Elem(mut->vars(), [&](
auto def) {
333 os << def->unique_name();
338 print(os,
", @{}", mut->var()->unique_name());
343 if (nest) recurse(nest->
mut2node(mut));
345 tab.
print(os,
"{, }\n", mut->ops());
347 tab.
print(os,
"}};\n");
350void Dumper::dump(
Lam* lam) {
352 auto ptrn = [&](
auto&) { dump_ptrn(lam->var(), lam->type()->dom()); };
354 if (Lam::isa_cn(lam))
355 tab.
println(os,
"con {}{} {}@({}) = {{", external(lam),
id(lam), ptrn, lam->filter());
357 tab.
println(os,
"lam {}{} {}: {} = {{", external(lam),
id(lam), ptrn, lam->type()->codom());
361 if (nest) recurse(nest->
mut2node(lam));
362 recurse(lam->filter());
363 recurse(lam->body(),
true);
364 if (lam->body()->isa_mut())
365 tab.
print(os,
"{}\n", lam->body());
367 tab.
print(os,
"{}\n", Inline(lam->body()));
369 tab.
print(os,
" <unset>\n");
372 tab.
print(os,
"}};\n");
375void Dumper::dump_let(
const Def* def) {
376 tab.
print(os,
"let {}: {} = {};\n", def->unique_name(), def->type(), Inline(def, 0));
379void Dumper::dump_ptrn(
const Def* def,
const Def* type) {
383 auto projs = def->tprojs();
384 if (projs.size() == 1 || std::ranges::all_of(projs, [](
auto def) { return !def; })) {
385 print(os,
"{}: {}", def->unique_name(), type);
388 print(os,
"{}::[{, }]", def->unique_name(),
389 Elem(projs, [&](
auto proj) { dump_ptrn(proj,
type->proj(i++)); }));
394void Dumper::recurse(
const Nest::Node* node) {
395 for (
auto child : node->child_muts())
396 if (
auto mut = isa_decl(child)) dump(mut);
399void Dumper::recurse(
const Def* def,
bool first ) {
400 if (
auto mut = isa_decl(def)) {
401 if (!nest) muts.push(mut);
405 if (!defs.emplace(def).second)
return;
407 for (
auto op : def->deps())
410 if (!first && !Inline(def)) dump_let(def);
422 if (def ==
nullptr)
return os <<
"<nullptr>";
425 return os << Inline(def);
427 return os << id(def);
432 auto dumper = Dumper(os);
435 os <<
this << std::endl;
436 }
else if (
auto mut = isa_decl(
this)) {
437 dumper.muts.push(mut);
439 dumper.recurse(
this);
440 dumper.tab.print(os,
"{}\n", Inline(
this));
444 for (; !dumper.muts.empty() && max > 0; --max)
445 dumper.dump(dumper.muts.pop());
450void Def::dump()
const { std::cout <<
this << std::endl; }
454 auto ofs = std::ofstream(file);
459 auto file = id(
this) +
".mim"s;
460 write(max, file.c_str());
471 if (
flags().dump_recursive) {
472 auto dumper = Dumper(os);
474 dumper.muts.push(mut);
475 while (!dumper.muts.empty())
476 dumper.dump(dumper.muts.pop());
478 auto nest =
Nest(*
this);
479 auto dumper = Dumper(os, &nest);
483 dumper.recurse(nest.root());
486 assertf(old_gid ==
curr_gid(),
"new nodes created during dump. old_gid: {}; curr_gid: {}", old_gid,
curr_gid());
496 auto ofs = std::ofstream(file);
501 auto file =
name().str() +
".mim"s;
A (possibly paramterized) Array.
World & world() const noexcept
const Def * var(nat_t a, nat_t i) noexcept
void write(int max) const
std::ostream & stream(std::ostream &, int max) const
Common base for TExtremum.
A built-in constant of type Nat -> *.
static const Def * isa(const Def *def)
Checks if def is a Idx s and returns s or nullptr otherwise.
static std::optional< T > isa(const Def *def)
Builds a nesting tree of all immutables/binders.
const auto & mut2node() const
A (possibly paramterized) Tuple.
A dependent function type.
static const Pi * isa_cn(const Def *d)
Is this a continuation - i.e. is the Pi::codom mim::Bottom?
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)
Data constructor for a Sigma.
const Driver & driver() const
u32 curr_gid() const
Manage global identifier - a unique number for each Def.
void dump()
Dump to std::cout.
void write()
Same above but file name defaults to World::name.
Flags & flags()
Retrieve compile Flags.
void debug_dump()
Dump in Debug build if World::log::level is Log::Level::Debug.
void write(const char *file)
Write to a file named file.
void dump(std::ostream &os)
Dump to os.
const Def * op(trait o, const Def *type)
std::ostream & print(std::ostream &os, const char *s)
Base case.
TBound< true > Join
AKA union.
GIDSet< const Def * > DefSet
std::ostream & operator<<(std::ostream &os, const Def *def)
This will stream def as an operand.
#define assertf(condition,...)
Use with print to output complicated std::ranges::ranges.
Use to World::freeze and automatically unfreeze at the end of scope.