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 <variant>
4
5#include "mim/def.h"
6
7namespace mim {
8
9/// A [dependent function type](https://en.wikipedia.org/wiki/Dependent_type#%CE%A0_type).
10/// @see Lam
11class Pi : public Def, public Setters<Pi> {
12protected:
13 /// Constructor for an *immutable* Pi.
14 Pi(const Def* type, const Def* dom, const Def* codom, bool implicit)
15 : Def(Node, type, {dom, codom}, (flags_t)implicit) {}
16 /// Constructor for a *mutable* Pi.
17 Pi(const Def* type, bool implicit)
18 : Def(Node, type, 2, implicit ? 1 : 0) {}
19
20public:
21 /// @name Get/Set implicit
22 ///@{
23 bool is_implicit() const { return flags(); }
24 Pi* make_implicit() { return flags_ = (flags_t) true, this; }
25 Pi* make_explicit() { return flags_ = (flags_t) false, this; }
26 ///@}
27
28 /// @name dom & codom
29 /// @anchor pi_dom
30 /// @see @ref proj
31 ///@{
32 const Def* dom() const { return op(0); }
33 const Def* codom() const { return op(1); }
34 MIM_PROJ(dom, const)
35 MIM_PROJ(codom, const)
36 ///@}
37
38 /// @name Continuations
39 /// @anchor continuations
40 /// Checks certain properties of @p d regarding continuations.
41 ///@{
42 // clang-format off
43 /// Is this a continuation - i.e. is the Pi::codom mim::Bot%tom?
44 static const Pi* isa_cn(const Def* d) { return d->isa<Pi>() && d->as<Pi>()->codom()->node() == Node::Bot ? d->as<Pi>() : nullptr; }
45 /// Is this a continuation (Pi::isa_cn) which has a Pi::ret_pi?
46 static const Pi* isa_returning(const Def* d) { return isa_cn(d) && d->as<Pi>()->ret_pi() ? d->as<Pi>() : nullptr; }
47 /// Is this a continuation (Pi::isa_cn) that is **not** Pi::isa_returning?
48 static const Pi* isa_basicblock(const Def* d) { return isa_cn(d) && !d->as<Pi>()->ret_pi() ? d->as<Pi>() : nullptr; }
49 // clang-format on
50 /// Is @p d an Pi::is_implicit (mutable) Pi?
51 static Pi* isa_implicit(const Def* d) {
52 if (auto pi = d->isa_mut<Pi>(); pi && pi->is_implicit()) return pi;
53 return nullptr;
54 }
55 /// Yields the Pi::ret_pi() of @p d, if it is in fact a Pi.
56 static const Pi* has_ret_pi(const Def* d) { return d->isa<Pi>() ? d->as<Pi>()->ret_pi() : nullptr; }
57 ///@}
58
59 /// @name Return Continuation
60 /// @anchor return_continuation
61 ///@{
62
63 /// Yields the last Pi::dom, if Pi::isa_basicblock.
64 const Pi* ret_pi() const;
65 /// Pi::dom%ain of Pi::ret_pi.
66 const Def* ret_dom() const { return ret_pi()->dom(); }
67 ///@}
68
69 /// @name Setters
70 /// @see @ref set_ops "Setting Ops"
71 ///@{
72 using Setters<Pi>::set;
73 Pi* set(const Def* dom, const Def* codom) { return set_dom(dom)->set_codom(codom); }
74 Pi* set_dom(const Def* dom) { return Def::set(0, dom)->as<Pi>(); }
75 Pi* set_dom(Defs doms);
76 Pi* set_codom(const Def* codom) { return Def::set(1, codom)->as<Pi>(); }
77 Pi* unset() { return Def::unset()->as<Pi>(); }
78 ///@}
79
80 /// @name Type Checking
81 ///@{
82 const Def* check(size_t, const Def*) override;
83 const Def* check() override;
84 static const Def* infer(const Def* dom, const Def* codom);
85 ///@}
86
87 /// @name Rebuild
88 ///@{
89 Pi* stub(const Def* type) { return stub_(world(), type)->set(dbg()); }
90 const Pi* immutabilize() override;
91 const Def* reduce(const Def* arg) const { return Def::reduce(arg).front(); }
92 constexpr size_t reduction_offset() const noexcept override { return 1; }
93 ///@}
94
95 static constexpr auto Node = mim::Node::Pi;
96
97private:
98 const Def* rebuild_(World&, const Def*, Defs) const override;
99 Pi* stub_(World&, const Def*) override;
100
101 friend class World;
102};
103
104/// A function.
105/// @see Pi
106class Lam : public Def, public Setters<Lam> {
107private:
108 Lam(const Pi* pi, const Def* filter, const Def* body)
109 : Def(Node, pi, {filter, body}, 0) {}
110 Lam(const Pi* pi)
111 : Def(Node, pi, 2, 0) {}
112
113public:
114 using Filter = std::variant<bool, const Def*>;
115
116 /// @name ops
117 ///@{
118 const Def* filter() const { return op(0); }
119 const Def* body() const { return op(1); }
120 ///@}
121
122 /// @name type
123 /// @anchor lam_dom
124 /// @see @ref proj
125 ///@{
126 const Pi* type() const { return Def::type()->as<Pi>(); }
127 const Def* dom() const { return type()->dom(); }
128 const Def* codom() const { return type()->codom(); }
129 MIM_PROJ(dom, const)
130 MIM_PROJ(codom, const)
131 ///@}
132
133 /// @name Continuations
134 /// @see @ref continuations "Pi: Continuations"
135 ///@{
136 // clang-format off
137 static const Lam* isa_cn(const Def* d) { return Pi::isa_cn(d->type()) ? d->isa<Lam>() : nullptr; }
138 static const Lam* isa_basicblock(const Def* d) { return Pi::isa_basicblock(d->type()) ? d->isa<Lam>() : nullptr; }
139 static const Lam* isa_returning(const Def* d) { return Pi::isa_returning (d->type()) ? d->isa<Lam>() : nullptr; }
140 static Lam* isa_mut_cn(const Def* d) { return isa_cn(d) ? d->isa_mut<Lam>() : nullptr; } ///< Only for mutables.
141 static Lam* isa_mut_basicblock(const Def* d) { return isa_basicblock(d) ? d->isa_mut<Lam>(): nullptr; } ///< Only for mutables.
142 static Lam* isa_mut_returning(const Def* d) { return isa_returning (d) ? d->isa_mut<Lam>(): nullptr; } ///< Only for mutables.
143 // clang-format on
144 ///@}
145
146 /// @name Return Continuation
147 /// @see @ref return_continuation "Pi: Return Continuation"
148 ///@{
149 const Pi* ret_pi() const { return type()->ret_pi(); }
150 const Def* ret_dom() const { return ret_pi()->dom(); }
151 /// Yields the Lam::var of the Lam::ret_pi.
152 const Def* ret_var() { return type()->ret_pi() ? var(num_vars() - 1) : nullptr; }
153 ///@}
154
155 /// @name Setters
156 /// Lam::Filter is a `std::variant<bool, const Def*>` that lets you set the Lam::filter() like this:
157 /// ```cpp
158 /// lam1->app(true, f, arg);
159 /// lam2->app(my_filter_def, f, arg);
160 /// ```
161 /// @note The filter belongs to the *Lam%bda* and **not** the body.
162 /// @see @ref set_ops "Setting Ops"
163 ///@{
164 using Setters<Lam>::set;
165 Lam* set(Filter filter, const Def* body) { return set_filter(filter)->set_body(body); }
166 Lam* set_filter(Filter); ///< Set filter first.
167 Lam* set_body(const Def* body) { return Def::set(1, body)->as<Lam>(); } ///< Set body second.
168 /// Set body to an App of @p callee and @p arg.
169 Lam* app(Filter filter, const Def* callee, const Def* arg);
170 /// Set body to an App of @p callee and @p args.
171 Lam* app(Filter filter, const Def* callee, Defs args);
172 /// Set body to an App of `(f, t)#cond mem` or `(f, t)#cond ()` if @p mem is `nullptr`.
173 Lam* branch(Filter filter, const Def* cond, const Def* t, const Def* f, const Def* mem = nullptr);
174 Lam* set(Defs ops) { return Def::set(ops)->as<Lam>(); }
175 Lam* unset() { return Def::unset()->as<Lam>(); }
176 ///@}
177
178 /// @name Rebuild
179 ///@{
180 Lam* stub(const Def* type) { return stub_(world(), type)->set(dbg()); }
181 const Def* reduce_body(const Def* arg) const { return reduce(arg).back(); }
182 constexpr size_t reduction_offset() const noexcept override { return 0; }
183 ///@}
184
185 /// @name Type Checking
186 ///@{
187 const Def* check(size_t, const Def*) override;
188 ///@}
189
190 static constexpr auto Node = mim::Node::Lam;
191
192private:
193 const Def* rebuild_(World&, const Def*, Defs) const override;
194 Lam* stub_(World&, const Def*) override;
195
196 friend class World;
197};
198
199/// @name Lam
200/// GIDSet / GIDMap keyed by Lam::gid of `Lam*`.
201///@{
202template<class To> using LamMap = GIDMap<Lam*, To>;
205///@}
206
207class App : public Def, public Setters<App> {
208private:
209 App(const Axm* axm, u8 curry, u8 trip, const Def* type, const Def* callee, const Def* arg)
210 : Def(Node, type, {callee, arg}, 0) {
211 axm_ = axm;
212 curry_ = curry;
213 trip_ = trip;
214 }
215
216public:
217 using Setters<App>::set;
218
219 /// @name callee
220 ///@{
221 const Def* callee() const { return op(0); }
222 const App* decurry() const { return callee()->as<App>(); } ///< Returns App::callee again as App.
223 const Pi* callee_type() const { return callee()->type()->as<Pi>(); }
224 ///@}
225
226 /// @name arg
227 /// @anchor app_arg
228 /// @see @ref proj
229 ///@{
230 const Def* arg() const { return op(1); }
231 MIM_PROJ(arg, const)
232 ///@}
233
234 /// @name Get axm, current curry counter and trip count
235 ///@{
236 const Axm* axm() const { return axm_; }
237 u8 curry() const { return curry_; }
238 u8 trip() const { return trip_; }
239 ///@}
240
241 static constexpr auto Node = mim::Node::App;
242
243private:
244 const Def* rebuild_(World&, const Def*, Defs) const override;
245
246 friend class World;
247};
248
249/// @name Helpers to work with Functions
250///@{
251inline const App* isa_callee(const Def* def, size_t i) { return i == 0 ? def->isa<App>() : nullptr; }
252
253/// These are Lam%s that are neither `nullptr`, nor Lam::is_external, nor Lam::is_unset.
254inline Lam* isa_workable(Lam* lam) {
255 if (!lam || lam->is_external() || !lam->is_set()) return nullptr;
256 return lam;
257}
258
259inline std::pair<const App*, Lam*> isa_apped_mut_lam(const Def* def) {
260 if (auto app = def->isa<App>()) return {app, app->callee()->isa_mut<Lam>()};
261 return {nullptr, nullptr};
262}
263
264/// Yields curried App%s in a flat `std::deque<const App*>`.
265std::deque<const App*> decurry(const Def*);
266
267/// The high level view is:
268/// ```
269/// f: B -> C
270/// g: A -> B
271/// f o g := λ x. f(g(x)) : A -> C
272/// ```
273/// In CPS the types look like:
274/// ```
275/// f: Cn[B, Cn C]
276/// g: Cn[A, Cn B]
277/// h = f o g
278/// h: Cn[A, cn C]
279/// h = λ (a ret_h) = g (a, h')
280/// h': Cn B
281/// h'= λ b = f (b, ret_h)
282/// ```
283const Def* compose_cn(const Def* f, const Def* g);
284
285/// Helper function to cope with the fact that normalizers take all arguments and not only its axm arguments.
286std::pair<const Def*, DefVec> collect_args(const Def* def);
287///@}
288
289} // namespace mim
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:115
const Axm * axm() const
Definition lam.h:236
const Pi * callee_type() const
Definition lam.h:223
u8 curry() const
Definition lam.h:237
const App * decurry() const
Returns App::callee again as App.
Definition lam.h:222
static constexpr auto Node
Definition lam.h:241
friend class World
Definition lam.h:246
const Def * callee() const
Definition lam.h:221
const Def * arg() const
Definition lam.h:230
u8 trip() const
Definition lam.h:238
Definition axm.h:9
Base class for all Defs.
Definition def.h:197
bool is_set() const
Yields true if empty or the last op is set.
Definition def.cpp:278
constexpr Node node() const noexcept
Definition def.h:220
Def * set(size_t i, const Def *)
Successively set from left to right.
Definition def.cpp:240
u8 trip_
Definition def.h:574
World & world() const noexcept
Definition def.cpp:387
virtual const Def * check()
Definition def.h:517
constexpr auto ops() const noexcept
Definition def.h:260
constexpr flags_t flags() const noexcept
Definition def.h:215
u8 curry_
Definition def.h:573
const Def * op(size_t i) const noexcept
Definition def.h:263
bool is_external() const
Definition def.h:413
nat_t num_vars() noexcept
Definition def.h:378
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.h:241
const Def * var()
Not necessarily a Var: E.g., if the return type is [], this will yield ().
Definition def.cpp:449
flags_t flags_
Definition def.h:572
Def * unset()
Unsets all Def::ops; works even, if not set at all or partially.
Definition def.cpp:256
constexpr auto reduce(const Def *arg) const noexcept
Definition def.h:505
Dbg dbg() const
Definition def.h:448
A function.
Definition lam.h:106
std::variant< bool, const Def * > Filter
Definition lam.h:114
Lam * unset()
Definition lam.h:175
const Def * filter() const
Definition lam.h:118
static const Lam * isa_cn(const Def *d)
Definition lam.h:137
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:32
Lam * stub_(World &, const Def *) override
Definition def.cpp:152
Lam * set(Filter filter, const Def *body)
Definition lam.h:165
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:141
static const Lam * isa_returning(const Def *d)
Definition lam.h:139
const Pi * ret_pi() const
Definition lam.h:149
const Def * dom() const
Definition lam.h:127
static Lam * isa_mut_returning(const Def *d)
Only for mutables.
Definition lam.h:142
const Pi * type() const
Definition lam.h:126
Lam * set(Defs ops)
Definition lam.h:174
static constexpr auto Node
Definition lam.h:190
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:120
friend class World
Definition lam.h:196
static const Lam * isa_basicblock(const Def *d)
Definition lam.h:138
Lam * app(Filter filter, const Def *callee, const Def *arg)
Set body to an App of callee and arg.
Definition lam.cpp:29
const Def * ret_dom() const
Definition lam.h:150
Lam * set_body(const Def *body)
Set body second.
Definition lam.h:167
Lam * stub(const Def *type)
Definition lam.h:180
const Def * body() const
Definition lam.h:119
static Lam * isa_mut_cn(const Def *d)
Only for mutables.
Definition lam.h:140
constexpr size_t reduction_offset() const noexcept override
First Def::op that needs to be dealt with during reduction; e.g.
Definition lam.h:182
const Def * reduce_body(const Def *arg) const
Definition lam.h:181
const Def * ret_var()
Yields the Lam::var of the Lam::ret_pi.
Definition lam.h:152
const Def * codom() const
Definition lam.h:128
A dependent function type.
Definition lam.h:11
const Def * ret_dom() const
Pi::domain of Pi::ret_pi.
Definition lam.h:66
Pi * stub_(World &, const Def *) override
Definition def.cpp:154
Pi(const Def *type, bool implicit)
Constructor for a mutable Pi.
Definition lam.h:17
Pi * unset()
Definition lam.h:77
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:56
constexpr size_t reduction_offset() const noexcept override
First Def::op that needs to be dealt with during reduction; e.g.
Definition lam.h:92
Pi * set_codom(const Def *codom)
Definition lam.h:76
Pi * make_implicit()
Definition lam.h:24
Pi(const Def *type, const Def *dom, const Def *codom, bool implicit)
Constructor for an immutable Pi.
Definition lam.h:14
static const Pi * isa_cn(const Def *d)
Is this a continuation - i.e. is the Pi::codom mim::Bottom?
Definition lam.h:44
static const Pi * isa_basicblock(const Def *d)
Is this a continuation (Pi::isa_cn) that is not Pi::isa_returning?
Definition lam.h:48
static const Def * infer(const Def *dom, const Def *codom)
Definition check.cpp:292
bool is_implicit() const
Definition lam.h:23
Pi * make_explicit()
Definition lam.h:25
const Def * dom() const
Definition lam.h:32
friend class World
Definition lam.h:101
const Def * codom() const
Definition lam.h:33
static Pi * isa_implicit(const Def *d)
Is d an Pi::is_implicit (mutable) Pi?
Definition lam.h:51
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:124
const Def * check() override
Definition check.cpp:299
Pi * set(const Def *dom, const Def *codom)
Definition lam.h:73
static constexpr auto Node
Definition lam.h:95
const Def * reduce(const Def *arg) const
Definition lam.h:91
const Pi * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:186
Pi * stub(const Def *type)
Definition lam.h:89
const Pi * ret_pi() const
Yields the last Pi::dom, if Pi::isa_basicblock.
Definition lam.cpp:13
Pi * set_dom(const Def *dom)
Definition lam.h:74
static const Pi * isa_returning(const Def *d)
Is this a continuation (Pi::isa_cn) which has a Pi::ret_pi?
Definition lam.h:46
CRTP-based Mixin to declare setters for Def::loc & Def::name using a covariant return type.
Definition def.h:142
#define MIM_PROJ(NAME, CONST)
Use as mixin to wrap all kind of Def::proj and Def::projs variants.
Definition def.h:126
Definition ast.h:14
View< const Def * > Defs
Definition def.h:48
std::pair< const Def *, DefVec > collect_args(const Def *def)
Helper function to cope with the fact that normalizers take all arguments and not only its axm argume...
Definition lam.cpp:82
GIDSet< Lam * > LamSet
Definition lam.h:203
u64 flags_t
Definition types.h:45
std::pair< const App *, Lam * > isa_apped_mut_lam(const Def *def)
Definition lam.h:259
absl::flat_hash_map< K, V, GIDHash< K > > GIDMap
Definition util.h:176
LamMap< Lam * > Lam2Lam
Definition lam.h:204
GIDMap< Lam *, To > LamMap
Definition lam.h:202
Lam * isa_workable(Lam *lam)
These are Lams that are neither nullptr, nor Lam::is_external, nor Lam::is_unset.
Definition lam.h:254
std::deque< const App * > decurry(const Def *)
Yields curried Apps in a flat std::deque<const App*>.
Definition lam.cpp:40
const App * isa_callee(const Def *def, size_t i)
Definition lam.h:251
const Def * compose_cn(const Def *f, const Def *g)
The high level view is:
Definition lam.cpp:49
absl::flat_hash_set< K, GIDHash< K > > GIDSet
Definition util.h:177
uint8_t u8
Definition types.h:34
@ Pi
Definition def.h:84
@ Bot
Definition def.h:84
@ Lam
Definition def.h:84
@ App
Definition def.h:84