MimIR 0.1
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
Classes | Namespaces | Macros | Typedefs
def.h File Reference
#include <optional>
#include <span>
#include <fe/assert.h>
#include <fe/cast.h>
#include <fe/enum.h>
#include "mim/config.h"
#include "mim/util/dbg.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...
 
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_IMM_NODE(m)
 
#define MIM_MUT_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
 

Enums that classify certain aspects of Defs.

#define CODE(node, _)
 
#define CODE(node, _)
 
enum class  mim::Node : node_t {
  mim::CODE ,
  mim::Lit ,
  mim::Axm ,
  mim::Var ,
  mim::Global ,
  mim::Proxy ,
  mim::Hole ,
  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::Inj ,
  mim::Match ,
  mim::Top ,
  mim::Meet ,
  mim::Merge ,
  mim::Split ,
  mim::Bot ,
  mim::Reform ,
  mim::Rule ,
  mim::Uniq ,
  mim::Nat ,
  mim::Idx
}
 
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...
 
enum class  mim::Mut {
  mim::Mut = 1 << 0 ,
  mim::Imm = 1 << 1
}
 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) +size_t(1) +size_t(1)
 

Macro Definition Documentation

◆ CODE [1/2]

#define CODE ( node,
_ )
Value:
node,

Definition at line 113 of file def.h.

◆ CODE [2/2]

#define CODE ( node,
_ )
Value:
+size_t(1)

Definition at line 113 of file def.h.

◆ MIM_IMM_NODE

#define MIM_IMM_NODE ( m)
Value:
m(Lit) \
m(Axm) \
m(Var) \
m(Proxy) \
m(Type) m(Univ) m(UMax) m(UInc) \
m(Pi) m(Lam) m(App) \
m(Sigma) m(Tuple) m(Extract) m(Insert) \
m(Arr) m(Pack) \
m(Join) m(Inj) m(Match) m(Top) \
m(Meet) m(Merge) m(Split) m(Bot) \
m(Rule) \
m(Uniq) \
m(Nat) \
m(Idx)

Definition at line 36 of file def.h.

Referenced by mim::Rewriter::rewrite_imm().

◆ MIM_MUT_NODE

#define MIM_MUT_NODE ( m)
Value:
m(Global) \
m(Hole) \
m(Pi) m(Lam) \
m(Sigma) \
m(Arr) m(Pack) \
m(Rule)

Definition at line 52 of file def.h.

Referenced by mim::Rewriter::rewrite_mut().

◆ MIM_NODE

#define MIM_NODE ( m)
Value:
m(Lit, Judge::Intro) /* keep this first - causes Lit to appear left in Def::less/Def::greater*/ \
m(Axm, Judge::Intro) \
m(Var, Judge::Intro) \
m(Global, Judge::Intro) \
m(Proxy, Judge::Intro) \
m(Hole, Judge::Hole ) \
m(Type, Judge::Meta ) m(Univ, Judge::Meta ) m(UMax, Judge::Meta) m(UInc, (Judge::Meta )) \
m(Pi, Judge::Form ) m(Lam, Judge::Intro) m(App, Judge::Elim) \
m(Sigma, Judge::Form ) m(Tuple, Judge::Intro) m(Extract, Judge::Elim) m(Insert, (Judge::Intro | Judge::Elim)) \
m(Arr, Judge::Form ) m(Pack, Judge::Intro) \
m(Join, Judge::Form ) m(Inj, Judge::Intro) m(Match, Judge::Elim) m(Top, (Judge::Intro )) \
m(Meet, Judge::Form ) m(Merge, Judge::Intro) m(Split, Judge::Elim) m(Bot, (Judge::Intro )) \
m(Reform, Judge::Form ) m(Rule, Judge::Intro) \
m(Uniq, Judge::Form ) \
m(Nat, Judge::Form ) \
m(Idx, Judge::Intro)

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 164 of file def.h.