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/sets.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::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

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

Typedefs
using	mim::NormalizeFn = const Def* (*)(const Def*, const Def*, const Def*)
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 = Sets<Def>::Set
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 = Sets<const Var>::Set
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>

Enums that classify certain aspects of Defs.
#define	CODE(node, name, _)
#define	CODE(node, name, _)
enum class	mim::Node : node_t {   mim::CODE ,   mim::Type ,   mim::Univ ,   mim::UMax ,   mim::UInc ,   mim::Pi ,   mim::Lam ,   mim::App ,   mim::Sigma ,   mim::Tuple ,   mim::Extract ,   mim::Insert ,   mim::Arr ,   mim::Pack ,   mim::Join ,   mim::Vel ,   mim::Test ,   mim::Top ,   mim::Meet ,   mim::Ac ,   mim::Pick ,   mim::Bot ,   mim::Uniq ,   mim::Nat ,   mim::Idx ,   mim::Lit ,   mim::Axiom ,   mim::Var ,   mim::Global ,   mim::Proxy ,   mim::Hole }
enum class	mim::Sort {   mim::Term ,   mim::Type ,   mim::Kind ,   mim::Space ,   mim::Univ ,   mim::Level }
	TODO remove or fix this. More...
enum class	mim::Dep : unsigned {   mim::None = 0 ,   mim::Mut = 1 << 0 ,   mim::Var = 1 << 1 ,   mim::Hole = 1 << 2 ,   mim::Proxy = 1 << 3 }
	Tracks a dependency to certain Defs transitively through the Def::deps() up to but excliding mutables. More...
enum class	mim::Judge : u32 {   mim::Form = 1 << 0 ,   mim::Intro = 1 << 1 ,   mim::Elim = 1 << 2 ,   mim::Meta = 1 << 3 ,   mim::Hole = 1 << 4 }
	Judgement. More...
static constexpr size_t	mim::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 84 of file def.h.

CODE [2/2]

#define CODE	(		node,
			name,
			_ )

Value:

+size_t(1)

Definition at line 84 of file def.h.

MIM_NODE

#define MIM_NODE

(

m

)

Value:

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

Definition at line 18 of file def.h.

Referenced by mim::Def::judge(), and 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(); }                               \
    const Def* NAME(nat_t a, nat_t i) CONST noexcept { return ((const Def*)NAME())->proj(a, i); }                      \
    const Def* NAME(nat_t i) CONST noexcept { return ((const Def*)NAME())->proj(i); }                                  \
    const Def* 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 127 of file def.h.