MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
check.cpp
Go to the documentation of this file.
1#include "mim/check.h"
2
3#include <absl/container/fixed_array.h>
4#include <fe/assert.h>
5
6#include "mim/rewrite.h"
7#include "mim/rule.h"
8#include "mim/world.h"
9
10namespace mim {
11
12namespace {
13
14static bool needs_zonk(const Def* def) {
15 if (def->has_dep(Dep::Hole)) {
16 for (auto mut : def->local_muts())
17 if (Hole::isa_set(mut)) return true;
18 }
19
20 return false;
21}
22
23class Zonker : public Rewriter {
24public:
25 Zonker(World& world, Def* root)
26 : Rewriter(world)
27 , root_(root) {}
28
29 const Def* rewrite(const Def* def) final {
30 if (auto hole = def->isa_mut<Hole>()) {
31 auto [last, op] = hole->find();
32 return op ? rewrite(op) : last;
33 }
34
35 return def == root_ || needs_zonk(def) ? Rewriter::rewrite(def) : def;
36 }
37
38 const Def* rewrite_mut(Def* root) final {
39 // Don't create a new stub, instead rewrire the ops of the old mutable root.
40 assert(root == root_);
41 map(root, root);
42
43 auto old_type = root->type();
44 auto old_ops = absl::FixedArray<const Def*>(root->ops().begin(), root->ops().end());
45
46 root->unset()->set_type(rewrite(old_type));
47
48 for (size_t i = 0, e = root->num_ops(); i != e; ++i)
49 root->set(i, rewrite(old_ops[i]));
50 if (auto new_imm = root->immutabilize()) return map(root, new_imm);
51
52 return root;
53 }
54
55private:
56 Def* root_; // Always rewrite this one!
57};
58
59} // namespace
60
61const Def* Def::zonk() const { return needs_zonk(this) ? Zonker(world(), nullptr).rewrite(this) : this; }
62
63const Def* Def::zonk_mut() const {
64 if (!is_set()) return this;
65
66 if (auto mut = isa_mut()) {
67 // TODO copy & paste from above
68 if (auto hole = mut->isa<Hole>()) {
69 auto [last, op] = hole->find();
70 return op ? op->zonk() : last;
71 }
72
73 bool zonk = false;
74 for (auto def : deps())
75 if (needs_zonk(def)) {
76 zonk = true;
77 break;
78 }
79
80 if (zonk) return Zonker(world(), mut).rewrite(mut);
81
82 if (auto imm = mut->immutabilize()) return imm;
83 return this;
84 }
85
86 return zonk();
87}
88
90 return DefVec(defs.size(), [defs](size_t i) { return defs[i]->zonk(); });
91}
92
93/*
94 * Hole
95 */
96
97std::pair<Hole*, const Def*> Hole::find() {
98 auto def = Def::op(0);
99 auto last = this;
100
101 while (def) {
102 if (auto h = def->isa_mut<Hole>()) {
103 def = h->op();
104 last = h;
105 } else {
106 break;
107 }
108 }
109
110 auto root = def ? def : last;
111
112 // path compression
113 for (auto h = this; h != last;) {
114 auto next = h->op()->as_mut<Hole>();
115 h->set(root);
116 h = next;
117 }
118
119 return {last, def};
120}
121
122const Def* Hole::tuplefy(nat_t n) {
123 if (is_set()) return this;
124
125 auto& w = world();
126 auto holes = absl::FixedArray<const Def*>(n);
127 if (auto sigma = type()->isa_mut<Sigma>(); sigma && n >= 1 && sigma->has_var()) {
128 auto var = sigma->has_var();
129 auto rw = VarRewriter(var, this);
130 holes[0] = w.mut_hole(sigma->op(0));
131 for (size_t i = 1; i != n; ++i) {
132 rw.map(sigma->var(n, i - 1), holes[i - 1]);
133 holes[i] = w.mut_hole(rw.rewrite(sigma->op(i)));
134 }
135 } else {
136 for (size_t i = 0; i != n; ++i)
137 holes[i] = w.mut_hole(type()->proj(n, i));
138 }
139
140 auto tuple = w.tuple(holes);
141 set(tuple);
142 return tuple;
143}
144
145/*
146 * Checker
147 */
148
149#ifdef MIM_ENABLE_CHECKS
150template<Checker::Mode mode>
151bool Checker::fail() {
152 if (mode == Check && world().flags().break_on_alpha) fe::breakpoint();
153 return false;
154}
155
156const Def* Checker::fail() {
157 if (world().flags().break_on_alpha) fe::breakpoint();
158 return {};
159}
160#endif
161
163 if (defs.empty()) return nullptr;
164 auto first = defs.front();
165 for (size_t i = 1, e = defs.size(); i != e; ++i)
166 if (!alpha<Test>(first, defs[i])) return nullptr;
167 return first;
168}
169
170const Def* Checker::assignable_(const Def* type, const Def* val) {
171 auto val_ty = val->type()->zonk();
172 if (type == val_ty) return val;
173
174 auto& w = world();
175 if (auto sigma = type->isa<Sigma>()) {
176 if (!alpha_<Check>(type->arity(), val_ty->arity())) return fail();
177
178 size_t a = sigma->num_ops();
179 auto red = sigma->reduce(val);
180 auto new_ops = absl::FixedArray<const Def*>(red.size());
181 for (size_t i = 0; i != a; ++i) {
182 auto new_val = assignable_(red[i], val->proj(a, i));
183 if (new_val)
184 new_ops[i] = new_val;
185 else
186 return fail();
187 }
188 return w.tuple(new_ops);
189 } else if (auto uniq = val->type()->isa<Uniq>()) {
190 if (auto new_val = assignable(type, uniq->op())) return new_val;
191 return fail();
192 }
193
194 return alpha_<Check>(type, val_ty) ? val : fail();
195}
196
197template<Checker::Mode mode>
198bool Checker::alpha_(const Def* d1, const Def* d2) {
199 for (bool todo = true; todo;) {
200 // below we check type and arity which may in turn open up more opportunities for zonking
201 todo = false;
202 d1 = d1->zonk_mut();
203 d2 = d2->zonk_mut();
204
205 // It is only safe to check for pointer equality if there are no Vars involved.
206 // Otherwise, we have to look more thoroughly.
207 // Example: λx.x - λz.x
208 if (!d1->has_dep(Dep::Var) && !d2->has_dep(Dep::Var) && d1 == d2) return true;
209
210 auto h1 = d1->isa_mut<Hole>();
211 auto h2 = d2->isa_mut<Hole>();
212
213 if constexpr (mode == Check) {
214 if (h1) return h1->set(d2), true;
215 if (h2) return h2->set(d1), true;
216 } else if (h1 || h2) // mode == Test and h1 or h2 is an unresolved Hole
217 return fail<Test>();
218
219 if (!d1->is_set() || !d2->is_set()) return fail<mode>();
220
221 auto mut1 = d1->isa_mut();
222 auto mut2 = d2->isa_mut();
223
224 if (mut1 && mut2 && mut1 == mut2) return true;
225
226 // Globals are HACKs and require additionaly HACKs:
227 // Unless they are pointer equal (above) always consider them unequal.
228 if (d1->isa<Global>() || d2->isa<Global>()) return false;
229
230 if (auto [i, ins] = bind(mut1, d2); !ins) return i->second == d2;
231 if (auto [i, ins] = bind(mut2, d1); !ins) return i->second == d1;
232
233 if (d1->isa<Top>() || d2->isa<Top>()) return mode == Check;
234
235 if (auto t1 = d1->type()) {
236 if (auto t2 = d2->type()) {
237 if (!alpha_<mode>(t1, t2)) return fail<mode>();
238 }
239 }
240
241 if (!alpha_<mode>(d1->arity(), d2->arity())) return fail<mode>();
242
243 auto new_d1 = d1->zonk_mut();
244 auto new_d2 = d2->zonk_mut();
245 if (new_d1 != d1 || new_d2 != d2) {
246 todo = true;
247 d1 = new_d1;
248 d2 = new_d2;
249 }
250 }
251
252 auto seq1 = d1->isa<Seq>();
253 auto seq2 = d2->isa<Seq>();
254
255 if constexpr (mode == Mode::Check) {
256 if (auto umax = d1->isa<UMax>(); umax && !d2->isa<UMax>()) return check(umax, d2);
257 if (auto umax = d2->isa<UMax>(); umax && !d1->isa<UMax>()) return check(umax, d1);
258
259 if (seq1 && seq1->arity() == world().lit_nat_1() && !seq2) return check1(seq1, d2);
260 if (seq2 && seq2->arity() == world().lit_nat_1() && !seq1) return check1(seq2, d1);
261
262 if (seq1 && seq2) {
263 if (auto mut_seq = seq1->isa_mut<Seq>(); mut_seq && seq2->isa_imm()) return check(mut_seq, seq2);
264 if (auto mut_seq = seq2->isa_mut<Seq>(); mut_seq && seq1->isa_imm()) return check(mut_seq, seq1);
265 }
266 }
267
268 if (auto prod = d1->isa<Prod>()) return check<mode>(prod, d2);
269 if (auto prod = d2->isa<Prod>()) return check<mode>(prod, d1);
270 if (seq1 && seq2) return alpha_<mode>(seq1->body(), seq2->body());
271
272 if (d1->node() != d2->node() || d1->flags() != d2->flags()) return fail<mode>();
273
274 if (auto var1 = d1->isa<Var>()) {
275 auto var2 = d2->as<Var>();
276 if (auto i = binders_.find(var1->mut()); i != binders_.end()) return i->second == var2->mut();
277 if (auto i = binders_.find(var2->mut()); i != binders_.end()) return fail<mode>(); // var2 is bound
278 // both var1 and var2 are free: OK, when they are the same or in Check mode
279 return var1 == var2 || mode == Check;
280 }
281
282 for (size_t i = 0, e = d1->num_ops(); i != e; ++i)
283 if (!alpha_<mode>(d1->op(i), d2->op(i))) return fail<mode>();
284 return true;
285}
286
287template<Checker::Mode mode>
288bool Checker::check(const Prod* prod, const Def* def) {
289 size_t a = prod->num_ops();
290 for (size_t i = 0; i != a; ++i)
291 if (!alpha_<mode>(prod->op(i), def->proj(a, i))) return fail<mode>();
292 return true;
293}
294
295// alpha(«1; body», def) -> alpha(body, def);
296bool Checker::check1(const Seq* seq, const Def* def) {
297 auto body = seq->reduce(world().lit_idx_1_0()); // try to get rid of var inside of body
298 if (!alpha_<Check>(body, def)) return fail<Check>();
299 if (auto mut_seq = seq->isa_mut<Seq>()) mut_seq->set(world().lit_nat_1(), body->zonk());
300 return true;
301}
302
303// Try to get rid of mut_seq's var: it may occur in its body and vanish after reduction
304// as holes might have been filled in the meantime.
305bool Checker::check(Seq* mut_seq, const Seq* imm_seq) {
306 auto mut_body = mut_seq->reduce(world().top(world().type_idx(mut_seq->arity())));
307 if (!alpha_<Check>(mut_body, imm_seq->body())) return fail<Check>();
308
309 mut_seq->set(mut_seq->arity(), mut_body->zonk());
310 return true;
311}
312
313bool Checker::check(const UMax* umax, const Def* def) {
314 for (auto op : umax->ops())
315 if (!alpha<Check>(op, def)) return fail<Check>();
316 return true;
317}
318
319/*
320 * infer & check
321 */
322
323const Def* Arr::check(size_t, const Def* def) { return def; } // TODO
324
325const Def* Arr::check() {
326 auto t = body()->unfold_type();
328 error(type()->loc(), "declared sort '{}' of array does not match inferred one '{}'", type(), t);
329 return t;
330}
331
333 auto elems = absl::FixedArray<const Def*>(ops.size());
334 for (size_t i = 0, e = ops.size(); i != e; ++i)
335 elems[i] = ops[i]->unfold_type();
336 return world.sigma(elems);
337}
338
340 auto elems = absl::FixedArray<const Def*>(ops.size());
341 for (size_t i = 0, e = ops.size(); i != e; ++i)
342 elems[i] = ops[i]->unfold_type();
343 return w.umax<UMax::Kind>(elems);
344}
345
346const Def* Sigma::check(size_t, const Def* def) { return def; } // TODO
347
349 auto t = infer(world(), ops());
350 if (t != type()) {
351 // TODO HACK
353 return t;
354 else {
355 world().WLOG(
356 "incorrect type '{}' for '{}'. Correct one would be: '{}'. I'll keep this one nevertheless due to "
357 "bugs in clos-conv",
358 type(), this, t);
359 return type();
360 }
361 }
362 return t;
363}
364
365const Def* Pi::infer(const Def* dom, const Def* codom) {
366 auto& w = dom->world();
367 return w.umax<UMax::Kind>({dom->unfold_type(), codom->unfold_type()});
368}
369
370const Def* Pi::check(size_t, const Def* def) { return def; }
371
372const Def* Pi::check() {
373 auto t = infer(dom(), codom());
375 error(type()->loc(), "declared sort '{}' of function type does not match inferred one '{}'", type(), t);
376 return t;
377}
378
379const Def* Lam::check(size_t i, const Def* def) {
380 if (i == 0) {
381 if (auto filter = Checker::assignable(world().type_bool(), def)) return filter;
382 throw Error().error(filter()->loc(), "filter '{}' of lambda is of type '{}' but must be of type 'Bool'",
383 filter(), filter()->type());
384 } else if (i == 1) {
385 if (auto body = Checker::assignable(codom(), def)) return body;
386 throw Error()
387 .error(def->loc(), "body of function is not assignable to declared codomain")
388 .note(def->loc(), "body: '{}'", def)
389 .note(def->loc(), "type: '{}'", def->type())
390 .note(codom()->loc(), "codomain: '{}'", codom());
391 }
392 fe::unreachable();
393}
394
395const Def* Reform::check() {
396 auto t = infer(meta_type());
398 error(type()->loc(), "declared sort '{}' of rule type does not match inferred one '{}'", type(), t);
399 return t;
400}
401
402const Def* Reform::infer(const Def* meta_type) { return meta_type->unfold_type(); }
403
404const Def* Rule::check() {
405 auto t1 = lhs()->type();
406 auto t2 = rhs()->type();
408 error(type()->loc(), "type mismatch: '{}' for lhs, but '{}' for rhs", t1, t2);
409 if (!Checker::assignable(world().type_bool(), guard()))
410 error(guard()->loc(), "condition '{}' of rewrite is of type '{}' but must be of type 'Bool'", guard(),
411 guard()->type());
412
413 return type();
414}
415
416const Def* Rule::check(size_t, const Def* def) {
417 return def;
418 // TODO: do actual check + what are the parameters ?
419}
420
421#ifndef DOXYGEN
422template bool Checker::alpha_<Checker::Check>(const Def*, const Def*);
423template bool Checker::alpha_<Checker::Test>(const Def*, const Def*);
424#endif
425
426} // namespace mim
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:325
static const Def * is_uniform(Defs defs)
Yields defs.front(), if all defs are Check::alpha-equivalent (Mode::Test) and nullptr otherwise.
Definition check.cpp:162
static bool alpha(const Def *d1, const Def *d2)
Definition check.h:96
World & world()
Definition check.h:84
@ Check
In Mode::Check, type inference is happening and Holes will be resolved, if possible.
Definition check.h:89
static const Def * assignable(const Def *type, const Def *value)
Can value be assigned to sth of type?
Definition check.h:103
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
const Def * zonk_mut() const
If *mutable, zonks all ops and tries to immutabilize it; otherwise just zonk.
Definition check.cpp:63
const Def * proj(nat_t a, nat_t i) const
Similar to World::extract while assuming an arity of a, but also works on Sigmas and Arrays.
Definition def.cpp:581
Defs deps() const noexcept
Definition def.cpp:464
const Def * zonk() const
If Holes have been filled, reconstruct the program without them.
Definition check.cpp:61
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
T * isa_mut() const
If this is mutable, it will cast constness away and perform a dynamic_cast to T.
Definition def.h:482
const Def * op(size_t i) const noexcept
Definition def.h:308
const Def * var(nat_t a, nat_t i) noexcept
Definition def.h:429
const Def * unfold_type() const
Yields the type of this Def and builds a new Type (UInc n) if necessary.
Definition def.cpp:443
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Definition def.h:295
Loc loc() const
Definition def.h:503
Error & error(Loc loc, const char *s, Args &&... args)
Definition dbg.h:72
Error & note(Loc loc, const char *s, Args &&... args)
Definition dbg.h:74
This node is a hole in the IR that is inferred by its context later on.
Definition check.h:14
std::pair< Hole *, const Def * > find()
Transitively walks up Holes until the last one while path-compressing everything.
Definition check.cpp:97
Hole * set(const Def *op)
Definition check.h:33
const Def * tuplefy(nat_t)
If unset, explode to Tuple.
Definition check.cpp:122
static const Def * isa_set(const Def *def)
Definition check.h:48
const Def * filter() const
Definition lam.h:121
const Pi * type() const
Definition lam.h:129
const Def * body() const
Definition lam.h:122
const Def * codom() const
Definition lam.h:131
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
static const Def * infer(const Def *dom, const Def *codom)
Definition check.cpp:365
const Def * dom() const
Definition lam.h:34
const Def * codom() const
Definition lam.h:35
Base class for Sigma and Tuple.
Definition tuple.h:10
Def(World *, Node, const Def *type, Defs ops, flags_t flags)
Constructor for an immutable Def.
Definition def.cpp:24
const Def * meta_type() const
Definition rule.h:15
static const Def * infer(const Def *meta_type)
Definition check.cpp:402
const Def * check() override
After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
Definition check.cpp:395
Recurseivly rebuilds part of a program into the provided World w.r.t. Rewriter::map.
Definition rewrite.h:11
virtual const Def * rewrite(const Def *)
Definition rewrite.cpp:14
const Def * lhs() const
Definition rule.h:50
const Def * guard() const
Definition rule.h:52
const Def * rhs() const
Definition rule.h:51
const Def * check() override
After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
Definition check.cpp:404
const Reform * type() const
Definition rule.h:49
Base class for Arr and Pack.
Definition tuple.h:84
const Def * body() const
Definition tuple.h:91
Def(World *, Node, const Def *type, Defs ops, flags_t flags)
Constructor for an immutable Def.
Definition def.cpp:24
A dependent tuple type.
Definition tuple.h:20
friend class World
Definition tuple.h:63
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
static const Def * infer(World &, Defs)
Definition check.cpp:339
friend class World
Definition tuple.h:80
static const Def * infer(World &, Defs)
Definition check.cpp:332
@ Kind
Definition def.h:731
const Def * op(trait o, const Def *type)
Definition core.h:33
Definition ast.h:14
View< const Def * > Defs
Definition def.h:76
u64 nat_t
Definition types.h:43
Vector< const Def * > DefVec
Definition def.h:77
@ Var
Definition def.h:126
@ Hole
Definition def.h:127
void error(Loc loc, const char *f, Args &&... args)
Definition dbg.h:125
TExt< true > Top
Definition lattice.h:172
@ Global
Definition def.h:114
@ Var
Definition def.h:114
@ Hole
Definition def.h:114
@ Uniq
Definition def.h:114
@ UMax
Definition def.h:114