(* This is the target language of closure conversion (see [cc.fml]). It has closed, binary functions, and pairs. *) type target = | TVar of atom | TAbs of < xve: atom * x: atom * inner t: target > where free(x) # free(xve) (* the two formal arguments have distinct names *) and free(t) <= free(x) U free(xve) (* the function is closed *) | TApp of target * target * target | TUnit | TPair of target * target | TFst of target | TSnd of target | TLet of < atom * outer target * inner target > (* This is the target language of hoisting. It has a toplevel [letrec] for mutually recursive function definitions, and no stand-alone lambda abstractions. *) (* In the definition of the type [toplevel] below, it is important to encode the fact that the definitions are self-contained, i.e., the free variables of the right-hand sides form of a subset of the variables on the left-hand sides. This is expressed by the constraint [free(defs) <= bound(defs)]. This property is used when checking the correctness of the function [hoist] below: in the [TLet] case, in order to prove that [x] does not escape its scope, one needs to know that the definitions that are being lifted do not mention [x]. Requiring this property in turn gives rise to another proof obligation, in the [TAbs] case, where the fact that every function is closed must now be exploited. *) type term = | HVar of atom | HApp of term * term * term | HUnit | HPair of term * term | HFst of term | HSnd of term | HLet of < atom * outer term * inner term > type rhs = | HAbs of < xve: atom * x: atom * inner t: term > where free(x) # free(xve) type definitions binds = | HDefNil | HDefCons of f: atom * inner rhs: rhs * defs: definitions where bound(f) # bound(defs) type toplevel = | HTop of < defs: definitions * inner main: term > where free(defs) <= bound(defs) (* important: the definitions are self-contained *) (* Concatenation of lists of definitions. *) fun cat accepts defs1, defs2 where bound(defs1) # bound (defs2) produces defs where bound(defs) == bound(defs1) U bound(defs2) = case defs1 of | HDefNil -> defs2 | HDefCons (f, rhs, defs1) -> HDefCons (f, rhs, cat (defs1, defs2)) end (* Hoisting definitions out of a term. *) (* With all appropriate definitions in place, the code is straightforward. It is a bit verbose because [HTop] is being constructed and de-constructed ad nauseum, but that is mostly a concrete syntax issue. *) fun hoist accepts t (* target *) produces top (* toplevel *) = case t of | TVar (a) -> HTop (HDefNil, HVar (a)) | TAbs (xve, x, t) -> let HTop (defs, h) = hoist (t) in (* create a fresh name for this function *) fresh f in (* hoist the definition of [f], and replace the lambda abstraction with a reference to [f] *) HTop (HDefCons (f, HAbs (xve, x, h), defs), HVar (f)) | TApp (t1, t2, t3) -> let HTop (defs1, h1) = hoist (t1) in let HTop (defs2, h2) = hoist (t2) in let HTop (defs3, h3) = hoist (t3) in HTop (cat (defs1, cat (defs2, defs3)), HApp (h1, h2, h3)) | TUnit -> HTop (HDefNil, HUnit) | TPair (t1, t2) -> let HTop (defs1, h1) = hoist (t1) in let HTop (defs2, h2) = hoist (t2) in HTop (cat (defs1, defs2), HPair (h1, h2)) | TFst (t) -> let HTop (defs, h) = hoist (t) in HTop (defs, HFst (h)) | TSnd (t) -> let HTop (defs, h) = hoist (t) in HTop (defs, HSnd (h)) | TLet (x, t1, t2) -> let HTop (defs1, h1) = hoist (t1) in let HTop (defs2, h2) = hoist (t2) in HTop (cat (defs1, defs2), HLet (x, h1, h2)) end