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