MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
world.h
Go to the documentation of this file.
1#pragma once
2
3#include <string>
4#include <string_view>
5#include <type_traits>
6
7#include <absl/container/btree_map.h>
8#include <absl/container/btree_set.h>
9#include <fe/arena.h>
10
11#include "mim/axiom.h"
12#include "mim/check.h"
13#include "mim/flags.h"
14#include "mim/lam.h"
15#include "mim/lattice.h"
16#include "mim/tuple.h"
17
18#include "mim/util/dbg.h"
19#include "mim/util/log.h"
20
21namespace mim {
22class Driver;
23
24/// The World represents the whole program and manages creation of MimIR nodes (Def%s).
25/// Def%s are hashed into an internal HashSet.
26/// The World's factory methods just calculate a hash and lookup the Def, if it is already present, or create a new one
27/// otherwise. This corresponds to value numbering.
28///
29/// You can create several worlds.
30/// All worlds are completely independent from each other.
31///
32/// Note that types are also just Def%s and will be hashed as well.
33class World {
34public:
35 /// @name State
36 ///@{
37 struct State {
38 State() = default;
39
40 /// [Plain Old Data](https://en.cppreference.com/w/cpp/named_req/PODType)
41 struct POD {
44 Loc loc;
45 Sym name;
46 mutable bool frozen = false;
47 } pod;
48
49#ifdef MIM_ENABLE_CHECKS
50 absl::flat_hash_set<uint32_t> breakpoints;
51#endif
52 friend void swap(State& s1, State& s2) noexcept {
53 using std::swap;
54 assert((!s1.pod.loc || !s2.pod.loc) && "Why is get_loc() still set?");
55 swap(s1.pod, s2.pod);
56#ifdef MIM_ENABLE_CHECKS
57 swap(s1.breakpoints, s2.breakpoints);
58#endif
59 }
60 };
61
62 /// @name Construction & Destruction
63 ///@{
64 World& operator=(World) = delete;
65
66 explicit World(Driver*);
67 World(Driver*, const State&);
68 World(World&& other) noexcept
69 : World(&other.driver(), other.state()) {
70 swap(*this, other);
71 }
72 World inherit() { return World(&driver(), state()); } ///< Inherits the @p state into the new World.
73 ~World();
74 ///@}
75
76 /// @name Getters/Setters
77 ///@{
78 const State& state() const { return state_; }
79
80 const Driver& driver() const { return *driver_; }
81 Driver& driver() { return *driver_; }
82
83 Sym name() const { return state_.pod.name; }
84 void set(Sym name) { state_.pod.name = name; }
85 void set(std::string_view name) { state_.pod.name = sym(name); }
86
87 /// Manage global identifier - a unique number for each Def.
88 u32 curr_gid() const { return state_.pod.curr_gid; }
89 u32 next_gid() { return ++state_.pod.curr_gid; }
90 u32 next_run() { return ++data_.curr_run; }
91
92 /// Retrieve compile Flags.
93 Flags& flags();
94 ///@}
95
96 /// @name Loc
97 ///@{
98 struct ScopedLoc {
99 ScopedLoc(World& world, Loc old_loc)
100 : world_(world)
101 , old_loc_(old_loc) {}
102 ~ScopedLoc() { world_.set_loc(old_loc_); }
103
104 private:
105 World& world_;
106 Loc old_loc_;
107 };
108
109 Loc get_loc() const { return state_.pod.loc; }
110 void set_loc(Loc loc = {}) { state_.pod.loc = loc; }
111 ScopedLoc push(Loc loc) {
112 auto sl = ScopedLoc(*this, get_loc());
113 set_loc(loc);
114 return sl;
115 }
116 ///@}
117
118 /// @name Sym
119 ///@{
120 Sym sym(std::string_view);
121 Sym sym(const char*);
122 Sym sym(const std::string&);
123 /// Appends a @p suffix or an increasing number if the suffix already exists.
124 Sym append_suffix(Sym name, std::string suffix);
125 ///@}
126
127 /// @name Freeze
128 /// In frozen state the World does not create any nodes.
129 ///@{
130 bool is_frozen() const { return state_.pod.frozen; }
131
132 /// Yields old frozen state.
133 bool freeze(bool on = true) const {
134 bool old = state_.pod.frozen;
135 state_.pod.frozen = on;
136 return old;
137 }
138
139 /// Use to World::freeze and automatically unfreeze at the end of scope.
140 struct Freezer {
142 : world(world)
143 , old(world.freeze(true)) {}
145
146 const World& world;
147 bool old;
148 };
149 ///@}
150
151 /// @name Debugging Features
152 ///@{
153#ifdef MIM_ENABLE_CHECKS
154 const auto& breakpoints() { return state_.breakpoints; }
155
156 Ref gid2def(u32 gid); ///< Lookup Def by @p gid.
157 void breakpoint(u32 gid); ///< Trigger breakpoint in your debugger when creating Def with Def::gid @p gid.
158
159 World& verify(); ///< Verifies that all externals() and annexes() are Def::is_closed(), if `MIM_ENABLE_CHECKS`.
160#else
161 World& verify() { return *this; }
162#endif
163 ///@}
164
165 /// @name Annexes
166 ///@{
167 const auto& flags2annex() const { return move_.flags2annex; }
168 auto annexes() const { return move_.flags2annex | std::views::values; }
169
170 /// Lookup annex by Axiom::id.
171 template<class Id> const Def* annex(Id id) {
172 auto flags = static_cast<flags_t>(id);
173 if (auto i = move_.flags2annex.find(flags); i != move_.flags2annex.end()) return i->second;
174 error("Axiom with ID '{x}' not found; demangled plugin name is '{}'", flags, Annex::demangle(driver(), flags));
175 }
176
177 /// Get Axiom from a plugin.
178 /// Can be used to get an Axiom without sub-tags.
179 /// E.g. use `w.annex<mem::M>();` to get the `%mem.M` Axiom.
180 template<annex_without_subs id> const Def* annex() { return annex(Annex::Base<id>); }
181
182 const Def* register_annex(flags_t f, const Def*);
183 const Def* register_annex(plugin_t p, tag_t t, sub_t s, const Def* def) {
184 return register_annex(p | (flags_t(t) << 8_u64) | flags_t(s), def);
185 }
186 ///@}
187
188 /// @name Externals
189 ///@{
190 const auto& sym2external() const { return move_.sym2external; }
191 Def* external(Sym name) { return mim::lookup(move_.sym2external, name); } ///< Lookup by @p name.
192 auto externals() const { return move_.sym2external | std::views::values; }
193 Vector<Def*> copy_externals() const { return {externals().begin(), externals().end()}; }
194
195 void make_external(Def* def) {
196 assert(!def->is_external());
197 assert(def->is_closed());
198 def->external_ = true;
199 assert_emplace(move_.sym2external, def->sym(), def);
200 }
201 void make_internal(Def* def) {
202 assert(def->is_external());
203 def->external_ = false;
204 auto num = move_.sym2external.erase(def->sym());
205 assert_unused(num == 1);
206 }
207 ///@}
208
209 /// @name Univ, Type, Var, Proxy, Infer
210 ///@{
211 const Univ* univ() { return data_.univ; }
212 Ref uinc(Ref op, level_t offset = 1);
213 template<Sort = Sort::Univ> Ref umax(Defs);
214 const Type* type(Ref level);
215 const Type* type_infer_univ() { return type(mut_infer_univ()); }
216 template<level_t level = 0> const Type* type() {
217 if constexpr (level == 0)
218 return data_.type_0;
219 else if constexpr (level == 1)
220 return data_.type_1;
221 else
222 return type(lit_univ(level));
223 }
224 Ref var(Ref type, Def* mut);
225 const Proxy* proxy(Ref type, Defs ops, u32 index, u32 tag) {
226 return unify<Proxy>(ops.size(), type, ops, index, tag);
227 }
228
232
233 /// Either a value `?:?:Type ?` or a type `?:Type ?:Type ?`.
235 auto t = type_infer_univ();
236 auto res = mut_infer(mut_infer(t));
237 assert(this == &res->world());
238 return res;
239 }
240 ///@}
241
242 /// @name Axiom
243 ///@{
244 const Axiom* axiom(NormalizeFn n, u8 curry, u8 trip, Ref type, plugin_t p, tag_t t, sub_t s) {
245 return unify<Axiom>(0, n, curry, trip, type, p, t, s);
246 }
247 const Axiom* axiom(Ref type, plugin_t p, tag_t t, sub_t s) { return axiom(nullptr, 0, 0, type, p, t, s); }
248
249 /// Builds a fresh Axiom with descending Axiom::sub.
250 /// This is useful during testing to come up with some entity of a specific type.
251 /// It uses the plugin Axiom::Global_Plugin and starts with `0` for Axiom::sub and counts up from there.
252 /// The Axiom::tag is set to `0` and the Axiom::normalizer to `nullptr`.
253 const Axiom* axiom(NormalizeFn n, u8 curry, u8 trip, Ref type) {
254 return axiom(n, curry, trip, type, Annex::Global_Plugin, 0, state_.pod.curr_sub++);
255 }
256 const Axiom* axiom(Ref type) { return axiom(nullptr, 0, 0, type); } ///< See above.
257 ///@}
258
259 /// @name Pi
260 ///@{
261 // clang-format off
262 const Pi* pi(Ref dom, Ref codom, bool implicit = false) { return unify<Pi>(2, Pi::infer(dom, codom), dom, codom, implicit); }
263 const Pi* pi(Defs dom, Ref codom, bool implicit = false) { return pi(sigma(dom), codom, implicit); }
264 const Pi* pi(Ref dom, Defs codom, bool implicit = false) { return pi(dom, sigma(codom), implicit); }
265 const Pi* pi(Defs dom, Defs codom, bool implicit = false) { return pi(sigma(dom), sigma(codom), implicit); }
266 Pi* mut_pi(Ref type, bool implicit = false) { return insert<Pi>(2, type, implicit); }
267 // clang-format on
268 ///@}
269
270 /// @name Cn
271 /// Pi with codom mim::Bot%tom
272 ///@{
273 // clang-format off
274 const Pi* cn( ) { return cn(sigma( ), false); }
275 const Pi* cn(Ref dom, bool implicit = false) { return pi( dom , type_bot(), implicit); }
276 const Pi* cn(Defs dom, bool implicit = false) { return cn(sigma(dom), implicit); }
277 const Pi* fn(Ref dom, Ref codom, bool implicit = false) { return cn({ dom , cn(codom)}, implicit); }
278 const Pi* fn(Defs dom, Ref codom, bool implicit = false) { return fn(sigma(dom), codom, implicit); }
279 const Pi* fn(Ref dom, Defs codom, bool implicit = false) { return fn( dom , sigma(codom), implicit); }
280 const Pi* fn(Defs dom, Defs codom, bool implicit = false) { return fn(sigma(dom), sigma(codom), implicit); }
281 // clang-format on
282 ///@}
283
284 /// @name Lam
285 ///@{
287 if (auto b = std::get_if<bool>(&filter)) return lit_bool(*b);
288 return std::get<Ref>(filter);
289 }
290 const Lam* lam(const Pi* pi, Lam::Filter f, Ref body) { return unify<Lam>(2, pi, filter(f), body); }
291 Lam* mut_lam(const Pi* pi) { return insert<Lam>(2, pi); }
292 // clang-format off
293 const Lam* con(Ref dom, Lam::Filter f, Ref body) { return unify<Lam>(2, cn(dom ), filter(f), body); }
294 const Lam* con(Defs dom, Lam::Filter f, Ref body) { return unify<Lam>(2, cn(dom ), filter(f), body); }
295 const Lam* lam(Ref dom, Ref codom, Lam::Filter f, Ref body) { return unify<Lam>(2, pi(dom, codom), filter(f), body); }
296 const Lam* lam(Defs dom, Ref codom, Lam::Filter f, Ref body) { return unify<Lam>(2, pi(dom, codom), filter(f), body); }
297 const Lam* lam(Ref dom, Defs codom, Lam::Filter f, Ref body) { return unify<Lam>(2, pi(dom, codom), filter(f), body); }
298 const Lam* lam(Defs dom, Defs codom, Lam::Filter f, Ref body) { return unify<Lam>(2, pi(dom, codom), filter(f), body); }
299 const Lam* fun(Ref dom, Ref codom, Lam::Filter f, Ref body) { return unify<Lam>(2, fn(dom, codom), filter(f), body); }
300 const Lam* fun(Defs dom, Ref codom, Lam::Filter f, Ref body) { return unify<Lam>(2, fn(dom, codom), filter(f), body); }
301 const Lam* fun(Ref dom, Defs codom, Lam::Filter f, Ref body) { return unify<Lam>(2, fn(dom, codom), filter(f), body); }
302 const Lam* fun(Defs dom, Defs codom, Lam::Filter f, Ref body) { return unify<Lam>(2, fn(dom, codom), filter(f), body); }
303 Lam* mut_con(Ref dom ) { return insert<Lam>(2, cn(dom )); }
304 Lam* mut_con(Defs dom ) { return insert<Lam>(2, cn(dom )); }
305 Lam* mut_lam(Ref dom, Ref codom) { return insert<Lam>(2, pi(dom, codom)); }
306 Lam* mut_lam(Defs dom, Ref codom) { return insert<Lam>(2, pi(dom, codom)); }
307 Lam* mut_lam(Ref dom, Defs codom) { return insert<Lam>(2, pi(dom, codom)); }
308 Lam* mut_lam(Defs dom, Defs codom) { return insert<Lam>(2, pi(dom, codom)); }
309 Lam* mut_fun(Ref dom, Ref codom) { return insert<Lam>(2, fn(dom, codom)); }
310 Lam* mut_fun(Defs dom, Ref codom) { return insert<Lam>(2, fn(dom, codom)); }
311 Lam* mut_fun(Ref dom, Defs codom) { return insert<Lam>(2, fn(dom, codom)); }
312 Lam* mut_fun(Defs dom, Defs codom) { return insert<Lam>(2, fn(dom, codom)); }
313 // clang-format on
314 ///@}
315
316 /// @name App
317 ///@{
318 template<bool Normalize = true> Ref app(Ref callee, Ref arg);
319 template<bool Normalize = true> Ref app(Ref callee, Defs args) { return app<Normalize>(callee, tuple(args)); }
320 Ref raw_app(const Axiom* axiom, u8 curry, u8 trip, Ref type, Ref callee, Ref arg);
321 Ref raw_app(Ref type, Ref callee, Ref arg);
322 Ref raw_app(Ref type, Ref callee, Defs args) { return raw_app(type, callee, tuple(args)); }
323 ///@}
324
325 /// @name Sigma
326 ///@{
327 Sigma* mut_sigma(Ref type, size_t size) { return insert<Sigma>(size, type, size); }
328 /// A *mut*able Sigma of type @p level.
329 template<level_t level = 0> Sigma* mut_sigma(size_t size) { return mut_sigma(type<level>(), size); }
330 Ref sigma(Defs ops);
331 const Sigma* sigma() { return data_.sigma; } ///< The unit type within Type 0.
332 ///@}
333
334 /// @name Arr
335 ///@{
336 Arr* mut_arr(Ref type) { return insert<Arr>(2, type); }
337 template<level_t level = 0> Arr* mut_arr() { return mut_arr(type<level>()); }
338 Ref arr(Ref shape, Ref body);
339 Ref arr(Defs shape, Ref body);
340 Ref arr(u64 n, Ref body) { return arr(lit_nat(n), body); }
341 Ref arr(View<u64> shape, Ref body) {
342 return arr(DefVec(shape.size(), [&](size_t i) { return lit_nat(shape[i]); }), body);
343 }
344 Ref arr_unsafe(Ref body) { return arr(top_nat(), body); }
345 ///@}
346
347 /// @name Tuple
348 ///@{
349 Ref tuple(Defs ops);
350 /// Ascribes @p type to this tuple - needed for dependently typed and mutable Sigma%s.
351 Ref tuple(Ref type, Defs ops);
352 const Tuple* tuple() { return data_.tuple; } ///< the unit value of type `[]`
353 Ref tuple(Sym sym); ///< Converts @p sym to a tuple of type '«n; I8»'.
354 ///@}
355
356 /// @name Pack
357 ///@{
359 Ref pack(Ref arity, Ref body);
360 Ref pack(Defs shape, Ref body);
361 Ref pack(u64 n, Ref body) { return pack(lit_nat(n), body); }
362 Ref pack(View<u64> shape, Ref body) {
363 return pack(DefVec(shape.size(), [&](auto i) { return lit_nat(shape[i]); }), body);
364 }
365 ///@}
366
367 /// @name Extract
368 /// @see core::extract_unsafe
369 ///@{
370 Ref extract(Ref d, Ref i);
371 Ref extract(Ref d, u64 a, u64 i) { return extract(d, lit_idx(a, i)); }
372 Ref extract(Ref d, u64 i) { return extract(d, d->as_lit_arity(), i); }
373
374 /// Builds `(f, t)#cond`.
375 /// @note Expects @p cond as first, @p t as second, and @p f as third argument.
376 Ref select(Ref cond, Ref t, Ref f) { return extract(tuple({f, t}), cond); }
377 ///@}
378
379 /// @name Insert
380 /// @see core::insert_unsafe
381 ///@{
382 Ref insert(Ref d, Ref i, Ref val);
383 Ref insert(Ref d, u64 a, u64 i, Ref val) { return insert(d, lit_idx(a, i), val); }
384 Ref insert(Ref d, u64 i, Ref val) { return insert(d, d->as_lit_arity(), i, val); }
385 ///@}
386
387 /// @name Lit
388 ///@{
389 const Lit* lit(Ref type, u64 val);
390 const Lit* lit_univ(u64 level) { return lit(univ(), level); }
391 const Lit* lit_univ_0() { return data_.lit_univ_0; }
392 const Lit* lit_univ_1() { return data_.lit_univ_1; }
393 const Lit* lit_nat(nat_t a) { return lit(type_nat(), a); }
394 const Lit* lit_nat_0() { return data_.lit_nat_0; }
395 const Lit* lit_nat_1() { return data_.lit_nat_1; }
396 const Lit* lit_nat_max() { return data_.lit_nat_max; }
397 const Lit* lit_0_1() { return data_.lit_0_1; }
398 // clang-format off
399 const Lit* lit_i1() { return lit_nat(Idx::bitwidth2size( 1)); };
400 const Lit* lit_i8() { return lit_nat(Idx::bitwidth2size( 8)); };
401 const Lit* lit_i16() { return lit_nat(Idx::bitwidth2size(16)); };
402 const Lit* lit_i32() { return lit_nat(Idx::bitwidth2size(32)); };
403 const Lit* lit_i64() { return lit_nat(Idx::bitwidth2size(64)); };
404 /// Constructs a Lit of type Idx of size @p size.
405 /// @note `size = 0` means `2^64`.
406 const Lit* lit_idx(nat_t size, u64 val) { return lit(type_idx(size), val); }
407
408 template<class I> const Lit* lit_idx(I val) {
409 static_assert(std::is_integral<I>());
410 return lit_idx(Idx::bitwidth2size(sizeof(I) * 8), val);
411 }
412
413 /// Constructs a Lit @p of type Idx of size 2^width.
414 /// `val = 64` will be automatically converted to size `0` - the encoding for 2^64.
415 const Lit* lit_int(nat_t width, u64 val) { return lit_idx(Idx::bitwidth2size(width), val); }
416 const Lit* lit_i1 (bool val) { return lit_int( 1, u64(val)); }
417 const Lit* lit_i2 (u8 val) { return lit_int( 2, u64(val)); }
418 const Lit* lit_i4 (u8 val) { return lit_int( 4, u64(val)); }
419 const Lit* lit_i8 (u8 val) { return lit_int( 8, u64(val)); }
420 const Lit* lit_i16(u16 val) { return lit_int(16, u64(val)); }
421 const Lit* lit_i32(u32 val) { return lit_int(32, u64(val)); }
422 const Lit* lit_i64(u64 val) { return lit_int(64, u64(val)); }
423 // clang-format on
424
425 /// Constructs a Lit of type Idx of size @p mod.
426 /// The value @p val will be adjusted modulo @p mod.
427 /// @note `mod == 0` is the special case for 2^64 and no modulo will be performed on @p val.
428 const Lit* lit_idx_mod(nat_t mod, u64 val) { return lit_idx(mod, mod == 0 ? val : (val % mod)); }
429
430 const Lit* lit_bool(bool val) { return data_.lit_bool[size_t(val)]; }
431 const Lit* lit_ff() { return data_.lit_bool[0]; }
432 const Lit* lit_tt() { return data_.lit_bool[1]; }
433 // clang-format off
434 ///@}
435
436 /// @name Lattice
437 ///@{
438 template<bool Up>
439 Ref ext(Ref type);
441 Ref top(Ref type) { return ext<true>(type); }
442 Ref type_bot() { return data_.type_bot; }
443 Ref type_top() { return data_.type_top; }
444 Ref top_nat() { return data_.top_nat; }
445 template<bool Up> TBound<Up>* mut_bound(Ref type, size_t size) { return insert<TBound<Up>>(size, type, size); }
446 /// A *mut*able Bound of Type @p l%evel.
447 template<bool Up, level_t l = 0> TBound<Up>* mut_bound(size_t size) { return mut_bound<Up>(type<l>(), size); }
448 template<bool Up> Ref bound(Defs ops);
449 Join* mut_join(Ref type, size_t size) { return mut_bound<true>(type, size); }
450 Meet* mut_meet(Ref type, size_t size) { return mut_bound<false>(type, size); }
451 template<level_t l = 0> Join* mut_join(size_t size) { return mut_join(type<l>(), size); }
452 template<level_t l = 0> Meet* mut_meet(size_t size) { return mut_meet(type<l>(), size); }
453 Ref join(Defs ops) { return bound<true>(ops); }
454 Ref meet(Defs ops) { return bound<false>(ops); }
455 Ref ac(Ref type, Defs ops);
456 /// Infers the type using an *immutable* Meet.
457 Ref ac(Defs ops);
458 Ref vel(Ref type, Ref value);
459 Ref pick(Ref type, Ref value);
460 Ref test(Ref value, Ref probe, Ref match, Ref clash);
461 Ref uniq(Ref inhabitant);
462 ///@}
463
464 /// @name Globals
465 /// @deprecated Will be removed.
466 ///@{
467 Global* global(Ref type, bool is_mutable = true) { return insert<Global>(1, type, is_mutable); }
468 ///@}
469 // clang-format on
470
471 /// @name Types
472 ///@{
473 const Nat* type_nat() { return data_.type_nat; }
474 const Idx* type_idx() { return data_.type_idx; }
475 /// @note `size = 0` means `2^64`.
476 Ref type_idx(Ref size) { return app(type_idx(), size); }
477 /// @note `size = 0` means `2^64`.
478 Ref type_idx(nat_t size) { return type_idx(lit_nat(size)); }
479
480 /// Constructs a type Idx of size 2^width.
481 /// `width = 64` will be automatically converted to size `0` - the encoding for 2^64.
483 // clang-format off
484 Ref type_bool() { return data_.type_bool; }
485 Ref type_i1() { return data_.type_bool; }
486 Ref type_i2() { return type_int( 2); };
487 Ref type_i4() { return type_int( 4); };
488 Ref type_i8() { return type_int( 8); };
489 Ref type_i16() { return type_int(16); };
490 Ref type_i32() { return type_int(32); };
491 Ref type_i64() { return type_int(64); };
492 // clang-format on
493 ///@}
494
495 /// @name Cope with implicit Arguments
496 ///@{
497
498 /// Places Infer arguments as demanded by Pi::implicit and then apps @p arg.
499 template<bool Normalize = true> Ref implicit_app(Ref callee, Ref arg);
500 template<bool Normalize = true> Ref implicit_app(Ref callee, Defs args) {
501 return implicit_app<Normalize>(callee, tuple(args));
502 }
503 template<bool Normalize = true> Ref implicit_app(Ref callee, nat_t arg) {
504 return implicit_app<Normalize>(callee, lit_nat(arg));
505 }
506 template<bool Normalize = true, class E>
507 Ref implicit_app(Ref callee, E arg) requires std::is_enum_v<E> && std::is_same_v<std::underlying_type_t<E>, nat_t>
508 {
509 return implicit_app<Normalize>(callee, lit_nat((nat_t)arg));
510 }
511
512 /// Complete curried call of annexes obeying implicits.
513 // clang-format off
514 template<class Id, bool Normalize = true, class... Args> const Def* call(Id id, Args&&... args) { return call_<Normalize>(annex(id), std::forward<Args>(args)...); }
515 template<class Id, bool Normalize = true, class... Args> const Def* call( Args&&... args) { return call_<Normalize>(annex<Id>(), std::forward<Args>(args)...); }
516 // clang-format on
517 ///@}
518
519 /// @name Vars & Muts
520 /// Manges sets of Vars and Muts.
521 ///@{
522 [[nodiscard]] auto& vars() { return move_.vars; }
523 [[nodiscard]] auto& muts() { return move_.muts; }
524 [[nodiscard]] const auto& vars() const { return move_.vars; }
525 [[nodiscard]] const auto& muts() const { return move_.muts; }
526 ///@}
527
528 /// @name dump/log
529 ///@{
530 Log& log();
531 void dummy() {}
532 void dump(std::ostream& os); ///< Dump to @p os.
533 void dump(); ///< Dump to `std::cout`.
534 void debug_dump(); ///< Dump in Debug build if World::log::level is Log::Level::Debug.
535 void write(const char* file); ///< Write to a file named @p file.
536 void write(); ///< Same above but file name defaults to World::name.
537 ///@}
538
539 /// @name dot
540 /// GraphViz output.
541 ///@{
542
543 /// Dumps DOT to @p os.
544 /// @param os Output stream
545 /// @param annexes If `true`, include all annexes - even if unused.
546 /// @param types Follow type dependencies?
547 void dot(std::ostream& os, bool annexes = false, bool types = false) const;
548 /// Same as above but write to @p file or `std::cout` if @p file is `nullptr`.
549 void dot(const char* file = nullptr, bool annexes = false, bool types = false) const;
550 ///@}
551
552private:
553 /// @name call_
554 /// Helpers to unwind World::call with variadic templates.
555 ///@{
556 template<bool Normalize = true, class T, class... Args> const Def* call_(Ref callee, T arg, Args&&... args) {
557 return call_<Normalize>(implicit_app(callee, arg), std::forward<Args>(args)...);
558 }
559 template<bool Normalize = true, class T> const Def* call_(Ref callee, T arg) {
560 return implicit_app<Normalize>(callee, arg);
561 }
562 ///@}
563
564 /// @name Put into Sea of Nodes
565 ///@{
566 template<class T, class... Args> const T* unify(size_t num_ops, Args&&... args) {
567 auto state = move_.arena.state();
568 auto def = allocate<T>(num_ops, std::forward<Args&&>(args)...);
569 if (auto loc = get_loc()) def->set(loc);
570 assert(!def->isa_mut());
571#ifdef MIM_ENABLE_CHECKS
572 if (flags().trace_gids) outln("{}: {} - {}", def->node_name(), def->gid(), def->flags());
573 if (flags().reeval_breakpoints && breakpoints().contains(def->gid())) fe::breakpoint();
574#endif
575 if (is_frozen()) {
576 --state_.pod.curr_gid;
577 auto i = move_.defs.find(def);
578 deallocate<T>(state, def);
579 if (i != move_.defs.end()) return static_cast<const T*>(*i);
580 return nullptr;
581 }
582
583 if (auto [i, ins] = move_.defs.emplace(def); !ins) {
584 deallocate<T>(state, def);
585 return static_cast<const T*>(*i);
586 }
587#ifdef MIM_ENABLE_CHECKS
588 if (!flags().reeval_breakpoints && breakpoints().contains(def->gid())) fe::breakpoint();
589#endif
590 return def;
591 }
592
593 template<class T> void deallocate(fe::Arena::State state, const T* ptr) {
594 ptr->~T();
595 move_.arena.deallocate(state);
596 }
597
598 template<class T, class... Args> T* insert(size_t num_ops, Args&&... args) {
599 auto def = allocate<T>(num_ops, std::forward<Args&&>(args)...);
600 if (auto loc = get_loc()) def->set(loc);
601#ifdef MIM_ENABLE_CHECKS
602 if (flags().trace_gids) outln("{}: {} - {}", def->node_name(), def->gid(), def->flags());
603 if (breakpoints().contains(def->gid())) fe::breakpoint();
604#endif
605 assert_emplace(move_.defs, def);
606 return def;
607 }
608
609#if (!defined(_MSC_VER) && defined(NDEBUG))
610 struct Lock {
611 Lock() { assert((guard_ = !guard_) && "you are not allowed to recursively invoke allocate"); }
612 ~Lock() { guard_ = !guard_; }
613 static bool guard_;
614 };
615#else
616 struct Lock {
617 ~Lock() {}
618 };
619#endif
620
621 template<class T, class... Args> T* allocate(size_t num_ops, Args&&... args) {
622 static_assert(sizeof(Def) == sizeof(T),
623 "you are not allowed to introduce any additional data in subclasses of Def");
624 auto lock = Lock();
625 auto num_bytes = sizeof(Def) + sizeof(uintptr_t) * num_ops;
626 auto ptr = move_.arena.allocate(num_bytes, alignof(T));
627 auto res = new (ptr) T(std::forward<Args&&>(args)...);
628 assert(res->num_ops() == num_ops);
629 return res;
630 }
631 ///@}
632
633 Driver* driver_;
634 State state_;
635
636 struct SeaHash {
637 size_t operator()(const Def* def) const { return def->hash(); }
638 };
639
640 struct SeaEq {
641 bool operator()(const Def* d1, const Def* d2) const { return d1->equal(d2); }
642 };
643
644 struct Move {
645 absl::btree_map<flags_t, const Def*> flags2annex;
646 absl::btree_map<Sym, Def*> sym2external;
647 fe::Arena arena;
648 absl::flat_hash_set<const Def*, SeaHash, SeaEq> defs;
649 Pool<const Var*> vars;
650 Pool<Def*> muts;
651 DefDefMap<DefVec> cache;
652
653 friend void swap(Move& m1, Move& m2) noexcept {
654 using std::swap;
655 // clang-format off
656 swap(m1.flags2annex, m2.flags2annex);
657 swap(m1.sym2external, m2.sym2external);
658 swap(m1.arena, m2.arena);
659 swap(m1.defs, m2.defs);
660 swap(m1.vars, m2.vars);
661 swap(m1.muts, m2.muts);
662 swap(m1.cache, m2.cache);
663 // clang-format on
664 }
665 } move_;
666
667 struct {
668 const Univ* univ;
669 const Type* type_0;
670 const Type* type_1;
671 const Bot* type_bot;
672 const Top* type_top;
673 const Def* type_bool;
674 const Top* top_nat;
675 const Sigma* sigma;
676 const Tuple* tuple;
677 const Nat* type_nat;
678 const Idx* type_idx;
679 const Def* table_id;
680 const Def* table_not;
681 const Lit* lit_univ_0;
682 const Lit* lit_univ_1;
683 const Lit* lit_nat_0;
684 const Lit* lit_nat_1;
685 const Lit* lit_nat_max;
686 const Lit* lit_0_1;
687 std::array<const Lit*, 2> lit_bool;
688 u32 curr_run = 0;
689 } data_;
690
691 friend void swap(World& w1, World& w2) noexcept {
692 using std::swap;
693 // clang-format off
694 swap(w1.state_, w2.state_);
695 swap(w1.data_, w2.data_ );
696 swap(w1.move_, w2.move_ );
697 // clang-format on
698
699 swap(w1.data_.univ->world_, w2.data_.univ->world_);
700 assert(&w1.univ()->world() == &w1);
701 assert(&w2.univ()->world() == &w2);
702 }
703
705};
706
707} // namespace mim
A (possibly paramterized) Array.
Definition tuple.h:67
Base class for all Defs.
Definition def.h:212
DefVec reduce(Ref arg) const
Rewrites Def::ops by substituting this mutable's Var with arg.
Definition def.cpp:204
bool is_external() const
Definition def.h:416
Sym sym() const
Definition def.h:453
bool is_closed() const
Has no free_vars()?
Definition def.cpp:363
Some "global" variables needed all over the place.
Definition driver.h:17
A built-in constant of type Nat -> *.
Definition def.h:761
static constexpr nat_t bitwidth2size(nat_t n)
Definition def.h:792
This node is a hole in the IR that is inferred by its context later on.
Definition check.h:10
A function.
Definition lam.h:105
std::variant< bool, Ref > Filter
Definition lam.h:113
Facility to log what you are doing.
Definition log.h:17
A (possibly paramterized) Tuple.
Definition tuple.h:114
A dependent function type.
Definition lam.h:11
static Ref infer(Ref dom, Ref codom)
Definition check.cpp:288
Helper class to retrieve Infer::arg if present.
Definition def.h:86
A dependent tuple type.
Definition tuple.h:9
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
Data constructor for a Sigma.
Definition tuple.h:50
This is a thin wrapper for absl::InlinedVector<T, N, / A> which in turn is a drop-in replacement for ...
Definition vector.h:16
The World represents the whole program and manages creation of MimIR nodes (Defs).
Definition world.h:33
const Lit * lit_idx(nat_t size, u64 val)
Constructs a Lit of type Idx of size size.
Definition world.h:406
const Lit * lit_idx(I val)
Definition world.h:408
const Lam * fun(Ref dom, Ref codom, Lam::Filter f, Ref body)
Definition world.h:299
Meet * mut_meet(Ref type, size_t size)
Definition world.h:450
Lam * mut_lam(Defs dom, Ref codom)
Definition world.h:306
const auto & flags2annex() const
Definition world.h:167
Ref pack(View< u64 > shape, Ref body)
Definition world.h:362
const Pi * cn()
Definition world.h:274
Ref type_i64()
Definition world.h:491
Lam * mut_lam(Ref dom, Ref codom)
Definition world.h:305
u32 next_run()
Definition world.h:90
friend void swap(World &w1, World &w2) noexcept
Definition world.h:691
Ref uniq(Ref inhabitant)
Definition world.cpp:527
Infer * mut_infer_type()
Definition world.h:231
const Lam * lam(Ref dom, Defs codom, Lam::Filter f, Ref body)
Definition world.h:297
Log & log()
Definition world.cpp:72
Ref type_i16()
Definition world.h:489
auto & muts()
Definition world.h:523
Infer * mut_infer(Ref type)
Definition world.h:229
Ref gid2def(u32 gid)
Lookup Def by gid.
Definition world.cpp:557
const Lit * lit_i8()
Definition world.h:400
Ref pack(u64 n, Ref body)
Definition world.h:361
Ref type_i2()
Definition world.h:486
World & operator=(World)=delete
const Lit * lit_i16(u16 val)
Definition world.h:420
const Lit * lit_i1(bool val)
Definition world.h:416
Global * global(Ref type, bool is_mutable=true)
Definition world.h:467
Ref arr(u64 n, Ref body)
Definition world.h:340
const Lit * lit_i32()
Definition world.h:402
Ref type_i1()
Definition world.h:485
Driver & driver()
Definition world.h:81
const Proxy * proxy(Ref type, Defs ops, u32 index, u32 tag)
Definition world.h:225
const Lam * con(Defs dom, Lam::Filter f, Ref body)
Definition world.h:294
Lam * mut_fun(Ref dom, Ref codom)
Definition world.h:309
Ref ext(Ref type)
Definition world.cpp:463
const Driver & driver() const
Definition world.h:80
const Lam * lam(Defs dom, Ref codom, Lam::Filter f, Ref body)
Definition world.h:296
const Axiom * axiom(Ref type)
See above.
Definition world.h:256
const Lit * lit_tt()
Definition world.h:432
World(Driver *)
Definition world.cpp:61
const Lam * fun(Defs dom, Ref codom, Lam::Filter f, Ref body)
Definition world.h:300
const auto & sym2external() const
Definition world.h:190
Lam * mut_con(Ref dom)
Definition world.h:303
void set(std::string_view name)
Definition world.h:85
Ref extract(Ref d, u64 i)
Definition world.h:372
u32 curr_gid() const
Manage global identifier - a unique number for each Def.
Definition world.h:88
World inherit()
Inherits the state into the new World.
Definition world.h:72
Ref implicit_app(Ref callee, nat_t arg)
Definition world.h:503
const Lam * lam(Defs dom, Defs codom, Lam::Filter f, Ref body)
Definition world.h:298
Ref implicit_app(Ref callee, Ref arg)
Places Infer arguments as demanded by Pi::implicit and then apps arg.
Definition world.cpp:163
Ref app(Ref callee, Defs args)
Definition world.h:319
const Pi * fn(Ref dom, Ref codom, bool implicit=false)
Definition world.h:277
const auto & muts() const
Definition world.h:525
Infer * mut_infer_univ()
Definition world.h:230
const Univ * univ()
Definition world.h:211
Ref test(Ref value, Ref probe, Ref match, Ref clash)
Definition world.cpp:513
Ref type_bool()
Definition world.h:484
const Lit * lit_0_1()
Definition world.h:397
const Pi * pi(Defs dom, Ref codom, bool implicit=false)
Definition world.h:263
const Pi * pi(Ref dom, Defs codom, bool implicit=false)
Definition world.h:264
World & verify()
Verifies that all externals() and annexes() are Def::is_closed(), if MIM_ENABLE_CHECKS.
Definition world.cpp:563
const Lam * fun(Defs dom, Defs codom, Lam::Filter f, Ref body)
Definition world.h:302
const Lit * lit_i64()
Definition world.h:403
const Lit * lit_idx_mod(nat_t mod, u64 val)
Constructs a Lit of type Idx of size mod.
Definition world.h:428
const Idx * type_idx()
Definition world.h:474
Ref umax(Defs)
Definition world.cpp:108
Pi * mut_pi(Ref type, bool implicit=false)
Definition world.h:266
const Lit * lit_univ_0()
Definition world.h:391
const Def * annex(Id id)
Lookup annex by Axiom::id.
Definition world.h:171
const Pi * cn(Ref dom, bool implicit=false)
Definition world.h:275
void set_loc(Loc loc={})
Definition world.h:110
Sym name() const
Definition world.h:83
Join * mut_join(Ref type, size_t size)
Definition world.h:449
Ref insert(Ref d, u64 i, Ref val)
Definition world.h:384
const Pi * cn(Defs dom, bool implicit=false)
Definition world.h:276
void dump()
Dump to std::cout.
Definition dump.cpp:486
void make_internal(Def *def)
Definition world.h:201
Arr * mut_arr(Ref type)
Definition world.h:336
const Lit * lit_univ_1()
Definition world.h:392
void write()
Same above but file name defaults to World::name.
Definition dump.cpp:497
Ref bot(Ref type)
Definition world.h:440
Ref implicit_app(Ref callee, E arg)
Definition world.h:507
const Def * register_annex(plugin_t p, tag_t t, sub_t s, const Def *def)
Definition world.h:183
Ref insert(Ref d, Ref i, Ref val)
Definition world.cpp:346
const Lit * lit_i1()
Definition world.h:399
const Nat * type_nat()
Definition world.h:473
Sigma * mut_sigma(Ref type, size_t size)
Definition world.h:327
Ref var(Ref type, Def *mut)
Definition world.cpp:154
Ref arr(Ref shape, Ref body)
Definition world.cpp:390
const Pi * fn(Ref dom, Defs codom, bool implicit=false)
Definition world.h:279
Lam * mut_lam(Ref dom, Defs codom)
Definition world.h:307
Ref meet(Defs ops)
Definition world.h:454
Flags & flags()
Retrieve compile Flags.
Definition world.cpp:73
ScopedLoc push(Loc loc)
Definition world.h:111
void debug_dump()
Dump in Debug build if World::log::level is Log::Level::Debug.
Definition dump.cpp:488
u32 next_gid()
Definition world.h:89
Lam * mut_fun(Ref dom, Defs codom)
Definition world.h:311
Ref type_idx(Ref size)
Definition world.h:476
const Def * call(Args &&... args)
Definition world.h:515
const auto & breakpoints()
Definition world.h:154
const Type * type()
Definition world.h:216
void set(Sym name)
Definition world.h:84
Ref type_int(nat_t width)
Constructs a type Idx of size 2^width.
Definition world.h:482
Lam * mut_fun(Defs dom, Defs codom)
Definition world.h:312
const Lit * lit_i2(u8 val)
Definition world.h:417
bool is_frozen() const
Definition world.h:130
Loc get_loc() const
Definition world.h:109
auto externals() const
Definition world.h:192
const Lit * lit_nat_0()
Definition world.h:394
Ref ac(Ref type, Defs ops)
Definition world.cpp:494
Sym sym(std::string_view)
Definition world.cpp:76
const Pi * pi(Ref dom, Ref codom, bool implicit=false)
Definition world.h:262
Infer * mut_infer_entity()
Either a value ?:?:Type ? or a type ?:Type ?:Type ?.
Definition world.h:234
const Lit * lit_i16()
Definition world.h:401
const Lit * lit_ff()
Definition world.h:431
const Lit * lit_nat_max()
Definition world.h:396
Ref raw_app(const Axiom *axiom, u8 curry, u8 trip, Ref type, Ref callee, Ref arg)
Definition world.cpp:219
Def * external(Sym name)
Lookup by name.
Definition world.h:191
Ref select(Ref cond, Ref t, Ref f)
Builds (f, t)#cond.
Definition world.h:376
Ref type_idx(nat_t size)
Definition world.h:478
TBound< Up > * mut_bound(Ref type, size_t size)
Definition world.h:445
Sym append_suffix(Sym name, std::string suffix)
Appends a suffix or an increasing number if the suffix already exists.
Definition world.cpp:529
Ref type_i32()
Definition world.h:490
Join * mut_join(size_t size)
Definition world.h:451
Ref arr_unsafe(Ref body)
Definition world.h:344
const Lam * fun(Ref dom, Defs codom, Lam::Filter f, Ref body)
Definition world.h:301
const Lit * lit_i32(u32 val)
Definition world.h:421
const Lit * lit_i8(u8 val)
Definition world.h:419
Ref pack(Ref arity, Ref body)
Definition world.cpp:417
Ref arr(View< u64 > shape, Ref body)
Definition world.h:341
Ref insert(Ref d, u64 a, u64 i, Ref val)
Definition world.h:383
Lam * mut_lam(Defs dom, Defs codom)
Definition world.h:308
Sigma * mut_sigma(size_t size)
A *mut*able Sigma of type level.
Definition world.h:329
const Lit * lit_univ(u64 level)
Definition world.h:390
Ref pick(Ref type, Ref value)
Definition world.cpp:511
const Pi * pi(Defs dom, Defs codom, bool implicit=false)
Definition world.h:265
Ref bound(Defs ops)
Definition world.cpp:470
const Tuple * tuple()
the unit value of type []
Definition world.h:352
const Type * type_infer_univ()
Definition world.h:215
const Def * call(Id id, Args &&... args)
Complete curried call of annexes obeying implicits.
Definition world.h:514
void make_external(Def *def)
Definition world.h:195
void dummy()
Definition world.h:531
Ref type_i8()
Definition world.h:488
Ref extract(Ref d, Ref i)
Definition world.cpp:284
Lam * mut_fun(Defs dom, Ref codom)
Definition world.h:310
Vector< Def * > copy_externals() const
Definition world.h:193
Ref app(Ref callee, Ref arg)
Definition world.cpp:168
Ref type_top()
Definition world.h:443
const Lit * lit_i64(u64 val)
Definition world.h:422
Ref filter(Lam::Filter filter)
Definition world.h:286
const Lit * lit(Ref type, u64 val)
Definition world.cpp:447
Ref vel(Ref type, Ref value)
Definition world.cpp:506
const Sigma * sigma()
The unit type within Type 0.
Definition world.h:331
const Lit * lit_nat(nat_t a)
Definition world.h:393
const State & state() const
Definition world.h:78
Ref implicit_app(Ref callee, Defs args)
Definition world.h:500
Ref top_nat()
Definition world.h:444
const auto & vars() const
Definition world.h:524
Ref extract(Ref d, u64 a, u64 i)
Definition world.h:371
TBound< Up > * mut_bound(size_t size)
A *mut*able Bound of Type level.
Definition world.h:447
const Axiom * axiom(NormalizeFn n, u8 curry, u8 trip, Ref type, plugin_t p, tag_t t, sub_t s)
Definition world.h:244
Ref raw_app(Ref type, Ref callee, Defs args)
Definition world.h:322
const Def * register_annex(flags_t f, const Def *)
Definition world.cpp:79
Ref join(Defs ops)
Definition world.h:453
Ref type_i4()
Definition world.h:487
const Pi * fn(Defs dom, Ref codom, bool implicit=false)
Definition world.h:278
Arr * mut_arr()
Definition world.h:337
const Axiom * axiom(NormalizeFn n, u8 curry, u8 trip, Ref type)
Builds a fresh Axiom with descending Axiom::sub.
Definition world.h:253
auto & vars()
Definition world.h:522
const Lit * lit_int(nat_t width, u64 val)
Constructs a Lit of type Idx of size 2^width.
Definition world.h:415
const Lit * lit_bool(bool val)
Definition world.h:430
void breakpoint(u32 gid)
Trigger breakpoint in your debugger when creating Def with Def::gid gid.
Definition world.cpp:555
const Lam * lam(Ref dom, Ref codom, Lam::Filter f, Ref body)
Definition world.h:295
Ref uinc(Ref op, level_t offset=1)
Definition world.cpp:99
Meet * mut_meet(size_t size)
Definition world.h:452
Lam * mut_con(Defs dom)
Definition world.h:304
auto annexes() const
Definition world.h:168
const Axiom * axiom(Ref type, plugin_t p, tag_t t, sub_t s)
Definition world.h:247
World(World &&other) noexcept
Definition world.h:68
const Lit * lit_nat_1()
Definition world.h:395
bool freeze(bool on=true) const
Yields old frozen state.
Definition world.h:133
Pack * mut_pack(Ref type)
Definition world.h:358
const Lit * lit_i4(u8 val)
Definition world.h:418
Ref top(Ref type)
Definition world.h:441
void dot(std::ostream &os, bool annexes=false, bool types=false) const
Dumps DOT to os.
Definition dot.cpp:146
const Lam * lam(const Pi *pi, Lam::Filter f, Ref body)
Definition world.h:290
const Lam * con(Ref dom, Lam::Filter f, Ref body)
Definition world.h:293
const Pi * fn(Defs dom, Defs codom, bool implicit=false)
Definition world.h:280
Ref type_bot()
Definition world.h:442
Lam * mut_lam(const Pi *pi)
Definition world.h:291
const Def * annex()
Get Axiom from a plugin.
Definition world.h:180
@ Sigma
Definition def.h:40
@ Tuple
Definition def.h:40
@ Nat
Definition def.h:40
@ Idx
Definition def.h:40
@ Lit
Definition def.h:40
Definition ast.h:14
u64 nat_t
Definition types.h:43
Vector< const Def * > DefVec
Definition def.h:62
absl::flat_hash_map< DefDef, To, DefDefHash, DefDefEq > DefDefMap
Definition def.h:614
u8 sub_t
Definition types.h:48
auto assert_emplace(C &container, Args &&... args)
Invokes emplace on container, asserts that insertion actually happened, and returns the iterator.
Definition util.h:104
u64 flags_t
Definition types.h:45
auto lookup(const C &container, const K &key)
Yields pointer to element (or the element itself if it is already a pointer), if found and nullptr ot...
Definition util.h:95
auto match(Ref def)
Definition axiom.h:112
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:178
std::ostream & outln(const char *fmt, Args &&... args)
Definition print.h:189
u64 plugin_t
Definition types.h:46
uint32_t u32
Definition types.h:34
TExt< false > Bot
Definition lattice.h:177
uint64_t u64
Definition types.h:34
u8 tag_t
Definition types.h:47
uint8_t u8
Definition types.h:34
Ref(*)(Ref, Ref, Ref) NormalizeFn
Definition def.h:105
uint16_t u16
Definition types.h:34
Compiler switches that must be saved and looked up in later phases of compilation.
Definition flags.h:11
constexpr decltype(auto) get(mim::Span< T, N > span)
Definition span.h:113
static constexpr plugin_t Global_Plugin
Definition plugin.h:58
static Sym demangle(Driver &, plugin_t plugin)
Reverts an Axiom::mangled string to a Sym.
Definition plugin.cpp:37
static constexpr flags_t Base
Definition plugin.h:118
Use to World::freeze and automatically unfreeze at the end of scope.
Definition world.h:140
Freezer(const World &world)
Definition world.h:141
const World & world
Definition world.h:146
ScopedLoc(World &world, Loc old_loc)
Definition world.h:99
friend void swap(State &s1, State &s2) noexcept
Definition world.h:52
struct mim::World::State::POD pod
absl::flat_hash_set< uint32_t > breakpoints
Definition world.h:50
Plain Old Data
Definition world.h:41