type term =
  | Var of atom
  | Lambda of < atom * inner term >
  | App of term * term
  | Let of < atom * outer term * inner term >
  | If of term * term * term

type context binds = (*latex \label{line:context} *)
  | CEmpty
  | CLet of x: atom * inner t: term * c: context (*latex \label{line:CLet:def} *)
            where free(t) # free(x) U bound(c)   (*latex \label{line:CLet:guard} *)
  | CCompose of c1: context * c2: context
                where inner(c1) # bound(c2) (*latex \label{line:CCompose:guard} *)

type closure = (*latex \label{line:closure} *)
  | Clo of < context * inner term >

fun fill accepts clo produces u = (*latex \label{line:fill} *)
  let Clo (c, t) = clo in
  case c of
  | CEmpty ->
      t
  | CLet (x, t1, c2) ->
      Let (x, t1, fill (Clo (c2, t)))
  | CCompose (c1, c2) ->
      fill (Clo (c1, fill (Clo (c2, t))))
  end

fun norm accepts t produces u =
  fill (split (t, false)) (*latex \label{line:norm:fill} *)

fun split accepts t, mode produces clo =
  case t of
  | Var (_) ->
      Clo (CEmpty, t)
  | Lambda (x, t) ->
      Clo (CEmpty, Lambda (x, norm (t)))
  | App (t1, t2) ->
      let Clo (c1, u1) = split (t1, true) in
      let Clo (c2, u2) = split (t2, true) in
      let clo = Clo (CCompose (c1, c2), App (u1, u2)) in
      valueify (clo, mode)
  | Let (x, t1, t2) ->
      let Clo (c1, u1) = split (t1, false) in
      let Clo (c2, u2) = split (t2, mode) in
      Clo (CCompose (c1, CLet (x, u1, c2)), u2) (*latex \label{line:error} *)
  | If (t1, t2, t3) ->
      let Clo (c1, u1) = split (t1, true) in
      let clo = Clo (c1, If (u1, norm (t2), norm (t3))) in
      valueify (clo, mode)
  end

fun valueify accepts clo, mode produces clo =
  if mode then
    let Clo (c, t) = clo in
    fresh x in (*latex \label{line:valueify:fresh} *)
    Clo (CCompose (c, CLet (x, t, CEmpty)), Var (x)) (*latex \label{line:valueify:float} *)
  else
    clo
  end