K-Normalization (kNormal.ml)

We stated that "compilation is about bridging the gaps between a high-level language and a low-level language," one of which was "nested expressions." For example, ML (as well as most languages) can compute at once the values of expressions like a + b + c - d, but ordinary assembly does not have such an instruction.

This gap is bridged by a translation called K-normalization, which defines every intermediate result of computation as a variable. (The name K-normalization originates in a compiler called ML Kit.) For example, the previous expression can be translated to:

let tmp1 = a + b in
let tmp2 = tmp1 + c in
tmp2 - d

In MinCaml, KNormal.g is the core of K-normalization and KNormal.t is the data type of K-normalized expressions (called K-normal forms). KNormal.g takes an expression before K-normalization with type environment env, and returns the expression after K-normalization paired with its type. (Types are passed around just for annotating variable definitions in let, and are not central to the essence of K-normalization.)

For example, in the case of e1 + e2, e1 is first K-normalized by g env e1, whose result is bound by let to variable x. Then, e2 is also K-normalized by g env e2, whose result is bound by let to variable y, and the expression x + y is returned with its type int.

In order to insert such let, we use an auxiliary function named insert_let. It takes expression e, creates a fresh variable x, and returns the expression let x = e in ... (though, if e is a variable in the first place, insert_let uses this variable as x and does not insert let in fact). It also takes the "continuation" function k, apply it to x, and uses its result for the expression after in (the body "..." above).

By the way, in addition to K-normalization, KNormal.g also translates booleans true and false to integers 1 and 0. In addition, comparisons and conditional branches are translated into combined forms like if e1 <= e2 then e3 else e4 from separate forms such as e1 <= e2 and if e then e1 else e2. This translation bridges one of the gaps between MinCaml and ordinary assembly where comparison and branches are combined. If condition e is not a comparison, it is translated into a comparison as in if e <> 0 then e1 else e2. Also by translating if (not e) then e1 else e2 to if e then e2 else e1 etc., all boolean expressions and conditional branches end up in either of the two forms

if e1 = e2 then e3 else e4


if e1 <= e2 then e3 else e4.

This translation is different from K-normalization, but implemented together with KNormal.g just because separating them requires extra work to define the intermediate data type.

In addition, uses of external variables are limited to calls to external functions (KNormal.ExtFunApp) or references to external arrays (KNormal.ExtArray) because they are necessary and sufficient for most applications. This restriction is also implemented together with K-normalization.