MimIR
MimIR is my Intermediate Representation
Loading...
Searching...
No Matches
mim Namespace Reference

Namespaces

namespace  ast
namespace  plug
namespace  sexpr

Classes

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. More...
class  Bound
 Common base for TBound. More...
class  Branch
 Matches (ff, tt)#cond arg where cond is not a Literal. 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  Checker
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 a dispatch through a jump table of the form: (target_0, target_1, ...)#index arg where index is not a Literal. More...
struct  DotConfig
 Options for Def::dot and World::dot. More...
class  Driver
 Some "global" variables needed all over the place. More...
class  Emitter
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  Global
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  Inj
 Constructs a Join value. More...
class  InplaceRWPhase
 Rewrites the current World in place - unlike an RWPhase, which rebuilds a new World. More...
class  Insert
 Creates a new Tuple / Pack by inserting Insert::value at position Insert::index into Insert::tuple. 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  Lit
class  Match
 Scrutinize Match::scrutinee() and dispatch to Match::arms. More...
class  Merge
 Constructs a Meet value. 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  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...
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  RWBase
 Common base of the two rewriting Phases: RWPhase rebuilds the World, InplaceRWPhase stays in it. More...
class  RWPhase
 Rebuilds old_world() into new_world() and then swaps them. More...
class  Scalarize
 Perform Scalarization (= Argument simplification). More...
class  Scheduler
class  Select
 Matches (ff, tt)#cond - where cond is 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  Sigma
 A dependent tuple type. More...
class  Split
 Picks the aspect of a Meet [value](Pick::value) by its [type](Def::type). More...
class  StaticArgOpt
 Static Argument Transformation. More...
class  TBound
 Specific Bound depending on Up. More...
class  TExt
 Extremum. Either Top (Up) or Bottom. More...
class  Tuple
 Data constructor for a Sigma. More...
class  Type
class  UInc
class  UMax
class  Uniq
 A singleton wraps a type into a higher order type. More...
class  Univ
class  Unload
class  Use
 const Def*erences a user. More...
struct  UseEq
struct  UseHash
class  Var
 A variable introduced by a binder (mutable). 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  Zonker

Concepts

concept  annex_with_subs
concept  annex_without_subs
concept  Enum

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 = absl::flat_hash_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 Mut2Mut = MutMap<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 Var2Var = VarMap<const Var*>
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>
using Meet = TBound<false>
 AKA intersection.
using Join = TBound<true>
 AKA union.
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>>
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 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 - Univ is the one Def that has no type at all.
void optimize (World &)
 Runs _compile or _default_compile, if available (in this order).
static bool isa_dim (const Def *def)
 Is def a Seq that spans exactly one dimension, i.e. one that a rank can be peeled off?
static Hole * isa_flex_rank (const Def *def)
 The rank of «s; T» with s: «r; Nat» is unknown as long as r is: World::seq cannot un-nest it yet.
static bool is_flex (const Def *def)
static const Def * drop_self (Hole *hole, const Def *def)
static constexpr unsigned node2dep (Node node, bool mut)
template<class F>
static bool any_free_vars (const Def *def, F f)
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)
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:
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)
 Value of <key>=<value>; std::nullopt if none of keys carries one.
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)
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)
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)

Variables

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 229 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::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, Markdown.
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, Markdown.
const char * name Name of the variable, e.g. "CUDA_HOME".

Typedef Documentation

◆ Bot

using mim::Bot = TExt<false>

Definition at line 164 of file lattice.h.

◆ Def2Def

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

Definition at line 90 of file def.h.

◆ DefMap

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

Definition at line 88 of file def.h.

◆ Defs

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

Definition at line 91 of file def.h.

◆ DefSet

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

Definition at line 89 of file def.h.

◆ DefVec

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

Definition at line 93 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 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 = absl::flat_hash_map<K, V, GIDHash<K>>

Definition at line 24 of file gid.h.

◆ GIDNodeMap

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

Definition at line 26 of file gid.h.

◆ GIDNodeSet

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

Definition at line 27 of file gid.h.

◆ GIDSet

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

Definition at line 25 of file gid.h.

◆ Join

using mim::Join = TBound<true>

AKA union.

Definition at line 167 of file lattice.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 27 of file driver.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 166 of file lattice.h.

◆ Mut2Mut

using mim::Mut2Mut = MutMap<Def*>

Definition at line 102 of file def.h.

◆ MutMap

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

Definition at line 100 of file def.h.

◆ Muts

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

Definition at line 103 of file def.h.

◆ MutSet

using mim::MutSet = GIDSet<Def*>

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

◆ Normalizers

using mim::Normalizers = absl::flat_hash_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 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 165 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 111 of file def.h.

◆ VarMap

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

Definition at line 110 of file def.h.

◆ Vars

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

Definition at line 112 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

◆ Assoc

enum class mim::ast::Assoc
strong

Associativity of an infix expression.

Definition at line 47 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 133 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 142 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 154 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 120 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 50 of file tok.h.

Function Documentation

◆ any_free_vars()

template<class F>
bool mim::any_free_vars ( const Def * def,
F f )
static

Definition at line 263 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::Prod::Def(), mim::Def::has_free_var(), and mim::Def::has_free_vars().

◆ 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 73 of file plugin.h.

References arg_bool().

Referenced by arg_bool(), mim::plug::compile::normalize_aggr(), and mim::plug::ll_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 88 of file plugin.h.

References arg_flag().

Referenced by arg_flag(), and mim::plug::ll_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 arg_value(), mim::plug::ll::Emit::start(), mim::plug::ll_nvptx::Emit::start(), and mim::plug::tensor::phase::Reassoc::start().

◆ cat() [1/4]

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

Definition at line 289 of file tuple.h.

References cat().

◆ cat() [2/4]

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

Definition at line 290 of file tuple.h.

References cat().

◆ cat() [3/4]

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

Definition at line 73 of file tuple.cpp.

References cat().

Referenced by cat(), cat(), 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 81 of file tuple.cpp.

References cat(), and mim::Def::proj().

◆ cat_sigma() [1/4]

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

Definition at line 302 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 303 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 93 of file tuple.cpp.

References cat(), and cat_sigma().

Referenced by cat_sigma(), cat_sigma(), cat_sigma(), and cat_sigma().

◆ cat_sigma() [4/4]

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

Definition at line 96 of file tuple.cpp.

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

◆ cat_tuple() [1/4]

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

Definition at line 300 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 301 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 92 of file tuple.cpp.

References cat(), and cat_tuple().

Referenced by cat_tuple(), cat_tuple(), 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 95 of file tuple.cpp.

References cat(), cat_tuple(), 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 67 of file lam.cpp.

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

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

◆ drop_self()

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

Definition at line 343 of file check.cpp.

References drop_self(), mim::World::umax(), mim::UMax::Univ, and mim::Def::world().

Referenced by drop_self().

◆ flatten_umax()

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

Definition at line 162 of file world.cpp.

References flatten_umax().

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

◆ 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 170 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 110 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 127 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 125 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 126 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 128 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 132 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 164 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 105 of file core.h.

References is_commutative().

◆ is_commutative() [3/9]

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

Definition at line 102 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 99 of file core.h.

References is_commutative().

◆ is_commutative() [5/9]

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

Definition at line 100 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 101 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 130 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 131 of file math.h.

References is_commutative().

◆ is_commutative() [9/9]

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

Definition at line 129 of file math.h.

References is_commutative().

◆ is_flex()

bool mim::is_flex ( const Def * def)
static

Definition at line 205 of file check.cpp.

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

Referenced by is_flex().

◆ is_unit()

bool mim::is_unit ( const Def * def)

Definition at line 46 of file tuple.cpp.

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

Referenced by is_unit().

◆ isa_apped_mut_lam()

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

Definition at line 354 of file lam.h.

References isa_apped_mut_lam().

Referenced by isa_apped_mut_lam().

◆ isa_callee()

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

Definition at line 342 of file lam.h.

References isa_callee().

Referenced by isa_callee().

◆ isa_dim()

bool mim::isa_dim ( const Def * def)
static

Is def a Seq that spans exactly one dimension, i.e. one that a rank can be peeled off?

Definition at line 188 of file check.cpp.

References mim::Def::arity(), isa_dim(), mim::Def::unfold_type(), and mim::Def::zonk_mut().

Referenced by isa_dim().

◆ 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(), 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: World::seq cannot un-nest it yet.

Returns
the unset Hole standing for r, or nullptr.

Definition at line 195 of file check.cpp.

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

Referenced by isa_flex_rank().

◆ isa_optimizable()

Lam * mim::isa_optimizable ( Lam * lam)
inline

These are Lams that are.

Definition at line 349 of file lam.h.

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

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

◆ 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(), mim_get_plugin(), and mim_get_plugin().

◆ node2dep()

constexpr unsigned mim::node2dep ( Node node,
bool mut )
staticconstexpr

Definition at line 29 of file def.cpp.

References Hole, Mut, node2dep(), None, Proxy, and Var.

Referenced by mim::Def::Def(), mim::Def::Def(), mim::Def::Def(), and node2dep().

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

This will stream def as an operand.

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

Definition at line 548 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::Phase::apply(), mim::Cleanup::Cleanup(), mim::World::driver(), mim::World::externals(), mim::Def::internalize(), mim::World::log(), mim::World::Externals::mutate(), optimize(), mim::Driver::phase(), mim::World::sym(), mim::Def::type(), and mim::App::uncurry_callee().

Referenced by optimize().

◆ post_order()

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

Definition at line 101 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 57 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 48 of file tuple.cpp.

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

Referenced by mim::Unload::apply(), 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 )

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 98 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 - Univ 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 1136 of file def.h.

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

Referenced by mim::World::app(), mim::Def::check(), mim::Def::check(), mim::World::extract(), mim::World::insert(), mim::World::match(), mim::World::tuple(), mim::World::type(), type_of(), mim::World::uinc(), and mim::World::umax().

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.

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

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