def.h File Reference

#include <optional>
#include <fe/assert.h>
#include <fe/cast.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::Use
	References a user. More...
struct	mim::UseHash
struct	mim::UseEq
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.
#define	MIM_SETTERS_(T)
	Use as mixin to declare setters for Def::loc & Def::name using a covariant return type.
#define	MIM_SETTERS(T)
#define	MIM_DEF_MIXIN(T)

Typedefs
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*>
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::Singleton }
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 }

Functions
std::ostream operator
std::ostream &	mim::operator<< (std::ostream &os, const Def *def)
	This will stream def as an operand.
std::ostream &	mim::operator<< (std::ostream &, Ref)

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)

Var
GIDSet / GIDMap keyed by Var::gid of const Var*.
enum class	mim::Sort {   mim::Term ,   mim::Type ,   mim::Kind ,   mim::Space ,   mim::Univ ,   mim::Level }
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*>
using	mim::NormalizeFn = Ref (*)(Ref, Ref, Ref)
using	mim::Uses = absl::flat_hash_set<Use, UseHash, UseEq>

Macro Definition Documentation

CODE [1/2]

#define CODE	(		node,
			name )

Value:

node,

Definition at line 38 of file def.h.

CODE [2/2]

#define CODE	(		node,
			name )

Value:

+size_t(1)

Definition at line 38 of file def.h.

MIM_DEF_MIXIN

#define MIM_DEF_MIXIN

(

T

)

Value:

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

Definition at line 196 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(Singleton, singleton)

Definition at line 17 of file def.h.

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

MIM_PROJ

#define MIM_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 157 of file def.h.

MIM_SETTERS

#define MIM_SETTERS

(

T

)

Value:

public:

Definition at line 191 of file def.h.

MIM_SETTERS_

#define MIM_SETTERS_

(

T

)

Value:

public:                                                                                                                      \
    template<bool Ow = false> const T* set(Loc l               ) const { if (Ow || !dbg_.loc()) dbg_.set(l); return this; } \
    template<bool Ow = false>       T* set(Loc l               )       { if (Ow || !dbg_.loc()) dbg_.set(l); return this; } \
    template<bool Ow = false> const T* set(       Sym s        ) const { if (Ow || !dbg_.sym()) dbg_.set(s); return this; } \
    template<bool Ow = false>       T* set(       Sym s        )       { if (Ow || !dbg_.sym()) dbg_.set(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 174 of file def.h.