def.h File Reference

#include <optional>
#include <fe/assert.h>
#include <fe/cast.h>
#include <fe/enum.h>
#include "mim/config.h"
#include "mim/util/dbg.h"
#include "mim/util/hash.h"
#include "mim/util/pool.h"
#include "mim/util/util.h"
#include "mim/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	mim::Ref
	Helper class to retrieve Infer::arg if present. More...
class	mim::Setters< P, D >
	CRTP-based Mixin to declare setters for Def::loc & Def::name using a covariant return type. More...
class	mim::Def
	Base class for all Defs. More...
struct	mim::DefDefHash
struct	mim::DefDefEq
class	mim::Var
class	mim::Univ
class	mim::UMax
class	mim::UInc
class	mim::Type
class	mim::Lit
class	mim::Nat
class	mim::Idx
	A built-in constant of type Nat -> *. More...
class	mim::Proxy
class	mim::Global

Namespaces
namespace	mim
namespace	mim::Node

Macros
#define	MIM_NODE(m)
#define	CODE(node, name)
#define	CODE(node, name)
#define	MIM_PROJ(NAME, CONST)
	Use as mixin to wrap all kind of Def::proj and Def::projs variants.

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

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

Variables
constexpr auto	mim::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)

Macro Definition Documentation

CODE [1/2]

#define CODE	(		node,
			name )

Value:

node,

Definition at line 39 of file def.h.

CODE [2/2]

#define CODE	(		node,
			name )

Value:

+size_t(1)

Definition at line 39 of file def.h.

MIM_NODE

#define MIM_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(Uniq,   Uniq)

Definition at line 18 of file def.h.

Referenced by mim::Def::node_name().

MIM_PROJ

#define MIM_PROJ	(		NAME,
			CONST )

Value:

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

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

Definition at line 141 of file def.h.