Thorin 1.9.0
The Higher ORder INtermediate representation
Loading...
Searching...
No Matches
def.cpp
Go to the documentation of this file.
1#include "thorin/def.h"
2
3#include <algorithm>
4#include <optional>
5#include <ranges>
6#include <stack>
7
8#include "thorin/rewrite.h"
9#include "thorin/world.h"
10
12
13#include "fe/assert.h"
14
15using namespace std::literals;
16
17namespace thorin {
18
19/*
20 * constructors
21 */
22
23Def::Def(World* w, node_t node, const Def* type, Defs ops, flags_t flags)
24 : world_(w)
25 , flags_(flags)
26 , node_(unsigned(node))
27 , mut_(false)
28 , external_(false)
29 , dep_(unsigned(node == Node::Axiom ? Dep::Axiom
30 : node == Node::Infer ? Dep::Infer
31 : node == Node::Proxy ? Dep::Proxy
32 : node == Node::Var ? Dep::Var
33 : Dep::None))
34 , valid_(false)
35 , num_ops_(ops.size())
36 , type_(type) {
37 std::ranges::copy(ops, ops_ptr());
38 gid_ = world().next_gid();
39
40 if (auto var = isa<Var>()) {
41 vars_.local = world().vars(var);
42 muts_.local = Muts();
43 } else {
44 vars_.local = Vars();
45 muts_.local = Muts();
46 for (auto op : extended_ops()) {
47 vars_.local = world().merge(vars_.local, op->local_vars());
48 muts_.local = world().merge(muts_.local, op->local_muts());
49 }
50 }
51
52 if (node == Node::Univ) {
53 hash_ = murmur3(gid());
54 } else {
55 hash_ = type ? type->gid() : 0;
56 for (auto op : ops) hash_ = murmur3(hash_, u32(op->gid()));
57 hash_ = murmur3(hash_, flags_);
58 hash_ = murmur3_rest(hash_, u8(node));
59 hash_ = murmur3_finalize(hash_, num_ops());
60 }
61}
62
63Def::Def(node_t n, const Def* type, Defs ops, flags_t flags)
64 : Def(nullptr, n, type, ops, flags) {}
65
66Def::Def(node_t node, const Def* type, size_t num_ops, flags_t flags)
67 : flags_(flags)
68 , node_(node)
69 , mut_(true)
70 , external_(false)
71 , dep_(Dep::Mut | (node == Node::Infer ? Dep::Infer : Dep::None))
72 , num_ops_(num_ops)
73 , type_(type) {
74 gid_ = world().next_gid();
75 hash_ = murmur3(gid());
76 var_ = nullptr;
77 vars_.free = Vars();
78 muts_.fv_consumers = Muts();
79 std::fill_n(ops_ptr(), num_ops, nullptr);
80 if (!type->dep_const()) type->uses_.emplace(this, Use::Type);
81}
82
83Nat::Nat(World& world)
84 : Def(Node, world.type(), Defs{}, 0) {}
85
86UMax::UMax(World& world, Defs ops)
87 : Def(Node, world.univ(), ops, 0) {}
88
89// clang-format off
90
91/*
92 * rebuild
93 */
94
95#ifndef DOXYGEN // TODO Doxygen doesn't expand THORIN_DEF_MIXIN
96Ref Infer ::rebuild_(World&, Ref, Defs ) const { fe::unreachable(); }
97Ref Global ::rebuild_(World&, Ref, Defs ) const { fe::unreachable(); }
98Ref Idx ::rebuild_(World& w, Ref , Defs ) const { return w.type_idx(); }
99Ref Nat ::rebuild_(World& w, Ref , Defs ) const { return w.type_nat(); }
100Ref Univ ::rebuild_(World& w, Ref , Defs ) const { return w.univ(); }
101Ref Ac ::rebuild_(World& w, Ref t, Defs o) const { return w.ac(t, o); }
102Ref App ::rebuild_(World& w, Ref , Defs o) const { return w.app(o[0], o[1]); }
103Ref Arr ::rebuild_(World& w, Ref , Defs o) const { return w.arr(o[0], o[1]); }
104Ref Extract ::rebuild_(World& w, Ref , Defs o) const { return w.extract(o[0], o[1]); }
105Ref Insert ::rebuild_(World& w, Ref , Defs o) const { return w.insert(o[0], o[1], o[2]); }
106Ref Lam ::rebuild_(World& w, Ref t, Defs o) const { return w.lam(t->as<Pi>(), o[0], o[1]); }
107Ref Lit ::rebuild_(World& w, Ref t, Defs ) const { return w.lit(t, get()); }
108Ref Pack ::rebuild_(World& w, Ref t, Defs o) const { return w.pack(t->arity(), o[0]); }
109Ref Pi ::rebuild_(World& w, Ref , Defs o) const { return w.pi(o[0], o[1], is_implicit()); }
110Ref Pick ::rebuild_(World& w, Ref t, Defs o) const { return w.pick(t, o[0]); }
111Ref Proxy ::rebuild_(World& w, Ref t, Defs o) const { return w.proxy(t, o, pass(), tag()); }
112Ref Sigma ::rebuild_(World& w, Ref , Defs o) const { return w.sigma(o); }
113Ref Singleton::rebuild_(World& w, Ref , Defs o) const { return w.singleton(o[0]); }
114Ref Type ::rebuild_(World& w, Ref , Defs o) const { return w.type(o[0]); }
115Ref Test ::rebuild_(World& w, Ref , Defs o) const { return w.test(o[0], o[1], o[2], o[3]); }
116Ref Tuple ::rebuild_(World& w, Ref t, Defs o) const { return w.tuple(t, o); }
117Ref UInc ::rebuild_(World& w, Ref , Defs o) const { return w.uinc(o[0], offset()); }
118Ref UMax ::rebuild_(World& w, Ref , Defs o) const { return w.umax(o); }
119Ref Var ::rebuild_(World& w, Ref t, Defs o) const { return w.var(t, o[0]->as_mut()); }
120Ref Vel ::rebuild_(World& w, Ref t, Defs o) const { return w.vel(t, o[0])->set(dbg()); }
121
122Ref Axiom ::rebuild_(World& w, Ref t, Defs ) const {
123 if (&w != &world()) return w.axiom(normalizer(), curry(), trip(), t, plugin(), tag(), sub())->set(dbg());
124 assert(Check::alpha(t, type()));
125 return this;
126}
127
128template<bool up> Ref TExt <up>::rebuild_(World& w, Ref t, Defs ) const { return w.ext <up>(t)->set(dbg()); }
129template<bool up> Ref TBound<up>::rebuild_(World& w, Ref , Defs o) const { return w.bound<up>(o)->set(dbg()); }
130#endif
131
132/*
133 * stub
134 */
135
136Arr* Arr ::stub_(World& w, Ref t) { return w.mut_arr (t); }
137Global* Global::stub_(World& w, Ref t) { return w.global (t, is_mutable()); }
138Infer* Infer ::stub_(World& w, Ref t) { return w.mut_infer(t); }
139Lam* Lam ::stub_(World& w, Ref t) { return w.mut_lam (t->as<Pi>()); }
140Pack* Pack ::stub_(World& w, Ref t) { return w.mut_pack (t); }
141Pi* Pi ::stub_(World& w, Ref t) { return w.mut_pi (t, is_implicit()); }
142Sigma* Sigma ::stub_(World& w, Ref t) { return w.mut_sigma(t, num_ops()); }
143
144template<bool up> TBound<up>* TBound<up>::stub_(World& w, Ref t) { return w.mut_bound<up>(t, num_ops()); }
145template<bool up> TExt <up>* TExt <up>::stub_(World& , Ref ) { fe::unreachable(); }
146
147/*
148 * instantiate templates
149 */
150
151#ifndef DOXYGEN
152template Ref TExt<false> ::rebuild_(World&, Ref, Defs) const;
153template Ref TExt<true > ::rebuild_(World&, Ref, Defs) const;
154template Ref TBound<false>::rebuild_(World&, Ref, Defs) const;
155template Ref TBound<true >::rebuild_(World&, Ref, Defs) const;
160#endif
161
162// clang-format on
163
164/*
165 * immutabilize
166 */
167
168// TODO check for recursion
170 if (auto var = has_var(); var && codom()->free_vars().contains(var)) return nullptr;
171 return world().pi(dom(), codom());
172}
173
175 if (auto v = has_var(); v && std::ranges::any_of(ops(), [v](auto op) { return op->free_vars().contains(v); }))
176 return nullptr;
177 return static_cast<const Sigma*>(*world().sigma(ops()));
178}
179
181 auto& w = world();
182 if (auto var = has_var(); !var || !body()->free_vars().contains(var)) return w.arr(shape(), body());
183
184 if (auto n = Lit::isa(shape()); n && *n < w.flags().scalerize_threshold)
185 return w.sigma(DefVec(*n, [&](size_t i) { return reduce(w.lit_idx(*n, i)); }));
186
187 return nullptr;
188}
189
191 auto& w = world();
192 if (auto var = has_var(); !var || !body()->free_vars().contains(var)) return w.pack(shape(), body());
193
194 if (auto n = Lit::isa(shape()); n && *n < w.flags().scalerize_threshold)
195 return w.tuple(DefVec(*n, [&](size_t i) { return reduce(w.lit_idx(*n, i)); }));
196
197 return nullptr;
198}
199
200/*
201 * reduce
202 */
203
204const Def* Arr::reduce(const Def* arg) const {
205 if (auto mut = isa_mut<Arr>()) return rewrite(1, mut, arg);
206 return body();
207}
208
209const Def* Pack::reduce(const Def* arg) const {
210 if (auto mut = isa_mut<Pack>()) return rewrite(0, mut, arg);
211 return body();
212}
213
214DefVec Def::reduce(const Def* arg) const {
215 if (auto mut = isa_mut()) return mut->reduce(arg);
216 return DefVec(ops().begin(), ops().end());
217}
218
219DefVec Def::reduce(const Def* arg) {
220 auto& cache = world().move_.cache;
221 if (auto i = cache.find({this, arg}); i != cache.end()) return i->second;
222
223 return cache[{this, arg}] = rewrite(this, arg);
224}
225
226const Def* Def::refine(size_t i, const Def* new_op) const {
227 DefVec new_ops(ops().begin(), ops().end());
228 new_ops[i] = new_op;
229 return rebuild(type(), new_ops);
230}
231
232/*
233 * Def - set
234 */
235
236void Def::finalize() {
237 for (size_t i = Use::Type; auto op : partial_ops()) {
238 if (op) {
239 dep_ |= op->dep();
240 if (!op->dep_const()) {
241 const auto& p = op->uses_.emplace(this, i);
242 assert_unused(p.second);
243 }
244 }
245 ++i;
246 }
247}
248
249// clang-format off
250Def* 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; }
251Def* 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; }
252// clang-format on
253
254Def* Def::set(size_t i, const Def* def) {
255 invalidate();
256 assert(def && !op(i) && curr_op_ == i);
257#ifndef NDEBUG
258 curr_op_ = (curr_op_ + 1) % num_ops();
259#endif
260 ops_ptr()[i] = def;
261 const auto& p = def->uses_.emplace(this, i);
262 assert_unused(p.second);
263
264 if (i == num_ops() - 1) {
265 check();
266 update();
267 }
268
269 return this;
270}
271
273 invalidate();
274#ifndef NDEBUG
275 curr_op_ = 0;
276#endif
277 for (size_t i = 0, e = num_ops(); i != e; ++i) {
278 if (op(i))
279 unset(i);
280 else {
281 assert(std::all_of(ops_ptr() + i + 1, ops_ptr() + num_ops(), [](auto op) { return !op; }));
282 break;
283 }
284 }
285 return this;
286}
287
288Def* Def::unset(size_t i) {
289 invalidate();
290 assert(op(i) && op(i)->uses_.contains(Use(this, i)));
291 op(i)->uses_.erase(Use(this, i));
292 ops_ptr()[i] = nullptr;
293 return this;
294}
295
296Def* Def::set_type(const Def* type) {
297 if (type_ != type) {
298 invalidate();
299 if (type_ != nullptr) unset_type();
300 type_ = type;
301 type->uses_.emplace(this, Use::Type);
302 }
303 return this;
304}
305
307 if (type_) {
308 invalidate();
309 assert(type_->uses_.contains(Use(this, Use::Type)));
310 type_->uses_.erase(Use(this, Use::Type));
311 type_ = nullptr;
312 }
313}
314
315bool Def::is_set() const {
316 if (num_ops() == 0) return true;
317 bool result = ops().back();
318 assert((!result || std::ranges::all_of(ops().rsubspan(1), [](auto op) { return op; }))
319 && "the last operand is set but others in front of it aren't");
320 return result;
321}
322
323/*
324 * free_vars
325 */
326
328 if (auto mut = isa_mut()) return world().muts(mut);
329 return muts_.local;
330}
331
333 if (auto mut = isa_mut()) return mut->free_vars();
334
335 auto vars = local_vars();
336 for (auto mut : local_muts()) vars = world().merge(vars, mut->free_vars());
337 return vars;
338}
339
341 if (!isa_mut()) return const_cast<const Def*>(this)->free_vars();
342 if (!is_set()) return {};
343
344 if (!valid_) {
345 // fixed-point interation to recompute vars_.free
346 uint32_t run = 1;
347 for (bool todo = true; todo;) {
348 todo = false;
349 free_vars(todo, ++run);
350 }
351 validate();
352 }
353
354 return vars_.free;
355}
356
357Vars Def::free_vars(bool& todo, uint32_t run) {
358 // Recursively recompute vars_.free. If
359 // * valid_ == true: no recomputation is necessary
360 // * mark_ == run: We are running in cycles within the *current* iteration of our fixed-point loop
361 if (valid_ || mark_ == run) return vars_.free;
362 mark_ = run;
363
364 auto fvs0 = vars_.free;
365 auto fvs = fvs0;
366
367 for (auto op : extended_ops()) fvs = world().merge(fvs, op->local_vars());
368
369 for (auto op : extended_ops()) {
370 for (auto local_mut : op->local_muts()) {
371 local_mut->muts_.fv_consumers = world().insert(local_mut->muts_.fv_consumers, this);
372 fvs = world().merge(fvs, local_mut->free_vars(todo, run));
373 }
374 }
375
376 if (auto var = has_var()) fvs = world().erase(fvs, var); // FV(λx.e) = FV(e) \ {x}
377
378 todo |= fvs0 != fvs;
379 return vars_.free = fvs;
380}
381
382void Def::validate() {
383 valid_ = true;
384 mark_ = 0;
385
386 for (auto op : extended_ops()) {
387 for (auto local_mut : op->local_muts())
388 if (!local_mut->valid_) local_mut->validate();
389 }
390}
391
392void Def::invalidate() {
393 if (valid_) {
394 valid_ = false;
395 for (auto mut : fv_consumers()) mut->invalidate();
396 vars_.free.clear();
397 muts_.fv_consumers.clear();
398 }
399}
400
401bool Def::is_closed() const {
402 if (local_vars().empty() && local_muts().empty()) return true;
403#ifdef THORIN_ENABLE_CHECKS
404 assert(!is_external() || free_vars().empty());
405#endif
406 return free_vars().empty();
407}
408
409bool Def::is_open() const {
410 if (!local_vars().empty() || !local_muts().empty()) return true;
411 return !free_vars().empty();
412}
413/*
414 * Def - misc
415 */
416
417Sym Def::sym(const char* s) const { return world().sym(s); }
418Sym Def::sym(std::string_view s) const { return world().sym(s); }
419Sym Def::sym(std::string s) const { return world().sym(std::move(s)); }
420
422 if (isa<Univ>()) return *world_;
423 if (auto type = isa<Type>()) return type->level()->world();
424 return type()->world(); // TODO unroll
425}
426
427const Def* Def::unfold_type() const {
428 if (!type_) {
429 if (auto t = isa<Type>()) return world().type(world().uinc(t->level()));
430 assert(isa<Univ>());
431 return nullptr;
432 }
433
434 return type_;
435}
436
437std::string_view Def::node_name() const {
438 switch (node()) {
439#define CODE(op, abbr) \
440 case Node::op: return #abbr;
442#undef CODE
443 default: fe::unreachable();
444 }
445}
446
448 if (isa<Type>() || isa<Univ>()) return Defs();
449 assert(type());
450 return Defs(ops_ptr() - 1, (is_set() ? num_ops_ : 0) + 1);
451}
452
453#ifndef NDEBUG
454const Def* Def::debug_prefix(std::string prefix) const {
455 dbg_.sym = world().sym(prefix + sym().str());
456 return this;
457}
458
459const Def* Def::debug_suffix(std::string suffix) const {
460 dbg_.sym = world().sym(sym().str() + suffix);
461 return this;
462}
463#endif
464
465// clang-format off
466
468 if (var_) return var_;
469 auto& w = world();
470
471 if (w.is_frozen()) return nullptr;
472 if (auto lam = isa<Lam >()) return w.var(lam ->dom(), lam);
473 if (auto pi = isa<Pi >()) return w.var(pi ->dom(), pi);
474 if (auto sig = isa<Sigma>()) return w.var(sig, sig);
475 if (auto arr = isa<Arr >()) return w.var(w.type_idx(arr ->shape()), arr ); // TODO shapes like (2, 3)
476 if (auto pack = isa<Pack >()) return w.var(w.type_idx(pack->shape()), pack); // TODO shapes like (2, 3)
477 if (isa<Bound >()) return w.var(this, this);
478 if (isa<Infer >()) return nullptr;
479 if (isa<Global>()) return nullptr;
480 fe::unreachable();
481}
482
483bool Def::is_term() const {
484 if (auto t = type()) {
485 if (auto u = t->type()) {
486 if (auto type = u->isa<Type>()) {
487 if (auto level = Lit::isa(type->level())) return *level == 0;
488 }
489 }
490 }
491 return false;
492}
493
495 if (auto sigma = isa<Sigma>()) return world().lit_nat(sigma->num_ops());
496 if (auto arr = isa<Arr >()) return arr->shape();
497 if (auto t = type()) return t->arity();
498 return world().lit_nat_1();
499}
500
501std::optional<nat_t> Def::isa_lit_arity() const {
502 if (auto sigma = isa<Sigma>()) return sigma->num_ops();
503 if (auto arr = isa<Arr >()) return Lit::isa(arr->shape());
504 if (auto t = type()) return t->isa_lit_arity();
505 return 1;
506}
507
508// clang-format on
509
510bool Def::equal(const Def* other) const {
511 if (isa<Univ>() || this->isa_mut() || other->isa_mut()) return this == other;
512
513 bool result = this->node() == other->node() && this->flags() == other->flags()
514 && this->num_ops() == other->num_ops() && this->type() == other->type();
515
516 for (size_t i = 0, e = num_ops(); result && i != e; ++i) result &= this->op(i) == other->op(i);
517
518 return result;
519}
520
521void Def::make_external() { return world().make_external(this); }
522void Def::make_internal() { return world().make_internal(this); }
523
524std::string Def::unique_name() const { return sym().str() + "_"s + std::to_string(gid()); }
525
527 if (auto a = isa_lit_arity(); a && *a < world().flags().scalerize_threshold) return *a;
528 return 1;
529}
530
531const Def* Def::proj(nat_t a, nat_t i) const {
532 static constexpr int Search_In_Uses_Threshold = 8;
533
534 if (a == 1) {
535 if (!type()) return this;
536 if (!isa_mut<Sigma>() && !type()->isa_mut<Sigma>()) return this;
537 }
538
539 World& w = world();
540
541 if (isa<Tuple>() || isa<Sigma>()) {
542 return op(i);
543 } else if (auto arr = isa<Arr>()) {
544 if (arr->arity()->isa<Top>()) return arr->body();
545 return arr->reduce(w.lit_idx(a, i));
546 } else if (auto pack = isa<Pack>()) {
547 if (pack->arity()->isa<Top>()) return pack->body();
548 assert(!w.is_frozen() && "TODO");
549 return pack->reduce(w.lit_idx(a, i));
550 }
551
552 if (w.is_frozen() || uses().size() < Search_In_Uses_Threshold) {
553 for (auto u : uses()) {
554 if (auto ex = u->isa<Extract>(); ex && ex->tuple() == this) {
555 if (auto index = Lit::isa(ex->index()); index && *index == i) return ex;
556 }
557 }
558
559 if (w.is_frozen()) return nullptr;
560 }
561
562 return w.extract(this, a, i);
563}
564
565/*
566 * Idx
567 */
568
570 if (auto app = def->isa<App>()) {
571 if (app->callee()->isa<Idx>()) return app->arg();
572 }
573
574 return nullptr;
575}
576
577std::optional<nat_t> Idx::size2bitwidth(const Def* size) {
578 if (size->isa<Top>()) return 64;
579 if (auto s = Lit::isa(size)) return size2bitwidth(*s);
580 return {};
581}
582
583/*
584 * Global
585 */
586
587const App* Global::type() const { return Def::type()->as<App>(); }
588const Def* Global::alloced_type() const { return type()->arg(0); }
589
590} // namespace thorin
const Def * arg() const
Definition lam.h:215
A (possibly paramterized) Array.
Definition tuple.h:50
const Def * body() const
Definition tuple.h:61
const Def * reduce(const Def *arg) const
Definition def.cpp:204
const Def * shape() const
Definition tuple.h:60
const Def * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:180
static bool alpha(Ref d1, Ref d2)
Are d1 and d2 α-equivalent?
Definition check.h:59
Base class for all Defs.
Definition def.h:222
Muts local_muts() const
Definition def.cpp:327
void make_external()
Definition def.cpp:521
Def * reset(size_t i, const Def *def)
Successively reset from left to right.
Definition def.h:291
Ref arity() const
Definition def.cpp:494
const Def * refine(size_t i, const Def *new_op) const
Definition def.cpp:226
Ref var()
Not necessarily a Var: E.g., if the return type is [], this will yield ().
Definition def.cpp:467
auto vars()
Definition def.h:403
void update()
Resolves Infers of this Def's type.
Definition def.h:299
auto ops() const
Definition def.h:268
std::optional< nat_t > isa_lit_arity() const
Definition def.cpp:501
std::string unique_name() const
name + "_" + Def::gid
Definition def.cpp:524
flags_t flags_
Definition def.h:577
Defs extended_ops() const
Definition def.cpp:447
bool is_open() const
Has free_vars()?
Definition def.cpp:409
bool is_set() const
Yields true if empty or the last op is set.
Definition def.cpp:315
Muts fv_consumers()
Definition def.h:428
bool is_external() const
Definition def.h:433
u32 gid() const
Definition def.h:238
Def * set_type(const Def *)
Definition def.cpp:296
unsigned dep() const
Definition def.h:335
const Def * op(size_t i) const
Definition def.h:269
const Uses & uses() const
Definition def.h:328
size_t num_ops() const
Definition def.h:270
const Def * debug_prefix(std::string) const
Definition def.cpp:454
Def * unset()
Unsets all Def::ops; works even, if not set at all or partially.
Definition def.cpp:272
Ref rebuild(World &w, Ref type, Defs ops) const
Def::rebuilds this Def while using new_op as substitute for its i'th Def::op.
Definition def.h:498
const Def * type() const
Yields the raw type of this Def, i.e. maybe nullptr.
Definition def.h:248
DefVec reduce(const Def *arg) const
Rewrites Def::ops by substituting this mutable's Var with arg.
Definition def.cpp:214
std::string_view node_name() const
Definition def.cpp:437
T * isa_mut() const
If this is *mut*able, it will cast constness away and perform a dynamic_cast to T.
Definition def.h:449
void make_internal()
Definition def.cpp:522
bool is_term() const
Yields true if this:T and T:(.Type 0).
Definition def.cpp:483
Vars free_vars() const
Definition def.cpp:332
Vars local_vars() const
Definition def.h:423
bool is_closed() const
Has no free_vars()?
Definition def.cpp:401
Defs partial_ops() const
Definition def.h:321
void unset_type()
Definition def.cpp:306
Dbg dbg_
Definition def.h:570
const Var * has_var()
Only returns not nullptr, if Var of this mutable has ever been created.
Definition def.h:407
const Def * unfold_type() const
Yields the type of this Def and builds a new .Type (UInc n) if necessary.
Definition def.cpp:427
Sym sym() const
Definition def.h:470
flags_t flags() const
Definition def.h:237
const Def * debug_suffix(std::string) const
Definition def.cpp:459
virtual void check()
Definition def.h:517
nat_t num_tprojs() const
As above but yields 1, if Flags::scalerize_threshold is exceeded.
Definition def.cpp:526
Def * set(size_t i, const Def *def)
Successively set from left to right.
Definition def.cpp:254
node_t node() const
Definition def.h:240
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:531
bool dep_const() const
Definition def.h:338
virtual Ref rebuild_(World &w, Ref type, Defs ops) const =0
World & world() const
Definition def.cpp:421
Extracts from a Sigma or Array-typed Extract::tuple the element at position Extract::index.
Definition tuple.h:118
const Def * tuple() const
Definition tuple.h:126
bool is_mutable() const
Definition def.h:805
const App * type() const
Definition def.cpp:587
const Def * alloced_type() const
Definition def.cpp:588
Global * stub_(World &, Ref) override
Definition def.cpp:137
A built-in constant of type .Nat -> *.
Definition def.h:745
static Ref size(Ref def)
Checks if def is a .Idx s and returns s or nullptr otherwise.
Definition def.cpp:569
static constexpr nat_t size2bitwidth(nat_t n)
Definition def.h:758
This node is a hole in the IR that is inferred by its context later on.
Definition check.h:12
A function.
Definition lam.h:97
static std::optional< T > isa(Ref def)
Definition def.h:726
A (possibly paramterized) Tuple.
Definition tuple.h:87
const Def * body() const
Definition tuple.h:97
const Def * shape() const
Definition tuple.cpp:41
const Def * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:190
const Def * reduce(const Def *arg) const
Definition def.cpp:209
A dependent function type.
Definition lam.h:11
const Pi * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:169
Ref dom() const
Definition lam.h:32
Ref codom() const
Definition lam.h:40
constexpr bool contains(const T &elem) const
Definition pool.h:66
constexpr bool empty() const noexcept
Definition pool.h:61
Helper class to retrieve Infer::arg if present.
Definition def.h:87
A dependent tuple type.
Definition tuple.h:9
const Def * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:174
This is a thin wrapper for std::span<T, N> with the following additional features:
Definition span.h:28
Specific Bound depending on Up.
Definition lattice.h:31
Ref rebuild_(World &, Ref, Defs) const override
TBound * stub_(World &, Ref) override
Definition def.cpp:144
Extremum. Either Top (Up) or Bottom.
Definition lattice.h:130
TExt * stub_(World &, Ref) override
Definition def.cpp:145
Ref rebuild_(World &, Ref, Defs) const override
References a user.
Definition def.h:109
static constexpr size_t Type
Definition def.h:111
The World represents the whole program and manages creation of Thorin nodes (Defs).
Definition world.h:35
Ref insert(Ref d, Ref i, Ref val)
Definition world.cpp:340
Vars erase(Vars vars, const Var *var)
Definition world.h:490
Flags & flags()
Retrive compile Flags.
Definition world.cpp:74
void make_external(Def *def)
Definition world.h:151
Sym sym(std::string_view)
Definition world.cpp:77
u32 next_gid()
Definition world.h:92
Vars vars(const Var *var)
Definition world.h:484
const Pi * pi(Ref dom, Ref codom, bool implicit=false)
Definition world.h:234
Muts muts(Def *mut)
Definition world.h:485
Ref sigma(Defs ops)
Definition world.cpp:218
void make_internal(Def *def)
Definition world.h:157
const Lit * lit_nat(nat_t a)
Definition world.h:367
const Lit * lit_nat_1()
Definition world.h:369
Vars merge(Vars a, Vars b)
Definition world.h:486
const Type * type(Ref level)
Definition world.cpp:92
#define CODE(node, name)
Definition def.h:40
#define THORIN_NODE(m)
Definition def.h:19
void * get(void *handle, const char *symbol_name)
Definition dl.cpp:36
Definition cfg.h:11
DefVec rewrite(Def *mut, Ref arg)
Definition rewrite.cpp:45
hash_t murmur3_finalize(hash_t h, hash_t len)
Definition hash.h:51
u64 nat_t
Definition types.h:44
uint64_t scalerize_threshold
Definition flags.h:13
Dep
Definition def.h:146
View< const Def * > Defs
Definition def.h:62
uint32_t u32
Definition types.h:35
PooledSet< Def * > Muts
Definition def.h:72
DefVec merge(Defs, Defs)
Definition tuple.cpp:87
hash_t murmur3(hash_t h, uint32_t key)
Definition hash.h:22
uint8_t u8
Definition types.h:35
Sym sym
Definition dbg.h:33
u8 node_t
Definition types.h:45
Vector< const Def * > DefVec
Definition def.h:63
u64 flags_t
Definition types.h:46
hash_t murmur3_rest(hash_t h, uint8_t key)
Definition hash.h:41
PooledSet< const Var * > Vars
Definition def.h:81