Namespaces
namespace	ast
namespace	plug

Classes
class	ADCE
	Aggressive Dead Code Elimination. More...
class	Analysis
	Traverses the current World using Rewriter infrastructure while staying in the same world. More...
struct	Annex
	Holds info about an entity defined within a Plugin (called Annex). More...
class	App
class	Arr
	A (possibly paramterized) Array. More...
class	Axm
class	BetaRed
	Inlines in post-order all Lams that occur exactly once in the program or are trivial forwarders. More...
class	Branch
	Matches (ff, tt)#cond arg where cond is not a Literal. More...
class	Check
class	Cleanup
	Removes unreachable and dead code by rebuilding the whole World into a new one and swapping them afterwards. More...
class	ClosedMutPhase
	Transitively visits all reachable, closed mutables in the World. More...
class	Def
	Base class for all Defs. More...
struct	DefKey
	Grants fe::Patricia access to Def::gid_. More...
class	Diag
	Renders a diagnostic through PlainNames and - if that turned out ambiguous - once more with Def::unique_name. More...
class	Dispatch
	Matches (target_0, target_1, ...)#index arg. More...
class	DispatchNormalize
	Normalizes Dispatches: η-expands non-Lam targets so that every target of a (t_0, ..., t_n)#index jump table is a Lam, as later phases and the backends expect. More...
struct	DotConfig
	Options for Def::dot, World::dot, and Nest::dot. More...
class	Driver
	Some "global" variables needed all over the place. More...
class	EtaConv
	Combined η-normalization: folds η-reduction and η-expansion into a single, idempotent phase. More...
class	Ext
	Common base for TExtremum. More...
class	Extract
	Extracts from a Sigma or Array-typed Extract::tuple the element at position Extract::index. More...
struct	Flags
	Compiler switches that must be saved and looked up in later phases of compilation. More...
struct	GIDHash
struct	GIDLt
class	Hole
	This node is a hole in the IR that is inferred by its context later on. More...
class	Idx
	A built-in constant of type Nat -> *. More...
class	Importer
	Imports from Driver::library: an annex therein is looked up via World::annex, so it is imported only once. More...
class	Inj
	Constructs a Join or Variant value. More...
class	Insert
	Creates a new Tuple / Pack by inserting Insert::value at position Insert::index into Insert::tuple. More...
class	Join
	A union type whose ops are sorted and deduplicated: T ∪ T is T. More...
class	Lam
	A function. More...
class	LamSpec
	Specializes a Lam at its call site by inlining all Pi-typed (i.e. higher-order) arguments. More...
class	Level
class	Lit
class	LMax
class	LSucc
class	Match
	Scrutinize Match::scrutinee() and dispatch to Match::arms. More...
class	Name
	Nominal newtype term introduction. More...
class	Nat
class	Nest
	Builds a nesting tree for all mutables/binders. More...
class	NestPhase
	Like ClosedMutPhase but computes a Nest for each NestPhase::visit. More...
class	Nom
	Nominal newtype formation. More...
class	NomErasure
	Eliminates all nominal newtypes, so that no Nom/Name/Struc ever reaches a backend. More...
class	Out
	A file name from the command line and the stream to write to;. More...
class	Pack
	A (possibly paramterized) Tuple. More...
class	Phase
	A Phase performs one self-contained task over the whole World. More...
class	PhaseMan
	Organizes several Phases into a pipeline. More...
class	Pi
	A dependent function type. More...
class	PlainNames
	Renders Defs with their plain Def::sym instead of Def::unique_name while alive. More...
struct	Plugin
	Basic info and registration function pointer to be returned from a specific plugin. More...
struct	PluginArg
	One -X <plugin>:<arg> a Plugin understands; see Arguments. More...
struct	PluginEnv
	One environment variable a Plugin reads; see Environment Variables. More...
struct	PluginSym
	One symbol a Plugin offers to other Plugins; see Driver::get_fun_ptr. More...
class	Prod
	Base class for Sigma and Tuple. More...
class	Proxy
	Used as intermediate value during optimizatinos such as Analysis. More...
class	Reform
	Type formation of a rewrite Rule. More...
class	Repl
	An RWPhase that searches for a pattern and replaces it. More...
class	RetWrap
class	Rewriter
	Recurseivly rebuilds part of a program into the provided World w.r.t. Rewriter::map. More...
class	Rule
	A rewrite rule. More...
class	RWPhase
	Rebuilds old_world() into new_world() and then swaps them. More...
class	Scalarize
	Scalarization (= argument simplification): More...
class	SCCP
	SCCP - Sparse Conditional Constant Propagation - but propagates arbitrary expressions. More...
class	Scheduler
class	Select
	Matches (ff, tt)#cond - where cond is a Bool but not a Literal. More...
class	Seq
	Base class for Arr and Pack. More...
class	Setters
	CRTP-based mixin to declare setters for Def::loc & Def::name using a covariant return type. More...
class	Shape
	The extents of a Seq's axes: a plain Nat for a single axis, an aggregate of them for several. More...
class	Sieve
	Filters the components of an aggregate and keeps track of where the survivors end up. More...
class	Sigma
	A dependent tuple type. More...
class	Single
	Singleton type formation. More...
class	SingleErasure
	Eliminates all types that have exactly one inhabitant, so that no Single/Wrap ever reaches a backend. More...
class	StaticArgOpt
	Static Argument Transformation. More...
class	Struc
	Nominal newtype term elimination. More...
class	Switch
	Matches a jump table (target_0, target_1, ...)#index where index is a non-Literal Idx n and n the arity. More...
class	TExt
	Extremum. Either Top (`Up`) or Bottom. More...
class	Tuple
	Data constructor for a Sigma. More...
class	Type
class	Use
	const Def*erences a user. More...
struct	UseEq
struct	UseHash
class	Var
	A variable introduced by a binder (mutable). More...
class	Variant
	A sum type whose cases are positional: unlike a Join, they are neither sorted nor deduplicated. More...
class	VarRewriter
	Extends Rewriter for variable substitution. More...
struct	Version
class	World
	The World represents the whole program and manages creation of MimIR nodes (Defs). More...
class	Wrap
	Singleton term introduction. More...
class	Zonker

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

Typedefs
using	NormalizeFn = const Def* ()(const Def, const Def, const Def)
using	Keys = fe::SymTab<ast::Tok::Tag, ast::Num_Keys + ast::Num_Subst>
	The reserved words the ast::Lexer looks up, keyed by the Sym it has just interned.
using	Phases = std::deque<std::unique_ptr<Phase>>
using	Uses = ankerl::unordered_dense::set<Use, UseHash, UseEq>
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 = fe::View<const Def*>
using	DefVec = fe::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	Muts = fe::Patricia<Def, DefKey>::Set
Var
GIDSet / GIDMap keyed by Var::gid of const Var*.
template<class To>
using	VarMap = GIDMap<const Var*, To>
using	Vars = fe::Patricia<const Var, DefKey>::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>
GID
template<class K, class V>
using	GIDMap = ankerl::unordered_dense::map<K, V, GIDHash<K>>
template<class K>
using	GIDSet = ankerl::unordered_dense::set<K, GIDHash<K>>
template<class K>
using	GIDNodeSet = ankerl::unordered_dense::segmented_set<K, GIDHash<K>>
template<class K, class V>
using	GIDNodeMap = ankerl::unordered_dense::segmented_map<K, V, GIDHash<K>>
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

Enumerations
enum	{ Proxy_Dead }
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
auto	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	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.
void	optimize (World &)
	Runs _compile or _default_compile, if available (in this order).
static std::optional< nat_t >	known_rank (const Def *def)
	The statically known rank of `def:` 0 if it isn't a Seq at all, nullopt if its own rank is dynamic.
static Hole *	isa_flex_rank (const Def *def)
	The rank of «s; T» with s: «r; Nat» is unknown as long as r is, and so is Def::arity.
static bool	is_flex (const Def *def)
static const Def *	drop_self (Hole hole, const Def def)
static bool	any_free_vars (const Def *def, std::predicate< Vars > auto f)
static bool	is_seq_arity (const Def *def)
std::ostream &	operator<< (std::ostream &os, const Def *def)
	Def::Dump::Expr: one Def, one line, no analysis - and the backend of std::formatter for every Def pointer.
static std::string	file_stem (World &world)
	The name of the file a World is dumped to - and hence the module its own annexes live in.
static const Def *	eta_callee (const Lam *lam)
static const Def *	eta_step (const Def *def)
static bool	has_inferred_type (const Tuple *tuple)
	Is `tuple's` type what World::tuple would infer from its ops?
static bool	is_trivial (Lam *lam)
static bool	has_nom (const Def *def)
static const Pi *	isa_flattenable (const Def *def)
	The only Pis we ever reshape: immutable (non-dependent) continuations.
static bool	is_value_telescope (const Def *def)
	A dependent Sigma of values only; other mutable Sigmas may be recursive or pack an existential, like a closure.
static bool	is_polymorphic_arg (const App *app)
	Is the argument of the Axm application `app` typed by one of the Axm's type variables?
static std::tuple< const Var , const Def >	tuple_of_dict (World &world, Def2Def &v2v)
static bool	isa_axes (const Def *type, auto leaf)
	Is `type` a `leaf` - or an aggregate of them? This is what makes a shape a shape and an index an index.
static void	default_level (const Def *level)
static level_t	eval0 (const Def *level)
static const Def *	level_of (const Def *type)
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)
Plugin Argument Lookup
Picks the -X <plugin>:<arg> strings of Driver::args / Phase::args apart. Each helper matches any of `keys` - arg_value(args(), "o", "output") - and the last occurrence wins.
template<class... Keys>
std::optional< std::string_view >	arg_value (fe::View< std::string > args, Keys... keys)
std::optional< bool >	arg_bool (fe::View< std::string > args, std::initializer_list< std::string_view > on, std::initializer_list< std::string_view > off)
	An `on` key ↦ true, an `off` key ↦ false; std::nullopt if neither occurs.
template<class... Keys>
bool	arg_flag (fe::View< std::string > args, Keys... keys)
	Whether any of `keys` occurs.
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)
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)

Enums that classify certain aspects of Defs.
enum class	Node : node_t { Lit , Axm , Var , Proxy , Hole , Type , Level , LMax , LSucc , Pi , Lam , App , Sigma , Tuple , Extract , Insert , Arr , Pack , Join , Inj , Match , Variant , Top , Bot , Reform , Rule , Single , Wrap , Nom , Name , Struc , Nat , Idx }
enum class	MutNode : node_t { Hole = node_t(Node::Hole) , Pi = node_t(Node::Pi) , Lam = node_t(Node::Lam) , Sigma = node_t(Node::Sigma) , Arr = node_t(Node::Arr) , Pack = node_t(Node::Pack) , Variant = node_t(Node::Variant) , Rule = node_t(Node::Rule) }
	The Nodes that may be mutable, with the same values as their Node. More...
enum class	Judge : u32 { Form = 1 << 0 , Intro = 1 << 1 , Elim = 1 << 2 , Meta = 1 << 3 , Hole = 1 << 4 }
	Judgement. 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) +size_t(1)
constexpr bool	is_mut_node (Node node) noexcept

Plugin Interface
See also Plugin
using	Normalizers = ankerl::unordered_dense::map<flags_t, NormalizeFn>
using	Flags2Phases = ankerl::unordered_dense::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, 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.

◆ mim::PluginArg

struct mim::PluginArg

One -X <plugin>:<arg> a Plugin understands; see Arguments.

A Plugin declares these next to the code that picks them apart, so that mim -p <plugin> -h can list them.

Definition at line 34 of file plugin.h.

Class Members
const char *	descr	What it does; one sentence of Markdown, but no links: the terminal help prints it as is.
const char *	syntax	How to spell the argument, e.g. "o=<file>, output=<file>".

◆ mim::PluginEnv

struct mim::PluginEnv

One environment variable a Plugin reads; see Environment Variables.

A Plugin declares these next to the code that reads them, so that mim -p <plugin> -h can list them.

Definition at line 41 of file plugin.h.

Class Members
const char *	descr	What it does; one sentence of Markdown, but no links: the terminal help prints it as is.
const char *	name	Name of the variable, e.g. "CUDA_HOME".

◆ mim::PluginSym

struct mim::PluginSym

One symbol a Plugin offers to other Plugins; see Driver::get_fun_ptr.

A statically linked Plugin has no shared object to look it up in.

Definition at line 48 of file plugin.h.

Class Members
const char *	name	Name of the symbol, e.g. "mim_ll_convert".
void *	ptr	Address of the symbol.

Typedef Documentation

◆ Bot

using mim::Bot = TExt<false>

Definition at line 39 of file union.h.

◆ Def2Def

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

Definition at line 95 of file def.h.

◆ DefMap

template<class To>

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

Definition at line 93 of file def.h.

◆ Defs

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

Definition at line 96 of file def.h.

◆ DefSet

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

Definition at line 94 of file def.h.

◆ DefVec

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

Definition at line 98 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 = ankerl::unordered_dense::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 30 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 = ankerl::unordered_dense::map<K, V, GIDHash<K>>

Definition at line 22 of file gid.h.

◆ GIDNodeMap

template<class K, class V>

using mim::GIDNodeMap = ankerl::unordered_dense::segmented_map<K, V, GIDHash<K>>

Definition at line 25 of file gid.h.

◆ GIDNodeSet

template<class K>

using mim::GIDNodeSet = ankerl::unordered_dense::segmented_set<K, GIDHash<K>>

Definition at line 24 of file gid.h.

◆ GIDSet

template<class K>

using mim::GIDSet = ankerl::unordered_dense::set<K, GIDHash<K>>

Definition at line 23 of file gid.h.

◆ Keys

using mim::Keys = fe::SymTab<ast::Tok::Tag, ast::Num_Keys + ast::Num_Subst>

The reserved words the ast::Lexer looks up, keyed by the Sym it has just interned.

Definition at line 28 of file driver.h.

◆ Lam2Lam

using mim::Lam2Lam = LamMap<Lam*>

Definition at line 212 of file lam.h.

◆ LamMap

template<class To>

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

Definition at line 210 of file lam.h.

◆ LamSet

using mim::LamSet = GIDSet<Lam*>

Definition at line 211 of file lam.h.

◆ level_t

using mim::level_t = u64

Definition at line 36 of file types.h.

◆ MutMap

template<class To>

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

Definition at line 105 of file def.h.

◆ Muts

using mim::Muts = fe::Patricia<Def, DefKey>::Set

Definition at line 107 of file def.h.

◆ MutSet

using mim::MutSet = GIDSet<Def*>

Definition at line 106 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 118 of file def.h.

◆ Normalizers

using mim::Normalizers = ankerl::unordered_dense::map<flags_t, NormalizeFn>

Definition at line 27 of file plugin.h.

◆ Phases

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

Definition at line 18 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 40 of file union.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 = ankerl::unordered_dense::set<Use, UseHash, UseEq>

Definition at line 41 of file schedule.h.

◆ VarMap

template<class To>

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

Definition at line 114 of file def.h.

◆ Vars

using mim::Vars = fe::Patricia<const Var, DefKey>::Set

Definition at line 115 of file def.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

◆ anonymous enum

anonymous enum

Enumerator
Proxy_Dead

Definition at line 5 of file adce.cpp.

◆ Assoc

enum class mim::ast::Assoc

strong

Associativity of an infix expression.

Definition at line 48 of file tok.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 163 of file def.h.

◆ MutNode

enum class mim::MutNode : node_t

strong

The Nodes that may be mutable, with the same values as their Node.

A switch over Def::mut_node without a default must handle each of them, so a new one breaks the build there.

Enumerator
Hole
Pi
Lam
Sigma
Arr
Pack
Variant
Rule

Definition at line 135 of file def.h.

◆ Node

enum class mim::Node : node_t

strong

Enumerator
Lit
Axm
Var
Proxy
Hole
Type
Level
LMax
LSucc
Pi
Lam
App
Sigma
Tuple
Extract
Insert
Arr
Pack
Join
Inj
Match
Variant
Top
Bot
Reform
Rule
Single
Wrap
Nom
Name
Struc
Nat
Idx

Definition at line 123 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 51 of file tok.h.

Function Documentation

◆ any_free_vars()

bool mim::any_free_vars	(	const Def *	def,
		std::predicate< Vars > auto	f )

static

Definition at line 267 of file def.cpp.

References any_free_vars(), mim::Def::isa_mut(), mim::Def::local_muts(), and mim::Def::local_vars().

Referenced by any_free_vars(), mim::Def::has_free_var(), mim::Def::has_free_vars(), and mim::Def::has_free_vars_in().

◆ arg_bool()

std::optional< bool > mim::arg_bool	(	fe::View< std::string >	args,
		std::initializer_list< std::string_view >	on,
		std::initializer_list< std::string_view >	off )

inline

An on key ↦ true, an off key ↦ false; std::nullopt if neither occurs.

Definition at line 74 of file plugin.h.

References arg_bool().

Referenced by arg_bool(), mim::plug::compile::normalize_aggr(), and mim::plug::nvptx::Emit::start().

◆ arg_flag()

template<class... Keys>

bool mim::arg_flag	(	fe::View< std::string >	args,
		Keys...	keys )

Whether any of keys occurs.

Definition at line 89 of file plugin.h.

References arg_flag().

Referenced by arg_flag(), and mim::plug::nvptx::Emit::start().

◆ arg_value()

template<class... Keys>

std::optional< std::string_view > mim::arg_value	(	fe::View< std::string >	args,
		Keys...	keys )

Value of <key>=<value>; std::nullopt if none of keys carries one.

Definition at line 64 of file plugin.h.

References arg_value().

Referenced by mim::Driver::arg_nat(), mim::plug::ll::arg_rt(), arg_value(), mim::plug::ll::Emit::start(), and mim::plug::nvptx::Emit::start().

◆ default_level()

void mim::default_level ( const Def * level )

static

Definition at line 288 of file world.cpp.

References default_level(), and mim::Hole::isa_unset().

Referenced by default_level(), and mim::World::solve_levels().

◆ drop_self()

const Def * mim::drop_self	(	Hole *	hole,
		const Def *	def )

static

Definition at line 353 of file check.cpp.

References drop_self(), mim::World::lmax(), and mim::Def::world().

Referenced by drop_self().

◆ eta_callee()

const Def * mim::eta_callee ( const Lam * lam )

static

Definition at line 53 of file lam.cpp.

References mim::Lam::body(), mim::Lam::dom(), eta_callee(), mim::Def::has_var(), mim::World::inhabitant(), mim::Def::is_set(), and mim::Def::world().

Referenced by eta_callee(), and eta_step().

◆ eta_step()

const Def * mim::eta_step ( const Def * def )

static

Definition at line 64 of file lam.cpp.

References eta_callee(), and eta_step().

Referenced by mim::Lam::eta_reduce(), and eta_step().

◆ eval0()

level_t mim::eval0 ( const Def * level )

static

Definition at line 299 of file world.cpp.

References eval0(), mim::Lit::isa(), mim::Hole::isa_unset(), and mim::Def::zonk().

Referenced by eval0(), and mim::World::solve_levels().

◆ file_stem()

std::string mim::file_stem ( World & world )

static

The name of the file a World is dumped to - and hence the module its own annexes live in.

Definition at line 1471 of file dump.cpp.

References file_stem(), mim::World::name(), and mim::World::sym().

Referenced by mim::World::dump(), file_stem(), and mim::World::write().

◆ has_inferred_type()

bool mim::has_inferred_type ( const Tuple * tuple )

static

Is tuple's type what World::tuple would infer from its ops?

Definition at line 232 of file phase.cpp.

References has_inferred_type(), mim::Tuple::infer(), mim::Def::ops(), mim::Def::type(), and mim::Def::world().

Referenced by has_inferred_type(), and mim::RWPhase::rewrite_imm_Tuple().

◆ has_nom()

bool mim::has_nom ( const Def * def )

static

Definition at line 7 of file nom_erasure.cpp.

References has_nom().

Referenced by has_nom(), and mim::NomErasure::lookup().

◆ 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 177 of file axm.h.

References is_associative(), and is_commutative().

Referenced by is_associative(), is_associative(), is_associative(), is_associative(), is_associative(), is_associative(), and is_associative().

◆ is_associative() [2/7]

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

constexpr

Definition at line 78 of file core.h.

References mim::plug::core::and_, mim::plug::core::f, mim::plug::core::fst, is_associative(), 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 95 of file core.h.

References is_associative(), and is_commutative().

◆ is_associative() [4/7]

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

constexpr

Definition at line 93 of file core.h.

References is_associative(), and is_commutative().

◆ is_associative() [5/7]

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

constexpr

Definition at line 94 of file core.h.

References is_associative(), and is_commutative().

◆ is_associative() [6/7]

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

constexpr

Definition at line 96 of file core.h.

References is_associative(), and is_commutative().

◆ is_associative() [7/7]

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

constexpr

Definition at line 97 of file math.h.

References is_associative(), and is_commutative().

◆ is_commutative() [1/9]

template<class Id>

bool mim::is_commutative ( Id )

constexpr

Definition at line 171 of file axm.h.

References is_commutative().

Referenced by is_associative(), is_associative(), is_associative(), is_associative(), is_associative(), is_associative(), is_commutative(), is_commutative(), is_commutative(), is_commutative(), is_commutative(), is_commutative(), is_commutative(), is_commutative(), is_commutative(), 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 73 of file core.h.

References is_commutative().

◆ is_commutative() [3/9]

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

constexpr

Definition at line 70 of file core.h.

References is_commutative(), and mim::plug::core::ne.

◆ is_commutative() [4/9]

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

constexpr

Definition at line 67 of file core.h.

References is_commutative().

◆ is_commutative() [5/9]

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

constexpr

Definition at line 68 of file core.h.

References is_commutative(), and mim::plug::core::ne.

◆ is_commutative() [6/9]

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

constexpr

Definition at line 69 of file core.h.

References mim::plug::core::add, is_commutative(), and mim::plug::core::mul.

◆ is_commutative() [7/9]

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

constexpr

Definition at line 95 of file math.h.

References mim::plug::math::add, is_commutative(), and mim::plug::math::mul.

◆ is_commutative() [8/9]

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

constexpr

Definition at line 96 of file math.h.

References is_commutative().

◆ is_commutative() [9/9]

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

constexpr

Definition at line 94 of file math.h.

References is_commutative().

◆ is_flex()

bool mim::is_flex ( const Def * def )

static

Definition at line 217 of file check.cpp.

References Hole, is_flex(), mim::Prod::isa_node(), mim::Seq::isa_node(), and mim::Def::node().

Referenced by is_flex().

◆ is_mut_node()

bool mim::is_mut_node ( Node node )

constexprnoexcept

Definition at line 141 of file def.h.

References CODE, is_mut_node(), and MIM_MUT_NODE.

Referenced by is_mut_node(), mim::Def::mut_node(), and mim::Def::reduction_offset().

◆ is_polymorphic_arg()

bool mim::is_polymorphic_arg ( const App * app )

static

Is the argument of the Axm application app typed by one of the Axm's type variables?

Definition at line 23 of file scalarize.cpp.

References mim::Pi::codom(), mim::Pi::dom(), is_polymorphic_arg(), mim::Def::type(), and mim::App::uncurry_callee().

Referenced by is_polymorphic_arg().

◆ is_seq_arity()

bool mim::is_seq_arity ( const Def * def )

static

Definition at line 636 of file def.cpp.

References is_seq_arity(), and mim::Def::type().

Referenced by is_seq_arity(), and mim::Def::num_tprojs().

◆ is_trivial()

bool mim::is_trivial ( Lam * lam )

static

Definition at line 5 of file beta_red.cpp.

References mim::Lam::body(), mim::Def::has_free_var(), mim::Def::has_var(), is_trivial(), and mim::Lam::ret_var().

Referenced by is_trivial().

◆ is_unit()

bool mim::is_unit ( const Def * def )

Definition at line 113 of file tuple.cpp.

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

Referenced by is_unit().

◆ is_value_telescope()

bool mim::is_value_telescope ( const Def * def )

static

A dependent Sigma of values only; other mutable Sigmas may be recursive or pack an existential, like a closure.

Definition at line 16 of file scalarize.cpp.

References is_value_telescope(), and mim::Def::isa_binder().

Referenced by is_value_telescope().

◆ isa_axes()

bool mim::isa_axes	(	const Def *	type,
		auto	leaf )

static

Is type a leaf - or an aggregate of them? This is what makes a shape a shape and an index an index.

Definition at line 39 of file tuple.cpp.

References isa_axes().

Referenced by isa_axes(), mim::Shape::isa_extents(), and mim::Shape::isa_indices().

◆ isa_flattenable()

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

static

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

Definition at line 10 of file scalarize.cpp.

References mim::Pi::isa_cn(), and isa_flattenable().

Referenced by isa_flattenable().

◆ isa_flex_rank()

Hole * mim::isa_flex_rank ( const Def * def )

static

The rank of «s; T» with s: «r; Nat» is unknown as long as r is, and so is Def::arity.

Returns: the unset Hole standing for r, or nullptr.

Definition at line 207 of file check.cpp.

References isa_flex_rank(), mim::Def::isa_imm(), and mim::Hole::isa_unset().

Referenced by isa_flex_rank().

◆ known_rank()

std::optional< nat_t > mim::known_rank ( const Def * def )

static

The statically known rank of def: 0 if it isn't a Seq at all, nullopt if its own rank is dynamic.

Definition at line 200 of file check.cpp.

References known_rank(), and mim::Def::zonk_mut().

Referenced by known_rank().

◆ level_of()

const Def * mim::level_of ( const Def * type )

static

Definition at line 336 of file world.cpp.

References mim::Check::alpha(), mim::Hole::isa_unset(), and level_of().

Referenced by mim::World::level(), and level_of().

◆ mim_get_plugin()

mim::Plugin mim::mim_get_plugin ( )

To be implemented and exported by a plugin.

Returns: a filled Plugin.

References MIM_EXPORT, and mim_get_plugin().

Referenced by mim::Driver::load(), and mim_get_plugin().

◆ 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, and MIM_8_16_32_64.

◆ 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<<()

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

Def::Dump::Expr: one Def, one line, no analysis - and the backend of std::formatter for every Def pointer.

Definition at line 1440 of file dump.cpp.

◆ 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::Lam::body(), mim::Phase::create(), mim::World::driver(), mim::World::externals(), mim::Def::internalize(), mim::World::log(), mim::Driver::move_to_library(), mim::World::Externals::mutate(), mim::Lam::num_doms(), optimize(), mim::Driver::phases(), mim::World::sym(), and mim::Def::type().

Referenced by optimize().

◆ post_order()

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.

descend picks the mutables to walk through, collect those that land in res. done is passed in so that several roots share one traversal.

Definition at line 1155 of file def.h.

References mim::Def::deps(), and post_order().

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

◆ prec_assoc()

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

constexpr

Associativity of precedence level p.

Definition at line 58 of file tok.h.

◆ rem() [1/3]

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

inline

Definition at line 88 of file types.h.

References rem().

◆ rem() [2/3]

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

inline

Definition at line 87 of file types.h.

References rem().

Referenced by rem(), rem(), and rem().

◆ rem() [3/3]

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

inline

Definition at line 89 of file types.h.

References rem().

◆ tuple2str()

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

Definition at line 115 of file tuple.cpp.

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

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

◆ tuple_of_dict()

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

static

Definition at line 12 of file rule.cpp.

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

Referenced by mim::Rule::replace(), and tuple_of_dict().

◆ tuple_of_types()

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

Definition at line 167 of file tuple.cpp.

References tuple_of_types().

Referenced by mim::plug::mem::op_lea(), and tuple_of_types().

◆ type_of()

auto mim::type_of ( const Def * def )

inline

Def::unfold_type of def for a diagnostic - Level is the one Def that has no type at all.

Streams lazily so that it still renders under the PlainNames guard Error::msg formats within.

Definition at line 1144 of file def.h.

References type_of(), and mim::Def::unfold_type().

Referenced by mim::World::app(), mim::ast::assign(), mim::Def::check(), mim::Def::check(), mim::ast::MatchExpr::emit_(), mim::ast::PrefixExpr::emit_(), mim::World::inj(), mim::World::inj(), mim::World::lmax(), mim::World::lsucc(), mim::World::match(), mim::World::name(), mim::World::seq(), mim::World::struc(), mim::World::tuple(), mim::World::type(), type_of(), and mim::World::unwrap().

Variable Documentation

◆ 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) +size_t(1)

staticconstexpr

Definition at line 130 of file def.h.

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

Namespaces

Classes

Concepts

Typedefs

Enumerations

Functions

Enums that classify certain aspects of Defs.

Plugin Interface

Class Documentation

◆ mim::DotConfig

◆ mim::PluginArg

◆ mim::PluginEnv

◆ mim::PluginSym

Typedef Documentation

◆ Bot

◆ Def2Def

◆ DefMap

◆ Defs

◆ DefSet

◆ DefVec

◆ f32

◆ f64

◆ Flags2Phases

◆ flags_t

◆ GIDMap

◆ GIDNodeMap

◆ GIDNodeSet

◆ GIDSet

◆ Keys

◆ Lam2Lam

◆ LamMap

◆ LamSet

◆ level_t

◆ 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

◆ VarMap

◆ Vars

◆ w2f

◆ w2s

◆ w2u

Enumeration Type Documentation

◆ anonymous enum

◆ Assoc

◆ Judge

◆ MutNode

◆ Node

◆ Prec

Function Documentation

◆ any_free_vars()

◆ arg_bool()

◆ arg_flag()

◆ arg_value()

◆ default_level()

◆ drop_self()

◆ eta_callee()

◆ eta_step()

◆ eval0()

◆ file_stem()

◆ has_inferred_type()

◆ has_nom()