3#include <absl/container/fixed_array.h>
14static bool needs_zonk(
const Def* def) {
16 for (
auto mut : def->local_muts())
25 Zonker(World& world, Def* root)
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;
38 const Def* rewrite_mut(Def* root)
final {
40 assert(root == root_);
43 auto old_type = root->type();
44 auto old_ops = absl::FixedArray<const Def*>(root->ops().begin(), root->ops().end());
46 root->unset()->set_type(rewrite(old_type));
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);
61const Def*
Def::zonk()
const {
return needs_zonk(
this) ? Zonker(
world(),
nullptr).rewrite(
this) :
this; }
64 if (!
is_set())
return this;
68 if (
auto hole = mut->isa<
Hole>()) {
69 auto [last,
op] = hole->find();
70 return op ?
op->zonk() : last;
74 for (
auto def :
deps())
75 if (needs_zonk(def)) {
80 if (
zonk)
return Zonker(
world(), mut).rewrite(mut);
82 if (
auto imm = mut->immutabilize())
return imm;
90 return DefVec(defs.size(), [defs](
size_t i) { return defs[i]->zonk(); });
102 if (
auto h = def->isa_mut<Hole>()) {
110 auto root = def ? def : last;
113 for (
auto h =
this; h != last;) {
114 auto next = h->op()->as_mut<Hole>();
123 if (
is_set())
return this;
126 auto holes = absl::FixedArray<const Def*>(n);
128 auto var = sigma->has_var();
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)));
136 for (
size_t i = 0; i != n; ++i)
137 holes[i] = w.mut_hole(
type()->
proj(n, i));
140 auto tuple = w.tuple(holes);
149#ifdef MIM_ENABLE_CHECKS
150template<Checker::Mode mode>
151bool Checker::fail() {
152 if (mode ==
Check &&
world().flags().break_on_alpha) fe::breakpoint();
156const Def* Checker::fail() {
157 if (
world().flags().break_on_alpha) fe::breakpoint();
163 if (defs.empty())
return nullptr;
164 auto first = defs.front();
165 for (
size_t i = 1, e = defs.size(); i != e; ++i)
170const Def* Checker::assignable_(
const Def* type,
const Def* val) {
172 if (type == val_ty)
return val;
175 if (
auto sigma = type->isa<
Sigma>()) {
176 if (!alpha_<Check>(type->arity(), val_ty->arity()))
return fail();
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));
184 new_ops[i] = new_val;
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;
194 return alpha_<Check>(type, val_ty) ? val : fail();
197template<Checker::Mode mode>
198bool Checker::alpha_(
const Def* d1,
const Def* d2) {
199 for (
bool todo =
true; todo;) {
208 if (!d1->has_dep(
Dep::Var) && !d2->has_dep(
Dep::Var) && d1 == d2)
return true;
210 auto h1 = d1->isa_mut<
Hole>();
211 auto h2 = d2->isa_mut<
Hole>();
214 if (h1)
return h1->set(d2),
true;
215 if (h2)
return h2->set(d1),
true;
219 if (!d1->is_set() || !d2->is_set())
return fail<mode>();
221 auto mut1 = d1->isa_mut();
222 auto mut2 = d2->isa_mut();
224 if (mut1 && mut2 && mut1 == mut2)
return true;
228 if (d1->isa<
Global>() || d2->isa<
Global>())
return false;
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;
235 if (
auto t1 = d1->type()) {
236 if (
auto t2 = d2->type()) {
237 if (!alpha_<mode>(t1, t2))
return fail<mode>();
241 if (!alpha_<mode>(d1->arity(), d2->arity()))
return fail<mode>();
243 auto new_d1 = d1->zonk_mut();
244 auto new_d2 = d2->zonk_mut();
245 if (new_d1 != d1 || new_d2 != d2) {
252 auto seq1 = d1->isa<Seq>();
253 auto seq2 = d2->isa<Seq>();
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);
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);
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);
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());
272 if (d1->node() != d2->node() || d1->flags() != d2->flags())
return fail<mode>();
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>();
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>();
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>();
296bool Checker::check1(
const Seq* seq,
const Def* def) {
297 auto body = seq->reduce(
world().lit_idx_1_0());
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());
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>();
309 mut_seq->set(mut_seq->arity(), mut_body->zonk());
313bool Checker::check(
const UMax* umax,
const Def* def) {
314 for (
auto op :
umax->ops())
328 error(
type()->
loc(),
"declared sort '{}' of array does not match inferred one '{}'",
type(), t);
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);
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();
356 "incorrect type '{}' for '{}'. Correct one would be: '{}'. I'll keep this one nevertheless due to "
366 auto& w =
dom->world();
370const Def*
Pi::check(
size_t,
const Def* def) {
return def; }
375 error(
type()->
loc(),
"declared sort '{}' of function type does not match inferred one '{}'",
type(), t);
382 throw Error().
error(
filter()->
loc(),
"filter '{}' of lambda is of type '{}' but must be of type 'Bool'",
387 .
error(def->
loc(),
"body of function is not assignable to declared codomain")
388 .
note(def->
loc(),
"body: '{}'", def)
398 error(
type()->
loc(),
"declared sort '{}' of rule type does not match inferred one '{}'",
type(), t);
408 error(
type()->
loc(),
"type mismatch: '{}' for lhs, but '{}' for rhs", t1, t2);
410 error(
guard()->
loc(),
"condition '{}' of rewrite is of type '{}' but must be of type 'Bool'",
guard(),
422template bool Checker::alpha_<Checker::Check>(
const Def*,
const Def*);
423template bool Checker::alpha_<Checker::Test>(
const Def*,
const Def*);
const Def * check() final
After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
static const Def * is_uniform(Defs defs)
Yields defs.front(), if all defs are Check::alpha-equivalent (Mode::Test) and nullptr otherwise.
static bool alpha(const Def *d1, const Def *d2)
@ Check
In Mode::Check, type inference is happening and Holes will be resolved, if possible.
static const Def * assignable(const Def *type, const Def *value)
Can value be assigned to sth of type?
bool is_set() const
Yields true if empty or the last op is set.
const Def * zonk_mut() const
If *mutable, zonks all ops and tries to immutabilize it; otherwise just zonk.
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.
Defs deps() const noexcept
const Def * zonk() const
If Holes have been filled, reconstruct the program without them.
World & world() const noexcept
virtual const Def * check()
After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
constexpr auto ops() const noexcept
T * isa_mut() const
If this is mutable, it will cast constness away and perform a dynamic_cast to T.
const Def * op(size_t i) const noexcept
const Def * var(nat_t a, nat_t i) noexcept
const Def * unfold_type() const
Yields the type of this Def and builds a new Type (UInc n) if necessary.
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Error & error(Loc loc, const char *s, Args &&... args)
Error & note(Loc loc, const char *s, Args &&... args)
This node is a hole in the IR that is inferred by its context later on.
std::pair< Hole *, const Def * > find()
Transitively walks up Holes until the last one while path-compressing everything.
Hole * set(const Def *op)
const Def * tuplefy(nat_t)
If unset, explode to Tuple.
static const Def * isa_set(const Def *def)
const Def * filter() const
const Def * codom() const
const Def * check() final
After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
static const Def * infer(const Def *dom, const Def *codom)
const Def * codom() const
Base class for Sigma and Tuple.
Def(World *, Node, const Def *type, Defs ops, flags_t flags)
Constructor for an immutable Def.
Recurseivly rebuilds part of a program into the provided World w.r.t. Rewriter::map.
virtual const Def * rewrite(const Def *)
const Def * guard() const
const Def * check() override
After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
const Reform * type() const
Base class for Arr and Pack.
Def(World *, Node, const Def *type, Defs ops, flags_t flags)
Constructor for an immutable Def.
const Def * check() final
After all Def::ops have ben Def::set, this method will be invoked to check the type of this mutable.
static const Def * infer(World &, Defs)
static const Def * infer(World &, Defs)
const Def * op(trait o, const Def *type)
Vector< const Def * > DefVec
void error(Loc loc, const char *f, Args &&... args)