Types

%compile.Pass

%compile.Phase

Types for compilation passes and phases.

axm %compile.Pass: *;

axm %compile.Phase: *;

%compile.Pipeline

%compile.PassList

Types for functions that accept an arbitrary number of phases and passes respectively.

rec %compile.Pipeline:      □ = %compile.Phase → %compile.Pipeline;
rec %compile.PassList:      □ = %compile.Pass  → %compile.PassList;
rec %compile.CombinedPhase: □ = %compile.Phase → %compile.CombinedPhase;

(This is a forward declaration for opt.mim.)

axm %compile.Plugin: *;

Expressions

Registered Plugins

We expect the name in the tag before the _ to be the name of the plugin (as given in Pluginplugin_name). (This is a forward declaration for opt.mim.)

axm %compile.core_plugin:     %compile.Plugin;
axm %compile.mem_plugin:      %compile.Plugin;
axm %compile.demo_plugin:     %compile.Plugin;
axm %compile.affine_plugin:   %compile.Plugin;
axm %compile.autodiff_plugin: %compile.Plugin;
axm %compile.clos_plugin:     %compile.Plugin;
axm %compile.direct_plugin:   %compile.Plugin;
axm %compile.refly_plugin:    %compile.Plugin;
axm %compile.regex_plugin:    %compile.Plugin;
axm %compile.matrix_plugin:   %compile.Plugin;

%opt.is_loaded

Indicates whether a plugin is loaded. The normalizer will statically evaluate this expression to a constant boolean. TODO: find correct point (not at parsing but before compilation)

// axm %opt.is_loaded: %opt.Plugin → Bool;

%compile.pipe

Given n phases, returns the representation of a pipeline.

axm %compile.pipe: %compile.Pipeline;

Passes and Phases

%compile.debug_phase

Given a log level, returns a phase that prints the externals (for log level >= 2).

axm %compile.debug_phase: Nat → %compile.Phase;

%compile.pass_phase

Given n passes, returns a phase that applies them in order.

TODO: combine two pass_list

axm %compile.pass_list: %compile.PassList;

pass_phase (pass_list pass1 ... passN) = passes_to_phase N (pass1, ..., passN)

axm %compile.pass_phase: %compile.PassList → %compile.Phase, normalize_pass_phase;

axm %compile.passes_to_phase: [n: Nat] → «n; %compile.Pass» → %compile.Phase;

combine_pass_list K (pass_list pass11 ... pass1N) ... (pass_list passK1 ... passKM) = pass_list pass11 ... p1N ... passK1 ... passKM

axm %compile.combine_pass_list: [n: Nat] → «n; %compile.PassList» → %compile.PassList, normalize_combine_pass_list;

single_pass_phase pass = passes_to_phase 1 pass

// TODO: as let instead of axiom

axm %compile.single_pass_phase: %compile.Pass → %compile.Phase, normalize_single_pass_phase;

%compile.combined_phase

Given n phases, returns a phase that applies them in order.

axm %compile.phase_list: %compile.CombinedPhase;

combined_phase (phase_list phase1 ... phaseN) = phases_to_phase N (phase1, ..., phaseN)

axm %compile.combined_phase: %compile.CombinedPhase → %compile.Phase, normalize_combined_phase;

axm %compile.phases_to_phase: [n: Nat] → «n; %compile.Phase» → %compile.Phase;

Passes

Basic passes that are defined in the core of Mim.

axm %compile.beta_red_pass: %compile.Pass;

axm %compile.eta_red_pass: %compile.Pass;

Eta expansion expects an instance of eta reduction as argument.

axm %compile.eta_exp_pass: %compile.Pass → %compile.Pass;

Scalarize expects an instance of eta expansion as argument.

axm %compile.scalarize_pass: %compile.Pass → %compile.Pass;

Tail recursion elimination expects an instance of eta reduction as argument.

axm %compile.tail_rec_elim_pass: %compile.Pass → %compile.Pass;
axm %compile.lam_spec_pass: %compile.Pass;
axm %compile.ret_wrap_pass: %compile.Pass;

has to be registered in the pipeline

axm %compile.nullptr_pass: %compile.Pass;

axm %compile.internal_cleanup_pass: %compile.Pass;

Phases

// TODO: allow functions by inlining them first
let optimization_pass_list =
    let eta_red = %compile.eta_red_pass;
    let eta_exp = %compile.eta_exp_pass eta_red;
    %compile.pass_list
        %compile.beta_red_pass
        eta_red
        eta_exp
        (%compile.scalarize_pass eta_exp)
        (%compile.tail_rec_elim_pass eta_red);
 
let optimization_phase = %compile.pass_phase optimization_pass_list;

Pipelines

let default_core_pipeline =
    let nullptr = %compile.nullptr_pass;
    %compile.pipe
        (%compile.single_pass_phase nullptr)
        (%compile.single_pass_phase (%compile.scalarize_pass nullptr))
        (%compile.single_pass_phase %compile.eta_red_pass)
        (%compile.single_pass_phase (%compile.tail_rec_elim_pass nullptr))
        optimization_phase
        (%compile.single_pass_phase %compile.internal_cleanup_pass)
        (%compile.single_pass_phase %compile.lam_spec_pass)
        (%compile.single_pass_phase %compile.ret_wrap_pass);
 
lam extern _fallback_compile(): %compile.Pipeline = default_core_pipeline;

Dependent Passes and Phases

let empty_pass = %compile.nullptr_pass;
let empty_phase = %compile.passes_to_phase 0 ();
axm %compile.plugin_select: [T: *] → %compile.Plugin → T → T → T;
let plugin_phase = %compile.plugin_select %compile.Phase;
let plugin_pass = %compile.plugin_select %compile.Pass;
lam plugin_cond_phase(plug: %compile.Plugin, phase: %compile.Phase): %compile.Phase = plugin_phase plug phase empty_phase;
lam plugin_cond_pass(plug: %compile.Plugin, pass: %compile.Pass): %compile.Pass = plugin_pass plug pass empty_pass;

Table of Contents