MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
world.cpp
Go to the documentation of this file.
1#include "mim/world.h"
2
3#include "mim/check.h"
4#include "mim/def.h"
5#include "mim/driver.h"
6#include "mim/rewrite.h"
7#include "mim/rule.h"
8#include "mim/tuple.h"
9
10#include "mim/util/util.h"
11
12namespace mim {
13
14namespace {
15
16bool is_shape(const Def* s) {
17 if (s->isa<Nat>()) return true;
18 if (auto arr = s->isa<Arr>()) return arr->body()->zonk()->isa<Nat>();
19 if (auto sig = s->isa_imm<Sigma>())
20 return std::ranges::all_of(sig->ops(), [](const Def* op) { return op->isa<Nat>(); });
21
22 return false;
23}
24
25} // namespace
26
27/*
28 * constructor & destructor
29 */
30
31#if (!defined(_MSC_VER) && defined(NDEBUG))
32bool World::Lock::guard_ = false;
33#endif
34
36 : driver_(driver)
37 , zonker_(*this)
38 , state_(state) {
39 data_.univ = insert<Univ>(*this);
40 data_.lit_univ_0 = lit_univ(0);
41 data_.lit_univ_1 = lit_univ(1);
42 data_.type_0 = type(lit_univ_0());
43 data_.type_1 = type(lit_univ_1());
44 data_.type_bot = insert<Bot>(type());
45 data_.type_top = insert<Top>(type());
46 data_.sigma = unify<Sigma>(type(), Defs{})->as<Sigma>();
47 data_.tuple = unify<Tuple>(sigma(), Defs{})->as<Tuple>();
48 data_.type_nat = insert<mim::Nat>(*this);
49 data_.type_idx = insert<mim::Idx>(pi(type_nat(), type()));
50 data_.top_nat = insert<Top>(type_nat());
51 data_.lit_nat_0 = lit_nat(0);
52 data_.lit_nat_1 = lit_nat(1);
53 data_.lit_idx_1_0 = lit_idx(1, 0);
54 data_.type_bool = type_idx(2);
55 data_.lit_bool[0] = lit_idx(2, 0_u64);
56 data_.lit_bool[1] = lit_idx(2, 1_u64);
57 data_.lit_nat_max = lit_nat(nat_t(-1));
58}
59
62
64 for (auto def : move_.defs)
65 def->~Def();
66}
67
68/*
69 * Driver
70 */
71
72Log& World::log() const { return driver().log(); }
73Flags& World::flags() { return driver().flags(); }
74
75Sym World::sym(const char* s) { return driver().sym(s); }
76Sym World::sym(std::string_view s) { return driver().sym(s); }
77Sym World::sym(const std::string& s) { return driver().sym(s); }
78
79const Def* World::register_annex(flags_t f, const Def* def) {
80 TLOG("register: 0x{x} -> {}", f, def);
81 auto plugin = Annex::demangle(driver(), f);
82 if (driver().is_loaded(plugin)) {
83 assert_emplace(move_.flags2annex, f, def);
84 return def;
85 }
86 return nullptr;
87}
88
90 assert(!def->is_external());
91 assert(def->is_closed());
92 def->external_ = true;
93 assert_emplace(move_.sym2external, def->sym(), def);
94}
95
97 assert(def->is_external());
98 def->external_ = false;
99 auto num = move_.sym2external.erase(def->sym());
100 assert_unused(num == 1);
101}
102
103/*
104 * factory methods
105 */
106
107const Type* World::type(const Def* level) {
108 level = level->zonk();
109
110 if (!level->type()->isa<Univ>())
111 error(level->loc(), "argument `{}` to `Type` must be of type `Univ` but is of type `{}`", level, level->type());
112
113 return unify<Type>(level)->as<Type>();
114}
115
116const Def* World::uinc(const Def* op, level_t offset) {
117 op = op->zonk();
118
119 if (!op->type()->isa<Univ>())
120 error(op->loc(), "operand '{}' of a universe increment must be of type `Univ` but is of type `{}`", op,
121 op->type());
122
123 if (auto l = Lit::isa(op)) return lit_univ(*l + 1);
124 return unify<UInc>(op, offset);
125}
126
127static void flatten_umax(DefVec& ops, const Def* def) {
128 if (auto umax = def->isa<UMax>())
129 for (auto op : umax->ops())
130 flatten_umax(ops, op);
131 else
132 ops.emplace_back(def);
133}
134
135template<int sort>
136const Def* World::umax(Defs ops_) {
137 DefVec ops;
138 for (auto op : ops_) {
139 op = op->zonk();
140
141 if constexpr (sort == UMax::Term) op = op->unfold_type();
142 if constexpr (sort >= UMax::Type) op = op->unfold_type();
143 if constexpr (sort >= UMax::Kind) {
144 if (auto type = op->isa<Type>())
145 op = type->level();
146 else
147 error(op->loc(), "operand '{}' must be a Type of some level", op); // TODO better error message
148 }
149
150 flatten_umax(ops, op);
151 }
152
153 level_t lvl = 0;
154 DefVec res;
155 for (auto op : ops) {
156 if (!op->type()->isa<Univ>())
157 error(op->loc(), "operand '{}' of a universe max must be of type 'Univ' but is of type '{}'", op,
158 op->type());
159
160 if (auto l = Lit::isa(op))
161 lvl = std::max(lvl, *l);
162 else
163 res.emplace_back(op);
164 }
165
166 const Def* l = lit_univ(lvl);
167 if (res.empty()) return sort == UMax::Univ ? l : type(l);
168 if (lvl > 0) res.emplace_back(l);
169
170 std::ranges::sort(res, [](auto op1, auto op2) { return op1->gid() < op2->gid(); });
171 res.erase(std::unique(res.begin(), res.end()), res.end());
172 const Def* umax = unify<UMax>(*this, res);
173 return sort == UMax::Univ ? umax : type(umax);
174}
175
176// TODO more thorough & consistent checks for singleton types
177
178const Def* World::var(Def* mut) {
179 if (auto s = Idx::isa(mut->var_type())) {
180 if (auto l = Lit::isa(s); l && l == 1) return lit_idx_1_0();
181 }
182
183 if (auto var = mut->var_) return var;
184 return mut->var_ = unify<Var>(mut);
185}
186
187template<bool Normalize>
188const Def* World::implicit_app(const Def* callee, const Def* arg) {
189 while (auto pi = Pi::isa_implicit(callee->type()))
190 callee = app(callee, mut_hole(pi->dom()));
191 return app<Normalize>(callee, arg);
192}
193
194template<bool Normalize>
195const Def* World::app(const Def* callee, const Def* arg) {
196 callee = callee->zonk();
197 arg = arg->zonk();
198
199 if (auto pi = callee->type()->isa<Pi>()) {
200 if (auto new_arg = Checker::assignable(pi->dom(), arg)) {
201 arg = new_arg->zonk();
202 if (auto imm = callee->isa_imm<Lam>()) return imm->body();
203
204 if (auto lam = callee->isa_mut<Lam>(); lam && lam->is_set() && lam->filter() != lit_ff()) {
205 if (auto var = lam->has_var()) {
206 if (auto i = move_.substs.find({var, arg}); i != move_.substs.end()) {
207 // Is there a cached version?
208 auto [filter, body] = i->second->defs<2>();
209 if (filter == lit_tt()) return body;
210 } else {
211 // First check filter, If true, reduce body and cache reduct.
212 auto rw = VarRewriter(var, arg);
213 auto filter = rw.rewrite(lam->filter());
214 if (filter == lit_tt()) {
215 DLOG("partial evaluate: {} ({})", lam, arg);
216 auto body = rw.rewrite(lam->body());
217 auto num_bytes = sizeof(Reduct) + 2 * sizeof(const Def*);
218 auto buf = move_.arena.substs.allocate(num_bytes, alignof(const Def*));
219 auto reduct = new (buf) Reduct(2);
220 reduct->defs_[0] = filter;
221 reduct->defs_[1] = body;
222 assert_emplace(move_.substs, std::pair{var, arg}, reduct);
223 return body;
224 }
225 }
226 } else if (lam->filter() == lit_tt()) {
227 return lam->body();
228 }
229 }
230
231 auto type = pi->reduce(arg)->zonk();
232 callee = callee->zonk();
233 auto [axm, curry, trip] = Axm::get(callee);
234 if (axm) {
235 curry = curry == 0 ? trip : curry;
236 curry = curry == Axm::Trip_End ? curry : curry - 1;
237
238 if (auto normalizer = axm->normalizer(); Normalize && normalizer && curry == 0) {
239 if (auto norm = normalizer(type, callee, arg)) return norm;
240 }
241 }
242
243 return raw_app(axm, curry, trip, type, callee, arg);
244 }
245
246 throw Error()
247 .error(arg->loc(), "cannot apply argument to callee")
248 .note(callee->loc(), "callee: '{}'", callee)
249 .note(arg->loc(), "argument: '{}'", arg)
250 .note(callee->loc(), "vvv domain type vvv\n'{}'\n'{}'", pi->dom(), arg->type())
251 .note(arg->loc(), "^^^ argument type ^^^");
252 }
253
254 throw Error()
255 .error(callee->loc(), "called expression not of function type")
256 .error(callee->loc(), "'{}' <--- callee type", callee->type());
257}
258
259const Def* World::raw_app(const Def* type, const Def* callee, const Def* arg) {
260 type = type->zonk();
261 callee = callee->zonk();
262 arg = arg->zonk();
263
264 auto [axm, curry, trip] = Axm::get(callee);
265 if (axm) {
266 curry = curry == 0 ? trip : curry;
267 curry = curry == Axm::Trip_End ? curry : curry - 1;
268 }
269
270 return raw_app(axm, curry, trip, type, callee, arg);
271}
272
273const Def* World::raw_app(const Axm* axm, u8 curry, u8 trip, const Def* type, const Def* callee, const Def* arg) {
274 return unify<App>(axm, curry, trip, type, callee, arg);
275}
276
277const Def* World::sigma(Defs ops) {
278 auto n = ops.size();
279 if (n == 0) return sigma();
280 if (n == 1) return ops[0]->zonk();
281
282 auto zops = Def::zonk(ops);
283 if (auto uni = Checker::is_uniform(zops)) return arr(n, uni);
284 return unify<Sigma>(Sigma::infer(*this, zops), zops);
285}
286
287const Def* World::tuple(Defs ops) {
288 auto n = ops.size();
289 if (n == 0) return tuple();
290 if (n == 1) return ops[0]->zonk();
291
292 auto zops = Def::zonk(ops);
293 auto sigma = Tuple::infer(*this, zops);
294 auto t = tuple(sigma, zops);
295 auto new_t = Checker::assignable(sigma, t);
296 if (!new_t)
297 error(t->loc(), "cannot assign tuple '{}' of type '{}' to incompatible tuple type '{}'", t, t->type(), sigma);
298
299 return new_t;
300}
301
302const Def* World::tuple(const Def* type, Defs ops_) {
303 // TODO type-check type vs inferred type
304 type = type->zonk();
305 auto ops = Def::zonk(ops_);
306
307 auto n = ops.size();
308 if (!type->isa_mut<Sigma>()) {
309 if (n == 0) return tuple();
310 if (n == 1) return ops[0];
311 if (auto uni = Checker::is_uniform(ops)) return pack(n, uni);
312 }
313
314 if (n != 0) {
315 // eta rule for tuples:
316 // (extract(tup, 0), extract(tup, 1), extract(tup, 2)) -> tup
317 if (auto extract = ops[0]->isa<Extract>()) {
318 auto tup = extract->tuple();
319 bool eta = tup->type() == type;
320 for (size_t i = 0; i != n && eta; ++i) {
321 if (auto extract = ops[i]->isa<Extract>()) {
322 if (auto index = Lit::isa(extract->index())) {
323 if (eta &= u64(i) == *index) {
324 eta &= extract->tuple() == tup;
325 continue;
326 }
327 }
328 }
329 eta = false;
330 }
331
332 if (eta) return tup;
333 }
334 }
335
336 return unify<Tuple>(type, ops);
337}
338
339const Def* World::tuple(Sym sym) {
340 DefVec defs;
341 std::ranges::transform(sym, std::back_inserter(defs), [this](auto c) { return lit_i8(c); });
342 return tuple(defs);
343}
344
345const Def* World::extract(const Def* d, const Def* index) {
346 d = d->zonk();
347 index = index->zonk();
348
349 if (auto tuple = index->isa<Tuple>()) {
350 for (auto op : tuple->ops())
351 d = extract(d, op);
352 return d;
353 } else if (auto pack = index->isa<Pack>()) {
354 if (auto a = Lit::isa(index->arity())) {
355 for (nat_t i = 0, e = *a; i != e; ++i) {
356 auto idx = pack->has_var() ? pack->reduce(lit_idx(*a, i)) : pack->body();
357 d = extract(d, idx);
358 }
359 return d;
360 }
361 }
362
363 auto size = Idx::isa(index->type());
364 auto type = d->unfold_type();
365
366 if (size) {
367 if (auto l = Lit::isa(size); l && *l == 1) {
368 if (auto l = Lit::isa(index); !l || *l != 0) WLOG("unknown Idx of size 1: {}", index);
369 if (auto sigma = type->isa_mut<Sigma>(); sigma && sigma->num_ops() == 1) {
370 // mut sigmas can be 1-tuples; TODO mutables Arr?
371 } else {
372 return d;
373 }
374 }
375 }
376
377 if (auto pack = d->isa_imm<Pack>()) return pack->body();
378
379 if (size && !Checker::alpha<Checker::Check>(type->arity(), size))
380 error(index->loc(), "index '{}' does not fit within arity '{}'", index, type->arity());
381
382 // extract(insert(x, index, val), index) -> val
383 if (auto insert = d->isa<Insert>()) {
384 if (index == insert->index()) return insert->value();
385 }
386
387 if (auto i = Lit::isa(index)) {
388 if (auto hole = d->isa_mut<Hole>()) d = hole->tuplefy(Idx::as_lit(index->type()));
389 if (auto tuple = d->isa<Tuple>()) return tuple->op(*i);
390
391 // extract(insert(x, j, val), i) -> extract(x, i) where i != j (guaranteed by rule above)
392 if (auto insert = d->isa<Insert>()) {
393 if (insert->index()->isa<Lit>()) return extract(insert->tuple(), index);
394 }
395
396 if (auto sigma = type->isa<Sigma>()) {
397 if (auto var = sigma->has_var()) {
398 auto t = VarRewriter(var, d).rewrite(sigma->op(*i));
399 return unify<Extract>(t, d, index);
400 }
401
402 return unify<Extract>(sigma->op(*i), d, index);
403 }
404 }
405
406 const Def* elem_t;
407 if (auto arr = type->isa<Arr>())
408 elem_t = arr->reduce(index);
409 else
410 elem_t = join(type->as<Sigma>()->ops());
411
412 if (index->isa<Top>()) {
413 if (auto hole = Hole::isa_unset(d)) {
414 auto elem_hole = mut_hole(elem_t);
415 hole->set(pack(size, elem_hole));
416 return elem_hole;
417 }
418 }
419
420 assert(d);
421 return unify<Extract>(elem_t, d, index);
422}
423
424const Def* World::insert(const Def* d, const Def* index, const Def* val) {
425 d = d->zonk();
426 index = index->zonk();
427 val = val->zonk();
428
429 auto type = d->unfold_type();
430 auto size = Idx::isa(index->type());
431 auto lidx = Lit::isa(index);
432
433 if (!size) error(d->loc(), "index '{}' must be of type 'Idx' but is of type '{}'", index, index->type());
434
435 if (!Checker::alpha<Checker::Check>(type->arity(), size))
436 error(index->loc(), "index '{}' does not fit within arity '{}'", index, type->arity());
437
438 if (lidx) {
439 auto elem_type = type->proj(*lidx);
440 auto new_val = Checker::assignable(elem_type, val);
441 if (!new_val) {
442 throw Error()
443 .error(val->loc(), "value to be inserted not assignable to element")
444 .note(val->loc(), "vvv value type vvv \n'{}'\n'{}'", val->type(), elem_type)
445 .note(val->loc(), "^^^ element type ^^^", elem_type);
446 }
447 val = new_val;
448 }
449
450 if (auto l = Lit::isa(size); l && *l == 1)
451 return tuple(d, {val}); // d could be mut - that's why the tuple ctor is needed
452
453 // insert((a, b, c, d), 2, x) -> (a, b, x, d)
454 if (auto t = d->isa<Tuple>(); t && lidx) return t->refine(*lidx, val);
455
456 // insert(‹4; x›, 2, y) -> (x, x, y, x)
457 if (auto pack = d->isa<Pack>(); pack && lidx) {
458 if (auto a = Lit::isa(pack->arity()); a && *a < flags().scalarize_threshold) {
459 auto new_ops = DefVec(*a, pack->body());
460 new_ops[*lidx] = val;
461 return tuple(type, new_ops);
462 }
463 }
464
465 // insert(insert(x, index, y), index, val) -> insert(x, index, val)
466 if (auto insert = d->isa<Insert>()) {
467 if (insert->index() == index) d = insert->tuple();
468 }
469
470 return unify<Insert>(d, index, val);
471}
472
473const Def* World::seq(bool term, const Def* arity, const Def* body) {
474 arity = arity->zonk(); // TODO use zonk_mut all over the place and rmeove zonk from is_shape?
475 body = body->zonk();
476
477 auto arity_ty = arity->unfold_type();
478 if (!is_shape(arity_ty)) error(arity->loc(), "expected arity but got `{}` of type `{}`", arity, arity_ty);
479
480 if (auto a = Lit::isa(arity)) {
481 if (*a == 0) return unit(term);
482 if (*a == 1) return body;
483 }
484
485 // «(a, b, c); body» -> «a; «(b, c); body»»
486 if (auto tuple = arity->isa<Tuple>())
487 return seq(term, tuple->ops().front(), seq(term, tuple->ops().subspan(1), body));
488
489 // «‹n; x›; body» -> «x; «<n-1, x>; body»»
490 if (auto p = arity->isa<Pack>()) {
491 if (auto s = Lit::isa(p->arity())) return seq(term, p->body(), seq(term, pack(*s - 1, p->body()), body));
492 }
493
494 if (term) {
495 auto type = arr(arity, body->type());
496 return unify<Pack>(type, body);
497 } else {
498 return unify<Arr>(body->unfold_type(), arity, body);
499 }
500}
501
502const Def* World::seq(bool term, Defs shape, const Def* body) {
503 if (shape.empty()) return body;
504 return seq(term, shape.rsubspan(1), seq(term, shape.back(), body));
505}
506
507const Lit* World::lit(const Def* type, u64 val) {
508 type = type->zonk();
509
510 if (auto size = Idx::isa(type)) {
511 if (size->isa<Top>()) {
512 // unsafe but fine
513 } else if (auto s = Lit::isa(size)) {
514 if (*s != 0 && val >= *s) error(type->loc(), "index '{}' does not fit within arity '{}'", size, val);
515 } else if (val != 0) { // 0 of any size is allowed
516 error(type->loc(), "cannot create literal '{}' of 'Idx {}' as size is unknown", val, size);
517 }
518 }
519
520 return unify<Lit>(type, val);
521}
522
523/*
524 * set
525 */
526
527template<bool Up>
528const Def* World::ext(const Def* type) {
529 type = type->zonk();
530
531 if (auto arr = type->isa<Arr>()) return pack(arr->arity(), ext<Up>(arr->body()));
532 if (auto sigma = type->isa<Sigma>())
533 return tuple(sigma, DefVec(sigma->num_ops(), [&](size_t i) { return ext<Up>(sigma->op(i)); }));
534 return unify<TExt<Up>>(type);
535}
536
537template<bool Up>
538const Def* World::bound(Defs ops_) {
539 auto ops = DefVec();
540 for (size_t i = 0, e = ops_.size(); i != e; ++i) {
541 auto op = ops_[i]->zonk();
542 if (!op->isa<TExt<!Up>>()) ops.emplace_back(op); // ignore: ext<!Up>
543 }
544
545 auto kind = umax<UMax::Type>(ops);
546
547 // has ext<Up> value?
548 if (std::ranges::any_of(ops, [&](const Def* op) -> bool { return op->isa<TExt<Up>>(); })) return ext<Up>(kind);
549
550 // sort and remove duplicates
551 std::ranges::sort(ops, GIDLt<const Def*>());
552 ops.resize(std::distance(ops.begin(), std::unique(ops.begin(), ops.end())));
553
554 if (ops.size() == 0) return ext<!Up>(kind);
555 if (ops.size() == 1) return ops[0];
556
557 // TODO simplify mixed terms with joins and meets?
558 return unify<TBound<Up>>(kind, ops);
559}
560
561const Def* World::merge(const Def* type, Defs ops_) {
562 type = type->zonk();
563 auto ops = Def::zonk(ops_);
564
565 if (type->isa<Meet>()) {
566 auto types = DefVec(ops.size(), [&](size_t i) { return ops[i]->type(); });
567 return unify<Merge>(meet(types), ops);
568 }
569
570 assert(ops.size() == 1);
571 return ops[0];
572}
573
574const Def* World::merge(Defs ops_) {
575 auto ops = Def::zonk(ops_);
576 return merge(umax<UMax::Term>(ops), ops);
577}
578
579const Def* World::inj(const Def* type, const Def* value) {
580 type = type->zonk();
581 value = value->zonk();
582
583 if (type->isa<Join>()) return unify<Inj>(type, value);
584 return value;
585}
586
587const Def* World::split(const Def* type, const Def* value) {
588 type = type->zonk();
589 value = value->zonk();
590
591 return unify<Split>(type, value);
592}
593
594const Def* World::match(Defs ops_) {
595 auto ops = Def::zonk(ops_);
596 if (ops.size() == 1) return ops.front();
597
598 auto scrutinee = ops.front();
599 auto arms = ops.span().subspan(1);
600 auto join = scrutinee->type()->isa<Join>();
601
602 if (!join) error(scrutinee->loc(), "scrutinee of a test expression must be of union type");
603
604 if (arms.size() != join->num_ops())
605 error(scrutinee->loc(), "test expression has {} arms but union type has {} cases", arms.size(),
606 join->num_ops());
607
608 for (auto arm : arms)
609 if (!arm->type()->isa<Pi>())
610 error(arm->loc(), "arm of test expression does not have a function type but is of type '{}'", arm->type());
611
612 std::ranges::sort(arms, [](const Def* arm1, const Def* arm2) {
613 return arm1->type()->as<Pi>()->dom()->gid() < arm2->type()->as<Pi>()->dom()->gid();
614 });
615
616 const Def* type = nullptr;
617 for (size_t i = 0, e = arms.size(); i != e; ++i) {
618 auto arm = arms[i];
619 auto pi = arm->type()->as<Pi>();
620 if (!Checker::alpha<Checker::Check>(pi->dom(), join->op(i)))
621 error(arm->loc(),
622 "domain type '{}' of arm in a test expression does not match case type '{}' in union type", pi->dom(),
623 join->op(i));
624 type = type ? this->join({type, pi->codom()}) : pi->codom();
625 }
626
627 return unify<Match>(type, ops);
628}
629
630const Def* World::uniq(const Def* inhabitant) {
631 inhabitant = inhabitant->zonk();
632 return unify<Uniq>(inhabitant->type()->unfold_type(), inhabitant);
633}
634
635Sym World::append_suffix(Sym symbol, std::string suffix) {
636 auto name = symbol.str();
637
638 auto pos = name.find(suffix);
639 if (pos != std::string::npos) {
640 auto num = name.substr(pos + suffix.size());
641 if (num.empty()) {
642 name += "_1";
643 } else {
644 num = num.substr(1);
645 num = std::to_string(std::stoi(num) + 1);
646 name = name.substr(0, pos + suffix.size()) + "_" + num;
647 }
648 } else {
649 name += suffix;
650 }
651
652 return sym(std::move(name));
653}
654
655Defs World::reduce(const Var* var, const Def* arg) {
656 auto mut = var->mut();
657 auto offset = mut->reduction_offset();
658 auto size = mut->num_ops() - offset;
659
660 if (auto i = move_.substs.find({var, arg}); i != move_.substs.end()) return i->second->defs();
661
662 auto buf = move_.arena.substs.allocate(sizeof(Reduct) + size * sizeof(const Def*), alignof(const Def*));
663 auto reduct = new (buf) Reduct(size);
664 auto rw = VarRewriter(var, arg);
665 for (size_t i = 0; i != size; ++i)
666 reduct->defs_[i] = rw.rewrite(mut->op(i + offset));
667 assert_emplace(move_.substs, std::pair{var, arg}, reduct);
668 return reduct->defs();
669}
670
671void World::for_each(bool elide_empty, std::function<void(Def*)> f) {
673 for (auto mut : externals())
674 queue.push(mut);
675
676 while (!queue.empty()) {
677 auto mut = queue.pop();
678 if (mut && mut->is_closed() && (!elide_empty || mut->is_set())) f(mut);
679
680 for (auto op : mut->deps())
681 for (auto mut : op->local_muts())
682 queue.push(mut);
683 }
684}
685
686/*
687 * debugging
688 */
689
690#ifdef MIM_ENABLE_CHECKS
691
692void World::breakpoint(u32 gid) { state_.breakpoints.emplace(gid); }
693void World::watchpoint(u32 gid) { state_.watchpoints.emplace(gid); }
694
695const Def* World::gid2def(u32 gid) {
696 auto i = std::ranges::find_if(move_.defs, [=](auto def) { return def->gid() == gid; });
697 if (i == move_.defs.end()) return nullptr;
698 return *i;
699}
700
702 for (auto mut : externals())
703 assert(mut->is_closed() && mut->is_set());
704 for (auto anx : annexes())
705 assert(anx->is_closed());
706 return *this;
707}
708
709#endif
710
711#ifndef DOXYGEN
712template const Def* World::umax<UMax::Term>(Defs);
713template const Def* World::umax<UMax::Type>(Defs);
714template const Def* World::umax<UMax::Kind>(Defs);
715template const Def* World::umax<UMax::Univ>(Defs);
716template const Def* World::ext<true>(const Def*);
717template const Def* World::ext<false>(const Def*);
718template const Def* World::bound<true>(Defs);
719template const Def* World::bound<false>(Defs);
720template const Def* World::app<true>(const Def*, const Def*);
721template const Def* World::app<false>(const Def*, const Def*);
722template const Def* World::implicit_app<true>(const Def*, const Def*);
723template const Def* World::implicit_app<false>(const Def*, const Def*);
724#endif
725
726} // namespace mim
A (possibly paramterized) Array.
Definition tuple.h:117
Definition axm.h:9
static constexpr u8 Trip_End
Definition axm.h:134
static std::tuple< const Axm *, u8, u8 > get(const Def *def)
Yields currying counter of def.
Definition axm.cpp:38
static const Def * is_uniform(Defs defs)
Yields defs.front(), if all defs are Check::alpha-equivalent (Mode::Test) and nullptr otherwise.
Definition check.cpp:115
static bool alpha(const Def *d1, const Def *d2)
Definition check.h:96
static const Def * assignable(const Def *type, const Def *value)
Can value be assigned to sth of type?
Definition check.h:103
Base class for all Defs.
Definition def.h:251
Defs deps() const noexcept
Definition def.cpp:470
const Def * zonk() const
If Holes have been filled, reconstruct the program without them.
Definition check.cpp:21
constexpr auto ops() const noexcept
Definition def.h:305
T * isa_mut() const
If this is mutable, it will cast constness away and perform a dynamic_cast to T.
Definition def.h:485
const Def * unfold_type() const
Yields the type of this Def and builds a new Type (UInc n) if necessary.
Definition def.cpp:452
Muts local_muts() const
Mutables reachable by following immutable deps(); mut->local_muts() is by definition the set { mut }...
Definition def.cpp:332
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.cpp:447
bool is_external() const noexcept
Definition def.h:467
Loc loc() const
Definition def.h:506
Sym sym() const
Definition def.h:507
const Def * var_type()
If this is a binder, compute the type of its Variable.
Definition def.cpp:314
constexpr u32 gid() const noexcept
Global id - unique number for this Def.
Definition def.h:270
virtual const Def * arity() const
Definition def.cpp:553
const T * isa_imm() const
Definition def.h:479
bool is_closed() const
Has no free_vars()?
Definition def.cpp:418
Some "global" variables needed all over the place.
Definition driver.h:17
Log & log() const
Definition driver.h:25
Flags & flags()
Definition driver.h:23
Error & error(Loc loc, const char *s, Args &&... args)
Definition dbg.h:72
Error & note(Loc loc, const char *s, Args &&... args)
Definition dbg.h:74
This node is a hole in the IR that is inferred by its context later on.
Definition check.h:14
static Hole * isa_unset(const Def *def)
Definition check.h:53
static nat_t as_lit(const Def *def)
Definition def.h:880
static const Def * isa(const Def *def)
Checks if def is a Idx s and returns s or nullptr otherwise.
Definition def.cpp:613
Creates a new Tuple / Pack by inserting Insert::value at position Insert::index into Insert::tuple.
Definition tuple.h:233
A function.
Definition lam.h:111
static std::optional< T > isa(const Def *def)
Definition def.h:824
Facility to log what you are doing.
Definition log.h:17
A (possibly paramterized) Tuple.
Definition tuple.h:166
A dependent function type.
Definition lam.h:15
static Pi * isa_implicit(const Def *d)
Is d an Pi::is_implicit (mutable) Pi?
Definition lam.h:55
A dependent tuple type.
Definition tuple.h:20
static const Def * infer(World &, Defs)
Definition check.cpp:292
Extremum. Either Top (Up) or Bottom.
Definition lattice.h:152
Data constructor for a Sigma.
Definition tuple.h:68
static const Def * infer(World &, Defs)
Definition check.cpp:285
@ Type
Definition def.h:745
@ Univ
Definition def.h:745
@ Term
Definition def.h:745
@ Kind
Definition def.h:745
const Def * rewrite(const Def *) final
Definition rewrite.cpp:181
A variable introduced by a binder (mutable).
Definition def.h:700
const Lit * lit_idx(nat_t size, u64 val)
Constructs a Lit of type Idx of size size.
Definition world.h:439
const Def * insert(const Def *d, const Def *i, const Def *val)
Definition world.cpp:424
const Def * meet(Defs ops)
Definition world.h:481
const Def * uinc(const Def *op, level_t offset=1)
Definition world.cpp:116
const Lit * lit(const Def *type, u64 val)
Definition world.cpp:507
const Lit * lit_i8()
Definition world.h:433
void watchpoint(u32 gid)
Trigger breakpoint in your debugger when Def::setting a Def with this gid.
Definition world.cpp:693
const Type * type(const Def *level)
Definition world.cpp:107
void make_external(Def *)
Definition world.cpp:89
const Driver & driver() const
Definition world.h:87
const Lit * lit_tt()
Definition world.h:466
const Def * filter(Lam::Filter filter)
Definition world.h:289
World(Driver *)
Definition world.cpp:60
const Def * sigma(Defs ops)
Definition world.cpp:277
const Def * pack(const Def *arity, const Def *body)
Definition world.h:376
const Def * unit(bool term)
Definition world.h:359
const Def * app(const Def *callee, const Def *arg)
Definition world.cpp:195
const Def * match(Defs)
Definition world.cpp:594
const Pi * pi(const Def *dom, const Def *codom, bool implicit=false)
Definition world.h:265
const Def * seq(bool term, const Def *arity, const Def *body)
Definition world.cpp:473
World & verify()
Verifies that all externals() and annexes() are Def::is_closed(), if MIM_ENABLE_CHECKS.
Definition world.cpp:701
const Idx * type_idx()
Definition world.h:499
const Lit * lit_univ_0()
Definition world.h:424
Sym name() const
Definition world.h:91
void for_each(bool elide_empty, std::function< void(Def *)>)
Definition world.cpp:671
const Lit * lit_univ_1()
Definition world.h:425
const Nat * type_nat()
Definition world.h:498
Hole * mut_hole(const Def *type)
Definition world.h:232
const Lam * lam(const Pi *pi, Lam::Filter f, const Def *body)
Definition world.h:293
const Def * tuple(Defs ops)
Definition world.cpp:287
const Def * gid2def(u32 gid)
Lookup Def by gid.
Definition world.cpp:695
Flags & flags()
Retrieve compile Flags.
Definition world.cpp:73
const Def * implicit_app(const Def *callee, const Def *arg)
Places Holes as demanded by Pi::is_implicit() and then apps arg.
Definition world.cpp:188
const Def * inj(const Def *type, const Def *value)
Definition world.cpp:579
const Type * type()
Definition world.h:221
const Axm * axm(NormalizeFn n, u8 curry, u8 trip, const Def *type, plugin_t p, tag_t t, sub_t s)
Definition world.h:247
const Def * extract(const Def *d, const Def *i)
Definition world.cpp:345
auto externals() const
Definition world.h:206
const Def * arr(const Def *arity, const Def *body)
Definition world.h:375
Sym sym(std::string_view)
Definition world.cpp:76
const Lit * lit_ff()
Definition world.h:465
const Def * bound(Defs ops)
Definition world.cpp:538
const Def * join(Defs ops)
Definition world.h:480
const Def * ext(const Def *type)
Definition world.cpp:528
Sym append_suffix(Sym name, std::string suffix)
Appends a suffix or an increasing number if the suffix already exists.
Definition world.cpp:635
void make_internal(Def *)
Definition world.cpp:96
const Lit * lit_idx_1_0()
Definition world.h:430
const Lit * lit_univ(u64 level)
Definition world.h:423
const Def * var(Def *mut)
Definition world.cpp:178
const Tuple * tuple()
the unit value of type []
Definition world.h:396
const Def * uniq(const Def *inhabitant)
Definition world.cpp:630
const Def * raw_app(const Axm *axm, u8 curry, u8 trip, const Def *type, const Def *callee, const Def *arg)
Definition world.cpp:273
const Def * umax(Defs)
Definition world.cpp:136
const Def * merge(const Def *type, Defs ops)
Definition world.cpp:561
const Sigma * sigma()
The unit type within Type 0.
Definition world.h:353
const Lit * lit_nat(nat_t a)
Definition world.h:426
const State & state() const
Definition world.h:86
const Def * register_annex(flags_t f, const Def *)
Definition world.cpp:79
Defs reduce(const Var *var, const Def *arg)
Yields the new body of [mut->var() -> arg]mut.
Definition world.cpp:655
void breakpoint(u32 gid)
Trigger breakpoint in your debugger when creating a Def with this gid.
Definition world.cpp:692
const Def * split(const Def *type, const Def *value)
Definition world.cpp:587
auto annexes() const
Definition world.h:178
Log & log() const
Definition world.cpp:72
bool empty() const
Definition util.h:168
bool push(T val)
Definition util.h:160
#define WLOG(...)
Definition log.h:90
#define TLOG(...)
Definition log.h:96
#define DLOG(...)
Vaporizes to nothingness in Debug build.
Definition log.h:95
Definition ast.h:14
View< const Def * > Defs
Definition def.h:76
u64 nat_t
Definition types.h:43
Vector< const Def * > DefVec
Definition def.h:77
auto assert_emplace(C &container, Args &&... args)
Invokes emplace on container, asserts that insertion actually happened, and returns the iterator.
Definition util.h:118
u64 flags_t
Definition types.h:45
TBound< true > Join
AKA union.
Definition lattice.h:174
void error(Loc loc, const char *f, Args &&... args)
Definition dbg.h:125
u64 level_t
Definition types.h:42
TExt< true > Top
Definition lattice.h:172
uint32_t u32
Definition types.h:34
static void flatten_umax(DefVec &ops, const Def *def)
Definition world.cpp:127
uint64_t u64
Definition types.h:34
uint8_t u8
Definition types.h:34
TBound< false > Meet
AKA intersection.
Definition lattice.h:173
Compiler switches that must be saved and looked up in later phases of compilation.
Definition flags.h:11
static Sym demangle(Driver &, plugin_t plugin)
Reverts an Axm::mangled string to a Sym.
Definition plugin.cpp:37