The CPS Plugin

Table of Contents

• Dependencies
• Operations
  • %cps.cps2ds
• Phases
  • %cps.conv

See also

mim::plug::cps

This plugin has three jobs:

1. Convert direct-style calls (and the functions they call) to CPS.
2. Wrap direct-style functions as CPS functions using an axiom.
3. Call CPS functions in direct style using an axiom.

Dependencies

import compile;

Operations

%cps.cps2ds

This axiom lets the user call a CPS function in direct style. The function is not converted; only the call site is changed. %cps.cps2ds_dep is the dependently-typed general form; %cps.cps2ds is the non-dependent shorthand.

axm %cps.cps2ds_dep: [T: *, U: T → *] → [   Fn [t: T] → U t] → [[t: T] → U t], 2;
lam %cps.cps2ds      (T: *, U:     *)   (f: Fn     T  → U  ):  [    T  → U  ] = %cps.cps2ds_dep (T, λ [T]: * = U) f;

Phases

%cps.conv

Converts direct-style functions and calls to CPS.

axm %cps.conv: %compile.Phase;