Executable Specification

[View trans.sig] [View trans.mod]

/*
 * Transformations on STLC with recursion
 * Date Created:   October 15, 2014
*/

sig trans.

kind nat type.
type z nat.
type s nat -> nat.

type add   nat -> nat -> nat -> o.
type npred  nat -> nat -> o.
type is_nat  nat -> o.

% Source and target types are in the same category.
kind ty type.

type tnat    ty.                 % for natural numbers
type arr     ty -> ty -> ty.     % for abstractions in source and
                                 %% closures in the target languages.
type tunit   ty.                 % for units
type prod    ty -> ty -> ty.     % for pairs 
type arr'    ty -> ty -> ty.     % for abstractions in the target language


% Source Terms
kind tm type.

type nat         nat -> tm.
type pred        tm -> tm.
type plus        tm -> tm -> tm.
type ifz         tm -> tm -> tm -> tm.
type unit        tm.
type pair        tm -> tm -> tm.
type fst, snd    tm -> tm.
type let         tm -> (tm -> tm) -> tm.
type fix         (tm -> tm -> tm) -> tm.
type app         tm -> tm -> tm.

type bnd         (tm -> tm) -> tm.
type base        tm -> tm.

% Target Terms
kind tm' type.
    
type nat'         nat -> tm'.
type pred'        tm' -> tm'.
type plus'        tm' -> tm' -> tm'.
type ifz'         tm' -> tm' -> tm' -> tm'.
type unit'        tm'.
type pair'        tm' -> tm' -> tm'.
type fst', snd'   tm' -> tm'.
type let'         tm' -> (tm' -> tm') -> tm'.
type abs'         (tm' -> tm') -> tm'.
type app'         tm' -> tm' -> tm'.
type clos'         tm' -> tm' -> tm'.
type open'        tm' -> (tm' -> tm' -> tm') -> tm'.

% Terms
type tm          tm -> o.
type tm'         tm' -> o.
type tm''        tm' -> o.
type tm''_body   tm' -> o.

% Source term list
kind tm_list type.
type snil tm_list.
type scons tm -> tm_list -> tm_list.
type smember tm -> tm_list -> o.
type sappend tm_list -> tm_list -> tm_list -> o.

% Target term list
kind tm'_list type.
type cnil tm'_list.
type ccons tm' -> tm'_list -> tm'_list.
type cmember tm' -> tm'_list -> o.
type cappend tm'_list -> tm'_list -> tm'_list -> o.
type crev tm'_list -> tm'_list -> tm'_list -> o.

% Values
type val         tm -> o.
type val'        tm' -> o.
type tm'_list_val   tm'_list -> o.

% Typing rules
type of          tm -> ty -> o.
type ofc'        tm' -> ty -> o.
type of'         tm' -> ty -> o.
type of''        tm' -> ty -> o.
type of''_env    tm'_list -> ty -> o.
type of''_body   ty -> tm' -> ty -> o.

% Well-formed types
type is_sty       ty -> o.
type is_cty       ty -> o.

% Call-by-value evaluation rules in small steps
type step        tm -> tm -> o.
type nstep       nat -> tm -> tm -> o.
type eval        tm -> tm -> o.
type step'        tm' -> tm' -> o.
type nstep'       nat -> tm' -> tm' -> o.
type eval'        tm' -> tm' -> o.
type eval''       tm' -> tm' -> o.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%          CPS Transformation                 %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
type cps  tm -> (tm -> tm) -> tm -> o.
type cps' tm -> tm -> o.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%          Closure Conversion                 %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Mapping from source variables to target terms
kind map type.
type map tm -> tm' -> map.
kind map_list type.
type mnil map_list.
type mcons map -> map_list -> map_list.
type mmember map -> map_list -> o.
type mappend map_list -> map_list -> map_list -> o.

% Projection from free variables to an environment parameter
type mapvar tm_list -> (tm' -> map_list) -> o.

% Forming the closure environment
type mapenv tm_list -> map_list -> tm' -> o.

% Collecting free variables in an abstraction
type notfree tm -> o.
type fvars tm -> tm_list -> tm_list -> o.

% Combining two lists; avoiding redundancy is not essential for correctness
type combine tm_list -> tm_list -> tm_list -> o.

% Closure conversion
% The first argument is a mapping from free variables to target terms 
% and the second argument is a list of these free variables
type cc map_list -> tm_list -> tm -> tm' -> o.
type cc' tm -> tm' -> o.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%          Code Hoisting                      %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Hoisted terms consisting of a list of closed functions and the body
type hbase     tm' -> tm'.             % Base term of the body
type habs      (tm' -> tm') -> tm'.    % Top-level bindings of the body
type htm       tm'_list -> tm' -> tm'. % The hoisted term

% Combining the bodies of two hoisted terms
type hcombine      tm' -> tm' -> (tm' -> tm' -> tm') -> tm' -> o.
type hcombine3     tm' -> tm' -> tm' ->
                   (tm' -> tm' -> tm' -> tm') -> tm' -> o.
type hcombine_abs  tm' -> (tm' -> tm') -> 
                   (tm' -> (tm' -> tm') -> tm') -> tm' -> o.

% Apply the construct under the abstractions of 
% the body hoisted terms.
type hconstr       tm' -> (tm' -> tm') -> tm' -> o.

% Extract functions out of an abstraction and produce
% a closed abstraction
type hoist_abs     (tm' -> tm') -> tm' -> tm' -> tm'_list -> 
                   tm' -> (tm' -> tm') -> o.
type abstract   (tm' -> tm') -> (tm' -> tm') -> (tm' -> tm' -> tm') -> o.

type tm'_list_to_tuple     tm'_list -> tm' -> o.

% Code hoisting
type ch        tm' -> tm' -> o.

/*
 * Transformations on STLC with recursion
 * Date Created:   October 15, 2014
*/

module trans.

% Addition of natural numbers
add z N N.
add (s N1) N2 (s N3) :- add N1 N2 N3.

npred z z.
npred (s N) N.

is_nat z.
is_nat (s N) :- is_nat N.


% Lists
smember X (scons X L).
smember Y (scons X L) :- smember Y L.
sappend snil L L.
sappend (scons X L1) L2 (scons X L3) :- sappend L1 L2 L3.


cmember X (ccons X L).
cmember Y (ccons X L) :- cmember Y L.
cappend cnil L L.
cappend (ccons X L1) L2 (ccons X L3) :- cappend L1 L2 L3.
crev cnil L L.
crev (ccons X L1) L2 L :- crev L1 (ccons X L2) L.

mmember X (mcons X L).
mmember Y (mcons X L) :- mmember Y L.
mappend mnil L L.
mappend (mcons X L1) L2 (mcons X L3) :- mappend L1 L2 L3.

% Source types
is_sty tnat.
is_sty tunit.
is_sty (prod T1 T2) :- is_sty T1, is_sty T2.
is_sty (arr T1 T2) :- is_sty T1, is_sty T2.

is_cty tnat.
is_cty tunit.
is_cty (prod T1 T2) :- is_cty T1, is_cty T2.
is_cty (arr T1 T2) :- is_cty T1, is_cty T2.
is_cty (arr' T1 T2) :- is_cty T1, is_cty T2.

% Typing rules for the source language
of (nat N) tnat.
of (pred M) tnat :- of M tnat.
of (plus M1 M2) tnat :- of M1 tnat, of M2 tnat.
of (ifz M M1 M2) T :- of M tnat, of M1 T, of M2 T.
of unit tunit.
of (pair M1 M2) (prod T1 T2) :- of M1 T1, of M2 T2.
of (fst M) T1 :- of M (prod T1 T2).
of (snd M) T2 :- of M (prod T1 T2).
of (let M R) T :- 
    of M T1, (pi x\ of x T1 => of (R x) T).
of (fix R) (arr T1 T2) :-
    pi f\ pi x\ of f (arr T1 T2) => of x T1 => of (R f x) T2,
    is_sty (arr T1 T2).
of (app M1 M2) T :- of M1 (arr T1 T), of M2 T1.

% Typing rules for the target language
ofc' (nat' N) tnat.
ofc' (pred' M) tnat :- ofc' M tnat.
ofc' (plus' M1 M2) tnat :- ofc' M1 tnat, ofc' M2 tnat.
ofc' (ifz' M M1 M2) T :- ofc' M tnat, ofc' M1 T, ofc' M2 T.
ofc' unit' tunit.
ofc' (pair' M1 M2) (prod T1 T2) :- ofc' M1 T1, ofc' M2 T2.
ofc' (fst' M) T1 :- ofc' M (prod T1 T2).
ofc' (snd' M) T2 :- ofc' M (prod T1 T2).
ofc' (let' M R) T :- 
    ofc' M T1, pi x\ ofc' x T1 => ofc' (R x) T.
ofc' (abs' R) (arr' T1 T2) :-
    pi x\ ofc' x T1 => ofc' (R x) T2, is_cty T1.
ofc' (app' M1 M2) T :- ofc' M1 (arr' T1 T), ofc' M2 T1.
ofc' (clos' F E) (arr T1 T2) :-
    ofc' F (arr' (prod (arr T1 T2) (prod T1 TL)) T2), ofc' E TL.
ofc' (open' M R) T :-
    ofc' M (arr T1 T2),
    pi f\ pi e\ pi l\
      ofc' f (arr' (prod (arr T1 T2) (prod T1 l)) T2) =>
      ofc' e l =>
      ofc' (R f e) T.

% The target typing rules can be reduced to the following ones when only
% terms involved in code hoisting are considered
of' (nat' N) tnat.
of' (pred' M) tnat :- of' M tnat.
of' (plus' M1 M2) tnat :- of' M1 tnat, of' M2 tnat.
of' (ifz' M M1 M2) T :- of' M tnat, of' M1 T, of' M2 T.
of' unit' tunit.
of' (pair' M1 M2) (prod T1 T2) :- of' M1 T1, of' M2 T2.
of' (fst' M) T1 :- of' M (prod T1 T2).
of' (snd' M) T2 :- of' M (prod T1 T2).
of' (let' M R) T :- 
    of' M T1, pi x\ of' x T1 => of' (R x) T.
of' (abs' R) (arr' T1 T2) :-
    pi x\ of' x T1 => of' (R x) T2, is_cty T1.
of' (app' M1 M2) T :- of' M1 (arr' T1 T), of' M2 T1.
of' (clos' F E) (arr T1 T2) :-
    of' F (arr' (prod (arr T1 T2) (prod T1 TL)) T2), of' E TL.
of' (open' M1 (f\ e\ app' f (pair' M1 (pair' M2 e)))) T2 :-
    of' M1 (arr T1 T2), of' M2 T1.

% Typing rules for hoisted terms
of'' (htm cnil (hbase M)) T :- of' M T.
of'' (htm (ccons M L) (habs R)) T :-
  of' M T1, pi x\ of' x T1 => of'' (htm L (R x)) T.
of''_env cnil tunit.
of''_env (ccons M ML) (prod T TE) :- 
  of' M T, of''_env ML TE.
of''_body tunit (hbase M) T :- of' M T.
of''_body (prod T1 TE) (habs R) T :-
  (pi x\ of' x T1 => of''_body TE (R x) T),
  is_cty T1.

% Source terms
tm (nat N).
tm (pred M) :- tm M.
tm (plus M1 M2) :- tm M1, tm M2.
tm (ifz M M1 M2) :- tm M, tm M1, tm M2.
tm unit.
tm (pair M1 M2) :- tm M1, tm M2.
tm (fst M) :- tm M.
tm (snd M) :- tm M.
tm (let M R) :- tm M, pi x\ tm x => tm (R x).
tm (fix R) :- pi f\ pi x\ tm f => tm x => tm (R f x).
tm (app M1 M2) :- tm M1, tm M2.

% Target terms
tm' (nat' N).
tm' (pred' M) :- tm' M.
tm' (plus' M1 M2) :- tm' M1, tm' M2.
tm' (ifz' M M1 M2) :- tm' M, tm' M1, tm' M2.
tm' unit'.
tm' (pair' M1 M2) :- tm' M1, tm' M2.
tm' (fst' M) :- tm' M.
tm' (snd' M) :- tm' M.
tm' (let' M R) :- tm' M, pi x\ tm' x => tm' (R x).
tm' (abs' R) :- pi x\ tm' x => tm' (R x).
tm' (app' M1 M2) :- tm' M1, tm' M2.
tm' (clos' M1 M2) :- tm' M1, tm' M2.
tm' (open' M R) :- tm' M, pi f\ pi e\ tm' f => tm' e => tm' (R f e).

% Hoisted terms
tm'' (htm cnil (hbase M)) :- tm' M.
tm'' (htm (ccons M L) (habs R)) :-
  tm' M, pi x\ tm' x => tm'' (htm L (R x)).
tm''_body (hbase M) :- tm' M.
tm''_body (habs R) :- pi x\ tm' x => tm''_body (R x).

% Source values
val (nat N).
val unit.
val (pair V1 V2) :- val V1, val V2.
val (fix R).

% Target values
val' (nat' N).
val' unit'.
val' (pair' V1 V2) :- val' V1, val' V2.
val' (abs' R).
val' (clos' F E) :- val' F, val' E.

tm'_list_val cnil.
tm'_list_val (ccons V VL) :- 
  val' V, tm'_list_val VL.


% Source evaluation rules
step (pred M) (pred M') :- step M M'.
step (pred (nat N)) (nat N') :- npred N N'.
step (plus M1 M2) (plus M1' M2) :- step M1 M1'.
step (plus V1 M2) (plus V1 M2') :- val V1, step M2 M2'.
step (plus (nat N1) (nat N2)) (nat N) :- add N1 N2 N.
step (ifz M M1 M2) (ifz M' M1 M2) :- step M M'.
step (ifz (nat z) M1 M2) M1.
step (ifz (nat (s N)) M1 M2) M2.
step (pair M1 M2) (pair M1' M2) :- step M1 M1'.
step (pair V1 M2) (pair V1 M2') :- val V1, step M2 M2'.
step (fst M) (fst M') :- step M M'.
step (fst (pair V1 V2)) V1 :- val (pair V1 V2).
step (snd M) (snd M') :- step M M'.
step (snd (pair V1 V2)) V2 :- val (pair V1 V2).
step (let M R) (let M' R) :- step M M'.
step (let V R) (R V) :- val V.
step (app M1 M2) (app M1' M2) :- step M1 M1'.
step (app V1 M2) (app V1 M2') :- val V1, step M2 M2'.
step (app (fix R) V) (R (fix R) V) :- val V.

nstep z M M.
nstep (s N) M M'' :- step M M', nstep N M' M''.

eval M V :- nstep N M V, val V.

% Target evaluation rules
step' (pred' M) (pred' M') :- step' M M'.
step' (pred' (nat' N)) (nat' N') :- npred N N'.
step' (plus' M1 M2) (plus' M1' M2) :- step' M1 M1'.
step' (plus' V1 M2) (plus' V1 M2') :- val' V1, step' M2 M2'.
step' (plus' (nat' N1) (nat' N2)) (nat' N) :- add N1 N2 N.
step' (ifz' M M1 M2) (ifz' M' M1 M2) :- step' M M'.
step' (ifz' (nat' z) M1 M2) M1.
step' (ifz' (nat' (s N)) M1 M2) M2.
step' (pair' M1 M2) (pair' M1' M2) :- step' M1 M1'.
step' (pair' V1 M2) (pair' V1 M2') :- val' V1, step' M2 M2'.
step' (fst' M) (fst' M') :- step' M M'.
step' (fst' (pair' V1 V2)) V1 :- val' (pair' V1 V2).
step' (snd' M) (snd' M') :- step' M M'.
step' (snd' (pair' V1 V2)) V2 :- val' (pair' V1 V2).
step' (let' M R) (let' M' R) :- step' M M'.
step' (let' V R) (R V) :- val' V.
step' (app' M1 M2) (app' M1' M2) :- step' M1 M1'.
step' (app' V1 M2) (app' V1 M2') :- val' V1, step' M2 M2'.
step' (app' (abs' R) V) (R V) :- val' V.
step' (clos' F E) (clos' F' E) :- step' F F'.
step' (clos' F E) (clos' F E') :- val' F, step' E E'.
step' (open' M R) (open' M' R) :- step' M M'.
step' (open' (clos' F E) R) (R F E) :- val' (clos' F E).

nstep' z M M.
nstep' (s N) M M'' :- step' M M', nstep' N M' M''.

eval' M V :- nstep' N M V, val' V.

% Evaluation for hoisted terms
eval'' (htm cnil (hbase M)) V :- eval' M V.
eval'' (htm (ccons F FE) (habs R)) V :- eval'' (htm FE (R F)) V.

% Auxiliary relations
mapvar snil (e\ mnil).
mapvar (scons X L) 
       (e\ mcons (map X (fst' e)) (Map (snd' e))) :-
     mapvar L Map.

mapenv snil _ unit'.
mapenv (scons X L) Map (pair' M ML) :-
       mmember (map X M) Map, mapenv L Map ML.

combine snil FVs2 FVs2.
combine (scons X FVs1) FVs2 FVs :-
      smember X FVs2, combine FVs1 FVs2 FVs.
combine (scons X FVs1) FVs2 (scons X FVs) :-
      combine FVs1 FVs2 FVs.

% Computing free variables
fvars X _ snil :- notfree X.
fvars Y Vs (scons Y snil) :- smember Y Vs.
fvars (nat _) _ snil.
fvars (pred M) Vs FVs :- fvars M Vs FVs.
fvars (plus M1 M2) Vs FVs :-
  fvars M1 Vs FVs1, fvars M2 Vs FVs2, combine FVs1 FVs2 FVs.
fvars (ifz M M1 M2) Vs FVs' :-
  fvars M Vs FVs, fvars M1 Vs FVs1, fvars M2 Vs FVs2,
  combine FVs FVs1 FVs1', combine FVs1' FVs2 FVs'.
fvars unit _ snil.
fvars (pair M1 M2) Vs FVs :-
  fvars M1 Vs FVs1, fvars M2 Vs FVs2, combine FVs1 FVs2 FVs.
fvars (fst M) Vs FVs :- fvars M Vs FVs.
fvars (snd M) Vs FVs :- fvars M Vs FVs.
fvars (let M R) Vs FVs:-
  fvars M Vs FVs1,
  (pi x\ notfree x => fvars (R x) Vs FVs2),
  combine FVs1 FVs2 FVs.
fvars (fix R) Vs FVs :-
  pi f\ pi x\ notfree f => notfree x => fvars (R f x) Vs FVs.
fvars (app M1 M2) Vs FVs :-
  fvars M1 Vs FVs1, fvars M2 Vs FVs2, combine FVs1 FVs2 FVs.


% Closure conversion
cc _ _ (nat N) (nat' N).
cc Map Vs X M :- mmember (map X M) Map.
cc Map Vs (pred M) (pred' M') :- cc Map Vs M M'.
cc Map Vs (plus M1 M2) (plus' M1' M2') :- 
   cc Map Vs M1 M1', cc Map Vs M2 M2'.
cc Map Vs (ifz M M1 M2) (ifz' M' M1' M2') :-
   cc Map Vs M M', cc Map Vs M1 M1', cc Map Vs M2 M2'.
cc Map Vs unit unit'.
cc Map Vs (pair M1 M2) (pair' M1' M2') :-
   cc Map Vs M1 M1', cc Map Vs M2 M2'.
cc Map Vs (fst M) (fst' M') :- cc Map Vs M M'.
cc Map Vs (snd M) (snd' M') :- cc Map Vs M M'.
cc Map Vs (let M R) (let' M' R') :-
   cc Map Vs M M', 
   pi x\ pi y\ cc (mcons (map x y) Map) (scons x Vs) (R x) (R' y).
cc Map Vs (fix R) 
          (clos' (abs' (p\ let' (fst' p) (g\ 
                           let' (fst' (snd' p)) (y\
                           let' (snd' (snd' p)) (e\
                           R' g y e)))))
                E) :-
   fvars (fix R) Vs FVs,
   mapenv FVs Map E,
   mapvar FVs NMap,
   pi f\ pi x\ pi g\ pi y\ pi e\
     cc (mcons (map x y) (mcons (map f g) (NMap e)))
        (scons x (scons f FVs))
        (R f x)
        (R' g y e).
cc Map Vs (app M1 M2) 
          (let' M1' (g\ open' g (f\ e\ app' f (pair' g (pair' M2' e))))) :-
   cc Map Vs M1 M1',
   cc Map Vs M2 M2'.

cc' M M' :- cc mnil snil M M'.

% CPS Transformation
cps (nat N) K (K (nat N)).
cps (pred M) K M' :-
  cps M (x\ let (pred x) (v\ K v)) M'.
cps (plus M1 M2) K M' :-
  pi x1\ cps M2 (x2\ let (plus x1 x2) (v\ K v)) (M2' x1),
  cps M1 M2' M'.
cps (ifz M1 M2 M3) K M' :-
  cps M2 K M2', cps M3 K M3', cps M1 (x1\ ifz x1 M2' M3') M'.
cps unit K (K unit).
cps (pair M1 M2) K M' :-
  pi x1\ cps M2 (x2\ let (pair x1 x2) (v\ K v)) (M2' x1),
  cps M1 M2' M'.
cps (fst M) K M' :-
  cps M (x\ let (fst x) (v\ K v)) M'.
cps (snd M) K M' :-
  cps M (x\ let (snd x) (v\ K v)) M'.
cps (let M R) K M' :-
  pi x\ (pi k\ cps x k (k x)) => cps (R x) K (R' x), cps M R' M'.
cps (fix R) K 
    (let (fix (f\p\ let (fst p) (k\ let (snd p) (x\ R' f k x)))) K) :-
  pi k\ pi f\ pi x\ (pi k\ cps f k (k f)) => (pi k\ cps x k (k x)) =>
    cps (R f x) (y\ app k y) (R' f k x).
cps (app M1 M2) K M' :-
  pi x1\ cps M2 
             (x2\ let (fix f\ K) (k\ let (pair k x2) (p\ app x1 p))) 
             (M2' x1),
  cps M1 M2' M'.

cps' M M' :- cps M (x\x) M'.


% Code Hoisting
ch (nat' N) (htm cnil (hbase (nat' N))).
ch (pred' M) (htm FE M'') :- 
  ch M (htm FE M'), hconstr M' (x\ pred' x) M''.
ch (plus' M1 M2) (htm FE M') :-
  ch M1 (htm FE1 M1'), ch M2 (htm FE2 M2'),
  cappend FE1 FE2 FE, hcombine M1' M2' (x\y\ plus' x y) M'.
ch (ifz' M1 M2 M3) (htm FE M') :-
  ch M1 (htm FE1 M1'), ch M2 (htm FE2 M2'), ch M3 (htm FE3 M3'),
  cappend FE1 FE2 FE12, cappend FE12 FE3 FE,
  hcombine3 M1' M2' M3' (x\y\z\ ifz' x y z) M'.
ch unit' (htm cnil (hbase unit')).
ch (pair' M1 M2) (htm FE M') :-
  ch M1 (htm FE1 M1'), ch M2 (htm FE2 M2'), 
  cappend FE1 FE2 FE, hcombine M1' M2' (x\y\ pair' x y) M'.
ch (let' M R) (htm FE M'') :-
  ch M (htm FE1 M'), (pi x\ ch x (htm cnil (hbase x)) => ch (R x) (htm FE2 (R' x))), 
  cappend FE1 FE2 FE, hcombine_abs M' R' (x\y\ let' x y) M''.
ch (fst' M) (htm FE M'') :- ch M (htm FE M'), hconstr M' (x\ fst' x) M''.
ch (snd' M) (htm FE M'') :- ch M (htm FE M'), hconstr M' (x\ snd' x) M''.
ch (app' M1 M2) (htm FE M') :-
  ch M1 (htm FE1 M1'), ch M2 (htm FE2 M2'), 
  cappend FE1 FE2 FE, hcombine M1' M2' (x\y\ app' x y) M'.
ch (abs' R) (htm (ccons (abs' l\ abs' (x\ F l x)) FE) (habs R'')):-
  (pi x\ ch x (htm cnil (hbase x)) => ch (R x) (htm FE (R' x))),
  abstract R' R'' F.
ch (clos' M1 M2) (htm FE M') :-
  ch M1 (htm FE1 M1'), ch M2 (htm FE2 M2'), 
  cappend FE1 FE2 FE, hcombine M1' M2' (x\y\ clos' x y) M'.
% Since the environment of a closure is not visible to user,
% code hoisting for an expression for unpacking closures
% will not inspect the environment parameter. The particular
% form of unpacking expressions dealt by code hoisting matches
% the output of closure conversion
ch (open' M1 (f\ e\ app' f (pair' M1 (pair' M2 e)))) (htm FE M') :-
  ch M1 (htm FE1 M1'),
  ch M2 (htm FE2 M2'),
  cappend FE1 FE2 FE,
  hcombine M1' M2' 
           (x\y\ (open' x (f\ e\ app' f (pair' x (pair' y e))))) M'.

hcombine (hbase M1) (hbase M2) C (hbase (C M1 M2)).
hcombine (habs R) M C (habs R') :-
  pi f\ hcombine (R f) M C (R' f).
hcombine (hbase M) (habs R) C (habs R') :-
  pi f\ hcombine (hbase M) (R f) C (R' f).

hcombine3 (hbase M1) (hbase M2) (hbase M3) C (hbase (C M1 M2 M3)).
hcombine3 (habs R) M2 M3 C (habs R') :-
  pi f\ hcombine3 (R f) M2 M3 C (R' f).
hcombine3 (hbase M1) (habs R) M3 C (habs R') :-
  pi f\ hcombine3 (hbase M1) (R f) M3 C (R' f).
hcombine3 (hbase M1) (hbase M2) (habs R) C (habs R') :-
  pi f\ hcombine3 (hbase M1) (hbase M2) (R f) C (R' f).

hcombine_abs (hbase M1) (x\ hbase (M2 x)) C (hbase (C M1 M2)).
hcombine_abs (habs R) M C (habs R') :-
  pi f\ hcombine_abs (R f) M C (R' f).
hcombine_abs (hbase M) (x\ habs (R x)) C (habs R') :-
  pi f\ hcombine_abs (hbase M) (x\ R x f) C (R' f).

hconstr (hbase M) C (hbase (C M)).
hconstr (habs R) C  (habs R') :- pi f\ hconstr (R f) C (R' f).

abstract R R' F :- 
  pi f\ pi l\ hoist_abs R f l cnil (R' f) (x\ F l x).
% Suppose we start with an abstraction over a hoisted term 
%     (x\ habs f1\ ... habs fn\ hbase M)
% hoist_abs maintains the following invariant: at the i-th step
% 1) The first argument is (x\ habs fi\ ... habs fn\ hbase M)
% 2) The second argument is f that binds the final abstraction
% 3) The third argument is (snd' (... (snd' l))) where l is
%    the variable pointing to the list of functions generated from
%    the function environment and snd is applied (i-1) times.
%    That is, it should evaluate to (fi,....,fn).
% 4) The forth argument is [f(i-1),...,f1]
% 5) The fifth argument is 
%    (habs fi\... habs fn\ app' f [f1,...,fn])
% 6) The sixth argument is
%     x\
%     let' fi = Pi(i,l) in 
%     ...
%     let' fn = Pi(n,l) in
%       M
%    where Pi(i,l) is the i-th element of l.
hoist_abs (x\ hbase (R x)) F L FA (hbase (app' F FA'')) R :-
  crev FA cnil FA', tm'_list_to_tuple FA' FA''.
hoist_abs (x\ habs (R x)) F L FA (habs F') (x\ let' (fst' L) (R' x)) :-
  pi f\ hoist_abs (x\ R x f) F (snd' L) (ccons f FA) (F' f) (x\ R' x f).

tm'_list_to_tuple cnil unit'.
tm'_list_to_tuple (ccons M ML) (pair' M ML') :-
  tm'_list_to_tuple ML ML'.