13using namespace std::literals;
27Def* isa_decl(
const Def* def) {
28 if (
auto mut = def->isa_mut()) {
29 if (mut->is_external() || mut->isa<
Lam>() || (mut->sym() && mut->sym() !=
'_'))
return mut;
34std::string
id(
const Def* def) {
35 if (def->is_external() || (!def->is_set() && def->isa<
Lam>()))
return def->sym().str();
36 return def->unique_name();
39std::string_view external(
const Def* def) {
40 if (def->is_external())
return "extern "sv;
49 if (def->isa<
Extract>())
return Prec::Extract;
50 if (
auto pi = def->isa<
Pi>(); pi && !
Pi::isa_cn(pi))
return Prec::Arrow;
51 if (
auto app = def->isa<
App>()) {
60 case 0_n:
return Prec::Lit;
75 Op(
const Def* def,
Prec prec = Prec::Bot,
bool is_left =
false)
78 , is_left_(is_left) {}
79 static Op
l(
const Def* def,
Prec prec = Prec::Bot) {
return {def, prec,
true}; }
80 static Op
r(
const Def* def,
Prec prec = Prec::Bot) {
return {def, prec,
false}; }
82 static auto map(
const auto& range) {
83 return fe::Join(range | std::views::transform([](
auto op) {
return Op(op); }));
88 Prec prec()
const {
return prec_; }
89 bool is_left()
const {
return is_left_; }
90 const Def* def()
const {
return def_; }
91 const Def* operator->()
const {
return def_; }
92 const Def* operator*()
const {
return def_; }
93 explicit operator bool()
const {
return def_ !=
nullptr; }
103 friend std::ostream&
operator<<(std::ostream&, Op);
107class Dump :
public Op {
109 Dump(
const Def* def,
Prec prec = Prec::Bot,
bool is_left =
false)
110 : Op(def, prec, is_left) {}
112 : Dump(
op.def(),
op.prec(),
op.is_left()) {}
114 explicit operator bool()
const {
return is_inline(); }
116 bool is_inline()
const {
117 if (
auto mut = def()->isa_mut()) {
118 if (isa_decl(mut))
return false;
124 if (
auto app = def()->isa<App>()) {
125 if (app->type()->isa<
Pi>())
return true;
126 if (app->type()->isa<
Type>())
return true;
127 if (app->callee()->isa<
Axm>())
return app->callee_type()->num_doms() <= 1;
134 bool needs_parens()
const {
135 if (!is_inline())
return false;
137 auto child_prec = def2prec(def());
138 if (child_prec < prec())
return true;
139 if (child_prec > prec())
return false;
142 case Assoc::R:
return is_left();
143 case Assoc::L:
return !is_left();
144 case Assoc::N:
return false;
149 friend std::ostream&
operator<<(std::ostream&, Dump);
156template<>
struct std::formatter<
mim::Op > : fe::ostream_formatter {};
157template<>
struct std::formatter<
mim::Dump> : fe::ostream_formatter {};
163std::ostream& ptrn(std::ostream& os,
const Def* def,
const Def* type) {
164 if (!def)
return os << Op(type);
166 auto projs = def->tprojs();
167 if (projs.size() == 1 || std::ranges::all_of(projs, [](
auto d) { return !d; }))
168 return os << std::format(
"{}: {}", def->unique_name(), Op(type));
172 for (
auto sep =
"";
auto proj : projs) {
174 ptrn(os, proj, type->proj(i++));
177 return os << std::format(
") as {}", def->unique_name());
180std::ostream& bndr(std::ostream& os,
const Def* def,
const Def* type) {
181 if (def)
return ptrn(os, def, type);
182 return os << std::format(
"_: {}", Op(type));
186curry(std::ostream& os,
const Def* def,
const Def* type,
bool implicit,
bool paren_style,
size_t limit,
bool alias) {
187 auto l = implicit ?
'{' : paren_style ?
'(' :
'[';
188 auto r = implicit ?
'}' : paren_style ?
')' :
']';
190 if (limit == 0)
return os <<
l <<
r;
193 bndr(os, def ? def->tproj(0) :
nullptr,
type->tproj(0));
198 for (
auto sep =
"";
auto i : std::views::iota(
size_t(0), limit)) {
200 bndr(os, def ? def->tproj(i) :
nullptr,
type->tproj(i));
204 if (alias && def) os << std::format(
" as {}", def->unique_name());
208std::ostream&
operator<<(std::ostream& os, Op op) {
209 if (*op ==
nullptr)
return os <<
"<nullptr>";
210 if (
auto d = Dump(op))
return os <<
d;
211 return os <<
id(*op);
214std::ostream&
operator<<(std::ostream& os, Dump d) {
215 if (
auto mut =
d->isa_mut(); mut && !mut->is_set())
return os <<
"unset";
216 if (
d.needs_parens())
return os << std::format(
"({})", Dump(*d));
218 bool ascii =
d->world().flags().ascii;
219 auto arw = ascii ?
"->" :
"→";
220 auto al = ascii ?
"<<" :
"«";
221 auto ar = ascii ?
">>" :
"»";
222 auto pl = ascii ?
"(<" :
"‹";
223 auto pr = ascii ?
">)" :
"›";
224 auto bot = ascii ?
"bot" :
"⊥";
225 auto top = ascii ?
"top" :
"⊤";
227 if (
auto type =
d->isa<
Type>()) {
228 if (
auto level =
Lit::isa(
type->level()); level && !ascii) {
229 if (level == 0)
return os <<
"*";
230 if (level == 1)
return os <<
"□";
232 return os << std::format(
"Type {}", Op::r(
type->level(), Prec::App));
233 }
else if (
d->isa<
Nat>()) {
235 }
else if (
d->isa<
Idx>()) {
237 }
else if (
auto ext =
d->isa<
Ext>()) {
238 return os << std::format(
"{}:{}", ext->isa<
Bot>() ? bot : top, Op::r(ext->type(), Prec::Lit));
239 }
else if (
auto axm =
d->isa<
Axm>()) {
240 const auto name = axm->sym();
241 return os << std::format(
"{}{}", name[0] ==
'%' ?
"" :
"%", name);
242 }
else if (
auto lit =
d->isa<
Lit>()) {
243 if (
lit->type()->isa<
Nat>()) {
245 switch (
lit->get()) {
246 case 0x0'0000'0100_n:
return os <<
"i8";
247 case 0x0'0001'0000_n:
return os <<
"i16";
248 case 0x1'0000'0000_n:
return os <<
"i32";
249 default:
return os << std::format(
"{}",
lit->get());
256 case 0x0'0000'0002_n:
return os << (
lit->get<
bool>() ?
"tt" :
"ff");
257 case 0x0'0000'0100_n:
return os <<
lit->get() <<
"I8";
258 case 0x0'0001'0000_n:
return os <<
lit->get() <<
"I16";
259 case 0x1'0000'0000_n:
return os <<
lit->get() <<
"I32";
260 case 0_n:
return os <<
lit->get() <<
"I64";
263 std::vector<uint8_t> digits;
264 for (
auto z = *s; z; z /= 10) digits.emplace_back(z % 10);
268 for (
auto d : digits | std::views::reverse)
271 for (
auto d : digits | std::views::reverse)
272 os << uint8_t(0xE2) << uint8_t(0x82) << (uint8_t(0x80 + d));
280 return os << std::format(
"{}:{}",
lit->get(), Op::r(
lit->type(), Prec::Lit));
281 }
else if (
auto ex =
d->isa<
Extract>()) {
282 if (ex->tuple()->isa<
Var>() && ex->index()->isa<
Lit>())
return os << ex->unique_name();
283 return os << std::format(
"{}#{}", Op::l(ex->tuple(), Prec::Extract), Op::r(ex->index(), Prec::Extract));
284 }
else if (
auto var =
d->isa<
Var>()) {
285 return os << var->unique_name();
286 }
else if (
auto [pi, var] =
d->isa_binder<
Pi>(); pi) {
287 auto l = pi->is_implicit() ?
'{' :
'[';
288 auto r = pi->is_implicit() ?
'}' :
']';
289 return os << std::format(
"{}{}: {}{} {} {}", l, Op(var), Op(pi->dom()), r, arw,
290 Op::r(pi->codom(), Prec::Arrow));
291 }
else if (
auto pi =
d->isa<
Pi>()) {
292 if (
Pi::isa_cn(pi))
return os << std::format(
"Cn {}", Op(pi->dom()));
293 return os << std::format(
"{} {} {}", Op::l(pi->dom(), Prec::Arrow), arw, Op::r(pi->codom(), Prec::Arrow));
294 }
else if (
auto lam =
d->isa<
Lam>()) {
296 return os << std::format(
"{}, {}", Op(lam->filter()), Op(lam->body()));
297 }
else if (
auto app =
d->isa<
App>()) {
302 case 0x0'0000'0002_n:
return os <<
"Bool";
303 case 0x0'0000'0100_n:
return os <<
"I8";
304 case 0x0'0001'0000_n:
return os <<
"I16";
305 case 0x1'0000'0000_n:
return os <<
"I32";
306 case 0_n:
return os <<
"I64";
313 return os << std::format(
"{} {}", Op::l(app->callee(), Prec::App), Op::r(app->arg(), Prec::App));
314 }
else if (
auto [sigma, var] =
d->isa_binder<
Sigma>(); sigma) {
316 auto elem = fe::StreamFn{[&](std::ostream& os) -> std::ostream& {
318 for (
auto op : sigma->ops()) {
320 if (
auto v = sigma->var(i++))
321 os << std::format(
"{}: {}", v, Op(op));
329 return os << std::format(
"[{}]", elem);
330 }
else if (
auto sigma =
d->isa<
Sigma>()) {
331 return os << std::format(
"[{}]", Op::map(sigma->ops()));
332 }
else if (
auto tuple =
d->isa<
Tuple>()) {
333 return os << std::format(
"({})", Op::map(tuple->ops()));
334 }
else if (
auto [arr, var] =
d->isa_binder<
Arr>(); arr) {
335 return os << std::format(
"{}{}: {}; {}{}", al, var, Op(arr->arity()), Op(arr->body()), ar);
336 }
else if (
auto arr =
d->isa<
Arr>()) {
337 return os << std::format(
"{}{}; {}{}", al, Op(arr->arity()), Op(arr->body()), ar);
338 }
else if (
auto [pack, var] =
d->isa_binder<
Pack>(); pack) {
339 return os << std::format(
"{}{}: {}; {}{}", pl, pack->var(), Op(pack->arity()), Op(pack->body()), pr);
340 }
else if (
auto pack =
d->isa<
Pack>()) {
341 return os << std::format(
"{}{}; {}{}", pl, Op(pack->arity()), Op(pack->body()), pr);
342 }
else if (
auto proxy =
d->isa<
Proxy>()) {
343 return os << std::format(
".proxy#{}#{} {}", proxy->pass(), proxy->tag(), Op::map(proxy->ops()));
344 }
else if (
auto bound =
d->isa<
Bound>()) {
345 auto op = bound->isa<
Join>() ?
"∪" :
"∩";
346 if (
auto mut =
d->isa_mut()) std::print(os,
"{}{}: {}", op, mut->unique_name(), Op(mut->type()));
347 return os << std::format(
"{}({})", op, Op::map(bound->ops()));
351 if (
d->flags() == 0)
return os << std::format(
"({} {})",
d->node_name(), fe::Join(
d->ops()));
352 return os << std::format(
"({}#{} {})",
d->node_name(),
d->flags(), Op::map(
d->ops()));
365 Dumper(std::ostream& os,
const Nest* nest =
nullptr)
371 void dump_let(
const Def*);
372 void recurse(
const Nest::Node*);
373 void recurse(
const Def*,
bool first =
false);
377 fe::Tab tab = fe::Tab::spaces();
378 unique_queue<MutSet> muts;
382void Dumper::dump(
Def* mut) {
383 if (
auto lam = mut->isa<Lam>()) {
388 auto mut_prefix = [&](
const Def* def) {
389 if (def->isa<Sigma>())
return "Sigma";
390 if (def->isa<Arr>())
return "Arr";
391 if (def->isa<Pack>())
return "pack";
392 if (def->isa<Pi>())
return "Pi";
393 if (def->isa<Hole>())
return "Hole";
394 if (def->isa<Rule>())
return "Rule";
398 auto mut_op0 = [&](
const Def* def) -> std::ostream& {
399 if (
auto sig = def->isa<Sigma>())
return os << std::format(
", {}", sig->num_ops());
400 if (
auto arr = def->isa<Arr>())
return os << std::format(
", {}", arr->arity());
401 if (
auto pack = def->isa<Pack>())
return os << std::format(
", {}", pack->arity());
402 if (
auto pi = def->isa<Pi>())
return os << std::format(
", {}", pi->dom());
403 if (
auto hole = def->isa_mut<Hole>())
404 return hole->is_set() ? (os << std::format(
", {}", hole->op())) : (os <<
", ??");
405 if (
auto rule = def->isa<Rule>())
return os << std::format(
"{} => {}", rule->lhs(), rule->rhs());
409 if (!mut->is_set()) {
410 std::print(os,
"{}{}: {} = {{ <unset> }};", tab,
id(mut), mut->type());
414 std::print(os,
"{}{} {}{}: {}", tab, mut_prefix(mut), external(mut),
id(mut), mut->type());
417 if (
auto e = mut->num_vars(); e != 1) {
418 for (
auto sep =
"";
auto def : mut->vars()) {
421 os << def->unique_name();
427 std::print(os,
", @{}", mut->var()->unique_name());
430 std::println(os,
"{} = {{", tab);
432 if (nest) recurse((*nest)[mut]);
434 std::println(os,
"{}{}", tab, fe::Join(mut->ops()));
436 std::println(os,
"{}}};", tab);
439void Dumper::dump_lam(
Lam* lam) {
440 std::vector<Lam*> currys;
441 for (Lam* curr = lam;;) {
442 currys.emplace_back(curr);
443 if (
auto body = curr->body())
444 if (
auto next = body->isa_mut<Lam>()) {
451 auto last = currys.back();
452 auto is_fun = Lam::isa_returning(last);
453 auto is_con = Lam::isa_cn(last) && !is_fun;
455 std::print(os,
"{}{} {}{}", tab, is_fun ?
"fun" : is_con ?
"con" :
"lam", external(lam),
id(lam));
456 for (
auto* c : currys) {
458 auto num_doms =
c->var() ?
c->var()->num_tprojs() :
c->type()->dom()->num_tprojs();
459 auto limit = is_fun &&
c ==
last ? num_doms - 1 : num_doms;
460 curry(os,
c->var(),
c->type()->dom(),
c->type()->is_implicit(), !is_con, limit, !is_fun || c != last);
461 if (is_con && c == last) std::print(os,
"@({})",
c->filter());
465 std::print(os,
": {} =",
last->ret_dom());
467 std::print(os,
": {} =",
last->type()->codom());
469 std::print(os,
" =");
473 if (
last->is_set()) {
474 if (nest && currys.size() == 1) recurse((*nest)[lam]);
475 for (
auto* curry : currys)
476 recurse(curry->filter());
477 recurse(
last->body(),
true);
478 if (
last->body()->isa_mut())
479 std::println(os,
"{}{};", tab,
last->body());
481 std::println(os,
"{}{};", tab, Dump(
last->body()));
483 std::println(os,
"{}<unset>;", tab);
486 std::println(os,
"{}", tab);
489void Dumper::dump_let(
const Def* def) {
490 std::println(os,
"{}let {}: {} = {};", tab, def->unique_name(), Op(def->type()), Dump(def));
493void Dumper::recurse(
const Nest::Node* node) {
494 for (
auto child : node->children().muts())
495 if (
auto mut = isa_decl(child)) dump(mut);
498void Dumper::recurse(
const Def* def,
bool first ) {
499 if (
auto mut = isa_decl(def)) {
500 if (!nest) muts.push(mut);
504 if (!defs.emplace(def).second)
return;
506 for (
auto op : def->deps())
509 if (!first && !Dump(def)) dump_let(def);
521 if (def ==
nullptr)
return os <<
"<nullptr>";
522 if (
auto d = Dump(def)) {
526 return os << id(def);
530 auto _ =
world().freeze();
531 auto dumper = Dumper(os);
534 os <<
this << std::endl;
535 }
else if (
auto mut = isa_decl(
this)) {
536 dumper.muts.push(mut);
538 dumper.recurse(
this);
539 std::println(os,
"{}{}", dumper.tab, Dump(
this));
543 for (; !dumper.muts.empty() && max > 0; --max)
544 dumper.dump(dumper.muts.pop());
549void Def::dump()
const { std::cout <<
this << std::endl; }
553 auto ofs = std::ofstream(file);
558 auto file = id(
this) +
".mim"s;
559 write(max, file.c_str());
570 if (
flags().dump_recursive) {
571 auto dumper = Dumper(os);
573 dumper.muts.push(mut);
574 while (!dumper.muts.empty())
575 dumper.dump(dumper.muts.pop());
577 auto nest =
Nest(*
this);
578 auto dumper = Dumper(os, &nest);
580 for (
const auto&
import :
driver().imports())
581 std::print(os,
"{} {};\n",
import.tag == ast::Tok::Tag::K_plugin ?
"plugin" :
"import",
import.
sym);
582 dumper.recurse(nest.root());
585 assertf(old_gid ==
curr_gid(),
"new nodes created during dump. old_gid: {}; curr_gid: {}", old_gid,
curr_gid());
595 auto ofs = std::ofstream(file);
600 auto file = (
name() ?
name() :
sym(
"_default")).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 for 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?
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.
@ bot
Alias for Mode::fast.
TBound< true > Join
AKA union.
GIDSet< const Def * > DefSet
std::ostream & operator<<(std::ostream &os, const Error::Msg &msg)
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.
Use to World::freeze and automatically unfreeze at the end of scope.