18 m(Type, type, Judge::Meta) m(Univ, univ, Judge::Meta) m(UMax, umax, Judge::Meta) m(UInc, uinc, Judge::Meta) \
19 m(Pi, pi, Judge::Form) m(Lam, lam, Judge::Intro) m(App, app, Judge::Elim) \
20 m(Sigma, sigma, Judge::Form) m(Tuple, tuple, Judge::Intro) m(Extract, extract, Judge::Elim) m(Insert, insert, Judge::Intro | Judge::Elim) \
21 m(Arr, arr, Judge::Form) m(Pack, pack, Judge::Intro) \
22 m(Join, join, Judge::Form) m(Inj, inj, Judge::Intro) m(Match, match, Judge::Elim) m(Top, top, Judge::Intro) \
23 m(Meet, meet, Judge::Form) m(Merge, merge, Judge::Intro) m(Split, split, Judge::Elim) m(Bot, bot, Judge::Intro) \
24 m(Uniq, Uniq, Judge::Form) \
25 m(Nat, nat, Judge::Form) \
26 m(Idx, idx, Judge::Intro) m(Lit, lit, Judge::Intro) \
27 m(Axm, axm, Judge::Intro) \
28 m(Var, var, Judge::Intro) \
29 m(Global, global, Judge::Intro) \
30 m(Proxy, proxy, Judge::Intro) \
31 m(Hole, hole, Judge::Hole)
83#define CODE(node, name, _) node,
88#define CODE(node, name, _) +size_t(1)
96enum class Dep :
unsigned {
119template<>
struct fe::is_bit_enum<
mim::
Dep> : std::true_type {};
120template<>
struct fe::is_bit_enum<
mim::
Judge> : std::true_type {};
126#define MIM_PROJ(NAME, CONST) \
127 nat_t num_##NAME##s() CONST noexcept { return ((const Def*)NAME())->num_projs(); } \
128 nat_t num_t##NAME##s() CONST noexcept { return ((const Def*)NAME())->num_tprojs(); } \
129 const Def* NAME(nat_t a, nat_t i) CONST noexcept { return ((const Def*)NAME())->proj(a, i); } \
130 const Def* NAME(nat_t i) CONST noexcept { return ((const Def*)NAME())->proj(i); } \
131 const Def* t##NAME(nat_t i) CONST noexcept { return ((const Def*)NAME())->tproj(i); } \
132 template<nat_t A = std::dynamic_extent, class F> auto NAME##s(F f) CONST noexcept { \
133 return ((const Def*)NAME())->projs<A, F>(f); \
135 template<class F> auto t##NAME##s(F f) CONST noexcept { return ((const Def*)NAME())->tprojs<F>(f); } \
136 template<nat_t A = std::dynamic_extent> auto NAME##s() CONST noexcept { return ((const Def*)NAME())->projs<A>(); } \
137 auto t##NAME##s() CONST noexcept { return ((const Def*)NAME())->tprojs(); } \
138 template<class F> auto NAME##s(nat_t a, F f) CONST noexcept { return ((const Def*)NAME())->projs<F>(a, f); } \
139 auto NAME##s(nat_t a) CONST noexcept { return ((const Def*)NAME())->projs(a); }
142template<
class P,
class D = Def>
class Setters {
144 P* super() {
return static_cast<P*
>(
this); }
145 const P* super()
const {
return static_cast<const P*
>(
this); }
149 template<
bool Ow = false>
const P*
set(Loc l )
const { super()->D::template
set<Ow>(l);
return super(); }
150 template<
bool Ow = false> P*
set(Loc l ) { super()->D::template
set<Ow>(l);
return super(); }
151 template<
bool Ow = false>
const P*
set( Sym s )
const { super()->D::template
set<Ow>(s);
return super(); }
152 template<
bool Ow = false> P*
set( Sym s ) { super()->D::template
set<Ow>(s);
return super(); }
153 template<
bool Ow = false>
const P*
set( std::string s)
const { super()->D::template
set<Ow>(std::move(s));
return super(); }
154 template<
bool Ow = false> P*
set( std::string s) { super()->D::template
set<Ow>(std::move(s));
return super(); }
155 template<
bool Ow = false>
const P*
set(Loc l, Sym s )
const { super()->D::template
set<Ow>(l, s);
return super(); }
156 template<
bool Ow = false> P*
set(Loc l, Sym s ) { super()->D::template
set<Ow>(l, s);
return super(); }
157 template<
bool Ow = false>
const P*
set(Loc l, std::string s)
const { super()->D::template
set<Ow>(l, std::move(s));
return super(); }
158 template<
bool Ow = false> P*
set(Loc l, std::string s) { super()->D::template
set<Ow>(l, std::move(s));
return super(); }
159 template<
bool Ow = false>
const P*
set(
Dbg d )
const { super()->D::template
set<Ow>(d);
return super(); }
160 template<
bool Ow = false> P*
set(
Dbg d ) { super()->D::template
set<Ow>(d);
return super(); }
197class Def :
public fe::RuntimeCast<Def> {
199 Def& operator=(
const Def&) =
delete;
200 Def(
const Def&) =
delete;
216 constexpr u32 gid() const noexcept {
return gid_; }
217 constexpr u32 tid() const noexcept {
return tid_; }
218 constexpr u32 mark() const noexcept {
return mark_; }
219 constexpr size_t hash() const noexcept {
return hash_; }
220 constexpr Node node() const noexcept {
return node_; }
241 const Def*
type() const noexcept {
return type_; }
253 assert(a.has_value());
260 template<
size_t N = std::dynamic_extent>
constexpr auto ops() const noexcept {
263 const Def*
op(
size_t i)
const noexcept {
return ops()[i]; }
264 constexpr size_t num_ops() const noexcept {
return num_ops_; }
298 const Def*
dep(
size_t i) const noexcept {
return deps()[i]; }
314 bool has_dep(
unsigned u)
const {
return dep_ & u; }
344 template<nat_t A = std::dynamic_extent,
class F>
auto projs(F f)
const {
345 using R = std::decay_t<
decltype(f(
this))>;
346 if constexpr (A == std::dynamic_extent) {
350 std::array<R, A> array;
351 for (
nat_t i = 0; i != A; ++i) array[i] = f(
proj(A, i));
359 using R = std::decay_t<
decltype(f(
this))>;
362 template<nat_t A = std::dynamic_extent>
auto projs()
const {
363 return projs<A>([](
const Def* def) {
return def; });
366 return tprojs([](
const Def* def) {
return def; });
369 return projs(a, [](
const Def* def) {
return def; });
429 template<
class T = Def,
bool invert = false> T*
isa_mut()
const {
430 if constexpr (std::is_same<T, Def>::value)
431 return mut_ ^ invert ?
const_cast<Def*
>(
this) :
nullptr;
433 return mut_ ^ invert ?
const_cast<Def*
>(
this)->
template isa<T>() :
nullptr;
437 template<
class T = Def,
bool invert = false> T*
as_mut()
const {
438 assert(mut_ ^ invert);
439 if constexpr (std::is_same<T, Def>::value)
440 return const_cast<Def*
>(
this);
442 return const_cast<Def*
>(
this)->
template as<T>();
458 template<
bool Ow = false>
const Def*
set(Loc l)
const {
if (Ow || !
dbg_.loc())
dbg_.set(l);
return this; }
459 template<
bool Ow = false> Def*
set(Loc l) {
if (Ow || !
dbg_.loc())
dbg_.set(l);
return this; }
460 template<
bool Ow = false>
const Def*
set(Sym s)
const {
if (Ow || !
dbg_.sym())
dbg_.set(s);
return this; }
461 template<
bool Ow = false> Def*
set(Sym s) {
if (Ow || !
dbg_.sym())
dbg_.set(s);
return this; }
462 template<
bool Ow = false>
const Def*
set( std::string s)
const {
set(
sym(std::move(s)));
return this; }
463 template<
bool Ow = false> Def*
set( std::string s) {
set(
sym(std::move(s)));
return this; }
464 template<
bool Ow = false>
const Def*
set(Loc l, Sym s )
const {
set(l);
set(s);
return this; }
465 template<
bool Ow = false> Def*
set(Loc l, Sym s ) {
set(l);
set(s);
return this; }
466 template<
bool Ow = false>
const Def*
set(Loc l, std::string s)
const {
set(l);
set(
sym(std::move(s)));
return this; }
467 template<
bool Ow = false> Def*
set(Loc l, std::string s) {
set(l);
set(
sym(std::move(s)));
return this; }
468 template<
bool Ow = false>
const Def*
set(
Dbg d)
const {
set(d.loc(), d.sym());
return this; }
469 template<
bool Ow = false> Def*
set(
Dbg d) {
set(d.loc(), d.sym());
return this; }
481 const Def*
debug_suffix(std::string)
const {
return this; }
505 template<
size_t N = std::dynamic_extent>
constexpr auto reduce(
const Def* arg)
const noexcept {
506 return reduce_(arg).span<N>();
516 virtual const Def*
check(
size_t,
const Def* def) {
return def; }
524 void dump(
int max)
const;
525 void write(
int max)
const;
526 void write(
int max,
const char* file)
const;
527 std::ostream&
stream(std::ostream&,
int max)
const;
534 void dot(std::ostream& os, uint32_t max = 0xFFFFFF,
bool types =
false)
const;
536 void dot(
const char* file =
nullptr, uint32_t max = 0xFFFFFF,
bool types =
false)
const;
537 void dot(
const std::string& file, uint32_t max = 0xFFFFFF,
bool types =
false)
const {
538 return dot(file.c_str(), max, types);
546 Sym
sym(
const char*)
const;
547 Sym
sym(std::string_view)
const;
548 Sym
sym(std::string)
const;
552 Defs reduce_(
const Def* arg)
const;
553 virtual Def*
stub_(
World&,
const Def*) { fe::unreachable(); }
558 Def*
unset(
size_t i);
559 const Def** ops_ptr()
const {
560 return reinterpret_cast<const Def**
>(
reinterpret_cast<char*
>(
const_cast<Def*
>(
this + 1)));
562 bool equal(
const Def* other)
const;
570 mutable World* world_;
590 mutable u32 tid_ = 0;
593 template<
class D,
size_t N>
friend class Sets;
596 friend std::ostream&
operator<<(std::ostream&,
const Def*);
620class Univ :
public Def,
public Setters<Univ> {
634class UMax :
public Def,
public Setters<UMax> {
647class UInc :
public Def,
public Setters<UInc> {
669class Type :
public Def,
public Setters<Type> {
700 template<
class T = flags_t> T
get()
const {
701 static_assert(
sizeof(T) <= 8);
712 template<
class T = nat_t>
static std::optional<T>
isa(
const Def* def) {
714 if (
auto lit = def->isa<Lit>())
return lit->get<T>();
717 template<
class T = nat_t>
static T
as(
const Def* def) {
return def->as<Lit>()->
get<T>(); }
756 static const Def*
isa(
const Def* def);
757 static const Def*
as(
const Def* def) {
762 static std::optional<nat_t>
isa_lit(
const Def* def);
765 assert(res.has_value());
787class Proxy :
public Def,
public Setters<Proxy> {
812class Global :
public Def,
public Setters<Global> {
822 const Def*
init()
const {
return op(0); }
bool is_set() const
Yields true if empty or the last op is set.
size_t num_deps() const noexcept
const Def * set(Dbg d) const
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.
void dot(std::ostream &os, uint32_t max=0xFFFFFF, bool types=false) const
T * as_mut() const
Asserts that this is a mutable, casts constness away and performs a static_cast to T.
const Var * has_var() const
As above if this is a mutable.
Defs deps() const noexcept
const T * isa_imm(R(T::*f)() const) const
bool has_dep(Dep d) const
bool is_elim() const noexcept
nat_t num_tprojs() const
As above but yields 1, if Flags::scalarize_threshold is exceeded.
nat_t as_lit_arity() const
bool has_dep(unsigned u) const
World & world() const noexcept
virtual const Def * check()
const Def * refine(size_t i, const Def *new_op) const
void dot(const std::string &file, uint32_t max=0xFFFFFF, bool types=false) const
std::string_view node_name() const
auto projs(nat_t a, F f) const
bool is_intro() const noexcept
constexpr auto ops() const noexcept
Vars local_vars() const
Vars reachable by following immutable deps().
constexpr flags_t flags() const noexcept
virtual Def * stub_(World &, const Def *)
const Def * set(std::string s) const
T * isa_mut() const
If this is mutable, it will cast constness away and perform a dynamic_cast to T.
constexpr u32 mark() const noexcept
Used internally by free_vars().
constexpr u32 tid() const noexcept
Trie id - only used in Trie.
auto projs(nat_t a) const
friend std::ostream & operator<<(std::ostream &, const Def *)
This will stream def as an operand.
const Def * debug_prefix(std::string) const
const Def * op(size_t i) const noexcept
bool is_immutabilizable()
virtual const Def * rebuild_(World &w, const Def *type, Defs ops) const =0
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.
const Def * proj(nat_t i) const
As above but takes Def::num_projs as arity.
auto projs(F f) const
Splits this Def via Def::projections into an Array (if A == std::dynamic_extent) or std::array (other...
bool is_open() const
Has free_vars()?
constexpr size_t hash() const noexcept
virtual const Def * immutabilize()
Tries to make an immutable from a mutable.
bool is_form() const noexcept
virtual const Def * check(size_t, const Def *def)
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 * set(Sym s) const
const Def * type() const noexcept
Yields the "raw" type of this Def (maybe nullptr).
const Def * dep(size_t i) 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.
const Def * set(Loc l, Sym s) const
bool is_meta() const noexcept
const Def * set(Loc l) const
void write(int max) const
Def * set(Loc l, std::string s)
Def * stub(const Def *type)
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::as_lit_arity(), if it is in fact a Lit, or 1 otherwise.
std::optional< nat_t > isa_lit_arity() const
std::ostream & stream(std::ostream &, int max) const
friend void swap(World &, World &) noexcept
constexpr u32 gid() const noexcept
Global id - unique number for this Def.
const Def * arity() const
Def * unset()
Unsets all Def::ops; works even, if not set at all or partially.
std::string unique_name() const
name + "_" + Def::gid
constexpr auto reduce(const Def *arg) const noexcept
const Def * set(Loc l, std::string s) const
const T * isa_imm() const
Muts users()
Set of mutables where this mutable is locally referenced.
bool is_closed() const
Has no free_vars()?
const Def * rebuild(const Def *type, Defs ops) const
Def * reset(size_t i, const Def *def)
Successively reset from left to right.
Def * stub(World &w, const Def *type)
u32 judge() const noexcept
const Def * tproj(nat_t i) const
As above but takes Def::num_tprojs.
const Var * has_var()
Only returns not nullptr, if Var of this mutable has ever been created.
constexpr size_t num_ops() const noexcept
void set(const Def *init)
Global * stub(const Def *type)
const Def * alloced_type() const
const Def * rebuild_(World &, const Def *, Defs) const override
static constexpr auto Node
Global * stub_(World &, const Def *) override
This node is a hole in the IR that is inferred by its context later on.
static constexpr auto Node
static nat_t as_lit(const Def *def)
const Def * rebuild_(World &, const Def *, Defs) const override
static constexpr nat_t size2bitwidth(nat_t n)
static constexpr nat_t bitwidth2size(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 const Def * as(const Def *def)
static constexpr auto Node
static std::optional< T > isa(const Def *def)
const Def * rebuild_(World &, const Def *, Defs) const override
static T as(const Def *def)
static constexpr auto Node
const Def * rebuild_(World &, const Def *, Defs) const override
const Def * rebuild_(World &, const Def *, Defs) const override
static constexpr auto Node
u32 pass() const
IPass::index within PassMan.
CRTP-based Mixin to declare setters for Def::loc & Def::name using a covariant return type.
const P * set(Sym s) const
const P * set(Loc l, Sym s) const
const P * set(Loc l) const
const P * set(Dbg d) const
const P * set(Loc l, std::string s) const
P * set(Loc l, std::string s)
const P * set(std::string s) const
const Def * rebuild_(World &, const Def *, Defs) const override
static constexpr auto Node
const Def * level() const
const Def * rebuild_(World &, const Def *, Defs) const override
static constexpr auto Node
static constexpr auto Node
const Def * rebuild_(World &, const Def *, Defs) const override
static constexpr auto Node
const Def * rebuild_(World &, const Def *, Defs) const override
const Def * rebuild_(World &, const Def *, Defs) const override
static constexpr auto Node
This is a thin wrapper for absl::InlinedVector<T, N, A> which is a drop-in replacement for std::vecto...
The World represents the whole program and manages creation of MimIR nodes (Defs).
#define MIM_PROJ(NAME, CONST)
Use as mixin to wrap all kind of Def::proj and Def::projs variants.
DefMap< const Def * > Def2Def
Vector< const Def * > DefVec
D bitcast(const S &src)
A bitcast from src of type S to D.
Dep
Tracks a dependency to certain Defs transitively through the Def::deps() up to but excliding mutables...
absl::flat_hash_map< K, V, GIDHash< K > > GIDMap
GIDSet< const Var * > VarSet
GIDMap< const Var *, To > VarMap
GIDMap< const Def *, To > DefMap
GIDSet< const Def * > DefSet
static constexpr size_t Num_Nodes
const Def *(*)(const Def *, const Def *, const Def *) NormalizeFn
Sets< const Var >::Set Vars
@ Intro
Term Introduction like λ(x: Nat): Nat = x.
@ Meta
Meta rules for Universe and Type levels.
@ Form
Type Formation like T -> T.
@ Elim
Term Elimination like f a.
absl::flat_hash_set< K, GIDHash< K > > GIDSet
Sort
TODO remove or fix this.
Vector(I, I, A=A()) -> Vector< typename std::iterator_traits< I >::value_type, Default_Inlined_Size< typename std::iterator_traits< I >::value_type >, A >
GIDMap< Def *, To > MutMap
VarMap< const Var * > Var2Var