Library f2cps
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.