MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
lam.h
Go to the documentation of this file.
1#pragma once
2
3#include <span>
4#include <type_traits>
5#include <variant>
6
7#include "mim/def.h"
8
9namespace mim {
10
11class Extract;
12
13/// A [dependent function type](https://en.wikipedia.org/wiki/Dependent_type#%CE%A0_type).
14/// @see Lam
15class Pi : public Def, public Setters<Pi> {
16protected:
17 /// Constructor for an *immutable* Pi.
18 Pi(const Def* type, const Def* dom, const Def* codom, bool implicit)
19 : Def(Node, type, {dom, codom}, (flags_t)implicit) {}
20 /// Constructor for a *mutable* Pi.
21 Pi(const Def* type, bool implicit)
22 : Def(Node, type, 2, implicit ? 1 : 0) {}
23
24public:
25 /// @name Get/Set implicit
26 ///@{
27 bool is_implicit() const { return flags(); }
28 Pi* make_implicit() { return flags_ = (flags_t) true, this; }
29 Pi* make_explicit() { return flags_ = (flags_t) false, this; }
30 ///@}
31
32 /// @name dom & codom
33 /// @anchor pi_dom
34 /// @see @ref proj
35 ///@{
36 const Def* dom() const { return op(0); }
37 const Def* codom() const { return op(1); }
38 MIM_PROJ(dom, const)
39 MIM_PROJ(codom, const)
40 ///@}
41
42 /// @name Continuations
43 /// @anchor continuations
44 /// Checks certain properties of @p d regarding continuations.
45 ///@{
46 // clang-format off
47 /// Is this a continuation - i.e. is the Pi::codom mim::Bot%tom?
48 static const Pi* isa_cn(const Def* d) { return d->isa<Pi>() && d->as<Pi>()->codom()->node() == Node::Bot ? d->as<Pi>() : nullptr; }
49 /// Is this a continuation (Pi::isa_cn) which has a Pi::ret_pi?
50 static const Pi* isa_returning(const Def* d) { return isa_cn(d) && d->as<Pi>()->ret_pi() ? d->as<Pi>() : nullptr; }
51 /// Is this a continuation (Pi::isa_cn) that is **not** Pi::isa_returning?
52 static const Pi* isa_basicblock(const Def* d) { return isa_cn(d) && !d->as<Pi>()->ret_pi() ? d->as<Pi>() : nullptr; }
53 // clang-format on
54 /// Is @p d an Pi::is_implicit (mutable) Pi?
55 static Pi* isa_implicit(const Def* d) {
56 if (auto pi = d->isa_mut<Pi>(); pi && pi->is_implicit()) return pi;
57 return nullptr;
58 }
59 /// Yields the Pi::ret_pi() of @p d, if it is in fact a Pi.
60 static const Pi* has_ret_pi(const Def* d) { return d->isa<Pi>() ? d->as<Pi>()->ret_pi() : nullptr; }
61 ///@}
62
63 /// @name Return Continuation
64 /// @anchor return_continuation
65 ///@{
66
67 /// Yields the last Pi::dom, if Pi::isa_basicblock.
68 const Pi* ret_pi() const;
69 /// Pi::dom%ain of Pi::ret_pi.
70 const Def* ret_dom() const { return ret_pi()->dom(); }
71 ///@}
72
73 /// @name Setters
74 /// @see @ref set_ops "Setting Ops"
75 ///@{
76 using Setters<Pi>::set;
77 Pi* set(const Def* dom, const Def* codom) { return Def::set({dom, codom})->as<Pi>(); }
78 Pi* set_dom(const Def* dom) { return Def::set(0, dom)->as<Pi>(); }
79 Pi* set_dom(Defs doms);
80 Pi* set_codom(const Def* codom) { return Def::set(1, codom)->as<Pi>(); }
81 Pi* unset() { return Def::unset()->as<Pi>(); }
82 ///@}
83
84 /// @name Type Checking
85 ///@{
86 const Def* check(size_t, const Def*) final;
87 const Def* check() final;
88 static const Def* infer(const Def* dom, const Def* codom);
89 ///@}
90
91 /// @name Rebuild
92 ///@{
93 Pi* stub(const Def* type) { return stub_(world(), type)->set(dbg()); }
94 const Pi* immutabilize() final;
95 const Def* reduce(const Def* arg) const { return Def::reduce(arg).front(); }
96 constexpr size_t reduction_offset() const noexcept final { return 1; }
97 ///@}
98
99 static constexpr auto Node = mim::Node::Pi;
100 static constexpr size_t Num_Ops = 2;
101
102private:
103 const Def* rebuild_(World&, const Def*, Defs) const final;
104 Pi* stub_(World&, const Def*) final;
105
106 friend class World;
107};
108
109/// A function.
110/// @see Pi
111class Lam : public Def, public Setters<Lam> {
112private:
113 Lam(const Pi* pi, const Def* filter, const Def* body)
114 : Def(Node, pi, {filter, body}, 0) {}
115 Lam(const Pi* pi)
116 : Def(Node, pi, 2, 0) {}
117
118public:
119 using Filter = std::variant<bool, const Def*>;
120
121 /// @name ops
122 ///@{
123 const Def* filter() const { return op(0); }
124 const Def* body() const { return op(1); }
125 ///@}
126
127 /// @name type
128 /// @anchor lam_dom
129 /// @see @ref proj
130 ///@{
131 const Pi* type() const { return Def::type()->as<Pi>(); }
132 const Def* dom() const { return type()->dom(); }
133 const Def* codom() const { return type()->codom(); }
134 MIM_PROJ(dom, const)
135 MIM_PROJ(codom, const)
136 ///@}
137
138 /// @name Continuations
139 /// @see @ref continuations "Pi: Continuations"
140 ///@{
141 // clang-format off
142 static const Lam* isa_cn(const Def* d) { return Pi::isa_cn(d->type()) ? d->isa<Lam>() : nullptr; }
143 static const Lam* isa_basicblock(const Def* d) { return Pi::isa_basicblock(d->type()) ? d->isa<Lam>() : nullptr; }
144 static const Lam* isa_returning(const Def* d) { return Pi::isa_returning (d->type()) ? d->isa<Lam>() : nullptr; }
145 static Lam* isa_mut_cn(const Def* d) { return isa_cn(d) ? d->isa_mut<Lam>() : nullptr; } ///< Only for mutables.
146 static Lam* isa_mut_basicblock(const Def* d) { return isa_basicblock(d) ? d->isa_mut<Lam>(): nullptr; } ///< Only for mutables.
147 static Lam* isa_mut_returning(const Def* d) { return isa_returning (d) ? d->isa_mut<Lam>(): nullptr; } ///< Only for mutables.
148 // clang-format on
149 ///@}
150
151 /// @name Return Continuation
152 /// @see @ref return_continuation "Pi: Return Continuation"
153 ///@{
154 const Pi* ret_pi() const { return type()->ret_pi(); }
155 const Def* ret_dom() const { return ret_pi()->dom(); }
156 /// Yields the Lam::var of the Lam::ret_pi.
157 const Def* ret_var() { return type()->ret_pi() ? var(num_vars() - 1) : nullptr; }
158 ///@}
159
160 /// @name Setters
161 /// Lam::Filter is a `std::variant<bool, const Def*>` that lets you set the Lam::filter() like this:
162 /// ```cpp
163 /// lam1->app(true, f, arg);
164 /// lam2->app(my_filter_def, f, arg);
165 /// ```
166 /// @note The filter belongs to the *Lam%bda* and **not** the body.
167 /// @see @ref set_ops "Setting Ops"
168 ///@{
169 using Setters<Lam>::set;
170 Lam* set(Filter filter, const Def* body);
171 Lam* set_filter(Filter); ///< Set filter first.
172 Lam* set_body(const Def* body) { return Def::set(1, body)->as<Lam>(); } ///< Set body second.
173 /// Set body to an App of @p callee and @p arg.
174 Lam* app(Filter filter, const Def* callee, const Def* arg);
175 /// Set body to an App of @p callee and @p args.
176 Lam* app(Filter filter, const Def* callee, Defs args);
177 /// Set body to an App of `(f, t)#cond mem` or `(f, t)#cond ()` if @p mem is `nullptr`.
178 Lam* branch(Filter filter, const Def* cond, const Def* t, const Def* f, const Def* arg = nullptr);
179 Lam* set(Defs ops) { return Def::set(ops)->as<Lam>(); }
180 Lam* unset() { return Def::unset()->as<Lam>(); }
181 ///@}
182
183 /// @name Rebuild
184 ///@{
185 Lam* stub(const Def* type) { return stub_(world(), type)->set(dbg()); }
186 using Def::reduce;
187 Defs reduce(Defs) const;
188 const Def* reduce_body(const Def* arg) const { return reduce(arg).back(); }
189 constexpr size_t reduction_offset() const noexcept final { return 0; }
190 ///@}
191
192 /// @name Eta-Conversion
193 ///@{
194 static Lam* eta_expand(Filter, const Def* f);
195 static Lam* eta_expand(const Def* f) { return eta_expand(true, f); } ///< Use `true` Filter.
196 /// Yields body(), if eta-convertible and `nullptr` otherwise.
197 /// η-convertible means: `lm x = body x` where `x` ∉ `body`.
198 const Def* eta_reduce() const;
199 ///@}
200
201 /// @name Type Checking
202 ///@{
203 const Def* check(size_t, const Def*) final;
204 ///@}
205
206 static constexpr auto Node = mim::Node::Lam;
207 static constexpr size_t Num_Ops = 2;
208
209private:
210 const Def* rebuild_(World&, const Def*, Defs) const final;
211 Lam* stub_(World&, const Def*) final;
212
213 friend class World;
214};
215
216/// @name Lam
217/// GIDSet / GIDMap keyed by Lam::gid of `Lam*`.
218///@{
219template<class To>
223///@}
224
225class App : public Def, public Setters<App> {
226private:
227 App(const Axm* axm, u8 curry, u8 trip, const Def* type, const Def* callee, const Def* arg)
228 : Def(Node, type, {callee, arg}, 0) {
229 axm_ = axm;
230 curry_ = curry;
231 trip_ = trip;
232 }
233
234 template<size_t N, bool Callee, bool Args>
235 static auto uncurry_(const Def* callee) {
236 if constexpr (N == std::dynamic_extent) {
237 auto args = DefVec();
238 while (auto app = callee->isa<App>()) {
239 if constexpr (Args) args.emplace_back(app->arg());
240 callee = app->callee();
241 }
242
243 if constexpr (Callee && Args) {
244 std::ranges::reverse(args);
245 return std::pair{callee, args};
246 } else if constexpr (Args) {
247 std::ranges::reverse(args);
248 return args;
249 } else {
250 return callee;
251 }
252 } else {
253 auto args = std::array<const Def*, N>();
254 for (size_t i = N; i-- != 0;) {
255 if (auto app = callee->isa<App>()) {
256 if constexpr (Args) args[i] = app->arg();
257 callee = app->callee();
258 } else {
259 if constexpr (Args) args[i] = nullptr;
260 }
261 }
262
263 if constexpr (Callee && Args)
264 return std::pair{callee, args};
265 else if constexpr (Args)
266 return args;
267 else
268 return callee;
269 }
270 }
271
272public:
273 using Setters<App>::set;
274
275 /// @name callee
276 ///@{
277 const Def* callee() const { return op(0); }
278 const App* decurry() const { return callee()->as<App>(); } ///< Returns App::callee again as App.
279 const Pi* callee_type() const { return callee()->type()->as<Pi>(); }
280 ///@}
281
282 /// @name arg
283 /// @anchor app_arg
284 /// @see @ref proj
285 ///@{
286 const Def* arg() const { return op(1); }
287 MIM_PROJ(arg, const)
288 ///@}
289
290 /// @name Get axm, current curry counter and trip count
291 ///@{
292 const Axm* axm() const { return axm_; }
293 u8 curry() const { return curry_; }
294 u8 trip() const { return trip_; }
295 ///@}
296
297 /// @name Uncurry
298 /// Retrieve all App::arg%s of a curried App.
299 /// Use like this:
300 /// ```
301 /// // 1. Variant:
302 /// auto [abc, de] = app->uncurry<2>();
303 /// auto [a, b, c] = abc->projs<3>();
304 /// auto [d, e] = de->projs<2>();
305 ///
306 /// // 2. Variant:
307 /// auto [callee , args] = App::uncurry(def);
308 ///
309 /// ```
310 /// @returns
311 /// 1. Variant: <br>
312 /// *only* the arguments in a `std::array<const Def*, N>`.
313 /// You will *not* retrieve the initial callee because if you know the number of curried App%s,
314 /// you probably also know the callee anyway.
315 /// Also, if you "overshoot" the number of curried App%s, the superflous args on the left will be set to
316 /// `nullptr`.
317 /// 2. Variant: <br>
318 /// A pair that contains:
319 /// 1. The initial callee.
320 /// 2. A DefVec of all curried App::arg%s.
321 /// You can enforce variant 1 / variant 2 by with the template argument @p Callee.
322 ///@{
323 // clang-format off
324 template<size_t N = std::dynamic_extent> static auto uncurry(const Def* def) { return uncurry_<N, true, true >(def ); }
325 template<size_t N = std::dynamic_extent> auto uncurry() const { return uncurry_<N, true, true >(this); }
326
327 static const Def* uncurry_callee(const Def* def) { return uncurry_<std::dynamic_extent, true, false>(def ); }
328 const Def* uncurry_callee() const { return uncurry_<std::dynamic_extent, true, false>(this); }
329
330 template<size_t N = std::dynamic_extent> static auto uncurry_args(const Def* def) { return uncurry_<N, false, true>(def ); }
331 template<size_t N = std::dynamic_extent> auto uncurry_args() const { return uncurry_<N, false, true>(this); }
332 // clang-format on
333 ///@}
334
335 static constexpr auto Node = mim::Node::App;
336 static constexpr size_t Num_Ops = 2;
337
338private:
339 const Def* rebuild_(World&, const Def*, Defs) const final;
340
341 friend class World;
342};
343
344/// @name Helpers to work with Functions
345///@{
346inline const App* isa_callee(const Def* def, size_t i) { return i == 0 ? def->isa<App>() : nullptr; }
347
348/// These are Lam%s that are neither `nullptr`, nor Lam::is_external, nor Lam::is_unset.
349inline Lam* isa_workable(Lam* lam) {
350 if (!lam || lam->is_external() || !lam->is_set()) return nullptr;
351 return lam;
352}
353
354inline std::pair<const App*, Lam*> isa_apped_mut_lam(const Def* def) {
355 if (auto app = def->isa<App>()) return {app, app->callee()->isa_mut<Lam>()};
356 return {nullptr, nullptr};
357}
358
359/// The high level view is:
360/// ```
361/// f: B -> C
362/// g: A -> B
363/// f o g := λ x. f(g(x)) : A -> C
364/// ```
365/// In CPS the types look like:
366/// ```
367/// f: Cn[B, Cn C]
368/// g: Cn[A, Cn B]
369/// h = f o g
370/// h: Cn[A, cn C]
371/// h = λ (a ret_h) = g (a, h')
372/// h': Cn B
373/// h'= λ b = f (b, ret_h)
374/// ```
375const Def* compose_cn(const Def* f, const Def* g);
376///@}
377
378} // namespace mim
const Axm * axm() const
Definition lam.h:292
static constexpr size_t Num_Ops
Definition lam.h:336
static const Def * uncurry_callee(const Def *def)
Definition lam.h:327
const Pi * callee_type() const
Definition lam.h:279
u8 curry() const
Definition lam.h:293
const App * decurry() const
Returns App::callee again as App.
Definition lam.h:278
static constexpr auto Node
Definition lam.h:335
friend class World
Definition lam.h:341
auto uncurry() const
Definition lam.h:325
static auto uncurry(const Def *def)
Definition lam.h:324
const Def * callee() const
Definition lam.h:277
static auto uncurry_args(const Def *def)
Definition lam.h:330
const Def * uncurry_callee() const
Definition lam.h:328
auto uncurry_args() const
Definition lam.h:331
const Def * arg() const
Definition lam.h:286
u8 trip() const
Definition lam.h:294
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:112
Definition axm.h:9
Base class for all Defs.
Definition def.h:251
bool is_set() const
Yields true if empty or the last op is set.
Definition def.cpp:295
constexpr Node node() const noexcept
Definition def.h:274
Def * set(size_t i, const Def *)
Successively set from left to right.
Definition def.cpp:263
u8 trip_
Definition def.h:669
World & world() const noexcept
Definition def.cpp:439
virtual const Def * check()
After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
Definition def.h:583
constexpr auto ops() const noexcept
Definition def.h:305
constexpr flags_t flags() const noexcept
Definition def.h:269
u8 curry_
Definition def.h:668
const Def * op(size_t i) const noexcept
Definition def.h:308
nat_t num_vars() noexcept
Definition def.h:429
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.cpp:447
bool is_external() const noexcept
Definition def.h:467
const Def * var()
Not necessarily a Var: E.g., if the return type is [], this will yield ().
Definition def.cpp:307
flags_t flags_
Definition def.h:667
Def * unset()
Unsets all Def::ops; works even, if not set at all or only partially set.
Definition def.cpp:286
constexpr auto reduce(const Def *arg) const
Definition def.h:563
Dbg dbg() const
Definition def.h:505
Extracts from a Sigma or Array-typed Extract::tuple the element at position Extract::index.
Definition tuple.h:206
A function.
Definition lam.h:111
std::variant< bool, const Def * > Filter
Definition lam.h:119
Lam * unset()
Definition lam.h:180
const Def * filter() const
Definition lam.h:123
static const Lam * isa_cn(const Def *d)
Definition lam.h:142
static constexpr size_t Num_Ops
Definition lam.h:207
Lam * set(Filter filter, const Def *body)
Definition lam.cpp:29
static Lam * eta_expand(Filter, const Def *f)
Definition lam.cpp:51
Lam * set_filter(Filter)
Set filter first.
Definition lam.cpp:28
static Lam * isa_mut_basicblock(const Def *d)
Only for mutables.
Definition lam.h:146
Defs reduce(Defs) const
Definition lam.cpp:39
static const Lam * isa_returning(const Def *d)
Definition lam.h:144
constexpr size_t reduction_offset() const noexcept final
First Def::op that needs to be dealt with during reduction; e.g.
Definition lam.h:189
const Pi * ret_pi() const
Definition lam.h:154
const Def * dom() const
Definition lam.h:132
static Lam * isa_mut_returning(const Def *d)
Only for mutables.
Definition lam.h:147
const Pi * type() const
Definition lam.h:131
Lam * set(Defs ops)
Definition lam.h:179
Lam * stub_(World &, const Def *) final
Definition def.cpp:151
static constexpr auto Node
Definition lam.h:206
friend class World
Definition lam.h:213
const Def * eta_reduce() const
Yields body(), if eta-convertible and nullptr otherwise.
Definition lam.cpp:43
static const Lam * isa_basicblock(const Def *d)
Definition lam.h:143
Lam * branch(Filter filter, const Def *cond, const Def *t, const Def *f, const Def *arg=nullptr)
Set body to an App of (f, t)#cond mem or (f, t)#cond () if mem is nullptr.
Definition lam.cpp:35
Lam * app(Filter filter, const Def *callee, const Def *arg)
Set body to an App of callee and arg.
Definition lam.cpp:30
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:117
const Def * ret_dom() const
Definition lam.h:155
Lam * set_body(const Def *body)
Set body second.
Definition lam.h:172
Lam * stub(const Def *type)
Definition lam.h:185
const Def * body() const
Definition lam.h:124
static Lam * isa_mut_cn(const Def *d)
Only for mutables.
Definition lam.h:145
static Lam * eta_expand(const Def *f)
Use true Filter.
Definition lam.h:195
const Def * reduce_body(const Def *arg) const
Definition lam.h:188
const Def * ret_var()
Yields the Lam::var of the Lam::ret_pi.
Definition lam.h:157
const Def * codom() const
Definition lam.h:133
A dependent function type.
Definition lam.h:15
constexpr size_t reduction_offset() const noexcept final
First Def::op that needs to be dealt with during reduction; e.g.
Definition lam.h:96
const Def * ret_dom() const
Pi::domain of Pi::ret_pi.
Definition lam.h:70
const Def * check() final
After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
Definition check.cpp:325
Pi(const Def *type, bool implicit)
Constructor for a mutable Pi.
Definition lam.h:21
Pi * unset()
Definition lam.h:81
static const Pi * has_ret_pi(const Def *d)
Yields the Pi::ret_pi() of d, if it is in fact a Pi.
Definition lam.h:60
Pi * set_codom(const Def *codom)
Definition lam.h:80
static constexpr size_t Num_Ops
Definition lam.h:100
Pi * make_implicit()
Definition lam.h:28
Pi(const Def *type, const Def *dom, const Def *codom, bool implicit)
Constructor for an immutable Pi.
Definition lam.h:18
static const Pi * isa_cn(const Def *d)
Is this a continuation - i.e. is the Pi::codom mim::Bottom?
Definition lam.h:48
static const Pi * isa_basicblock(const Def *d)
Is this a continuation (Pi::isa_cn) that is not Pi::isa_returning?
Definition lam.h:52
static const Def * infer(const Def *dom, const Def *codom)
Definition check.cpp:318
bool is_implicit() const
Definition lam.h:27
Pi * make_explicit()
Definition lam.h:29
const Def * dom() const
Definition lam.h:36
friend class World
Definition lam.h:106
const Def * codom() const
Definition lam.h:37
static Pi * isa_implicit(const Def *d)
Is d an Pi::is_implicit (mutable) Pi?
Definition lam.h:55
Pi * set(const Def *dom, const Def *codom)
Definition lam.h:77
static constexpr auto Node
Definition lam.h:99
const Def * reduce(const Def *arg) const
Definition lam.h:95
const Pi * immutabilize() final
Tries to make an immutable from a mutable.
Definition def.cpp:188
Pi * stub(const Def *type)
Definition lam.h:93
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:121
const Pi * ret_pi() const
Yields the last Pi::dom, if Pi::isa_basicblock.
Definition lam.cpp:13
Pi * stub_(World &, const Def *) final
Definition def.cpp:153
Pi * set_dom(const Def *dom)
Definition lam.h:78
static const Pi * isa_returning(const Def *d)
Is this a continuation (Pi::isa_cn) which has a Pi::ret_pi?
Definition lam.h:50
CRTP-based mixin to declare setters for Def::loc & Def::name using a covariant return type.
Definition def.h:195
#define MIM_PROJ(NAME, CONST)
Use as mixin to wrap all kind of Def::proj and Def::projs variants.
Definition def.h:164
Definition ast.h:14
View< const Def * > Defs
Definition def.h:76
Vector< const Def * > DefVec
Definition def.h:77
GIDSet< Lam * > LamSet
Definition lam.h:221
u64 flags_t
Definition types.h:45
std::pair< const App *, Lam * > isa_apped_mut_lam(const Def *def)
Definition lam.h:354
absl::flat_hash_map< K, V, GIDHash< K > > GIDMap
Definition util.h:195
LamMap< Lam * > Lam2Lam
Definition lam.h:222
GIDMap< Lam *, To > LamMap
Definition lam.h:220
Lam * isa_workable(Lam *lam)
These are Lams that are neither nullptr, nor Lam::is_external, nor Lam::is_unset.
Definition lam.h:349
const App * isa_callee(const Def *def, size_t i)
Definition lam.h:346
const Def * compose_cn(const Def *f, const Def *g)
The high level view is:
Definition lam.cpp:62
absl::flat_hash_set< K, GIDHash< K > > GIDSet
Definition util.h:196
uint8_t u8
Definition types.h:34
@ Pi
Definition def.h:114
@ Bot
Definition def.h:114
@ Lam
Definition def.h:114
@ App
Definition def.h:114