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.

beta_red

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

axm beta_red: Phase;

branch_normalize

η-expands non-Lam branch targets so both sides of a branch are Lams (mim::BranchNormalize).

axm branch_normalize: Phase;

cleanup

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

axm cleanup: 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;

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;

static_arg_opt

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

axm static_arg_opt: Phase;

unload

Unloads a plugin and nukes its annexes on the next World swap.

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