MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
tuple.h
Go to the documentation of this file.
1#pragma once
2
3#include <span>
4
5#include "mim/def.h"
6
7namespace mim {
8
9/// Base class for Sigma and Tuple.
10class Prod : public Def, public Setters<Prod> {
11protected:
12 using Def::Def;
13
14public:
15 static constexpr size_t Num_Ops = std::dynamic_extent;
16};
17
18/// A [dependent tuple type](https://en.wikipedia.org/wiki/Dependent_type#%CE%A3_type).
19/// @see Tuple, Arr, Pack, Prod
20class Sigma : public Prod, public Setters<Sigma> {
21private:
22 Sigma(const Def* type, Defs ops)
23 : Prod(Node, type, ops, 0) {} ///< Constructor for an *immutable* Sigma.
24 Sigma(const Def* type, size_t size)
25 : Prod(Node, type, size, 0) {} ///< Constructor for a *mutable* Sigma.
26
27public:
28 /// @name Setters
29 /// @see @ref set_ops "Setting Ops"
30 ///@{
31 using Setters<Sigma>::set;
32 Sigma* set(size_t i, const Def* def) { return Def::set(i, def)->as<Sigma>(); }
33 Sigma* set(Defs ops) { return Def::set(ops)->as<Sigma>(); }
34 Sigma* unset() { return Def::unset()->as<Sigma>(); }
35 ///@}
36
37 /// @name Rebuild
38 ///@{
39 const Def* immutabilize() final;
40 Sigma* stub(const Def* type) { return stub_(world(), type)->set(dbg()); }
41
42 /// @note Technically, it would make sense to have an offset of 1 as the first element can't be reduced.
43 /// For example, in `[n: Nat, F n]` `n` only occurs free in the second element.
44 /// However, this would cause a lot of confusion and special code to cope with the first element,
45 /// So we just keep it.
46 constexpr size_t reduction_offset() const noexcept final { return 0; }
47 ///@}
48
49 /// @name Type Checking
50 ///@{
51 const Def* check(size_t, const Def*) final;
52 const Def* check() final;
53 static const Def* infer(World&, Defs);
54 const Def* arity() const final;
55 ///@}
56
57 static constexpr auto Node = mim::Node::Sigma;
58
59private:
60 const Def* rebuild_(World&, const Def*, Defs) const final;
61 Sigma* stub_(World&, const Def*) final;
62
63 friend class World;
64};
65
66/// Data constructor for a Sigma.
67/// @see Sigma, Arr, Pack, Prod
68class Tuple : public Prod, public Setters<Tuple> {
69public:
70 using Setters<Tuple>::set;
71 static const Def* infer(World&, Defs);
72 static constexpr auto Node = mim::Node::Tuple;
73
74private:
75 Tuple(const Def* type, Defs args)
76 : Prod(Node, type, args, 0) {}
77
78 const Def* rebuild_(World&, const Def*, Defs) const final;
79
80 friend class World;
81};
82
83/// Base class for Arr and Pack.
84class Seq : public Def, public Setters<Seq> {
85protected:
86 using Def::Def;
87
88public:
89 /// @name ops
90 ///@{
91 const Def* body() const { return ops().back(); }
92 ///@}
93
94 /// @name Setters
95 /// @see @ref set_ops "Setting Ops"
96 ///@{
97 using Setters<Seq>::set;
98
99 /// Common setter for Pack%s and Arr%ays.
100 /// @p arity will be ignored, if it's a Pack.
101 Seq* set(const Def* arity, const Def* body) {
102 return (node() == Node::Arr ? Def::set({arity, body}) : Def::set({body}))->as<Seq>();
103 }
104 Seq* unset() { return Def::unset()->as<Seq>(); }
105 ///@}
106
107 /// @name Rebuild
108 ///@{
109 Seq* stub(World& w, const Def* type) { return Def::stub(w, type)->as<Seq>(); }
110 virtual const Def* reduce(const Def* arg) const = 0;
111 ///@}
112};
113
114/// A (possibly paramterized) Arr%ay.
115/// Arr%ays are usually homogenous but they can be *inhomogenous* as well: `«i: N; T#i»`
116/// @see Sigma, Tuple, Pack
117class Arr : public Seq, public Setters<Arr> {
118private:
119 Arr(const Def* type, const Def* arity, const Def* body)
120 : Seq(Node, type, {arity, body}, 0) {} ///< Constructor for an *immutable* Arr.
121 Arr(const Def* type)
122 : Seq(Node, type, 2, 0) {} ///< Constructor for a *mutable* Arr.
123
124public:
125 /// @name ops
126 ///@{
127 const Def* arity() const final { return op(0); }
128 ///@}
129
130 /// @name Setters
131 /// @see @ref set_ops "Setting Ops"
132 ///@{
133 using Setters<Arr>::set;
134 Arr* set_arity(const Def* arity) { return Def::set(0, arity)->as<Arr>(); }
135 Arr* set_body(const Def* body) { return Def::set(1, body)->as<Arr>(); }
136 Arr* set(const Def* arity, const Def* body) { return set_arity(arity)->set_body(body); }
137 Arr* unset() { return Def::unset()->as<Arr>(); }
138 ///@}
139
140 /// @name Rebuild
141 ///@{
142 Arr* stub(const Def* type) { return stub_(world(), type)->set(dbg()); }
143 const Def* immutabilize() final;
144 const Def* reduce(const Def* arg) const final { return Def::reduce(arg).front(); }
145 constexpr size_t reduction_offset() const noexcept final { return 1; }
146 ///@}
147
148 /// @name Type Checking
149 ///@{
150 const Def* check(size_t, const Def*) final;
151 const Def* check() final;
152 ///@}
153
154 static constexpr auto Node = mim::Node::Arr;
155 static constexpr size_t Num_Ops = 2;
156
157private:
158 const Def* rebuild_(World&, const Def*, Defs) const final;
159 Arr* stub_(World&, const Def*) final;
160
161 friend class World;
162};
163
164/// A (possibly paramterized) Tuple.
165/// @see Sigma, Tuple, Arr
166class Pack : public Seq, public Setters<Pack> {
167private:
168 Pack(const Def* type, const Def* body)
169 : Seq(Node, type, {body}, 0) {} ///< Constructor for an *immutable* Pack.
170 Pack(const Def* type)
171 : Seq(Node, type, 1, 0) {} ///< Constructor for a *mutable* Pack.
172
173public:
174 /// @name ops
175 ///@{
176 const Def* arity() const final;
177 ///@}
178
179 /// @name Setters
180 /// @see @ref set_ops "Setting Ops"
181 ///@{
182 using Setters<Pack>::set;
183 Pack* set(const Def* body) { return Def::set({body})->as<Pack>(); }
184 Pack* unset() { return Def::unset()->as<Pack>(); }
185 ///@}
186
187 /// @name Rebuild
188 ///@{
189 Pack* stub(const Def* type) { return stub_(world(), type)->set(dbg()); }
190 const Def* immutabilize() final;
191 const Def* reduce(const Def* arg) const final { return Def::reduce(arg).front(); }
192 constexpr size_t reduction_offset() const noexcept final { return 0; }
193 ///@}
194
195 static constexpr auto Node = mim::Node::Pack;
196 static constexpr size_t Num_Ops = 1;
197
198private:
199 const Def* rebuild_(World&, const Def*, Defs) const final;
200 Pack* stub_(World&, const Def*) final;
201
202 friend class World;
203};
204
205/// Extracts from a Sigma or Arr%ay-typed Extract::tuple the element at position Extract::index.
206class Extract : public Def, public Setters<Extract> {
207private:
208 Extract(const Def* type, const Def* tuple, const Def* index)
209 : Def(Node, type, {tuple, index}, 0) {}
210
211public:
212 using Setters<Extract>::set;
213
214 /// @name ops
215 ///@{
216 const Def* tuple() const { return op(0); }
217 const Def* index() const { return op(1); }
218 ///@}
219
220 static constexpr auto Node = mim::Node::Extract;
221 static constexpr size_t Num_Ops = 2;
222
223private:
224 const Def* rebuild_(World&, const Def*, Defs) const final;
225
226 friend class World;
227};
228
229/// Creates a new Tuple / Pack by inserting Insert::value at position Insert::index into Insert::tuple.
230/// @attention This is a *functional* Insert.
231/// The Insert::tuple itself remains untouched.
232/// The Insert itself is a *new* Tuple / Pack which contains the inserted Insert::value.
233class Insert : public Def, public Setters<Insert> {
234private:
235 Insert(const Def* tuple, const Def* index, const Def* value)
236 : Def(Node, tuple->type(), {tuple, index, value}, 0) {}
237
238public:
239 using Setters<Insert>::set;
240
241 /// @name ops
242 ///@{
243 const Def* tuple() const { return op(0); }
244 const Def* index() const { return op(1); }
245 const Def* value() const { return op(2); }
246 ///@}
247
248 static constexpr auto Node = mim::Node::Insert;
249 static constexpr size_t Num_Ops = 3;
250
251private:
252 const Def* rebuild_(World&, const Def*, Defs) const final;
253
254 friend class World;
255};
256
257/// Matches `(ff, tt)#cond` - where `cond` is not a Lit%eral.
258/// @note If `cond` is a Lit%eral, either
259/// * `(x, y)#lit` would have been folded to `x`/`y` anymway, or
260/// * Select::pair() yields again `pair#lit` for `pair#lit`.
261class Select {
262public:
263 Select(const Def*);
264
265 explicit operator bool() const noexcept { return tt_; }
266
267 const Extract* extract() const { return extract_; }
268 const Def* pair() const { return pair_; }
269 const Def* cond() const { return cond_; }
270 const Def* tt() const { return tt_; }
271 const Def* ff() const { return ff_; }
272
273private:
274 const Extract* extract_ = nullptr;
275 const Def* pair_ = nullptr;
276 const Def* cond_ = nullptr;
277 const Def* tt_ = nullptr;
278 const Def* ff_ = nullptr;
279};
280
281/// Matches `(ff, tt)#cond arg`.
282/// `(ff, tt)#cond` is matched as a Select.
283class Branch : public Select {
284public:
285 Branch(const Def*);
286
287 const App* app() const { return app_; }
288 const Def* callee() const { return callee_; }
289 const Def* arg() const { return arg_; }
290
291private:
292 const App* app_ = nullptr;
293 const Def* callee_ = nullptr;
294 const Def* arg_ = nullptr;
295};
296
297/// @name Helpers to work with Tulpes/Sigmas/Arrays/Packs
298///@{
299bool is_unit(const Def*);
300std::string tuple2str(const Def*);
301
302/// Flattens a sigma/array/pack/tuple.
303const Def* flatten(const Def* def);
304/// Same as unflatten, but uses the operands of a flattened Pack / Tuple directly.
305size_t flatten(DefVec& ops, const Def* def, bool flatten_sigmas = true);
306
307/// Applies the reverse transformation on a Pack / Tuple, given the original type.
308const Def* unflatten(const Def* def, const Def* type);
309/// Same as unflatten, but uses the operands of a flattened Pack / Tuple directly.
310const Def* unflatten(Defs ops, const Def* type, bool flatten_muts = true);
311
312DefVec merge(Defs, Defs);
313DefVec merge(const Def* def, Defs defs);
314const Def* merge_sigma(const Def* def, Defs defs);
315const Def* merge_tuple(const Def* def, Defs defs);
316
317const Def* tuple_of_types(const Def* t);
318///@}
319
320} // namespace mim
A (possibly paramterized) Array.
Definition tuple.h:117
const Def * arity() const final
Definition tuple.h:127
static constexpr auto Node
Definition tuple.h:154
Arr * unset()
Definition tuple.h:137
constexpr size_t reduction_offset() const noexcept final
First Def::op that needs to be dealt with during reduction; e.g.
Definition tuple.h:145
Arr * set(const Def *arity, const Def *body)
Definition tuple.h:136
static constexpr size_t Num_Ops
Definition tuple.h:155
Arr * set_body(const Def *body)
Definition tuple.h:135
const Def * reduce(const Def *arg) const final
Definition tuple.h:144
friend class World
Definition tuple.h:161
Arr * set_arity(const Def *arity)
Definition tuple.h:134
Arr * stub_(World &, const Def *) final
Definition def.cpp:151
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:116
Arr * stub(const Def *type)
Definition tuple.h:142
const App * app() const
Definition tuple.h:287
const Def * callee() const
Definition tuple.h:288
Branch(const Def *)
Definition tuple.cpp:67
const Def * arg() const
Definition tuple.h:289
Base class for all Defs.
Definition def.h:251
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
World & world() const noexcept
Definition def.cpp:436
constexpr auto ops() const noexcept
Definition def.h:305
const Def * op(size_t i) const noexcept
Definition def.h:308
friend class World
Definition def.h:683
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.h:295
virtual const Def * arity() const
Definition def.cpp:546
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
Def * stub(World &w, const Def *type)
Definition def.h:541
Extracts from a Sigma or Array-typed Extract::tuple the element at position Extract::index.
Definition tuple.h:206
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:117
const Def * tuple() const
Definition tuple.h:216
friend class World
Definition tuple.h:226
static constexpr size_t Num_Ops
Definition tuple.h:221
static constexpr auto Node
Definition tuple.h:220
const Def * index() const
Definition tuple.h:217
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:119
static constexpr auto Node
Definition tuple.h:248
const Def * tuple() const
Definition tuple.h:243
friend class World
Definition tuple.h:254
const Def * index() const
Definition tuple.h:244
static constexpr size_t Num_Ops
Definition tuple.h:249
const Def * value() const
Definition tuple.h:245
Pack * stub_(World &, const Def *) final
Definition def.cpp:155
const Def * arity() const final
Definition tuple.cpp:46
static constexpr size_t Num_Ops
Definition tuple.h:196
Pack * unset()
Definition tuple.h:184
friend class World
Definition tuple.h:202
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:123
const Def * reduce(const Def *arg) const final
Definition tuple.h:191
static constexpr auto Node
Definition tuple.h:195
Pack * set(const Def *body)
Definition tuple.h:183
Pack * stub(const Def *type)
Definition tuple.h:189
constexpr size_t reduction_offset() const noexcept final
First Def::op that needs to be dealt with during reduction; e.g.
Definition tuple.h:192
Base class for Sigma and Tuple.
Definition tuple.h:10
static constexpr size_t Num_Ops
Definition tuple.h:15
Def(World *, Node, const Def *type, Defs ops, flags_t flags)
Constructor for an immutable Def.
Definition def.cpp:24
const Def * cond() const
Definition tuple.h:269
const Def * pair() const
Definition tuple.h:268
const Def * tt() const
Definition tuple.h:270
const Def * ff() const
Definition tuple.h:271
const Extract * extract() const
Definition tuple.h:267
Select(const Def *)
Definition tuple.cpp:52
Base class for Arr and Pack.
Definition tuple.h:84
Seq * set(const Def *arity, const Def *body)
Common setter for Packs and Arrays.
Definition tuple.h:101
virtual const Def * reduce(const Def *arg) const =0
const Def * body() const
Definition tuple.h:91
Seq * unset()
Definition tuple.h:104
Seq * stub(World &w, const Def *type)
Definition tuple.h:109
Def(World *, Node, const Def *type, Defs ops, flags_t flags)
Constructor for an immutable Def.
Definition def.cpp:24
CRTP-based mixin to declare setters for Def::loc & Def::name using a covariant return type.
Definition def.h:195
const Tuple * set(Loc l) const
Definition def.h:202
Sigma * unset()
Definition tuple.h:34
Sigma * stub(const Def *type)
Definition tuple.h:40
const Def * rebuild_(World &, const Def *, Defs) const final
Definition def.cpp:128
Sigma * set(Defs ops)
Definition tuple.h:33
constexpr size_t reduction_offset() const noexcept final
Definition tuple.h:46
friend class World
Definition tuple.h:63
const Def * immutabilize() final
Tries to make an immutable from a mutable.
Definition def.cpp:198
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:348
Sigma * stub_(World &, const Def *) final
Definition def.cpp:158
static const Def * infer(World &, Defs)
Definition check.cpp:339
static constexpr auto Node
Definition tuple.h:57
const Def * arity() const final
Definition tuple.cpp:40
Sigma * set(size_t i, const Def *def)
Definition tuple.h:32
friend class World
Definition tuple.h:80
static constexpr auto Node
Definition tuple.h:72
The World represents the whole program and manages creation of MimIR nodes (Defs).
Definition world.h:36
Definition ast.h:14
View< const Def * > Defs
Definition def.h:76
@ Arr
Definition def.h:114
@ Pack
Definition def.h:114
@ Sigma
Definition def.h:114
@ Extract
Definition def.h:114
@ Insert
Definition def.h:114
@ Tuple
Definition def.h:114