5#include <absl/container/fixed_array.h>
13using namespace std::literals;
34 , num_ops_(
ops.size())
37 gid_ =
world->next_gid();
39 }
else if (
auto var = isa<Var>()) {
42 auto&
world = mut->world();
43 gid_ =
world.next_gid();
63 auto muts = &
world->muts();
65 gid_ =
world->next_gid();
67 for (
size_t i = 0, e =
ops.size(); i != e; ++i) {
71 vars_ =
vars->merge(vars_,
op->local_vars());
72 muts_ = muts->merge(muts_,
op->local_muts());
92 std::fill_n(ops_ptr(),
num_ops,
nullptr);
98UMax::UMax(World& world,
Defs ops)
99 : Def(Node, world.univ(), ops, 0) {}
107const Def* Hole ::rebuild_(
World&,
const Def*,
Defs )
const { fe::unreachable(); }
108const Def* Global ::rebuild_(
World&,
const Def*,
Defs )
const { fe::unreachable(); }
109const Def* Idx ::rebuild_(
World& w,
const Def* ,
Defs )
const {
return w.type_idx(); }
110const Def* Nat ::rebuild_(
World& w,
const Def* ,
Defs )
const {
return w.type_nat(); }
111const Def* Univ ::rebuild_(
World& w,
const Def* ,
Defs )
const {
return w.univ(); }
112const Def* App ::rebuild_(
World& w,
const Def* ,
Defs o)
const {
return w.app(o[0], o[1]); }
113const Def* Arr ::rebuild_(
World& w,
const Def* ,
Defs o)
const {
return w.arr(o[0], o[1]); }
115const Def* Inj ::rebuild_(
World& w,
const Def* t,
Defs o)
const {
return w.inj(t, o[0])->set(
dbg()); }
116const Def* Insert ::rebuild_(
World& w,
const Def* ,
Defs o)
const {
return w.insert(o[0], o[1], o[2]); }
117const Def* Lam ::rebuild_(
World& w,
const Def* t,
Defs o)
const {
return w.lam(t->as<
Pi>(), o[0], o[1]); }
118const Def* Lit ::rebuild_(
World& w,
const Def* t,
Defs )
const {
return w.lit(t,
get()); }
119const Def* Merge ::rebuild_(
World& w,
const Def* t,
Defs o)
const {
return w.merge(t, o); }
120const Def* Pack ::rebuild_(
World& w,
const Def* t,
Defs o)
const {
return w.pack(t->arity(), o[0]); }
122const Def* Proxy ::rebuild_(
World& w,
const Def* t,
Defs o)
const {
return w.proxy(t, o,
pass(),
tag()); }
123const Def* Rule ::rebuild_(
World& w,
const Def* t,
Defs o)
const {
return w.rule(t->as<
Reform>(), o[0], o[1], o[2]); }
124const Def* Reform ::rebuild_(
World& w,
const Def* ,
Defs o)
const {
return w.reform(o[0]); }
125const Def* Sigma ::rebuild_(
World& w,
const Def* ,
Defs o)
const {
return w.sigma(o); }
126const Def* Split ::rebuild_(
World& w,
const Def* t,
Defs o)
const {
return w.split(t, o[0]); }
127const Def* Match ::rebuild_(
World& w,
const Def* ,
Defs o)
const {
return w.match(o); }
128const Def* Tuple ::rebuild_(
World& w,
const Def* t,
Defs o)
const {
return w.tuple(t, o); }
129const Def* Type ::rebuild_(
World& w,
const Def* ,
Defs o)
const {
return w.type(o[0]); }
130const Def* UInc ::rebuild_(
World& w,
const Def* ,
Defs o)
const {
return w.uinc(o[0],
offset()); }
131const Def* UMax ::rebuild_(
World& w,
const Def* ,
Defs o)
const {
return w.umax(o); }
132const Def* Uniq ::rebuild_(
World& w,
const Def* ,
Defs o)
const {
return w.uniq(o[0]); }
133const Def* Var ::rebuild_(
World& w,
const Def* ,
Defs o)
const {
return w.var(o[0]->
as_mut()); }
135const Def* Axm ::rebuild_(
World& w,
const Def* t,
Defs )
const {
148Arr* Arr ::stub_(
World& w,
const Def* t) {
return w.mut_arr (t); }
150Hole* Hole ::stub_(
World& w,
const Def* t) {
return w.mut_hole (t); }
151Lam* Lam ::stub_(
World& w,
const Def* t) {
return w.mut_lam (t->as<
Pi>()); }
152Pack* Pack ::stub_(
World& w,
const Def* t) {
return w.mut_pack (t); }
154Rule* Rule ::stub_(
World& w,
const Def* t) {
return w.mut_rule(t->as<
Reform>()); }
175 if (!
is_set())
return false;
179 if (
op->free_vars().contains(v))
return false;
182 for (
auto mut :
op->local_muts())
183 if (mut ==
this)
return false;
204 if (
auto n =
Lit::isa(
arity()); n && *n < w.flags().scalarize_threshold)
205 return w.sigma(
DefVec(*n, [&](
size_t i) {
return reduce(w.lit_idx(*n, i)); }));
214 if (
auto n =
Lit::isa(
arity()); n && *n < w.flags().scalarize_threshold)
215 return w.tuple(
DefVec(*n, [&](
size_t i) {
return reduce(w.lit_idx(*n, i)); }));
224Defs Def::reduce_(
const Def* arg)
const {
230 auto new_ops = absl::FixedArray<const Def*>(
num_ops());
231 for (
size_t j = 0, e =
num_ops(); j != e; ++j)
232 new_ops[j] = i == j ? new_op :
op(j);
241#ifdef MIM_ENABLE_CHECKS
242 if (
world().watchpoints().contains(
gid())) fe::breakpoint();
246 size_t n =
ops.size();
247 assert(n ==
num_ops() &&
"num ops don't match");
249 for (
size_t i = 0; i != n; ++i) {
264#ifdef MIM_ENABLE_CHECKS
265 if (
world().watchpoints().contains(
gid())) fe::breakpoint();
270 assert(def && !
op(i) && curr_op_++ == i);
291 std::ranges::fill(ops_ptr(), ops_ptr() +
num_ops(),
nullptr);
296 if (
num_ops() == 0)
return true;
297 bool result =
ops().back();
298 assert((!result || std::ranges::all_of(
ops().rsubspan(1), [](
auto op) {
return op; }))
299 &&
"the last operand is set but others in front of it aren't");
308 if (var_)
return var_;
310 if (w.is_frozen())
return nullptr;
318 if (w.is_frozen())
return nullptr;
319 if (
auto lam = isa<Lam >())
return lam->dom();
320 if (
auto pi = isa<Pi >())
return pi ->dom();
321 if (
auto sig = isa<Sigma>())
return sig;
322 if (
auto arr = isa<Arr >())
return w.type_idx(arr ->
arity());
323 if (
auto pack = isa<Pack >())
return w.type_idx(pack->arity());
324 if (
auto rule = isa<Rule >())
return rule->type()->meta_type();
325 if (isa<Bound >())
return this;
326 if (isa<Hole >())
return nullptr;
327 if (isa<Global>())
return nullptr;
338 if (
auto mut =
isa_mut())
return mut->free_vars();
343 fvs =
vars.merge(fvs, mut->free_vars());
359 for (
bool todo = cyclic; todo;) {
378 if (mark_ != 0 && mark_ != run - 1) {
379 if constexpr (init) todo |= mark_ == run;
388 auto& muts = w.muts();
389 auto&
vars = w.vars();
395 if constexpr (init) mut->muts_ = muts.insert(mut->muts_,
this);
396 fvs =
vars.merge(fvs, mut->free_vars<init>(todo, run));
402 if constexpr (!
init) todo |= fvs0 != fvs;
407void Def::invalidate() {
411 for (
auto mut :
users())
420#ifdef MIM_ENABLE_CHECKS
440 if (
auto var = isa<Var>())
return var->mut()->world();
442 for (
auto def =
this;; def = def->type()) {
443 if (def->isa<
Univ>())
return *def->world_;
444 if (
auto type = def->isa<
Type>())
return *
type->level()->type()->as<
Univ>()->world_;
448 if (
auto var = isa<Var>())
return var->mut()->var_type();
453 if (
auto t =
type())
return t;
455 if (
auto t = isa<Type>())
return w.type(w.uinc(t->level()));
462#define CODE(name, _) \
463 case Node::name: return #name;
466 default: fe::unreachable();
471 if (isa<Type>() || isa<Univ>())
return Defs();
472 if (isa<Var>())
return ops();
474 return Defs(ops_ptr() - 1, (
is_set() ? num_ops_ : 0) + 1);
480 case Node::n: return u32(j);
483 default: fe::unreachable();
488 if (
auto t =
type()) {
489 if (
auto u = t->type()) {
491 if (
auto level =
Lit::isa(
type->level()))
return *level == 0;
508 if (a == b)
return Cmp::E;
520 assert(a->isa_imm() && b->
isa_imm());
522 if (
auto va = a->isa<
Var>()) {
523 auto vb = b->as<
Var>();
527 if (mb->is_set() && mb->free_vars().contains(va))
return Cmp::G;
532 for (
size_t i = a->num_ops(); i-- != 0;)
533 if (
auto res =
cmp(a->op(i), b->
op(i)); res ==
Cmp::L || res ==
Cmp::G)
return res;
535 return cmp(a->type(), b->
type());
539bool Def::cmp_(
const Def* a,
const Def* b) {
540 auto res =
cmp(a, b);
542 a->world().WLOG(
"resorting to unstable gid-based compare for commute check");
543 return c ==
Cmp::L ? a->gid() < b->
gid() : a->gid() > b->
gid();
549bool Def::less (
const Def* a,
const Def* b) {
return cmp_<Cmp::L>(a, b); }
550bool Def::greater(
const Def* a,
const Def* b) {
return cmp_<Cmp::G>(a, b); }
554 if (
auto t =
type(); t && !t->isa<
Type>())
return t->arity();
558bool Def::equal(
const Def* other)
const {
559 if (isa<Univ>() || this->
isa_mut() || other->
isa_mut())
return this == other;
564 for (
size_t i = 0, e =
num_ops(); result && i != e; ++i)
565 result &= this->
op(i) == other->
op(i);
574 assert(this->
sym() == to->
sym());
591 if (w.is_frozen())
return nullptr;
594 assert(i == 0 &&
"only inhabitant of Idx 2 is 0_1");
595 if (!
type())
return this;
599 if (
auto seq = isa<Seq>()) {
600 if (seq->has_var())
return seq->reduce(
world().lit_idx(a, i));
604 if (isa<Prod>())
return op(i);
606 return w.extract(
this, a, i);
614 if (
auto app = def->isa<
App>()) {
615 if (app->callee()->isa<Idx>())
return app->arg();
623 if (
auto l =
Lit::isa(size))
return l;
628 if (size->isa<
Top>())
return 64;
const Def * arity() const final
const Def * reduce(const Def *arg) const final
const Def * immutabilize() final
Tries to make an immutable from a mutable.
NormalizeFn normalizer() const
static bool alpha(const Def *d1, const Def *d2)
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.
constexpr Node node() const noexcept
Def * set(size_t i, const Def *)
Successively set from left to right.
T * as_mut() const
Asserts that this is a mutable, casts constness away and performs a static_cast to T.
Defs deps() const noexcept
nat_t num_tprojs() const
As above but yields 1, if Flags::scalarize_threshold is exceeded.
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.
const Def * refine(size_t i, const Def *new_op) const
Def * set_type(const Def *)
Update type.
std::string_view node_name() const
constexpr auto ops() const noexcept
Vars local_vars() const
Vars reachable by following immutable deps().
constexpr flags_t flags() const noexcept
T * isa_mut() const
If this is mutable, it will cast constness away and perform a dynamic_cast to T.
const Def * debug_prefix(std::string) const
const Def * op(size_t i) const noexcept
bool is_immutabilizable()
const Def * var(nat_t a, nat_t i) noexcept
void transfer_external(Def *to)
const Def * unfold_type() const
Yields the type of this Def and builds a new Type (UInc n) if necessary.
bool is_open() const
Has free_vars()?
Muts local_muts() const
Mutables reachable by following immutable deps(); mut->local_muts() is by definition the set { mut }...
const Def * debug_suffix(std::string) const
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
bool is_external() const noexcept
const Def * rebuild(World &w, const Def *type, Defs ops) const
Def::rebuilds this Def while using new_op as substitute for its i'th Def::op.
static bool less(const Def *a, const Def *b)
static bool greater(const Def *a, const Def *b)
const Def * var()
Not necessarily a Var: E.g., if the return type is [], this will yield ().
static Cmp cmp(const Def *a, const Def *b)
virtual constexpr size_t reduction_offset() const noexcept
First Def::op that needs to be dealt with during reduction; e.g.
nat_t num_projs() const
Yields Def::arity(), if it is a Lit, or 1 otherwise.
const Def * var_type()
If this is a binder, compute the type of its Variable.
constexpr u32 gid() const noexcept
Global id - unique number for this Def.
virtual const Def * arity() const
Def * unset()
Unsets all Def::ops; works even, if not set at all or only partially set.
std::string unique_name() const
name + "_" + Def::gid
const T * isa_imm() const
Muts users()
Set of mutables where this mutable is locally referenced.
bool is_closed() const
Has no free_vars()?
Vars free_vars() const
Compute a global solution by transitively following mutables as well.
u32 judge() const noexcept
const Var * has_var()
Only returns not nullptr, if Var of this mutable has ever been created.
constexpr size_t num_ops() const noexcept
const Def * alloced_type() const
Global * stub_(World &, const Def *) final
This node is a hole in the IR that is inferred by its context later on.
static constexpr nat_t size2bitwidth(nat_t n)
static const Def * isa(const Def *def)
Checks if def is a Idx s and returns s or nullptr otherwise.
static std::optional< nat_t > isa_lit(const Def *def)
static std::optional< T > isa(const Def *def)
const Def * immutabilize() final
Tries to make an immutable from a mutable.
const Def * arity() const final
const Def * reduce(const Def *arg) const final
A dependent function type.
Pi(const Def *type, const Def *dom, const Def *codom, bool implicit)
Constructor for an immutable Pi.
const Def * codom() const
const Pi * immutabilize() final
Tries to make an immutable from a mutable.
Def(World *, Node, const Def *type, Defs ops, flags_t flags)
Constructor for an immutable Def.
u32 pass() const
IPass::index within PassMan.
const Def * guard() const
const Rule * immutabilize() override
Tries to make an immutable from a mutable.
const Reform * type() const
Def(World *, Node, const Def *type, Defs ops, flags_t flags)
Constructor for an immutable Def.
constexpr bool empty() const noexcept
Is empty?
bool contains(D *d) const noexcept
Is ?.
const TExt< Up > * set(Loc l) const
const Def * immutabilize() final
Tries to make an immutable from a mutable.
const Def * rebuild_(World &, const Def *, Defs) const final
Extremum. Either Top (Up) or Bottom.
const Def * rebuild_(World &, const Def *, Defs) const final
A variable introduced by a binder (mutable).
The World represents the whole program and manages creation of MimIR nodes (Defs).
void make_external(Def *)
const Def * sigma(Defs ops)
const Pi * pi(const Def *dom, const Def *codom, bool implicit=false)
Flags & flags()
Retrieve compile Flags.
Sym sym(std::string_view)
void make_internal(Def *)
Defs reduce(const Var *var, const Def *arg)
Yields the new body of [mut->var() -> arg]mut.
const Rule * rule(const Reform *type, const Def *lhs, const Def *rhs, const Def *guard)
Vector< const Def * > DefVec
Dep
Tracks a dependency to certain Defs transitively through the Def::deps() up to but excliding mutables...
uint64_t scalarize_threshold
constexpr size_t hash_combine(size_t seed, T v) noexcept
constexpr decltype(auto) get(Span< T, N > span) noexcept
consteval size_t hash_begin() noexcept
constexpr size_t hash(size_t h) noexcept
Sets< const Var >::Set Vars