(* Danvy and Nielsen's first-order, one pass CPS transformation. *) (* There is no difficulty, since fresh and Abs are always used together. *) type expr = | Var of atom | Abs of < atom * inner expr > | App of expr * expr (* The ``curly E'' function accepts an expression and the name of a continuation. *) fun transform_expr accepts e, k produces f = case e of | App (e0, e1) -> transform_application (e0, e1, Var (k)) | _ -> App (Var (k), transform_value (e)) end (* The ``curly S'' function accepts an application (a pair of expressions) and a continuation (another expression). *) fun transform_application accepts e0, e1, k produces f = case e0, e1 of | App (e00, e01), App (e10, e11) -> fresh x0, x1 in transform_application (e00, e01, Abs (x0, transform_application (e10, e11, Abs (x1, App (App (Var (x0), Var (x1)), k) ) ) ) ) | App (e00, e01), _ -> fresh x0 in transform_application (e00, e01, Abs (x0, App (App (Var (x0), transform_value (e1)), k) ) ) | _, App (e10, e11) -> fresh x1 in transform_application (e10, e11, Abs (x1, App (App (transform_value (e0), Var (x1)), k) ) ) | _, _ -> App (App (transform_value (e0), transform_value (e1)), k) end (* The ``curly T'' function transforms values. *) fun transform_value accepts v produces f = case v of | Var (_) -> v | Abs (x, e) -> fresh k in Abs (x, Abs (k, transform_expr (e, k))) end (* The toplevel transform. *) fun transform accepts e produces f = fresh k in Abs (k, transform_expr (e, k))