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