(* 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