The CPS Plugin

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

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 cps2ds_dep: {T: *} → [U: T → *] → [Fn [t: T] → U t] → [[t: T] → U t], 3;
anx lam cps2ds       {T U: *}           (f: Fn     T  → U  ):  [    T  → U  ] = cps2ds_dep (λ (_: T): * = U) f;

Phases

conv

Converts direct-style functions and calls to CPS.

axm conv: compile.Phase;