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