19 m(Lit, Judge::Intro) \
20 m(Axm, Judge::Intro) \
21 m(Var, Judge::Intro) \
22 m(Global, Judge::Intro) \
23 m(Proxy, Judge::Intro) \
24 m(Hole, Judge::Hole ) \
25 m(Type, Judge::Meta ) m(Univ, Judge::Meta ) m(UMax, Judge::Meta) m(UInc, (Judge::Meta )) \
26 m(Pi, Judge::Form ) m(Lam, Judge::Intro) m(App, Judge::Elim) \
27 m(Sigma, Judge::Form ) m(Tuple, Judge::Intro) m(Extract, Judge::Elim) m(Insert, (Judge::Intro | Judge::Elim)) \
28 m(Arr, Judge::Form ) m(Pack, Judge::Intro) \
29 m(Join, Judge::Form ) m(Inj, Judge::Intro) m(Match, Judge::Elim) m(Top, (Judge::Intro )) \
30 m(Meet, Judge::Form ) m(Merge, Judge::Intro) m(Split, Judge::Elim) m(Bot, (Judge::Intro )) \
31 m(Reform, Judge::Form ) m(Rule, Judge::Intro) \
32 m(Uniq, Judge::Form ) \
33 m(Nat, Judge::Form ) \
36#define MIM_IMM_NODE(m) \
41 m(Type) m(Univ) m(UMax) m(UInc) \
43 m(Sigma) m(Tuple) m(Extract) m(Insert) \
45 m(Join) m(Inj) m(Match) m(Top) \
46 m(Meet) m(Merge) m(Split) m(Bot) \
52#define MIM_MUT_NODE(m) \
105using fe::operator<=>;
113#define CODE(node, _) node,
118#define CODE(node, _) +size_t(1)
123enum class Dep :
unsigned {
155template<>
struct fe::is_bit_enum<
mim::
Dep> : std::true_type {};
156template<>
struct fe::is_bit_enum<
mim::
Judge> : std::true_type {};
157template<>
struct fe::is_bit_enum<
mim::
Mut> : std::true_type {};
164#define MIM_PROJ(NAME, CONST) \
165 nat_t num_##NAME##s() CONST noexcept { return ((const Def*)NAME())->num_projs(); } \
166 nat_t num_t##NAME##s() CONST noexcept { return ((const Def*)NAME())->num_tprojs(); } \
167 const Def* NAME(nat_t a, nat_t i) CONST noexcept { return ((const Def*)NAME())->proj(a, i); } \
168 const Def* NAME(nat_t i) CONST noexcept { return ((const Def*)NAME())->proj(i); } \
169 const Def* t##NAME(nat_t i) CONST noexcept { return ((const Def*)NAME())->tproj(i); } \
170 template<nat_t A = std::dynamic_extent, class F> \
171 auto NAME##s(F f) CONST noexcept { \
172 return ((const Def*)NAME())->projs<A, F>(f); \
175 auto t##NAME##s(F f) CONST noexcept { \
176 return ((const Def*)NAME())->tprojs<F>(f); \
178 template<nat_t A = std::dynamic_extent> \
179 auto NAME##s() CONST noexcept { \
180 return ((const Def*)NAME())->projs<A>(); \
182 auto t##NAME##s() CONST noexcept { return ((const Def*)NAME())->tprojs(); } \
184 auto NAME##s(nat_t a, F f) CONST noexcept { \
185 return ((const Def*)NAME())->projs<F>(a, f); \
187 auto NAME##s(nat_t a) CONST noexcept { return ((const Def*)NAME())->projs(a); }
190template<
class P,
class D = Def>
193 __declspec(empty_bases)
197 P* super() {
return static_cast<P*
>(
this); }
198 const P* super()
const {
return static_cast<const P*
>(
this); }
202 template<
bool Ow = false>
const P*
set(Loc l )
const { super()->D::template
set<Ow>(l);
return super(); }
203 template<
bool Ow = false> P*
set(Loc l ) { super()->D::template
set<Ow>(l);
return super(); }
204 template<
bool Ow = false>
const P*
set( Sym s )
const { super()->D::template
set<Ow>(s);
return super(); }
205 template<
bool Ow = false> P*
set( Sym s ) { super()->D::template
set<Ow>(s);
return super(); }
206 template<
bool Ow = false>
const P*
set( std::string s)
const { super()->D::template
set<Ow>(std::move(s));
return super(); }
207 template<
bool Ow = false> P*
set( std::string s) { super()->D::template
set<Ow>(std::move(s));
return super(); }
208 template<
bool Ow = false>
const P*
set(Loc l, Sym s )
const { super()->D::template
set<Ow>(l, s);
return super(); }
209 template<
bool Ow = false> P*
set(Loc l, Sym s ) { super()->D::template
set<Ow>(l, s);
return super(); }
210 template<
bool Ow = false>
const P*
set(Loc l, std::string s)
const { super()->D::template
set<Ow>(l, std::move(s));
return super(); }
211 template<
bool Ow = false> P*
set(Loc l, std::string s) { super()->D::template
set<Ow>(l, std::move(s));
return super(); }
212 template<
bool Ow = false>
const P*
set(
Dbg d )
const { super()->D::template
set<Ow>(d);
return super(); }
213 template<
bool Ow = false> P*
set(
Dbg d ) { super()->D::template
set<Ow>(d);
return super(); }
251class Def :
public fe::RuntimeCast<Def> {
253 Def& operator=(
const Def&) =
delete;
254 Def(
const Def&) =
delete;
270 constexpr u32 gid() const noexcept {
return gid_; }
271 constexpr u32 tid() const noexcept {
return tid_; }
272 constexpr u32 mark() const noexcept {
return mark_; }
273 constexpr size_t hash() const noexcept {
return hash_; }
274 constexpr Node node() const noexcept {
return node_; }
295 const Def*
type() const noexcept {
return type_; }
304 template<
size_t N = std::dynamic_extent>
305 constexpr auto ops() const noexcept {
308 const Def*
op(
size_t i)
const noexcept {
return ops()[i]; }
309 constexpr size_t num_ops() const noexcept {
return num_ops_; }
343 const Def*
dep(
size_t i) const noexcept {
return deps()[i]; }
359 bool has_dep(
unsigned u)
const {
return dep_ & u; }
389 template<nat_t A = std::dynamic_extent,
class F>
391 using R = std::decay_t<
decltype(f(
this))>;
392 if constexpr (A == std::dynamic_extent) {
395 std::array<R, A> array;
396 for (
nat_t i = 0; i != A; ++i)
397 array[i] = f(
proj(A, i));
409 using R = std::decay_t<
decltype(f(
this))>;
412 template<nat_t A = std::dynamic_extent>
414 return projs<A>([](
const Def* def) {
return def; });
417 return tprojs([](
const Def* def) {
return def; });
420 return projs(a, [](
const Def* def) {
return def; });
481 template<
class T = Def,
bool invert = false>
483 if constexpr (std::is_same<T, Def>::value)
484 return mut_ ^ invert ?
const_cast<Def*
>(
this) :
nullptr;
486 return mut_ ^ invert ?
const_cast<Def*
>(
this)->
template isa<T>() :
nullptr;
490 template<
class T = Def,
bool invert = false>
492 assert(mut_ ^ invert);
493 if constexpr (std::is_same<T, Def>::value)
494 return const_cast<Def*
>(
this);
496 return const_cast<Def*
>(
this)->
template as<T>();
512 template<
bool Ow = false>
const Def*
set(Loc l)
const {
if (Ow || !
dbg_.loc())
dbg_.set(l);
return this; }
513 template<
bool Ow = false> Def*
set(Loc l) {
if (Ow || !
dbg_.loc())
dbg_.set(l);
return this; }
514 template<
bool Ow = false>
const Def*
set(Sym s)
const {
if (Ow || !
dbg_.sym())
dbg_.set(s);
return this; }
515 template<
bool Ow = false> Def*
set(Sym s) {
if (Ow || !
dbg_.sym())
dbg_.set(s);
return this; }
516 template<
bool Ow = false>
const Def*
set( std::string s)
const {
set<Ow>(
sym(std::move(s)));
return this; }
517 template<
bool Ow = false> Def*
set( std::string s) {
set<Ow>(
sym(std::move(s)));
return this; }
518 template<
bool Ow = false>
const Def*
set(Loc l, Sym s )
const {
set<Ow>(l);
set<Ow>(s);
return this; }
520 template<
bool Ow = false>
const Def*
set(Loc l, std::string s)
const {
set<Ow>(l);
set<Ow>(
sym(std::move(s)));
return this; }
521 template<
bool Ow = false> Def*
set(Loc l, std::string s) {
set<Ow>(l);
set<Ow>(
sym(std::move(s)));
return this; }
522 template<
bool Ow = false>
const Def*
set(
Dbg d)
const {
set<Ow>(d.loc(), d.sym());
return this; }
523 template<
bool Ow = false> Def*
set(
Dbg d) {
set<Ow>(d.loc(), d.sym());
return this; }
535 const Def*
debug_suffix(std::string)
const {
return this; }
559 template<
size_t N = std::dynamic_extent>
560 constexpr auto reduce(
const Def* arg)
const {
561 return reduce_(arg).span<N>();
575 virtual const Def*
check([[maybe_unused]]
size_t i,
const Def* def) {
return def; }
597 void dump(
int max)
const;
598 void write(
int max)
const;
599 void write(
int max,
const char* file)
const;
600 std::ostream&
stream(std::ostream&,
int max)
const;
611 [[nodiscard]]
static Cmp cmp(
const Def* a,
const Def* b);
612 [[nodiscard]]
static bool less(
const Def* a,
const Def* b);
613 [[nodiscard]]
static bool greater(
const Def* a,
const Def* b);
619 void dot(std::ostream& os, uint32_t max = 0xFFFFFF,
bool types =
false)
const;
621 void dot(
const char* file =
nullptr, uint32_t max = 0xFFFFFF,
bool types =
false)
const;
622 void dot(
const std::string& file, uint32_t max = 0xFFFFFF,
bool types =
false)
const {
623 return dot(file.c_str(), max, types);
631 Sym
sym(
const char*)
const;
632 Sym
sym(std::string_view)
const;
633 Sym
sym(std::string)
const;
637 Defs reduce_(
const Def* arg)
const;
638 virtual Def*
stub_(
World&,
const Def*) { fe::unreachable(); }
644 const Def** ops_ptr()
const {
645 return reinterpret_cast<const Def**
>(
reinterpret_cast<char*
>(
const_cast<Def*
>(
this + 1)));
647 bool equal(
const Def* other)
const;
650 [[nodiscard]]
static bool cmp_(
const Def* a,
const Def* b);
658 mutable World* world_;
678 mutable u32 tid_ = 0;
681 template<
class D,
size_t N>
685 friend std::ostream&
operator<<(std::ostream&,
const Def*);
710class Univ :
public Def,
public Setters<Univ> {
725class UMax :
public Def,
public Setters<UMax> {
729 static constexpr size_t Num_Ops = std::dynamic_extent;
741class UInc :
public Def,
public Setters<UInc> {
764class Type :
public Def,
public Setters<Type> {
796 template<
class T = flags_t>
798 static_assert(
sizeof(T) <= 8);
809 template<
class T = nat_t>
810 static std::optional<T>
isa(
const Def* def) {
812 if (
auto lit = def->isa<Lit>())
return lit->get<T>();
815 template<
class T = nat_t>
816 static T
as(
const Def* def) {
817 return def->as<Lit>()->
get<T>();
859 static const Def*
isa(
const Def* def);
860 static const Def*
as(
const Def* def) {
865 static std::optional<nat_t>
isa_lit(
const Def* def);
868 assert(res.has_value());
891class Proxy :
public Def,
public Setters<Proxy> {
906 static constexpr size_t Num_Ops = std::dynamic_extent;
917class Global :
public Def,
public Setters<Global> {
927 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 * zonk_mut() const
If *mutable, zonks all ops and tries to immutabilize it; otherwise just zonk.
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
virtual const Def * check(size_t i, const Def *def)
Checks whether the ith operand can be set to def.
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
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.
const Def * zonk() const
If Holes have been filled, reconstruct the program without them.
bool has_dep(unsigned u) const
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.
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
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
bool is_mutable() const noexcept
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.
const Def * set(Loc l, Sym s) const
static bool less(const Def *a, const Def *b)
bool is_meta() const noexcept
static bool greater(const Def *a, const Def *b)
const Def * set(Loc l) const
void write(int max) const
Def * set(Loc l, std::string s)
Def * stub(const Def *type)
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.
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.
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
constexpr auto reduce(const Def *arg) const
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 * 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 final
static constexpr size_t Num_Ops
Global * stub_(World &, const Def *) final
static constexpr auto Node
This node is a hole in the IR that is inferred by its context later on.
const Def * rebuild_(World &, const Def *, Defs) const final
static constexpr auto Node
static nat_t as_lit(const Def *def)
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 constexpr size_t Num_Ops
static const Def * as(const Def *def)
static constexpr auto Node
static std::optional< T > isa(const Def *def)
static T as(const Def *def)
static constexpr size_t Num_Ops
const Def * rebuild_(World &, const Def *, Defs) const final
static constexpr auto Node
const Def * rebuild_(World &, const Def *, Defs) const final
static constexpr size_t Num_Ops
static constexpr size_t Num_Ops
const Def * rebuild_(World &, const Def *, Defs) const final
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
static constexpr size_t Num_Ops
static constexpr auto Node
const Def * level() const
const Def * rebuild_(World &, const Def *, Defs) const final
static constexpr auto Node
static constexpr size_t Num_Ops
const Def * rebuild_(World &, const Def *, Defs) const final
static constexpr auto Node
const Def * rebuild_(World &, const Def *, Defs) const final
static constexpr size_t Num_Ops
static constexpr size_t Num_Ops
static constexpr auto Node
const Def * rebuild_(World &, const Def *, Defs) const final
const Def * rebuild_(World &, const Def *, Defs) const final
static constexpr auto Node
static constexpr size_t Num_Ops
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
@ Imm
Node may be immmutable.
@ 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
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