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/axm.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)) {}
144 ~Freezer() { world.freeze(old); }
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 const Def* 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 Axm::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("Axm with ID '{x}' not found; demangled plugin name is '{}'", flags, Annex::demangle(driver(), flags));
175 }
176
177 /// Get Axm from a plugin.
178 /// Can be used to get an Axm without sub-tags.
179 /// E.g. use `w.annex<mem::M>();` to get the `%mem.M` Axm.
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 void make_external(Def*);
195 void make_internal(Def*);
196 ///@}
197
198 /// @name Univ, Type, Var, Proxy, Hole
199 ///@{
200 const Univ* univ() { return data_.univ; }
201 const Def* uinc(const Def* op, level_t offset = 1);
202 template<Sort = Sort::Univ> const Def* umax(Defs);
203 const Type* type(const Def* level);
204 const Type* type_infer_univ() { return type(mut_hole_univ()); }
205 template<level_t level = 0> const Type* type() {
206 if constexpr (level == 0)
207 return data_.type_0;
208 else if constexpr (level == 1)
209 return data_.type_1;
210 else
211 return type(lit_univ(level));
212 }
213 const Def* var(const Def* type, Def* mut);
214 const Proxy* proxy(const Def* type, Defs ops, u32 index, u32 tag) {
215 return unify<Proxy>(ops.size(), type, ops, index, tag);
216 }
217
218 Hole* mut_hole(const Def* type) { return insert<Hole>(1, type); }
219 Hole* mut_hole_univ() { return mut_hole(univ()); }
221
222 /// Either a value `?:?:Type ?` or a type `?:Type ?:Type ?`.
224 auto t = type_infer_univ();
225 auto res = mut_hole(mut_hole(t));
226 assert(this == &res->world());
227 return res;
228 }
229 ///@}
230
231 /// @name Axm
232 ///@{
233 const Axm* axm(NormalizeFn n, u8 curry, u8 trip, const Def* type, plugin_t p, tag_t t, sub_t s) {
234 return unify<Axm>(0, n, curry, trip, type, p, t, s);
235 }
236 const Axm* axm(const Def* type, plugin_t p, tag_t t, sub_t s) { return axm(nullptr, 0, 0, type, p, t, s); }
237
238 /// Builds a fresh Axm with descending Axm::sub.
239 /// This is useful during testing to come up with some entity of a specific type.
240 /// It uses the plugin Axm::Global_Plugin and starts with `0` for Axm::sub and counts up from there.
241 /// The Axm::tag is set to `0` and the Axm::normalizer to `nullptr`.
242 const Axm* axm(NormalizeFn n, u8 curry, u8 trip, const Def* type) {
243 return axm(n, curry, trip, type, Annex::Global_Plugin, 0, state_.pod.curr_sub++);
244 }
245 const Axm* axm(const Def* type) { return axm(nullptr, 0, 0, type); } ///< See above.
246 ///@}
247
248 /// @name Pi
249 ///@{
250 // clang-format off
251 const Pi* pi(const Def* dom, const Def* codom, bool implicit = false) { return unify<Pi>(2, Pi::infer(dom, codom), dom, codom, implicit); }
252 const Pi* pi(Defs dom, const Def* codom, bool implicit = false) { return pi(sigma(dom), codom, implicit); }
253 const Pi* pi(const Def* dom, Defs codom, bool implicit = false) { return pi(dom, sigma(codom), implicit); }
254 const Pi* pi(Defs dom, Defs codom, bool implicit = false) { return pi(sigma(dom), sigma(codom), implicit); }
255 Pi* mut_pi(const Def* type, bool implicit = false) { return insert<Pi>(2, type, implicit); }
256 // clang-format on
257 ///@}
258
259 /// @name Cn
260 /// Pi with codom mim::Bot%tom
261 ///@{
262 // clang-format off
263 const Pi* cn( ) { return cn(sigma( ), false); }
264 const Pi* cn(const Def* dom, bool implicit = false) { return pi( dom , type_bot(), implicit); }
265 const Pi* cn(Defs dom, bool implicit = false) { return cn(sigma(dom), implicit); }
266 const Pi* fn(const Def* dom, const Def* codom, bool implicit = false) { return cn({ dom , cn(codom)}, implicit); }
267 const Pi* fn(Defs dom, const Def* codom, bool implicit = false) { return fn(sigma(dom), codom, implicit); }
268 const Pi* fn(const Def* dom, Defs codom, bool implicit = false) { return fn( dom , sigma(codom), implicit); }
269 const Pi* fn(Defs dom, Defs codom, bool implicit = false) { return fn(sigma(dom), sigma(codom), implicit); }
270 // clang-format on
271 ///@}
272
273 /// @name Lam
274 ///@{
276 if (auto b = std::get_if<bool>(&filter)) return lit_bool(*b);
277 return std::get<const Def*>(filter);
278 }
279 const Lam* lam(const Pi* pi, Lam::Filter f, const Def* body) { return unify<Lam>(2, pi, filter(f), body); }
280 Lam* mut_lam(const Pi* pi) { return insert<Lam>(2, pi); }
281 // clang-format off
282 const Lam* con(const Def* dom, Lam::Filter f, const Def* body) { return unify<Lam>(2, cn(dom ), filter(f), body); }
283 const Lam* con(Defs dom, Lam::Filter f, const Def* body) { return unify<Lam>(2, cn(dom ), filter(f), body); }
284 const Lam* lam(const Def* dom, const Def* codom, Lam::Filter f, const Def* body) { return unify<Lam>(2, pi(dom, codom), filter(f), body); }
285 const Lam* lam(Defs dom, const Def* codom, Lam::Filter f, const Def* body) { return unify<Lam>(2, pi(dom, codom), filter(f), body); }
286 const Lam* lam(const Def* dom, Defs codom, Lam::Filter f, const Def* body) { return unify<Lam>(2, pi(dom, codom), filter(f), body); }
287 const Lam* lam(Defs dom, Defs codom, Lam::Filter f, const Def* body) { return unify<Lam>(2, pi(dom, codom), filter(f), body); }
288 const Lam* fun(const Def* dom, const Def* codom, Lam::Filter f, const Def* body) { return unify<Lam>(2, fn(dom, codom), filter(f), body); }
289 const Lam* fun(Defs dom, const Def* codom, Lam::Filter f, const Def* body) { return unify<Lam>(2, fn(dom, codom), filter(f), body); }
290 const Lam* fun(const Def* dom, Defs codom, Lam::Filter f, const Def* body) { return unify<Lam>(2, fn(dom, codom), filter(f), body); }
291 const Lam* fun(Defs dom, Defs codom, Lam::Filter f, const Def* body) { return unify<Lam>(2, fn(dom, codom), filter(f), body); }
292 Lam* mut_con(const Def* dom ) { return insert<Lam>(2, cn(dom )); }
293 Lam* mut_con(Defs dom ) { return insert<Lam>(2, cn(dom )); }
294 Lam* mut_lam(const Def* dom, const Def* codom) { return insert<Lam>(2, pi(dom, codom)); }
295 Lam* mut_lam(Defs dom, const Def* codom) { return insert<Lam>(2, pi(dom, codom)); }
296 Lam* mut_lam(const Def* dom, Defs codom) { return insert<Lam>(2, pi(dom, codom)); }
297 Lam* mut_lam(Defs dom, Defs codom) { return insert<Lam>(2, pi(dom, codom)); }
298 Lam* mut_fun(const Def* dom, const Def* codom) { return insert<Lam>(2, fn(dom, codom)); }
299 Lam* mut_fun(Defs dom, const Def* codom) { return insert<Lam>(2, fn(dom, codom)); }
300 Lam* mut_fun(const Def* dom, Defs codom) { return insert<Lam>(2, fn(dom, codom)); }
301 Lam* mut_fun(Defs dom, Defs codom) { return insert<Lam>(2, fn(dom, codom)); }
302 // clang-format on
303 ///@}
304
305 /// @name App
306 ///@{
307 template<bool Normalize = true> const Def* app(const Def* callee, const Def* arg);
308 template<bool Normalize = true> const Def* app(const Def* callee, Defs args) {
309 return app<Normalize>(callee, tuple(args));
310 }
311 const Def* raw_app(const Axm* axm, u8 curry, u8 trip, const Def* type, const Def* callee, const Def* arg);
312 const Def* raw_app(const Def* type, const Def* callee, const Def* arg);
313 const Def* raw_app(const Def* type, const Def* callee, Defs args) { return raw_app(type, callee, tuple(args)); }
314 ///@}
315
316 /// @name Sigma
317 ///@{
318 Sigma* mut_sigma(const Def* type, size_t size) { return insert<Sigma>(size, type, size); }
319 /// A *mutable* Sigma of type @p level.
320 template<level_t level = 0> Sigma* mut_sigma(size_t size) { return mut_sigma(type<level>(), size); }
321 const Def* sigma(Defs ops);
322 const Sigma* sigma() { return data_.sigma; } ///< The unit type within Type 0.
323 ///@}
324
325 /// @name Arr
326 ///@{
327 Arr* mut_arr(const Def* type) { return insert<Arr>(2, type); }
328 template<level_t level = 0> Arr* mut_arr() { return mut_arr(type<level>()); }
329 const Def* arr(const Def* shape, const Def* body);
330 const Def* arr(Defs shape, const Def* body);
331 const Def* arr(u64 n, const Def* body) { return arr(lit_nat(n), body); }
332 const Def* arr(View<u64> shape, const Def* body) {
333 return arr(DefVec(shape.size(), [&](size_t i) { return lit_nat(shape[i]); }), body);
334 }
335 const Def* arr_unsafe(const Def* body) { return arr(top_nat(), body); }
336 ///@}
337
338 /// @name Tuple
339 ///@{
340 const Def* tuple(Defs ops);
341 /// Ascribes @p type to this tuple - needed for dependently typed and mutable Sigma%s.
342 const Def* tuple(const Def* type, Defs ops);
343 const Tuple* tuple() { return data_.tuple; } ///< the unit value of type `[]`
344 const Def* tuple(Sym sym); ///< Converts @p sym to a tuple of type '«n; I8»'.
345 ///@}
346
347 /// @name Pack
348 ///@{
349 Pack* mut_pack(const Def* type) { return insert<Pack>(1, type); }
350 const Def* pack(const Def* arity, const Def* body);
351 const Def* pack(Defs shape, const Def* body);
352 const Def* pack(u64 n, const Def* body) { return pack(lit_nat(n), body); }
353 const Def* pack(View<u64> shape, const Def* body) {
354 return pack(DefVec(shape.size(), [&](auto i) { return lit_nat(shape[i]); }), body);
355 }
356 ///@}
357
358 /// @name Extract
359 /// @see core::extract_unsafe
360 ///@{
361 const Def* extract(const Def* d, const Def* i);
362 const Def* extract(const Def* d, u64 a, u64 i) { return extract(d, lit_idx(a, i)); }
363 const Def* extract(const Def* d, u64 i) { return extract(d, d->as_lit_arity(), i); }
364
365 /// Builds `(f, t)#cond`.
366 /// @note Expects @p cond as first, @p t as second, and @p f as third argument.
367 const Def* select(const Def* cond, const Def* t, const Def* f) { return extract(tuple({f, t}), cond); }
368 ///@}
369
370 /// @name Insert
371 /// @see core::insert_unsafe
372 ///@{
373 const Def* insert(const Def* d, const Def* i, const Def* val);
374 const Def* insert(const Def* d, u64 a, u64 i, const Def* val) { return insert(d, lit_idx(a, i), val); }
375 const Def* insert(const Def* d, u64 i, const Def* val) { return insert(d, d->as_lit_arity(), i, val); }
376 ///@}
377
378 /// @name Lit
379 ///@{
380 const Lit* lit(const Def* type, u64 val);
381 const Lit* lit_univ(u64 level) { return lit(univ(), level); }
382 const Lit* lit_univ_0() { return data_.lit_univ_0; }
383 const Lit* lit_univ_1() { return data_.lit_univ_1; }
384 const Lit* lit_nat(nat_t a) { return lit(type_nat(), a); }
385 const Lit* lit_nat_0() { return data_.lit_nat_0; }
386 const Lit* lit_nat_1() { return data_.lit_nat_1; }
387 const Lit* lit_nat_max() { return data_.lit_nat_max; }
388 const Lit* lit_0_1() { return data_.lit_0_1; }
389 // clang-format off
390 const Lit* lit_i1() { return lit_nat(Idx::bitwidth2size( 1)); };
391 const Lit* lit_i8() { return lit_nat(Idx::bitwidth2size( 8)); };
392 const Lit* lit_i16() { return lit_nat(Idx::bitwidth2size(16)); };
393 const Lit* lit_i32() { return lit_nat(Idx::bitwidth2size(32)); };
394 const Lit* lit_i64() { return lit_nat(Idx::bitwidth2size(64)); };
395 /// Constructs a Lit of type Idx of size @p size.
396 /// @note `size = 0` means `2^64`.
397 const Lit* lit_idx(nat_t size, u64 val) { return lit(type_idx(size), val); }
398
399 template<class I> const Lit* lit_idx(I val) {
400 static_assert(std::is_integral<I>());
401 return lit_idx(Idx::bitwidth2size(sizeof(I) * 8), val);
402 }
403
404 /// Constructs a Lit @p of type Idx of size 2^width.
405 /// `val = 64` will be automatically converted to size `0` - the encoding for 2^64.
406 const Lit* lit_int(nat_t width, u64 val) { return lit_idx(Idx::bitwidth2size(width), val); }
407 const Lit* lit_i1 (bool val) { return lit_int( 1, u64(val)); }
408 const Lit* lit_i2 (u8 val) { return lit_int( 2, u64(val)); }
409 const Lit* lit_i4 (u8 val) { return lit_int( 4, u64(val)); }
410 const Lit* lit_i8 (u8 val) { return lit_int( 8, u64(val)); }
411 const Lit* lit_i16(u16 val) { return lit_int(16, u64(val)); }
412 const Lit* lit_i32(u32 val) { return lit_int(32, u64(val)); }
413 const Lit* lit_i64(u64 val) { return lit_int(64, u64(val)); }
414 // clang-format on
415
416 /// Constructs a Lit of type Idx of size @p mod.
417 /// The value @p val will be adjusted modulo @p mod.
418 /// @note `mod == 0` is the special case for 2^64 and no modulo will be performed on @p val.
419 const Lit* lit_idx_mod(nat_t mod, u64 val) { return lit_idx(mod, mod == 0 ? val : (val % mod)); }
420
421 const Lit* lit_bool(bool val) { return data_.lit_bool[size_t(val)]; }
422 const Lit* lit_ff() { return data_.lit_bool[0]; }
423 const Lit* lit_tt() { return data_.lit_bool[1]; }
424 ///@}
425
426 /// @name Lattice
427 ///@{
428 template<bool Up> const Def* ext(const Def* type);
429 const Def* bot(const Def* type) { return ext<false>(type); }
430 const Def* top(const Def* type) { return ext<true>(type); }
431 const Def* type_bot() { return data_.type_bot; }
432 const Def* type_top() { return data_.type_top; }
433 const Def* top_nat() { return data_.top_nat; }
434 template<bool Up> const Def* bound(Defs ops);
435 const Def* join(Defs ops) { return bound<true>(ops); }
436 const Def* meet(Defs ops) { return bound<false>(ops); }
437 const Def* merge(const Def* type, Defs ops);
438 const Def* merge(Defs ops); ///< Infers the type using a Meet.
439 const Def* inj(const Def* type, const Def* value);
440 const Def* split(const Def* type, const Def* value);
441 const Def* match(Defs);
442 const Def* uniq(const Def* inhabitant);
443 ///@}
444
445 /// @name Globals
446 /// @deprecated Will be removed.
447 ///@{
448 Global* global(const Def* type, bool is_mutable = true) { return insert<Global>(1, type, is_mutable); }
449 ///@}
450
451 /// @name Types
452 ///@{
453 const Nat* type_nat() { return data_.type_nat; }
454 const Idx* type_idx() { return data_.type_idx; }
455 /// @note `size = 0` means `2^64`.
456 const Def* type_idx(const Def* size) { return app(type_idx(), size); }
457 /// @note `size = 0` means `2^64`.
458 const Def* type_idx(nat_t size) { return type_idx(lit_nat(size)); }
459
460 /// Constructs a type Idx of size 2^width.
461 /// `width = 64` will be automatically converted to size `0` - the encoding for 2^64.
462 const Def* type_int(nat_t width) { return type_idx(lit_nat(Idx::bitwidth2size(width))); }
463 // clang-format off
464 const Def* type_bool() { return data_.type_bool; }
465 const Def* type_i1() { return data_.type_bool; }
466 const Def* type_i2() { return type_int( 2); };
467 const Def* type_i4() { return type_int( 4); };
468 const Def* type_i8() { return type_int( 8); };
469 const Def* type_i16() { return type_int(16); };
470 const Def* type_i32() { return type_int(32); };
471 const Def* type_i64() { return type_int(64); };
472 // clang-format on
473 ///@}
474
475 /// @name Cope with implicit Arguments
476 ///@{
477
478 /// Places Hole%s as demanded by Pi::is_implicit() and then apps @p arg.
479 template<bool Normalize = true> const Def* implicit_app(const Def* callee, const Def* arg);
480 template<bool Normalize = true> const Def* implicit_app(const Def* callee, Defs args) {
481 return implicit_app<Normalize>(callee, tuple(args));
482 }
483 template<bool Normalize = true> const Def* implicit_app(const Def* callee, nat_t arg) {
484 return implicit_app<Normalize>(callee, lit_nat(arg));
485 }
486 template<bool Normalize = true, class E>
487 const Def* implicit_app(const Def* callee, E arg)
488 requires std::is_enum_v<E> && std::is_same_v<std::underlying_type_t<E>, nat_t>
489 {
490 return implicit_app<Normalize>(callee, lit_nat((nat_t)arg));
491 }
492
493 /// Complete curried call of annexes obeying implicits.
494 // clang-format off
495 template<class Id, bool Normalize = true, class... Args> const Def* call(Id id, Args&&... args) { return call_<Normalize>(annex(id), std::forward<Args>(args)...); }
496 template<class Id, bool Normalize = true, class... Args> const Def* call( Args&&... args) { return call_<Normalize>(annex<Id>(), std::forward<Args>(args)...); }
497 // clang-format on
498 ///@}
499
500 /// @name Vars & Muts
501 /// Manges sets of Vars and Muts.
502 ///@{
503 [[nodiscard]] auto& vars() { return move_.vars; }
504 [[nodiscard]] auto& muts() { return move_.muts; }
505 [[nodiscard]] const auto& vars() const { return move_.vars; }
506 [[nodiscard]] const auto& muts() const { return move_.muts; }
507
508 /// Yields the new body of `[mut->var() -> arg]mut`.
509 /// The new body may have fewer elements as `mut->num_ops()` addording to Def::reduction_offset.
510 /// E.g. a Pi has a Pi::reduction_offset of 1, and only Pi::dom will be reduced - *not* Pi::codom.
511 Defs reduce(const Var* var, const Def* arg);
512 ///@}
513
514 /// @name dump/log
515 ///@{
516 Log& log();
517 void dummy() {}
518 void dump(std::ostream& os); ///< Dump to @p os.
519 void dump(); ///< Dump to `std::cout`.
520 void debug_dump(); ///< Dump in Debug build if World::log::level is Log::Level::Debug.
521 void write(const char* file); ///< Write to a file named @p file.
522 void write(); ///< Same above but file name defaults to World::name.
523 ///@}
524
525 /// @name dot
526 /// GraphViz output.
527 ///@{
528
529 /// Dumps DOT to @p os.
530 /// @param os Output stream
531 /// @param annexes If `true`, include all annexes - even if unused.
532 /// @param types Follow type dependencies?
533 void dot(std::ostream& os, bool annexes = false, bool types = false) const;
534 /// Same as above but write to @p file or `std::cout` if @p file is `nullptr`.
535 void dot(const char* file = nullptr, bool annexes = false, bool types = false) const;
536 ///@}
537
538private:
539 /// @name call_
540 /// Helpers to unwind World::call with variadic templates.
541 ///@{
542 template<bool Normalize = true, class T, class... Args> const Def* call_(const Def* callee, T arg, Args&&... args) {
543 return call_<Normalize>(implicit_app(callee, arg), std::forward<Args>(args)...);
544 }
545 template<bool Normalize = true, class T> const Def* call_(const Def* callee, T arg) {
546 return implicit_app<Normalize>(callee, arg);
547 }
548 ///@}
549
550 /// @name Put into Sea of Nodes
551 ///@{
552 template<class T, class... Args> const T* unify(size_t num_ops, Args&&... args) {
553 auto state = move_.arena.defs.state();
554 auto def = allocate<T>(num_ops, std::forward<Args&&>(args)...);
555 if (auto loc = get_loc()) def->set(loc);
556 assert(!def->isa_mut());
557#ifdef MIM_ENABLE_CHECKS
558 if (flags().trace_gids) outln("{}: {} - {}", def->node_name(), def->gid(), def->flags());
559 if (flags().reeval_breakpoints && breakpoints().contains(def->gid())) fe::breakpoint();
560#endif
561 if (is_frozen()) {
562 auto i = move_.defs.find(def);
563 deallocate<T>(state, def);
564 if (i != move_.defs.end()) return static_cast<const T*>(*i);
565 return nullptr;
566 }
567
568 if (auto [i, ins] = move_.defs.emplace(def); !ins) {
569 deallocate<T>(state, def);
570 return static_cast<const T*>(*i);
571 }
572#ifdef MIM_ENABLE_CHECKS
573 if (!flags().reeval_breakpoints && breakpoints().contains(def->gid())) fe::breakpoint();
574#endif
575 return def;
576 }
577
578 template<class T> void deallocate(fe::Arena::State state, const T* ptr) {
579 --state_.pod.curr_gid;
580 ptr->~T();
581 move_.arena.defs.deallocate(state);
582 }
583
584 template<class T, class... Args> T* insert(size_t num_ops, Args&&... args) {
585 auto def = allocate<T>(num_ops, std::forward<Args&&>(args)...);
586 if (auto loc = get_loc()) def->set(loc);
587#ifdef MIM_ENABLE_CHECKS
588 if (flags().trace_gids) outln("{}: {} - {}", def->node_name(), def->gid(), def->flags());
589 if (breakpoints().contains(def->gid())) fe::breakpoint();
590#endif
591 assert_emplace(move_.defs, def);
592 return def;
593 }
594
595#if (!defined(_MSC_VER) && defined(NDEBUG))
596 struct Lock {
597 Lock() { assert((guard_ = !guard_) && "you are not allowed to recursively invoke allocate"); }
598 ~Lock() { guard_ = !guard_; }
599 static bool guard_;
600 };
601#else
602 struct Lock {
603 ~Lock() {}
604 };
605#endif
606
607 template<class T, class... Args> T* allocate(size_t num_ops, Args&&... args) {
608 static_assert(sizeof(Def) == sizeof(T),
609 "you are not allowed to introduce any additional data in subclasses of Def");
610 auto lock = Lock();
611 auto num_bytes = sizeof(Def) + sizeof(uintptr_t) * num_ops;
612 auto ptr = move_.arena.defs.allocate(num_bytes, alignof(T));
613 auto res = new (ptr) T(std::forward<Args&&>(args)...);
614 assert(res->num_ops() == num_ops);
615 return res;
616 }
617 ///@}
618
619 Driver* driver_;
620 State state_;
621
622 struct SeaHash {
623 size_t operator()(const Def* def) const { return def->hash(); }
624 };
625
626 struct SeaEq {
627 bool operator()(const Def* d1, const Def* d2) const { return d1->equal(d2); }
628 };
629
630 class Reduct {
631 public:
632 constexpr Reduct(size_t size) noexcept
633 : size_(size) {}
634
635 template<size_t N = std::dynamic_extent> constexpr auto defs() const noexcept {
636 return View<const Def*, N>{defs_, size_};
637 }
638
639 private:
640 size_t size_;
641 const Def* defs_[];
642
643 friend class World;
644 };
645
646 struct Move {
647 struct {
648 fe::Arena defs, substs;
649 } arena;
650
651 absl::btree_map<flags_t, const Def*> flags2annex;
652 absl::btree_map<Sym, Def*> sym2external;
653 absl::flat_hash_set<const Def*, SeaHash, SeaEq> defs;
656 absl::flat_hash_map<std::pair<const Var*, const Def*>, const Reduct*> substs;
657
658 friend void swap(Move& m1, Move& m2) noexcept {
659 using std::swap;
660 // clang-format off
661 swap(m1.arena.defs, m2.arena.defs);
662 swap(m1.arena.substs, m2.arena.substs);
663 swap(m1.defs, m2.defs);
664 swap(m1.substs, m2.substs);
665 swap(m1.vars, m2.vars);
666 swap(m1.muts, m2.muts);
667 swap(m1.flags2annex, m2.flags2annex);
668 swap(m1.sym2external, m2.sym2external);
669 // clang-format on
670 }
671 } move_;
672
673 struct {
674 const Univ* univ;
675 const Type* type_0;
676 const Type* type_1;
677 const Bot* type_bot;
678 const Top* type_top;
679 const Def* type_bool;
680 const Top* top_nat;
681 const Sigma* sigma;
682 const Tuple* tuple;
683 const Nat* type_nat;
684 const Idx* type_idx;
685 const Def* table_id;
686 const Def* table_not;
687 const Lit* lit_univ_0;
688 const Lit* lit_univ_1;
689 const Lit* lit_nat_0;
690 const Lit* lit_nat_1;
691 const Lit* lit_nat_max;
692 const Lit* lit_0_1;
693 std::array<const Lit*, 2> lit_bool;
694 u32 curr_run = 0;
695 } data_;
696
697 friend void swap(World& w1, World& w2) noexcept {
698 using std::swap;
699 // clang-format off
700 swap(w1.state_, w2.state_);
701 swap(w1.data_, w2.data_ );
702 swap(w1.move_, w2.move_ );
703 // clang-format on
704
705 swap(w1.data_.univ->world_, w2.data_.univ->world_);
706 assert(&w1.univ()->world() == &w1);
707 assert(&w2.univ()->world() == &w2);
708 }
709};
710
711} // namespace mim
A (possibly paramterized) Array.
Definition tuple.h:74
Definition axm.h:9
Base class for all Defs.
Definition def.h:197
Some "global" variables needed all over the place.
Definition driver.h:17
This node is a hole in the IR that is inferred by its context later on.
Definition check.h:10
A built-in constant of type Nat -> *.
Definition def.h:742
static constexpr nat_t bitwidth2size(nat_t n)
Definition def.h:773
A function.
Definition lam.h:106
std::variant< bool, const Def * > Filter
Definition lam.h:114
Facility to log what you are doing.
Definition log.h:17
A (possibly paramterized) Tuple.
Definition tuple.h:122
A dependent function type.
Definition lam.h:11
static const Def * infer(const Def *dom, const Def *codom)
Definition check.cpp:292
A dependent tuple type.
Definition tuple.h:9
Data constructor for a Sigma.
Definition tuple.h:56
This is a thin wrapper for absl::InlinedVector<T, N, A> which is a drop-in replacement for std::vecto...
Definition vector.h:17
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:397
const Lit * lit_idx(I val)
Definition world.h:399
const Def * insert(const Def *d, const Def *i, const Def *val)
Definition world.cpp:383
const Def * type_i16()
Definition world.h:469
const Pi * fn(Defs dom, const Def *codom, bool implicit=false)
Definition world.h:267
const Def * meet(Defs ops)
Definition world.h:436
const auto & flags2annex() const
Definition world.h:167
const Lam * con(Defs dom, Lam::Filter f, const Def *body)
Definition world.h:283
const Def * uinc(const Def *op, level_t offset=1)
Definition world.cpp:112
const Pi * cn()
Definition world.h:263
const Lit * lit(const Def *type, u64 val)
Definition world.cpp:484
const Def * arr(u64 n, const Def *body)
Definition world.h:331
u32 next_run()
Definition world.h:90
friend void swap(World &w1, World &w2) noexcept
Definition world.h:697
Log & log()
Definition world.cpp:70
const Def * implicit_app(const Def *callee, nat_t arg)
Definition world.h:483
const Def * extract(const Def *d, u64 a, u64 i)
Definition world.h:362
auto & muts()
Definition world.h:504
const Def * type_i4()
Definition world.h:467
const Lit * lit_i8()
Definition world.h:391
Hole * mut_hole_infer_entity()
Either a value ?:?:Type ? or a type ?:Type ?:Type ?.
Definition world.h:223
const Pi * cn(const Def *dom, bool implicit=false)
Definition world.h:264
const Def * type_int(nat_t width)
Constructs a type Idx of size 2^width.
Definition world.h:462
World & operator=(World)=delete
const Lit * lit_i16(u16 val)
Definition world.h:411
const Lit * lit_i1(bool val)
Definition world.h:407
const Def * arr(View< u64 > shape, const Def *body)
Definition world.h:332
const Lit * lit_i32()
Definition world.h:393
Driver & driver()
Definition world.h:81
Lam * mut_fun(const Def *dom, Defs codom)
Definition world.h:300
const Type * type(const Def *level)
Definition world.cpp:105
void make_external(Def *)
Definition world.cpp:87
const Driver & driver() const
Definition world.h:80
const Lam * lam(const Def *dom, const Def *codom, Lam::Filter f, const Def *body)
Definition world.h:284
Lam * mut_lam(const Def *dom, Defs codom)
Definition world.h:296
const Lit * lit_tt()
Definition world.h:423
const Def * filter(Lam::Filter filter)
Definition world.h:275
World(Driver *)
Definition world.cpp:59
const auto & sym2external() const
Definition world.h:190
const Def * type_idx(nat_t size)
Definition world.h:458
const Def * pack(const Def *arity, const Def *body)
Definition world.cpp:454
void set(std::string_view name)
Definition world.h:85
const Def * app(const Def *callee, const Def *arg)
Definition world.cpp:181
u32 curr_gid() const
Manage global identifier - a unique number for each Def.
Definition world.h:88
const Axm * axm(const Def *type)
See above.
Definition world.h:245
const Def * match(Defs)
Definition world.cpp:550
World inherit()
Inherits the state into the new World.
Definition world.h:72
const Def * type_bot()
Definition world.h:431
const Def * arr(const Def *shape, const Def *body)
Definition world.cpp:427
const Pi * pi(const Def *dom, const Def *codom, bool implicit=false)
Definition world.h:251
const Def * pack(u64 n, const Def *body)
Definition world.h:352
const Def * insert(const Def *d, u64 a, u64 i, const Def *val)
Definition world.h:374
const auto & muts() const
Definition world.h:506
const Univ * univ()
Definition world.h:200
const Lam * lam(Defs dom, const Def *codom, Lam::Filter f, const Def *body)
Definition world.h:285
const Lit * lit_0_1()
Definition world.h:388
const Lam * fun(Defs dom, const Def *codom, Lam::Filter f, const Def *body)
Definition world.h:289
const Def * type_i8()
Definition world.h:468
World & verify()
Verifies that all externals() and annexes() are Def::is_closed(), if MIM_ENABLE_CHECKS.
Definition world.cpp:636
const Def * bot(const Def *type)
Definition world.h:429
const Lit * lit_i64()
Definition world.h:394
Arr * mut_arr(const Def *type)
Definition world.h:327
const Lam * lam(const Def *dom, Defs codom, Lam::Filter f, const Def *body)
Definition world.h:286
const Lit * lit_idx_mod(nat_t mod, u64 val)
Constructs a Lit of type Idx of size mod.
Definition world.h:419
const Idx * type_idx()
Definition world.h:454
const Def * type_i1()
Definition world.h:465
Pi * mut_pi(const Def *type, bool implicit=false)
Definition world.h:255
const Lit * lit_univ_0()
Definition world.h:382
const Def * annex(Id id)
Lookup annex by Axm::id.
Definition world.h:171
void set_loc(Loc loc={})
Definition world.h:110
const Def * implicit_app(const Def *callee, E arg)
Definition world.h:487
Sym name() const
Definition world.h:83
const Pi * cn(Defs dom, bool implicit=false)
Definition world.h:265
void dump()
Dump to std::cout.
Definition dump.cpp:484
const Lam * fun(const Def *dom, Defs codom, Lam::Filter f, const Def *body)
Definition world.h:290
const Lit * lit_univ_1()
Definition world.h:383
void write()
Same above but file name defaults to World::name.
Definition dump.cpp:495
const Lam * lam(Defs dom, Defs codom, Lam::Filter f, const Def *body)
Definition world.h:287
const Def * register_annex(plugin_t p, tag_t t, sub_t s, const Def *def)
Definition world.h:183
Lam * mut_fun(Defs dom, const Def *codom)
Definition world.h:299
Lam * mut_fun(const Def *dom, const Def *codom)
Definition world.h:298
const Lit * lit_i1()
Definition world.h:390
const Axm * axm(NormalizeFn n, u8 curry, u8 trip, const Def *type)
Builds a fresh Axm with descending Axm::sub.
Definition world.h:242
const Nat * type_nat()
Definition world.h:453
const Pi * fn(const Def *dom, Defs codom, bool implicit=false)
Definition world.h:268
Hole * mut_hole(const Def *type)
Definition world.h:218
const Axm * axm(const Def *type, plugin_t p, tag_t t, sub_t s)
Definition world.h:236
const Lam * lam(const Pi *pi, Lam::Filter f, const Def *body)
Definition world.h:279
const Lam * fun(Defs dom, Defs codom, Lam::Filter f, const Def *body)
Definition world.h:291
Lam * mut_lam(const Def *dom, const Def *codom)
Definition world.h:294
const Def * gid2def(u32 gid)
Lookup Def by gid.
Definition world.cpp:630
Flags & flags()
Retrieve compile Flags.
Definition world.cpp:71
const Def * implicit_app(const Def *callee, const Def *arg)
Places Holes as demanded by Pi::is_implicit() and then apps arg.
Definition world.cpp:176
ScopedLoc push(Loc loc)
Definition world.h:111
const Def * implicit_app(const Def *callee, Defs args)
Definition world.h:480
void debug_dump()
Dump in Debug build if World::log::level is Log::Level::Debug.
Definition dump.cpp:486
u32 next_gid()
Definition world.h:89
const Def * extract(const Def *d, u64 i)
Definition world.h:363
const Lam * fun(const Def *dom, const Def *codom, Lam::Filter f, const Def *body)
Definition world.h:288
const Def * inj(const Def *type, const Def *value)
Definition world.cpp:543
const Def * call(Args &&... args)
Definition world.h:496
const auto & breakpoints()
Definition world.h:154
const Type * type()
Definition world.h:205
const Axm * axm(NormalizeFn n, u8 curry, u8 trip, const Def *type, plugin_t p, tag_t t, sub_t s)
Definition world.h:233
const Def * var(const Def *type, Def *mut)
Definition world.cpp:167
void set(Sym name)
Definition world.h:84
const Def * app(const Def *callee, Defs args)
Definition world.h:308
const Def * pack(View< u64 > shape, const Def *body)
Definition world.h:353
Lam * mut_fun(Defs dom, Defs codom)
Definition world.h:301
const Lit * lit_i2(u8 val)
Definition world.h:408
const Def * extract(const Def *d, const Def *i)
Definition world.cpp:321
Pack * mut_pack(const Def *type)
Definition world.h:349
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:385
Sym sym(std::string_view)
Definition world.cpp:74
const Lit * lit_i16()
Definition world.h:392
Global * global(const Def *type, bool is_mutable=true)
Definition world.h:448
Lam * mut_lam(Defs dom, const Def *codom)
Definition world.h:295
const Lit * lit_ff()
Definition world.h:422
const Lit * lit_nat_max()
Definition world.h:387
const Def * raw_app(const Def *type, const Def *callee, Defs args)
Definition world.h:313
const Pi * pi(Defs dom, const Def *codom, bool implicit=false)
Definition world.h:252
Def * external(Sym name)
Lookup by name.
Definition world.h:191
const Def * bound(Defs ops)
Definition world.cpp:507
const Def * join(Defs ops)
Definition world.h:435
const Def * ext(const Def *type)
Definition world.cpp:500
Sym append_suffix(Sym name, std::string suffix)
Appends a suffix or an increasing number if the suffix already exists.
Definition world.cpp:587
void make_internal(Def *)
Definition world.cpp:94
const Proxy * proxy(const Def *type, Defs ops, u32 index, u32 tag)
Definition world.h:214
const Lit * lit_i32(u32 val)
Definition world.h:412
const Lit * lit_i8(u8 val)
Definition world.h:410
Lam * mut_lam(Defs dom, Defs codom)
Definition world.h:297
const Def * type_top()
Definition world.h:432
Sigma * mut_sigma(size_t size)
A mutable Sigma of type level.
Definition world.h:320
const Lit * lit_univ(u64 level)
Definition world.h:381
const Pi * pi(Defs dom, Defs codom, bool implicit=false)
Definition world.h:254
const Tuple * tuple()
the unit value of type []
Definition world.h:343
const Type * type_infer_univ()
Definition world.h:204
const Def * call(Id id, Args &&... args)
Complete curried call of annexes obeying implicits.
Definition world.h:495
const Def * type_bool()
Definition world.h:464
const Def * uniq(const Def *inhabitant)
Definition world.cpp:585
void dummy()
Definition world.h:517
const Def * raw_app(const Axm *axm, u8 curry, u8 trip, const Def *type, const Def *callee, const Def *arg)
Definition world.cpp:254
const Def * umax(Defs)
Definition world.cpp:121
Vector< Def * > copy_externals() const
Definition world.h:193
const Lam * con(const Def *dom, Lam::Filter f, const Def *body)
Definition world.h:282
const Def * type_i2()
Definition world.h:466
const Def * arr_unsafe(const Def *body)
Definition world.h:335
const Def * merge(const Def *type, Defs ops)
Definition world.cpp:531
const Lit * lit_i64(u64 val)
Definition world.h:413
const Def * type_i64()
Definition world.h:471
const Sigma * sigma()
The unit type within Type 0.
Definition world.h:322
const Lit * lit_nat(nat_t a)
Definition world.h:384
const State & state() const
Definition world.h:78
Hole * mut_hole_type()
Definition world.h:220
const auto & vars() const
Definition world.h:505
const Def * register_annex(flags_t f, const Def *)
Definition world.cpp:77
const Def * top(const Def *type)
Definition world.h:430
const Def * type_idx(const Def *size)
Definition world.h:456
Lam * mut_con(const Def *dom)
Definition world.h:292
Arr * mut_arr()
Definition world.h:328
auto & vars()
Definition world.h:503
Defs reduce(const Var *var, const Def *arg)
Yields the new body of [mut->var() -> arg]mut.
Definition world.cpp:607
const Lit * lit_int(nat_t width, u64 val)
Constructs a Lit of type Idx of size 2^width.
Definition world.h:406
const Lit * lit_bool(bool val)
Definition world.h:421
void breakpoint(u32 gid)
Trigger breakpoint in your debugger when creating Def with Def::gid gid.
Definition world.cpp:628
const Def * select(const Def *cond, const Def *t, const Def *f)
Builds (f, t)#cond.
Definition world.h:367
Sigma * mut_sigma(const Def *type, size_t size)
Definition world.h:318
Hole * mut_hole_univ()
Definition world.h:219
Lam * mut_con(Defs dom)
Definition world.h:293
const Def * split(const Def *type, const Def *value)
Definition world.cpp:548
const Def * top_nat()
Definition world.h:433
const Pi * fn(const Def *dom, const Def *codom, bool implicit=false)
Definition world.h:266
auto annexes() const
Definition world.h:168
World(World &&other) noexcept
Definition world.h:68
const Lit * lit_nat_1()
Definition world.h:386
const Pi * pi(const Def *dom, Defs codom, bool implicit=false)
Definition world.h:253
bool freeze(bool on=true) const
Yields old frozen state.
Definition world.h:133
const Def * type_i32()
Definition world.h:470
const Lit * lit_i4(u8 val)
Definition world.h:409
void dot(std::ostream &os, bool annexes=false, bool types=false) const
Dumps DOT to os.
Definition dot.cpp:147
const Def * insert(const Def *d, u64 i, const Def *val)
Definition world.h:375
const Pi * fn(Defs dom, Defs codom, bool implicit=false)
Definition world.h:269
Lam * mut_lam(const Pi *pi)
Definition world.h:280
const Def * annex()
Get Axm from a plugin.
Definition world.h:180
Definition ast.h:14
View< const Def * > Defs
Definition def.h:48
u64 nat_t
Definition types.h:43
Vector< const Def * > DefVec
Definition def.h:49
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:103
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:94
Span< const T, N > View
Definition span.h:93
void error(Loc loc, const char *f, Args &&... args)
Definition dbg.h:122
u64 level_t
Definition types.h:42
TExt< true > Top
Definition lattice.h:159
std::ostream & outln(const char *fmt, Args &&... args)
Definition print.h:190
const Def *(*)(const Def *, const Def *, const Def *) NormalizeFn
Definition def.h:70
u64 plugin_t
Definition types.h:46
uint32_t u32
Definition types.h:34
TExt< false > Bot
Definition lattice.h:158
uint64_t u64
Definition types.h:34
u8 tag_t
Definition types.h:47
uint8_t u8
Definition types.h:34
@ Nat
Definition def.h:84
@ Univ
Definition def.h:84
@ Idx
Definition def.h:84
@ Sigma
Definition def.h:84
@ Type
Definition def.h:84
@ Tuple
Definition def.h:84
@ Lit
Definition def.h:84
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
static constexpr plugin_t Global_Plugin
Definition plugin.h:58
static Sym demangle(Driver &, plugin_t plugin)
Reverts an Axm::mangled string to a Sym.
Definition plugin.cpp:37
static constexpr flags_t Base
Definition plugin.h:118
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