16bool is_shape(
const Def* s) {
17 if (
s->isa<
Nat>())
return true;
18 if (
auto arr =
s->isa<
Arr>())
return arr->body()->zonk()->isa<
Nat>();
19 if (
auto sig =
s->isa_imm<
Sigma>())
20 return std::ranges::all_of(sig->ops(), [](
const Def* op) { return op->isa<Nat>(); });
31#if (!defined(_MSC_VER) && defined(NDEBUG))
32bool World::Lock::guard_ =
false;
45 data_.sigma = unify<Sigma>(
type(),
Defs{})->as<Sigma>();
46 data_.tuple = unify<Tuple>(
sigma(),
Defs{})->as<Tuple>();
52 data_.lit_idx_1_0 =
lit_idx(1, 0);
54 data_.lit_bool[0] =
lit_idx(2, 0_u64);
55 data_.lit_bool[1] =
lit_idx(2, 1_u64);
63 for (
auto def : move_.defs)
79 DLOG(
"register: 0x{x} -> {}", f, def);
81 if (
driver().is_loaded(plugin)) {
91 def->external_ =
true;
97 def->external_ =
false;
98 auto num = move_.sym2external.erase(def->
sym());
99 assert_unused(num == 1);
107 level = level->
zonk();
110 error(level->
loc(),
"argument `{}` to `Type` must be of type `Univ` but is of type `{}`", level, level->
type());
112 return unify<Type>(level)->as<
Type>();
119 error(op->
loc(),
"operand '{}' of a universe increment must be of type `Univ` but is of type `{}`", op,
123 return unify<UInc>(op, offset);
127 if (
auto umax = def->isa<
UMax>())
128 for (
auto op : umax->ops())
131 ops.emplace_back(def);
137 for (
auto op : ops_) {
146 error(op->
loc(),
"operand '{}' must be a Type of some level", op);
154 for (
auto op : ops) {
156 error(op->
loc(),
"operand '{}' of a universe max must be of type 'Univ' but is of type '{}'", op,
160 lvl = std::max(lvl, *l);
162 res.emplace_back(op);
167 if (lvl > 0) res.emplace_back(l);
169 std::ranges::sort(res, [](
auto op1,
auto op2) {
return op1->gid() < op2->gid(); });
170 res.erase(std::unique(res.begin(), res.end()), res.end());
171 const Def*
umax = unify<UMax>(*
this, res);
184 if (
auto var = mut->var_)
return var;
185 return mut->var_ = unify<Var>(
type, mut);
188template<
bool Normalize>
195template<
bool Normalize>
197 callee = callee->
zonk();
200 if (
auto pi = callee->
type()->isa<
Pi>()) {
202 arg = new_arg->
zonk();
203 if (
auto imm = callee->
isa_imm<
Lam>())
return imm->body();
206 if (
auto var =
lam->has_var()) {
207 if (
auto i = move_.substs.find({var, arg}); i != move_.substs.end()) {
209 auto [
filter, body] = i->second->defs<2>();
216 DLOG(
"partial evaluate: {} ({})",
lam, arg);
217 auto body = rw.rewrite(
lam->body());
218 auto num_bytes =
sizeof(Reduct) + 2 *
sizeof(
const Def*);
219 auto buf = move_.arena.substs.allocate(num_bytes,
alignof(
const Def*));
220 auto reduct =
new (buf) Reduct(2);
221 reduct->defs_[0] =
filter;
222 reduct->defs_[1] = body;
232 auto type =
pi->reduce(arg)->zonk();
233 callee = callee->
zonk();
236 curry = curry == 0 ? trip : curry;
239 if (
auto normalizer =
axm->normalizer(); Normalize && normalizer && curry == 0) {
240 if (
auto norm = normalizer(
type, callee, arg))
return norm;
248 .
error(arg->
loc(),
"cannot apply argument to callee")
249 .
note(callee->
loc(),
"callee: '{}'", callee)
250 .
note(arg->
loc(),
"argument: '{}'", arg)
251 .
note(callee->
loc(),
"vvv domain type vvv\n'{}'\n'{}'",
pi->dom(), arg->
type())
252 .
note(arg->
loc(),
"^^^ argument type ^^^");
256 .
error(callee->
loc(),
"called expression not of function type")
257 .
error(callee->
loc(),
"'{}' <--- callee type", callee->
type());
262 callee = callee->
zonk();
267 curry = curry == 0 ? trip : curry;
275 return unify<App>(
axm, curry, trip,
type, callee, arg);
280 if (n == 0)
return sigma();
281 if (n == 1)
return ops[0]->zonk();
290 if (n == 0)
return tuple();
291 if (n == 1)
return ops[0]->zonk();
298 error(t->loc(),
"cannot assign tuple '{}' of type '{}' to incompatible tuple type '{}'", t, t->type(),
sigma);
310 if (n == 0)
return tuple();
311 if (n == 1)
return ops[0];
318 if (
auto extract = ops[0]->isa<Extract>()) {
320 bool eta = tup->type() ==
type;
321 for (
size_t i = 0; i != n && eta; ++i) {
322 if (
auto extract = ops[i]->isa<Extract>()) {
324 if (eta &=
u64(i) == *index) {
325 eta &=
extract->tuple() == tup;
337 return unify<Tuple>(
type, ops);
342 std::ranges::transform(
sym, std::back_inserter(defs), [
this](
auto c) {
return lit_i8(c); });
348 index = index->
zonk();
351 for (
auto op :
tuple->ops())
354 }
else if (
auto pack = index->isa<
Pack>()) {
356 for (
nat_t i = 0, e = *a; i != e; ++i) {
365 auto type = d->unfold_type();
368 if (
auto l =
Lit::isa(size); l && *l == 1) {
369 if (
auto l =
Lit::isa(index); !l || *l != 0)
WLOG(
"unknown Idx of size 1: {}", index);
378 if (
auto pack = d->isa_imm<
Pack>())
return pack->body();
381 error(index->
loc(),
"index '{}' does not fit within arity '{}'", index,
type->arity());
400 return unify<Extract>(t, d, index);
403 return unify<Extract>(
sigma->op(*i), d, index);
409 elem_t =
arr->reduce(index);
413 if (index->isa<
Top>()) {
416 hole->set(
pack(size, elem_hole));
422 return unify<Extract>(elem_t, d, index);
427 index = index->
zonk();
430 auto type = d->unfold_type();
434 if (!size)
error(d->loc(),
"index '{}' must be of type 'Idx' but is of type '{}'", index, index->
type());
437 error(index->
loc(),
"index '{}' does not fit within arity '{}'", index,
type->arity());
440 auto elem_type =
type->proj(*lidx);
444 .
error(val->
loc(),
"value to be inserted not assignable to element")
445 .
note(val->
loc(),
"vvv value type vvv \n'{}'\n'{}'", val->
type(), elem_type)
446 .
note(val->
loc(),
"^^^ element type ^^^", elem_type);
451 if (
auto l =
Lit::isa(size); l && *l == 1)
452 return tuple(d, {val});
455 if (
auto t = d->isa<
Tuple>(); t && lidx)
return t->refine(*lidx, val);
461 new_ops[*lidx] = val;
471 return unify<Insert>(d, index, val);
475 arity = arity->
zonk();
479 if (!is_shape(arity_ty))
error(arity->
loc(),
"expected arity but got `{}` of type `{}`", arity, arity_ty);
482 if (*a == 0)
return unit(term);
483 if (*a == 1)
return body;
488 return seq(term,
tuple->ops().front(),
seq(term,
tuple->ops().subspan(1), body));
491 if (
auto p = arity->isa<
Pack>()) {
492 if (
auto s =
Lit::isa(p->arity()))
return seq(term, p->body(),
seq(term,
pack(*s - 1, p->body()), body));
497 return unify<Pack>(
type, body);
499 return unify<Arr>(body->
unfold_type(), arity, body);
504 if (shape.empty())
return body;
505 return seq(term, shape.rsubspan(1),
seq(term, shape.back(), body));
512 if (size->isa<
Top>()) {
514 }
else if (
auto s =
Lit::isa(size)) {
515 if (*s != 0 && val >= *s)
error(
type->loc(),
"index '{}' does not fit within arity '{}'", size, val);
516 }
else if (val != 0) {
517 error(
type->loc(),
"cannot create literal '{}' of 'Idx {}' as size is unknown", val, size);
521 return unify<Lit>(
type, val);
535 return unify<TExt<Up>>(
type);
541 for (
size_t i = 0, e = ops_.size(); i != e; ++i) {
542 auto op = ops_[i]->zonk();
543 if (!op->isa<
TExt<!Up>>()) ops.emplace_back(op);
549 if (std::ranges::any_of(ops, [&](
const Def* op) ->
bool {
return op->isa<
TExt<Up>>(); }))
return ext<Up>(kind);
553 ops.resize(std::distance(ops.begin(), std::unique(ops.begin(), ops.end())));
555 if (ops.size() == 0)
return ext<!Up>(kind);
556 if (ops.size() == 1)
return ops[0];
559 return unify<TBound<Up>>(kind, ops);
567 auto types =
DefVec(ops.size(), [&](
size_t i) { return ops[i]->type(); });
568 return unify<Merge>(
meet(types), ops);
571 assert(ops.size() == 1);
582 value = value->
zonk();
590 value = value->
zonk();
592 return unify<Split>(
type, value);
597 if (ops.size() == 1)
return ops.front();
599 auto scrutinee = ops.front();
600 auto arms = ops.span().subspan(1);
601 auto join = scrutinee->type()->isa<
Join>();
603 if (!
join)
error(scrutinee->loc(),
"scrutinee of a test expression must be of union type");
605 if (arms.size() !=
join->num_ops())
606 error(scrutinee->loc(),
"test expression has {} arms but union type has {} cases", arms.size(),
609 for (
auto arm : arms)
610 if (!arm->type()->isa<
Pi>())
611 error(arm->loc(),
"arm of test expression does not have a function type but is of type '{}'", arm->type());
613 std::ranges::sort(arms, [](
const Def* arm1,
const Def* arm2) {
618 for (
size_t i = 0, e = arms.size(); i != e; ++i) {
620 auto pi = arm->type()->as<
Pi>();
623 "domain type '{}' of arm in a test expression does not match case type '{}' in union type",
pi->dom(),
628 return unify<Match>(
type, ops);
632 inhabitant = inhabitant->
zonk();
637 auto name = symbol.str();
639 auto pos =
name.find(suffix);
640 if (pos != std::string::npos) {
641 auto num =
name.substr(pos + suffix.size());
646 num = std::to_string(std::stoi(num) + 1);
647 name =
name.substr(0, pos + suffix.size()) +
"_" + num;
657 auto mut =
var->mut();
658 auto offset = mut->reduction_offset();
659 auto size = mut->num_ops() - offset;
661 if (
auto i = move_.substs.find({var, arg}); i != move_.substs.end())
return i->second->defs();
663 auto buf = move_.arena.substs.allocate(
sizeof(Reduct) + size *
sizeof(
const Def*),
alignof(
const Def*));
664 auto reduct =
new (buf) Reduct(size);
666 for (
size_t i = 0; i != size; ++i)
667 reduct->defs_[i] = rw.rewrite(mut->op(i + offset));
669 return reduct->defs();
676#ifdef MIM_ENABLE_CHECKS
682 auto i = std::ranges::find_if(move_.defs, [=](
auto def) { return def->gid() == gid; });
683 if (i == move_.defs.end())
return nullptr;
689 assert(mut->is_closed() && mut->is_set());
691 assert(anx->is_closed());
A (possibly paramterized) Array.
static constexpr u8 Trip_End
static std::tuple< const Axm *, u8, u8 > get(const Def *def)
Yields currying counter of def.
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)
static const Def * assignable(const Def *type, const Def *value)
Can value be assigned to sth of type?
const Def * zonk() const
If Holes have been filled, reconstruct the program without them.
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 * 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).
bool is_external() const noexcept
constexpr u32 gid() const noexcept
Global id - unique number for this Def.
virtual const Def * arity() const
const T * isa_imm() const
bool is_closed() const
Has no free_vars()?
Some "global" variables needed all over the place.
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.
static Hole * isa_unset(const Def *def)
static nat_t as_lit(const Def *def)
static const Def * isa(const Def *def)
Checks if def is a Idx s and returns s or nullptr otherwise.
Creates a new Tuple / Pack by inserting Insert::value at position Insert::index into Insert::tuple.
static std::optional< T > isa(const Def *def)
Facility to log what you are doing.
A (possibly paramterized) Tuple.
A dependent function type.
static Pi * isa_implicit(const Def *d)
Is d an Pi::is_implicit (mutable) Pi?
static const Def * infer(World &, Defs)
Extremum. Either Top (Up) or Bottom.
Data constructor for a Sigma.
static const Def * infer(World &, Defs)
const Def * rewrite(const Def *old_def) final
const Lit * lit_idx(nat_t size, u64 val)
Constructs a Lit of type Idx of size size.
const Def * insert(const Def *d, const Def *i, const Def *val)
const Def * meet(Defs ops)
const Def * uinc(const Def *op, level_t offset=1)
const Lit * lit(const Def *type, u64 val)
void watchpoint(u32 gid)
Trigger breakpoint in your debugger when Def::setting a Def with this gid.
const Type * type(const Def *level)
void make_external(Def *)
const Driver & driver() const
const Def * filter(Lam::Filter filter)
const Def * sigma(Defs ops)
const Def * pack(const Def *arity, const Def *body)
const Def * unit(bool term)
const Def * app(const Def *callee, const Def *arg)
const Pi * pi(const Def *dom, const Def *codom, bool implicit=false)
const Def * seq(bool term, const Def *arity, const Def *body)
World & verify()
Verifies that all externals() and annexes() are Def::is_closed(), if MIM_ENABLE_CHECKS.
Hole * mut_hole(const Def *type)
const Lam * lam(const Pi *pi, Lam::Filter f, const Def *body)
const Def * tuple(Defs ops)
const Def * gid2def(u32 gid)
Lookup Def by gid.
Flags & flags()
Retrieve compile Flags.
const Def * implicit_app(const Def *callee, const Def *arg)
Places Holes as demanded by Pi::is_implicit() and then apps arg.
const Def * inj(const Def *type, const Def *value)
const Axm * axm(NormalizeFn n, u8 curry, u8 trip, const Def *type, plugin_t p, tag_t t, sub_t s)
const Def * var(const Def *type, Def *mut)
const Def * extract(const Def *d, const Def *i)
const Def * arr(const Def *arity, const Def *body)
Sym sym(std::string_view)
const Def * bound(Defs ops)
const Def * join(Defs ops)
const Def * ext(const Def *type)
Sym append_suffix(Sym name, std::string suffix)
Appends a suffix or an increasing number if the suffix already exists.
void make_internal(Def *)
const Lit * lit_idx_1_0()
const Lit * lit_univ(u64 level)
const Tuple * tuple()
the unit value of type []
const Def * uniq(const Def *inhabitant)
const Def * raw_app(const Axm *axm, u8 curry, u8 trip, const Def *type, const Def *callee, const Def *arg)
const Def * merge(const Def *type, Defs ops)
const Sigma * sigma()
The unit type within Type 0.
const Lit * lit_nat(nat_t a)
const State & state() const
const Def * register_annex(flags_t f, const Def *)
Defs reduce(const Var *var, const Def *arg)
Yields the new body of [mut->var() -> arg]mut.
void breakpoint(u32 gid)
Trigger breakpoint in your debugger when creating a Def with this gid.
const Def * split(const Def *type, const Def *value)
#define DLOG(...)
Vaporizes to nothingness in Debug build.
Vector< const Def * > DefVec
auto assert_emplace(C &container, Args &&... args)
Invokes emplace on container, asserts that insertion actually happened, and returns the iterator.
TBound< true > Join
AKA union.
void error(Loc loc, const char *f, Args &&... args)
static void flatten_umax(DefVec &ops, const Def *def)
TBound< false > Meet
AKA intersection.
Compiler switches that must be saved and looked up in later phases of compilation.
static Sym demangle(Driver &, plugin_t plugin)
Reverts an Axm::mangled string to a Sym.