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();
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 elem_t = extract(tuple(type->as<Sigma>()->ops()), index);
378
379 assert(d);
380 return unify<Extract>(2, elem_t, d, index);
381}
382
383const Def* World::insert(const Def* d, const Def* index, const Def* val) {
384 auto type = d->unfold_type();
385 auto size = Idx::isa(index->type());
386 auto lidx = Lit::isa(index);
387
388 if (!Checker::alpha<Checker::Check>(type->arity(), size))
389 error(index->loc(), "index '{}' does not fit within arity '{}'", index, type->arity());
390
391 if (lidx) {
392 auto elem_type = type->proj(*lidx);
393 auto new_val = Checker::assignable(elem_type, val);
394 if (!new_val) {
395 throw Error()
396 .error(val->loc(), "value to be inserted not assignable to element")
397 .note(val->loc(), "vvv value type vvv \n'{}'\n'{}'", val->type(), elem_type)
398 .note(val->loc(), "^^^ element type ^^^", elem_type);
399 }
400 val = new_val;
401 }
402
403 if (auto l = Lit::isa(size); l && *l == 1)
404 return tuple(d, {val}); // d could be mut - that's why the tuple ctor is needed
405
406 // insert((a, b, c, d), 2, x) -> (a, b, x, d)
407 if (auto t = d->isa<Tuple>(); t && lidx) return t->refine(*lidx, val);
408
409 // insert(‹4; x›, 2, y) -> (x, x, y, x)
410 if (auto pack = d->isa<Pack>(); pack && lidx) {
411 if (auto a = pack->isa_lit_arity(); a && *a < flags().scalarize_threshold) {
412 auto new_ops = DefVec(*a, pack->body());
413 new_ops[*lidx] = val;
414 return tuple(type, new_ops);
415 }
416 }
417
418 // insert(insert(x, index, y), index, val) -> insert(x, index, val)
419 if (auto insert = d->isa<Insert>()) {
420 if (insert->index() == index) d = insert->tuple();
421 }
422
423 return unify<Insert>(3, d, index, val);
424}
425
426// TODO merge this code with pack
427const Def* World::arr(const Def* shape, const Def* body) {
428 if (!is_shape(shape->type())) error(shape->loc(), "expected shape but got '{}' of type '{}'", shape, shape->type());
429
430 if (auto a = Lit::isa(shape)) {
431 if (*a == 0) return sigma();
432 if (*a == 1) return body;
433 }
434
435 // «(a, b)#i; T» -> («a, T», <b, T»)#i
436 if (auto ex = shape->isa<Extract>()) {
437 if (auto tup = ex->tuple()->isa<Tuple>()) {
438 auto arrs = DefVec(tup->num_ops(), [&](size_t i) { return arr(tup->op(i), body); });
439 return extract(tuple(arrs), ex->index());
440 }
441 }
442
443 // «(a, b, c); body» -> «a; «(b, c); body»»
444 if (auto tuple = shape->isa<Tuple>()) return arr(tuple->ops().front(), arr(tuple->ops().subspan(1), body));
445
446 // «<n; x>; body» -> «x; «<n-1, x>; body»»
447 if (auto p = shape->isa<Pack>()) {
448 if (auto s = Lit::isa(p->shape())) return arr(*s, arr(pack(*s - 1, p->body()), body));
449 }
450
451 return unify<Arr>(2, body->unfold_type(), shape, body);
452}
453
454const Def* World::pack(const Def* shape, const Def* body) {
455 if (!is_shape(shape->type())) error(shape->loc(), "expected shape but got '{}' of type '{}'", shape, shape->type());
456
457 if (auto a = Lit::isa(shape)) {
458 if (*a == 0) return tuple();
459 if (*a == 1) return body;
460 }
461
462 // <(a, b, c); body> -> <a; «(b, c); body>>
463 if (auto tuple = shape->isa<Tuple>()) return pack(tuple->ops().front(), pack(tuple->ops().subspan(1), body));
464
465 // <<n; x>; body> -> <x; <<n-1, x>; body>>
466 if (auto p = shape->isa<Pack>()) {
467 if (auto s = Lit::isa(p->shape())) return pack(*s, pack(pack(*s - 1, p->body()), body));
468 }
469
470 auto type = arr(shape, body->type());
471 return unify<Pack>(1, type, body);
472}
473
474const Def* World::arr(Defs shape, const Def* body) {
475 if (shape.empty()) return body;
476 return arr(shape.rsubspan(1), arr(shape.back(), body));
477}
478
479const Def* World::pack(Defs shape, const Def* body) {
480 if (shape.empty()) return body;
481 return pack(shape.rsubspan(1), pack(shape.back(), body));
482}
483
484const Lit* World::lit(const Def* type, u64 val) {
485 if (auto size = Idx::isa(type)) {
486 if (auto s = Lit::isa(size)) {
487 if (*s != 0 && val >= *s) error(type->loc(), "index '{}' does not fit within arity '{}'", size, val);
488 } else if (val != 0) { // 0 of any size is allowed
489 error(type->loc(), "cannot create literal '{}' of 'Idx {}' as size is unknown", val, size);
490 }
491 }
492
493 return unify<Lit>(0, type, val);
494}
495
496/*
497 * set
498 */
499
500template<bool Up> const Def* World::ext(const Def* type) {
501 if (auto arr = type->isa<Arr>()) return pack(arr->shape(), ext<Up>(arr->body()));
502 if (auto sigma = type->isa<Sigma>())
503 return tuple(sigma, DefVec(sigma->num_ops(), [&](size_t i) { return ext<Up>(sigma->op(i)); }));
504 return unify<TExt<Up>>(0, type);
505}
506
507template<bool Up> const Def* World::bound(Defs ops) {
508 auto kind = umax<Sort::Type>(ops);
509
510 // has ext<Up> value?
511 if (std::ranges::any_of(ops, [&](const Def* op) { return Up ? bool(op->isa<Top>()) : bool(op->isa<Bot>()); }))
512 return ext<Up>(kind);
513
514 // ignore: ext<!Up>
515 DefVec cpy(ops.begin(), ops.end());
516 auto [_, end] = std::ranges::copy_if(ops, cpy.begin(), [&](const Def* op) { return !op->isa<Ext>(); });
517
518 // sort and remove duplicates
519 std::sort(cpy.begin(), end, GIDLt<const Def*>());
520 end = std::unique(cpy.begin(), end);
521 cpy.resize(std::distance(cpy.begin(), end));
522
523 if (cpy.size() == 0) return ext<!Up>(kind);
524 if (cpy.size() == 1) return cpy[0];
525
526 // TODO simplify mixed terms with joins and meets?
527
528 return unify<TBound<Up>>(cpy.size(), kind, cpy);
529}
530
531const Def* World::merge(const Def* type, Defs ops) {
532 if (type->isa<Meet>()) {
533 auto types = DefVec(ops.size(), [&](size_t i) { return ops[i]->type(); });
534 return unify<Merge>(ops.size(), meet(types), ops);
535 }
536
537 assert(ops.size() == 1);
538 return ops[0];
539}
540
541const Def* World::merge(Defs ops) { return merge(umax<Sort::Term>(ops), ops); }
542
543const Def* World::inj(const Def* type, const Def* value) {
544 if (type->isa<Join>()) return unify<Inj>(1, type, value);
545 return value;
546}
547
548const Def* World::split(const Def* type, const Def* value) { return unify<Split>(1, type, value); }
549
550const Def* World::match(Defs ops_) {
551 if (ops_.size() == 1) return ops_.front();
552
553 auto ops = DefVec(ops_.begin(), ops_.end());
554 auto value = ops.front();
555 auto arms = ops.span().subspan(1);
556 auto join = value->type()->isa<Join>();
557
558 if (!join) error(value->loc(), "scrutinee of a test expression must be of union type");
559
560 if (arms.size() != join->num_ops())
561 error(value->loc(), "test expression has {} arms but union type has {} cases", arms.size(), join->num_ops());
562
563 for (auto arm : arms)
564 if (!arm->type()->isa<Pi>())
565 error(arm->loc(), "arm of test expression does not have a function type but is of type '{}'", arm->type());
566
567 std::ranges::sort(arms, [](const Def* arm1, const Def* arm2) {
568 return arm1->type()->as<Pi>()->dom()->gid() < arm2->type()->as<Pi>()->dom()->gid();
569 });
570
571 const Def* type = nullptr;
572 for (size_t i = 0, e = arms.size(); i != e; ++i) {
573 auto arm = arms[i];
574 auto pi = arm->type()->as<Pi>();
575 if (!Checker::alpha<Checker::Check>(pi->dom(), join->op(i)))
576 error(arm->loc(),
577 "domain type '{}' of arm in a test expression does not match case type '{}' in union type", pi->dom(),
578 join->op(i));
579 type = type ? this->join({type, pi->codom()}) : pi->codom();
580 }
581
582 return unify<Match>(ops.size(), type, ops);
583}
584
585const Def* World::uniq(const Def* inhabitant) { return unify<Uniq>(1, inhabitant->type()->unfold_type(), inhabitant); }
586
587Sym World::append_suffix(Sym symbol, std::string suffix) {
588 auto name = symbol.str();
589
590 auto pos = name.find(suffix);
591 if (pos != std::string::npos) {
592 auto num = name.substr(pos + suffix.size());
593 if (num.empty()) {
594 name += "_1";
595 } else {
596 num = num.substr(1);
597 num = std::to_string(std::stoi(num) + 1);
598 name = name.substr(0, pos + suffix.size()) + "_" + num;
599 }
600 } else {
601 name += suffix;
602 }
603
604 return sym(std::move(name));
605}
606
607Defs World::reduce(const Var* var, const Def* arg) {
608 auto mut = var->mut();
609 auto offset = mut->reduction_offset();
610 auto size = mut->num_ops() - offset;
611
612 if (auto i = move_.substs.find({var, arg}); i != move_.substs.end()) return i->second->defs();
613
614 auto buf = move_.arena.substs.allocate(sizeof(Reduct) + size * sizeof(const Def*), alignof(const Def*));
615 auto reduct = new (buf) Reduct(size);
616 auto rw = VarRewriter(var, arg);
617 for (size_t i = 0; i != size; ++i) reduct->defs_[i] = rw.rewrite(mut->op(i + offset));
618 assert_emplace(move_.substs, std::pair{var, arg}, reduct);
619 return reduct->defs();
620}
621
622/*
623 * debugging
624 */
625
626#ifdef MIM_ENABLE_CHECKS
627
628void World::breakpoint(u32 gid) { state_.breakpoints.emplace(gid); }
629
630const Def* World::gid2def(u32 gid) {
631 auto i = std::ranges::find_if(move_.defs, [=](auto def) { return def->gid() == gid; });
632 if (i == move_.defs.end()) return nullptr;
633 return *i;
634}
635
637 for (auto mut : externals()) assert(mut->is_closed() && mut->is_set());
638 for (auto anx : annexes()) assert(anx->is_closed());
639 return *this;
640}
641
642#endif
643
644#ifndef DOXYGEN
645template const Def* World::umax<Sort::Term>(Defs);
646template const Def* World::umax<Sort::Type>(Defs);
647template const Def* World::umax<Sort::Kind>(Defs);
648template const Def* World::umax<Sort::Univ>(Defs);
649template const Def* World::ext<true>(const Def*);
650template const Def* World::ext<false>(const Def*);
651template const Def* World::bound<true>(Defs);
652template const Def* World::bound<false>(Defs);
653template const Def* World::app<true>(const Def*, const Def*);
654template const Def* World::app<false>(const Def*, const Def*);
655template const Def* World::implicit_app<true>(const Def*, const Def*);
656template const Def* World::implicit_app<false>(const Def*, const Def*);
657#endif
658
659} // 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:240
static bool alpha(const Def *d1, const Def *d2)
Definition check.h:71
static const Def * assignable(const Def *type, const Def *value)
Can value be assigned to sth of type?
Definition check.h:77
Base class for all Defs.
Definition def.h:197
const Def * zonk() const
Definition check.cpp:35
nat_t as_lit_arity() const
Definition def.h:251
constexpr auto ops() const noexcept
Definition def.h:260
T * isa_mut() const
If this is mutable, it will cast constness away and perform a dynamic_cast to T.
Definition def.h:429
const Def * op(size_t i) const noexcept
Definition def.h:263
bool is_external() const
Definition def.h:413
const Def * unfold_type() const
Yields the type of this Def and builds a new Type (UInc n) if necessary.
Definition def.cpp:394
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.h:241
Loc loc() const
Definition def.h:449
Sym sym() const
Definition def.h:450
constexpr u32 gid() const noexcept
Global id - unique number for this Def.
Definition def.h:216
const T * isa_imm() const
Definition def.h:423
bool is_closed() const
Has no free_vars()?
Definition def.cpp:366
constexpr size_t num_ops() const noexcept
Definition def.h:264
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 const Def * isa(const Def *def)
Checks if def is a Idx s and returns s or nullptr otherwise.
Definition def.cpp:529
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:712
static T as(const Def *def)
Definition def.h:717
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:11
A dependent tuple type.
Definition tuple.h:9
static const Def * infer(World &, Defs)
Definition check.cpp:267
Data constructor for a Sigma.
Definition tuple.h:56
static const Def * infer(World &, Defs)
Definition check.cpp:261
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:383
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:484
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:454
const Def * app(const Def *callee, const Def *arg)
Definition world.cpp:181
const Def * match(Defs)
Definition world.cpp:550
const Def * arr(const Def *shape, const Def *body)
Definition world.cpp:427
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:636
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:630
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:543
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:507
const Def * join(Defs ops)
Definition world.h:435
const Def * ext(const Def *type)
Definition world.cpp:500
Sym append_suffix(Sym name, std::string suffix)
Appends a suffix or an increasing number if the suffix already exists.
Definition world.cpp:587
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:585
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:531
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:607
void breakpoint(u32 gid)
Trigger breakpoint in your debugger when creating Def with Def::gid gid.
Definition world.cpp:628
const Def * split(const Def *type, const Def *value)
Definition world.cpp:548
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:48
u64 nat_t
Definition types.h:43
Vector< const Def * > DefVec
Definition def.h:49
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:93
@ Type
Definition def.h:93
@ Term
Definition def.h:93
@ Kind
Definition def.h:93
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