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 "mim/def.h"
4
5namespace mim {
6
7/// A [dependent tuple type](https://en.wikipedia.org/wiki/Dependent_type#%CE%A3_type).
8/// @see Tuple, Arr, Pack
9class Sigma : public Def, public Setters<Sigma> {
10private:
11 Sigma(const Def* type, Defs ops)
12 : Def(Node, type, ops, 0) {} ///< Constructor for an *immutable* Sigma.
13 Sigma(const Def* type, size_t size)
14 : Def(Node, type, size, 0) {} ///< Constructor for a *mutable* Sigma.
15
16public:
17 /// @name Setters
18 /// @see @ref set_ops "Setting Ops"
19 ///@{
20 using Setters<Sigma>::set;
21 Sigma* set(size_t i, const Def* def) { return Def::set(i, def)->as<Sigma>(); }
22 Sigma* set(Defs ops) { return Def::set(ops)->as<Sigma>(); }
23 Sigma* unset() { return Def::unset()->as<Sigma>(); }
24 ///@}
25
26 /// @name Rebuild
27 ///@{
28 const Def* immutabilize() override;
29 Sigma* stub(const Def* type) { return stub_(world(), type)->set(dbg()); }
30
31 /// @note Technically, it would make sense to have an offset of 1 as the first element can't be reduced.
32 /// For example, in `[n: Nat, F n]` `n` only occurs free in the second element.
33 /// However, this would cause a lot of confusion and special code to cope with the first element,
34 /// So we just keep it.
35 constexpr size_t reduction_offset() const noexcept override { return 0; }
36 ///@}
37
38 /// @name Type Checking
39 ///@{
40 const Def* check(size_t, const Def*) override;
41 const Def* check() override;
42 static const Def* infer(World&, Defs);
43 ///@}
44
45 static constexpr auto Node = mim::Node::Sigma;
46
47private:
48 const Def* rebuild_(World&, const Def*, Defs) const override;
49 Sigma* stub_(World&, const Def*) override;
50
51 friend class World;
52};
53
54/// Data constructor for a Sigma.
55/// @see Sigma, Arr, Pack
56class Tuple : public Def, public Setters<Tuple> {
57public:
58 using Setters<Tuple>::set;
59 static const Def* infer(World&, Defs);
60 static constexpr auto Node = mim::Node::Tuple;
61
62private:
63 Tuple(const Def* type, Defs args)
64 : Def(Node, type, args, 0) {}
65
66 const Def* rebuild_(World&, const Def*, Defs) const override;
67
68 friend class World;
69};
70
71/// A (possibly paramterized) Arr%ay.
72/// Arr%ays are usually homogenous but they can be *inhomogenous* as well: `«i: N; T#i»`
73/// @see Sigma, Tuple, Pack
74class Arr : public Def, public Setters<Arr> {
75private:
76 Arr(const Def* type, const Def* shape, const Def* body)
77 : Def(Node, type, {shape, body}, 0) {} ///< Constructor for an *immutable* Arr.
78 Arr(const Def* type)
79 : Def(Node, type, 2, 0) {} ///< Constructor for a *mutable* Arr.
80
81public:
82 /// @name ops
83 ///@{
84 const Def* shape() const { return op(0); }
85 const Def* body() const { return op(1); }
86 ///@}
87
88 /// @name Setters
89 /// @see @ref set_ops "Setting Ops"
90 ///@{
91 using Setters<Arr>::set;
92 Arr* set_shape(const Def* shape) { return Def::set(0, shape)->as<Arr>(); }
93 Arr* set_body(const Def* body) { return Def::set(1, body)->as<Arr>(); }
94 Arr* unset() { return Def::unset()->as<Arr>(); }
95 ///@}
96
97 /// @name Rebuild
98 ///@{
99 Arr* stub(const Def* type) { return stub_(world(), type)->set(dbg()); }
100 const Def* immutabilize() override;
101 const Def* reduce(const Def* arg) const { return Def::reduce(arg).front(); }
102 constexpr size_t reduction_offset() const noexcept override { return 1; }
103 ///@}
104
105 /// @name Type Checking
106 ///@{
107 const Def* check(size_t, const Def*) override;
108 const Def* check() override;
109 ///@}
110
111 static constexpr auto Node = mim::Node::Arr;
112
113private:
114 const Def* rebuild_(World&, const Def*, Defs) const override;
115 Arr* stub_(World&, const Def*) override;
116
117 friend class World;
118};
119
120/// A (possibly paramterized) Tuple.
121/// @see Sigma, Tuple, Arr
122class Pack : public Def, public Setters<Pack> {
123private:
124 Pack(const Def* type, const Def* body)
125 : Def(Node, type, {body}, 0) {} ///< Constructor for an *immutable* Pack.
126 Pack(const Def* type)
127 : Def(Node, type, 1, 0) {} ///< Constructor for a *mutable* Pack.
128
129public:
130 /// @name ops
131 ///@{
132 const Def* body() const { return op(0); }
133 const Def* shape() const;
134 ///@}
135
136 /// @name Setters
137 /// @see @ref set_ops "Setting Ops"
138 ///@{
139 using Setters<Pack>::set;
140 Pack* set(const Def* body) { return Def::set(0, body)->as<Pack>(); }
141 Pack* reset(const Def* body) { return unset()->set(body); }
142 Pack* unset() { return Def::unset()->as<Pack>(); }
143 ///@}
144
145 /// @name Rebuild
146 ///@{
147 Pack* stub(const Def* type) { return stub_(world(), type)->set(dbg()); }
148 const Def* immutabilize() override;
149 const Def* reduce(const Def* arg) const { return Def::reduce(arg).front(); }
150 constexpr size_t reduction_offset() const noexcept override { return 0; }
151 ///@}
152
153 static constexpr auto Node = mim::Node::Pack;
154
155private:
156 const Def* rebuild_(World&, const Def*, Defs) const override;
157 Pack* stub_(World&, const Def*) override;
158
159 friend class World;
160};
161
162/// Extracts from a Sigma or Arr%ay-typed Extract::tuple the element at position Extract::index.
163class Extract : public Def, public Setters<Extract> {
164private:
165 Extract(const Def* type, const Def* tuple, const Def* index)
166 : Def(Node, type, {tuple, index}, 0) {}
167
168public:
169 using Setters<Extract>::set;
170
171 /// @name ops
172 ///@{
173 const Def* tuple() const { return op(0); }
174 const Def* index() const { return op(1); }
175 ///@}
176
177 static constexpr auto Node = mim::Node::Extract;
178
179private:
180 const Def* rebuild_(World&, const Def*, Defs) const override;
181
182 friend class World;
183};
184
185/// Creates a new Tuple / Pack by inserting Insert::value at position Insert::index into Insert::tuple.
186/// @attention This is a *functional* Insert.
187/// The Insert::tuple itself remains untouched.
188/// The Insert itself is a *new* Tuple / Pack which contains the inserted Insert::value.
189class Insert : public Def, public Setters<Insert> {
190private:
191 Insert(const Def* tuple, const Def* index, const Def* value)
192 : Def(Node, tuple->type(), {tuple, index, value}, 0) {}
193
194public:
195 using Setters<Insert>::set;
196
197 /// @name ops
198 ///@{
199 const Def* tuple() const { return op(0); }
200 const Def* index() const { return op(1); }
201 const Def* value() const { return op(2); }
202 ///@}
203
204 static constexpr auto Node = mim::Node::Insert;
205
206private:
207 const Def* rebuild_(World&, const Def*, Defs) const override;
208
209 friend class World;
210};
211
212/// @name Helpers to work with Tulpes/Sigmas/Arrays/Packs
213///@{
214bool is_unit(const Def*);
215std::string tuple2str(const Def*);
216
217/// Flattens a sigma/array/pack/tuple.
218const Def* flatten(const Def* def);
219/// Same as unflatten, but uses the operands of a flattened Pack / Tuple directly.
220size_t flatten(DefVec& ops, const Def* def, bool flatten_sigmas = true);
221
222/// Applies the reverse transformation on a Pack / Tuple, given the original type.
223const Def* unflatten(const Def* def, const Def* type);
224/// Same as unflatten, but uses the operands of a flattened Pack / Tuple directly.
225const Def* unflatten(Defs ops, const Def* type, bool flatten_muts = true);
226
228DefVec merge(const Def* def, Defs defs);
229const Def* merge_sigma(const Def* def, Defs defs);
230const Def* merge_tuple(const Def* def, Defs defs);
231
232const Def* tuple_of_types(const Def* t);
233///@}
234
235} // namespace mim
A (possibly paramterized) Array.
Definition tuple.h:74
const Def * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:196
const Def * body() const
Definition tuple.h:85
static constexpr auto Node
Definition tuple.h:111
Arr * unset()
Definition tuple.h:94
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:116
Arr * set_body(const Def *body)
Definition tuple.h:93
Arr * set_shape(const Def *shape)
Definition tuple.h:92
friend class World
Definition tuple.h:117
const Def * shape() const
Definition tuple.h:84
constexpr size_t reduction_offset() const noexcept override
First Def::op that needs to be dealt with during reduction; e.g.
Definition tuple.h:102
const Def * check() override
Definition check.cpp:254
Arr * stub_(World &, const Def *) override
Definition def.cpp:149
const Def * reduce(const Def *arg) const
Definition tuple.h:101
Arr * stub(const Def *type)
Definition tuple.h:99
Base class for all Defs.
Definition def.h:197
Def * set(size_t i, const Def *)
Successively set from left to right.
Definition def.cpp:240
World & world() const noexcept
Definition def.cpp:387
constexpr auto ops() const noexcept
Definition def.h:260
const Def * op(size_t i) const noexcept
Definition def.h:263
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.h:241
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
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:117
const Def * tuple() const
Definition tuple.h:173
friend class World
Definition tuple.h:182
static constexpr auto Node
Definition tuple.h:177
const Def * index() const
Definition tuple.h:174
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:119
static constexpr auto Node
Definition tuple.h:204
const Def * tuple() const
Definition tuple.h:199
friend class World
Definition tuple.h:209
const Def * index() const
Definition tuple.h:200
const Def * value() const
Definition tuple.h:201
A (possibly paramterized) Tuple.
Definition tuple.h:122
const Def * body() const
Definition tuple.h:132
Pack * reset(const Def *body)
Definition tuple.h:141
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:123
constexpr size_t reduction_offset() const noexcept override
First Def::op that needs to be dealt with during reduction; e.g.
Definition tuple.h:150
Pack * unset()
Definition tuple.h:142
const Def * shape() const
Definition tuple.cpp:40
friend class World
Definition tuple.h:159
const Def * reduce(const Def *arg) const
Definition tuple.h:149
const Def * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:206
static constexpr auto Node
Definition tuple.h:153
Pack * set(const Def *body)
Definition tuple.h:140
Pack * stub_(World &, const Def *) override
Definition def.cpp:153
Pack * stub(const Def *type)
Definition tuple.h:147
CRTP-based Mixin to declare setters for Def::loc & Def::name using a covariant return type.
Definition def.h:142
Sigma * unset()
Definition tuple.h:23
const Def * immutabilize() override
Tries to make an immutable from a mutable.
Definition def.cpp:191
Sigma * stub(const Def *type)
Definition tuple.h:29
constexpr size_t reduction_offset() const noexcept override
Definition tuple.h:35
Sigma * set(Defs ops)
Definition tuple.h:22
friend class World
Definition tuple.h:51
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:126
Sigma * stub_(World &, const Def *) override
Definition def.cpp:155
static const Def * infer(World &, Defs)
Definition check.cpp:267
const Def * check() override
Definition check.cpp:275
static constexpr auto Node
Definition tuple.h:45
Sigma * set(size_t i, const Def *def)
Definition tuple.h:21
friend class World
Definition tuple.h:68
static const Def * infer(World &, Defs)
Definition check.cpp:261
const Def * rebuild_(World &, const Def *, Defs) const override
Definition def.cpp:129
static constexpr auto Node
Definition tuple.h:60
The World represents the whole program and manages creation of MimIR nodes (Defs).
Definition world.h:33
Definition ast.h:14
View< const Def * > Defs
Definition def.h:48
const Def * flatten(const Def *def)
Flattens a sigma/array/pack/tuple.
Definition tuple.cpp:66
Vector< const Def * > DefVec
Definition def.h:49
bool is_unit(const Def *)
Definition tuple.cpp:46
const Def * merge_sigma(const Def *def, Defs defs)
Definition tuple.cpp:93
std::string tuple2str(const Def *)
Definition tuple.cpp:48
DefVec merge(Defs, Defs)
Definition tuple.cpp:86
const Def * unflatten(const Def *def, const Def *type)
Applies the reverse transformation on a Pack / Tuple, given the original type.
Definition tuple.cpp:80
const Def * tuple_of_types(const Def *t)
Definition tuple.cpp:109
const Def * merge_tuple(const Def *def, Defs defs)
Definition tuple.cpp:98
@ Arr
Definition def.h:84
@ Pack
Definition def.h:84
@ Sigma
Definition def.h:84
@ Extract
Definition def.h:84
@ Insert
Definition def.h:84
@ Tuple
Definition def.h:84