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