def.h File Reference

#include <optional>
#include <vector>
#include <fe/assert.h>
#include <fe/cast.h>
#include "thorin/config.h"
#include "thorin/util/dbg.h"
#include "thorin/util/hash.h"
#include "thorin/util/pool.h"
#include "thorin/util/print.h"
#include "thorin/util/util.h"
#include "thorin/util/vector.h"

Include dependency graph for def.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	thorin::Ref
	Helper class to retrieve Infer::arg if present. More...
class	thorin::Use
	References a user. More...
struct	thorin::UseHash
struct	thorin::UseEq
class	thorin::Def
	Base class for all Defs. More...
struct	thorin::DefDefHash
struct	thorin::DefDefEq
class	thorin::Var
class	thorin::Univ
class	thorin::UMax
class	thorin::UInc
class	thorin::Type
class	thorin::Lit
class	thorin::Nat
class	thorin::Idx
	A built-in constant of type .Nat -> *. More...
class	thorin::Proxy
class	thorin::Global

Namespaces
namespace	thorin
namespace	thorin::Node

Macros
#define	THORIN_NODE(m)
#define	CODE(node, name)   node,
#define	CODE(node, name)   +size_t(1)
#define	THORIN_PROJ(NAME, CONST)
	Use as mixin to wrap all kind of Def::proj and Def::projs variants.
#define	THORIN_SETTERS_(T)
	Use as mixin to declare setters for Def::loc & Def::name using a covariant return type.
#define	THORIN_SETTERS(T)   public:
#define	THORIN_DEF_MIXIN(T)

Typedefs
Def
GIDSet / GIDMap keyed by Def::gid of conset Def*.
template<class To >
using	thorin::DefMap = GIDMap< const Def *, To >
using	thorin::DefSet = GIDSet< const Def * >
using	thorin::Def2Def = DefMap< const Def * >
using	thorin::Defs = View< const Def * >
using	thorin::DefVec = Vector< const Def * >
Def (Mutable)
GIDSet / GIDMap keyed by Def::gid of Def*.
template<class To >
using	thorin::MutMap = GIDMap< Def *, To >
using	thorin::MutSet = GIDSet< Def * >
using	thorin::Mut2Mut = MutMap< Def * >
using	thorin::Muts = PooledSet< Def * >
DefDef
using	thorin::DefDef = std::tuple< const Def *, const Def * >
template<class To >
using	thorin::DefDefMap = absl::flat_hash_map< DefDef, To, DefDefHash, DefDefEq >
using	thorin::DefDefSet = absl::flat_hash_set< DefDef, DefDefHash, DefDefEq >

Enumerations
enum	: node_t {   thorin::Node::Type ,   thorin::Node::Univ ,   thorin::Node::UMax ,   thorin::Node::UInc ,   thorin::Node::Pi ,   thorin::Node::Lam ,   thorin::Node::App ,   thorin::Node::Sigma ,   thorin::Node::Tuple ,   thorin::Node::Extract ,   thorin::Node::Insert ,   thorin::Node::Arr ,   thorin::Node::Pack ,   thorin::Node::Join ,   thorin::Node::Vel ,   thorin::Node::Test ,   thorin::Node::Top ,   thorin::Node::Meet ,   thorin::Node::Ac ,   thorin::Node::Pick ,   thorin::Node::Bot ,   thorin::Node::Proxy ,   thorin::Node::Axiom ,   thorin::Node::Lit ,   thorin::Node::Nat ,   thorin::Node::Idx ,   thorin::Node::Var ,   thorin::Node::Infer ,   thorin::Node::Global ,   thorin::Node::Singleton }
Dep
enum class	thorin::Dep : unsigned {   thorin::None = 0 ,   thorin::Axiom = 1 << 0 ,   thorin::Infer = 1 << 1 ,   thorin::Mut = 1 << 2 ,   thorin::Proxy = 1 << 3 ,   thorin::Var = 1 << 4 }

Functions
std::ostream operator
std::ostream &	thorin::operator<< (std::ostream &os, const Def *def)
	This will stream def as an operand.
std::ostream &	thorin::operator<< (std::ostream &, Ref)
Formatted Output
Provides a printf-like interface to format s with args and puts it into os. Use {} as a placeholder within your format string s. By default, os << t will be used to stream the appropriate argument: print(os, "int: {}, float: {}", 23, 42.f); You can also place a function as argument to inject arbitrary code: print(os, "int: {}, fun: {}, float: {}", 23, [&]() { os << "hey :)"}, 42.f); There is also a variant to pass os to the function, if you don't have easy access to it: print(os, "int: {}, fun: {}, float: {}", 23, [&](auto& os) { os << "hey :)"}, 42.f); You can put a std::ranges::range as argument. This will output a list - using the given specifier as separator. Each element elem of the range will be output via os << elem: std::vector<int> v = {0, 1, 2, 3}; print(os, "v: {, }", v); If you have a std::ranges::range that needs to be formatted in a more complicated way, bundle it with an Elem: std::vector<int> v = {3, 2, 1, 0}; size_t i = 0; print(os, "v: {, }", Elem(v, [&](auto elem) { print(os, "{}: {}", i++, elem); })); You again have the option to pass os to the bundled function: std::vector<int> v = {3, 2, 1, 0}; size_t i = 0; print(os, "v: {, }", Elem(v, [&](auto& os, auto elem) { print(os, "{}: {}", i++, elem); })); * Use `{{` or `}}` to literally output `{` or `{`: print(os, "{{{}}}", 23); // "{23}" See also Tab
template<class T = std::logic_error, class... Args>
void	thorin::error (const Def *def, const char *fmt, Args &&... args)

Variables
constexpr auto	thorin::Node::Num_Nodes = size_t(0) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1) +size_t(1)

Var
GIDSet / GIDMap keyed by Var::gid of const Var*.
enum class	thorin::Sort {   thorin::Term ,   thorin::Type ,   thorin::Kind ,   thorin::Space ,   thorin::Univ ,   thorin::Level }
template<class To >
using	thorin::VarMap = GIDMap< const Var *, To >
using	thorin::VarSet = GIDSet< const Var * >
using	thorin::Var2Var = VarMap< const Var * >
using	thorin::Vars = PooledSet< const Var * >
using	thorin::NormalizeFn = Ref(*)(Ref, Ref, Ref)
using	thorin::Uses = absl::flat_hash_set< Use, UseHash, UseEq >

Macro Definition Documentation

CODE [1/2]

#define CODE	(		node,
			name
	)		node,

Definition at line 40 of file def.h.

CODE [2/2]

#define CODE	(		node,
			name
	)		+size_t(1)

Definition at line 40 of file def.h.

THORIN_DEF_MIXIN

#define THORIN_DEF_MIXIN

(

T

)

Value:

public:                                             \
    THORIN_SETTERS(T)                               \
    static constexpr auto Node = Node::T;           \
                                                    \
private:                                            \
    Ref rebuild_(World&, Ref, Defs) const override; \
    friend class World;

Definition at line 198 of file def.h.

THORIN_NODE

#define THORIN_NODE

(

m

)

Value:

    m(Type, type)       m(Univ, univ)   m(UMax, umax)       m(UInc, uinc)     \
    m(Pi, pi)           m(Lam, lam)     m(App, app)                           \
    m(Sigma, sigma)     m(Tuple, tuple) m(Extract, extract) m(Insert, insert) \
    m(Arr, arr)         m(Pack, pack)                                         \
    m(Join, join)       m(Vel, vel)     m(Test, test)       m(Top, top)       \
    m(Meet, meet)       m(Ac,  ac )     m(Pick, pick)       m(Bot, bot)       \
    m(Proxy, proxy)                                                           \
    m(Axiom, axiom)                                                           \
    m(Lit, lit)                                                               \
    m(Nat, nat)         m(Idx, idx)                                           \
    m(Var, var)                                                               \
    m(Infer, infer)                                                           \
    m(Global, global)                                                         \
    m(Singleton, singleton)

Definition at line 19 of file def.h.

THORIN_PROJ

#define THORIN_PROJ	(		NAME,
			CONST
	)

Value:

    nat_t num_##NAME##s() CONST { return ((const Def*)NAME())->num_projs(); }                                 \
    nat_t num_t##NAME##s() CONST { return ((const Def*)NAME())->num_tprojs(); }                               \
    Ref NAME(nat_t a, nat_t i) CONST { return ((const Def*)NAME())->proj(a, i); }                             \
    Ref NAME(nat_t i) CONST { return ((const Def*)NAME())->proj(i); }                                         \
    Ref t##NAME(nat_t i) CONST { return ((const Def*)NAME())->tproj(i); }                                     \
    template<nat_t A = std::dynamic_extent, class F> auto NAME##s(F f) CONST {                                \
        return ((const Def*)NAME())->projs<A, F>(f);                                                          \
    }                                                                                                         \
    template<class F> auto t##NAME##s(F f) CONST { return ((const Def*)NAME())->tprojs<F>(f); }               \
    template<nat_t A = std::dynamic_extent> auto NAME##s() CONST { return ((const Def*)NAME())->projs<A>(); } \
    auto t##NAME##s() CONST { return ((const Def*)NAME())->tprojs(); }                                        \
    template<class F> auto NAME##s(nat_t a, F f) CONST { return ((const Def*)NAME())->projs<F>(a, f); }       \
    auto NAME##s(nat_t a) CONST { return ((const Def*)NAME())->projs(a); }

Use as mixin to wrap all kind of Def::proj and Def::projs variants.

Definition at line 159 of file def.h.

THORIN_SETTERS

#define THORIN_SETTERS

(

T

)

public:

Definition at line 193 of file def.h.

THORIN_SETTERS_

#define THORIN_SETTERS_

(

T

)

Value:

public:                                                                                                                    \
    template<bool Ow = false> const T* set(Loc l               ) const { if (Ow || !dbg_.loc) dbg_.loc = l; return this; } \
    template<bool Ow = false>       T* set(Loc l               )       { if (Ow || !dbg_.loc) dbg_.loc = l; return this; } \
    template<bool Ow = false> const T* set(       Sym s        ) const { if (Ow || !dbg_.sym) dbg_.sym = s; return this; } \
    template<bool Ow = false>       T* set(       Sym s        )       { if (Ow || !dbg_.sym) dbg_.sym = s; return this; } \
    template<bool Ow = false> const T* set(       std::string s) const {         set(sym(std::move(s))); return this; }    \
    template<bool Ow = false>       T* set(       std::string s)       {         set(sym(std::move(s))); return this; }    \
    template<bool Ow = false> const T* set(Loc l, Sym s        ) const { set(l); set(s);                 return this; }    \
    template<bool Ow = false>       T* set(Loc l, Sym s        )       { set(l); set(s);                 return this; }    \
    template<bool Ow = false> const T* set(Loc l, std::string s) const { set(l); set(sym(std::move(s))); return this; }    \
    template<bool Ow = false>       T* set(Loc l, std::string s)       { set(l); set(sym(std::move(s))); return this; }    \
    template<bool Ow = false> const T* set(Dbg d) const { set(d.loc, d.sym); return this; }                                \
    template<bool Ow = false>       T* set(Dbg d)       { set(d.loc, d.sym); return this; }

Use as mixin to declare setters for Def::loc & Def::name using a covariant return type.

Definition at line 176 of file def.h.