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'.

% CMinor like code
type dummyval     tm'.
type loc'         nat -> tm'.
type alloc'       nat -> tm'.
type move'        tm' -> nat -> tm' -> tm'.
type load'        tm' -> nat -> tm'.

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

% List
type memb    A -> list A -> o.
type appd    list A -> list A -> list A -> o.
type combine list A -> list A -> list A -> o.
type rev list A -> list A -> list A -> o.

% Mapping 
kind map type -> type -> type.
type map A -> B -> map A B.

% Values
type val         tm -> o.
type val'        tm' -> o.
type tm'_list_val   list tm' -> o.
type val''       tm' -> 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    list tm' -> 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.

% Evaluation semantics of generated code using heaps
kind state        type.
type st           nat -> (list (map nat tm')) -> state.
type allocate     nat -> nat -> (list (map nat tm')) -> (list (map nat tm')) -> o.
type update_heap  (list (map nat tm')) -> nat -> tm' -> (list (map nat tm')) -> o.
type lookup_heap  (list (map nat tm')) -> nat -> tm' -> o.
type step''       state -> tm' -> state -> tm' -> o.
type nstep''      nat -> state -> tm' -> state -> tm' -> o.
type heval        tm' -> state -> tm' -> o.
type eval'''      tm' -> state -> tm' -> o.

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

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

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

% Forming the closure environment
type mapenv list tm -> list (map tm tm') -> tm' -> o.

% Collecting free variables in an abstraction
type notfree tm -> o.
type fvars tm -> list tm -> list tm -> 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    list (map tm tm') -> list tm -> 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       list tm' -> 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' -> list tm' -> 
                   tm' -> (tm' -> tm') -> o.
type abstract   (tm' -> tm') -> (tm' -> tm') -> (tm' -> tm' -> tm') -> o.

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

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


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%          Code Generation                    %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

type cgen       tm' -> (tm' -> tm') -> tm' -> o.

type ecgen      list tm' -> list tm' -> o.
type bcgen      tm' -> tm' -> o.
type hcgen'     tm' -> tm' -> o.
type hcgen      tm' -> tm' -> o.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%          Full Compilation                   %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

type compile    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
memb X (X :: L).
memb Y (X :: L) :- memb Y L.
appd nil L L.
appd (X :: L1) L2 (X :: L3) :- appd L1 L2 L3.
rev nil L L.
rev (X :: L1) L2 L :- rev L1 (X :: L2) L.
combine nil L L.
combine (X :: L1) L2 L :-
      memb X L2, combine L1 L2 L.
combine (X :: L1) L2 (X :: L) :-
      combine L1 L2 L.


% Mapping

% 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 nil (hbase M)) T :- of' M T.
of'' (htm (M :: L) (habs R)) T :-
  of' M T1, pi x\ of' x T1 => of'' (htm L (R x)) T.
of''_env nil tunit.
of''_env (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 nil (hbase M)) :- tm' M.
tm'' (htm (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 nil.
tm'_list_val (V :: VL) :- 
  val' V, tm'_list_val VL.

% Values in generated code
val'' dummyval.
val'' (loc' L).
val'' (nat' N).
val'' (abs' R).


% 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 nil (hbase M)) V :- eval' M V.
eval'' (htm (F :: FE) (habs R)) V :- eval'' (htm FE (R F)) V.

% Evaluations semantics of generated code
step'' St (pred' (nat' N)) St (nat' N') :- npred N N'.
step'' St (plus' (nat' N1) (nat' N2)) St (nat' N) :- add N1 N2 N.
step'' St (ifz' (nat' z) M1 M2) St M1.
step'' St (ifz' (nat' (s N)) M1 M2) St M2.
step'' (st N H) (alloc' S) (st N' H') (loc' N) :-
  add N S N', allocate N S H H'.
step'' (st N H) (move' (loc' L) S V) (st N H') dummyval :-
  add L S L', update_heap H L' V H'.
step'' (st N H) (load' (loc' L) S) (st N H) V :-
  add L S L', lookup_heap H L' V.
step'' St (let' M R) St' (let' M' R) :- step'' St M St' M'.
step'' St (let' V R) St (R V) :- val'' V.
step'' St (app' (abs' R) V) St (R V) :- val'' V.

allocate N z H H.
allocate N (s S) H H' :- 
  allocate (s N) S (map N dummyval :: H) H'.
  
update_heap (map L V :: H) L V' (map L V' :: H).
update_heap (M :: H) L V' (M :: H') :- update_heap H L V' H'.

lookup_heap (map L V :: H) L V.
lookup_heap (M :: H) L V :- lookup_heap H L V.

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

heval M St V :- nstep'' N (st z nil) M St V, val'' V. 
eval''' (htm nil (hbase M)) St V :- heval M St V.
eval''' (htm (F :: FE) (habs R)) St V :- eval''' (htm FE (R F)) St V.


% Auxiliary relations
mapvar nil (e\ nil).
mapvar (X :: L) 
       (e\ (map X (fst' e)) :: (Map (snd' e))) :-
     mapvar L Map.

mapenv nil _ unit'.
mapenv (X :: L) Map (pair' M ML) :-
       memb (map X M) Map, mapenv L Map ML.

% Computing free variables
fvars X _ nil :- notfree X.
fvars Y Vs (Y :: nil) :- memb Y Vs.
fvars (nat _) _ nil.
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 _ nil.
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 :- memb (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 ((map x y) :: Map) (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 ((map x y) :: (map f g) :: (NMap e))
        (x :: 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 nil nil 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' :-
  (pi k\ cps M2 (x\ app k x) (M2' k)),
  (pi k\ cps M3 (x\ app k x) (M3' k)),
  cps M1 (x1\ let (fix f\ K) (k\ ifz x1 (M2' k) (M3' k))) 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 nil (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'),
  appd 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'),
  appd FE1 FE2 FE12, appd FE12 FE3 FE,
  hcombine3 M1' M2' M3' (x\y\z\ ifz' x y z) M'.
ch unit' (htm nil (hbase unit')).
ch (pair' M1 M2) (htm FE M') :-
  ch M1 (htm FE1 M1'), ch M2 (htm FE2 M2'), 
  appd 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 nil (hbase x)) => ch (R x) (htm FE2 (R' x))), 
  appd 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'), 
  appd FE1 FE2 FE, hcombine M1' M2' (x\y\ app' x y) M'.
ch (abs' R) (htm ((abs' l\ abs' (x\ F l x)) :: FE) (habs R'')) :-
  (pi x\ ch x (htm nil (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'), 
  appd 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'),
  appd 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 nil (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 :-
  rev FA nil 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) (f :: FA) (F' f) (x\ R' x f).

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


% Code Generation
cgen (nat' N) K (K (nat' N)).
cgen (pred' M) K M' :-
  cgen M (x\ let' (pred' x) (v\ K v)) M'.
cgen (plus' M1 M2) K M' :-
  (pi x1\ cgen M2 (x2\ let' (plus' x1 x2) (v\ K v)) (M2' x1)),
  cgen M1 M2' M'.
cgen (ifz' M1 M2 M3) K M' :-
  cgen M2 (x\x) M2', cgen M3 (x\x) M3',
  cgen M1 (x1\ let' (ifz' x1 M2' M3') (v\ K v)) M'.
cgen unit' K (K dummyval).
cgen (pair' M1 M2) K M' :-
  (pi x1\ cgen M2 
                 (x2\ let' (alloc' (s (s z))) (p\
                      let' (move' p z x1) (u1\
                      let' (move' p (s z) x2) (u2\
                      K p))))
                 (M2' x1)),
  cgen M1 M2' M'.
cgen (fst' M) K M' :-
  cgen M (x\ let' (load' x z) (v\ K v)) M'.
cgen (snd' M) K M' :-
  cgen M (x\ let' (load' x (s z)) (v\ K v)) M'.
cgen (let' M R) K M' :-
  pi x\ (pi k\ cgen x k (k x)) => cgen (R x) K (R' x), cgen M R' M'.
cgen (app' M1 M2) K M' :-
  pi x1\ cgen M2 (x2\ let' (app' x1 x2) (v\ K v)) (M2' x1),
  cgen M1 M2' M'.
cgen (clos' M1 M2) K M' :- cgen (pair' M1 M2) K M'.
cgen (open' M1 (f\ e\ app' f (pair' M1 (pair' M2 e)))) K M' :-
  (pi f\ pi e\ pi x1\
      cgen M2 (x2\ let' (alloc' (s (s z))) (p1\
                   let' (move' p1 z x2) (v1\
                   let' (move' p1 (s z) e) (v2\
                   let' (alloc' (s (s z))) (p2\
                   let' (move' p2 z x1) (v3\
                   let' (move' p2 (s z) p1) (v4\
                   let' (app' f p2) (v\ K v))))))))
           (M3 f e x1)),
  cgen M1 (x1\ let' (load' x1 z) (f\
               let' (load' x1 (s z)) (e\
               M3 f e x1)))
       M'.


ecgen nil nil.
ecgen ((abs' l\ abs' x\ F l x) :: FE) 
        ((abs' l\ abs' x\ F' l x) :: FE') :-
  (pi l\ pi x\ 
    (pi k\ cgen l k (k l)) => (pi k\ cgen x k (k x)) => 
    cgen (F l x) (x\x) (F' l x)),
  ecgen FE FE'.

bcgen (hbase M) (hbase M') :- cgen M (x\x) M'.
bcgen (habs R) (habs R') :- 
  pi x\ (pi k\ cgen x k (k x)) => bcgen (R x) (R' x). 

hcgen (htm FE M) (htm FE M).
hcgen' (htm FE M) (htm FE' M') :- 
  ecgen FE FE', bcgen M M'.

compile M M' :- 
  cps' M M1, cc' M1 M2,
  ch M2 (htm FE M3), hcgen (htm FE M3) M'.