3#include <absl/container/fixed_array.h>
13static bool needs_zonk(
const Def* def) {
15 for (
auto mut : def->local_muts())
16 if (
auto hole = mut->isa<
Hole>(); hole && hole->
is_set())
return true;
27 const Def* rewrite(
const Def* def)
override {
28 if (
auto hole = def->isa_mut<
Hole>()) {
29 auto [
last,
op] = hole->find();
30 return op ? rewrite(op) :
last;
39const Def*
Def::zonk()
const {
return needs_zonk(
this) ? Zonker(
world()).rewrite(
this) :
this; }
43 for (
auto def :
deps())
44 if (needs_zonk(def)) {
50 auto zonker = Zonker(
world());
51 auto old_type =
type();
52 auto old_ops = absl::FixedArray<const Def*>(
ops().begin(),
ops().end());
55 for (
size_t i = 0, e =
num_ops(); i != e; ++i)
set(i, zonker.rewrite(old_ops[i]));
63 return DefVec(defs.size(), [defs](
size_t i) { return defs[i]->zonk(); });
75 if (
auto h = def->isa_mut<Hole>()) {
83 auto root = def ? def : last;
86 for (
auto h =
this; h != last;) {
87 auto next = h->op()->as_mut<Hole>();
88 h->unset()->set(root);
99 auto holes = absl::FixedArray<const Def*>(n);
101 auto var = sigma->has_var();
103 holes[0] = w.mut_hole(sigma->op(0));
104 for (
size_t i = 1; i != n; ++i) {
105 rw.map(sigma->var(n, i - 1), holes[i - 1]);
106 holes[i] = w.mut_hole(rw.rewrite(sigma->op(i)));
109 for (
size_t i = 0; i != n; ++i) holes[i] = w.mut_hole(
type()->
proj(n, i));
112 auto tuple = w.tuple(holes);
121#ifdef MIM_ENABLE_CHECKS
122template<Checker::Mode mode>
bool Checker::fail() {
123 if (mode ==
Check &&
world().flags().break_on_alpha) fe::breakpoint();
127const Def* Checker::fail() {
128 if (
world().flags().break_on_alpha) fe::breakpoint();
133template<Checker::Mode mode>
bool Checker::alpha_(
const Def* d1_,
const Def* d2_) {
134 auto ds = std::array<const Def*, 2>{d1_->zonk(), d2_->zonk()};
137 if (!d1 && !d2)
return true;
138 if (!d1 || !d2)
return fail<mode>();
143 if (!d1->has_dep(
Dep::Var) && !d2->has_dep(
Dep::Var) && d1 == d2)
return true;
145 auto h1 = d1->isa_mut<
Hole>();
146 auto h2 = d2->isa_mut<
Hole>();
148 if ((!h1 && !d1->is_set()) || (!h2 && !d2->is_set()))
return fail<mode>();
152 return h1->set(d2),
true;
154 return h2->set(d1),
true;
157 auto muts = std::array<Def*, 2>{d1->isa_mut(), d2->isa_mut()};
158 auto& [mut1, mut2] = muts;
160 if (mut1 && mut2 && mut1 == mut2)
return true;
164 if (d1->isa<
Global>() || d2->isa<
Global>())
return false;
167 for (
size_t i = 0; i != 2; ++i) {
169 if (!mut || !mut->is_set())
continue;
170 size_t other = (i + 1) % 2;
172 if (
auto imm = mut->zonk_mut())
173 mut =
nullptr, ds[i] = imm, redo =
true;
174 else if (
auto [i, ins] = binders_.emplace(mut, ds[other]); !ins)
175 return i->second == ds[other];
181template<Checker::Mode mode>
bool Checker::alpha_internal(
const Def* d1,
const Def* d2) {
182 if (d1->type() && d2->type() && !alpha_<mode>(d1->type(), d2->type()))
return fail<mode>();
184 if (mode ==
Test && (d1->isa_mut<
Hole>() || d2->isa_mut<
Hole>()))
return fail<mode>();
185 if (!alpha_<mode>(d1->arity(), d2->arity()))
return fail<mode>();
187 auto check1 = [
this](
const Arr* arr,
const Def*
d) {
188 auto body = arr->reduce(
world().lit_idx(1, 0))->zonk();
189 if (!alpha_<mode>(body, d))
return fail<mode>();
190 if (
auto mut_arr = arr->isa_mut<
Arr>()) mut_arr->unset()->set(
world().lit_nat_1(), body->zonk());
195 if (
auto arr = d1->isa<
Arr>();
196 arr && arr->is_set() && arr->shape()->zonk() ==
world().lit_nat_1() && !d2->isa<
Arr>())
197 return check1(arr, d2);
199 if (
auto arr = d2->isa<
Arr>();
200 arr && arr->is_set() && arr->shape()->zonk() ==
world().lit_nat_1() && !d1->isa<
Arr>())
201 return check1(arr, d1);
204 if (
auto prod = d1->isa<Prod>()) {
205 size_t a =
prod->num_ops();
206 for (
size_t i = 0; i !=
a; ++i)
207 if (!alpha_<mode>(
prod->op(i), d2->proj(a, i)))
return fail<mode>();
209 }
else if (
auto seq = d1->isa<Seq>()) {
210 if (seq->node() != d2->node())
return fail<mode>();
212 if (
auto a = seq->isa_lit_arity()) {
213 for (
size_t i = 0; i != *
a; ++i)
214 if (!alpha_<mode>(seq->proj(*a, i), d2->proj(*a, i)))
return fail<mode>();
218 auto check_arr = [
this](
Arr* mut_arr,
const Arr* imm_arr) {
219 if (!alpha_<mode>(mut_arr->shape(), imm_arr->shape()))
return fail<mode>();
221 auto mut_shape = mut_arr->shape()->zonk();
222 auto mut_body = mut_arr->reduce(
world().
top(
world().type_idx(mut_arr->shape())));
223 if (!alpha_<mode>(mut_body, imm_arr->body()))
return fail<mode>();
225 mut_arr->unset()->set(mut_shape, mut_body->zonk());
230 if (
auto mut_arr = d1->isa_mut<
Arr>(); mut_arr && mut_arr->is_set()) {
231 if (
auto imm_arr = d2->isa_imm<
Arr>())
return check_arr(mut_arr, imm_arr);
233 if (
auto mut_arr = d2->isa_mut<
Arr>(); mut_arr && mut_arr->is_set()) {
234 if (
auto imm_arr = d1->isa_imm<
Arr>())
return check_arr(mut_arr, imm_arr);
239 for (
auto op :
umax->ops())
240 if (
auto inf =
op->
isa_mut<
Hole>(); inf && !inf->is_set()) inf->set(d2);
244 if (d1->node() != d2->node() || d1->flags() != d2->flags() || d1->num_ops() != d2->num_ops())
return fail<mode>();
246 if (
auto var1 = d1->isa<
Var>()) {
247 auto var2 = d2->as<
Var>();
248 if (
auto i = binders_.find(var1->mut()); i != binders_.end())
return i->second == var2->mut();
249 if (
auto i = binders_.find(var2->mut()); i != binders_.end())
return fail<mode>();
254 for (
size_t i = 0, e = d1->num_ops(); i != e; ++i)
255 if (!alpha_<mode>(d1->op(i), d2->op(i)))
return fail<mode>();
259const Def* Checker::assignable_(
const Def* type,
const Def* val) {
261 if (type == val_ty)
return val;
265 if (!alpha_<Check>(
type->arity(), val_ty->arity()))
return fail();
267 size_t a = sigma->num_ops();
268 auto red = sigma->reduce(val);
269 auto new_ops = absl::FixedArray<const Def*>(red.size());
270 for (
size_t i = 0; i !=
a; ++i) {
271 auto new_val = assignable_(red[i], val->proj(a, i));
273 new_ops[i] = new_val;
277 return w.tuple(new_ops);
278 }
else if (
auto arr =
type->isa<
Arr>()) {
279 if (!alpha_<Check>(
type->arity(), val_ty->arity()))
return fail();
283 if (
auto a =
Lit::isa(arr->arity())) {
284 auto new_ops = absl::FixedArray<const Def*>(*a);
285 for (
size_t i = 0; i != *
a; ++i) {
286 auto new_val = assignable_(arr->proj(*a, i), val->proj(*a, i));
288 new_ops[i] = new_val;
292 return w.tuple(new_ops);
294 }
else if (
auto inj = val->isa<
Inj>()) {
295 if (
auto new_val = assignable_(type, inj->value()))
return w.inj(type, new_val);
297 }
else if (
auto uniq = val->type()->isa<
Uniq>()) {
298 if (
auto new_val =
assignable(type, uniq->inhabitant()))
return new_val;
302 return alpha_<Check>(type, val_ty) ? val : fail();
306 if (defs.empty())
return nullptr;
307 auto first = defs.front();
308 for (
size_t i = 1, e = defs.size(); i != e; ++i)
322 error(
type()->
loc(),
"declared sort '{}' of array does not match inferred one '{}'",
type(), t);
327 auto elems = absl::FixedArray<const Def*>(
ops.size());
328 for (
size_t i = 0, e =
ops.size(); i != e; ++i) elems[i] =
ops[i]->unfold_type();
329 return world.sigma(elems);
333 auto elems = absl::FixedArray<const Def*>(
ops.size());
334 for (
size_t i = 0, e =
ops.size(); i != e; ++i) elems[i] =
ops[i]->unfold_type();
348 "incorrect type '{}' for '{}'. Correct one would be: '{}'. I'll keep this one nevertheless due to "
358 auto& w =
dom->world();
362const Def*
Pi::check(
size_t,
const Def* def) {
return def; }
367 error(
type()->
loc(),
"declared sort '{}' of function type does not match inferred one '{}'",
type(), t);
374 throw Error().
error(
filter()->
loc(),
"filter '{}' of lambda is of type '{}' but must be of type 'Bool'",
379 .
error(def->
loc(),
"body of function is not assignable to declared codomain")
380 .
note(def->
loc(),
"body: '{}'", def)
388template bool Checker::alpha_<Checker::Check>(
const Def*,
const Def*);
389template 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)
@ Test
In Mode::Test, no type inference is happening and Holes will not be touched.
@ 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 * 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.
Def * set(size_t i, const Def *)
Successively set from left to right.
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.
Def * set_type(const Def *)
Update type.
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.
virtual const Def * immutabilize()
Tries to make an immutable from a mutable.
const Def * zonk_mut()
zonks all ops of this mutable and tries to immutabilize it; if it succeeds return it.
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
Def * unset()
Unsets all Def::ops; works even, if not set at all or partially.
constexpr size_t num_ops() const noexcept
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.
const Def * filter() const
const Def * codom() const
static std::optional< T > isa(const Def *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(const Def *dom, const Def *codom)
const Def * codom() const
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 *)
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)