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