Library CPS
CPS: 4th intermediate language of MLCompCert
Author: Zaynah Dargaye
Created : 29th April 2009
Nml for substitution with 2 kind of variables : one for source variables (Tvar) and for continuation variables (Cvar) which are variables adding by CPS conversion. Each abstraction binds one more parameter which the continuation parameter.
Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
I. Syntax
Inductive cpsterm:Set:=
|TVar : nat->cpsterm
|CVar : nat ->cpsterm
| TLamb : nat -> cpsterm->cpsterm
| TMu : nat->cpsterm->cpsterm
| TApp : cpsterm->list cpsterm->cpsterm
| TLet :cpsterm->cpsterm->cpsterm
| TConstr : nat -> list cpsterm -> cpsterm
| TMatch : cpsterm -> list cpat -> cpsterm
with cpat :Set :=
| TPatc : nat -> cpsterm -> cpat.
II. Some smart constructions
Definition unApp (t t1:cpsterm) := TApp t (t1::nil).
Fixpoint catom (a:cpsterm):Prop:=
match a with
| TVar _ => True
| CVar _ =>True
| TLamb _ _ => True
| TConstr _ tl => let fix catom_list (al:list cpsterm) :Prop:=
match al with
| nil => True
|a::m=>catom a/\catom_list m
end in catom_list tl
|_ => False
end.
Fixpoint catom_list (al:list cpsterm) :Prop:=
match al with
| nil => True
|a::m=>catom a/\catom_list m
end .
Fixpoint is_catom (t:cpsterm) :bool:=
match t with
| TVar _ => true
| CVar _ =>true
| TLamb _ _ => true
| TMu _ _ =>true
|TConstr _ tl => let fix is_catom_list (al:list cpsterm) :bool:=
match al with
| nil => true
|a::m=>if (is_catom a) then is_catom_list m else false
end in is_catom_list tl
|_ => false
end.
Fixpoint is_catom_list (al:list cpsterm) :bool:=
match al with
| nil => true
|a::m=>if (is_catom a) then is_catom_list m else false
end.
Fixpoint Clift_rec (t:cpsterm) (ari:nat) {struct t}: cpsterm:=
match t with
| CVar i => if lt_ge_dec i ari then CVar i else CVar (i+1)
| TVar i => TVar i
| TLamb k b => TLamb k (Clift_rec b (S ari))
| TMu k b => TMu k (Clift_rec b (S ari))
| TApp t1 t2 =>
let fix Clift_list_rec (tl:list cpsterm) (n:nat) {struct tl}: list cpsterm:=
match tl with
| nil => nil
| a::m => (Clift_rec a n):: (Clift_list_rec m n)
end in
TApp (Clift_rec t1 ari) (Clift_list_rec t2 ari)
| TLet t1 t2 => TLet (Clift_rec t1 ari) (Clift_rec t2 ari)
| TConstr k tl =>
let fix Clift_list_rec (tl:list cpsterm) (ari:nat) {struct tl}:list cpsterm:=
match tl with
| nil => nil
| a::m => (Clift_rec a ari)::(Clift_list_rec m ari)
end in
TConstr k (Clift_list_rec tl ari)
|TMatch t pl =>
let fix Clift_patlist_rec (tl:list cpat) (ari:nat) {struct tl}:list cpat:=
match tl with
| nil => nil
| a::m => (Clift_pat_rec a ari)::(Clift_patlist_rec m ari)
end in
TMatch (Clift_rec t ari) (Clift_patlist_rec pl ari)
end
with Clift_pat_rec (p:cpat) ( ari:nat) {struct p}: cpat:=
match p with
| TPatc k t => TPatc k (Clift_rec t ari)
end.
Definition Clift (t:cpsterm) := Clift_rec t O.
Fixpoint Clift_list_rec (tl:list cpsterm) (n:nat) {struct tl}: list cpsterm:=
match tl with
| nil => nil
| a::m => (Clift_rec a n):: (Clift_list_rec m n)
end.
Fixpoint Clift_patlist_rec (tl:list cpat) (ari:nat) {struct tl}:list cpat:=
match tl with
| nil => nil
| a::m => (Clift_pat_rec a ari)::(Clift_patlist_rec m ari)
end.
Fixpoint Clift_list (tl:list cpsterm) {struct tl}: list cpsterm:=
match tl with
| nil => nil
| a::m => (Clift a)::(Clift_list m)
end.
Fixpoint Tlift_rec (t:cpsterm) (n:nat) (ari:nat){struct t}: cpsterm:=
match t with
| TVar i => if lt_ge_dec i n then TVar i else TVar (i+ari)
| CVar i => CVar i
| TLamb m b => TLamb m (Tlift_rec b (n+ m) ari)
| TMu m b => TMu m (Tlift_rec b (n+S m) ari)
| TApp t1 t2 =>
let fix Tlift_list_rec (tl:list cpsterm) (n:nat) (ari:nat) {struct tl}:list cpsterm:=
match tl with
| nil => nil
| a::m => (Tlift_rec a n ari)::(Tlift_list_rec m n ari)
end in
TApp (Tlift_rec t1 n ari) (Tlift_list_rec t2 n ari)
|TLet t1 t2 => TLet (Tlift_rec t1 n ari) (Tlift_rec t2 (S n) ari)
|TConstr m tl =>
let fix Tlift_list_rec (tl:list cpsterm) (n:nat) (ari:nat) {struct tl}:list cpsterm:=
match tl with
| nil => nil
| a::m => (Tlift_rec a n ari)::(Tlift_list_rec m n ari)
end in TConstr m (Tlift_list_rec tl n ari)
|TMatch t pl =>
let fix Tlift_patlist_rec (tl:list cpat) (n:nat) (ari:nat) {struct tl}:list cpat:=
match tl with
| nil => nil
| a::m => (Tlift_pat_rec a n ari)::(Tlift_patlist_rec m n ari)
end in
TMatch (Tlift_rec t n ari) (Tlift_patlist_rec pl n ari)
end
with Tlift_pat_rec (p:cpat) (n ari:nat) {struct p}: cpat:=
match p with
| TPatc k t => TPatc k (Tlift_rec t (n+ k) ari)
end.
Definition Tlift (t:cpsterm) (ari:nat) := Tlift_rec t O ari .
Fixpoint Tlift_list (tl:list cpsterm)(ari:nat) {struct tl}:list cpsterm:=
match tl with
| nil => nil
| a::m => (Tlift a ari)::(Tlift_list m ari)
end.
Fixpoint Tlift_list_rec (tl:list cpsterm) (n:nat) (ari:nat) {struct tl}:list cpsterm:=
match tl with
| nil => nil
| a::m => (Tlift_rec a n ari)::(Tlift_list_rec m n ari)
end.
Fixpoint Tlift_patlist_rec (tl:list cpat) (n:nat) (ari:nat) {struct tl}:list cpat:=
match tl with
| nil => nil
| a::m => (Tlift_pat_rec a n ari)::(Tlift_patlist_rec m n ari)
end .
Definition CTlift (t:cpsterm) (ari:nat) := (Clift (Tlift t ari)).
Fixpoint CTlift_list (tl:list cpsterm) (ari:nat) {struct tl}:list cpsterm:=
match tl with
| nil => nil
| a::m => (CTlift a ari)::(CTlift_list m ari)
end.
Inductive cps_case: Set:=
|clamb: cpsterm->cps_case
| other: cps_case.
Definition cps_case_of (t: cpsterm) :=
match t with
|TLamb 0 b => clamb b
| _ => other
end.
V. Induction scheme on CPS terms
Section cpsterm_ind_sect.
Variable
(P: cpsterm->Prop)
(Pl: list cpsterm -> Prop)
(Pp: cpat->Prop)
(Ppl: list cpat ->Prop).
Hypothesis
(Htv: forall n, P(TVar n) )
(Hcv: forall n, P (CVar n))
(Hl:forall ari t, P t -> P(TLamb ari t))
(Hmu:forall ari t, P t-> P(TMu ari t))
(Hlet: forall t1 t2, P t1 ->P t2 -> P (TLet t1 t2))
(Happ: forall t tl, P t -> Pl tl -> P (TApp t tl))
(Hconstr: forall n l, Pl l -> P (TConstr n l))
(Hm: forall t pl, P t -> Ppl pl -> P (TMatch t pl))
(Hnil : Pl nil)
(Hcons: forall t tl, P t -> Pl tl -> Pl (t::tl))
(Hpat: forall n t, P t -> Pp (TPatc n t))
(Hpnil: Ppl nil)
(Hpcons: forall p pl, Pp p -> Ppl pl-> Ppl (p::pl)).
Fixpoint cpsterm_ind2 (t:cpsterm): P t:=
match t as x return P x with
| TVar n => Htv n
|CVar n => Hcv n
|TLet t1 t2=> Hlet t1 t2 (cpsterm_ind2 t1) (cpsterm_ind2 t2)
|TLamb ari t => Hl ari t (cpsterm_ind2 t)
|TMu ari t => Hmu ari t (cpsterm_ind2 t)
|TApp t tl => Happ t tl (cpsterm_ind2 t)
((fix l_ind (tl: list cpsterm): Pl tl :=
match tl as x return Pl x with
| nil => Hnil
| a::m => Hcons a m (cpsterm_ind2 a) (l_ind m)end) tl)
|TConstr n l => Hconstr n l ((fix l_ind(tl: list cpsterm): Pl tl :=
match tl as x return Pl x with
| nil => Hnil
| a::m => Hcons a m (cpsterm_ind2 a) (l_ind m)end) l)
|TMatch t pl =>Hm t pl (cpsterm_ind2 t)
((fix pl_ind (pl:list cpat) {struct pl}: Ppl pl:=
match pl as x return Ppl x with
| nil => Hpnil
|a::m => Hpcons a m (pat_ind2 a) (pl_ind m)end)pl)
end
with pat_ind2 (p:cpat) {struct p}:Pp p:=
match p as x return Pp x with
|TPatc n t => Hpat n t (cpsterm_ind2 t)
end.
End cpsterm_ind_sect.