``` ```

# Naive CPS conversion

Author : Zaynah Dargaye

Created: 29th April 2009

Adaption of the algorithm of Plotkin. Conversion only uses in the proof of semantics preservation of our CPs conversion.
``` Require Import List. Require Import Coqlib. Require Import Coqlib2. Require Import Fml. Require Import CPS. ```
I. Smart constructors
``` Fixpoint mklist (n:nat) :list cpsterm:=  match n with  | O => nil  | S k => CVar k ::(mklist k) end. Fixpoint mkargs2 (targs:list cpsterm) (body:cpsterm) {struct targs}:cpsterm:=  match targs with  | nil => body  | a::m => (unApp a (TLamb 0 (mkargs2 m body)))  end. Definition Appn (tf:cpsterm) (targs:list cpsterm) (body:cpsterm):=  TLamb 0 (unApp tf (TLamb 0 (mkargs2 targs body))) . Definition Appn_body (ari:nat) :=     (TApp (CVar ari) ((CVar (S ari))::mklist ari)). Definition Constr_body (m ari:nat) :=  unApp (CVar ari) (TConstr m (mklist ari)). Definition mkL (ari:nat) (ope:list cpsterm) (body: cpsterm) :=  TLamb 0 (mkargs2 ope body). Definition mkConstr (ari:nat) (targs :list cpsterm):=  mkL ari targs (Constr_body ari (length targs) ). Fixpoint is_atom (f:term) :bool:=  match f with  | Var _ => true  | Lamb _ _ => true  | Mu _ _ =>true  |Con _ tl => let fix is_atom_list (al:list term) :bool:=                                     match al with                                     | nil => true                                     |a::m=>if (is_atom a) then is_atom_list m else false                                     end in is_atom_list tl  |_ => false end. Fixpoint is_atom_list (al:list term) :bool:= match al with   | nil => true   |a::m=>if (is_atom a) then is_atom_list m else false end. ```
II. Naive CPS conversion
``` Fixpoint ctrad (t:term) {struct t}:cpsterm:=  match t with | Var n => TLamb 0 (unApp (CVar O) (TVar n)) |Lamb m t1 => TLamb 0 (unApp (CVar O)                                  (TLamb (S m) (unApp (ctrad t1) (CVar O)))) | Mu m t1=> TLamb 0 (unApp (CVar O)                                  (TMu (S m) (unApp (ctrad t1) (CVar O)))) | App tf tl =>      let fix ctrad_list (tl:list term):=      match tl with      | nil => nil      | a::b => ctrad a::ctrad_list b      end in      Appn (ctrad tf) (ctrad_list tl) (Appn_body (length tl))  |tLet t1 t2 => TLamb 0 (unApp (ctrad t1)                              (TLamb 0 (TLet (CVar O)                                  (unApp (ctrad t2) (CVar 1)))))  | Con m tl =>       if is_atom_list tl then        let fix ctrad_atom_list (tl:list term):=          match tl with         | nil => nil         | a::b => ctrad_atom a::ctrad_atom_list b        end in TLamb 0 (unApp (CVar O) (TConstr m (ctrad_atom_list tl)))      else       let fix ctrad_list (tl:list term):=      match tl with      | nil => nil      | a::b => ctrad a::ctrad_list b      end in (mkConstr m (ctrad_list tl))  | Match t1 pl =>      let fix ctrad_plist (pl:list pat) :list cpat:=      match pl with      | nil => nil | a::m => ctrad_pat a::ctrad_plist m end    in    TLamb 0 (unApp (ctrad t1)               (TLamb 0 (TMatch (CVar O) (ctrad_plist pl)))) end with ctrad_pat (p:pat):cpat:=  match p with  | Patc m t1 => TPatc m (unApp (ctrad t1) (CVar 1)) end with ctrad_atom (t:term) {struct t}:cpsterm:=  match t with | Var n => TVar n | Lamb m t1 => TLamb (S m) (unApp (ctrad t1) (CVar O)) | Mu m t1 => TMu (S m) (unApp (ctrad t1) (CVar O)) | Con m tl =>      let fix ctrad_atom_list (tl:list term) {struct tl}:list cpsterm:=       match tl with | nil => nil | a::m=>ctrad_atom a :: ctrad_atom_list m end in      TConstr m (ctrad_atom_list tl) | _ => TLamb (S O) (TVar O)  end. Fixpoint ctrad_list (tl:list term){struct tl}:list cpsterm:=  match tl with  | nil => nil  | a::b => ctrad a::ctrad_list b  end. ```