MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
def.cpp
Go to the documentation of this file.
1#include "mim/def.h"
2
3#include <algorithm>
4
5#include <absl/container/fixed_array.h>
6#include <fe/assert.h>
7
8#include "mim/world.h"
9
10#include "mim/util/hash.h"
11
12using namespace std::literals;
13
14namespace mim {
15
16template void Sets<const Var>::dot();
17template void Sets<Def>::dot();
18
19/*
20 * constructors
21 */
22
23Def::Def(World* world, Node node, const Def* type, Defs ops, flags_t flags)
24 : world_(world)
25 , flags_(flags)
26 , node_(node)
27 , mut_(false)
28 , external_(false)
29 , dep_(node == Node::Hole ? unsigned(Dep::Hole)
30 : node == Node::Proxy ? unsigned(Dep::Proxy)
31 : node == Node::Var ? (Dep::Var | Dep::Mut)
32 : 0)
33 , num_ops_(ops.size())
34 , type_(type) {
35 if (node == Node::Univ) {
36 gid_ = world->next_gid();
38 } else if (auto var = isa<Var>()) {
39 assert(flags_ == 0); // if we ever need flags here, we need to hash that
40 gid_ = type->world().next_gid();
41 vars_ = Vars(var);
42 dep_ |= type->dep_;
43 auto op = ops[0];
44 ops_ptr()[0] = op;
45 hash_ = hash_begin(node_t(Node::Var));
46 hash_ = hash_combine(hash_, type->gid());
47 hash_ = hash_combine(hash_, op->gid());
48 } else {
50 Sets<Def>* muts;
51 hash_ = hash_begin(u8(node));
52 hash_ = hash_combine(hash_, flags_);
53
54 if (type) {
55 world = &type->world();
56 vars = &world->vars();
57 muts = &world->muts();
58 dep_ |= type->dep_;
59 vars_ = vars->merge(vars_, type->local_vars());
60 muts_ = muts->merge(muts_, type->local_muts());
61 hash_ = hash_combine(hash_, type->gid());
62 } else {
63 world = &ops[0]->world();
64 vars = &world->vars();
65 muts = &world->muts();
66 }
67
68 gid_ = world->next_gid();
69 auto ptr = ops_ptr();
70 for (size_t i = 0, e = ops.size(); i != e; ++i) {
71 auto op = ops[i];
72 ptr[i] = op;
73 dep_ |= op->dep_;
74 vars_ = vars->merge(vars_, op->local_vars());
75 muts_ = muts->merge(muts_, op->local_muts());
76 hash_ = hash_combine(hash_, op->gid());
77 }
78 }
79}
80
81Def::Def(Node n, const Def* type, Defs ops, flags_t flags)
82 : Def(nullptr, n, type, ops, flags) {}
83
84Def::Def(Node node, const Def* type, size_t num_ops, flags_t flags)
85 : flags_(flags)
86 , node_(node)
87 , mut_(true)
88 , external_(false)
89 , dep_(Dep::Mut | (node == Node::Hole ? Dep::Hole : Dep::None))
90 , num_ops_(num_ops)
91 , type_(type) {
92 gid_ = world().next_gid();
93 hash_ = mim::hash(gid());
94 var_ = nullptr;
95 std::fill_n(ops_ptr(), num_ops, nullptr);
96}
97
98Nat::Nat(World& world)
99 : Def(Node, world.type(), Defs{}, 0) {}
100
101UMax::UMax(World& world, Defs ops)
102 : Def(Node, world.univ(), ops, 0) {}
103
104// clang-format off
105
106/*
107 * rebuild
108 */
109
110const Def* Hole ::rebuild_(World&, const Def*, Defs ) const { fe::unreachable(); }
111const Def* Global ::rebuild_(World&, const Def*, Defs ) const { fe::unreachable(); }
112const Def* Idx ::rebuild_(World& w, const Def* , Defs ) const { return w.type_idx(); }
113const Def* Nat ::rebuild_(World& w, const Def* , Defs ) const { return w.type_nat(); }
114const Def* Univ ::rebuild_(World& w, const Def* , Defs ) const { return w.univ(); }
115const Def* App ::rebuild_(World& w, const Def* , Defs o) const { return w.app(o[0], o[1]); }
116const Def* Arr ::rebuild_(World& w, const Def* , Defs o) const { return w.arr(o[0], o[1]); }
117const Def* Extract::rebuild_(World& w, const Def* , Defs o) const { return w.extract(o[0], o[1]); }
118const Def* Inj ::rebuild_(World& w, const Def* t, Defs o) const { return w.inj(t, o[0])->set(dbg()); }
119const Def* Insert ::rebuild_(World& w, const Def* , Defs o) const { return w.insert(o[0], o[1], o[2]); }
120const Def* Lam ::rebuild_(World& w, const Def* t, Defs o) const { return w.lam(t->as<Pi>(), o[0], o[1]); }
121const Def* Lit ::rebuild_(World& w, const Def* t, Defs ) const { return w.lit(t, get()); }
122const Def* Merge ::rebuild_(World& w, const Def* t, Defs o) const { return w.merge(t, o); }
123const Def* Pack ::rebuild_(World& w, const Def* t, Defs o) const { return w.pack(t->arity(), o[0]); }
124const Def* Pi ::rebuild_(World& w, const Def* , Defs o) const { return w.pi(o[0], o[1], is_implicit()); }
125const Def* Proxy ::rebuild_(World& w, const Def* t, Defs o) const { return w.proxy(t, o, pass(), tag()); }
126const Def* Sigma ::rebuild_(World& w, const Def* , Defs o) const { return w.sigma(o); }
127const Def* Split ::rebuild_(World& w, const Def* t, Defs o) const { return w.split(t, o[0]); }
128const Def* Match ::rebuild_(World& w, const Def* , Defs o) const { return w.match(o); }
129const Def* Tuple ::rebuild_(World& w, const Def* t, Defs o) const { return w.tuple(t, o); }
130const Def* Type ::rebuild_(World& w, const Def* , Defs o) const { return w.type(o[0]); }
131const Def* UInc ::rebuild_(World& w, const Def* , Defs o) const { return w.uinc(o[0], offset()); }
132const Def* UMax ::rebuild_(World& w, const Def* , Defs o) const { return w.umax(o); }
133const Def* Uniq ::rebuild_(World& w, const Def* , Defs o) const { return w.uniq(o[0]); }
134const Def* Var ::rebuild_(World& w, const Def* t, Defs o) const { return w.var(t, o[0]->as_mut()); }
135
136const Def* Axm ::rebuild_(World& w, const Def* t, Defs ) const {
137 if (&w != &world()) return w.axm(normalizer(), curry(), trip(), t, plugin(), tag(), sub())->set(dbg());
139 return this;
140}
141
142template<bool up> const Def* TExt <up>::rebuild_(World& w, const Def* t, Defs ) const { return w.ext <up>(t)->set(dbg()); }
143template<bool up> const Def* TBound<up>::rebuild_(World& w, const Def* , Defs o) const { return w.bound<up>(o)->set(dbg()); }
144
145/*
146 * stub
147 */
148
149Arr* Arr ::stub_(World& w, const Def* t) { return w.mut_arr (t); }
150Global* Global::stub_(World& w, const Def* t) { return w.global (t, is_mutable()); }
151Hole* Hole ::stub_(World& w, const Def* t) { return w.mut_hole(t); }
152Lam* Lam ::stub_(World& w, const Def* t) { return w.mut_lam (t->as<Pi>()); }
153Pack* Pack ::stub_(World& w, const Def* t) { return w.mut_pack (t); }
154Pi* Pi ::stub_(World& w, const Def* t) { return w.mut_pi (t, is_implicit()); }
155Sigma* Sigma ::stub_(World& w, const Def* t) { return w.mut_sigma(t, num_ops()); }
156
157/*
158 * instantiate templates
159 */
160
161#ifndef DOXYGEN
162template const Def* TExt<false> ::rebuild_(World&, const Def*, Defs) const;
163template const Def* TExt<true > ::rebuild_(World&, const Def*, Defs) const;
164template const Def* TBound<false>::rebuild_(World&, const Def*, Defs) const;
165template const Def* TBound<true >::rebuild_(World&, const Def*, Defs) const;
166#endif
167
168// clang-format on
169
170/*
171 * immutabilize
172 */
173
175 if (auto v = has_var()) {
176 for (auto op : deps())
177 if (op->free_vars().contains(v)) return false;
178 }
179 for (auto op : deps()) {
180 for (auto mut : op->local_muts())
181 if (mut == this) return false; // recursion
182 }
183 return true;
184}
185
187 if (is_immutabilizable()) return world().pi(dom(), codom());
188 return nullptr;
189}
190
192 if (is_immutabilizable()) return static_cast<const Sigma*>(world().sigma(ops()));
193 return nullptr;
194}
195
196const Def* Arr::immutabilize() {
197 auto& w = world();
198 if (is_immutabilizable()) return w.arr(shape(), body());
199
200 if (auto n = Lit::isa(shape()); n && *n < w.flags().scalarize_threshold)
201 return w.sigma(DefVec(*n, [&](size_t i) { return reduce(w.lit_idx(*n, i)); }));
202
203 return nullptr;
204}
205
206const Def* Pack::immutabilize() {
207 auto& w = world();
208 if (is_immutabilizable()) return w.pack(shape(), body());
209
210 if (auto n = Lit::isa(shape()); n && *n < w.flags().scalarize_threshold)
211 return w.tuple(DefVec(*n, [&](size_t i) { return reduce(w.lit_idx(*n, i)); }));
212
213 return nullptr;
214}
215
216/*
217 * reduce
218 */
219
220Defs Def::reduce_(const Def* arg) const {
221 if (auto var = has_var()) return world().reduce(var, arg);
222 return {ops().begin() + reduction_offset(), num_ops() - reduction_offset()};
223}
224
225const Def* Def::refine(size_t i, const Def* new_op) const {
226 auto new_ops = absl::FixedArray<const Def*>(num_ops());
227 for (size_t j = 0, e = num_ops(); j != e; ++j) new_ops[j] = i == j ? new_op : op(j);
228 return rebuild(type(), new_ops);
229}
230
231/*
232 * Def - set
233 */
234
235// clang-format off
236Def* Def:: set(Defs ops) { assert(ops.size() == num_ops()); for (size_t i = 0, e = num_ops(); i != e; ++i) set(i, ops[i]); return this; }
237Def* Def::reset(Defs ops) { assert(ops.size() == num_ops()); for (size_t i = 0, e = num_ops(); i != e; ++i) reset(i, ops[i]); return this; }
238// clang-format on
239
240Def* Def::set(size_t i, const Def* def) {
241 invalidate();
242 def = check(i, def);
243 assert(def && !op(i) && curr_op_ == i);
244#ifndef NDEBUG
245 curr_op_ = (curr_op_ + 1) % num_ops();
246#endif
247 ops_ptr()[i] = def;
248
249 if (i == num_ops() - 1) { // set last op, so check kind
250 if (auto t = check(); t != type()) type_ = t;
251 }
252
253 return this;
254}
255
257 invalidate();
258#ifndef NDEBUG
259 curr_op_ = 0;
260#endif
261 for (size_t i = 0, e = num_ops(); i != e; ++i) {
262 if (op(i))
263 unset(i);
264 else {
265 assert(std::all_of(ops_ptr() + i + 1, ops_ptr() + num_ops(), [](auto op) { return !op; }));
266 break;
267 }
268 }
269 return this;
270}
271
272Def* Def::unset(size_t i) {
273 invalidate();
274 ops_ptr()[i] = nullptr;
275 return this;
276}
277
278bool Def::is_set() const {
279 if (num_ops() == 0) return true;
280 bool result = ops().back();
281 assert((!result || std::ranges::all_of(ops().rsubspan(1), [](auto op) { return op; }))
282 && "the last operand is set but others in front of it aren't");
283 return result;
284}
285
286/*
287 * free_vars
288 */
289
291 if (auto mut = isa_mut()) return Muts(mut);
292 return muts_;
293}
294
296 if (auto mut = isa_mut()) return mut->free_vars();
297
298 auto& vars = world().vars();
299 auto fvs = local_vars();
300 for (auto mut : local_muts()) fvs = vars.merge(fvs, mut->free_vars());
301
302 return fvs;
303}
304
305Vars Def::local_vars() const { return mut_ ? Vars() : vars_; }
306
308 if (!is_set()) return {};
309
310 if (mark_ == 0) {
311 // fixed-point iteration to recompute free vars:
312 // (run - 1) identifies the previous iteration; so make sure to offset run by 2 for the first iteration
313 auto& w = world();
314 w.next_run();
315 for (bool todo = true, cyclic = false; todo;) {
316 todo = false;
317 free_vars(todo, cyclic, w.next_run());
318 if (!cyclic) break; // triggers either immediately or never
319 }
320 }
321
322 return vars_;
323}
324
325Vars Def::free_vars(bool& todo, bool& cyclic, uint32_t run) {
326 // Recursively recompute free vars. If
327 // * mark_ == 0: invalid - need to recompute
328 // * mark_ == run - 1: Previous iteration - need to recompute
329 // * mark_ == run: We are running in cycles within the *current* iteration of our fixed-point loop
330 // * all other values for mark_: valid!
331 if (mark_ != 0 && mark_ != run - 1) return cyclic |= mark_ == run, vars_;
332 mark_ = run;
333
334 auto fvs0 = vars_;
335 auto fvs = fvs0;
336 auto& w = world();
337 auto& muts = w.muts();
338 auto& vars = w.vars();
339
340 for (auto op : deps()) {
341 fvs = vars.merge(fvs, op->local_vars());
342
343 for (auto mut : op->local_muts()) {
344 mut->muts_ = muts.insert(mut->muts_, this); // register "this" as user of local_mut
345 fvs = vars.merge(fvs, mut->free_vars(todo, cyclic, run));
346 }
347 }
348
349 if (auto var = has_var()) fvs = vars.erase(fvs, var); // FV(λx.e) = FV(e) \ {x}
350
351 todo |= fvs0 != fvs;
352 return vars_ = fvs;
353}
354
355void Def::invalidate() {
356 if (mark_ != 0) {
357 mark_ = 0;
358 if (vars_) { // only necessary, if the cached free vars are non-empty
359 for (auto mut : users()) mut->invalidate();
360 vars_ = Vars();
361 }
362 muts_ = Muts();
363 }
364}
365
366bool Def::is_closed() const {
367 if (local_vars().empty() && local_muts().empty()) return true;
368#ifdef MIM_ENABLE_CHECKS
369 assert(!is_external() || free_vars().empty());
370#endif
371 return free_vars().empty();
372}
373
374bool Def::is_open() const {
375 if (!local_vars().empty()) return true;
376 return !free_vars().empty();
377}
378
379/*
380 * Def - misc
381 */
382
383Sym Def::sym(const char* s) const { return world().sym(s); }
384Sym Def::sym(std::string_view s) const { return world().sym(s); }
385Sym Def::sym(std::string s) const { return world().sym(std::move(s)); }
386
387World& Def::world() const noexcept {
388 for (auto def = this;; def = def->type()) {
389 if (def->isa<Univ>()) return *def->world_;
390 if (auto type = def->isa<Type>()) return *type->level()->type()->as<Univ>()->world_;
391 }
392}
393
394const Def* Def::unfold_type() const {
395 if (!type_) {
396 auto& w = world();
397 if (auto t = isa<Type>()) return w.type(w.uinc(t->level()));
398 assert(isa<Univ>());
399 return nullptr;
400 }
401
402 return type_;
403}
404
405std::string_view Def::node_name() const {
406 switch (node()) {
407#define CODE(name, _, __) \
408 case Node::name: return #name;
410#undef CODE
411 default: fe::unreachable();
412 }
413}
414
415Defs Def::deps() const noexcept {
416 if (isa<Type>() || isa<Univ>()) return Defs();
417 assert(type());
418 return Defs(ops_ptr() - 1, (is_set() ? num_ops_ : 0) + 1);
419}
420
421u32 Def::judge() const noexcept {
422 switch (node()) {
423#define CODE(n, _, j) \
424 case Node::n: return u32(j);
426#undef CODE
427 default: fe::unreachable();
428 }
429}
430
431bool Def::is_term() const {
432 if (auto t = type()) {
433 if (auto u = t->type()) {
434 if (auto type = u->isa<Type>()) {
435 if (auto level = Lit::isa(type->level())) return *level == 0;
436 }
437 }
438 }
439 return false;
440}
441
442#ifndef NDEBUG
443const Def* Def::debug_prefix(std::string prefix) const { return dbg_.set(world().sym(prefix + sym().str())), this; }
444const Def* Def::debug_suffix(std::string suffix) const { return dbg_.set(world().sym(sym().str() + suffix)), this; }
445#endif
446
447// clang-format off
448
449const Def* Def::var() {
450 if (var_) return var_;
451 auto& w = world();
452
453 if (w.is_frozen()) return nullptr;
454 if (auto lam = isa<Lam >()) return w.var(lam ->dom(), lam);
455 if (auto pi = isa<Pi >()) return w.var(pi ->dom(), pi);
456 if (auto sig = isa<Sigma>()) return w.var(sig, sig);
457 if (auto arr = isa<Arr >()) return w.var(w.type_idx(arr ->shape()), arr ); // TODO shapes like (2, 3)
458 if (auto pack = isa<Pack >()) return w.var(w.type_idx(pack->shape()), pack); // TODO shapes like (2, 3)
459 if (isa<Bound >()) return w.var(this, this);
460 if (isa<Hole >()) return nullptr;
461 if (isa<Global>()) return nullptr;
462 fe::unreachable();
463}
464
465const Def* Def::arity() const {
466 if (auto sigma = isa<Sigma>()) return world().lit_nat(sigma->num_ops());
467 if (auto arr = isa<Arr >()) return arr->shape();
468 if (auto t = type()) return t->arity();
469 return world().lit_nat_1();
470}
471
472std::optional<nat_t> Def::isa_lit_arity() const {
473 if (auto sigma = isa<Sigma>()) return sigma->num_ops();
474 if (auto arr = isa<Arr >()) return Lit::isa(arr->shape());
475 if (auto t = type()) return t->isa_lit_arity();
476 return 1;
477}
478
479// clang-format on
480
481bool Def::equal(const Def* other) const {
482 if (isa<Univ>() || this->isa_mut() || other->isa_mut()) return this == other;
483
484 bool result = this->node() == other->node() && this->flags() == other->flags()
485 && this->num_ops() == other->num_ops() && this->type() == other->type();
486
487 for (size_t i = 0, e = num_ops(); result && i != e; ++i) result &= this->op(i) == other->op(i);
488
489 return result;
490}
491
492void Def::make_external() { return world().make_external(this); }
493void Def::make_internal() { return world().make_internal(this); }
494
495std::string Def::unique_name() const { return sym().str() + "_"s + std::to_string(gid()); }
496
498 if (auto a = isa_lit_arity(); a && *a < world().flags().scalarize_threshold) return *a;
499 return 1;
500}
501
502const Def* Def::proj(nat_t a, nat_t i) const {
503 World& w = world();
504
505 if (auto arr = isa<Arr>()) {
506 if (arr->arity()->isa<Top>()) return arr->body();
507 return arr->reduce(w.lit_idx(a, i));
508 } else if (auto pack = isa<Pack>()) {
509 if (pack->arity()->isa<Top>()) return pack->body();
510 assert(!w.is_frozen() && "TODO");
511 return pack->reduce(w.lit_idx(a, i));
512 }
513
514 if (a == 1) {
515 if (!type()) return this;
516 if (!isa_mut<Sigma>() && !type()->isa_mut<Sigma>()) return this;
517 }
518
519 if (isa<Tuple>() || isa<Sigma>()) return op(i);
520 if (w.is_frozen()) return nullptr;
521
522 return w.extract(this, a, i);
523}
524
525/*
526 * Idx
527 */
528
529const Def* Idx::isa(const Def* def) {
530 if (auto app = def->isa<App>()) {
531 if (app->callee()->isa<Idx>()) return app->arg();
532 }
533
534 return nullptr;
535}
536
537std::optional<nat_t> Idx::isa_lit(const Def* def) {
538 if (auto size = Idx::isa(def))
539 if (auto l = Lit::isa(size)) return l;
540 return {};
541}
542
543std::optional<nat_t> Idx::size2bitwidth(const Def* size) {
544 if (size->isa<Top>()) return 64;
545 if (auto s = Lit::isa(size)) return size2bitwidth(*s);
546 return {};
547}
548
549/*
550 * Global
551 */
552
553const App* Global::type() const { return Def::type()->as<App>(); }
554const Def* Global::alloced_type() const { return type()->arg(0); }
555
556} // namespace mim
friend class World
Definition lam.h:246
const Def * arg() const
Definition lam.h:230
const Def * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:196
const Def * body() const
Definition tuple.h:85
friend class World
Definition tuple.h:117
const Def * shape() const
Definition tuple.h:84
const Def * reduce(const Def *arg) const
Definition tuple.h:101
tag_t tag() const
Definition axm.h:55
u8 trip() const
Definition axm.h:38
friend class World
Definition axm.h:136
NormalizeFn normalizer() const
Definition axm.h:36
sub_t sub() const
Definition axm.h:56
plugin_t plugin() const
Definition axm.h:54
u8 curry() const
Definition axm.h:37
static bool alpha(const Def *d1, const Def *d2)
Definition check.h:71
Base class for all Defs.
Definition def.h:197
bool is_set() const
Yields true if empty or the last op is set.
Definition def.cpp:278
const Def * proj(nat_t a, nat_t i) const
Similar to World::extract while assuming an arity of a, but also works on Sigmas and Arrays.
Definition def.cpp:502
constexpr Node node() const noexcept
Definition def.h:220
Def * set(size_t i, const Def *)
Successively set from left to right.
Definition def.cpp:240
void make_internal()
Definition def.cpp:493
T * as_mut() const
Asserts that this is a mutable, casts constness away and performs a static_cast to T.
Definition def.h:437
Defs deps() const noexcept
Definition def.cpp:415
nat_t num_tprojs() const
As above but yields 1, if Flags::scalarize_threshold is exceeded.
Definition def.cpp:497
World & world() const noexcept
Definition def.cpp:387
virtual const Def * check()
Definition def.h:517
const Def * refine(size_t i, const Def *new_op) const
Definition def.cpp:225
std::string_view node_name() const
Definition def.cpp:405
constexpr auto ops() const noexcept
Definition def.h:260
Vars local_vars() const
Vars reachable by following immutable deps().
Definition def.cpp:305
void make_external()
Definition def.cpp:492
constexpr flags_t flags() const noexcept
Definition def.h:215
Dbg dbg_
Definition def.h:565
T * isa_mut() const
If this is mutable, it will cast constness away and perform a dynamic_cast to T.
Definition def.h:429
auto vars() noexcept
Definition def.h:378
bool is_term() const
Definition def.cpp:431
const Def * debug_prefix(std::string) const
Definition def.cpp:443
const Def * op(size_t i) const noexcept
Definition def.h:263
bool is_immutabilizable()
Definition def.cpp:174
const Def * var(nat_t a, nat_t i) noexcept
Definition def.h:378
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
bool is_open() const
Has free_vars()?
Definition def.cpp:374
friend class World
Definition def.h:594
Muts local_muts() const
Mutables reachable by following immutable deps(); mut->local_muts() is by definition the set { mut }...
Definition def.cpp:290
const Def * debug_suffix(std::string) const
Definition def.cpp:444
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.h:241
auto vars(F f) noexcept
Definition def.h:378
const Def * rebuild(World &w, const Def *type, Defs ops) const
Def::rebuilds this Def while using new_op as substitute for its i'th Def::op.
Definition def.h:491
const Def * var()
Not necessarily a Var: E.g., if the return type is [], this will yield ().
Definition def.cpp:449
virtual constexpr size_t reduction_offset() const noexcept
First Def::op that needs to be dealt with during reduction; e.g.
Definition def.h:511
Sym sym() const
Definition def.h:450
std::optional< nat_t > isa_lit_arity() const
Definition def.cpp:472
flags_t flags_
Definition def.h:572
constexpr u32 gid() const noexcept
Global id - unique number for this Def.
Definition def.h:216
const Def * arity() const
Definition def.cpp:465
Def * unset()
Unsets all Def::ops; works even, if not set at all or partially.
Definition def.cpp:256
std::string unique_name() const
name + "_" + Def::gid
Definition def.cpp:495
Muts users()
Set of mutables where this mutable is locally referenced.
Definition def.h:406
bool is_closed() const
Has no free_vars()?
Definition def.cpp:366
Def * reset(size_t i, const Def *def)
Successively reset from left to right.
Definition def.h:285
Vars free_vars() const
Compute a global solution by transitively following mutables as well.
Definition def.cpp:295
Dbg dbg() const
Definition def.h:448
u32 judge() const noexcept
Definition def.cpp:421
const Var * has_var()
Only returns not nullptr, if Var of this mutable has ever been created.
Definition def.h:382
constexpr size_t num_ops() const noexcept
Definition def.h:264
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:117
friend class World
Definition tuple.h:182
const Def * alloced_type() const
Definition def.cpp:554
friend class World
Definition def.h:848
bool is_mutable() const
Definition def.h:834
const App * type() const
Definition def.cpp:553
Global * stub_(World &, const Def *) override
Definition def.cpp:150
This node is a hole in the IR that is inferred by its context later on.
Definition check.h:10
friend class World
Definition check.h:51
static constexpr nat_t size2bitwidth(nat_t n)
Definition def.h:774
static const Def * isa(const Def *def)
Checks if def is a Idx s and returns s or nullptr otherwise.
Definition def.cpp:529
friend class World
Definition def.h:784
static std::optional< nat_t > isa_lit(const Def *def)
Definition def.cpp:537
friend class World
Definition lattice.h:83
friend class World
Definition tuple.h:209
friend class World
Definition lam.h:196
static std::optional< T > isa(const Def *def)
Definition def.h:712
friend class World
Definition def.h:725
friend class World
Definition lattice.h:129
friend class World
Definition lattice.h:60
friend class World
Definition def.h:738
const Def * body() const
Definition tuple.h:132
const Def * shape() const
Definition tuple.cpp:40
friend class World
Definition tuple.h:159
const Def * reduce(const Def *arg) const
Definition tuple.h:149
const Def * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:206
A dependent function type.
Definition lam.h:11
Pi(const Def *type, const Def *dom, const Def *codom, bool implicit)
Constructor for an immutable Pi.
Definition lam.h:14
bool is_implicit() const
Definition lam.h:23
const Def * dom() const
Definition lam.h:32
friend class World
Definition lam.h:101
const Def * codom() const
Definition lam.h:33
const Pi * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:186
friend class World
Definition def.h:806
u32 pass() const
IPass::index within PassMan.
Definition def.h:797
u32 tag() const
Definition def.h:798
constexpr bool empty() const noexcept
Is empty?
Definition sets.h:235
void dot()
Definition sets.h:553
Set merge(Set s1, Set s2)
Yields .
Definition sets.h:481
Set insert(Set s, D *d)
Yields .
Definition sets.h:415
const TExt< Up > * set(Loc l) const
Definition def.h:149
const Def * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:191
friend class World
Definition tuple.h:51
friend class World
Definition lattice.h:105
friend class World
Definition lattice.h:44
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:143
Extremum. Either Top (Up) or Bottom.
Definition lattice.h:140
friend class World
Definition lattice.h:153
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:142
friend class World
Definition tuple.h:68
friend class World
Definition def.h:687
friend class World
Definition def.h:666
level_t offset() const
Definition def.h:658
friend class World
Definition def.h:644
friend class World
Definition lattice.h:185
friend class World
Definition def.h:631
friend class World
Definition def.h:617
The World represents the whole program and manages creation of MimIR nodes (Defs).
Definition world.h:33
auto & muts()
Definition world.h:504
void make_external(Def *)
Definition world.cpp:87
const Def * sigma(Defs ops)
Definition world.cpp:258
const Pi * pi(const Def *dom, const Def *codom, bool implicit=false)
Definition world.h:251
Flags & flags()
Retrieve compile Flags.
Definition world.cpp:71
u32 next_gid()
Definition world.h:89
Sym sym(std::string_view)
Definition world.cpp:74
void make_internal(Def *)
Definition world.cpp:94
const Lit * lit_nat(nat_t a)
Definition world.h:384
auto & vars()
Definition world.h:503
Defs reduce(const Var *var, const Def *arg)
Yields the new body of [mut->var() -> arg]mut.
Definition world.cpp:607
const Lit * lit_nat_1()
Definition world.h:386
#define MIM_NODE(m)
Definition def.h:17
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
Dep
Tracks a dependency to certain Defs transitively through the Def::deps() up to but excliding mutables...
Definition def.h:96
@ None
Definition def.h:97
@ Mut
Definition def.h:98
u64 flags_t
Definition types.h:45
uint64_t scalarize_threshold
Definition flags.h:13
u8 node_t
Definition types.h:44
constexpr size_t hash_combine(size_t seed, T v) noexcept
Definition hash.h:58
Sets< Def >::Set Muts
Definition def.h:58
TExt< true > Top
Definition lattice.h:159
constexpr decltype(auto) get(Span< T, N > span) noexcept
Definition span.h:107
consteval size_t hash_begin() noexcept
Definition hash.h:71
constexpr size_t hash(size_t h) noexcept
Definition hash.h:32
Sets< const Var >::Set Vars
Definition def.h:67
uint32_t u32
Definition types.h:34
uint8_t u8
Definition types.h:34
Node
Definition def.h:82
@ Univ
Definition def.h:84
@ Var
Definition def.h:84
CODE(node, name, _)
Definition def.h:83