See also: -X compile:<arg>; mim::plug::compile

This plugin provides the building blocks for MimIR's optimization pipeline: its axioms denote mim::Phases and the combinators that assemble them into a pipeline. Invoke the pipeline by defining a function _compile: [] → compile.Phase (or rely on a plugin-provided _default_compile such as the one in the opt plugin).

Types

Phase

The type of compilation phases.

axm Phase: *;

Operations

aggr

Makes a fixed-point flag switchable from the command line. compile.aggr fallback yields tt if -X compile:aggr was passed, ff if -X compile:no-aggr was passed, and otherwise the given fallback. Use it as the Bool of a compile.phases to make that pipeline's fixed-point iteration switchable via the CLI.

axm aggr: Bool → Bool, normalize_aggr;

cond

Yields phase if the named plugin is loaded, otherwise compile.null. Used to gate whole sub-pipelines on a plugin without importing it.

axm cond: {n: Nat} → «n; I8» → Phase → Phase, normalize_cond;

is_loaded

Checks whether the given plugin is loaded.

axm is_loaded: {n: Nat} → «n; I8» → Bool, normalize_is_loaded;

named

Resolves to the compile.Phase annex with the given fully-qualified name (e.g. "clos.clos_conv"). Resolution is deferred until the phase pipeline is built so that the referenced plugin's .mim file does not have to be imported by users of this axm. If the named annex is missing at pipeline build time (its plugin is not loaded), it is silently elided, i.e. the enclosing compile.phases simply skips it.

axm named: {n: Nat} → «n; I8» → Phase;

phases

Bundles n phases into one pipeline (a mim::PhaseMan). The Bool selects fixed-point iteration: tt reruns the pipeline until no phase requests another round, ff runs it once.

axm phases: {n: Nat} → Bool → «n; Phase» → Phase;

Phases

The phases this plugin itself registers; every other one is contributed by the plugin that implements it.

adce

Aggressive dead code elimination; removes Lam params nobody needs (mim::ADCE).

axm adce: Phase;

beta_red

β-reduction; inlines Lams that occur exactly once in the program (mim::BetaRed).

axm beta_red: Phase;

cleanup

Removes dead and unreachable code by rebuilding the World (mim::Cleanup).

axm cleanup: Phase;

dispatch_normalize

η-expands non-Lam dispatch targets so every target of a jump table is a Lam (mim::DispatchNormalize).

axm dispatch_normalize: Phase;

eta_conv

Combined, idempotent η-reduction/η-expansion (mim::EtaConv).

axm eta_conv: Phase;

lam_spec

Specializes a Lam at its call site by inlining higher-order arguments (mim::LamSpec).

axm lam_spec: Phase;

nom_erasure

Eliminates all nominal newtypes so that none reaches a backend (mim::NomErasure). nom N = T degrades to T, and both v inj N and #v to v.

axm nom_erasure: Phase;

null

Does nothing; useful as an elided placeholder.

axm null: Phase;

ret_wrap

Prepares return continuations for the backend (mim::RetWrap).

axm ret_wrap: Phase;

scalarize

Flattens function signatures (mim::Scalarize).

axm scalarize: Phase;

sccp

Sparse Conditional Constant Propagation; propagates arbitrary expressions, not just constants (mim::SCCP).

axm sccp: Phase;

single_erasure

Eliminates all types with exactly one inhabitant so that none reaches a backend (mim::SingleErasure). Within an aggregate the component is dropped; elsewhere «e» degrades to [] and ‹e› to (). Besides «e» this also catches [] and Idx 1.

axm single_erasure: Phase;

static_arg_opt

Drops params that recursive calls merely forward, turning them into loops (mim::StaticArgOpt).

axm static_arg_opt: Phase;