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/rule.h"
9#include "mim/world.h"
10
11#include "mim/util/hash.h"
12
13using namespace std::literals;
14
15namespace mim {
16
17template void Sets<const Var>::dot();
18template void Sets<Def>::dot();
19
20/*
21 * constructors
22 */
23
24Def::Def(World* world, Node node, const Def* type, Defs ops, flags_t flags)
25 : world_(world)
26 , flags_(flags)
27 , node_(node)
28 , mut_(false)
29 , external_(false)
30 , dep_(node == Node::Hole ? unsigned(Dep::Hole)
31 : node == Node::Proxy ? unsigned(Dep::Proxy)
32 : node == Node::Var ? (Dep::Var | Dep::Mut)
33 : 0)
34 , num_ops_(ops.size())
35 , type_(type) {
36 if (node == Node::Univ) {
37 gid_ = world->next_gid();
39 } else if (auto var = isa<Var>()) {
40 assert(flags_ == 0); // if we ever need flags here, we need to hash that
41 auto& world = type->world();
42 gid_ = world.next_gid();
43 vars_ = world.vars().insert(type->local_vars(), var);
44 muts_ = type->local_muts();
45 dep_ |= type->dep_;
46 auto op = ops[0];
47 ops_ptr()[0] = op;
48 hash_ = hash_begin(node_t(Node::Var));
49 hash_ = hash_combine(hash_, type->gid());
50 hash_ = hash_combine(hash_, op->gid());
51 } else {
52 hash_ = hash_begin(u8(node));
53 hash_ = hash_combine(hash_, flags_);
54
55 if (type) {
56 world = &type->world();
57 dep_ |= type->dep_;
58 vars_ = type->local_vars();
59 muts_ = type->local_muts();
60 hash_ = hash_combine(hash_, type->gid());
61 } else {
62 world = &ops[0]->world();
63 }
64
65 auto vars = &world->vars();
66 auto muts = &world->muts();
67 auto ptr = ops_ptr();
68 gid_ = world->next_gid();
69
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* Rule ::rebuild_(World& w, const Def* t, Defs o) const { return w.rule(t->as<Reform>(), o[0], o[1], o[2]); }
127const Def* Reform ::rebuild_(World& w, const Def* , Defs o) const { return w.reform(o[0]); }
128const Def* Sigma ::rebuild_(World& w, const Def* , Defs o) const { return w.sigma(o); }
129const Def* Split ::rebuild_(World& w, const Def* t, Defs o) const { return w.split(t, o[0]); }
130const Def* Match ::rebuild_(World& w, const Def* , Defs o) const { return w.match(o); }
131const Def* Tuple ::rebuild_(World& w, const Def* t, Defs o) const { return w.tuple(t, o); }
132const Def* Type ::rebuild_(World& w, const Def* , Defs o) const { return w.type(o[0]); }
133const Def* UInc ::rebuild_(World& w, const Def* , Defs o) const { return w.uinc(o[0], offset()); }
134const Def* UMax ::rebuild_(World& w, const Def* , Defs o) const { return w.umax(o); }
135const Def* Uniq ::rebuild_(World& w, const Def* , Defs o) const { return w.uniq(o[0]); }
136const Def* Var ::rebuild_(World& w, const Def* t, Defs o) const { return w.var(t, o[0]->as_mut()); }
137
138const Def* Axm ::rebuild_(World& w, const Def* t, Defs ) const {
139 if (&w != &world()) return w.axm(normalizer(), curry(), trip(), t, plugin(), tag(), sub())->set(dbg());
141 return this;
142}
143
144template<bool up> const Def* TExt <up>::rebuild_(World& w, const Def* t, Defs ) const { return w.ext <up>(t)->set(dbg()); }
145template<bool up> const Def* TBound<up>::rebuild_(World& w, const Def* , Defs o) const { return w.bound<up>(o)->set(dbg()); }
146
147/*
148 * stub
149 */
150
151Arr* Arr ::stub_(World& w, const Def* t) { return w.mut_arr (t); }
152Global* Global::stub_(World& w, const Def* t) { return w.global (t, is_mutable()); }
153Hole* Hole ::stub_(World& w, const Def* t) { return w.mut_hole (t); }
154Lam* Lam ::stub_(World& w, const Def* t) { return w.mut_lam (t->as<Pi>()); }
155Pack* Pack ::stub_(World& w, const Def* t) { return w.mut_pack (t); }
156Pi* Pi ::stub_(World& w, const Def* t) { return w.mut_pi (t, is_implicit()); }
157Rule* Rule ::stub_(World& w, const Def* t) { return w.mut_rule(t->as<Reform>()); }
158Sigma* Sigma ::stub_(World& w, const Def* t) { return w.mut_sigma(t, num_ops()); }
159
160/*
161 * instantiate templates
162 */
163
164#ifndef DOXYGEN
165template const Def* TExt<false> ::rebuild_(World&, const Def*, Defs) const;
166template const Def* TExt<true > ::rebuild_(World&, const Def*, Defs) const;
167template const Def* TBound<false>::rebuild_(World&, const Def*, Defs) const;
168template const Def* TBound<true >::rebuild_(World&, const Def*, Defs) const;
169#endif
170
171// clang-format on
172
173/*
174 * immutabilize
175 */
176
178 if (!is_set()) return false;
179
180 if (auto v = has_var()) {
181 for (auto op : deps())
182 if (op->free_vars().contains(v)) return false;
183 }
184 for (auto op : deps()) {
185 for (auto mut : op->local_muts())
186 if (mut == this) return false; // recursion
187 }
188 return true;
189}
190
192 if (is_immutabilizable()) return world().pi(dom(), codom());
193 return nullptr;
194}
195
196const Rule* Rule::immutabilize() { return world().rule(type(), lhs(), rhs(), guard()); }
197
199 if (is_immutabilizable()) return static_cast<const Sigma*>(world().sigma(ops()));
200 return nullptr;
201}
202
204 auto& w = world();
205 if (is_immutabilizable()) return w.arr(arity(), body());
206
207 if (auto n = Lit::isa(arity()); n && *n < w.flags().scalarize_threshold)
208 return w.sigma(DefVec(*n, [&](size_t i) { return reduce(w.lit_idx(*n, i)); }));
209
210 return nullptr;
211}
212
214 auto& w = world();
215 if (is_immutabilizable()) return w.pack(arity(), body());
216
217 if (auto n = Lit::isa(arity()); n && *n < w.flags().scalarize_threshold)
218 return w.tuple(DefVec(*n, [&](size_t i) { return reduce(w.lit_idx(*n, i)); }));
219
220 return nullptr;
221}
222
223/*
224 * reduce
225 */
226
227Defs Def::reduce_(const Def* arg) const {
228 if (auto var = has_var()) return world().reduce(var, arg);
229 return {ops().begin() + reduction_offset(), num_ops() - reduction_offset()};
230}
231
232const Def* Def::refine(size_t i, const Def* new_op) const {
233 auto new_ops = absl::FixedArray<const Def*>(num_ops());
234 for (size_t j = 0, e = num_ops(); j != e; ++j)
235 new_ops[j] = i == j ? new_op : op(j);
236 return rebuild(type(), new_ops);
237}
238
239/*
240 * Def - set
241 */
242
244#ifdef MIM_ENABLE_CHECKS
245 if (world().watchpoints().contains(gid())) fe::breakpoint();
246#endif
247 invalidate();
248
249 size_t n = ops.size();
250 assert(n == num_ops() && "num ops don't match");
251
252 for (size_t i = 0; i != n; ++i) {
253 auto def = check(i, ops[i]);
254 assert(def);
255 ops_ptr()[i] = def;
256 }
257#ifndef NDEBUG
258 curr_op_ = n;
259#endif
261 if (auto t = check()->zonk(); t != type()) type_ = t;
262
263 return this;
264}
265
266Def* Def::set(size_t i, const Def* def) {
267#ifdef MIM_ENABLE_CHECKS
268 if (world().watchpoints().contains(gid())) fe::breakpoint();
269#endif
270
271 invalidate();
272 def = check(i, def);
273 assert(def && !op(i) && curr_op_++ == i);
274 ops_ptr()[i] = def;
275
276 if (i + 1 == num_ops()) { // set last op, so check kind
277 if (auto t = check()->zonk(); t != type()) type_ = t;
278 }
279
280 return this;
281}
282
283Def* Def::set_type(const Def* type) {
284 invalidate();
285 type_ = type;
286 return this;
287}
288
290 invalidate();
291#ifndef NDEBUG
292 curr_op_ = 0;
293#endif
294 std::ranges::fill(ops_ptr(), ops_ptr() + num_ops(), nullptr);
295 return this;
296}
297
298bool Def::is_set() const {
299 if (num_ops() == 0) return true;
300 bool result = ops().back();
301 assert((!result || std::ranges::all_of(ops().rsubspan(1), [](auto op) { return op; }))
302 && "the last operand is set but others in front of it aren't");
303 return result;
304}
305
306/*
307 * free_vars
308 */
309
310const Def* Def::var() {
311 if (var_) return var_;
312 auto& w = world();
313
314 // clang-format off
315 if (w.is_frozen()) return nullptr;
316 if (auto lam = isa<Lam >()) return w.var(lam ->dom(), lam);
317 if (auto pi = isa<Pi >()) return w.var(pi ->dom(), pi);
318 if (auto sig = isa<Sigma>()) return w.var(sig, sig);
319 if (auto arr = isa<Arr >()) return w.var(w.type_idx(arr ->arity()), arr ); // TODO shapes like (2, 3)
320 if (auto pack = isa<Pack >()) return w.var(w.type_idx(pack->arity()), pack); // TODO shapes like (2, 3)
321 if (auto rule = isa<Rule >()) return w.var(rule->type()->meta_type(), rule);
322 if (isa<Bound >()) return w.var(this, this);
323 if (isa<Hole >()) return nullptr;
324 if (isa<Global>()) return nullptr;
325 // clang-format on
326 fe::unreachable();
327}
328
330 if (auto mut = isa_mut()) return Muts(mut);
331 return muts_;
332}
333
335 if (auto mut = isa_mut()) return mut->free_vars();
336
337 auto& vars = world().vars();
338 auto fvs = local_vars();
339 for (auto mut : local_muts())
340 fvs = vars.merge(fvs, mut->free_vars());
341
342 return fvs;
343}
344
345Vars Def::local_vars() const { return mut_ ? Vars() : vars_; }
346
348 if (mark_ == 0) {
349 // fixed-point iteration to recompute free vars:
350 // (run - 1) identifies the previous iteration; so make sure to offset run by 2 for the first iteration
351 auto& w = world();
352 bool cyclic = false;
353 w.next_run();
354 free_vars<true>(cyclic, w.next_run());
355
356 for (bool todo = cyclic; todo;) {
357 todo = false;
358 free_vars<false>(todo, w.next_run());
359 }
360 }
361
362 return vars_;
363}
364
365template<bool init>
366Vars Def::free_vars(bool& todo, uint32_t run) {
367 // If init == true : todo flag detects cycle.
368 // If init == false: todo flag keeps track whether sth changed.
369 //
370 // Recursively recompute free vars. If
371 // * mark_ == 0: Invalid - need to recompute.
372 // * mark_ == run - 1: Previous iteration - need to recompute.
373 // * mark_ == run: We are running in cycles within the *current* iteration of our fixed-point loop.
374 // * otherwise: Valid!
375 if (mark_ != 0 && mark_ != run - 1) {
376 if constexpr (init) todo |= mark_ == run;
377 return vars_;
378 }
379
380 mark_ = run;
381
382 auto fvs0 = vars_;
383 auto fvs = fvs0;
384 auto& w = world();
385 auto& muts = w.muts();
386 auto& vars = w.vars();
387
388 for (auto op : deps()) {
389 if constexpr (init) fvs = vars.merge(fvs, op->local_vars());
390
391 for (auto mut : op->local_muts()) {
392 if constexpr (init) mut->muts_ = muts.insert(mut->muts_, this); // register "this" as user of local_mut
393 fvs = vars.merge(fvs, mut->free_vars<init>(todo, run));
394 }
395 }
396
397 if (auto var = has_var()) fvs = vars.erase(fvs, var); // FV(λx.e) = FV(e) \ {x}
398
399 if constexpr (!init) todo |= fvs0 != fvs;
400
401 return vars_ = fvs;
402}
403
404void Def::invalidate() {
405 if (mark_ != 0) {
406 mark_ = 0;
407 // TODO optimize if vars empty?
408 for (auto mut : users())
409 mut->invalidate();
410 vars_ = Vars();
411 muts_ = Muts();
412 }
413}
414
415bool Def::is_closed() const {
416 if (local_vars().empty() && local_muts().empty()) return true;
417#ifdef MIM_ENABLE_CHECKS
418 assert(!is_external() || free_vars().empty());
419#endif
420 return free_vars().empty();
421}
422
423bool Def::is_open() const {
424 if (!local_vars().empty()) return true;
425 return !free_vars().empty();
426}
427
428/*
429 * Def - misc
430 */
431
432Sym Def::sym(const char* s) const { return world().sym(s); }
433Sym Def::sym(std::string_view s) const { return world().sym(s); }
434Sym Def::sym(std::string s) const { return world().sym(std::move(s)); }
435
436World& Def::world() const noexcept {
437 for (auto def = this;; def = def->type()) {
438 if (def->isa<Univ>()) return *def->world_;
439 if (auto type = def->isa<Type>()) return *type->level()->type()->as<Univ>()->world_;
440 }
441}
442
443const Def* Def::unfold_type() const {
444 if (!type_) {
445 auto& w = world();
446 if (auto t = isa<Type>()) return w.type(w.uinc(t->level()));
447 assert(isa<Univ>());
448 return nullptr;
449 }
450
451 return type_;
452}
453
454std::string_view Def::node_name() const {
455 switch (node()) {
456#define CODE(name, _) \
457 case Node::name: return #name;
459#undef CODE
460 default: fe::unreachable();
461 }
462}
463
464Defs Def::deps() const noexcept {
465 if (isa<Type>() || isa<Univ>()) return Defs();
466 assert(type());
467 return Defs(ops_ptr() - 1, (is_set() ? num_ops_ : 0) + 1);
468}
469
470u32 Def::judge() const noexcept {
471 switch (node()) {
472#define CODE(n, j) \
473 case Node::n: return u32(j);
475#undef CODE
476 default: fe::unreachable();
477 }
478}
479
480bool Def::is_term() const {
481 if (auto t = type()) {
482 if (auto u = t->type()) {
483 if (auto type = u->isa<Type>()) {
484 if (auto level = Lit::isa(type->level())) return *level == 0;
485 }
486 }
487 }
488 return false;
489}
490
491#ifndef NDEBUG
492const Def* Def::debug_prefix(std::string prefix) const { return dbg_.set(world().sym(prefix + sym().str())), this; }
493const Def* Def::debug_suffix(std::string suffix) const { return dbg_.set(world().sym(sym().str() + suffix)), this; }
494#endif
495
496/*
497 * cmp
498 */
499
500Def::Cmp Def::cmp(const Def* a, const Def* b) {
501 if (a == b) return Cmp::E;
502
503 if (a->isa_imm() && b->isa_mut()) return Cmp::L;
504 if (a->isa_mut() && b->isa_imm()) return Cmp::G;
505
506 // clang-format off
507 if (a->node() != b->node() ) return a->node() < b->node() ? Cmp::L : Cmp::G;
508 if (a->num_ops() != b->num_ops()) return a->num_ops() < b->num_ops() ? Cmp::L : Cmp::G;
509 if (a->flags() != b->flags() ) return a->flags() < b->flags() ? Cmp::L : Cmp::G;
510 // clang-format on
511
512 if (a->isa_mut() && b->isa_mut()) return Cmp::U;
513 assert(a->isa_imm() && b->isa_imm());
514
515 if (auto va = a->isa<Var>()) {
516 auto vb = b->as<Var>();
517 auto ma = va->mut();
518 auto mb = vb->mut();
519 if (ma->is_set() && ma->free_vars().contains(vb)) return Cmp::L;
520 if (mb->is_set() && mb->free_vars().contains(va)) return Cmp::G;
521 return Cmp::U;
522 }
523
524 // heuristic: iterate backwards as index (often a Lit) comes last and will faster find a solution
525 for (size_t i = a->num_ops(); i-- != 0;)
526 if (auto res = cmp(a->op(i), b->op(i)); res == Cmp::L || res == Cmp::G) return res;
527
528 return cmp(a->type(), b->type());
529}
530
531template<Def::Cmp c>
532bool Def::cmp_(const Def* a, const Def* b) {
533 auto res = cmp(a, b);
534 if (res == Cmp::U) {
535 a->world().WLOG("resorting to unstable gid-based compare for commute check");
536 return c == Cmp::L ? a->gid() < b->gid() : a->gid() > b->gid();
537 }
538 return res == c;
539}
540
541// clang-format off
542bool Def::less (const Def* a, const Def* b) { return cmp_<Cmp::L>(a, b); }
543bool Def::greater(const Def* a, const Def* b) { return cmp_<Cmp::G>(a, b); }
544// clang-format on
545
546const Def* Def::arity() const {
547 if (auto t = type(); t && !t->isa<Type>()) return t->arity();
548 return world().lit_nat_1();
549}
550
551bool Def::equal(const Def* other) const {
552 if (isa<Univ>() || this->isa_mut() || other->isa_mut()) return this == other;
553
554 bool result = this->node() == other->node() && this->flags() == other->flags()
555 && this->num_ops() == other->num_ops() && this->type() == other->type();
556
557 for (size_t i = 0, e = num_ops(); result && i != e; ++i)
558 result &= this->op(i) == other->op(i);
559
560 return result;
561}
562
563void Def::make_external() { return world().make_external(this); }
564void Def::make_internal() { return world().make_internal(this); }
565
567 assert(this->sym() == to->sym());
569 to->make_external();
570}
571
572std::string Def::unique_name() const { return sym().str() + "_"s + std::to_string(gid()); }
573
574nat_t Def::num_projs() const { return Lit::isa(arity()).value_or(1); }
575
577 if (auto a = Lit::isa(arity()); a && *a < world().flags().scalarize_threshold) return *a;
578 return 1;
579}
580
581const Def* Def::proj(nat_t a, nat_t i) const {
582 World& w = world();
583
584 if (a == 1) {
585 assert(i == 0 && "only inhabitant of Idx 2 is 0_1");
586 if (!type()) return this;
587 if (!isa_mut<Sigma>() && !type()->isa_mut<Sigma>()) return this;
588 }
589
590 if (auto seq = isa<Seq>()) {
591 if (seq->has_var()) return seq->reduce(world().lit_idx(a, i));
592 return seq->body();
593 }
594
595 if (isa<Prod>()) return op(i);
596 if (w.is_frozen()) return nullptr;
597
598 return w.extract(this, a, i);
599}
600
601/*
602 * Idx
603 */
604
605const Def* Idx::isa(const Def* def) {
606 if (auto app = def->isa<App>()) {
607 if (app->callee()->isa<Idx>()) return app->arg();
608 }
609
610 return nullptr;
611}
612
613std::optional<nat_t> Idx::isa_lit(const Def* def) {
614 if (auto size = Idx::isa(def))
615 if (auto l = Lit::isa(size)) return l;
616 return {};
617}
618
619std::optional<nat_t> Idx::size2bitwidth(const Def* size) {
620 if (size->isa<Top>()) return 64;
621 if (auto s = Lit::isa(size)) return size2bitwidth(*s);
622 return {};
623}
624
625/*
626 * Global
627 */
628
629const App* Global::type() const { return Def::type()->as<App>(); }
630const Def* Global::alloced_type() const { return type()->arg(0); }
631
632} // namespace mim
friend class World
Definition lam.h:337
const Def * arg() const
Definition lam.h:282
const Def * arity() const final
Definition tuple.h:127
const Def * reduce(const Def *arg) const final
Definition tuple.h:144
friend class World
Definition tuple.h:161
const Def * immutabilize() final
Tries to make an immutable from a mutable.
Definition def.cpp:203
tag_t tag() const
Definition axm.h:55
u8 trip() const
Definition axm.h:38
friend class World
Definition axm.h:141
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:96
Base class for all Defs.
Definition def.h:251
bool is_set() const
Yields true if empty or the last op is set.
Definition def.cpp:298
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:581
constexpr Node node() const noexcept
Definition def.h:274
Def * set(size_t i, const Def *)
Successively set from left to right.
Definition def.cpp:266
void make_internal()
Definition def.cpp:564
T * as_mut() const
Asserts that this is a mutable, casts constness away and performs a static_cast to T.
Definition def.h:491
Defs deps() const noexcept
Definition def.cpp:464
nat_t num_tprojs() const
As above but yields 1, if Flags::scalarize_threshold is exceeded.
Definition def.cpp:576
const Def * zonk() const
If Holes have been filled, reconstruct the program without them.
Definition check.cpp:61
World & world() const noexcept
Definition def.cpp:436
virtual const Def * check()
After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
Definition def.h:580
const Def * refine(size_t i, const Def *new_op) const
Definition def.cpp:232
Def * set_type(const Def *)
Update type.
Definition def.cpp:283
std::string_view node_name() const
Definition def.cpp:454
constexpr auto ops() const noexcept
Definition def.h:305
Vars local_vars() const
Vars reachable by following immutable deps().
Definition def.cpp:345
void make_external()
Definition def.cpp:563
constexpr flags_t flags() const noexcept
Definition def.h:269
Dbg dbg_
Definition def.h:653
T * isa_mut() const
If this is mutable, it will cast constness away and perform a dynamic_cast to T.
Definition def.h:482
auto vars() noexcept
Definition def.h:429
bool is_term() const
Definition def.cpp:480
const Def * debug_prefix(std::string) const
Definition def.cpp:492
const Def * op(size_t i) const noexcept
Definition def.h:308
bool is_immutabilizable()
Definition def.cpp:177
const Def * var(nat_t a, nat_t i) noexcept
Definition def.h:429
void transfer_external(Def *to)
Definition def.cpp:566
const Def * unfold_type() const
Yields the type of this Def and builds a new Type (UInc n) if necessary.
Definition def.cpp:443
bool is_open() const
Has free_vars()?
Definition def.cpp:423
friend class World
Definition def.h:683
Muts local_muts() const
Mutables reachable by following immutable deps(); mut->local_muts() is by definition the set { mut }...
Definition def.cpp:329
const Def * debug_suffix(std::string) const
Definition def.cpp:493
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
auto vars(F f) noexcept
Definition def.h:429
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:545
static bool less(const Def *a, const Def *b)
Definition def.cpp:542
static bool greater(const Def *a, const Def *b)
Definition def.cpp:543
const Def * var()
Not necessarily a Var: E.g., if the return type is [], this will yield ().
Definition def.cpp:310
static Cmp cmp(const Def *a, const Def *b)
Definition def.cpp:500
virtual constexpr size_t reduction_offset() const noexcept
First Def::op that needs to be dealt with during reduction; e.g.
Definition def.h:566
Sym sym() const
Definition def.h:504
nat_t num_projs() const
Yields Def::arity(), if it is a Lit, or 1 otherwise.
Definition def.cpp:574
flags_t flags_
Definition def.h:660
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
Def * unset()
Unsets all Def::ops; works even, if not set at all or only partially set.
Definition def.cpp:289
std::string unique_name() const
name + "_" + Def::gid
Definition def.cpp:572
const T * isa_imm() const
Definition def.h:476
Muts users()
Set of mutables where this mutable is locally referenced.
Definition def.h:457
bool is_closed() const
Has no free_vars()?
Definition def.cpp:415
Vars free_vars() const
Compute a global solution by transitively following mutables as well.
Definition def.cpp:334
Dbg dbg() const
Definition def.h:502
u32 judge() const noexcept
Definition def.cpp:470
const Var * has_var()
Only returns not nullptr, if Var of this mutable has ever been created.
Definition def.h:433
constexpr size_t num_ops() const noexcept
Definition def.h:309
@ E
Equal.
Definition def.h:608
@ U
Unknown.
Definition def.h:609
@ L
Less.
Definition def.h:606
@ G
Greater.
Definition def.h:607
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:117
friend class World
Definition tuple.h:226
const Def * alloced_type() const
Definition def.cpp:630
friend class World
Definition def.h:954
bool is_mutable() const
Definition def.h:939
const App * type() const
Definition def.cpp:629
Global * stub_(World &, const Def *) final
Definition def.cpp:152
This node is a hole in the IR that is inferred by its context later on.
Definition check.h:14
friend class World
Definition check.h:75
static constexpr nat_t size2bitwidth(nat_t n)
Definition def.h:877
static const Def * isa(const Def *def)
Checks if def is a Idx s and returns s or nullptr otherwise.
Definition def.cpp:605
friend class World
Definition def.h:888
static std::optional< nat_t > isa_lit(const Def *def)
Definition def.cpp:613
friend class World
Definition lattice.h:89
friend class World
Definition tuple.h:254
friend class World
Definition lam.h:209
static std::optional< T > isa(const Def *def)
Definition def.h:810
friend class World
Definition def.h:827
friend class World
Definition lattice.h:140
friend class World
Definition lattice.h:65
friend class World
Definition def.h:841
const Def * immutabilize() final
Tries to make an immutable from a mutable.
Definition def.cpp:213
const Def * arity() const final
Definition tuple.cpp:46
friend class World
Definition tuple.h:202
const Def * reduce(const Def *arg) const final
Definition tuple.h:191
A dependent function type.
Definition lam.h:13
Pi(const Def *type, const Def *dom, const Def *codom, bool implicit)
Constructor for an immutable Pi.
Definition lam.h:16
bool is_implicit() const
Definition lam.h:25
const Def * dom() const
Definition lam.h:34
friend class World
Definition lam.h:104
const Def * codom() const
Definition lam.h:35
const Pi * immutabilize() final
Tries to make an immutable from a mutable.
Definition def.cpp:191
Def(World *, Node, const Def *type, Defs ops, flags_t flags)
Constructor for an immutable Def.
Definition def.cpp:24
friend class World
Definition def.h:911
u32 pass() const
IPass::index within PassMan.
Definition def.h:901
u32 tag() const
Definition def.h:902
Type formation of a rewrite Rule.
Definition rule.h:9
friend class World
Definition rule.h:34
const Def * lhs() const
Definition rule.h:50
const Def * guard() const
Definition rule.h:52
friend class World
Definition rule.h:99
const Rule * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:196
const Def * rhs() const
Definition rule.h:51
const Reform * type() const
Definition rule.h:49
const Def * body() const
Definition tuple.h:91
Def(World *, Node, const Def *type, Defs ops, flags_t flags)
Constructor for an immutable Def.
Definition def.cpp:24
constexpr bool empty() const noexcept
Is empty?
Definition sets.h:240
bool contains(D *d) const noexcept
Is ?.
Definition sets.h:252
void dot()
Definition sets.h:562
const TExt< Up > * set(Loc l) const
Definition def.h:202
friend class World
Definition tuple.h:63
const Def * immutabilize() final
Tries to make an immutable from a mutable.
Definition def.cpp:198
friend class World
Definition lattice.h:112
friend class World
Definition lattice.h:48
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:145
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:144
friend class World
Definition lattice.h:166
friend class World
Definition tuple.h:80
friend class World
Definition def.h:783
friend class World
Definition def.h:761
level_t offset() const
Definition def.h:752
friend class World
Definition def.h:738
friend class World
Definition lattice.h:199
friend class World
Definition def.h:722
friend class World
Definition def.h:707
Def * mut() const
Definition def.h:698
The World represents the whole program and manages creation of MimIR nodes (Defs).
Definition world.h:36
void make_external(Def *)
Definition world.cpp:88
const Def * sigma(Defs ops)
Definition world.cpp:278
const Pi * pi(const Def *dom, const Def *codom, bool implicit=false)
Definition world.h:264
Flags & flags()
Retrieve compile Flags.
Definition world.cpp:72
u32 next_gid()
Definition world.h:96
Sym sym(std::string_view)
Definition world.cpp:75
void make_internal(Def *)
Definition world.cpp:95
auto & vars()
Definition world.h:550
Defs reduce(const Var *var, const Def *arg)
Yields the new body of [mut->var() -> arg]mut.
Definition world.cpp:656
const Rule * rule(const Reform *type, const Def *lhs, const Def *rhs, const Def *guard)
Definition world.h:322
const Lit * lit_nat_1()
Definition world.h:427
#define MIM_NODE(m)
Definition def.h:18
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
Dep
Tracks a dependency to certain Defs transitively through the Def::deps() up to but excliding mutables...
Definition def.h:123
@ None
Definition def.h:124
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:62
Sets< Def >::Set Muts
Definition def.h:87
TExt< true > Top
Definition lattice.h:172
constexpr decltype(auto) get(Span< T, N > span) noexcept
Definition span.h:115
consteval size_t hash_begin() noexcept
Definition hash.h:75
constexpr size_t hash(size_t h) noexcept
Definition hash.h:32
Sets< const Var >::Set Vars
Definition def.h:97
uint32_t u32
Definition types.h:34
Mut
Judgement.
Definition def.h:143
uint8_t u8
Definition types.h:34
Node
Definition def.h:112
@ Univ
Definition def.h:114
CODE(node, _)
Definition def.h:113
@ Var
Definition def.h:114