Library Cpsopt
Require Import List.
Require Import Coqlib.
Require Import Fml.
Require Import CPS.
Require Import CPS_subst.
Require Import CPS_pre.
Require Import f2cps.
Require Import f2cps_help.
I. The smart App
Definition App_beta (t1 t2: cpsterm) :=
match cps_case_of t1 with
| clamb t => if (is_catom t2) then (CTsubst_rec (t2::nil) nil t O O ) else unApp t1 t2
| other => unApp t1 t2
end.
II. smart constructors
Definition Appn_bodyk (k:cpsterm) (n:nat) :=
TApp (CVar n) (k :: mklist n).
Definition Constr_bodyk (k:cpsterm)(m ari:nat) :=
unApp k (TConstr m (mklist ari)).
III. CPs conversion of terms
Fixpoint cps3 (t:term) (k:cpsterm) {struct t}:cpsterm:=
match t with
| Var n => App_beta k (TVar n)
| Lamb ari t1 =>
App_beta k (TLamb (S ari) (cps3 t1 (CVar O)))
| Mu ari t1 =>
App_beta k (TMu (S ari) (cps3 t1 (CVar O)))
| App t1 t2 =>
let fix cps3_list (tl0 : list term) ( k:cpsterm) {struct tl0}: cpsterm :=
match tl0 with
| nil => k
| a :: b => (cps3 a (TLamb 0 ( cps3_list b k )))
end in
cps3 t1 (TLamb 0 (cps3_list t2
(Appn_bodyk (Clift_n k (S(length t2)))(length t2) )))
| tLet t1 t2 => cps3 t1 (TLamb 0 (TLet (CVar O) (cps3 t2 (Tlift (Clift k)1))))
|Con m tl => if is_atom_list tl then
let fix cps3_atom_list (tl:list term):=
match tl with
| nil => nil
| a::b => cps3_atom a::cps3_atom_list b
end in (App_beta k (TConstr m (cps3_atom_list tl)))
else
let fix cps3_list (tl0 : list term) ( k:cpsterm) {struct tl0}: cpsterm :=
match tl0 with
| nil => k
| a :: b => (cps3 a (TLamb 0 ( cps3_list b k )))
end in
cps3_list tl ( Constr_bodyk (Clift_n k (length tl)) m (length tl))
|Match t1 pl =>
let fix cps3_plist (pl:list pat) (k:cpsterm) {struct pl}:list cpat:=
match pl with
| nil => nil | a::m => cps3_pat a k::cps3_plist m k end
in cps3 t1 (TLamb 0 (TMatch (CVar O) (cps3_plist pl (Clift k))))
end
with cps3_pat (p:pat) (k:cpsterm) {struct p}:cpat:=
match p with | Patc m t1=> TPatc m (cps3 t1 (Tlift k m)) end
with cps3_atom (t:term) {struct t}:cpsterm:=
match t with
| Var n => TVar n
| Lamb m t1 => TLamb (S m) (cps3 t1 (CVar O))
| Mu m t1 => TMu (S m) (cps3 t1 (CVar O))
|Con m tl =>
let fix cps3_atom_list (tl:list term) {struct tl}:list cpsterm:=
match tl with | nil => nil | a::m=>cps3_atom a :: cps3_atom_list m end in
TConstr m (cps3_atom_list tl)
| _ => TLamb (S O) (TVar O)
end.
Fixpoint cps3_list (tl0 : list term) ( k:cpsterm) {struct tl0}: cpsterm :=
match tl0 with
| nil => k
| a :: b => (cps3 a (TLamb 0 ( cps3_list b k )))
end .
Fixpoint cps3_plist (pl:list pat) (k:cpsterm) {struct pl}:list cpat:=
match pl with
| nil => nil | a::m => cps3_pat a k::cps3_plist m k end.
Fixpoint cps3_atom_list (tl:list term) {struct tl}:list cpsterm:=
match tl with | nil => nil | a::m=>cps3_atom a :: cps3_atom_list m end.
IV. CPS conversion of a program
Definition cps_comp (t:term) := cps3 t (TLamb 0 (CVar O)).