The compile Plugin

Table of Contents

• Types
  • %compile.Pass / %compile.Phase
• Utility
  • %compile.is_loaded
• Constructors
  • %compile.phases / %compile.passes
  • Phases
  • Repls
  • Passes
  • Pipelines

See also

mim::plug::compile

This plugin handles the optimization pipeline of the compilation of MimIR programs. This plugin's axioms can register mim::Passes and mim::Phases. Invoke the optimization pipeline by defining a function _compile: [] → %compile.Phase.

Types

%compile.Pass / %compile.Phase

Types for compilation passes and phases.

axm %compile.Phase: *;
axm %compile.Pass:  *;
axm %compile.Repl:  *;

Utility

%compile.is_loaded

Checks whether the given plugin is loaded.

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

Constructors

%compile.phases / %compile.passes

Sets up n phases / passes anad bundles them

axm %compile.phases: {n: Nat} → Bool → «n; %compile.Phase» → %compile.Phase;
axm %compile.passes: {n: Nat} →        «n; %compile.Pass » → %compile.Pass;
axm %compile.repls:  {n: Nat} →        «n; %compile.Repl » → %compile.Repl;

Phases

axm %compile.beta_red_phase:                            %compile.Phase;
axm %compile.branch_normalize_phase:                    %compile.Phase;
axm %compile.cleanup_phase:                             %compile.Phase;
axm %compile.eta_exp_phase:                             %compile.Phase;
axm %compile.eta_red_phase:                             %compile.Phase;
axm %compile.null_phase:                                %compile.Phase;
axm %compile.ret_wrap_phase:                            %compile.Phase;
axm %compile.pass2phase:                %compile.Pass → %compile.Phase;
axm %compile.repl2phase:                %compile.Repl → %compile.Phase;
axm %compile.prefix_cleanup_phase: {n: Nat} → «n; I8» → %compile.Phase;
 
let %compile.internal_cleanup_phase = %compile.prefix_cleanup_phase "internal_";

Repls

axm %compile.null_repl: %compile.Repl;

Passes

axm %compile.beta_red_pass:                             %compile.Pass;
axm %compile.eta_exp_pass:                              %compile.Pass;
axm %compile.eta_red_pass:                       Bool → %compile.Pass;
axm %compile.lam_spec_pass:                             %compile.Pass;
axm %compile.null_pass:                                 %compile.Pass;
axm %compile.scalarize_pass:                            %compile.Pass;
axm %compile.tail_rec_elim_pass:                        %compile.Pass;

Pipelines

let optimization_passes = %compile.passes (
    %compile.beta_red_pass,
    %compile.eta_red_pass ff,
    %compile.eta_exp_pass,
    %compile.scalarize_pass,
    %compile.tail_rec_elim_pass,
);
 
let optimization_phase = %compile.pass2phase optimization_passes;