Namespaces
namespace	ast
namespace	plug
namespace	sexpr
namespace	dl
namespace	lct
namespace	sys

Classes
class	Axm
class	Emitter
class	Hole
	This node is a hole in the IR that is inferred by its context later on. More...
class	Checker
class	Setters
	CRTP-based mixin to declare setters for Def::loc & Def::name using a covariant return type. More...
struct	DotConfig
	Options for Def::dot and World::dot. More...
class	Def
	Base class for all Defs. More...
class	Var
	A variable introduced by a binder (mutable). More...
class	Univ
class	UMax
class	UInc
class	Type
class	Lit
class	Nat
class	Idx
	A built-in constant of type Nat -> *. More...
class	Proxy
class	Global
class	Driver
	Some "global" variables needed all over the place. More...
struct	Flags
	Compiler switches that must be saved and looked up in later phases of compilation. More...
class	Pi
	A dependent function type. More...
class	Lam
	A function. More...
class	App
class	Bound
	Common base for TBound. More...
class	TBound
	Specific Bound depending on `Up`. More...
class	Merge
	Constructs a Meet value. More...
class	Inj
	Constructs a Join value. More...
class	Split
	Picks the aspect of a Meet [value](Pick::value) by its [type](Def::type). More...
class	Match
	Scrutinize Match::scrutinee() and dispatch to Match::arms. More...
class	Ext
	Common base for TExtremum. More...
class	TExt
	Extremum. Either Top (`Up`) or Bottom. More...
class	Uniq
	A singleton wraps a type into a higher order type. More...
class	Nest
	Builds a nesting tree for all mutables/binders. More...
class	Phase
	A Phase performs one self-contained task over the whole World. More...
class	Analysis
	Traverses the current World using Rewriter infrastructure while staying in the same world. More...
class	RWPhase
	Rebuilds old_world() into new_world() and then swaps them. More...
class	Repl
	An RWPhase that searches for a pattern and replaces it. More...
class	Cleanup
	Removes unreachable and dead code by rebuilding the whole World into a new one and swapping them afterwards. More...
class	PhaseMan
	Organizes several Phases into a pipeline. More...
class	ClosedMutPhase
	Transitively visits all reachable, closed mutables in the World. More...
class	NestPhase
	Like ClosedMutPhase but computes a Nest for each NestPhase::visit. More...
class	BetaRed
	Inlines in post-order all Lams that occur exactly once in the program. More...
class	BranchNormalize
	Normalizes branches: η-expands non-Lam branch targets so that both sides of a (f, t)#cond branch are Lams, as later phases and the backends expect. More...
class	EtaConv
	Combined η-normalization: folds η-reduction and η-expansion into a single, idempotent phase. More...
class	LamSpec
	Specializes a Lam at its call site by inlining all Pi-typed (i.e. higher-order) arguments. More...
class	PrefixCleanup
class	RetWrap
class	Scalarize
	Perform Scalarization (= Argument simplification). More...
class	TailRecElim
	Eliminates tail recursion: A returning Lam f that calls itself with its own ret var as continuation is split into a wrapper rec (same signature) and a loop basic block (signature without the ret var); the recursive call becomes a jump to loop. More...
struct	Version
struct	Plugin
	Basic info and registration function pointer to be returned from a specific plugin. More...
struct	Annex
	Holds info about an entity defined within a Plugin (called Annex). More...
class	Rewriter
	Recurseivly rebuilds part of a program into the provided World w.r.t. Rewriter::map. More...
class	VarRewriter
	Extends Rewriter for variable substitution. More...
class	Zonker
class	Reform
	Type formation of a rewrite Rule. More...
class	Rule
	A rewrite rule. More...
class	Use
	const Def*erences a user. More...
struct	UseHash
struct	UseEq
class	Scheduler
class	Prod
	Base class for Sigma and Tuple. More...
class	Sigma
	A dependent tuple type. More...
class	Tuple
	Data constructor for a Sigma. More...
class	Seq
	Base class for Arr and Pack. More...
class	Arr
	A (possibly paramterized) Array. More...
class	Pack
	A (possibly paramterized) Tuple. More...
class	Extract
	Extracts from a Sigma or Array-typed Extract::tuple the element at position Extract::index. More...
class	Insert
	Creates a new Tuple / Pack by inserting Insert::value at position Insert::index into Insert::tuple. More...
class	Select
	Matches (ff, tt)#cond - where cond is not a Literal. More...
class	Branch
	Matches (ff, tt)#cond arg where cond is not a Literal. More...
class	Dispatch
	Matches a dispatch through a jump table of the form: (target_0, target_1, ...)#index arg where index is not a Literal. More...
class	Error
struct	Dbg
struct	FNV1
struct	FNV1< 4 >
struct	FNV1< 8 >
class	Log
	Facility to log what you are doing. More...
class	Profiler
	Records wall-clock timings for (possibly nested) Phase runs and reports them in various formats. More...
class	Sets
class	Span
	This is a thin wrapper for std::span<T, N> with the following additional features: More...
class	unique_queue
struct	GIDHash
struct	GIDLt
class	Restore
	RAII guard that restores `ref` to its current value at the end of the scope. More...
class	Vector
	This is a thin wrapper for absl::InlinedVector<T, N, A> which is a drop-in replacement for std::vector<T, A>. More...
class	World
	The World represents the whole program and manages creation of MimIR nodes (Defs). More...

Concepts
concept	annex_with_subs
concept	annex_without_subs
concept	Vectorlike
	Something which behaves like std::vector or std::array.
concept	Enum

Typedefs
using	NormalizeFn = const Def* ()(const Def, const Def, const Def)
using	Phases = std::deque<std::unique_ptr<Phase>>
using	Uses = absl::flat_hash_set<Use, UseHash, UseEq>
template<class T, size_t N = std::dynamic_extent>
using	View = Span<const T, N>
Def
GIDSet / GIDMap keyed by Def::gid of const Def*.
template<class To>
using	DefMap = GIDMap<const Def*, To>
using	DefSet = GIDSet<const Def*>
using	Def2Def = DefMap<const Def*>
using	Defs = View<const Def*>
using	DefVec = Vector<const Def*>
Def (Mutable)
GIDSet / GIDMap keyed by Def::gid of Def*.
template<class To>
using	MutMap = GIDMap<Def*, To>
using	MutSet = GIDSet<Def*>
using	Mut2Mut = MutMap<Def*>
using	Muts = Sets<Def>::Set
Var
GIDSet / GIDMap keyed by Var::gid of const Var*.
template<class To>
using	VarMap = GIDMap<const Var*, To>
using	VarSet = GIDSet<const Var*>
using	Var2Var = VarMap<const Var*>
using	Vars = Sets<const Var>::Set
Lam
GIDSet / GIDMap keyed by Lam::gid of Lam*.
template<class To>
using	LamMap = GIDMap<Lam*, To>
using	LamSet = GIDSet<Lam*>
using	Lam2Lam = LamMap<Lam*>
Lattice
using	Bot = TExt<false>
using	Top = TExt<true>
using	Meet = TBound<false>
	AKA intersection.
using	Join = TBound<true>
	AKA union.
Aliases for some Base Types
using	s8 = int8_t
using	u8 = uint8_t
using	s16 = int16_t
using	u16 = uint16_t
using	s32 = int32_t
using	u32 = uint32_t
using	s64 = int64_t
using	u64 = uint64_t
using	u1 = bool
using	f32 = float
using	f64 = double
using	level_t = u64
using	nat_t = u64
using	node_t = u8
using	flags_t = u64
using	plugin_t = u64
using	tag_t = u8
using	sub_t = u8
Width to Signed/Unsigned/Float
template<int w>
using	w2u = typename detail::w2u_<w>::type
template<int w>
using	w2s = typename detail::w2s_<w>::type
template<int w>
using	w2f = typename detail::w2f_<w>::type
GID
template<class K, class V>
using	GIDMap = absl::flat_hash_map<K, V, GIDHash<K>>
template<class K>
using	GIDSet = absl::flat_hash_set<K, GIDHash<K>>
template<class K, class V>
using	GIDNodeMap = absl::node_hash_map<K, V, GIDHash<K>>
template<class K>
using	GIDNodeSet = absl::node_hash_set<K, GIDHash<K>>

Enumerations
enum class	Assoc
	Associativity of an infix expression. More...
enum class	Prec
	Expression precedences used by the parser and the dumper; ordered low to high. More...

Functions
void	optimize (World &)
	Runs _compile or _default_compile, if available (in this order).
std::ostream &	operator<< (std::ostream &os, const Error::Msg &msg)
template<size_t I, class T, size_t N>
constexpr decltype(auto)	get (Span< T, N > span) noexcept
std::ostream &	operator<< (std::ostream &os, const Def *def)
	This will stream `def` as an operand.
static const Pi *	isa_flattenable (const Def *def)
	The only Pis we ever reshape: immutable (non-dependent) continuations.
static void	collect (DefSet &set, const Def *def)
	Collects `def's` immutable subtree into `set`; stops at mutables.
std::tuple< const Var , const Def >	tuple_of_dict (World &world, Def2Def &v2v)
static void	post_order (const Nest &nest, const Nest::Node *node, Scheduler::Schedule &res, MutSet &done)
static void	flatten_umax (DefVec &ops, const Def *def)
bool	isa_indicies (const Def *def)
constexpr Assoc	prec_assoc (Prec p)
	Associativity of precedence level `p`.
is_commutative/is_associative
template<class Id>
constexpr bool	is_commutative (Id)
template<class Id>
constexpr bool	is_associative (Id id)
constexpr bool	is_commutative (plug::core::nat id)
constexpr bool	is_commutative (plug::core::ncmp id)
constexpr bool	is_commutative (plug::core::wrap id)
constexpr bool	is_commutative (plug::core::icmp id)
constexpr bool	is_commutative (plug::core::bit2 id)
constexpr bool	is_associative (plug::core::bit2 id)
constexpr bool	is_associative (plug::core::nat id)
constexpr bool	is_associative (plug::core::ncmp id)
constexpr bool	is_associative (plug::core::icmp id)
constexpr bool	is_associative (plug::core::wrap id)
constexpr bool	is_commutative (plug::math::extrema)
constexpr bool	is_commutative (plug::math::arith id)
constexpr bool	is_commutative (plug::math::cmp id)
constexpr bool	is_associative (plug::math::arith id)
Helpers to work with Functions
const App *	isa_callee (const Def *def, size_t i)
Lam *	isa_optimizable (Lam *lam)
	These are Lams that are.
std::pair< const App , Lam >	isa_apped_mut_lam (const Def *def)
const Def *	compose_cn (const Def f, const Def g)
	The high level view is:
Helpers to work with Tuples/Sigmas/Arrays/Packs
bool	is_unit (const Def *)
std::string	tuple2str (const Def *)
const Def *	tuple_of_types (const Def *t)
Concatenation
Works for Tuples, Packs, Sigmas, and Arrays alike.
DefVec	cat (Defs, Defs)
DefVec	cat (const Def *a, Defs bs)
DefVec	cat (Defs as, const Def *b)
DefVec	cat (nat_t n, nat_t m, const Def a, const Def b)
const Def *	cat_tuple (nat_t n, nat_t m, const Def a, const Def b)
const Def *	cat_sigma (nat_t n, nat_t m, const Def a, const Def b)
const Def *	cat_tuple (World &, Defs, Defs)
const Def *	cat_sigma (World &, Defs, Defs)
const Def *	cat_tuple (const Def *a, Defs bs)
const Def *	cat_tuple (Defs as, const Def *b)
const Def *	cat_sigma (const Def *a, Defs bs)
const Def *	cat_sigma (Defs as, const Def *b)
Formatted Output
template<class... Args>
void	error (Loc loc, std::format_string< Args... > f, Args &&... args)
Simple Hash
See Wikipedia.
constexpr uint32_t	murmur3 (uint32_t h) noexcept
constexpr uint64_t	splitmix64 (uint64_t h) noexcept
constexpr size_t	hash (size_t h) noexcept
FNV-1 Hash
See Wikipedia.
template<class T>
constexpr size_t	hash_combine (size_t seed, T v) noexcept
consteval size_t	hash_begin () noexcept
template<class T>
constexpr size_t	hash_begin (T val) noexcept
Deduction Guides
template<class I, class E>
	Span (I, E) -> Span< std::remove_reference_t< std::iter_reference_t< I > > >
template<class T, size_t N>
	Span (T(&)[N]) -> Span< T, N >
template<class T, size_t N>
	Span (std::array< T, N > &) -> Span< T, N >
template<class T, size_t N>
	Span (const std::array< T, N > &) -> Span< const T, N >
template<class R>
	Span (R &&) -> Span< std::remove_reference_t< std::ranges::range_reference_t< R > > >
template<Vectorlike Vec>
	Span (Vec &) -> Span< typename Vec::value_type, std::dynamic_extent >
template<Vectorlike Vec>
	Span (const Vec &) -> Span< const typename Vec::value_type, std::dynamic_extent >
template<class I, class A = std::allocator<typename std::iterator_traits<I>::value_type>>
	Vector (I, I, A=A()) -> Vector< typename std::iterator_traits< I >::value_type, Default_Inlined_Size< typename std::iterator_traits< I >::value_type >, A >
User-Defined Literals
constexpr s8	operator""_s8 (unsigned long long int s)
constexpr u8	operator""_u8 (unsigned long long int u)
constexpr s16	operator""_s16 (unsigned long long int s)
constexpr u16	operator""_u16 (unsigned long long int u)
constexpr s32	operator""_s32 (unsigned long long int s)
constexpr u32	operator""_u32 (unsigned long long int u)
constexpr s64	operator""_s64 (unsigned long long int s)
constexpr u64	operator""_u64 (unsigned long long int u)
constexpr nat_t	operator""_n (unsigned long long int i)
rem
float	rem (float a, float b)
double	rem (double a, double b)
long double	rem (long double a, long double b)
Utility Functions
template<class D, class S> requires (std::is_trivially_copyable_v<S> && std::is_trivially_copyable_v<D>)
constexpr D	bitcast_resize (const S &src) noexcept
	A bitcast from `src` of type `S` to `D`, supporting different sizes.
constexpr std::uint64_t	pad (std::uint64_t offset, std::uint64_t align) noexcept
Algorithms
template<class I, class T, class L>
constexpr I	binary_find (I begin, I end, T val, L lt) noexcept
constexpr std::string_view	subview (std::string_view s, size_t i, size_t n=std::string_view::npos) noexcept
	Like std::string::substr, but works on std::string_view instead.
void	find_and_replace (std::string &str, std::string_view what, std::string_view repl)
	Replaces all occurrences of `what` with `repl`.
Helpers for Containers
template<class S>
auto	pop (S &s) -> decltype(s.top(), typename S::value_type())
template<class Q>
auto	pop (Q &q) -> decltype(q.front(), typename Q::value_type())
template<class C, class K>
auto	lookup (const C &container, const K &key)
	Yields pointer to element (or the element itself if it is already a pointer), if found and nullptr otherwise.
template<class C, class K>
auto	assert_lookup (C &container, const K &key)
	Looks up `key` in `container`, asserts that it exists, and returns the mapped value.
template<class C, class... Args>
auto	assert_emplace (C &container, Args &&... args)
	Invokes emplace on `container`, asserts that insertion actually happened, and returns the iterator.
erase
template<class T, size_t N, class A, class U>
Vector< T, N, A >::size_type	erase (Vector< T, N, A > &c, const U &value) noexcept
template<class T, size_t N, class A, class Pred>
Vector< T, N, A >::size_type	erase_if (Vector< T, N, A > &c, Pred pred) noexcept

Variables
template<class T>
static constexpr size_t	Default_Inlined_Size = std::max((size_t)1, 4 * sizeof(size_t) / sizeof(T))
	Use up to 4 words (i.e., 4 * sizeof(size_t)) of inlined storage, rounded up.
static constexpr auto	BitmaskWidth = sizeof(u64) * 8
	Number of params a single u64 keep-bitmask can represent; wider doms fall back to the ⊤ sentinel.

Enums that classify certain aspects of Defs.
enum class	Node : node_t { Lit , Axm , Var , Global , Proxy , Hole , Type , Univ , UMax , UInc , Pi , Lam , App , Sigma , Tuple , Extract , Insert , Arr , Pack , Join , Inj , Match , Top , Meet , Merge , Split , Bot , Reform , Rule , Uniq , Nat , Idx }
enum class	Dep : unsigned { None = 0 , Mut = 1 << 0 , Var = 1 << 1 , Hole = 1 << 2 , Proxy = 1 << 3 }
	Tracks whether a Def transitively depends - through its Def::deps() but only up to (and excluding) the next mutable - on certain kinds of Defs. More...
enum class	Judge : u32 { Form = 1 << 0 , Intro = 1 << 1 , Elim = 1 << 2 , Meta = 1 << 3 , Hole = 1 << 4 }
	Judgement. More...
enum class	Mut { Mut = 1 << 0 , Imm = 1 << 1 }
	Classifies whether a Node may occur as a mutable, an immutable, or both. More...
static constexpr size_t	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)

Plugin Interface
See also Plugin
using	Normalizers = absl::flat_hash_map<flags_t, NormalizeFn>
using	Flags2Phases = absl::flat_hash_map<flags_t, std::function<std::unique_ptr<Phase>(World&)>>
	Maps an axiom of a Phase to a function that creates one.
mim::Plugin	mim_get_plugin ()

Class Documentation

◆ mim::DotConfig

struct mim::DotConfig

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

Note: Def::dot and World::dot honor DotConfig::max; World::dot also honors DotConfig::all_annexes.

Definition at line 217 of file def.h.

Class Members
bool	all_annexes = false	Include all annexes - even if unused (World::dot only).
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.
int	max = std::numeric_limits<int>::max()	Maximum recursion depth.
bool	show_hidden = false	Render otherwise-transparent detached edges (Var→binder back-edges, shared literals/axioms, type edges) with a visible color.

◆ mim::FNV1

struct mim::FNV1

template<size_t>
struct mim::FNV1< size_t >

Magic numbers for FNV-1 hash.

Definition at line 47 of file hash.h.

Inheritance diagram for mim::FNV1< size_t >:

[legend]

Typedef Documentation

◆ Bot

using mim::Bot = TExt<false>

Definition at line 176 of file lattice.h.

◆ Def2Def

using mim::Def2Def = DefMap<const Def*>

Definition at line 77 of file def.h.

◆ DefMap

template<class To>

using mim::DefMap = GIDMap<const Def*, To>

Definition at line 75 of file def.h.

◆ Defs

using mim::Defs = View<const Def*>

Definition at line 78 of file def.h.

◆ DefSet

using mim::DefSet = GIDSet<const Def*>

Definition at line 76 of file def.h.

◆ DefVec

using mim::DefVec = Vector<const Def*>

Definition at line 79 of file def.h.

◆ f32

using mim::f32 = float

Definition at line 34 of file types.h.

◆ f64

using mim::f64 = double

Definition at line 35 of file types.h.

◆ Flags2Phases

using mim::Flags2Phases = absl::flat_hash_map<flags_t, std::function<std::unique_ptr<Phase>(World&)>>

Maps an axiom of a Phase to a function that creates one.

Definition at line 25 of file plugin.h.

◆ flags_t

using mim::flags_t = u64

Definition at line 39 of file types.h.

◆ GIDMap

template<class K, class V>

using mim::GIDMap = absl::flat_hash_map<K, V, GIDHash<K>>

Definition at line 168 of file util.h.

◆ GIDNodeMap

template<class K, class V>

using mim::GIDNodeMap = absl::node_hash_map<K, V, GIDHash<K>>

Definition at line 170 of file util.h.

◆ GIDNodeSet

template<class K>

using mim::GIDNodeSet = absl::node_hash_set<K, GIDHash<K>>

Definition at line 171 of file util.h.

◆ GIDSet

template<class K>

using mim::GIDSet = absl::flat_hash_set<K, GIDHash<K>>

Definition at line 169 of file util.h.

◆ Join

using mim::Join = TBound<true>

AKA union.

Definition at line 179 of file lattice.h.

◆ Lam2Lam

using mim::Lam2Lam = LamMap<Lam*>

Definition at line 221 of file lam.h.

◆ LamMap

template<class To>

using mim::LamMap = GIDMap<Lam*, To>

Definition at line 219 of file lam.h.

◆ LamSet

using mim::LamSet = GIDSet<Lam*>

Definition at line 220 of file lam.h.

◆ level_t

using mim::level_t = u64

Definition at line 36 of file types.h.

◆ Meet

using mim::Meet = TBound<false>

AKA intersection.

Definition at line 178 of file lattice.h.

◆ Mut2Mut

using mim::Mut2Mut = MutMap<Def*>

Definition at line 88 of file def.h.

◆ MutMap

template<class To>

using mim::MutMap = GIDMap<Def*, To>

Definition at line 86 of file def.h.

◆ Muts

using mim::Muts = Sets<Def>::Set

Definition at line 89 of file def.h.

◆ MutSet

using mim::MutSet = GIDSet<Def*>

Definition at line 87 of file def.h.

◆ nat_t

using mim::nat_t = u64

Definition at line 37 of file types.h.

◆ node_t

using mim::node_t = u8

Definition at line 38 of file types.h.

◆ NormalizeFn

using mim::NormalizeFn = const Def* (*)(const Def*, const Def*, const Def*)

Definition at line 102 of file def.h.

◆ Normalizers

using mim::Normalizers = absl::flat_hash_map<flags_t, NormalizeFn>

Definition at line 22 of file plugin.h.

◆ Phases

using mim::Phases = std::deque<std::unique_ptr<Phase>>

Definition at line 20 of file phase.h.

◆ plugin_t

using mim::plugin_t = u64

Definition at line 40 of file types.h.

◆ s16

using mim::s16 = int16_t

Definition at line 27 of file types.h.

◆ s32

using mim::s32 = int32_t

Definition at line 27 of file types.h.

◆ s64

using mim::s64 = int64_t

Definition at line 27 of file types.h.

◆ s8

using mim::s8 = int8_t

Definition at line 27 of file types.h.

◆ sub_t

using mim::sub_t = u8

Definition at line 42 of file types.h.

◆ tag_t

using mim::tag_t = u8

Definition at line 41 of file types.h.

◆ Top

using mim::Top = TExt<true>

Definition at line 177 of file lattice.h.

◆ u1

using mim::u1 = bool

Definition at line 30 of file types.h.

◆ u16

using mim::u16 = uint16_t

Definition at line 27 of file types.h.

◆ u32

using mim::u32 = uint32_t

Definition at line 27 of file types.h.

◆ u64

using mim::u64 = uint64_t

Definition at line 27 of file types.h.

◆ u8

using mim::u8 = uint8_t

Definition at line 27 of file types.h.

◆ Uses

using mim::Uses = absl::flat_hash_set<Use, UseHash, UseEq>

Definition at line 42 of file schedule.h.

◆ Var2Var

using mim::Var2Var = VarMap<const Var*>

Definition at line 98 of file def.h.

◆ VarMap

template<class To>

using mim::VarMap = GIDMap<const Var*, To>

Definition at line 96 of file def.h.

◆ Vars

using mim::Vars = Sets<const Var>::Set

Definition at line 99 of file def.h.

◆ VarSet

using mim::VarSet = GIDSet<const Var*>

Definition at line 97 of file def.h.

◆ View

template<class T, size_t N = std::dynamic_extent>

using mim::View = Span<const T, N>

Definition at line 102 of file span.h.

◆ w2f

template<int w>

using mim::w2f = typename detail::w2f_<w>::type

Definition at line 68 of file types.h.

◆ w2s

template<int w>

using mim::w2s = typename detail::w2s_<w>::type

Definition at line 67 of file types.h.

◆ w2u

template<int w>

using mim::w2u = typename detail::w2u_<w>::type

Definition at line 66 of file types.h.

Enumeration Type Documentation

◆ Assoc

enum class mim::ast::Assoc

strong

Associativity of an infix expression.

Definition at line 35 of file tok.h.

◆ Dep

enum class mim::Dep : unsigned

strong

Tracks whether a Def transitively depends - through its Def::deps() but only up to (and excluding) the next mutable - on certain kinds of Defs.

See also: Def::has_dep

Enumerator
None	Depends on nothing of interest.
Mut	Depends on a mutable.
Var	Depends on a Var.
Hole	Depends on a Hole.
Proxy	Depends on a Proxy.

Definition at line 120 of file def.h.

◆ Judge

enum class mim::Judge : u32

strong

Judgement.

Enumerator
Form	Type Formation like T -> T.
Intro	Term Introduction like λ(x: Nat): Nat = x.
Elim	Term Elimination like f a.
Meta	Meta rules for Universe and Type levels.
Hole	Special rule for Hole.

Definition at line 129 of file def.h.

◆ Mut

enum class mim::Mut

strong

Classifies whether a Node may occur as a mutable, an immutable, or both.

See also: Immutables vs. Mutables

Enumerator
Mut	Node may be mutable.
Imm	Node may be immutable.

Definition at line 141 of file def.h.

◆ Node

enum class mim::Node : node_t

strong

Enumerator
Lit
Axm
Var
Global
Proxy
Hole
Type
Univ
UMax
UInc
Pi
Lam
App
Sigma
Tuple
Extract
Insert
Arr
Pack
Join
Inj
Match
Top
Meet
Merge
Split
Bot
Reform
Rule
Uniq
Nat
Idx

Definition at line 107 of file def.h.

◆ Prec

enum class mim::ast::Prec

strong

Expression precedences used by the parser and the dumper; ordered low to high.

Definition at line 38 of file tok.h.

Function Documentation

◆ assert_emplace()

template<class C, class... Args>

auto mim::assert_emplace	(	C &	container,
		Args &&...	args )

Invokes emplace on container, asserts that insertion actually happened, and returns the iterator.

Definition at line 117 of file util.h.

Referenced by mim::World::app(), mim::World::Annexes::attach(), mim::World::Externals::externalize(), mim::Phase::hook(), mim::Driver::load(), mim::World::reduce(), reg_phases(), and mim::Scheduler::Scheduler().

◆ assert_lookup()

template<class C, class K>

auto mim::assert_lookup	(	C &	container,
		const K &	key )

Looks up key in container, asserts that it exists, and returns the mapped value.

Definition at line 109 of file util.h.

◆ binary_find()

template<class I, class T, class L>

I mim::binary_find	(	I	begin,
		I	end,
		T	val,
		L	lt )

constexprnoexcept

Definition at line 56 of file util.h.

Referenced by mim::Bound::find().

◆ bitcast_resize()

template<class D, class S>
requires (std::is_trivially_copyable_v<S> && std::is_trivially_copyable_v<D>)

D mim::bitcast_resize ( const S & src )

constexprnoexcept

A bitcast from src of type S to D, supporting different sizes.

Definition at line 31 of file util.h.

Referenced by mim::Lit::get().

◆ cat() [1/4]

DefVec mim::cat	(	const Def *	a,
		Defs	bs )

inline

Definition at line 342 of file tuple.h.

References cat().

◆ cat() [2/4]

DefVec mim::cat	(	Defs	as,
		const Def *	b )

inline

Definition at line 343 of file tuple.h.

References cat().

◆ cat() [3/4]

DefVec mim::cat	(	Defs	a,
		Defs	b )

Definition at line 81 of file tuple.cpp.

Referenced by cat(), cat(), cat_sigma(), cat_sigma(), cat_tuple(), cat_tuple(), and mim::plug::tensor::phase::LowerMapReduce::rewrite_imm_App().

◆ cat() [4/4]

DefVec mim::cat	(	nat_t	n,
		nat_t	m,
		const Def *	a,
		const Def *	b )

Definition at line 89 of file tuple.cpp.

References mim::Def::proj().

◆ cat_sigma() [1/4]

const Def * mim::cat_sigma	(	const Def *	a,
		Defs	bs )

inline

Definition at line 355 of file tuple.h.

References cat_sigma().

◆ cat_sigma() [2/4]

const Def * mim::cat_sigma	(	Defs	as,
		const Def *	b )

inline

Definition at line 356 of file tuple.h.

References cat_sigma(), and mim::Def::world().

◆ cat_sigma() [3/4]

const Def * mim::cat_sigma	(	nat_t	n,
		nat_t	m,
		const Def *	a,
		const Def *	b )

Definition at line 101 of file tuple.cpp.

References cat().

Referenced by cat_sigma(), and cat_sigma().

◆ cat_sigma() [4/4]

const Def * mim::cat_sigma	(	World &	world,
		Defs	a,
		Defs	b )

Definition at line 104 of file tuple.cpp.

References cat(), and mim::World::sigma().

◆ cat_tuple() [1/4]

const Def * mim::cat_tuple	(	const Def *	a,
		Defs	bs )

inline

Definition at line 353 of file tuple.h.

References cat_tuple().

◆ cat_tuple() [2/4]

const Def * mim::cat_tuple	(	Defs	as,
		const Def *	b )

inline

Definition at line 354 of file tuple.h.

References cat_tuple(), and mim::Def::world().

◆ cat_tuple() [3/4]

const Def * mim::cat_tuple	(	nat_t	n,
		nat_t	m,
		const Def *	a,
		const Def *	b )

Definition at line 100 of file tuple.cpp.

References cat().

Referenced by cat_tuple(), cat_tuple(), mim::plug::tuple::normalize_cat(), and mim::plug::vec::normalize_cat().

◆ cat_tuple() [4/4]

const Def * mim::cat_tuple	(	World &	world,
		Defs	a,
		Defs	b )

Definition at line 103 of file tuple.cpp.

References cat(), and mim::World::tuple().

◆ collect()

void mim::collect	(	DefSet &	set,
		const Def *	def )

static

Collects def's immutable subtree into set; stops at mutables.

Definition at line 52 of file scalarize.cpp.

References collect(), mim::Def::deps(), and mim::Def::isa_mut().

Referenced by collect().

◆ compose_cn()

const Def * mim::compose_cn	(	const Def *	f,
		const Def *	g )

The high level view is:

f: B -> C
g: A -> B
f o g := λ x. f(g(x)) : A -> C

In CPS the types look like:

f:  Cn[B, Cn C]
g:  Cn[A, Cn B]
h = f o g
h:  Cn[A, cn C]
h = λ (a ret_h) = g (a, h')
h': Cn B
h'= λ b = f (b, ret_h)

Definition at line 62 of file lam.cpp.

References mim::Pi::dom(), mim::Pi::isa_returning(), and mim::Pi::ret_dom().

Referenced by mim::plug::autodiff::phase::Eval::augment_app().

◆ erase()

template<class T, size_t N, class A, class U>

Vector< T, N, A >::size_type mim::erase	(	Vector< T, N, A > &	c,
		const U &	value )

noexcept

Definition at line 85 of file vector.h.

Referenced by mim::plug::regex::normalize_disj().

◆ erase_if()

template<class T, size_t N, class A, class Pred>

Vector< T, N, A >::size_type mim::erase_if	(	Vector< T, N, A > &	c,
		Pred	pred )

noexcept

Definition at line 93 of file vector.h.

◆ error()

template<class... Args>

void mim::error	(	Loc	loc,
		std::format_string< Args... >	f,
		Args &&...	args )

Single Error that throws immediately.

Definition at line 114 of file dbg.h.

References error().

Referenced by mim::Arr::check(), mim::Pi::check(), mim::Reform::check(), mim::Rule::check(), dfa2matcher(), mim::ast::AxmDecl::emit(), mim::ast::ExtractExpr::emit_(), mim::ast::RetExpr::emit_(), mim::ast::LamDecl::emit_body(), mim::ast::encode_f(), error(), mim::World::extract(), mim::World::insert(), mim::World::lit(), mim::World::match(), mim::plug::refly::normalize_check_bot(), mim::plug::refly::normalize_equiv(), mim::World::seq(), mim::World::tuple(), mim::World::type(), mim::World::uinc(), and mim::World::umax().

◆ find_and_replace()

void mim::find_and_replace	(	std::string &	str,
		std::string_view	what,
		std::string_view	repl )

inline

Replaces all occurrences of what with repl.

Definition at line 73 of file util.h.

Referenced by mim::plug::autodiff::phase::Eval::augment_().

◆ flatten_umax()

void mim::flatten_umax	(	DefVec &	ops,
		const Def *	def )

static

Definition at line 133 of file world.cpp.

References flatten_umax().

Referenced by flatten_umax(), and mim::World::umax().

◆ get()

template<size_t I, class T, size_t N>

decltype(auto) mim::get ( Span< T, N > span )

constexprnoexcept

Definition at line 119 of file span.h.

Referenced by mim::ast::ExtractExpr::emit_(), mim::Lit::rebuild_(), mim::plug::matrix::phase::LowerMatrixMediumLevel::rewrite_imm_App(), mim::Rewriter::Rewriter(), and tuple_of_dict().

◆ hash()

size_t mim::hash ( size_t h )

inlineconstexprnoexcept

Definition at line 32 of file hash.h.

References murmur3(), and splitmix64().

Referenced by mim::Def::Def(), mim::GIDHash< T >::operator()(), and mim::UseHash::operator()().

◆ hash_begin() [1/2]

size_t mim::hash_begin ( )

inlineconstevalnoexcept

Definition at line 75 of file hash.h.

Referenced by mim::Def::Def(), mim::Def::Def(), hash_begin(), and mim::UseHash::operator()().

◆ hash_begin() [2/2]

template<class T>

size_t mim::hash_begin ( T val )

constexprnoexcept

Definition at line 78 of file hash.h.

References hash_begin(), and hash_combine().

◆ hash_combine()

template<class T>

size_t mim::hash_combine	(	size_t	seed,
		T	v )

constexprnoexcept

Definition at line 62 of file hash.h.

Referenced by mim::Def::Def(), mim::Def::Def(), hash_begin(), and mim::UseHash::operator()().

◆ is_associative() [1/7]

template<class Id>

bool mim::is_associative ( Id id )

constexpr

Warning: By default we assume that any commutative operation is also associative. Please provide a proper specialization if this is not the case.

Definition at line 168 of file axm.h.

References is_commutative().

◆ is_associative() [2/7]

bool mim::is_associative ( plug::core::bit2 id )

constexpr

Definition at line 110 of file core.h.

References mim::plug::core::and_, mim::plug::core::f, mim::plug::core::fst, mim::plug::core::nxor, mim::plug::core::or_, mim::plug::core::snd, mim::plug::core::t, and mim::plug::core::xor_.

◆ is_associative() [3/7]

bool mim::is_associative ( plug::core::icmp id )

constexpr

Definition at line 127 of file core.h.

References is_commutative().

◆ is_associative() [4/7]

bool mim::is_associative ( plug::core::nat id )

constexpr

Definition at line 125 of file core.h.

References is_commutative().

◆ is_associative() [5/7]

bool mim::is_associative ( plug::core::ncmp id )

constexpr

Definition at line 126 of file core.h.

References is_commutative().

◆ is_associative() [6/7]

bool mim::is_associative ( plug::core::wrap id )

constexpr

Definition at line 128 of file core.h.

References is_commutative().

◆ is_associative() [7/7]

bool mim::is_associative ( plug::math::arith id )

constexpr

Definition at line 133 of file math.h.

References is_commutative().

◆ is_commutative() [1/9]

template<class Id>

bool mim::is_commutative ( Id )

constexpr

Definition at line 162 of file axm.h.

Referenced by is_associative(), is_associative(), is_associative(), is_associative(), is_associative(), is_associative(), mim::plug::core::normalize_bit2(), mim::plug::core::normalize_nat(), and mim::plug::core::normalize_ncmp().

◆ is_commutative() [2/9]

bool mim::is_commutative ( plug::core::bit2 id )

constexpr

Definition at line 105 of file core.h.

◆ is_commutative() [3/9]

bool mim::is_commutative ( plug::core::icmp id )

constexpr

Definition at line 102 of file core.h.

References mim::plug::core::ne.

◆ is_commutative() [4/9]

bool mim::is_commutative ( plug::core::nat id )

constexpr

Definition at line 99 of file core.h.

◆ is_commutative() [5/9]

bool mim::is_commutative ( plug::core::ncmp id )

constexpr

Definition at line 100 of file core.h.

References mim::plug::core::ne.

◆ is_commutative() [6/9]

bool mim::is_commutative ( plug::core::wrap id )

constexpr

Definition at line 101 of file core.h.

References mim::plug::core::add, and mim::plug::core::mul.

◆ is_commutative() [7/9]

bool mim::is_commutative ( plug::math::arith id )

constexpr

Definition at line 131 of file math.h.

References mim::plug::math::add, and mim::plug::math::mul.

◆ is_commutative() [8/9]

bool mim::is_commutative ( plug::math::cmp id )

constexpr

Definition at line 132 of file math.h.

◆ is_commutative() [9/9]

bool mim::is_commutative ( plug::math::extrema )

constexpr

Definition at line 130 of file math.h.

◆ is_unit()

bool mim::is_unit ( const Def * def )

Definition at line 55 of file tuple.cpp.

References mim::World::sigma(), mim::Def::type(), and mim::Def::world().

◆ isa_apped_mut_lam()

std::pair< const App *, Lam * > mim::isa_apped_mut_lam ( const Def * def )

inline

Definition at line 357 of file lam.h.

◆ isa_callee()

const App * mim::isa_callee	(	const Def *	def,
		size_t	i )

inline

Definition at line 345 of file lam.h.

◆ isa_flattenable()

const Pi * mim::isa_flattenable ( const Def * def )

static

The only Pis we ever reshape: immutable (non-dependent) continuations.

Definition at line 13 of file scalarize.cpp.

References mim::Pi::isa_cn().

◆ isa_indicies()

bool mim::isa_indicies ( const Def * def )

Definition at line 366 of file world.cpp.

References mim::Idx::isa().

Referenced by mim::World::extract().

◆ isa_optimizable()

Lam * mim::isa_optimizable ( Lam * lam )

inline

These are Lams that are.

neither nullptr,
nor Lam::is_external,
nor Lam::is_annex,
nor Lam::is_unset.

Definition at line 352 of file lam.h.

References mim::Def::is_annex(), mim::Def::is_external(), and mim::Def::is_set().

Referenced by mim::LamSpec::rewrite_imm_App(), mim::Scalarize::rewrite_imm_App(), and mim::Scalarize::rewrite_mut_Lam().

◆ lookup()

template<class C, class K>

auto mim::lookup	(	const C &	container,
		const K &	key )

Yields pointer to element (or the element itself if it is already a pointer), if found and nullptr otherwise.

Warning: If the element is not already a pointer, this lookup will simply take the address of this element. This means that, e.g., a rehash of an absl::flat_hash_map will invalidate this pointer.

Definition at line 99 of file util.h.

Referenced by mim::World::annex(), mim::World::annex(), mim::Driver::get_fun_ptr(), mim::Driver::is_loaded(), mim::Driver::normalizer(), mim::World::Externals::operator[](), mim::Driver::phase(), mim::plug::clos::phase::LowerTypedClos::rewrite(), and mim::plug::mem::phase::SEO::rewrite_imm_App().

◆ mim_get_plugin()

mim::Plugin mim::mim_get_plugin ( )

To be implemented and exported by a plugin.

Returns: a filled Plugin.

References MIM_EXPORT.

Referenced by mim::Driver::load().

◆ murmur3()

uint32_t mim::murmur3 ( uint32_t h )

inlineconstexprnoexcept

Use for a single value to hash.

Definition at line 14 of file hash.h.

Referenced by hash().

◆ operator""_n()

nat_t mim::operator""_n ( unsigned long long int i )

constexpr

Definition at line 79 of file types.h.

◆ operator""_s16()

s16 mim::operator""_s16 ( unsigned long long int s )

constexpr

Definition at line 76 of file types.h.

References CODE4.

◆ operator""_s32()

s32 mim::operator""_s32 ( unsigned long long int s )

constexpr

Definition at line 76 of file types.h.

◆ operator""_s64()

s64 mim::operator""_s64 ( unsigned long long int s )

constexpr

Definition at line 76 of file types.h.

◆ operator""_s8()

s8 mim::operator""_s8 ( unsigned long long int s )

constexpr

Definition at line 76 of file types.h.

◆ operator""_u16()

u16 mim::operator""_u16 ( unsigned long long int u )

constexpr

Definition at line 76 of file types.h.

◆ operator""_u32()

u32 mim::operator""_u32 ( unsigned long long int u )

constexpr

Definition at line 76 of file types.h.

◆ operator""_u64()

u64 mim::operator""_u64 ( unsigned long long int u )

constexpr

Definition at line 76 of file types.h.

◆ operator""_u8()

u8 mim::operator""_u8 ( unsigned long long int u )

constexpr

Definition at line 76 of file types.h.

◆ operator<<() [1/2]

std::ostream & mim::operator<<	(	std::ostream &	os,
		const Def *	def )

This will stream def as an operand.

This is usually id(def) unless it can be displayed Inline.

Definition at line 520 of file dump.cpp.

◆ operator<<() [2/2]

std::ostream & mim::operator<<	(	std::ostream &	os,
		const Error::Msg &	msg )

inline

Definition at line 167 of file dbg.h.

◆ optimize()

void mim::optimize ( World & world )

Runs _compile or _default_compile, if available (in this order).

Definition at line 8 of file optimize.cpp.

References mim::Phase::apply(), mim::World::driver(), mim::World::externals(), mim::Def::internalize(), mim::World::Externals::mutate(), mim::Driver::phase(), mim::World::sym(), mim::Def::type(), and mim::App::uncurry_callee().

Referenced by main().

◆ pad()

std::uint64_t mim::pad	(	std::uint64_t	offset,
		std::uint64_t	align )

constexprnoexcept

Definition at line 44 of file util.h.

Referenced by mim::plug::core::normalize_trait().

◆ pop() [1/2]

template<class Q>

auto mim::pop ( Q & q ) -> decltype(q.front(), typename Q::value_type())

Definition at line 89 of file util.h.

◆ pop() [2/2]

template<class S>

auto mim::pop ( S & s ) -> decltype(s.top(), typename S::value_type())

Definition at line 82 of file util.h.

Referenced by mim::unique_queue< Set >::pop().

◆ post_order()

void mim::post_order	(	const Nest &	nest,
		const Nest::Node *	node,
		Scheduler::Schedule &	res,
		MutSet &	done )

static

Definition at line 105 of file schedule.cpp.

References mim::Nest::Node::children(), mim::Def::deps(), mim::Nest::Node::mut(), mim::Nest::Node::Children::nodes(), and post_order().

Referenced by post_order(), and mim::Scheduler::schedule().

◆ prec_assoc()

Assoc mim::ast::prec_assoc ( Prec p )

constexpr

Associativity of precedence level p.

Definition at line 45 of file tok.h.

◆ rem() [1/3]

double mim::rem	(	double	a,
		double	b )

inline

Definition at line 88 of file types.h.

◆ rem() [2/3]

float mim::rem	(	float	a,
		float	b )

inline

Definition at line 87 of file types.h.

◆ rem() [3/3]

long double mim::rem	(	long double	a,
		long double	b )

inline

Definition at line 89 of file types.h.

◆ Span() [1/7]

template<class T, size_t N>

mim::Span ( const std::array< T, N > & ) -> Span< const T, N >

◆ Span() [2/7]

template<Vectorlike Vec>

mim::Span ( const Vec & ) -> Span< const typename Vec::value_type, std::dynamic_extent >

◆ Span() [3/7]

template<class I, class E>

mim::Span	(	I	,
		E	) -> Span< std::remove_reference_t< std::iter_reference_t< I > > >

◆ Span() [4/7]

template<class R>

mim::Span ( R && ) -> Span< std::remove_reference_t< std::ranges::range_reference_t< R > > >

◆ Span() [5/7]

template<class T, size_t N>

mim::Span ( std::array< T, N > & ) -> Span< T, N >

◆ Span() [6/7]

template<class T, size_t N>

mim::Span ( T(&) [N] ) -> Span< T, N >

◆ Span() [7/7]

template<Vectorlike Vec>

mim::Span ( Vec & ) -> Span< typename Vec::value_type, std::dynamic_extent >

◆ splitmix64()

uint64_t mim::splitmix64 ( uint64_t h )

inlineconstexprnoexcept

Definition at line 23 of file hash.h.

Referenced by hash().

◆ subview()

std::string_view mim::subview	(	std::string_view	s,
		size_t	i,
		size_t	n = std::string_view::npos )

constexprnoexcept

Like std::string::substr, but works on std::string_view instead.

Definition at line 67 of file util.h.

Referenced by mim::Annex::split().

◆ tuple2str()

std::string mim::tuple2str ( const Def * def )

Definition at line 57 of file tuple.cpp.

References mim::Def::arity(), mim::Lit::isa(), mim::Def::proj(), and mim::Def::world().

Referenced by mim::PrefixCleanup::apply(), Named::apply(), mim::plug::refly::normalize_check(), mim::plug::compile::normalize_cond(), and mim::plug::compile::normalize_is_loaded().

◆ tuple_of_dict()

std::tuple< const Var , const Def > mim::tuple_of_dict	(	World &	world,
		Def2Def &	v2v )

Definition at line 12 of file rule.cpp.

References get(), mim::World::mut_hole(), mim::World::mut_hole_type(), and mim::World::tuple().

Referenced by mim::Rule::replace().

◆ tuple_of_types()

const Def * mim::tuple_of_types ( const Def * t )

Definition at line 106 of file tuple.cpp.

Referenced by mim::plug::mem::op_lea().

◆ Vector()

template<class I, class A = std::allocator<typename std::iterator_traits<I>::value_type>>

mim::Vector	(	I	,
		I	,
		A	= A() ) -> Vector< typename std::iterator_traits< I >::value_type, Default_Inlined_Size< typename std::iterator_traits< I >::value_type >, A >

References Default_Inlined_Size.

Referenced by mim::Sets< Def >::Set< Def >::erase(), mim::Sets< Def >::Set< Def >::merge(), mim::Def::projs(), mim::Scalarize::rewrite_imm_Pi(), and mim::Scalarize::rewrite_mut_Lam().

Variable Documentation

◆ BitmaskWidth

auto mim::BitmaskWidth = sizeof(u64) * 8

staticconstexpr

Number of params a single u64 keep-bitmask can represent; wider doms fall back to the ⊤ sentinel.

Definition at line 10 of file scalarize.cpp.

◆ Default_Inlined_Size

template<class T>

size_t mim::Default_Inlined_Size = std::max((size_t)1, 4 * sizeof(size_t) / sizeof(T))

staticconstexpr

Use up to 4 words (i.e., 4 * sizeof(size_t)) of inlined storage, rounded up.

Definition at line 11 of file vector.h.

Referenced by Vector().

◆ Num_Nodes

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)

staticconstexpr

Definition at line 114 of file def.h.

Namespaces

Classes

Concepts

Typedefs

Enumerations

Functions

Variables

Enums that classify certain aspects of Defs.

Plugin Interface

Class Documentation

◆ mim::DotConfig

◆ mim::FNV1

Typedef Documentation

◆ Bot

◆ Def2Def

◆ DefMap

◆ Defs

◆ DefSet

◆ DefVec

◆ f32

◆ f64

◆ Flags2Phases

◆ flags_t

◆ GIDMap

◆ GIDNodeMap

◆ GIDNodeSet

◆ GIDSet

◆ Join

◆ Lam2Lam

◆ LamMap

◆ LamSet

◆ level_t

◆ Meet

◆ Mut2Mut

◆ MutMap

◆ Muts

◆ MutSet

◆ nat_t

◆ node_t

◆ NormalizeFn

◆ Normalizers

◆ Phases

◆ plugin_t

◆ s16

◆ s32

◆ s64

◆ s8

◆ sub_t

◆ tag_t

◆ Top

◆ u1

◆ u16

◆ u32

◆ u64

◆ u8

◆ Uses

◆ Var2Var

◆ VarMap

◆ Vars

◆ VarSet

◆ View

◆ w2f

◆ w2s

◆ w2u

Enumeration Type Documentation

◆ Assoc

◆ Dep

◆ Judge

◆ Mut

◆ Node

◆ Prec

Function Documentation

◆ assert_emplace()

◆ assert_lookup()

◆ binary_find()

◆ bitcast_resize()

◆ cat() [1/4]

◆ cat() [2/4]

◆ cat() [3/4]

◆ cat() [4/4]