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