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