#include <concepts>
#include <algorithm>
#include <format>
#include <limits>
#include <optional>
#include <span>
#include <type_traits>
#include <utility>
#include <fe/algo.h>
#include <fe/cast.h>
#include <fe/container.h>
#include <fe/enum.h>
#include <fe/patricia.h>
#include <fe/term.h>
#include <fe/vector.h>
#include "mim/config.h"
#include "mim/util/dbg.h"
#include "mim/util/gid.h"
#include "mim/util/types.h"

Include dependency graph for def.h:

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

Classes
struct	mim::DefKey
	Grants fe::Patricia access to Def::gid_. More...
class	mim::Setters< P, D >
	CRTP-based mixin to declare setters for Def::loc & Def::name using a covariant return type. More...
struct	mim::DotConfig
	Options for Def::dot, World::dot, and Nest::dot. More...
class	mim::Def
	Base class for all Defs. More...
class	mim::Var
	A variable introduced by a binder (mutable). More...
class	mim::Level
class	mim::LMax
class	mim::LSucc
class	mim::Type
class	mim::Lit
class	mim::Nat
class	mim::Idx
	A built-in constant of type Nat -> *. More...
class	mim::Proxy
	Used as intermediate value during optimizatinos such as Analysis. More...

Namespaces
namespace	mim

Concepts
concept	mim::Projector
concept	mim::DefPred
	Used by Def::proj & friends.
concept	mim::MutPred

Macros
#define	MIM_NODE(X)
#define	MIM_IMM_NODE(X)
#define	MIM_MUT_NODE(X)
#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 const 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 = fe::View<const Def*>
using	mim::DefVec = fe::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::Muts = fe::Patricia<Def, DefKey>::Set
Var
GIDSet / GIDMap keyed by Var::gid of const Var*.
template<class To>
using	mim::VarMap = GIDMap<const Var*, To>
using	mim::Vars = fe::Patricia<const Var, DefKey>::Set

Functions
auto	mim::type_of (const Def *def)
	Def::unfold_type of `def` for a diagnostic - Level is the one Def that has no type at all.
void	mim::post_order (Def mut, MutSet &done, fe::Vector< Def > &res, MutPred auto descend, MutPred auto collect)
	Appends the mutables reachable from `mut` via Def::deps / Def::local_muts to `res` in post-order: callees first, so a name is always bound before its uses.

Enums that classify certain aspects of Defs.
#define	CODE(node, _)
#define	CODE(node, _)
#define	CODE(node)
#define	CODE(node)
#define	CODE(node)
#define	CODE(node, judge)
enum class	mim::Node : node_t { mim::Lit , mim::Axm , mim::Var , mim::Proxy , mim::Hole , mim::Type , mim::Level , mim::LMax , mim::LSucc , 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::Variant , mim::Top , mim::Bot , mim::Reform , mim::Rule , mim::Single , mim::Wrap , mim::Nom , mim::Name , mim::Struc , mim::Nat , mim::Idx }
enum class	mim::MutNode : node_t { mim::Hole = node_t(Node::Hole) , mim::Pi = node_t(Node::Pi) , mim::Lam = node_t(Node::Lam) , mim::Sigma = node_t(Node::Sigma) , mim::Arr = node_t(Node::Arr) , mim::Pack = node_t(Node::Pack) , mim::Variant = node_t(Node::Variant) , mim::Rule = node_t(Node::Rule) }
	The Nodes that may be mutable, with the same values as their Node. 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) +size_t(1) +size_t(1) +size_t(1)
constexpr bool	mim::is_mut_node (Node node) noexcept

Class Documentation

◆ mim::DotConfig

struct mim::DotConfig

Options for Def::dot, World::dot, and Nest::dot.

Note: Def::dot and World::dot honor DotConfig::max. Nest::dot only honors DotConfig::dark.

Definition at line 241 of file def.h.

Class Members
bool	dark = false	Drop the white background and lighten the edges for a dark backdrop.
bool	default_filter = false	Show Lam::filter() even if it has its default value.
bool	follow_types = false	Follow Def::type() dependencies.
bool	inline_consts = false	Wire up literals, axioms, etc. with normal edges instead of detaching them.
bool	lean_labels = false	Label a node <node_name> <unique_name> instead of the HTML table. This drops the per-op ports, so its edges dock at the node itself.
int	max = std::numeric_limits<int>::max()	Maximum recursion depth.
bool	no_tooltip = false	Omit the per-node tooltip; it is by far the bulkiest part of the output.
bool	show_hidden = false	Render otherwise-transparent detached edges (Var→binder back-edges, shared literals/axioms, type edges) with a visible color.

Macro Definition Documentation