(* Defunctionalized version of the CPS code by Flanagan et al. Even more obscure than the original version, due to the non-local nature of defunctionalization. *) type term = | Var of atom | Lambda of < atom * inner term > | Let of < atom * outer term * inner term > | If0 of term * term * term | App of term * term type continuation = | CIdentity | CLetLeft of < atom * inner term > | CIf0 of continuation * term * term | CAppLeft of continuation * term | CAppRight of continuation * term | CRequireValue of continuation fun normalize_term accepts m produces n = normalize (m, CIdentity) fun normalize accepts m, k produces n = case m of | Var (_) -> fill (k, m) | Lambda (x, body) -> fill (k, Lambda (x, normalize_term (body))) | Let (x, m1, m2) -> normalize (m1, CLetLeft (x, normalize (m2, k))) | If0 (m1, m2, m3) -> normalize_name (m1, CIf0 (k, normalize_term (m2), normalize_term (m3))) | App (m1, m2) -> normalize_name (m1, CAppLeft (k, m2)) end fun normalize_name accepts m, k produces n = normalize (m, CRequireValue (k)) fun fill accepts k, m produces n = case k of | CIdentity -> m | CLetLeft (x, body) -> Let (x, m, body) | CIf0 (k, m2, m3) -> fill (k, If0 (m, m2, m3)) | CAppLeft (k, m2) -> normalize_name (m2, CAppRight (k, m)) | CAppRight (k, m1) -> fill (k, App (m1, m)) | CRequireValue (k) -> case m of | Var (_) -> fill (k, m) | Lambda (_, _) -> fill (k, m) | _ -> fresh x in Let (x, m, fill (k, Var (x))) end end