12using namespace std::literals;
26Def* isa_decl(
const Def* def) {
27 if (
auto mut = def->isa_mut()) {
28 if (mut->is_external() || mut->isa<
Lam>() || (mut->sym() && mut->sym() !=
'_'))
return mut;
33std::string
id(
const Def* def) {
34 if (def->is_external() || (!def->is_set() && def->isa<
Lam>()))
return def->sym().str();
35 return def->unique_name();
38std::string_view external(
const Def* def) {
39 if (def->is_external())
return "extern "sv;
48 if (def->isa<
Extract>())
return Prec::Extract;
49 if (
auto pi = def->isa<
Pi>(); pi && !
Pi::isa_cn(pi))
return Prec::Arrow;
50 if (
auto app = def->isa<
App>()) {
59 case 0_n:
return Prec::Lit;
74 Op(
const Def* def,
Prec prec = Prec::Bot,
bool is_left =
false)
77 , is_left_(is_left) {}
78 static Op
l(
const Def* def,
Prec prec = Prec::Bot) {
return {def, prec,
true}; }
79 static Op
r(
const Def* def,
Prec prec = Prec::Bot) {
return {def, prec,
false}; }
83 Prec prec()
const {
return prec_; }
84 bool is_left()
const {
return is_left_; }
85 const Def* def()
const {
return def_; }
86 const Def* operator->()
const {
return def_; }
87 const Def* operator*()
const {
return def_; }
88 explicit operator bool()
const {
return def_ !=
nullptr; }
98 friend std::ostream&
operator<<(std::ostream&, Op);
102class Dump :
public Op {
104 Dump(
const Def* def,
Prec prec = Prec::Bot,
bool is_left =
false)
105 : Op(def, prec, is_left) {}
107 : Dump(
op.def(),
op.prec(),
op.is_left()) {}
109 explicit operator bool()
const {
return is_inline(); }
111 bool is_inline()
const {
112 if (
auto mut = def()->isa_mut()) {
113 if (isa_decl(mut))
return false;
119 if (
auto app = def()->isa<App>()) {
120 if (app->type()->isa<
Pi>())
return true;
121 if (app->type()->isa<
Type>())
return true;
122 if (app->callee()->isa<
Axm>())
return app->callee_type()->num_doms() <= 1;
129 bool needs_parens()
const {
130 if (!is_inline())
return false;
132 auto child_prec = def2prec(def());
133 if (child_prec < prec())
return true;
134 if (child_prec > prec())
return false;
137 case Assoc::R:
return is_left();
138 case Assoc::L:
return !is_left();
139 case Assoc::N:
return false;
144 friend std::ostream&
operator<<(std::ostream&, Dump);
147auto ptrn(
const Def* def,
const Def* type) {
148 return StreamFn{[=](std::ostream& os) -> std::ostream& {
149 if (!def)
return os << Op(type);
151 auto projs = def->tprojs();
152 if (projs.size() == 1 || std::ranges::all_of(projs, [](
auto def) { return !def; }))
153 return print(os,
"{}: {}", def->unique_name(), Op(type));
156 auto elem =
Elem(projs, [&](
auto proj) { os << ptrn(proj,
type->proj(i++)); });
157 return print(os,
"({, }) as {}", elem, def->unique_name());
161auto bndr(
const Def* def,
const Def* type) {
162 return StreamFn{[=](std::ostream& os) -> std::ostream& {
163 if (def)
return os << ptrn(def, type);
164 return print(os,
"_: {}", Op(type));
168auto curry(
const Def* def,
const Def* type,
bool implicit,
bool paren_style,
size_t limit,
bool alias) {
169 return StreamFn{[=](std::ostream& os) -> std::ostream& {
170 auto l = implicit ?
'{' : paren_style ?
'(' :
'[';
171 auto r = implicit ?
'}' : paren_style ?
')' :
']';
173 if (limit == 0)
return os <<
l <<
r;
174 if (limit == 1)
return print(os,
"{}{}{}", l, bndr(def ? def->tproj(0) :
nullptr,
type->tproj(0)), r);
176 auto elem = [&](
auto i) { os << bndr(def ? def->tproj(i) :
nullptr,
type->tproj(i)); };
177 print(os,
"{}{, }{}", l,
Elem(std::views::iota(
size_t(0), limit), elem), r);
178 if (alias && def)
print(os,
" as {}", def->unique_name());
183std::ostream&
operator<<(std::ostream& os, Op op) {
184 if (*op ==
nullptr)
return os <<
"<nullptr>";
185 if (
auto d = Dump(op))
return os <<
d;
186 return os <<
id(*op);
189std::ostream&
operator<<(std::ostream& os, Dump d) {
190 if (
auto mut =
d->isa_mut(); mut && !mut->is_set())
return os <<
"unset";
191 if (
d.needs_parens())
return print(os,
"({})", Dump(*d));
193 bool ascii =
d->world().flags().ascii;
194 auto arw = ascii ?
"->" :
"→";
195 auto al = ascii ?
"<<" :
"«";
196 auto ar = ascii ?
">>" :
"»";
197 auto pl = ascii ?
"(<" :
"‹";
198 auto pr = ascii ?
">)" :
"›";
199 auto bot = ascii ?
"bot" :
"⊥";
200 auto top = ascii ?
"top" :
"⊤";
202 if (
auto type =
d->isa<
Type>()) {
203 if (
auto level =
Lit::isa(
type->level()); level && !ascii) {
204 if (level == 0)
return print(os,
"*");
205 if (level == 1)
return print(os,
"□");
207 return print(os,
"Type {}", Op::r(
type->level(), Prec::App));
208 }
else if (
d->isa<
Nat>()) {
209 return print(os,
"Nat");
210 }
else if (
d->isa<
Idx>()) {
211 return print(os,
"Idx");
212 }
else if (
auto ext =
d->isa<
Ext>()) {
213 return print(os,
"{}:{}", ext->isa<
Bot>() ? bot : top, Op::r(ext->type(), Prec::Lit));
214 }
else if (
auto axm =
d->isa<
Axm>()) {
215 const auto name = axm->sym();
216 return print(os,
"{}{}", name[0] ==
'%' ?
"" :
"%", name);
217 }
else if (
auto lit =
d->isa<
Lit>()) {
218 if (
lit->type()->isa<
Nat>()) {
220 switch (
lit->get()) {
221 case 0x0'0000'0100_n:
return os <<
"i8";
222 case 0x0'0001'0000_n:
return os <<
"i16";
223 case 0x1'0000'0000_n:
return os <<
"i32";
224 default:
return print(os,
"{}",
lit->get());
231 case 0x0'0000'0002_n:
return os << (
lit->get<
bool>() ?
"tt" :
"ff");
232 case 0x0'0000'0100_n:
return os <<
lit->get() <<
"I8";
233 case 0x0'0001'0000_n:
return os <<
lit->get() <<
"I16";
234 case 0x1'0000'0000_n:
return os <<
lit->get() <<
"I32";
235 case 0_n:
return os <<
lit->get() <<
"I64";
238 std::vector<uint8_t> digits;
239 for (
auto z = *s; z; z /= 10) digits.emplace_back(z % 10);
243 for (
auto d : digits | std::ranges::views::reverse)
246 for (
auto d : digits | std::ranges::views::reverse)
247 os << uint8_t(0xE2) << uint8_t(0x82) << (uint8_t(0x80 + d));
255 return print(os,
"{}:{}",
lit->get(), Op::r(
lit->type(), Prec::Lit));
256 }
else if (
auto ex =
d->isa<
Extract>()) {
257 if (ex->tuple()->isa<
Var>() && ex->index()->isa<
Lit>())
return os << ex->unique_name();
258 return print(os,
"{}#{}", Op::l(ex->tuple(), Prec::Extract), Op::r(ex->index(), Prec::Extract));
259 }
else if (
auto var =
d->isa<
Var>()) {
260 return os << var->unique_name();
261 }
else if (
auto [pi, var] =
d->isa_binder<
Pi>(); pi) {
262 auto l = pi->is_implicit() ?
'{' :
'[';
263 auto r = pi->is_implicit() ?
'}' :
']';
264 return print(os,
"{}{}: {}{} {} {}", l, Op(var), Op(pi->dom()), r, arw, Op::r(pi->dom(), Prec::Arrow));
265 }
else if (
auto pi =
d->isa<
Pi>()) {
267 return print(os,
"{} {} {}", Op::l(pi->dom(), Prec::Arrow), arw, Op::r(pi->dom(), Prec::Arrow));
268 }
else if (
auto lam =
d->isa<
Lam>()) {
270 return print(os,
"{}, {}", Op(lam->filter()), Op(lam->body()));
271 }
else if (
auto app =
d->isa<
App>()) {
276 case 0x0'0000'0002_n:
return os <<
"Bool";
277 case 0x0'0000'0100_n:
return os <<
"I8";
278 case 0x0'0001'0000_n:
return os <<
"I16";
279 case 0x1'0000'0000_n:
return os <<
"I32";
280 case 0_n:
return os <<
"I64";
287 return print(os,
"{} {}", Op::l(app->callee(), Prec::App), Op::r(app->arg(), Prec::App));
288 }
else if (
auto [sigma, var] =
d->isa_binder<
Sigma>(); sigma) {
290 auto elem =
Elem(sigma->ops(), [&os, sigma, &i](
auto op) {
291 if (auto v = sigma->var(i++))
292 print(os,
"{}: {}", v, Op(op));
297 return print(os,
"[{, }]", elem);
298 }
else if (
auto sigma =
d->isa<
Sigma>()) {
300 }
else if (
auto tuple =
d->isa<
Tuple>()) {
302 }
else if (
auto [arr, var] =
d->isa_binder<
Arr>(); arr) {
303 return print(os,
"{}{}: {}; {}{}", al, var, Op(arr->arity()), Op(arr->body()), ar);
304 }
else if (
auto arr =
d->isa<
Arr>()) {
305 return print(os,
"{}{}; {}{}", al, Op(arr->arity()), Op(arr->body()), ar);
306 }
else if (
auto [pack, var] =
d->isa_binder<
Pack>(); pack) {
307 return print(os,
"{}{}: {}; {}{}", pl, pack->var(), Op(pack->arity()), Op(pack->body()), pr);
308 }
else if (
auto pack =
d->isa<
Pack>()) {
309 return print(os,
"{}{}; {}{}", pl, Op(pack->arity()), Op(pack->body()), pr);
310 }
else if (
auto proxy =
d->isa<
Proxy>()) {
311 return print(os,
".proxy#{}#{} {, }", proxy->pass(), proxy->tag(),
elems<Op>(os, proxy->ops()));
312 }
else if (
auto bound =
d->isa<
Bound>()) {
313 auto op = bound->isa<
Join>() ?
"∪" :
"∩";
314 if (
auto mut =
d->isa_mut())
print(os,
"{}{}: {}", op, mut->unique_name(), Op(mut->type()));
319 if (
d->flags() == 0)
return print(os,
"({} {, })",
d->node_name(),
d->ops());
320 return print(os,
"({}#{} {, })",
d->node_name(),
d->flags(),
elems<Op>(os,
d->ops()));
333 Dumper(std::ostream& os,
const Nest* nest =
nullptr)
339 void dump_let(
const Def*);
340 void recurse(
const Nest::Node*);
341 void recurse(
const Def*,
bool first =
false);
346 unique_queue<MutSet> muts;
350void Dumper::dump(
Def* mut) {
351 if (
auto lam = mut->isa<Lam>()) {
356 auto mut_prefix = [&](
const Def* def) {
357 if (def->isa<Sigma>())
return "Sigma";
358 if (def->isa<Arr>())
return "Arr";
359 if (def->isa<Pack>())
return "pack";
360 if (def->isa<Pi>())
return "Pi";
361 if (def->isa<Hole>())
return "Hole";
362 if (def->isa<Rule>())
return "Rule";
366 auto mut_op0 = [&](
const Def* def) -> std::ostream& {
367 if (
auto sig = def->isa<Sigma>())
return print(os,
", {}", sig->num_ops());
368 if (
auto arr = def->isa<Arr>())
return print(os,
", {}", arr->arity());
369 if (
auto pack = def->isa<Pack>())
return print(os,
", {}", pack->arity());
370 if (
auto pi = def->isa<Pi>())
return print(os,
", {}", pi->dom());
371 if (
auto hole = def->isa_mut<Hole>())
return hole->is_set() ?
print(os,
", {}", hole->op()) :
print(os,
", ??");
372 if (
auto rule = def->isa<Rule>())
return print(os,
"{} => {}", rule->lhs(), rule->rhs());
376 if (!mut->is_set()) {
377 tab.
print(os,
"{}: {} = {{ <unset> }};",
id(mut), mut->type());
381 tab.
print(os,
"{} {}{}: {}", mut_prefix(mut), external(mut),
id(mut), mut->type());
384 if (
auto e = mut->num_vars(); e != 1) {
385 print(os,
"{, }", Elem(mut->vars(), [&](
auto def) {
387 os << def->unique_name();
392 print(os,
", @{}", mut->var()->unique_name());
397 if (nest) recurse((*nest)[mut]);
399 tab.
print(os,
"{, }\n", mut->ops());
401 tab.
print(os,
"}};\n");
404void Dumper::dump_lam(
Lam* lam) {
405 std::vector<Lam*> currys;
406 for (Lam* curr = lam;;) {
407 currys.emplace_back(curr);
408 if (
auto body = curr->body())
409 if (
auto next = body->isa_mut<Lam>()) {
416 auto last = currys.back();
417 auto is_fun = Lam::isa_returning(last);
418 auto is_con = Lam::isa_cn(last) && !is_fun;
420 tab.
print(os,
"{} {}{}", is_fun ?
"fun" : is_con ?
"con" :
"lam", external(lam),
id(lam));
421 for (
auto* c : currys) {
423 auto num_doms =
c->var() ?
c->var()->num_tprojs() :
c->type()->dom()->num_tprojs();
424 auto limit = is_fun &&
c ==
last ? num_doms - 1 : num_doms;
425 os << curry(
c->var(),
c->type()->dom(),
c->type()->is_implicit(), !is_con, limit, !is_fun || c != last);
426 if (is_con && c == last)
print(os,
"@({})",
c->filter());
432 print(os,
": {} =",
last->type()->codom());
438 if (
last->is_set()) {
439 if (nest && currys.size() == 1) recurse((*nest)[lam]);
440 for (
auto* curry : currys)
441 recurse(curry->filter());
442 recurse(
last->body(),
true);
443 if (
last->body()->isa_mut())
446 tab.
print(os,
"{};\n", Dump(
last->body()));
448 tab.
print(os,
"<unset>;\n");
454void Dumper::dump_let(
const Def* def) {
455 tab.
print(os,
"let {}: {} = {};\n", def->unique_name(), Op(def->type()), Dump(def));
458void Dumper::recurse(
const Nest::Node* node) {
459 for (
auto child : node->children().muts())
460 if (
auto mut = isa_decl(child)) dump(mut);
463void Dumper::recurse(
const Def* def,
bool first ) {
464 if (
auto mut = isa_decl(def)) {
465 if (!nest) muts.push(mut);
469 if (!defs.emplace(def).second)
return;
471 for (
auto op : def->deps())
474 if (!first && !Dump(def)) dump_let(def);
486 if (def ==
nullptr)
return os <<
"<nullptr>";
487 if (
auto d = Dump(def)) {
491 return os << id(def);
495 auto _ =
world().freeze();
496 auto dumper = Dumper(os);
499 os <<
this << std::endl;
500 }
else if (
auto mut = isa_decl(
this)) {
501 dumper.muts.push(mut);
503 dumper.recurse(
this);
504 dumper.tab.print(os,
"{}\n", Dump(
this));
508 for (; !dumper.muts.empty() && max > 0; --max)
509 dumper.dump(dumper.muts.pop());
514void Def::dump()
const { std::cout <<
this << std::endl; }
518 auto ofs = std::ofstream(file);
523 auto file = id(
this) +
".mim"s;
524 write(max, file.c_str());
535 if (
flags().dump_recursive) {
536 auto dumper = Dumper(os);
538 dumper.muts.push(mut);
539 while (!dumper.muts.empty())
540 dumper.dump(dumper.muts.pop());
542 auto nest =
Nest(*
this);
543 auto dumper = Dumper(os, &nest);
545 for (
const auto&
import :
driver().imports())
546 print(os,
"{} {};\n",
import.tag == ast::Tok::Tag::K_plugin ?
"plugin" :
"import",
import.
sym);
547 dumper.recurse(nest.root());
550 assertf(old_gid ==
curr_gid(),
"new nodes created during dump. old_gid: {}; curr_gid: {}", old_gid,
curr_gid());
560 auto ofs = std::ofstream(file);
565 auto file =
name().str() +
".mim"s;
A (possibly paramterized) Array.
World & world() const 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 mutables/binders.
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.
A variable introduced by a binder (mutable).
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.
Freezer freeze()
Use like this to freeze and automatically unfreeze:
Sym sym(std::string_view)
void write(const char *file)
Write to a file named file.
const Externals & externals() const
void dump(std::ostream &os)
Dump to os.
Assoc
Associativity of an infix expression.
constexpr Assoc prec_assoc(Prec p)
Associativity of precedence level p.
Prec
Expression precedences used by the parser and the dumper; ordered low to high.
const Def * op(trait o, const Def *type)
@ bot
Alias for Mode::fast.
std::ostream & print(std::ostream &os, const char *s)
Base case.
TBound< true > Join
AKA union.
auto elems(std::ostream &os, const auto &range)
Wrap all elements in range through os << T(elem).
GIDSet< const Def * > DefSet
std::ostream & operator<<(std::ostream &os, const Def *def)
This will stream def as an operand.
constexpr Assoc prec_assoc(Prec p)
Associativity of precedence level p.
Prec
Expression precedences used by the parser and the dumper; ordered low to high.
#define assertf(condition,...)
Use with print to output complicated std::ranges::ranges.
Create function-wrapper objects amenable for opeartor<<.
Use to World::freeze and automatically unfreeze at the end of scope.