Library Cpsopt

The CPs conversion of MLCompCert



Author : Zaynah Dargaye

Created: 29th April 2009

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